1 by INT_2:def 4; A7: x>1 by INT_2:def 4; then x|^xca divides a by NAT_3:def 7; then A8: p|-count a1 =(p|-count a)-'(p|-count x|^xca) by A3,A5,NAT_3:31; x|^xcb divides b by A7,NAT_3:def 7; then A9: p|-count b1 = (p|-count b)-'(p|-count x|^xcb) by A4,A5,NAT_3:31; per cases; suppose x=p; then p|-count x|^xca = p|-count a by A6,NAT_3:25; hence thesis by A8,NAT_2:8; end; suppose A10: x<>p; p|-count x|^xcb=xcb * (p|-count x) by A5,NAT_3:32 .= xcb * 0 by A6,A10,NAT_3:24 .= 0; then A11: p|-count b1=(p|-count b)-0 by A9,XREAL_1:233 .=p|-count b; p|-count x|^xca=xca * (p|-count x) by A5,NAT_3:32 .= xca * 0 by A6,A10,NAT_3:24 .= 0; then p|-count a1=(p|-count a)-0 by A8,XREAL_1:233 .=p|-count a; hence thesis by A2,A5,A11; end; end; A12: for a being non zero Nat, x being Prime holds a div (x|^(x|-count a)) is non zero Nat proof let a be non zero Nat; let x be Prime; assume A13: not a div (x|^(x|-count a)) is non zero Nat; set xca=x|^(x|-count a); x>1 by INT_2:def 4; then A14: xca divides a by NAT_3:def 7; ex t being Nat st a = xca * (0 qua Nat) + t & t < xca by A13,NAT_D:def 1; hence contradiction by A14,NAT_D:7; end; defpred P[Nat] means for a,b being non zero Nat st card(support pfexp b)=\$1 holds (for p being Element of NAT st p is prime holds p |-count a <= p |-count b) implies (ex c being Element of NAT st b=a*c); let a,b be non zero Nat; assume A15: for p being Element of NAT st p is prime holds p |-count a <= p |-count b; A16: ex n1 being Element of NAT st n1=card(support pfexp b); A17: for n1,n2 being non zero Nat st n1 divides n2 holds (n2 div n1)*n1 = n2 proof let n1,n2 be non zero Nat; assume n1 divides n2; then ex a being Nat st n2=n1*a by NAT_D:def 3; hence thesis by NAT_D:18; end; A18: for b,b1 being non zero Nat, x being Prime, n being Element of NAT st card(support pfexp b)=n+1 & b1=b div (x|^(x|-count b)) & x in support pfexp b holds card(support pfexp b1)=n proof let b,b1 be non zero Nat; let x be Prime; let n be Element of NAT; assume A19: card(support pfexp b)=n+1; set xcb=x|-count b; assume A20: b1=b div (x|^(x|-count b)); A21: x>1 by INT_2:def 4; then x|^xcb divides b by NAT_3:def 7; then A22: b=b1*x|^xcb by A17,A20; reconsider b1 as Element of NAT by ORDINAL1:def 12; A23: b1,x are_coprime proof assume not b1,x are_coprime; then b1 gcd x = x by PEPIN:2; then x divides b1 by NAT_D:def 5; then consider c be Nat such that A24: b1=x*c by NAT_D:def 3; A25: not x|^(xcb+1) divides b by A21,NAT_3:def 7; x|^xcb divides b by A21,NAT_3:def 7; then b = x*c*x|^xcb by A17,A20,A24 .= c*(x|^xcb*x) .= c*x|^(xcb+1) by NEWTON:6; hence contradiction by A25,NAT_D:def 3; end; assume x in support pfexp b; then (pfexp b).x<>0 by PRE_POLY:def 7; then A26: xcb<>0 by NAT_3:def 8; reconsider b1 as non zero Nat; card support pfexp (x|^xcb*b1) = card support pfexp x|^xcb + card support pfexp b1 by A23,EULER_2:17,NAT_3:47; then n+1=card {x} + card support pfexp b1 by A19,A22,A26,NAT_3:42; then n+1=1+card (support pfexp b1) by CARD_2:42; hence thesis; end; A27: for n being Nat holds P[n] implies P[n+1] proof let n be Nat; assume A28: P[n]; for a,b being non zero Nat st card(support pfexp b)=n+1 holds (for p being Element of NAT st p is prime holds p |-count a <= p |-count b) implies ex c being Element of NAT st b=a*c proof let a,b be non zero Nat; assume A29: card(support pfexp b)=n+1; then support pfexp b<>{}; then consider x being object such that A30: x in support pfexp b; reconsider x as Prime by A30,NAT_3:34; set a1=a div (x|^(x|-count a)); set b1=b div (x|^(x|-count b)); reconsider a1,b1 as non zero Nat by A12; assume A31: for p being Element of NAT st p is prime holds p |-count a <= p |-count b; then A32: for p being Element of NAT st p is prime holds p |-count a1 <= p |-count b1 by A1; set xca=x|-count a; set xcb=x|-count b; x in NAT by ORDINAL1:def 12; then A33: xcb-xca=xcb-'xca by A31,XREAL_1:233; n in NAT by ORDINAL1:def 12; then card(support pfexp b1)=n by A18,A29,A30; then consider d be Element of NAT such that A34: b1=a1*d by A28,A32; reconsider e=d*x|^(xcb-'xca) as Element of NAT by ORDINAL1:def 12; take e; A35: x<>1 by INT_2:def 4; then A36: x|^(xca) divides a by NAT_3:def 7; x|^(xcb) divides b by A35,NAT_3:def 7; then b = d*(a div (x|^xca))*(x|^(xca+(xcb-'xca))) by A17,A34,A33 .= d*(a div (x|^xca))*(x|^xca*x|^(xcb-'xca)) by NEWTON:8 .= d*((a div (x|^xca))*x|^xca)*x|^(xcb-'xca) .= d*a*x|^(xcb-'xca) by A17,A36 .= a*(d*x|^(xcb-'xca)); hence thesis; end; hence thesis; end; A37: P[0] proof let a,b be non zero Nat; assume A38: card support pfexp b=0; (for p being Element of NAT st p is prime holds p |-count a <= p |-count b) implies ex c being Element of NAT st b=a*c proof set d=1; assume A39: for p being Element of NAT st p is prime holds p |-count a <= p |-count b; take d; A40: (support pfexp b)={} by A38; (support pfexp a)={} proof assume (support pfexp a)<>{}; then consider x be object such that A41: x in support pfexp a; reconsider x as Prime by A41,NAT_3:34; reconsider x as prime Element of NAT by ORDINAL1:def 12; (pfexp a).x<>0 by A41,PRE_POLY:def 7; then x|-count a<>0 by NAT_3:def 8; then x|-count b>0 by A39; then (pfexp b).x<>0 by NAT_3:def 8; hence contradiction by A40,PRE_POLY:def 7; end; then a=1 by NAT_3:52; hence thesis by A40,NAT_3:52; end; hence thesis; end; for n being Nat holds P[n] from NAT_1:sch 2(A37,A27); hence thesis by A15,A16; end; theorem Th21: for a,b being non zero Nat holds (for p being Element of NAT st p is prime holds p |-count a = p |-count b) implies a=b proof let a,b be non zero Nat; assume A1: for p being Element of NAT st p is prime holds p |-count a = p |-count b; then for p being Element of NAT st p is prime holds p |-count a <= p |-count b; then consider c being Element of NAT such that A2: b=a*c by Th20; for p being Element of NAT st p is prime holds p |-count b <= p |-count a by A1; then consider d being Element of NAT such that A3: a=b*d by Th20; a=a*(c*d) by A2,A3; then c = 1 by NAT_1:15,XCMPLX_1:7; hence thesis by A2; end; theorem Th22: for p1,p2 being Prime, m being non zero Element of NAT st p1|^( p1 |-count m) = p2|^(p2 |-count m) & p1 |-count m > 0 holds p1=p2 proof let p1,p2 be Prime; let m be non zero Element of NAT; assume A1: p1|^(p1 |-count m) = p2|^(p2 |-count m); A2: p1 > 1 by INT_2:def 4; assume p1 |-count m > 0; then p1 to_power (p1 |-count m) > 1 by A2,POWER:35; then A3: p1|^(p1|-count m) > 1 by POWER:41; assume p1 <> p2; then p1 <> 1 & not p1 divides p2|^(p2 |-count m) by INT_2:def 4,NAT_3:6; then p1 |-count (p1|^(p1 |-count m)) = 0 by A1,NAT_3:27; then p1 |-count m = 0 by A2,NAT_3:25; hence contradiction by A3,NEWTON:4; end; begin :: Pocklington's theorem. theorem Th23: for n,k,q,p,n1,p,a being Element of NAT st n-1=k*q|^n1 & k>0 & n1>0 & q is prime & a|^(n-'1) mod n = 1 & p is prime & p divides n holds p divides (a|^((n-'1) div q) -' 1) or p mod q|^n1 = 1 proof let n,k,q,p,n1,p,a be Element of NAT; assume that A1: n-1=k*q|^n1 and A2: k>0 and A3: n1>0 and A4: q is prime; A5: n-1+1 > 0+1 by A1,A2,A4,XREAL_1:6; assume A6: a|^(n-'1) mod n = 1; a|^((n-'1) div q)>=1 proof assume a|^((n-'1) div q)<1; then A7: a=0 by NAT_1:14; n-'1 + 1 > 1 by A5,XREAL_1:233; then n-'1 >= 1 by NAT_1:13; then a|^(n-'1) mod n = 0*n mod n by A7,NEWTON:11 .= 0 by NAT_D:13; hence contradiction by A6; end; then A8: a|^((n-'1) div q)-'1=a|^((n-'1) div q)-1 by XREAL_1:233; n1+1 > 0+1 by A3,XREAL_1:6; then n1>=1 by NAT_1:13; then A9: n1-'1=n1-1 by XREAL_1:233; then A10: (n-'1) div q = (q|^(n1-'1+1))*k div q by A1,A5,XREAL_1:233 .=q*q|^(n1-'1)*k div q by NEWTON:6 .=q*(q|^(n1-'1)*k) div q .=k*q|^(n1-'1) by A4,NAT_D:18; assume that A11: p is prime and A12: p divides n; consider i being Nat such that A13: n=p*i by A12,NAT_D:def 3; assume not p divides (a|^((n-'1) div q)-'1); then A14: not a|^((n-'1) div q) mod p = 1 by A11,A8,PEPIN:8; set nn=n-'1; n1+1 > 0+1 by A3,XREAL_1:6; then n1>=1 by NAT_1:13; then A15: n1-'1=n1-1 by XREAL_1:233; A16: p > 1 by A11,INT_2:def 4; then p-'1=p-1 by XREAL_1:233; then A17: p-'1+1=p; reconsider i as Element of NAT by ORDINAL1:def 12; i*p<>0 by A1,A13; then A18: a|^(n-'1) mod p = 1 by A6,A16,A13,PEPIN:9; 0+1 1 by A4,INT_2:def 4; hence thesis by A3,A17,A22,NAT_D:16,PEPIN:25; end; theorem Th24: for n,f,c being Element of NAT st n-1=f*c & f>c & c>0 & (for q being Element of NAT st q divides f & q is prime holds ex a being Element of NAT st a|^(n-'1) mod n = 1 & (a|^((n-'1) div q)-'1) gcd n = 1) holds n is prime proof let n,f,c be Element of NAT; assume that A1: n-1=f*c and A2: f>c and A3: c>0; A4: n-1+1>0+1 by A1,A2,A3,XREAL_1:6; assume A5: for q being Element of NAT st q divides f & q is prime holds ex a being Element of NAT st a|^(n-'1) mod n = 1 & (a|^((n-'1) div q)-'1) gcd n = 1; assume not n is prime; then consider p be Element of NAT such that A6: p divides n and A7: 1

1-1 by A7,XREAL_1:9; then A12: p-'1>0 by A7,XREAL_1:233; A13: for q1 being Element of NAT st q1 in support (pfexp f) & q1 |-count f > 0 holds p mod q1|^(q1 |-count f) = 1 proof let q1 be Element of NAT; set n1=q1 |-count f; assume A14: q1 in support (pfexp f); then A15: q1 is prime by NAT_3:34; A16: q1 is prime by A14,NAT_3:34; then consider a be Element of NAT such that A17: a|^(n-'1) mod n = 1 and A18: (a|^((n-'1) div q1)-'1) gcd n = 1 by A5,A14,NAT_3:36; assume A19: q1 |-count f > 0; A20: not p divides (a|^((n-'1) div q1)-'1) by A6,NEWTON:50,A7,A18,NAT_D:7; q1<>1 by A16,INT_2:def 4; then q1|^(q1 |-count f) divides f by A2,NAT_3:def 7; then consider d be Nat such that A21: f=q1|^n1*d by NAT_D:def 3; reconsider d as Element of NAT by ORDINAL1:def 12; set k=d*c; A22: k>0 proof assume k<=0; then d=0 by A3; hence contradiction by A2,A21; end; n-1=k*q1|^n1 by A1,A21; hence thesis by A6,A9,A19,A17,A22,A15,A20,Th23; end; for q1 being Element of NAT st q1 is prime holds q1 |-count f <= q1 |-count (p-'1) proof let q1 be Element of NAT; assume A23: q1 is prime; per cases; suppose A24: q1 in support (pfexp f); then (pfexp f).q1<>0 by PRE_POLY:def 7; then q1 |-count f>0 by A23,NAT_3:def 8; then p mod q1|^(q1 |-count f) = 1 by A13,A24; then A25: q1 |-count (q1|^(q1 |-count f)) <= q1 |-count (p-'1) by A11,A10,A23, NAT_3:30,PEPIN:8; q1>1 by A23,INT_2:def 4; hence thesis by A25,NAT_3:25; end; suppose not q1 in support (pfexp f); then (pfexp f).q1=0 by PRE_POLY:def 7; hence thesis by A23,NAT_3:def 8; end; end; then ex n2 being Element of NAT st (p-'1)=f*n2 by A2,A12,Th20; then f divides (p-'1) by NAT_D:def 3; then f<=(p-'1) by A12,NAT_D:7; then p-1+1>=f+1 by A10,XREAL_1:6; then p>f by NAT_1:13; then A26: p^2>f^2 by SQUARE_1:16; c>=0+1 by A3,NAT_1:13; then A27: c+1>=1+1 by XREAL_1:6; f>=c+1 by A2,NAT_1:13; then f>=2 by A27,XXREAL_0:2; then f-1>=2-1 by XREAL_1:9; then A28: n+(f-1)>=n+1 by XREAL_1:6; f>=c+1 by A2,NAT_1:13; then f*f>=f*(c+1) by XREAL_1:64; then p^2>f+(n-1) by A1,A26,XXREAL_0:2; then p^2>=n+1 by A28,XXREAL_0:2; hence contradiction by A8,NAT_1:13; end; ::\$N Pocklington's theorem theorem Th25: for n,f,d,n1,a,q being Element of NAT st n-1=q|^n1*d & q|^n1>d & d>0 & q is prime & a|^(n-'1) mod n = 1 & (a|^((n-'1) div q)-'1) gcd n = 1 holds n is prime proof let n,f,d,n1,a,q be Element of NAT; assume that A1: n-1=q|^n1*d & q|^n1>d & d>0 and A2: q is prime; set f=q|^n1; assume A3: a|^(n-'1) mod n = 1; assume A4: (a|^((n-'1) div q)-'1) gcd n = 1; for q1 being Element of NAT st q1 divides f & q1 is prime holds ex a being Element of NAT st a|^(n-'1) mod n = 1 & (a|^((n-'1) div q1)-'1) gcd n = 1 proof let q1 be Element of NAT; assume A5: q1 divides f; assume A6: q1 is prime; consider a be Element of NAT such that A7: a|^(n-'1) mod n = 1 & (a|^((n-'1) div q)-'1) gcd n = 1 by A3,A4; take a; thus thesis by A2,A5,A6,A7,Th18; end; hence thesis by A1,Th24; end; Lm2: for n being Element of NAT st 1 0) holds Product F > 0 proof defpred P[Nat] means for F being FinSequence of REAL st (for k being Element of NAT st k in dom F holds F.k > 0) & len F = \$1 holds Product F > 0; let F be FinSequence of REAL; A1: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A2: P[n]; for F being FinSequence of REAL st (for k being Element of NAT st k in dom F holds F.k > 0) & len F = n+1 holds Product F > 0 proof let F be FinSequence of REAL; assume A3: for k being Element of NAT st k in dom F holds F.k > 0; assume A4: len F = n+1; then consider F1,F2 being FinSequence of REAL such that A5: len F1 = n and A6: len F2 = 1 and A7: F=F1^F2 by FINSEQ_2:23; 1 in Seg 1 by FINSEQ_1:3; then 1 in dom F2 by A6,FINSEQ_1:def 3; then A8: F.(n+1) = F2.1 by A5,A7,FINSEQ_1:def 7; for k being Element of NAT st k in dom F1 holds F1.k > 0 proof let k be Element of NAT; assume A9: k in dom F1; then F.k > 0 by A3,A7,FINSEQ_2:15; hence thesis by A7,A9,FINSEQ_1:def 7; end; then A10: Product F1 > 0 by A2,A5; set x=F2.1; Seg (n+1) = dom F by A4,FINSEQ_1:def 3; then A11: x > 0 by A3,A8,FINSEQ_1:3; Product F = Product (F1^<*x*>) by A6,A7,FINSEQ_1:40 .= Product F1 * x by RVSUM_1:96; hence thesis by A10,A11; end; hence thesis; end; A12: P[0] proof let F be FinSequence of REAL such that for k being Element of NAT st k in dom F holds F.k > 0; assume len F = 0; then F = <*>REAL; hence thesis by RVSUM_1:94; end; A13: for n being Nat holds P[n] from NAT_1:sch 2(A12,A1); A14: ex n being Element of NAT st n = len F; assume for k being Element of NAT st k in dom F holds F.k > 0; hence thesis by A13,A14; end; theorem Th42: for X1 being set, X2 being finite set st X1 c= X2 & X2 c= NAT & not {} in X2 holds Product Sgm X1 <= Product Sgm X2 proof let X1 be set; defpred P[Nat] means for X1 being set, X2 being finite set st X1 c= X2 & X2 c= NAT & (not {} in X2) & card X2 = \$1 holds Product Sgm X1 <= Product Sgm X2; A1: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A2: P[n]; now let X1 be set; let X2 be finite set; assume that A3: X1 c= X2 and A4: X2 c= NAT and A5: not {} in X2 and A6: card X2 = n+1; set A=X2; reconsider A as finite non empty real-membered set by A4,A6; set m = max A; set X11=X1 \ {m}; set X12=X2 \ {m}; A7: m in X2 by XXREAL_2:def 8; then A8: X12 \/ {m} = X2 by ZFMISC_1:116; A9: X12 /\ {m} = (X2 /\ {m}) \ {m} by XBOOLE_1:49 .= {m} \ {m} by A7,ZFMISC_1:46 .= {} by XBOOLE_1:37; card(X12\/{m})=card X12 + card {m} - card(X12 /\{m}) by CARD_2:45; then A10: card X2 = card X12 + 1 - card {} by A8,A9,CARD_1:30; reconsider m as Element of NAT by A4,A7; A11: X11 c= X12 by A3,XBOOLE_1:33; A12: X12 c= X2 by XBOOLE_1:36; then A13: X12 c= NAT & not {} in X12 by A4,A5; then A14: Product Sgm X11 <= Product Sgm X12 by A2,A3,A6,A10,XBOOLE_1:33; now let x be object; set r=x; assume A15: x in X12; then x in A by A12; then reconsider r as Element of NAT by A4; not r=0 by A5,A12,A15; then 0+1 < r+1 by XREAL_1:6; then A16: 1 <= r by NAT_1:13; r <= m by A12,A15,XXREAL_2:def 8; hence x in Seg m by A16,FINSEQ_1:1; end; then A17: X12 c= Seg m; A18: not m=0 by A5,XXREAL_2:def 8; then 0+1 < m+1 by XREAL_1:6; then A19: 1 <= m by NAT_1:13; then m in Seg m by FINSEQ_1:1; then A20: {m} c= Seg m by ZFMISC_1:31; now let n1,n2 be Nat; assume that A21: n1 in X12 and A22: n2 in {m}; not n1 in {m} by A21,XBOOLE_0:def 5; then A23: n1<>m by TARSKI:def 1; n2=m & n1 <= m by A12,A21,A22,TARSKI:def 1,XXREAL_2:def 8; hence n1 < n2 by A23,XXREAL_0:1; end; then Product Sgm X2 = Product((Sgm X12) ^ (Sgm {m})) by A8,A17,A20, FINSEQ_3:42; then A24: Product Sgm X2 = (Product (Sgm X12))*(Product (Sgm {m})) by RVSUM_1:97 .= (Product (Sgm X12))*(Product <*m*>) by A18,FINSEQ_3:44 .= (Product (Sgm X12))*m by RVSUM_1:95; A25: 1*Product (Sgm X12) <= m*Product (Sgm X12) by A19,XREAL_1:64; per cases; suppose A26: m in X1; A27: now let n1,n2 be Nat; assume that A28: n1 in X11 and A29: n2 in {m}; not n1 in {m} by A28,XBOOLE_0:def 5; then A30: n1<>m by TARSKI:def 1; n1 in X12 by A11,A28; then A31: n1 <= m by A12,XXREAL_2:def 8; n2=m by A29,TARSKI:def 1; hence n1 < n2 by A30,A31,XXREAL_0:1; end; now let x be object; set r=x; assume x in X11; then A32: x in X1 by XBOOLE_0:def 5; then x in A by A3; then reconsider r as Element of NAT by A4; not r=0 by A3,A5,A32; then 0+1 < r+1 by XREAL_1:6; then A33: 1 <= r by NAT_1:13; r <= m by A3,A32,XXREAL_2:def 8; hence x in Seg m by A33,FINSEQ_1:1; end; then A34: X11 c= Seg m; X1 = X11 \/ {m} by A26,ZFMISC_1:116; then Product Sgm X1 = Product((Sgm X11) ^ (Sgm {m})) by A20,A34,A27, FINSEQ_3:42 .= (Product (Sgm X11))*(Product (Sgm {m})) by RVSUM_1:97 .= (Product (Sgm X11))*(Product <*m*>) by A18,FINSEQ_3:44 .= (Product (Sgm X11))*m by RVSUM_1:95; hence Product Sgm X1 <= Product Sgm X2 by A2,A6,A11,A10,A13,A24, XREAL_1:64; end; suppose not m in X1; then Product Sgm X1 <= Product Sgm X12 by A14,ZFMISC_1:57; hence Product Sgm X1 <= Product Sgm X2 by A24,A25,XXREAL_0:2; end; end; hence thesis; end; let X2 be finite set; assume A35: X1 c= X2 & X2 c= NAT & not {} in X2; A36: ex n being Element of NAT st card X2 = n; A37: P[0] proof let X1 be set; let X2 be finite set; assume that A38: X1 c= X2 and X2 c= NAT and not {} in X2 and A39: card X2 = 0; X2={} by A39; hence thesis by A38,XBOOLE_1:3; end; for n being Nat holds P[n] from NAT_1:sch 2(A37,A1); hence thesis by A35,A36; end; theorem Th43: for a,k being Element of NAT, X being set, F being FinSequence of SetPrimes, p being Prime st X c= SetPrimes & X c= Seg k & F = Sgm X & a = Product F holds (p in rng F implies p |-count a = 1) & (not p in rng F implies p |-count a = 0) proof let a,k be Element of NAT, X be set, F be FinSequence of SetPrimes, p be Prime; defpred P[Nat] means for a,k being Element of NAT, X being set, F being FinSequence of SetPrimes, p being Prime st X c= SetPrimes & X c= Seg k & F = Sgm X & a = Product F & len F = \$1 holds (p in rng F implies p |-count a = 1) & (not( p in rng F) implies p |-count a = 0); now let F be FinSequence of SetPrimes; rng F c= REAL; hence F is FinSequence of REAL by FINSEQ_1:def 4; end; then reconsider F as FinSequence of REAL; A1: ex n being Element of NAT st n = len F; A2: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A3: P[n]; for a,k being Element of NAT, X being set, F being FinSequence of SetPrimes, p being Prime st X c= SetPrimes & X c= Seg k & F = Sgm X & a = Product F & len F = n+1 holds (p in rng F implies p |-count a = 1) & (not p in rng F implies p |-count a = 0) proof let a,k be Element of NAT, X be set, F be FinSequence of SetPrimes, p be Prime; assume that A4: X c= SetPrimes and A5: X c= Seg k and A6: F = Sgm X and A7: a = Product F; set x = F.(n+1); assume A8: len F = n+1; then A9: Seg (n+1) = dom F by FINSEQ_1:def 3; then n+1 in dom F by FINSEQ_1:3; then A10: x in rng F by FUNCT_1:def 3; rng F c= SetPrimes by FINSEQ_1:def 4; then reconsider x as Prime by A10,NEWTON:def 6; set X1 = X \ {x}; A11: X1 c= X by XBOOLE_1:36; then A12: X1 c= Seg k by A5; A13: rng F = X by A5,A6,FINSEQ_1:def 13; now let y be object; assume y in {x}; then y=x by TARSKI:def 1; hence y in Seg k by A5,A10,A13; end; then A14: {x} c= Seg k; A15: for m1,n1 being Nat st m1 in X1 & n1 in {x} holds m1 < n1 proof set n9=n+1; let m1,n1 be Nat; assume that A16: m1 in X1 and A17: n1 in {x}; set l=(F").m1; A18: F is one-to-one by A5,A6,FINSEQ_3:92; m1 in rng F by A11,A13,A16; then m1 in dom (F") by A18,FUNCT_1:33; then l in rng (F") by FUNCT_1:def 3; then A19: l in Seg (n+1) by A9,A18,FUNCT_1:33; then reconsider l as Element of NAT; A20: l <= n+1 by A19,FINSEQ_1:1; A21: m1=F.l by A11,A13,A16,A18,FUNCT_1:35; then not n9=l by A16,ZFMISC_1:56; then A22: l < n9 by A20,XXREAL_0:1; A23: n1=F.n9 by A17,TARSKI:def 1; 1<= l by A19,FINSEQ_1:1; hence thesis by A5,A6,A8,A21,A23,A22,FINSEQ_1:def 13; end; set F2 = Sgm {x}; set F1 = Sgm X1; reconsider F1 as FinSequence of NAT; set a1 = Product F1; A24: F2 = <*x*> by FINSEQ_3:44; then A25: rng F2 = {x} by FINSEQ_1:39; A26: X1 \/ {x} = X \/ {x} by XBOOLE_1:39 .= X by A10,A13,ZFMISC_1:40; then A27: F = F1 ^ F2 by A6,A12,A14,A15,FINSEQ_3:42; then rng F c= SetPrimes & rng F1 c= rng F by FINSEQ_1:29,def 4; then A28: rng F1 c= SetPrimes; len F = len F1 + len F2 by A27,FINSEQ_1:22; then A29: n+1=len F1 + 1 by A8,A24,FINSEQ_1:39; reconsider F1 as FinSequence of SetPrimes by A28,FINSEQ_1:def 4; A30: F1 is FinSequence of REAL by FINSEQ_2:24,NUMBERS:19; now let k be Element of NAT; assume k in dom F1; then F1.k in rng F1 by FUNCT_1:def 3; then F1.k is Prime by A28,NEWTON:def 6; hence F1.k>0; end; then A31: a1<>0 by Th41,A30; Product F = Product (F1^F2) by A6,A12,A14,A15,A26,FINSEQ_3:42 .= Product (F1^<*x*>) by FINSEQ_3:44 .= Product F1 * x by RVSUM_1:96; then A32: p |-count a = (p |-count a1) + (p |-count x) by A7,A31,NAT_3:28; A33: X1 c= SetPrimes by A4,A11; A34: rng F1 = X \ {x} by A12,FINSEQ_1:def 13; A35: now assume p in rng F; then p in (rng F1 \/ rng F2) by A27,FINSEQ_1:31; then A36: p in rng F1 or p in {x} by A25,XBOOLE_0:def 3; A37: p>1 by INT_2:def 4; per cases by A36,TARSKI:def 1; suppose A38: p in rng F1; then not p in {x} by A34,XBOOLE_0:def 5; then p<>x by TARSKI:def 1; then p |-count x = 0 by A37,NAT_3:24; hence p |-count a=1 by A3,A33,A12,A29,A32,A38; end; suppose A39: p=x; then p in {x} by TARSKI:def 1; then not p in rng F1 by A34,XBOOLE_0:def 5; then p |-count a1 = 0 by A3,A33,A12,A29; hence p |-count a=1 by A32,A37,A39,NAT_3:22; end; end; now assume not p in rng F; then A40: not p in (rng F1 \/ rng F2) by A27,FINSEQ_1:31; then not p in {x} by A25,XBOOLE_0:def 3; then A41: p<>x by TARSKI:def 1; not p in rng F1 by A40,XBOOLE_0:def 3; then A42: p |-count a1 = 0 by A3,A33,A12,A29; p<>1 by INT_2:def 4; hence p |-count a=0 by A32,A42,A41,NAT_3:24; end; hence thesis by A35; end; hence thesis; end; A43: P[0] proof let a,k be Element of NAT, X be set, F be FinSequence of SetPrimes, p be Prime; assume that X c= SetPrimes and X c= Seg k and F = Sgm X and A44: a = Product F and A45: len F = 0; A46: F=<*>REAL by A45; assume A47: not(p in rng F implies p |-count a = 1) or not(not p in rng F implies p |-count a = 0); per cases by A47; suppose not(p in rng F implies p |-count a = 1); hence contradiction by A46; end; suppose A48: not(not p in rng F implies p |-count a = 0); F = <*>SetPrimes by A45; then a=1 & p<>1 by A44,INT_2:def 4,RVSUM_1:94; hence contradiction by A48,NAT_3:21; end; end; for n being Nat holds P[n] from NAT_1:sch 2(A43,A2); hence thesis by A1; end; theorem Th44: for n being Element of NAT holds Product Sgm{p where p is prime Element of NAT:p<=n+1} <= 4 to_power n proof defpred P[Nat] means Product Sgm{p where p is prime Element of NAT:p<=\$1+1} <=(4 to_power \$1); let n be Element of NAT; A1: for m being Nat st (for n being Nat st n < m holds P[n]) holds P[m] proof let m be Nat; assume A2: for n being Nat st n < m holds P[n]; per cases by XXREAL_0:1; suppose A3: m<1; A4: now assume {p where p is prime Element of NAT:p<=0+1}<>{}; then consider y being object such that A5: y in {p where p is prime Element of NAT:p<=1} by XBOOLE_0:def 1; ex y9 being prime Element of NAT st y9=y & y9<=1 by A5; hence contradiction by Lm1; end; m=0 by A3,NAT_1:14; hence thesis by A4,FINSEQ_3:43,POWER:24,RVSUM_1:94; end; suppose A6: m=1; A7: 4 to_power 1=4 by POWER:25; A8: now let y be object; assume y in {p where p is prime Element of NAT:p<=2}; then consider y9 being prime Element of NAT such that A9: y9=y & y9<=2; y9>1 by Lm1; then y9>=1+1 by NAT_1:13; hence y=2 by A9,XXREAL_0:1; end; for y being object st y = 2 holds y in {p where p is prime Element of NAT:p<=2} by INT_2:28; then A10: {p where p is prime Element of NAT:p<=2}={2} by A8,TARSKI:def 1; Product Sgm{2}=Product <*2*> by FINSEQ_3:44 .=2 by RVSUM_1:95; hence thesis by A6,A10,A7; end; suppose A11: m>1; per cases; suppose m+1 is odd; then consider k being Nat such that A12: m+1=2*k+1 by ABIAN:9; A13: (2*k+1) choose k<=2 to_power (2*k) proof defpred Q[Nat] means (2*\$1+1) choose \$1<=2 to_power (2*\$1 ); A14: for k being Nat st Q[k] holds Q[k+1] proof let k be Nat; set r=2*k+1-k; set r9=2*k+3-(k+1); set r99=k+1; A15: 2*((2 to_power (2*k))*2)= 2*((2 to_power (2*k))*(2 to_power 1)) by POWER:25 .= 2*(2 to_power (2*k+1)) by POWER:27 .= (2 to_power 1)*(2 to_power (2*k+1)) by POWER:25 .= (2 to_power (1+2*k+1)) by POWER:27; A16: k+1>=0; then reconsider r as Element of NAT; A17: 2*k+1-k+k>=0+k by A16,XREAL_1:6; 2*k+3<2*k+4 by XREAL_1:6; then (2*k+3)/(k+2)<(2*(k+2))/(k+2) by XREAL_1:74; then (2*k+3)/(k+2)<2*((k+2)/(k+2)) by XCMPLX_1:74; then A18: (2*k+3)/(k+2)<2*1 by XCMPLX_1:60; assume (2*k+1) choose k<=2 to_power (2*k); then ((2*k+1) choose k)*((2*k+3)/(k+2))<=(2 to_power (2*k))*2 by A18,XREAL_1:66; then A19: 2*(((2*k+1) choose k)*((2*k+3)/(k+2)))<=2*((2 to_power (2*k ))*2) by XREAL_1:64; A20: k+2>=0; then reconsider r9 as Element of NAT; (r99!)*(r9!) = (k!)*(k+1)*((r+1)!) by NEWTON:15 .=(k!)*(k+1)*((r!)*(r+1)) by NEWTON:15 .=(k!)*(r!)*(k+1)*(r+1); then A21: ((k!)*(r!))/((r99!)*(r9!)) =((k!)*(r!))/(((k!)*(r!))*((k+1)* (r+1))) .=((k!)*(r!))/((k!)*(r!))/((k+1)*(r+1)) by XCMPLX_1:78 .= 1/((k+1)*(r+1)) by XCMPLX_1:60; A22: (2*k+1)! = (2*k+1)!/((k!)*(r!))*((k!)*(r!)) by XCMPLX_1:87 .=((2*k+1) choose k)*((k!)*(r!)) by A17,NEWTON:def 3; 2*k+3-r99+r99>=0+r99 by A20,XREAL_1:6; then (2*(k+1)+1) choose (k+1) = (2*k+2+1)!/((r99!)*(r9!)) by NEWTON:def 3 .= (((2*k+1+1)!)*(2*k+3))/((r99!)*(r9!)) by NEWTON:15 .= (((2*k+1)!)*(2*k+2)*(2*k+3))/((r99!)*(r9!)) by NEWTON:15 .= ((2*k+2)*(2*k+3))*((2*k+1)!)/((r99!)*(r9!)) .= 2*(k+1)*(2*k+3)* ((((2*k+1) choose k)* ((k!)*(r!))/((r99!)* (r9!)))) by A22,XCMPLX_1:74 .= 2*(k+1)*(2*k+3)*(((2*k+1) choose k)* ((((k!)*(r!))/((r99!)* (r9!))))) by XCMPLX_1:74 .= 2*(k+1)*(2*k+3)*((2*k+1) choose k)*(1/((k+1)*(r+1))) by A21 .= (2*((2*k+1) choose k))* ((k+1)*(2*k+3))/((k+1)*(r+1)) by XCMPLX_1:99 .= (2*((2*k+1) choose k))*(((k+1)*(2*k+3))/((k+1)*(r+1))) by XCMPLX_1:74 .= 2*((2*k+1) choose k)*(((k+1)/(k+1))*((2*k+3)/(r+1))) by XCMPLX_1:76 .= 2*((2*k+1) choose k)*(1*((2*k+3)/(r+1))) by XCMPLX_1:60 .= 2*((2*k+1) choose k)*((2*k+3)/(k+2)); hence thesis by A15,A19; end; (2*0+1) choose 0 = 1 by NEWTON:19; then A23: Q[0] by POWER:24; for k being Nat holds Q[k] from NAT_1:sch 2(A23,A14); hence thesis; end; set Y={p where p is prime Element of NAT:p>k+1 & p<=2*k+1}; set SY = Sgm Y; A24: rng SY c= REAL; set X={p where p is prime Element of NAT:p<=k+1}; set SX = Sgm X; rng SX c= REAL; then reconsider SX as FinSequence of REAL by FINSEQ_1:def 4; m/2=(k*2)/2 by A12; then A25: Product SX<=(4 to_power k) by A2,A11,XREAL_1:216; for y being object holds y in X implies y in Seg (k+1) proof let y be object; assume y in X; then A26: ex y9 being prime Element of NAT st y9=y & y9<=k+1; then reconsider y as prime Element of NAT; y>=1 by Lm1; hence thesis by A26,FINSEQ_1:1; end; then A27: X c= Seg (k+1); for k9 being Element of NAT st k9 in dom SX holds SX.k9 > 0 proof let k9 be Element of NAT; assume A28: k9 in dom SX; rng SX = X by A27,FINSEQ_1:def 13; then SX.k9 in X by A28,FUNCT_1:3; then ex y9 being prime Element of NAT st y9=SX.k9 & y9<=k+1; hence thesis; end; then A29: 0<=Product SX by Th41; reconsider SY as FinSequence of REAL by A24,FINSEQ_1:def 4; A30: for a,b being Nat st a in X & b in Y holds a < b proof let a,b be Nat; assume a in X; then A31: ex y9 being prime Element of NAT st y9=a & y9<=k+1; assume b in Y; then ex y99 being prime Element of NAT st y99=b & y99>k+1 & y99<=2*k +1; hence thesis by A31,XXREAL_0:2; end; for y being object holds y in Y implies y in Seg (2*k+1) proof let y be object; assume y in Y; then A32: ex y9 being prime Element of NAT st y9=y & y9>k+1 & y9<=2*k+1; then reconsider y as prime Element of NAT; y>=1 by Lm1; hence thesis by A32,FINSEQ_1:1; end; then A33: Y c= Seg (2*k+1); A34: for k9 being Element of NAT st k9 in dom SY holds SY.k9 > 0 proof let k9 be Element of NAT; assume A35: k9 in dom SY; rng SY = Y by A33,FINSEQ_1:def 13; then SY.k9 in Y by A35,FUNCT_1:3; then ex y9 being prime Element of NAT st y9=SY.k9 & y9>k+1 & y9<=2*k +1; hence thesis; end; A36: Product SY<=(2*k+1) choose k proof set r=2*k+1-k; set b=(2*k+1) choose k; reconsider SY as FinSequence of NAT; set a=Product SY; A37: k+1>=0; then reconsider r as Element of NAT; A38: 2*k+1-k+k>=0+k by A37,XREAL_1:6; then b = (2*k+1)!/((k!)*(r!)) by NEWTON:def 3; then A39: b>0; A40: for p being Element of NAT st p is prime holds p |-count a <= p |-count b proof now let y be object; assume y in Y; then ex y9 being prime Element of NAT st y9=y & y9>k+1 & y9<=2*k +1; hence y in SetPrimes by NEWTON:def 6; end; then Y c= SetPrimes; then rng SY c= SetPrimes by A33,FINSEQ_1:def 13; then reconsider SY as FinSequence of SetPrimes by FINSEQ_1:def 4; let p be Element of NAT; assume A41: p is prime; A42: rng Sgm Y = Y by A33,FINSEQ_1:def 13; A43: p divides a implies p>k+1 & p<=2*k+1 proof assume p divides a; then p in rng SY by A41,NAT_3:8; then ex y9 being prime Element of NAT st y9=p & y9>k+1 & y9<=2*k +1 by A42; hence thesis; end; per cases; suppose A44: p>k+1 & p<=2*k+1; set c = ((k!)*(r!)); A45: b*c = ((2*k+1)!)/c*c by A38,NEWTON:def 3 .= (2*k+1)! by XCMPLX_1:87; A46: p divides b proof assume not p divides b; then A47: p divides c by A41,A44,A45,NEWTON:41,80; per cases by A41,A47,NEWTON:80; suppose A48: p divides k!; k+01 by A41,INT_2:def 4; then p |-count b <> 0 by A39,A46,NAT_3:27; then 0+1 < p |-count b +1 by XREAL_1:6; then A49: 1 <= p |-count b by NAT_1:13; now let y be object; assume y in Y; then ex y9 being prime Element of NAT st y9=y & y9>k+1 & y9<=2 *k+1; hence y in SetPrimes by NEWTON:def 6; end; then A50: Y c= SetPrimes; p in rng SY by A41,A42,A44; hence thesis by A33,A41,A50,A49,Th43; end; suppose not(p>k+1 & p<=2*k+1); then A51: not p |^ (0+1) divides a by A43; 1 divides a by NAT_D:6; then A52: p |^ 0 divides a by NEWTON:4; p<>1 & a<>0 by A34,A41,Th41,INT_2:def 4; hence thesis by A52,A51,NAT_3:def 7; end; end; a is non zero Nat by A34,Th41; then ex n being Element of NAT st b=a*n by A39,A40,Th20; then a divides b by NAT_D:def 3; hence thesis by A39,NAT_D:7; end; for y being object holds y in {p where p is prime Element of NAT:p<= 2*k+1} iff y in X \/ Y proof let y be object; A53: now assume A54: y in X \/ Y; per cases by A54,XBOOLE_0:def 3; suppose y in X; then consider y9 being prime Element of NAT such that A55: y9=y and A56: y9<=k+1; 1*k<=2*k by XREAL_1:68; then k+1<=2*k+1 by XREAL_1:6; then y9<=2*k+1 by A56,XXREAL_0:2; hence y in {p where p is prime Element of NAT:p<=2*k+1} by A55; end; suppose y in Y; then ex y9 being prime Element of NAT st y9=y & y9>k+1 & y9<=2*k +1; hence y in {p where p is prime Element of NAT:p<=2*k+1}; end; end; now assume y in {p where p is prime Element of NAT:p<=2*k+1}; then consider y9 being prime Element of NAT such that A57: y9=y & y9<=2*k+1; y in X or y in Y proof per cases by A57; suppose y9=y & y9<=k+1; hence thesis; end; suppose y9=y & y9>k+1 & y9<=2*k+1; hence thesis; end; end; hence y in X \/ Y by XBOOLE_0:def 3; end; hence thesis by A53; end; then A58: {p where p is prime Element of NAT: p<=2*k+1}=X \/ Y by TARSKI:2; 2 to_power (2*k)=2 to_power (k+k) .=(2 to_power k)*(2 to_power k) by POWER:27 .=(2*2) to_power k by POWER:30; then A59: Product SY<=(4 to_power k) by A36,A13,XXREAL_0:2; 01-1 by A11,XREAL_1:9; then reconsider k as Element of NAT by INT_1:3; for y being object holds y in {p where p is prime Element of NAT:p <=m+1 } iff y in {p where p is prime Element of NAT:p<=m} proof let y be object; A61: now assume y in {p where p is prime Element of NAT:p<=m+1}; then consider y9 being prime Element of NAT such that A62: y=y9 and A63: y9<=m+1; m+1>1+1 by A11,XREAL_1:6; then not m+1 is Prime by A60,PEPIN:17; then y9=2 holds Product Sgm{p where p is prime Element of NAT:p<=x} <= 4 to_power (x-1) proof let x be Real; set A={p where p is prime Element of NAT:p<=x}; A1: A is finite proof ex m being Element of NAT st x=2; A is non empty proof assume A7: A is empty; 2 in A by A6,INT_2:28; hence contradiction by A7; end; then reconsider A as finite non empty real-membered set by A1,A5; set q = max A; q in A by XXREAL_2:def 8; then A8: ex q9 being prime Element of NAT st q9=q & q9<=x; then reconsider q as Prime; for y being object holds y in {p where p is prime Element of NAT:p<=q} iff y in {p where p is prime Element of NAT:p<=x} proof let y be object; hereby assume y in {p where p is prime Element of NAT:p<=q}; then consider y9 being prime Element of NAT such that A9: y9=y and A10: y9<=q; y9<=x by A8,A10,XXREAL_0:2; hence y in {p where p is prime Element of NAT:p<=x} by A9; end; assume A11: y in {p where p is prime Element of NAT:p<=x}; then consider y9 being prime Element of NAT such that A12: y9=y and y9<=x; y9<=q by A11,A12,XXREAL_2:def 8; hence thesis by A12; end; then A13: {p where p is prime Element of NAT:p<=q}= {p where p is prime Element of NAT:p<=x} by TARSKI:2; A14: 4 to_power (q-1)<=4 to_power (x-1) proof per cases by A8,XXREAL_0:1; suppose q=x; hence thesis; end; suppose q1 by Lm1; then q-'1=q-1 by XREAL_1:233; then q=n+1; then a<=b by Th44; hence thesis by A13,A14,XXREAL_0:2; end; hence thesis; end; theorem Th46: for n being Element of NAT, p being Prime st n<>0 ex f being FinSequence of NAT st len f = n & (for k being Element of NAT st k in dom f holds (f.k=1 iff p|^k divides n) & (f.k=0 iff not p|^k divides n)) & p |-count n = Sum f proof let n be Element of NAT; let p be Prime; defpred P[Nat,object] means (\$2=1 iff p|^\$1 divides n) & (\$2=0 iff not p|^\$1 divides n); set f1 = ((p |-count n) |-> 1) ^ ((n -' p|-count n) |-> 0); set n1 = p |-count n; set n2 = n -' p|-count n; set fa=(p |-count n) |-> 1; set fb=(n -' p|-count n) |-> 0; A1: Sum f1 = (Sum fa) + Sum fb by RVSUM_1:75 .= (p |-count n)*1 + Sum fb by RVSUM_1:80 .= p |-count n + (n -' p|-count n)*0 by RVSUM_1:80; assume A2: n<>0; A3: now p<>1 by INT_2:def 4; then p|^(p |-count n) divides n by A2,NAT_3:def 7; then A4: p |^ (p |-count n) <= n by A2,NAT_D:7; A5: p>1 by INT_2:def 4; assume n < p |-count n; then p to_power n < p to_power (p |-count n) by A5,POWER:39; then p |^ n < p to_power (p |-count n) by POWER:41; then p |^ n < p |^ (p |-count n) by POWER:41; then p |^ n < n by A4,XXREAL_0:2; hence contradiction by A5,Th3; end; A6: for k being Nat st k in Seg n ex x being object st P[k,x] proof let k be Nat; assume k in Seg n; per cases; suppose A7: p|^k divides n; set x = 1; take x; thus thesis by A7; end; suppose A8: not p|^k divides n; set x = 0; take x; thus thesis by A8; end; end; consider f being FinSequence such that A9: dom f = Seg n and A10: for k being Nat st k in Seg n holds P[k,f.k] from FINSEQ_1:sch 1(A6 ); now let x be object; assume x in rng f; then consider k being object such that A11: k in dom f and A12: f.k=x by FUNCT_1:def 3; reconsider k as Element of NAT by A11; P[k,f.k] by A9,A10,A11; hence x in NAT by A12; end; then rng f c= NAT; then reconsider f as FinSequence of NAT by FINSEQ_1:def 4; A13: len f1 = len(n1 |-> 1)+len(n2 |-> 0) by FINSEQ_1:22 .= n1 + len(n2 |-> 0) by CARD_1:def 7 .= n1 + n2 by CARD_1:def 7 .= p |-count n + (n - p |-count n) by A3,XREAL_1:233; A14: for x being object st x in dom f holds f.x=f1.x proof set ff2=n2 |-> 0; set ff1=n1 |-> 1; let x be object; assume A15: x in dom f; then reconsider x1 = x as Element of NAT; A16: x in dom f1 by A9,A13,A15,FINSEQ_1:def 3; per cases by A16,FINSEQ_1:25; suppose A17: x1 in dom ff1; then A18: x in Seg n1 by FUNCOP_1:13; A19: p |^ x1 divides n proof per cases; suppose x1=0; then p |^ x1 = 1 by NEWTON:4; hence thesis by NAT_D:6; end; suppose x1>0; then x1+1>0+1 by XREAL_1:6; then x1>=1 by NAT_1:13; then A20: x1-'1=x1-1 by XREAL_1:233; set j=p|-count n; set i=x1-'1; p<>1 by INT_2:def 4; then A21: p |^ j divides n by A2,NAT_3:def 7; -1+x1<0+x1 & x1 <= p |-count n by A18,FINSEQ_1:1,XREAL_1:6; then A22: i

=1 by FINSEQ_1:1; then m+(p |-count n) > 0+(p |-count n) by XREAL_1:6; then A25: x1 > p |-count n by A24,CARD_1:def 7; A26: not p |^ x1 divides n proof assume p |^ x1 divides n; then A27: p |-count (p |^ x1) <= p |-count n by A2,NAT_3:30; p>1 by INT_2:def 4; hence contradiction by A25,A27,NAT_3:25; end; ff2.m=0; then f1.x=0 by A23,A24,FINSEQ_1:def 7; hence thesis by A9,A10,A15,A26; end; end; take f; thus len f = n by A9,FINSEQ_1:def 3; thus for k being Element of NAT st k in dom f holds (f.k=1 iff p|^k divides n) & (f.k=0 iff not p|^k divides n) by A9,A10; dom f = dom f1 by A9,A13,FINSEQ_1:def 3; hence thesis by A14,A1,FUNCT_1:2; end; theorem Th47: for n being Element of NAT, p being Prime ex f being FinSequence of NAT st len f = n & (for k being Element of NAT st k in dom f holds f.k=[\ n/ (p|^k) /]) & p |-count (n!) = Sum f proof defpred P[Nat] means for p being Prime ex f being FinSequence of NAT st len f = \$1 & (for k being Element of NAT st k in dom f holds f.k=[\ \$1/( p|^k) /]) & p |-count (\$1!) = Sum f; let n be Element of NAT; let p be Prime; A1: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A2: P[n]; for p being Prime ex f being FinSequence of NAT st len f = n+1 & (for k being Element of NAT st k in dom f holds f.k=[\ (n+1)/(p|^k) /]) & p |-count ((n+1)!) = Sum f proof let p be Prime; consider fn being FinSequence of NAT such that A3: len fn = n and A4: for k being Element of NAT st k in dom fn holds fn.k=[\ n/(p|^k) /] and A5: p |-count (n!) = Sum fn by A2; reconsider fnn=fn as FinSequence of REAL by FINSEQ_2:24,NUMBERS:19; set fn0=fnn ^ <* In(0,REAL) *>; consider fn1 being FinSequence of NAT such that A6: len fn1 = n + 1 and A7: for k being Element of NAT st k in dom fn1 holds (fn1.k=1 iff p |^k divides (n+1)) & (fn1.k=0 iff not p|^k divides (n+1)) and A8: p |-count (n+1) = Sum fn1 by Th46; A9: Seg(n+1) = dom fn1 by A6,FINSEQ_1:def 3; set f = (fn ^ <* 0 *>)+fn1; for y being object st y in rng f holds y in NAT by ORDINAL1:def 12; then rng f c= NAT; then reconsider f as FinSequence of NAT by FINSEQ_1:def 4; take f; reconsider fn0 as FinSequence of REAL; reconsider fn1 as FinSequence of REAL by FINSEQ_2:24,NUMBERS:19; A10: dom f = dom fn0 /\ dom fn1 by VALUED_1:def 1; A11: len fn0 = len fn + len <* 0 *> by FINSEQ_1:22 .= n + 1 by A3,FINSEQ_1:39; then Seg(n+1) = dom fn0 by FINSEQ_1:def 3; hence len f = n+1 by A10,A9,FINSEQ_1:def 3; thus for k being Element of NAT st k in dom f holds f.k=[\ (n+1)/(p|^k) /] proof let k be Element of NAT; A12: (p|^k)/(p|^k)=1 by XCMPLX_1:60; assume A13: k in dom f; then A14: f.k = fn0.k + fn1.k by VALUED_1:def 1; A15: k in dom fn0 by A10,A13,XBOOLE_0:def 4; A16: fn0.k=[\ n/(p|^k) /] proof per cases by A15,FINSEQ_1:25; suppose A17: k in dom fn; then fn.k=[\ n/(p|^k) /] by A4; hence thesis by A17,FINSEQ_1:def 7; end; suppose ex n1 being Nat st n1 in dom <* 0 *> & k=len fn + n1; then consider n1 being Nat such that A18: n1 in dom <* 0 *> and A19: k=len fn + n1; n1 in Seg 1 by A18,FINSEQ_1:38; then A20: n1=1 by FINSEQ_1:2,TARSKI:def 1; p>1 by INT_2:def 4; then A21: p*p|^n>1*p|^n & p|^n>n by Th3,XREAL_1:68; p|^(n+1)=p|^n*p by NEWTON:6; then p|^k>n by A3,A19,A20,A21,XXREAL_0:2; then n/(p|^k)<1 by XREAL_1:189; then A22: n/(p|^k)-1<1-1 by XREAL_1:9; fn0.(n+1)=<* 0 *>.1 by A3,A18,A20,FINSEQ_1:def 7; then fn0.k=0 by A3,A19,A20,FINSEQ_1:40; hence thesis by A22,INT_1:def 6; end; end; A23: k in dom fn1 by A10,A13,XBOOLE_0:def 4; per cases; suppose A24: p|^k divides (n+1); then consider r being Nat such that A25: n+1=(p|^k)*r by NAT_D:def 3; A26: (n+1)/(p|^k) = r/((p|^k)/(p|^k)) by A25,XCMPLX_1:77 .= r/(1/1) by XCMPLX_1:60 .= r; ((p|^k)/(p|^k))+((-1)/(p|^k))-1<0 by A12; then A27: (p|^k+(-1))/(p|^k)-1<0 by XCMPLX_1:62; [\ n/(p|^k) /] + 1 = [\ n/(p|^k) +1 /] by INT_1:28 .=[\ n/(p|^k) + (p|^k)/(p|^k) /] by XCMPLX_1:60 .=[\ (n+p|^k)/(p|^k) /] by XCMPLX_1:62 .=[\ ((n+1)+(p|^k -1))/(p|^k) /] .=[\ (n+1)/(p|^k) + (p|^k-1)/(p|^k) /] by XCMPLX_1:62 .=(n+1)/(p|^k) + [\ (p|^k-1)/(p|^k) /] by A26,INT_1:28 .=(n+1)/(p|^k) + 0 by A27,INT_1:def 6 .=[\ (n+1)/(p|^k) /] by A26,INT_1:25; hence thesis by A7,A14,A23,A16,A24; end; suppose A28: not p|^k divides (n+1); set m=(n+1) mod (p|^k); set d=(n+1) div (p|^k); A29: n+1 = (p|^k) * d + m by NAT_D:2; then not m=0 by A28,NAT_D:def 3; then m+1>0+1 by XREAL_1:6; then m>=1 by NAT_1:13; then A30: m-1>=1-1 by XREAL_1:9; mNAT; let p be Prime; take f; thus len f = 0; thus for k being Element of NAT st k in dom f holds f.k=[\ 0/(p|^k) /]; p<>1 by INT_2:def 4; hence thesis by NAT_3:21,NEWTON:12,RVSUM_1:72; end; for n being Nat holds P[n] from NAT_1:sch 2(A35,A1); then consider f being FinSequence of NAT such that A36: ( len f = n & for k being Element of NAT st k in dom f holds f.k=[\ n/(p|^k) /] )& p |-count (n!) = Sum f; take f; thus thesis by A36; end; theorem Th48: for n being Element of NAT, p being Prime ex f being FinSequence of REAL st len f = 2*n & (for k being Element of NAT st k in dom f holds f.k=[\ (2*n)/(p|^k)/] - 2*[\n/(p|^k)/]) & p |-count (2*n choose n) = Sum f proof let n be Element of NAT; let p be Prime; set f0=n|->0; consider f1 being FinSequence of NAT such that A1: len f1 = n and A2: for k being Element of NAT st k in dom f1 holds f1.k=[\ n/(p|^k) /] and A3: p |-count (n!) = Sum f1 by Th47; consider f2 being FinSequence of NAT such that A4: len f2 = 2*n and A5: for k being Element of NAT st k in dom f2 holds f2.k=[\ (2*n)/(p|^k) /] and A6: p |-count ((2*n)!) = Sum f2 by Th47; reconsider f2 as FinSequence of REAL by FINSEQ_2:24,NUMBERS:19; set f = f2+((-(f1^f0))+(-(f1^f0))); take f; A7: dom (f1^f0) = Seg (len f1 + len f0) by FINSEQ_1:def 7 .= Seg (n+n) by A1,CARD_1:def 7 .= Seg (2*n); A8: dom ((-(f1^f0))+(-(f1^f0))) = dom (-(f1^f0)) /\ dom (-(f1^f0)) by VALUED_1:def 1 .= Seg (2*n) by A7,VALUED_1:8; A9: dom f = dom f2 /\ dom ((-(f1^f0))+(-(f1^f0))) by VALUED_1:def 1 .= Seg (2*n) /\ Seg (2*n) by A4,A8,FINSEQ_1:def 3; hence len f = 2*n by FINSEQ_1:def 3; thus for k being Element of NAT st k in dom f holds f.k=[\(2*n)/(p|^k)/]- 2* [\n/(p|^k)/] proof let k be Element of NAT; assume A10: k in dom f; then A11: k in dom f2 by A4,A9,FINSEQ_1:def 3; A12: f.k = f2.k+((-(f1^f0))+(-(f1^f0))).k by A10,VALUED_1:def 1 .=f2.k+((-(f1^f0)).k+(-(f1^f0)).k) by A8,A9,A10,VALUED_1:def 1 .=f2.k+2*(-(f1^f0)).k .=f2.k+2*(-(f1^f0).k) by RVSUM_1:17 .=f2.k-2*(f1^f0).k .=[\(2*n)/(p|^k)/]-2*(f1^f0).k by A5,A11; per cases by A7,A9,A10,FINSEQ_1:25; suppose A13: k in dom f1; then (f1^f0).k=f1.k by FINSEQ_1:def 7 .=[\n/(p|^k)/] by A2,A13; hence thesis by A12; end; suppose ex e being Nat st e in dom f0 & k=len f1 + e; then consider e being Nat such that A14: e in dom f0 and A15: k=len f1 + e; dom f0 = Seg n by FUNCOP_1:13; then e >= 1 by A14,FINSEQ_1:1; then e + len f1 >= 1 + len f1 by XREAL_1:6; then A16: k > 1 + n or k = 1 + n by A1,A15,XXREAL_0:1; A17: (f1^f0).k = f0.e by A14,A15,FINSEQ_1:def 7 .= 0; p>1 by INT_2:def 4; then p to_power k >= p to_power (1+n) by A16,POWER:39; then p|^k >= p to_power (1+n) by POWER:41; then A18: p|^k >= p|^(1+n) by POWER:41; A19: p>1 by INT_2:def 4; then p*p|^n>1*p|^n by XREAL_1:68; then p|^(1+n)>p|^n by NEWTON:6; then A20: p|^k>p|^n by A18,XXREAL_0:2; per cases; suppose n=0; hence thesis by A12,A17,INT_1:25; end; suppose A21: n<>0; (p|^n)/(p|^n)>n/(p|^n) by A19,Th3,XREAL_1:74; then A22: 1>n/(p|^n) by XCMPLX_1:60; n/(p|^n)>n/(p|^k) by A20,A21,XREAL_1:76; then 1>n/(p|^k) by A22,XXREAL_0:2; then 1-1>n/(p|^k)-1 by XREAL_1:9; hence thesis by A12,A17,INT_1:def 6; end; end; end; p |-count (2*n choose n) = Sum f proof per cases; suppose A23: n=0; then A24: 2*n choose n = 1 by NEWTON:19; p>1 by INT_2:def 4; then A25: p |-count (2*n choose n) = 0 by A24,NAT_3:21; len f = 0 by A9,A23,FINSEQ_1:def 3; hence thesis by A25,PROB_3:62; end; suppose A26: n<>0; A27: 2*n-n=n; A28: n+n>n+0 by A26,XREAL_1:6; then (2*n choose n)*((n!)*(n!)) = ((2*n)!)/((n!)*(n!))*((n!)*(n!)) by A27 ,NEWTON:def 3 .= (2*n)! by XCMPLX_1:87; then A29: ((n!) * (n!)) divides ((2*n)!) by NAT_D:def 3; 2*n choose n = ((2*n)!)/((n!)*(n!)) by A28,A27,NEWTON:def 3; then A30: 2*n choose n = ((n!) * (n!)) * (((2*n)!) div ((n!) * (n!))) /((n!)* (n!)) by A29,NAT_D:3 .= ((2*n)!) div ((n!) * (n!)) by XCMPLX_1:89; A31: -(f1^f0) is Element of len(-(f1^f0))-tuples_on REAL by FINSEQ_2:92; A32: p |-count (((2*n)!) div ((n!)*(n!))) = p |-count ((2*n)!) -' p |-count ((n!)*(n!)) by A29,NAT_3:31 .= p |-count ((2*n)!) - p |-count ((n!)*(n!)) by A29,NAT_3:30 ,XREAL_1:233; A33: ((-(f1^f0))+(-(f1^f0))) is Element of len((-(f1^f0))+(-(f1^f0))) -tuples_on REAL by FINSEQ_2:92; len((-(f1^f0))+(-(f1^f0)))=len f2 & f2 is Element of len(f2) -tuples_on REAL by A4,A8,FINSEQ_1:def 3,FINSEQ_2:92; then Sum f = Sum f2 + Sum((-(f1^f0))+(-(f1^f0))) by A33,RVSUM_1:89 .= Sum f2 + (Sum(-(f1^f0)) + Sum(-(f1^f0))) by A31,RVSUM_1:89 .= Sum f2 + (- Sum(f1^f0) + Sum(-(f1^f0))) by RVSUM_1:88 .= Sum f2 + (- Sum(f1^f0) + (- Sum(f1^f0))) by RVSUM_1:88 .= Sum f2 - 2*Sum(f1^f0) .= Sum f2 - 2*(Sum(f1) + Sum(f0)) by RVSUM_1:75 .= Sum f2 - 2*(Sum f1 + n*0) by RVSUM_1:80 .= p |-count ((2*n)!) -(p |-count (n!) + p |-count (n!)) by A3,A6 .= p |-count (((2*n)!) div ((n!)*(n!))) by A32,NAT_3:28; hence thesis by A30; end; end; hence thesis; end; Lm8: for n,r being Element of NAT, p being Prime, f being FinSequence of REAL st p|^r <= 2*n & 2*n < p|^(r+1) & len f = 2*n & (for k being Element of NAT st k in dom f holds f.k=[\(2*n)/(p|^k)/] - 2*[\n/(p|^k)/]) holds Sum f <= r proof let n,r be Element of NAT; let p be Prime; let f be FinSequence of REAL; set f0 = (r |-> 1)^((2*n -' r)|-> 0); A1: p>1 by INT_2:def 4; assume A2: p|^r <= 2*n; A3: 2*n >= r proof assume 2*n < r; then p to_power (2*n)

1) + len((2*n -' r)|-> 0) by FINSEQ_1:22 .= r + len((2*n -' r)|->0) by CARD_1:def 7 .= r + (2*n -' r) by CARD_1:def 7 .= r + (2*n - r) by A3,XREAL_1:233 .= len f by A5; assume A7: for k being Element of NAT st k in dom f holds f.k=[\(2*n)/(p|^k)/] - 2*[\n/(p|^k)/]; A8: for k be Element of NAT st k in dom f holds f.k <= f0.k proof let k be Element of NAT; assume A9: k in dom f; then A10: f.k=[\(2*n)/(p|^k)/] - 2*[\n/(p|^k)/] by A7; k in Seg (2*n) by A5,A9,FINSEQ_1:def 3; then A11: k in dom f0 by A5,A6,FINSEQ_1:def 3; per cases by A11,FINSEQ_1:25; suppose A12: k in dom (r |-> 1); [\n/(p|^k)/] <= n/(p|^k) by INT_1:def 6; then -[\n/(p|^k)/] >= -n/(p|^k) by XREAL_1:24; then (2*n)/(p|^k) - 1 < [\(2*n)/(p|^k)/] & (-[\n/(p|^k)/])*2 >= (-n/(p|^ k))*2 by INT_1:def 6,XREAL_1:64; then ((2*n)/(p|^k) - 1) + 2*(-n/(p|^k)) < [\(2*n)/(p|^k)/] + (-2*[\n/(p |^k)/]) by XREAL_1:8; then [\(2*n)/(p|^k)/] -2*[\n/(p|^k)/] > 2*(n/(p|^k)) -1 + 2*(-n/(p|^k)) by XCMPLX_1:74; then f.k >= -1 +1 by A10,INT_1:7; then A13: f.k is Element of NAT by A10,INT_1:3; n/(p|^k) - 1 < [\n/(p|^k)/] by INT_1:def 6; then -[\n/(p|^k)/] < -(n/(p|^k) - 1) by XREAL_1:24; then [\(2*n)/(p|^k)/] <= (2*n)/(p|^k) & (-[\n/(p|^k)/])*2 < (-(n/(p|^k) - 1))*2 by INT_1:def 6,XREAL_1:68; then (2*n)/(p|^k)= 2*(n/(p|^k)) & -2*[\n/(p|^k)/] + [\(2*n)/(p|^k)/] < 2 *(-n/(p|^ k) + 1) + (2*n)/(p|^k) by XCMPLX_1:74,XREAL_1:8; then A14: f.k < 1+1 by A10; A15: k in Seg r by A12,FUNCOP_1:13; f0.k = (r |-> 1).k by A12,FINSEQ_1:def 7 .= 1 by A15,FUNCOP_1:7; hence thesis by A13,A14,NAT_1:13; end; suppose A16: ex n0 being Nat st n0 in dom ((2*n -' r)|-> 0) & k=len (r |-> 1 )+ n0; reconsider k1=k as Element of NAT; consider n0 be Nat such that A17: n0 in dom ((2*n -' r)|-> 0) and A18: k=len (r |-> 1)+ n0 by A16; n0 in Seg (2*n -' r) by A17,FUNCOP_1:13; then 1<=n0 by FINSEQ_1:1; then A19: 1+r<=n0+r by XREAL_1:6; k=r + n0 by A18,CARD_1:def 7; then r+1 In(1,REAL))^((2*n -' r)|-> In(0,REAL)); Sum f0 = Sum (r |-> 1) + Sum ((2*n -' r)|-> 0) by RVSUM_1:75 .= r*1 + Sum ((2*n -' r)|-> 0) by RVSUM_1:80 .= r + (2*n -' r)*0 by RVSUM_1:80 .= r; hence thesis by A6,A8,INTEGRA5:3,A22; end; Lm9: for n being Element of NAT, p being Prime st n>=3 holds (p>2*n implies p |-count (2*n choose n) = 0) & (n

=3; A2: for n,r being Element of NAT, p being Prime st n>=2 & p|^r <= 2*n & 2*n < p|^(r+1) holds p |-count (2*n choose n) <= r proof let n,r be Element of NAT; let p be Prime; assume that n>=2 and A3: p|^r <= 2*n & 2*n < p|^(r+1); ex f be FinSequence of REAL st len f = 2*n &( for k being Element of NAT st k in dom f holds f.k=[\(2*n)/(p|^k)/] - 2*[\n/(p|^k)/])& p |-count (2*n choose n) = Sum f by Th48; hence thesis by A3,Lm8; end; thus p>2*n implies p |-count (2*n choose n) = 0 proof set r = 0; assume p>2*n; then A4: p|^(r+1)>2*n; A5: n>=2 by A1,XXREAL_0:2; then n*2>=2*2 by XREAL_1:64; then 2*n>=1 by XXREAL_0:2; then p|^r <= 2*n by NEWTON:4; hence thesis by A2,A5,A4; end; thus n

=2 by A1,XXREAL_0:2; then 2

0; assume A10: 2*n/31 by INT_2:def 4; then p to_power 2 <= p to_power k by A27,POWER:39; then p|^2 <= p to_power k by POWER:41; then A29: p|^2 <= p|^k by POWER:41; then 2*n < p|^k by A28,XXREAL_0:2; then 2*n/(p|^k) < (p|^k)/(p|^k) by XREAL_1:74; then 2*n/(p|^k) < 1 by XCMPLX_1:60; then 2*n/(p|^k) - 1 < 1-1 by XREAL_1:9; then A30: [\2*n/(p|^k)/] = 0 by INT_1:def 6; 1*n<=2*n by XREAL_1:64; then n0 by A1,SQUARE_1:25; then sqrt(2*n)*sqrt(2*n)=2 by A1,XXREAL_0:2; hence thesis by A2,A36,A35; end; assume p<=sqrt(2*n); then sqrt(2*n)*p >= p*p & sqrt(2*n)*sqrt(2*n) >= p*sqrt(2*n) by XREAL_1:64; then (sqrt(2*n))^2 >= p*p by XXREAL_0:2; then A37: 2*n>=p*p by SQUARE_1:def 2; set k0=p |-count (2*n choose n); set r = [\ log(p,2*n) /]; A38: r <= log(p,2*n) by INT_1:def 6; A39: log(p,2*n) - 1 < r by INT_1:def 6; A40: p>1 by INT_2:def 4; then p*p>1*p by XREAL_1:68; then 2*n>p by A37,XXREAL_0:2; then log(p,2*n)>log(p,p) by A40,POWER:57; then log(p,2*n)>1 by A40,POWER:52; then log(p,2*n)-1>1-1 by XREAL_1:9; then reconsider r as Element of NAT by A39,INT_1:3; r < log(p,2*n) or r = log(p,2*n) by A38,XXREAL_0:1; then p to_power r <= p to_power log(p,2*n) by A40,POWER:39; then p|^r <= p to_power log(p,2*n) by POWER:41; then A41: p|^r <= 2*n by A40,A37,POWER:def 3; log(p,2*n) - 1 +1 < r +1 by A39,XREAL_1:6; then p to_power log(p,2*n) < p to_power (r+1) by A40,POWER:39; then p to_power log(p,2*n) < p|^(r+1) by POWER:41; then A42: 2*n < p|^(r+1) by A40,POWER:def 3; n>=2 by A1,XXREAL_0:2; then k0 <= r by A2,A41,A42; then k0 = r or k0 < r by XXREAL_0:1; then p to_power k0 <= p to_power r by A40,POWER:39; then p|^k0 <= p to_power r by POWER:41; then p|^k0 <= p|^r by POWER:41; hence thesis by A41,XXREAL_0:2; end; definition let f be FinSequence of NAT,p be Prime; func p |-count f -> FinSequence of NAT means :Def1: len it = len f & for i being set st i in dom it holds it.i = p |-count f.i; existence proof deffunc F(Nat) = p |-count f.\$1; consider g being FinSequence such that A1: len g = len f and A2: for k being Nat st k in dom g holds g.k = F(k) from FINSEQ_1:sch 2; now let y be object; assume y in rng g; then consider x be object such that A3: x in dom g and A4: y=g.x by FUNCT_1:def 3; reconsider x as Element of NAT by A3; y=F(x) by A2,A3,A4; hence y in NAT; end; then rng g c= NAT; then reconsider g as FinSequence of NAT by FINSEQ_1:def 4; take g; thus len g = len f by A1; let i be set; assume i in dom g; hence thesis by A2; end; uniqueness proof let g,h be FinSequence of NAT such that A5: len g = len f and A6: for i being set st i in dom g holds g.i = p |-count f.i and A7: len h = len f and A8: for i being set st i in dom h holds h.i = p |-count f.i; A9: dom g = Seg len g & dom h = Seg len h by FINSEQ_1:def 3; for k being Nat st k in dom g holds g.k = h.k proof let k be Nat; assume A10: k in dom g; hence g.k = p |-count f.k by A6 .= h.k by A5,A7,A8,A9,A10; end; hence thesis by A5,A7,A9,FINSEQ_1:13; end; end; theorem Th49: for p being Prime, f being FinSequence of NAT st f={} holds p |-count f = {} proof let p be Prime; let f be FinSequence of NAT; assume f={}; then len (p |-count f) = len {} by Def1; hence thesis; end; theorem Th50: for p being Prime, f1,f2 being FinSequence of NAT holds p |-count (f1^f2) = (p |-count f1)^(p |-count f2) proof let p be Prime; let f1,f2 be FinSequence of NAT; A1: len (p |-count f2) = len f2 by Def1; A2: dom (p |-count (f1^f2)) = Seg len (p |-count (f1^f2)) by FINSEQ_1:def 3 .= Seg len (f1^f2) by Def1; A3: for k being Nat st k in dom (p |-count (f1^f2)) holds (p |-count (f1^f2) ).k = ((p |-count f1)^(p |-count f2)).k proof let k be Nat; assume A4: k in dom (p |-count (f1^f2)); then A5: k in dom (f1^f2) by A2,FINSEQ_1:def 3; per cases by A5,FINSEQ_1:25; suppose A6: k in dom f1; A7: dom f1 = Seg len f1 by FINSEQ_1:def 3 .= Seg len (p |-count f1) by Def1 .= dom (p |-count f1) by FINSEQ_1:def 3; (p |-count (f1^f2)).k = p |-count (f1^f2).k by A4,Def1 .= p |-count (f1.k) by A6,FINSEQ_1:def 7 .= (p |-count f1).k by A6,A7,Def1; hence thesis by A6,A7,FINSEQ_1:def 7; end; suppose A8: ex n being Nat st n in dom f2 & k=len f1 + n; A9: dom f2 = Seg len f2 by FINSEQ_1:def 3 .= Seg len (p |-count f2) by Def1 .= dom (p |-count f2) by FINSEQ_1:def 3; consider n be Nat such that A10: n in dom f2 and A11: k=len f1 + n by A8; A12: ((p |-count f1)^(p |-count f2)).k = ((p |-count f1)^(p |-count f2)) .(len (p |-count f1) + n) by A11,Def1 .= (p |-count f2).n by A10,A9,FINSEQ_1:def 7; (f1^f2).k = f2.n by A10,A11,FINSEQ_1:def 7; then (p |-count (f1^f2)).k = p |-count (f2.n) by A4,Def1 .= (p |-count f2).n by A10,A9,Def1; hence thesis by A12; end; end; Seg len (f1^f2) = Seg (len f1 + len f2) by FINSEQ_1:22 .= Seg (len (p |-count f1) + len (p |-count f2)) by A1,Def1 .= Seg len ((p |-count f1)^(p |-count f2)) by FINSEQ_1:22 .= dom ((p |-count f1)^(p |-count f2)) by FINSEQ_1:def 3; hence thesis by A2,A3,FINSEQ_1:13; end; theorem Th51: for p being Prime, n being non zero Element of NAT holds p |-count <*n*> = <* (p |-count n) *> proof let p be Prime; let n be non zero Element of NAT; A1: dom (p |-count <*n*>) = Seg len (p |-count <*n*>) by FINSEQ_1:def 3 .= Seg len <*n*> by Def1 .= Seg 1 by FINSEQ_1:39; A2: for k being Nat st k in dom (p |-count <*n*>) holds (p |-count <*n*>).k = <* p |-count n *>.k proof let k be Nat; assume A3: k in dom (p |-count <*n*>); then 1<=k & k<=1 by A1,FINSEQ_1:1; then A4: k=1 by XXREAL_0:1; (p |-count <*n*>).k = p |-count <*n*>.k by A3,Def1; then (p |-count <*n*>).k = p |-count n by A4,FINSEQ_1:40; hence thesis by A4,FINSEQ_1:40; end; Seg 1 = Seg len <* p |-count n *> by FINSEQ_1:39; then dom (p |-count <*n*>) = dom <* (p |-count n) *> by A1,FINSEQ_1:def 3; hence thesis by A2,FINSEQ_1:13; end; theorem Th52: for f being FinSequence of NAT, p being Prime st Product f <> 0 holds p |-count (Product f) = Sum (p |-count f) proof let f be FinSequence of NAT; defpred P[Nat] means for f being FinSequence of NAT, p being Prime st \$1=len f & Product f <> 0 holds p |-count (Product f) = Sum (p |-count f); let p be Prime; assume A1: Product f<>0; A2: ex n being Element of NAT st n=len f; A3: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A4: P[n]; for f being FinSequence of NAT, p being Prime st n+1=len f & Product f <> 0 holds p |-count (Product f) = Sum (p |-count f) proof let f be FinSequence of NAT; let p be Prime; assume that A5: n+1=len f and A6: Product f <> 0; consider g being FinSequence of NAT, d being Element of NAT such that A7: f = g^<*d*> by A5,FINSEQ_2:19; len f = len g + len <*d*> by A7,FINSEQ_1:22; then A8: n+1 = len g + 1 by A5,FINSEQ_1:39; A9: (Product g) * d <> 0 by A6,A7,RVSUM_1:96; then A10: Product g <> 0; A11: d <> 0 by A9; p |-count (Product f) = p |-count ((Product g) * d) by A7,RVSUM_1:96 .= (p |-count (Product g)) + (p |-count d) by A10,A11,NAT_3:28 .= Sum (p |-count g) + (p |-count d) by A4,A10,A8 .= Sum ((p |-count g)^<*(p |-count d)*>) by RVSUM_1:74 .= Sum ((p |-count g)^(p |-count <*d*>)) by A11,Th51 .= Sum (p |-count (g^<*d*>)) by Th50; hence thesis by A7; end; hence thesis; end; A12: P[0] proof let f be FinSequence of NAT; let p be Prime; assume that A13: 0=len f and Product f<>0; A14: p<>1 by INT_2:def 4; A15: f={} by A13; then Sum (p |-count f) = 0 by Th49,RVSUM_1:72; hence thesis by A15,A14,NAT_3:21,RVSUM_1:94; end; for n being Nat holds P[n] from NAT_1:sch 2(A12,A3); hence thesis by A1,A2; end; theorem Th53: for f1,f2 being FinSequence of REAL st len f1 = len f2 & (for k being Element of NAT st k in dom f1 holds f1.k<=f2.k & f1.k>0) holds Product f1 <= Product f2 proof let f1,f2 be FinSequence of REAL; defpred P[Nat] means for f1,f2 being FinSequence of REAL st len f1 = len f2 & \$1 = len f1 & (for k being Element of NAT st k in dom f1 holds f1 .k<=f2.k & f1.k>0) holds Product f1 <= Product f2; assume A1: len f1 = len f2; A2: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A3: P[n]; for f1,f2 being FinSequence of REAL st len f1 = len f2 & n+1 = len f1 & (for k being Element of NAT st k in dom f1 holds f1.k<=f2.k & f1.k>0) holds Product f1 <= Product f2 proof let f1,f2 be FinSequence of REAL; assume that A4: len f1=len f2 and A5: n+1=len f1; consider g2 be FinSequence of REAL, r2 be Element of REAL such that A6: f2 = g2^<*r2*> by A4,A5,FINSEQ_2:19; len f2 = len g2 + len <* r2 *> by A6,FINSEQ_1:22; then A7: n+1 = len g2 + 1 by A4,A5,FINSEQ_1:39; A8: Product f2 = (Product g2) * r2 by A6,RVSUM_1:96; consider g1 be FinSequence of REAL, r1 be Element of REAL such that A9: f1 = g1^<*r1*> by A5,FINSEQ_2:19; set k1 = len g1+1; A10: Product f1 = (Product g1) * r1 by A9,RVSUM_1:96; len f1 = len g1 + len <* r1 *> by A9,FINSEQ_1:22; then A11: n+1 = len g1 + 1 by A5,FINSEQ_1:39; assume A12: for k being Element of NAT st k in dom f1 holds f1.k<=f2.k & f1. k>0; A13: now let k be Element of NAT; A14: dom g1 c= dom f1 by A9,FINSEQ_1:26; assume A15: k in dom g1; then k in Seg len g2 by A11,A7,FINSEQ_1:def 3; then k in dom g2 by FINSEQ_1:def 3; then A16: f2.k=g2.k by A6,FINSEQ_1:def 7; f1.k=g1.k by A9,A15,FINSEQ_1:def 7; hence g1.k<=g2.k & g1.k>0 by A12,A15,A16,A14; end; then A17: for k being Element of NAT st k in dom g1 holds g1.k > 0; Product g1 <= Product g2 by A3,A11,A7,A13; then A18: Product g2 > 0 by A17,Th41; n+1>=0+1 by XREAL_1:6; then k1 in Seg (n+1) by A11,FINSEQ_1:1; then A19: k1 in dom f1 by A5,FINSEQ_1:def 3; then f1.k1<=f2.k1 by A12; then r1 <= f2.k1 by A9,FINSEQ_1:42; then r1 <= r2 by A6,A11,A7,FINSEQ_1:42; then A20: r1 * (Product g2) <= r2 * (Product g2) by A18,XREAL_1:64; f1.k1>0 by A12,A19; then r1>0 by A9,FINSEQ_1:42; then (Product g1) * r1 <= (Product g2) * r1 by A3,A11,A7,A13,XREAL_1:64; hence thesis by A10,A8,A20,XXREAL_0:2; end; hence thesis; end; A21: P[0] proof let f1,f2 be FinSequence of REAL; assume len f1 = len f2 & 0=len f1; then f1={} & f2 = {}; hence thesis; end; A22: for n being Nat holds P[n] from NAT_1:sch 2(A21,A2); assume for k being Element of NAT st k in dom f1 holds f1.k<=f2.k & f1.k>0; hence thesis by A22,A1; end; theorem Th54: for n being Element of NAT, r being Real st r>0 holds Product (n |-> r) = r to_power n proof defpred P[Nat] means for r being Real st r>0 holds Product (\$1 |-> r) = r to_power \$1; A1: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A2: P[n]; now let r be Real; assume A3: r>0; Product ((n+1)|-> r) = Product ((n |-> r) ^ <*r*>) by FINSEQ_2:60 .= Product (n |-> r) * r by RVSUM_1:96 .= (r to_power n) * r by A2,A3 .= (r to_power n) * (r to_power 1) by POWER:25; hence Product ((n+1)|-> r) = r to_power (n+1) by A3,POWER:27; end; hence thesis; end; A4: P[0] by POWER:24,RVSUM_1:94; for n being Nat holds P[n] from NAT_1:sch 2(A4,A1); hence thesis; end; scheme scheme1 { P[set,set,set] } : for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]} holds Product Sgm X > 0 proof let p be Prime; let n be Element of NAT; let m be non zero Element of NAT; let X be set; set f = Sgm X; assume A1: X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]}; A2: for k being Element of NAT st k in dom f holds f.k > 0 proof set XX=Seg m; let k be Element of NAT; now let x be object; assume x in X; then ex y9 being prime Element of NAT st y9|^(y9 |-count m) = x & P[n,m, y9] by A1; then ex b being Element of NAT st b=x & 1<=b & b<=m by Th16; hence x in XX by FINSEQ_1:1; end; then X c= Seg m; then A3: rng f = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m, p9]} by A1,FINSEQ_1:def 13; assume k in dom f; then f.k in {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9 ]} by A3,FUNCT_1:3; then ex y9 being prime Element of NAT st y9|^(y9 |-count m) = f.k & P[n,m, y9]; hence thesis; end; rng f c= REAL; then f is FinSequence of REAL by FINSEQ_1:def 4; hence thesis by A2,Th41; end; scheme scheme2 { P[set,set,set] } : for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]} & not p|^(p |-count m) in X holds p |-count (Product Sgm X) = 0 proof let p be Prime; let n be Element of NAT; let m be non zero Element of NAT; let X be set; assume A1: X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]}; set f=p |-count (Sgm X); set g=(len f) |-> 0; assume A2: not p|^(p |-count m) in X; A3: for k being Nat st 1 <=k & k <= len f holds f.k=g.k proof set XX=Seg m; let k be Nat; assume A4: 1 <=k; assume k <= len f; then A5: k in Seg len f by A4,FINSEQ_1:1; then k in dom f by FINSEQ_1:def 3; then A6: f.k = p |-count (Sgm X).k by Def1; now let x be object; assume x in X; then ex y9 being prime Element of NAT st y9|^(y9 |-count m) = x & P[n,m, y9] by A1; then ex b being Element of NAT st b=x & 1<=b & b<=m by Th16; hence x in XX by FINSEQ_1:1; end; then X c= Seg m; then A7: rng Sgm X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n ,m,p9]} by A1,FINSEQ_1:def 13; len f = len (Sgm X) by Def1; then k in dom Sgm X by A5,FINSEQ_1:def 3; then (Sgm X).k in {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[ n,m,p9]} by A7,FUNCT_1:3; then consider p1 be prime Element of NAT such that A8: p1|^(p1 |-count m) = (Sgm X).k and A9: P[n,m,p1]; p1<>p by A1,A2,A9; then p<>1 & not p divides p1|^(p1 |-count m) by INT_2:def 4,NAT_3:6; then f.k = 0 by A6,A8,NAT_3:27; hence thesis; end; for p being Prime, n being Element of NAT, m being non zero Element of NAT , X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]} holds Product Sgm X > 0 from scheme1; then Product Sgm X <> 0 by A1; then A10: p |-count (Product Sgm X) = Sum (p |-count (Sgm X)) by Th52; len f = len g & Sum g = (len f)*0 by CARD_1:def 7,RVSUM_1:80; hence thesis by A10,A3,FINSEQ_1:14; end; scheme scheme3 { P[set,set,set] } : for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]} & p|^(p |-count m) in X holds p |-count ( Product Sgm X) = p |-count m proof let p be Prime; let n be Element of NAT; let m be non zero Element of NAT; let X be set; set XX=Seg m; defpred P1[Element of NAT,Element of NAT,Prime] means P[\$1,\$2,\$3] & \$3|^(\$3 |-count \$2) <= p|^(p |-count \$2); defpred P2[Element of NAT,Element of NAT,Prime] means P[\$1,\$2,\$3] & \$3|^(\$3 |-count \$2) > p|^(p |-count \$2); set X1 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P1[n,m,p9]}; set X2 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P2[n,m,p9]}; A1: now let k1,k2 be Nat; assume k1 in X1 & k2 in X2; then ( ex p1 being prime Element of NAT st p1|^(p1 |-count m)=k1 & P1[n, m ,p1])& ex p2 being prime Element of NAT st p2|^(p2 |-count m)=k2 & P2[n,m,p2]; hence k1 < k2 by XXREAL_0:2; end; A2: now assume p|^(p |-count m) in X2; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m) & P2[n,m,p9]; hence contradiction; end; set m1=p|^(p |-count m); defpred P12[Element of NAT,Element of NAT,Prime] means P[\$1,\$2,\$3] & \$3|^(\$3 |-count \$2) = p|^(p |-count \$2); defpred P11[Element of NAT,Element of NAT,Prime] means P[\$1,\$2,\$3] & \$3|^(\$3 |-count \$2) < p|^(p |-count \$2); set X11 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P11[n,m,p9]}; set X12 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P12[n,m,p9]}; A3: now let k1,k2 be Nat; assume k1 in X11 & k2 in X12; then ( ex p1 being prime Element of NAT st p1|^(p1 |-count m)=k1 & P11[n,m ,p1])& ex p2 being prime Element of NAT st p2|^(p2 |-count m)=k2 & P12[n,m,p2]; hence k1 < k2; end; now let x be object; assume x in X1; then consider p9 being prime Element of NAT such that A4: p9|^(p9 |-count m)=x & P1[n,m,p9]; p9|^(p9 |-count m)=x & P11[n,m,p9] or p9|^(p9 |-count m)=x & P12[n,m, p9] by A4,XXREAL_0:1; then x in X11 or x in X12; hence x in X11 \/ X12 by XBOOLE_0:def 3; end; then A5: X1 c= X11 \/ X12; assume A6: X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]}; now let x be object; assume x in X; then ex y9 being prime Element of NAT st y9|^(y9 |-count m) = x & P[n,m,y9 ] by A6; then ex b being Element of NAT st b=x & 1<=b & b<=m by Th16; hence x in XX by FINSEQ_1:1; end; then A7: X c= Seg m; now let x be object; assume x in X12; then ex p9 be prime Element of NAT st p9|^(p9 |-count m) = x & P12[n,m,p9]; hence x in {p|^(p |-count m)} by TARSKI:def 1; end; then A8: X12 c= {p|^(p |-count m)}; for p being Prime, n being Element of NAT, m being non zero Element of NAT , X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]} holds Product Sgm X > 0 from scheme1; then A9: Product Sgm X <> 0 by A6; A10: 1 < p by INT_2:def 4; A11: p |-count (p|^(p |-count m)) = (p |-count m) * (p |-count p) by NAT_3:32 .= (p |-count m) * 1 by A10,NAT_3:22; now let x be object; assume x in X1; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=x & P1[n,m,p9]; hence x in X by A6; end; then A12: X1 c= X; then A13: X1 c= Seg m by A7; now let x be object; assume x in X12; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=x & P12[n,m,p9 ]; hence x in X1; end; then A14: X12 c= X1; then A15: X12 c= Seg m by A13; now let x be object; assume x in X11; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=x & P11[n,m,p9 ]; hence x in X1; end; then A16: X11 c= X1; then A17: X11 c= Seg m by A13; X11 \/ X12 c= X1 \/ X1 by A16,A14,XBOOLE_1:13; then A18: Sum (p |-count (Sgm X1)) = Sum (p |-count (Sgm (X11 \/ X12))) by A5, XBOOLE_0:def 10 .= Sum (p |-count (Sgm(X11) ^ Sgm(X12))) by A17,A15,A3,FINSEQ_3:42 .= Sum ((p |-count Sgm(X11)) ^ (p |-count Sgm(X12))) by Th50 .= Sum (p |-count Sgm(X11)) + Sum (p |-count Sgm(X12)) by RVSUM_1:75; for p being Prime, n being Element of NAT, m being non zero Element of NAT , X2 being set st X2 = {p9|^(p9 |-count m) where p9 is prime Element of NAT : P2[n,m,p9]} & not p|^(p |-count m) in X2 holds p |-count (Product Sgm X2) = 0 from scheme2; then A19: p |-count (Product Sgm X2) = 0 by A2; for p being Prime, n being Element of NAT, m being non zero Element of NAT , X2 being set st X2 = {p9|^(p9 |-count m) where p9 is prime Element of NAT : P2[n,m,p9]} holds Product Sgm X2 > 0 from scheme1; then A20: Product Sgm(X2) <> 0; now let x be object; assume x in X; then consider p9 being prime Element of NAT such that A21: p9|^(p9 |-count m)=x & P[n,m,p9] by A6; p9|^(p9 |-count m)=x & P1[n,m,p9] or p9|^(p9 |-count m)=x & P2[n,m,p9 ] by A21; then x in X1 or x in X2; hence x in X1 \/ X2 by XBOOLE_0:def 3; end; then A22: X c= X1 \/ X2; now let x be object; assume x in X2; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=x & P2[n,m,p9]; hence x in X by A6; end; then A23: X2 c= X; then A24: X2 c= Seg m by A7; reconsider m1 as non zero Element of NAT by ORDINAL1:def 12; A25: now assume p|^(p |-count m) in X11; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m) & P11[n,m,p9]; hence contradiction; end; assume p|^(p |-count m) in X; then p|^(p |-count m) in X1 by A22,A2,XBOOLE_0:def 3; then p|^(p |-count m) in X12 by A5,A25,XBOOLE_0:def 3; then for x being object st x in {p|^(p |-count m)} holds x in X12 by TARSKI:def 1; then A26: {p|^(p |-count m)} c= X12; for p being Prime, n being Element of NAT, m being non zero Element of NAT , X11 being set st X11 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P11[n,m,p9]} & not p|^(p |-count m) in X11 holds p |-count (Product Sgm X11) = 0 from scheme2; then A27: p |-count (Product Sgm X11) = 0 by A25; for p being Prime, n being Element of NAT, m being non zero Element of NAT , X11 being set st X11 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P11[n,m,p9]} holds Product Sgm X11 > 0 from scheme1; then A28: Product Sgm(X11) <> 0; X1 \/ X2 c= X \/ X by A12,A23,XBOOLE_1:13; then Sum (p |-count (Sgm X)) = Sum (p |-count (Sgm (X1 \/ X2))) by A22, XBOOLE_0:def 10 .= Sum (p |-count (Sgm(X1) ^ Sgm(X2))) by A13,A24,A1,FINSEQ_3:42 .= Sum ((p |-count Sgm(X1)) ^ (p |-count Sgm(X2))) by Th50 .= Sum (p |-count Sgm(X1)) + Sum (p |-count Sgm(X2)) by RVSUM_1:75; then p |-count (Product Sgm X) = Sum (p |-count Sgm(X1)) + Sum (p |-count Sgm(X2)) by A9,Th52 .= Sum (p |-count Sgm(X1)) + 0 by A20,A19,Th52 .= 0 + Sum (p |-count Sgm(X12)) by A18,A28,A27,Th52 .= Sum (p |-count Sgm({p|^(p |-count m)})) by A26,A8,XBOOLE_0:def 10 .= Sum (p |-count <* m1 *>) by FINSEQ_3:44 .= Sum <* p |-count m1 *> by Th51 .= p |-count m1 by RVSUM_1:73; hence thesis by A11; end; Lm10: for n, m being Element of NAT st m = 2*n choose n & n>=3 holds m = Product Sgm {p|^(p |-count m) where p is prime Element of NAT: p<=sqrt(2*n) & p |-count m>0} * Product Sgm {p|^(p |-count m) where p is prime Element of NAT: sqrt(2*n)

0} * Product Sgm {p|^(p |-count m) where p is prime Element of NAT: n

0} proof defpred P3[Element of NAT,Element of NAT,Prime] means \$1<\$3 & \$3<=2*\$1 & \$3 |-count \$2>0; defpred P2[Element of NAT,Element of NAT,Prime] means sqrt(2*\$1)<\$3 & \$3<=2* \$1/3 & \$3 |-count \$2>0; defpred P1[Element of NAT,Element of NAT,Prime] means \$3<=sqrt(2*\$1) & \$3 |-count \$2>0; let n, m be Element of NAT; assume A1: m = 2*n choose n; set X3 = {p|^(p |-count m) where p is prime Element of NAT: P3[n,m,p]}; set X2 = {p|^(p |-count m) where p is prime Element of NAT: P2[n,m,p]}; set X1 = {p|^(p |-count m) where p is prime Element of NAT: P1[n,m,p]}; set f1 = Sgm X1; set f2 = Sgm X2; set f3 = Sgm X3; set n1=Product f1; set n2=Product f2; set n3=Product f3; A2: for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P2[n,m,p9]} & not p|^(p |-count m) in X holds p |-count (Product Sgm X) = 0 from scheme2; set k = Product f1 * Product f2 * Product f3; A3: for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P1[n,m,p9]} holds Product Sgm X > 0 from scheme1; assume A4: n >= 3; A5: now 2*n<3*n by A4,XREAL_1:68; then A6: 2*n/3<3*n/3 by XREAL_1:74; assume n<2*n/3; hence contradiction by A6; end; A7: now sqrt 2 < sqrt 3 & sqrt 3 <= sqrt n by A4,SQUARE_1:26,27; then A8: sqrt 2 < sqrt n by XXREAL_0:2; sqrt n > 0 by A4,SQUARE_1:25; then (sqrt 2)*(sqrt n) < (sqrt n)*(sqrt n) by A8,XREAL_1:68; then sqrt(2*n) < (sqrt n)*(sqrt n) by SQUARE_1:29; then A9: sqrt(2*n) < sqrt(n^2) by SQUARE_1:29; assume n= 4|^n / (2*n) * (2*n) by A1,Th6,XREAL_1:64; then A10: m<>0 by A4; A11: for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P3[n,m,p9]} holds Product Sgm X > 0 from scheme1; then A12: Product f3 > 0 by A10; A13: for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P2[n,m,p9]} holds Product Sgm X > 0 from scheme1; then A14: Product f2 > 0 by A10; A15: for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P3[n,m,p9]} & not p|^(p |-count m) in X holds p |-count (Product Sgm X) = 0 from scheme2; A16: for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P1[n,m,p9]} & not p|^(p |-count m) in X holds p |-count (Product Sgm X) = 0 from scheme2; A17: for p being Prime st p>2*n holds p |-count n1 = 0 & p |-count n2 = 0 & p |-count n3 = 0 proof let p be Prime; assume A18: p>2*n; then A19: p |-count m = 0 by A1,A4,Lm9; now assume p|^(p |-count m) in X1; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m) & P1[n,m,p9]; hence contradiction by A10,A19,Th22; end; hence p |-count n1 = 0 by A10,A16; now assume p|^(p |-count m) in X2; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m) & P2[n,m,p9]; hence contradiction by A10,A19,Th22; end; hence p |-count n2 = 0 by A10,A2; now assume p|^(p |-count m) in X3; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m) & P3[n,m,p9]; hence contradiction by A10,A18,Th22; end; hence thesis by A10,A15; end; A20: for p being Prime st 2*n/3

0; then p|^(p |-count m) in X2 by A26,A27,A28; hence thesis by A10,A24; end; suppose A29: p |-count m = 0; now assume p|^(p |-count m) in X2; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m)& P2[n,m,p9]; hence contradiction by A10,A29,Th22; end; hence thesis by A10,A2,A29; end; end; A30: for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P3[n,m,p9]} & p|^(p |-count m) in X holds p |-count (Product Sgm X) = p |-count m from scheme3; A31: for p being Prime st n

0; then p|^(p |-count m) in X3 by A32,A33,A34; hence thesis by A10,A30; end; suppose A35: p |-count m = 0; now assume p|^(p |-count m) in X3; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m)& P3[n,m,p9]; hence contradiction by A10,A35,Th22; end; hence thesis by A10,A15,A35; end; end; A36: for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P1[n,m,p9]} & p|^(p |-count m) in X holds p |-count (Product Sgm X) = p |-count m from scheme3; A37: for p being Prime st p<=sqrt(2*n) holds p |-count n2 = 0 & p |-count n3 = 0 & p |-count n1 = p |-count m proof let p be Prime; A38: p in NAT by ORDINAL1:def 12; assume A39: p<=sqrt(2*n); now assume p|^(p |-count m) in X2; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m) & P2[n,m,p9]; hence contradiction by A10,A39,Th22; end; hence p |-count n2 = 0 by A10,A2; now assume p|^(p |-count m) in X3; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m) & P3[n,m,p9]; then n

0; then p|^(p |-count m) in X1 by A39,A38; hence thesis by A10,A36; end; suppose A40: p |-count m = 0; now assume p|^(p |-count m) in X1; then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count m)& P1[n,m,p9]; hence contradiction by A10,A40,Th22; end; hence thesis by A10,A16,A40; end; end; A41: for p being Element of NAT st p is prime holds p |-count m = p |-count k proof reconsider n3 as non zero Element of NAT by A10,A11; reconsider n2 as non zero Element of NAT by A10,A13; reconsider n1 as non zero Element of NAT by A10,A3; let p be Element of NAT; assume A42: p is prime; then A43: p |-count k = (p |-count (n1*n2)) + (p |-count n3) by NAT_3:28 .= (p |-count n1)+(p |-count n2)+(p |-count n3) by A42,NAT_3:28; per cases; suppose A44: p>2*n; then A45: p |-count n2 = 0 by A17,A42; p |-count m = 0 & p |-count n1 = 0 by A1,A4,A17,A42,A44,Lm9; hence thesis by A17,A42,A43,A44,A45; end; suppose A46: n

0 by A10,A3; hence thesis by A10,A14,A12,A41,Th21; end; scheme scheme4 { A(set,set) -> set, P[set,set] } : for n,m being Element of NAT, r being Real, X being finite set st X = {A(p,m) where p is prime Element of NAT: p <= r & P[p,m]} & r>=0 holds card X <= [\ r /] proof let n,m be Element of NAT; defpred P1[Nat] means for n,m being Element of NAT, r being Real, X being finite set st X = {A(p,m) where p is prime Element of NAT: p <= r & P[p ,m]} & r>=0 & \$1 = [\ r /] holds card X <= [\ r /]; A1: for n being Nat st P1[n] holds P1[n+1] proof let n be Nat; assume A2: P1[n]; now let m be Element of NAT; let r be Real; let X be finite set; set r1 = r - 1; set X1 = {A(p,m) where p is prime Element of NAT: p <= r1 & P[p,m]}; set X2 = {A(p,m) where p is prime Element of NAT: r1 < p & p <= r & P[p, m]}; A3: 0+n <= 1+n by XREAL_1:6; assume A4: X = {A(p,m) where p is prime Element of NAT: p <= r & P[p,m]}; now let x be object; assume A5: x in X1 \/ X2; per cases by A5,XBOOLE_0:def 3; suppose x in X1; then consider p being prime Element of NAT such that A6: A(p,m)=x and A7: p<=r1 and A8: P[p,m]; -1+r<=0+r by XREAL_1:6; then p<=r by A7,XXREAL_0:2; hence x in X by A4,A6,A8; end; suppose x in X2; then ex p being prime Element of NAT st A(p,m)=x & r1 < p & p<=r & P [p,m]; hence x in X by A4; end; end; then A9: X1 \/ X2 c= X; assume r >= 0; now let x be object; assume x in X; then consider p being prime Element of NAT such that A10: A(p,m)=x & p<=r & P[p,m] by A4; A(p,m)=x & p<=r1 & P[p,m] or A(p,m)=x & r1

=0 by INT_1:def 6; then A15: card X1 <= [\ r1 /] by A2,A13; per cases; suppose not ex x being object st x in X2; then X2={} by XBOOLE_0:def 1; hence card X <= [\ r /] by A12,A13,A11,A15,A3,XXREAL_0:2; end; suppose A16: ex x being set st x in X2; then consider x be set such that A17: x in X2; A18: now assume X2<>{x}; then consider y be object such that A19: y in X2 and A20: y<>x by A16,ZFMISC_1:35; consider p1 be prime Element of NAT such that A21: A(p1,m)=x and A22: r1=0; assume A26: 0 = [\ r /]; then r - 1 < 0 by INT_1:def 6; then A27: r - 1 + 1 < 0 + 1 by XREAL_1:6; now let x be object; assume x in X; then consider p be prime Element of NAT such that A(p,m)=x and A28: p<=r and P[p,m] by A25; p<1 by A27,A28,XXREAL_0:2; hence contradiction by INT_2:def 4; end; hence thesis by A26,CARD_1:27,XBOOLE_0:def 1; end; A29: for n being Nat holds P1[n] from NAT_1:sch 2(A24,A1); let r be Real; let X be finite set; assume that A30: X = {A(p,m) where p is prime Element of NAT: p <= r & P[p,m]} and A31: r>=0; [\ r /] is Element of NAT by A31,INT_1:53; hence thesis by A29,A30,A31; end; Lm11: for n, m being Element of NAT st m = 2*n choose n & n>=3 holds Product Sgm {p|^(p |-count m) where p is prime Element of NAT: p<=sqrt(2*n) & p |-count m>0} <= (2*n) to_power sqrt(2*n) proof deffunc A(Element of NAT,Element of NAT) = \$1|^(\$1 |-count \$2); defpred P[Element of NAT,Element of NAT] means \$1 |-count \$2 > 0; let n, m be Element of NAT; assume A1: m = 2*n choose n; set r = sqrt(2*n); A2: r>=0 by SQUARE_1:def 2; A3: for n,m being Element of NAT, r being Real, X being finite set st X = { A(k,m) where k is prime Element of NAT: k <= r & P[k,m]} & r>=0 holds card X <= [\ r /] from scheme4; set XX=Seg m; set X = {p|^(p |-count m) where p is prime Element of NAT: p<=sqrt(2*n) & p |-count m>0}; assume A4: n>=3; set f1 = Sgm X; set f2 = (len f1) |-> (2*n); m * (2*n) >= 4|^n / (2*n) * (2*n) by A1,Th6,XREAL_1:64; then A5: m<>0 by A4; now let x be object; assume x in X; then ex p being prime Element of NAT st p|^(p |-count m) = x & p<=sqrt(2*n) & p |-count m>0; then ex b being Element of NAT st b=x & 1<=b & b<=m by A5,Th16; hence x in XX by FINSEQ_1:1; end; then A6: X c= Seg m; A7: now let k be Element of NAT; assume A8: k in dom f1; rng f1 = X by A6,FINSEQ_1:def 13; then f1.k in X by A8,FUNCT_1:3; then A9: ex p being prime Element of NAT st p|^(p |-count m)=f1.k & p<=sqrt(2* n) & p |-count m>0; k in Seg len f1 by A8,FINSEQ_1:def 3; then f2.k = 2*n by FUNCOP_1:7; hence f1.k<=f2.k & f1.k>0 by A1,A4,A9,Lm9; end; reconsider X as finite set by A6; A10: len f1 = len f2 by CARD_1:def 7; rng f1 c= REAL; then reconsider f1 as FinSequence of REAL by FINSEQ_1:def 4; A11: rng f2 c= REAL; reconsider rr=r as Real; A12: rr >= 0 by A2; len f1 = card X by A6,FINSEQ_3:39; then [\ sqrt(2*n) /] <= sqrt(2*n) & len f1 <= [\ sqrt(2*n) /] by A12,A3, INT_1:def 6; then len f1 <= sqrt(2*n) by XXREAL_0:2; then A13: len f1 < sqrt(2*n) or len f1 = sqrt(2*n) by XXREAL_0:1; reconsider f2 as FinSequence of REAL by A11,FINSEQ_1:def 4; Product f1 <= Product f2 by A10,A7,Th53; then A14: Product f1 <= (2*n) to_power len(f1) by A4,Th54; n*2 >= 3*2 by A4,XREAL_1:64; then 2*n > 1 by XXREAL_0:2; then (2*n) to_power len f1 <= (2*n) to_power sqrt(2*n) by A13,POWER:39; hence thesis by A14,XXREAL_0:2; end; begin :: Bertrand's postulate. ::\$N Bertrand's postulate theorem for n being Element of NAT st n>=1 holds ex p being Prime st n

=1; per cases; suppose n<4000; then n<4001 by XXREAL_0:2; hence thesis by A1,Lm7; end; suppose A2: n>=4000; set m = 2*n choose n; set X1={p|^(p |-count m) where p is prime Element of NAT: p<=sqrt(2*n) & p |-count m>0}; set X2={p|^(p |-count m) where p is prime Element of NAT: sqrt(2*n)

0}; set X3={p|^(p |-count m) where p is prime Element of NAT: n

0}; assume A3: not ex p being Prime st n

{}; then consider x be object such that A4: x in X3 by XBOOLE_0:def 1; ex p be prime Element of NAT st p|^(p |-count m)=x & n

0 by A4; hence contradiction by A3; end; then A5: m = (Product Sgm X1)*(Product Sgm X2)*1 by A2,Lm10,FINSEQ_3:43,RVSUM_1:94 ,XXREAL_0:2; A6: 4|^n / (2*n) <= m by Th6; set X = {p where p is prime Element of NAT: p<=2*n/3}; A7: n>=3 by A2,XXREAL_0:2; then n/3>=3/3 by XREAL_1:72; then (n/3)*2>=1*2 by XREAL_1:64; then A8: Product Sgm X <= (4 to_power ((2*n/3)-1)) by Th45; set mm=[/ 2*n/3 \]; reconsider mm as Element of NAT by INT_1:53; set XX=Seg mm; A9: now assume {} in X; then ex p being prime Element of NAT st p = {} & p<=2*n/3; hence contradiction; end; -1+(2*n/3)<0+(2*n/3) by XREAL_1:6; then A10: 4 to_power ((2*n/3)-1) < 4 to_power (2*n/3) by POWER:39; now let x be object; assume x in X2; then consider p be prime Element of NAT such that A11: p|^(p |-count m)=x and A12: sqrt(2*n)

0; p |-count m <= 1 by A7,A12,A13,Lm9; then p |-count m < 1+1 by NAT_1:13; then p |-count m = 1 by A14,NAT_1:23; then p=x by A11; hence x in X by A13; end; then A15: X2 c= X; now let x be object; assume x in X; then consider p being prime Element of NAT such that A16: p = x and A17: p<=2*n/3; A18: 1<=p by INT_2:def 4; 2*n/3<=[/ 2*n/3 \] by INT_1:def 7; then p<=[/ 2*n/3 \] by A17,XXREAL_0:2; hence x in XX by A16,A18,FINSEQ_1:1; end; then A19: X c= Seg mm; then X c= NAT by XBOOLE_1:1; then Product Sgm X2 <= Product Sgm X by A19,A9,A15,Th42; then A20: Product Sgm X2 <= (4 to_power ((2*n/3)-1)) by A8,XXREAL_0:2; n>=3 by A2,XXREAL_0:2; then Product Sgm X1 <= (2*n) to_power sqrt(2*n) by Lm11; then m <= ((2*n) to_power sqrt(2*n))*(4 to_power ((2*n/3)-1)) by A20,A5, XREAL_1:66; then A21: 4|^n / (2*n) <= ((2*n) to_power sqrt(2*n))*(4 to_power ((2*n/3)-1 )) by A6,XXREAL_0:2; A22: 4 to_power (2*n/3)>0 by POWER:34; (2*n) to_power sqrt(2*n)>0 by A2,POWER:34; then (4 to_power ((2*n/3)-1))*((2*n) to_power sqrt(2*n)) < (4 to_power (2* n/3))*((2*n) to_power sqrt(2*n)) by A10,XREAL_1:68; then 4|^n / (2*n) <= ((2*n) to_power sqrt(2*n))*(4 to_power (2*n/3)) by A21 ,XXREAL_0:2; then 4|^n/(2*n)*(2*n)<=((2*n) to_power sqrt(2*n))*(4 to_power (2*n/3))*(2* n) by XREAL_1:64; then 4|^n = 4 to_power (3*n/3) & 4|^n<=((2*n) to_power sqrt(2*n))*(2*n)*(4 to_power (2*n/3)) by A2,POWER:41,XCMPLX_1:87; then (4 to_power (3*n/3))/(4 to_power (2*n/3)) <= (((2*n) to_power sqrt(2* n))*(2*n))* (4 to_power (2*n/3))/(4 to_power (2*n/3)) by A22,XREAL_1:72; then (4 to_power (3*n/3))/(4 to_power (2*n/3)) <= ((2*n) to_power sqrt(2*n ))*(2*n) by A22,XCMPLX_1:89; then 4 to_power ((3*n/3)-(2*n/3)) <= ((2*n) to_power sqrt(2*n))*(2*n) by POWER:29; then 4 to_power (n/3) <= ((2*n) to_power sqrt(2*n))*((2*n) to_power 1) by POWER:25; then 4 to_power (n/3) <= (2*n) to_power (sqrt(2*n)+1) by A2,POWER:27; then A23: 4 to_power (n/3) < (2*n) to_power (sqrt(2*n)+1) or 4 to_power (n/3) = (2*n) to_power (sqrt(2*n)+1) by XXREAL_0:1; 4 to_power (n/3)>0 by POWER:34; then (4 to_power (n/3)) to_power 3 <= ((2*n) to_power (sqrt(2*n)+1)) to_power 3 by A23,POWER:37; then 4 to_power ((n/3)*3) <= ((2*n) to_power (sqrt(2*n)+1)) to_power 3 by POWER:33; then A24: 4 to_power n <= (2*n) to_power ((sqrt(2*n)+1)*3) by A2,POWER:33; reconsider 2n=2*n as Real; A25: 6-root(2*n) to_power 6 = 6-root(2n) |^ 6 by POWER:41 .= 2n by COMPTRIG:4; 2 to_power 2 = 2|^2 by POWER:41 .= Product <* 2, 2 *> by FINSEQ_2:61 .= 2*2 by RVSUM_1:99; then A26: 2 to_power (2*n)>0 & 4 to_power n = 2 to_power (2*n) by POWER:33,34; set n1=[\ 6-root(2*n) /]; 6-root(2*n) -1 < n1 by INT_1:def 6; then A27: 6-root(2*n) -1 +1 < n1 +1 by XREAL_1:6; 6-root(2*n) > 6-root 0 by A2,POWER:17; then A28: 6-root(2*n) > 0 by POWER:5; then reconsider n1 as Element of NAT by INT_1:53; n1 <= 6-root(2*n) by INT_1:def 6; then n1 < 6-root(2*n) or n1 = 6-root(2*n) by XXREAL_0:1; then A29: 2 to_power n1 <= 2 to_power (6-root(2*n)) by POWER:39; n1+1 <= 2|^n1 by NEWTON:85; then n1+1 <= 2 to_power n1 by POWER:41; then n1+1 <= 2 to_power (6-root(2*n)) by A29,XXREAL_0:2; then n1+1 < 2 to_power (6-root(2*n)) or n1+1 = 2 to_power (6-root(2*n)) by XXREAL_0:1; then A30: (n1+1) to_power 6 <= (2 to_power (6-root(2*n))) to_power 6 by POWER:37; 6-root(2*n) to_power 6 < (n1+1) to_power 6 by A27,A28,POWER:37; then 2*n < (2 to_power (6-root(2*n))) to_power 6 by A30,A25,XXREAL_0:2; then A31: 2*n < 2 to_power ((6-root(2*n))*6) by POWER:33; sqrt(2*n)>0 by A2,SQUARE_1:25; then (2*n) to_power ((sqrt(2*n)+1)*3) < (2 to_power ((6-root(2*n))*6)) to_power ((sqrt(2*n)+1)*3) by A2,A31,POWER:37; then 4 to_power n < (2 to_power ((6-root(2*n))*6)) to_power ((sqrt(2*n)+1) *3) by A24,XXREAL_0:2; then 4 to_power n < 2 to_power (((6-root(2*n))*6)*((sqrt(2*n)+1)*3)) by POWER:33; then log(2,2 to_power (2*n)) < log(2,2 to_power (((6-root(2*n))*6)*((sqrt( 2*n)+1)*3))) by A26,POWER:57; then (2*n)*log(2,2) < log(2,2 to_power (((6-root(2*n))*6)*((sqrt(2*n)+1)*3 ))) by POWER:55; then (2*n)*log(2,2) < (((6-root(2*n))*6)*((sqrt(2*n)+1)*3))*log(2,2) by POWER:55; then (2*n)*1 < (((6-root(2*n))*6)*((sqrt(2*n)+1)*3))*log(2,2) by POWER:52; then A32: 2*n < (((6-root(2*n))*6)*((sqrt(2*n)+1)*3))*1 by POWER:52; 42 < n by A2,XXREAL_0:2; then 42*2 < n*2 by XREAL_1:68; then 81 < 2*n by XXREAL_0:2; then A33: sqrt(81) < sqrt(2*n) by SQUARE_1:27; 81=9^2; then sqrt 81 = 9 by SQUARE_1:22; then 9*2 < sqrt(2*n)*2 by A33,XREAL_1:68; then 18 + 18*sqrt(2*n) < 2*sqrt(2*n)+18*sqrt(2*n) by XREAL_1:6; then (18 + 18*sqrt(2*n))*(6-root(2*n)) < 20*sqrt(2*n)*(6-root(2*n)) by A28, XREAL_1:68; then 2*n < 20*(sqrt(2*n)*(6-root(2*n))) by A32,XXREAL_0:2; then 2*n < 20*((2-Root(2*n))*(6-root(2*n))) by PREPOWER:32; then 2*n < 20*((2-root(2*n))*(6-root(2*n))) by POWER:def 1; then 2*n < 20*(((2*n) to_power (1/2))*(6-root(2*n))) by POWER:45; then 2*n < 20*(((2*n) to_power (1/2))*((2*n) to_power (1/6))) by POWER:45; then A34: 2*n < 20*((2*n) to_power (1/2+1/6)) by A2,POWER:27; A35: (2*n) to_power (2/3)<>0 by A2,POWER:34; (2*n) to_power (2/3)>0 by A2,POWER:34; then (2*n)/((2*n) to_power (2/3)) < 20*((2*n) to_power (2/3))/((2*n) to_power (2/3)) by A34,XREAL_1:74; then (2*n)/((2*n) to_power (2/3)) < 20 by A35,XCMPLX_1:89; then ((2*n) to_power 1)/((2*n) to_power (2/3)) < 20 by POWER:25; then A36: ((2*n) to_power (1-(2/3))) < 20 by A2,POWER:29; (2*n) to_power (1/3)>0 by A2,POWER:34; then ((2*n) to_power (1/3)) to_power 3 < 20 to_power 3 by A36,POWER:37; then ((2*n) to_power ((1/3)*3)) < 20 to_power 3 by A2,POWER:33; then 2*n < 20 to_power (2+1) by POWER:25; then 2*n < (20 to_power 2)*(20 to_power 1) by POWER:27; then 2*n < (20 to_power (1+1))*20 by POWER:25; then 2*n < (20 to_power 1)*(20 to_power 1)*20 by POWER:27; then 2*n < (20 to_power 1)*20*20 by POWER:25; then 2*n < 20*20*20 by POWER:25; then 2*n/2 < 8000/2 by XREAL_1:74; hence contradiction by A2; end; end;