proposition: Lemma infinite_power5 n p m (x:=\aleph n) (y:= \aleph (n +o p)): ordinalp n -> ordinalp p -> m <> \0o -> cardinal p <=c m -> y ^c m = (x ^c m) *c (y ^c (cardinal p)).
proof: Proof. move=> on op mnz cpm. have cm := (proj32 cpm). have ca: cardinalp (x ^c m) by rewrite /cpow; fprops. pose hyp p:= cardinal p <=c m -> \aleph (n +o p) ^c m = x ^c m *c \aleph (n +o p) ^c (cardinal p). case:(least_ordinal6 hyp op); first by apply. set q :=least_ordinal _ _; move=> [oq pb] [] pa. have xnz: x <> \0c by apply: aleph_nz. move: (pa); rewrite - {1} (card_card cm) => pa'. case: (ordinal_limA oq) => h. by rewrite h cardinal_set0 (osum0r on) cpowx0 cprod1r. move:h=> [r or qv]. rewrite qv - osum2_succ //. have rq1: inc r q by rewrite qv; fprops. have cq:= (cleT (sub_smaller (ordinal_transitive oq rq1)) pa). move: (pb _ rq1 cq). set y1 := \aleph (n +o r); set y2 := \aleph (osucc (n +o r)). have onr: ordinalp (n +o r) by fprops. move: (infinite_power2 onr mnz); rewrite -/y1 -/y2 cpowcr => r1 r2. have osnr: ordinalp (osucc (n +o r)) by fprops. have cy1m: cardinalp (y1 ^c m) by rewrite /cpow; fprops. have icy2: infinite_c y2 by apply: CIS_aleph. have icy1: infinite_c y1 by apply: CIS_aleph. have icx: infinite_c x by apply: CIS_aleph. have y1nz: y1 <> \0c by apply: aleph_nz. have y2nz: y2 <> \0c by apply: aleph_nz. move: (icy1) (icy2) (icx) => [cy1 _ ] [cy2 _] [cx _]. have le1 :=(cpow_Mleeq m (aleph_le_lec (osum_Mle0 on or)) xnz). have le0 := (aleph_le_lec(proj1 (oltS (OS_sum2 on or)))). have le2:= (cpow_Mleeq m le0 y1nz). move: (cpow_Meqle y2nz pa'); rewrite !cpowcr qv => lexx. have paa:=(cpow_Mle1 (proj1 icx) mnz). have icxm:= (cle_inf_inf icx paa). have icy1m:= (cle_inf_inf icxm le1). have icy2m:= (cle_inf_inf icy1m le2). have y1mnz:=(cpow_nz y1nz (b:=m)). have xmnz := (cpow_nz xnz (b:=m)). case: (cleT_ee cy1m cy2) => r3. move: (cprod_inf r3 icy2 y1mnz). rewrite cprodC; move=> h; rewrite h in r1. rewrite r1; rewrite r1 in lexx. rewrite (cleA lexx (cpow_Mle1 cy2 (@osucc_nz r))). have r6: x ^c m <=c y2 by rewrite -r1; apply:cleT le1 le2. by rewrite cprodC (cprod_inf r6 icy2 xmnz). have r4 := (cprod_inf r3 icy1m y2nz). rewrite r4 in r1. have r6:= (cpow_nz y2nz (b := (osucc r))). case: (equal_or_not (x ^c m) (y1 ^c m)) => r7. by rewrite r7 -r1 (cprod_inf lexx icy2m r6). have r9: y1 ^c m = y1 ^c r. case:(cleT_ee (proj32 paa) (CS_pow y1 r)) => h. by rewrite r2 cprodC(cprod_inf h (cle_inf_inf icxm h) xmnz). by case: r7;rewrite - (cprod_inf h icxm (cpow_nz y1nz (b := r))) r2. have crr1:cardinal r <=c cardinal (osucc r). apply: sub_smaller; rewrite /osucc; fprops. move: (cpow_Mlele y1nz le0 crr1); rewrite !cpowcr -r9 -r1 => le3. by rewrite (cleA lexx le3) cprodC (cprod_inf (cleT le1 le2) icy2m xmnz). have onq:=(OS_sum2 on oq). apply cleA; last first. move: (CIS_pow (CIS_aleph onq) mnz) => r1. have r2 :=(cpow_Mleeq m (aleph_le_lec (osum_Mle0 on oq)) xnz). apply: (cprod_inf4 r2 _ r1);apply: cpow_Meqle => //; apply: (aleph_nz onq). set E := (fun_image q (fun z => \aleph (n +o z))). set f := Lg q (fun z => \aleph (n +o z)). have r2: E = range f by rewrite Lg_range. have r1 : \aleph (n +o q) = \osup E. move: (normal_ofs_compose aleph_normal (osum_normal on)) => [xa xb]. by move: (xb _ h) => /= ->. have fgf: fgraph f by rewrite /f; fprops. have r3: forall i, inc i (domain f) -> \2c <=c Vg f i. rewrite /f; aw; move=> i idf; rewrite LgV//; apply: infinite_ge2. apply: CIS_aleph; apply: (OS_sum2 on (Os_ordinal oq idf)). have r4: \aleph (n +o q) = csum f. rewrite r1 r2 - csum_of_small_b4 //. - move=> a ad; exact: (proj32 (r3 _ ad)). - by rewrite -r2 -r1; apply: CIS_aleph. - rewrite - r2 -r1 /f; aw. apply:cleT (aleph_le_lec (osum_M0le on oq)). rewrite - (card_card (CS_aleph oq)); exact: (ocle1 (aleph_pr6 oq)). have r5: \aleph (n +o q) <=c cprod f. rewrite r4; apply: compare_sum_prod2 => //. move=> i idf; move: (r3 _ idf) => [_ c _]; fprops. move: (cpow_Mleeq m r5 (aleph_nz onq)). rewrite cpow_prod {1} /f Lgd /cprodb. have ->: (Lg q (fun i => Vg f i ^c m)) = Lg q (fun t => x ^c m *c \aleph (n +o t) ^c (cardinal t)). apply: Lg_exten; move=> t tq. have tq1: t <o q by apply /(oltP oq). rewrite /f LgV//; apply (pb _ tq); apply: (cleT _ pa). apply:(ocle1 (proj1 tq1)). rewrite -/(cprodb q _) -prod_of_prods cprod_of_same - cpow_pow. have icq: infinite_c (cardinal q). apply: (cle_inf_inf CIS_omega). by move:(sub_smaller (proj33 (limit_ge_omega h))); rewrite cardinal_Nat. have ->: (m *c q) = m. have icm:= (cle_inf_inf icq pa). move: (cprod_inf pa icm (infinite_nz icq)). by rewrite cprod2cr. set f2:= \aleph (n +o q) ^c (cardinal q). set ff:= (fun i => \aleph (n +o i) ^c (cardinal i)). move => r6. have: cprod (Lg q ff) <=c f2 ^c (cardinal q). rewrite cpowcr - cprod_of_same /cst_graph. apply: cprod_increasing; aw; trivial. move=> t tq; rewrite (LgV tq) (LgV tq). have [tq1 _]: t <o q by apply /oltP. apply: cpow_Mlele (ocle1 tq1). apply: (aleph_nz (OS_sum2 on (proj31 tq1))). exact: (aleph_le_lec (osum_Meqle tq1 on)). rewrite /f2 - cpow_pow (csquare_inf icq) => r7. apply: (cleT r6); apply: (cprod_Mlele _ r7); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)