proposition: Lemma infinite_prod_pE (o2 := omega1 +o omega0): cprodb o2 \aleph = (\aleph o2) ^c aleph1.
proof: Proof. set o1 := \aleph \1o. have ico:= CIS_omega. have ioo:= OS_omega. have oo1: ordinalp o1 by apply: OS_aleph; apply: OS1. move: (CIS_aleph OS1) => io1. move /infinite_c_P2: (io1) => io2. have px: cprod (Lg o1 \aleph) = (\aleph o1 ^c o1) ^c omega0. rewrite - cpow_pow (cprod_inf io2 io1 omega_nz) //. set x := (Lg o1 \aleph). have qa: (fgraph x) by rewrite /x; fprops. have qb: (infinite_c (domain x)) by rewrite /x; aw. have qc: cardinal_pos_fam x. move; rewrite /x; aw => a ao; rewrite LgV//; apply: (aleph_nz1 (Os_ordinal oo1 ao)). have qd: fg_Mle_lec x. move; rewrite /x; aw; move => a b ax bx ab; rewrite !LgV//. exact (aleph_le_lec ab). move: (infinite_increasing_power qa qb qc qd). by rewrite /x; rewrite (ord_sup_aleph (aleph_limit OS1)); aw. have pa: cprod (Lg omega0 (fun z => (\aleph (o1 +o z)))) = (\aleph o2) ^c omega0. set x := (Lg omega0 (fun z => (\aleph (o1 +o z)))). have qa: (fgraph x) by rewrite /x; fprops. have qb: (infinite_c (domain x)) by rewrite /x; aw. have qc: cardinal_pos_fam x. move; rewrite /x; aw => a ao; rewrite LgV//; apply: aleph_nz1. by apply: OS_sum2 => //; apply (Os_ordinal ioo ao). have qd: fg_Mle_lec x. move;rewrite /x; aw; move => a b ax bx ab; rewrite !LgV//. exact (aleph_le_lec (osum_Meqle ab oo1)). move: (infinite_increasing_power qa qb qc qd). by rewrite /x; move => ->; aw; rewrite (ord_sup_aleph_sum oo1). have <- : cprod (Lg omega0 (fun z => (\aleph (o1 +o z) ^c o1))) = \aleph o2 ^c o1. move: pa; set f:= Lg omega0 _. have pb: fgraph f by rewrite /f; fprops. move: (cpow_prod o1 f); rewrite /cprodb. have -> : (Lg (domain f) (fun i => Vg f i ^c o1)) = (Lg omega0 (fun z => \aleph (o1 +o z) ^c o1)). rewrite /f; aw; apply: Lg_exten => t te;rewrite LgV//. move => <- ->. rewrite - cpow_pow cprodC (cprod_inf io2 io1 omega_nz) //. suff: cprodb omega0 (fun z => \aleph (o1 +o z) ^c o1) = cprodb omega0 (fun z => \aleph o1 ^c o1 *c \aleph (o1 +o z)). rewrite -/(cprodb omega0 _); move => ->. by rewrite - prod_of_prods (cprod_An1 \aleph oo1 ioo) cprod_of_same/cprodb px. rewrite /cprodb;set l1:= Lg _ _; set l2 := Lg _ _. have la: fgraph l1 by rewrite /l1; fprops. have lb: fgraph l2 by rewrite /l2; fprops. have lc: (domain l1 = domain l2) by rewrite /l1 /l2; aw. have ld: inc \0o (domain l1) by rewrite /l1; aw; apply /NatP; fprops. have oz: inc \0c omega0 by apply:NS0. have aux1: \aleph o1 ^c o1 <> \0c. apply: infinite_nz; apply: CIS_pow2; apply: CIS_aleph; fprops. have le: (Vg l1 \0c) <> \0c by rewrite /l1 LgV// (osum0r oo1). have lf: (Vg l2 \0c) <> \0c. rewrite /l2 LgV//. by rewrite (osum0r oo1); apply: cprod2_nz => //; apply: aleph_nz. have lg: (exists j, [/\ inc j (domain l1), j <> \0c, infinite_c (Vg l1 j), Vg l1 \0o <=c Vg l1 j & Vg l2 \0o <=c Vg l1 j]). have oo: inc \1o omega0 by apply:NS1. have d1: domain l1 = omega0 by rewrite /l1; aw. have i1d: inc \1o (domain l1) by ue. have le1: \aleph (o1 +o \0o) <=c \aleph (o1 +o \1o). apply: aleph_le_lec;apply: (osum_Meqle ole_01 oo1). exists \1o; split => //. - fprops. - rewrite /l1 LgV//; apply: CIS_pow2; apply: CIS_aleph; fprops. - rewrite /l1 ! LgV//; apply: cpow_Mleeq => //. apply: aleph_nz; apply: OS_sum2; fprops. rewrite /l1/l2 ! LgV// (osum0r oo1). set w := \aleph (o1 +o \1o) ^c o1. have sa: \aleph o1 <> \0c by apply: aleph_nz; fprops. have sb: \aleph o1 ^c o1 <=c w. apply: cpow_Mleeq => //; apply: aleph_le_lec. apply: osum_Mle0; fprops. have sc: \aleph o1 <=c \aleph o1 ^c o1. have co1: cardinalp (\aleph o1) by apply CS_aleph. apply: cpow_Mle1 => //;apply: aleph_nz => //; fprops. move: (cle_inf_inf (CIS_aleph oo1) sc) => i2. exact: (cleT (cprod_inf1 sc i2) sb). have lh: (forall j, inc j (domain l1) -> j = \0o \/ Vg l1 j = Vg l2 j). rewrite /l1 /l2; aw;move => j jb. case: (equal_or_not j \0o) => jnz;[by left | right; rewrite !LgV//]. move: (card_nat jb) => pd. have pb: \aleph \1o <> \0o by apply: aleph_nz; fprops. have pc: cardinal j <=c \aleph \1o. rewrite pd; apply: (cleT _ io2). by apply: cle_fin_inf => //; apply /NatP. have pe:=(CIS_aleph (OS_sum2 oo1 (OS_nat jb))). move: (infinite_power5 oo1 (Os_ordinal ioo jb) pb pc). rewrite cpowcr. by rewrite - /omega1 -/o1 (cpow_inf pe jb jnz). by rewrite (cprod_inf_eq la lb lc ld le lf lg lh). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)