nat_4.miz

begin

 theorem :: NAT_4:1



 Th1: for r,s be Real holds 0 <= r & (s * s) < (r * r) implies s < r

 proof

 let r,s be Real;

 assume that

 A1: 0 <= r and

 A2: (s * s) < (r * r);

 assume s >= r;

 then (r * s) <= (s * s) & (r * r) <= (s * r) by A1, XREAL_1: 64;

 hence contradiction by A2, XXREAL_0: 2;

 end;

 theorem :: NAT_4:2



 Th2: for r,s be Real holds 1 < r & (r * r) <= s implies r < s

 proof

 let r,s be Real;

 assume that

 A1: 1 < r and

 A2: (r * r) <= s;

 r < (r * r) by A1, XREAL_1: 155;

 hence thesis by A2, XXREAL_0: 2;

 end;

 theorem :: NAT_4:3



 Th3: for a,n be Nat st a > 1 holds (a |^ n) > n

 proof

 defpred P[ Nat] means for a be Nat st a > 1 holds (a |^ $1) > $1;



 A1: for n be Nat holds P[n] implies P[(n + 1)]

 proof

 let n be Nat;

 assume

 A2: P[n];

 now

 let a be Nat;

 assume

 A3: a > 1;

 then a >= (1 + 1) by NAT_1: 13;

 then

 A4: (a * n) >= (2 * n) by XREAL_1: 64;

 per cases ;

 suppose n = 0 ;

 hence (a |^ (n + 1)) > (n + 1) by A3;

 end;

 suppose n > 0 ;

 then n >= ( 0 + 1) by NAT_1: 13;

 then (n + n) >= (n + 1) by XREAL_1: 6;

 then

 A5: (a * n) >= (n + 1) by A4, XXREAL_0: 2;

 ((a |^ n) * a) > (n * a) by A2, A3, XREAL_1: 68;

 then (a |^ (n + 1)) > (n * a) by NEWTON: 6;

 hence (a |^ (n + 1)) > (n + 1) by A5, XXREAL_0: 2;

 end;

 end;

 hence thesis;

 end;



 A6: P[ 0 ];

 for n be Nat holds P[n] from NAT_1:sch 2( A6, A1);

 hence thesis;

 end;

 theorem :: NAT_4:4



 Th4: for n,k,m be Nat st k <= n & m = [\(n / 2)/] holds (n choose m) >= (n choose k)

 proof

 defpred P[ Nat] means for k,m be Nat st k <= m & m = [\($1 / 2)/] holds ($1 choose m) >= ($1 choose k);



 A1: ((1 / 2) - 1) < 0 ;



 A2: for n be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume

 A3: P[n];

 for k,m1 be Nat st k <= m1 & m1 = [\((n + 1) / 2)/] holds ((n + 1) choose m1) >= ((n + 1) choose k)

 proof

 [\(n / 2)/] <= (n / 2) by INT_1:def 6;

 then ( - [\(n / 2)/]) >= ( - (n / 2)) by XREAL_1: 24;

 then

 A4: (( - [\(n / 2)/]) + (n + 1)) >= (( - (n / 2)) + (n + 1)) by XREAL_1: 6;

 set m = [\(n / 2)/];

 let k,m1 be Nat;

 assume

 A5: k <= m1;

 set nk1 = ((n + 1) - k);

 set l = (n - m);

 reconsider m as Element of NAT by INT_1: 53;

 (2 * n) >= (1 * n) by XREAL_1: 64;

 then

 A6: (n / 2) >= [\(n / 2)/] & ((2 * n) / 2) >= (n / 2) by INT_1:def 6, XREAL_1: 72;

 then

 A7: n >= m by XXREAL_0: 2;

 (n - m) = (n -' m) by A6, XREAL_1: 233, XXREAL_0: 2;

 then

 reconsider l as Element of NAT ;

 (((n + 1) ! ) / (n ! )) = (((n + 1) * (n ! )) / (n ! )) by NEWTON: 15

 .= ((n + 1) * ((n ! ) / (n ! ))) by XCMPLX_1: 74

 .= ((n + 1) * 1) by XCMPLX_1: 60;

 then

 A8: ((n ! ) / ((n + 1) ! )) = (1 / (n + 1)) by XCMPLX_1: 57;



 A9: (( - (n / 2)) + (n + 1)) = ((n / 2) + 1);

 set nk = (n - k);

 set l1 = ((n + 1) -' m1);



 A10: (1 * m1) <= (2 * m1) by XREAL_1: 64;

 assume

 A11: m1 = [\((n + 1) / 2)/];

 then m1 <= ((n + 1) / 2) by INT_1:def 6;

 then

 A12: (m1 * 2) <= (((n + 1) / 2) * 2) by XREAL_1: 64;

 then

 A13: (n + 1) >= m1 & l1 = ((n + 1) - m1) by A10, XREAL_1: 233, XXREAL_0: 2;



 A14: ((n + 1) / 2) >= [\((n + 1) / 2)/] by INT_1:def 6;



 A15: n >= k

 proof

 per cases ;

 suppose n = 0 ;

 hence thesis by A1, A5, A11, INT_1:def 6;

 end;

 suppose n <> 0 ;

 then (n + 1) > ( 0 + 1) by XREAL_1: 6;

 then n >= 1 by NAT_1: 13;

 then (n + n) >= (1 + n) by XREAL_1: 6;

 then ((2 * n) / 2) >= ((n + 1) / 2) by XREAL_1: 72;

 then n >= [\((n + 1) / 2)/] by A14, XXREAL_0: 2;

 hence thesis by A5, A11, XXREAL_0: 2;

 end;

 end;

 then (n - k) = (n -' k) by XREAL_1: 233;

 then

 reconsider nk as Element of NAT ;

 ((n / 2) - 1) < [\(n / 2)/] by INT_1:def 6;

 then

 A16: (((n / 2) - 1) + 1) < ( [\(n / 2)/] + 1) by XREAL_1: 6;

 ((n + 1) - k) = (nk + 1);

 then

 reconsider nk1 as Element of NAT ;

 ( 0 + n) <= (1 + n) by XREAL_1: 6;

 then

 A17: k <= (n + 1) by A15, XXREAL_0: 2;

 then

 A18: ((n + 1) choose k) = (((n + 1) ! ) / ((nk1 ! ) * (k ! ))) by NEWTON:def 3;



 A19: ((nk1 ! ) / (nk ! )) = (((nk + 1) * (nk ! )) / (nk ! )) by NEWTON: 15

 .= ((nk + 1) * ((nk ! ) / (nk ! ))) by XCMPLX_1: 74

 .= ((nk + 1) * 1) by XCMPLX_1: 60;

 (n choose k) = ((n ! ) / ((nk ! ) * (k ! ))) by A15, NEWTON:def 3;



 then ((n choose k) / ((n + 1) choose k)) = (((n ! ) / ((nk ! ) * (k ! ))) / (((n + 1) ! ) / ((nk1 ! ) * (k ! )))) by A17, NEWTON:def 3

 .= ((((n ! ) / ((nk ! ) * (k ! ))) / ((n + 1) ! )) * ((nk1 ! ) * (k ! ))) by XCMPLX_1: 82

 .= (((n ! ) / (((n + 1) ! ) * ((nk ! ) * (k ! )))) * ((nk1 ! ) * (k ! ))) by XCMPLX_1: 78

 .= (((1 / (n + 1)) / ((nk ! ) * (k ! ))) * ((nk1 ! ) * (k ! ))) by A8, XCMPLX_1: 78

 .= ((1 / (n + 1)) / (((nk ! ) * (k ! )) / ((nk1 ! ) * (k ! )))) by XCMPLX_1: 82

 .= ((1 / (n + 1)) / (((nk ! ) / (nk1 ! )) / ((k ! ) / (k ! )))) by XCMPLX_1: 84

 .= ((1 / (n + 1)) / (((nk ! ) / (nk1 ! )) / 1)) by XCMPLX_1: 60

 .= ((1 / (n + 1)) / (1 / (nk + 1))) by A19, XCMPLX_1: 57

 .= ((1 * (nk + 1)) / (1 * (n + 1))) by XCMPLX_1: 84

 .= ((nk + 1) / (n + 1));

 then

 A20: ((n choose k) / (((n + 1) choose k) / ((n + 1) choose k))) = (((nk + 1) / (n + 1)) * ((n + 1) choose k)) by XCMPLX_1: 82;



 A21: (n choose k) = ((n choose k) / 1)

 .= (((nk + 1) / (n + 1)) * ((n + 1) choose k)) by A18, A20, XCMPLX_1: 60;



 then

 A22: ((n choose k) * ((n + 1) / (l + 1))) = (((((nk + 1) / (n + 1)) * ((n + 1) choose k)) * (n + 1)) / (l + 1)) by XCMPLX_1: 74

 .= (((((nk + 1) / (n + 1)) * (n + 1)) * ((n + 1) choose k)) / (l + 1))

 .= (((((n + 1) / (n + 1)) * (nk + 1)) * ((n + 1) choose k)) / (l + 1)) by XCMPLX_1: 75

 .= (((1 * (nk + 1)) * ((n + 1) choose k)) / (l + 1)) by XCMPLX_1: 60

 .= (((n + 1) choose k) * ((nk + 1) / (l + 1))) by XCMPLX_1: 74;



 A23: ((n choose k) * ((n + 1) / (m + 1))) = (((((nk + 1) / (n + 1)) * ((n + 1) choose k)) * (n + 1)) / (m + 1)) by A21, XCMPLX_1: 74

 .= (((((nk + 1) / (n + 1)) * (n + 1)) * ((n + 1) choose k)) / (m + 1))

 .= (((((n + 1) / (n + 1)) * (nk + 1)) * ((n + 1) choose k)) / (m + 1)) by XCMPLX_1: 75

 .= (((1 * (nk + 1)) * ((n + 1) choose k)) / (m + 1)) by XCMPLX_1: 60

 .= (((n + 1) choose k) * ((nk + 1) / (m + 1))) by XCMPLX_1: 74;

 per cases ;

 suppose n is even;

 then

 consider k1 be Nat such that

 A24: n = (2 * k1) by ABIAN:def 2;



 A25: [\((n + 1) / 2)/] = [\(((2 * k1) / 2) + (1 / 2))/] by A24

 .= (k1 + [\(1 / 2)/]) by INT_1: 28

 .= (k1 + 0 ) by A1, INT_1:def 6

 .= [\(n / 2)/] by A24, INT_1: 25;

 then

 A26: (n choose m) >= (n choose k) by A3, A5, A11;

 ( - k) >= ( - [\(n / 2)/]) by A5, A11, A25, XREAL_1: 24;

 then (( - k) + (n + 1)) >= (( - [\(n / 2)/]) + (n + 1)) by XREAL_1: 6;

 then (((n - k) + 1) / ((n - [\(n / 2)/]) + 1)) >= (((n - [\(n / 2)/]) + 1) / ((n - [\(n / 2)/]) + 1)) by A4, A9, XREAL_1: 72;

 then (((n - k) + 1) / ((n - [\(n / 2)/]) + 1)) >= 1 by A4, A9, XCMPLX_1: 60;

 then

 A27: ((((n - k) + 1) / ((n - [\(n / 2)/]) + 1)) * ((n + 1) choose k)) >= (1 * ((n + 1) choose k)) by XREAL_1: 64;



 A28: l1 = ((n + 1) - m1) by A12, A10, XREAL_1: 233, XXREAL_0: 2

 .= (l + 1) by A11, A25;

 ((n + 1) choose m1) = (((n + 1) ! ) / ((m1 ! ) * (l1 ! ))) by A13, NEWTON:def 3

 .= (((n + 1) * (n ! )) / ((m ! ) * ((l + 1) ! ))) by A11, A25, A28, NEWTON: 15

 .= (((n + 1) * (n ! )) / ((m ! ) * ((l + 1) * (l ! )))) by NEWTON: 15

 .= (((n + 1) * (n ! )) / ((l + 1) * ((m ! ) * (l ! ))))

 .= (((n + 1) / (l + 1)) / (((m ! ) * (l ! )) / (n ! ))) by XCMPLX_1: 84

 .= (((n ! ) / ((m ! ) * (l ! ))) * ((n + 1) / (l + 1))) by XCMPLX_1: 80

 .= ((n choose m) * ((n + 1) / (l + 1))) by A7, NEWTON:def 3;

 then ((n + 1) choose m) >= (((n + 1) choose k) * ((nk + 1) / (l + 1))) by A11, A22, A25, A26, XREAL_1: 64;

 hence thesis by A11, A25, A27, XXREAL_0: 2;

 end;

 suppose not n is even;

 then

 consider j be Integer such that

 A29: n = ((2 * j) + 1) by ABIAN: 1;



 A30: [\((n + 1) / 2)/] = ((j + 0 ) + 1) by A29, INT_1: 25

 .= ((j + [\(1 / 2)/]) + 1) by A1, INT_1:def 6

 .= ( [\(j + (1 / 2))/] + 1) by INT_1: 28

 .= ( [\(n / 2)/] + 1) by A29;



 A31: l1 = ((n + 1) - m1) by A12, A10, XREAL_1: 233, XXREAL_0: 2

 .= l by A11, A30;

 per cases by A5, A11, A30, XXREAL_0: 1;

 suppose k = (m + 1);

 hence thesis by A11, A30;

 end;

 suppose k < (m + 1);

 then

 A32: k <= m by NAT_1: 13;

 then

 A33: (n choose m) >= (n choose k) by A3;

 (n / 2) >= [\(n / 2)/] by INT_1:def 6;

 then ((n / 2) * 2) >= ( [\(n / 2)/] * 2) by XREAL_1: 64;

 then (n - [\(n / 2)/]) >= (( [\(n / 2)/] * 2) - [\(n / 2)/]) by XREAL_1: 9;

 then (n - [\(n / 2)/]) >= k by A32, XXREAL_0: 2;

 then ((n - [\(n / 2)/]) - (k - [\(n / 2)/])) >= (k - (k - [\(n / 2)/])) by XREAL_1: 9;

 then ((n - k) + 1) >= ( [\(n / 2)/] + 1) by XREAL_1: 6;

 then (((n - k) + 1) / ( [\(n / 2)/] + 1)) >= (( [\(n / 2)/] + 1) / ( [\(n / 2)/] + 1)) by A16, XREAL_1: 72;

 then (((n - k) + 1) / ( [\(n / 2)/] + 1)) >= 1 by A16, XCMPLX_1: 60;

 then

 A34: ((((n - k) + 1) / ( [\(n / 2)/] + 1)) * ((n + 1) choose k)) >= (1 * ((n + 1) choose k)) by XREAL_1: 64;

 ((n + 1) choose m1) = (((n + 1) ! ) / ((m1 ! ) * (l1 ! ))) by A13, NEWTON:def 3

 .= (((n + 1) * (n ! )) / (((m + 1) ! ) * (l ! ))) by A11, A30, A31, NEWTON: 15

 .= (((n + 1) * (n ! )) / (((m ! ) * (m + 1)) * (l ! ))) by NEWTON: 15

 .= (((n + 1) * (n ! )) / ((m + 1) * ((m ! ) * (l ! ))))

 .= (((n + 1) / (m + 1)) / (((m ! ) * (l ! )) / (n ! ))) by XCMPLX_1: 84

 .= (((n ! ) / ((m ! ) * (l ! ))) * ((n + 1) / (m + 1))) by XCMPLX_1: 80

 .= ((n choose m) * ((n + 1) / (m + 1))) by A7, NEWTON:def 3;

 then ((n + 1) choose m1) >= (((n + 1) choose k) * ((nk + 1) / (m + 1))) by A23, A33, XREAL_1: 64;

 hence thesis by A34, XXREAL_0: 2;

 end;

 end;

 end;

 hence thesis;

 end;



 A35: P[ 0 ]

 proof

 let k,m be Nat;

 assume

 A36: k <= m;

 assume m = [\( 0 / 2)/];

 then m = 0 by INT_1: 25;

 hence thesis by A36;

 end;



 A37: for n be Nat holds P[n] from NAT_1:sch 2( A35, A2);

 for n,k,m be Nat st k <= n & m = [\(n / 2)/] holds (n choose m) >= (n choose k)

 proof

 let n,k,m be Nat;

 assume

 A38: k <= n;

 assume

 A39: m = [\(n / 2)/];

 per cases ;

 suppose k <= m;

 hence thesis by A37, A39;

 end;

 suppose

 A40: k > m;

 set r = (n -' k);



 A41: (n -' k) = (n - k) by A38, XREAL_1: 233;

 then

 A42: (n choose k) = (n choose r) by A38, NEWTON: 20;

 per cases ;

 suppose

 A43: n is even;

 ( - k) < ( - m) by A40, XREAL_1: 24;

 then

 A44: (( - k) + n) < (( - m) + n) by XREAL_1: 6;

 ex j be Nat st n = (2 * j) by A43, ABIAN:def 2;

 then (n / 2) = [\(n / 2)/] by INT_1: 25;

 hence thesis by A37, A39, A41, A42, A44;

 end;

 suppose not n is even;

 then

 consider j be Integer such that

 A45: n = ((2 * j) + 1) by ABIAN: 1;



 A46: k >= (m + 1) by A40, NAT_1: 13;



 A47: [\(n / 2)/] = [\(j + (1 / 2))/] by A45

 .= (j + [\(1 / 2)/]) by INT_1: 28

 .= (j + 0 ) by A1, INT_1:def 6

 .= j;

 per cases by A46, XXREAL_0: 1;

 suppose

 A48: k = (m + 1);

 set nm1 = (n - (m + 1));

 set nm = (n - m);

 (2 * n) >= (1 * n) by XREAL_1: 64;

 then

 A49: (n / 2) >= [\(n / 2)/] & ((2 * n) / 2) >= (n / 2) by INT_1:def 6, XREAL_1: 72;

 then

 A50: n >= m by A39, XXREAL_0: 2;

 (n - m) = (n -' m) by A39, A49, XREAL_1: 233, XXREAL_0: 2;

 then

 reconsider nm as Element of NAT ;

 (2 * m) >= (1 * m) by XREAL_1: 64;

 then

 A51: n >= (m + 1) by A39, A45, A47, XREAL_1: 6;

 then (n - (m + 1)) = (n -' (m + 1)) by XREAL_1: 233;

 then

 reconsider nm1 as Element of NAT ;



 A52: (n choose (m + 1)) = ((n ! ) / ((nm1 ! ) * ((m + 1) ! ))) by A51, NEWTON:def 3;

 nm = (m + 1) by A39, A45, A47;

 hence thesis by A48, A50, A52, NEWTON:def 3;

 end;

 suppose k > (m + 1);

 then ( - k) < ( - (m + 1)) by XREAL_1: 24;

 then (( - k) + n) < (( - (m + 1)) + n) by XREAL_1: 6;

 hence thesis by A37, A39, A41, A42, A45, A47;

 end;

 end;

 end;

 end;

 hence thesis;

 end;

 theorem :: NAT_4:5



 Th5: for n,m be Nat st m = [\(n / 2)/] & n >= 2 holds (n choose m) >= ((2 |^ n) / n)

 proof

 reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

 set f2a = <*jj*>;

 let n,m be Nat;

 assume

 A1: m = [\(n / 2)/];

 reconsider f1 = ( Newton_Coeff n) as FinSequence of REAL ;

 reconsider nm = (n choose m) as Element of REAL by XREAL_0:def 1;

 set f2b = ((n -' 1) |-> nm);

 reconsider f2 = ((f2a ^ f2b) ^ f2a) as FinSequence of REAL ;



 A2: ( Sum f2b) = ((n -' 1) * (n choose m)) by RVSUM_1: 80;

 assume

 A3: n >= 2;

 then

 A4: (n -' 1) = (n - 1) by XREAL_1: 233, XXREAL_0: 2;



 A5: ( len f2) = (( len (f2a ^ f2b)) + ( len f2a)) by FINSEQ_1: 22

 .= (( len (f2a ^ f2b)) + 1) by FINSEQ_1: 39

 .= ((( len f2a) + ( len f2b)) + 1) by FINSEQ_1: 22

 .= ((( len f2a) + (n - 1)) + 1) by A4, CARD_1:def 7

 .= ((1 + (n - 1)) + 1) by FINSEQ_1: 39

 .= (n + 1);

 ( len f1) = (n + 1) by NEWTON:def 5;

 then ( dom f1) = ( Seg (n + 1)) by FINSEQ_1:def 3;

 then

 A6: ( dom f1) = ( dom f2) by A5, FINSEQ_1:def 3;



 A7: for i be Element of NAT st i in ( dom f1) holds (f1 . i) <= (f2 . i)

 proof

 let i be Element of NAT ;

 assume

 A8: i in ( dom f1);

 per cases by A6, A8, FINSEQ_1: 25;

 suppose

 A9: i in ( dom (f2a ^ f2b));

 then

 A10: (f2 . i) = ((f2a ^ f2b) . i) by FINSEQ_1:def 7;

 per cases by A9, FINSEQ_1: 25;

 suppose

 A11: i in ( dom f2a);

 set k = (1 - 1);

 k = 0 ;

 then

 reconsider k as Element of NAT ;



 A12: (f2 . i) = (f2a . i) by A10, A11, FINSEQ_1:def 7;

 i in ( Seg 1) by A11, FINSEQ_1: 38;

 then

 A13: i = 1 by FINSEQ_1: 2, TARSKI:def 1;



 then (f1 . i) = (n choose k) by A8, NEWTON:def 5

 .= 1 by NEWTON: 19;

 hence thesis by A12, A13, FINSEQ_1: 40;

 end;

 suppose

 A14: ex j be Nat st j in ( dom f2b) & i = (( len f2a) + j);

 set k = (i -' 1);

 consider j be Nat such that

 A15: j in ( dom f2b) and

 A16: i = (( len f2a) + j) by A14;



 A17: j in ( Seg (n -' 1)) by A15, FUNCOP_1: 13;

 (j + 1) >= ( 0 + 1) by XREAL_1: 6;

 then i >= 1 by A16, FINSEQ_1: 39;

 then

 A18: k = (i - 1) by XREAL_1: 233;

 (f2 . i) = (f2b . j) by A10, A15, A16, FINSEQ_1:def 7;

 then

 A19: (f2 . i) = (n choose m) by A17, FUNCOP_1: 7;

 i = (1 + j) by A16, FINSEQ_1: 39;

 then (( - 1) + n) < ( 0 + n) & (i - 1) <= (n - 1) by A4, A17, FINSEQ_1: 1, XREAL_1: 6;

 then

 A20: k <= n by A18, XXREAL_0: 2;

 (f1 . i) = (n choose k) by A8, A18, NEWTON:def 5;

 hence thesis by A1, A19, A20, Th4;

 end;

 end;

 suppose

 A21: ex j be Nat st j in ( dom f2a) & i = (( len (f2a ^ f2b)) + j);

 reconsider k = ((n + 1) - 1) as Element of NAT by ORDINAL1:def 12;

 consider j be Nat such that

 A22: j in ( dom f2a) and

 A23: i = (( len (f2a ^ f2b)) + j) by A21;



 A24: j in ( Seg 1) by A22, FINSEQ_1: 38;

 then

 A25: j = 1 by FINSEQ_1: 2, TARSKI:def 1;

 i = (( len (f2a ^ f2b)) + 1) by A23, A24, FINSEQ_1: 2, TARSKI:def 1

 .= ((( len f2a) + ( len f2b)) + 1) by FINSEQ_1: 22

 .= ((( len f2a) + (n - 1)) + 1) by A4, CARD_1:def 7

 .= ((1 + (n - 1)) + 1) by FINSEQ_1: 39

 .= (n + 1);



 then

 A26: (f1 . i) = (n choose k) by A8, NEWTON:def 5

 .= 1 by NEWTON: 21;

 (f2 . i) = (f2a . j) by A22, A23, FINSEQ_1:def 7;

 hence thesis by A25, A26, FINSEQ_1: 40;

 end;

 end;

 1 <= n by A3, XXREAL_0: 2;

 then

 A27: (n choose 1) <= (n choose m) by A1, Th4;

 2 <= (n choose 1) by A3, NEWTON: 23, XXREAL_0: 2;

 then 2 <= (n choose m) by A27, XXREAL_0: 2;

 then

 A28: (2 + ((n - 1) * (n choose m))) <= ((n choose m) + ((n - 1) * (n choose m))) by XREAL_1: 6;



 A29: ( Sum f2) = (( Sum (f2a ^ f2b)) + 1) by RVSUM_1: 74

 .= ((1 + ( Sum f2b)) + 1) by RVSUM_1: 76

 .= (2 + ((n -' 1) * (n choose m))) by A2

 .= (2 + ((n - 1) * (n choose m))) by A3, XREAL_1: 233, XXREAL_0: 2;

 ( len f1) = ( len f2) by A5, NEWTON:def 5;

 then ( Sum f1) <= ( Sum f2) by A7, INTEGRA5: 3;

 then (2 |^ n) <= (2 + ((n - 1) * (n choose m))) by A29, NEWTON: 32;

 then (2 |^ n) <= (n * (n choose m)) by A28, XXREAL_0: 2;

 then ((2 |^ n) / n) <= ((n * (n choose m)) / n) by XREAL_1: 72;

 hence thesis by A3, XCMPLX_1: 89;

 end;

 theorem :: NAT_4:6



 Th6: for n be Nat holds ((2 * n) choose n) >= ((4 |^ n) / (2 * n))

 proof

 let n be Nat;

 per cases ;

 suppose n = 0 ;

 hence thesis;

 end;

 suppose

 A1: n <> 0 ;

 set m = [\((2 * n) / 2)/];



 A2: (2 |^ 2) = ( Product <*2, 2*>) by FINSEQ_2: 61

 .= (2 * 2) by RVSUM_1: 99

 .= 4;



 A3: m = n by INT_1: 25;

 then

 reconsider m as Element of NAT by ORDINAL1:def 12;

 (2 * n) >= (2 * 1) by A1, NAT_1: 14, XREAL_1: 64;

 then ((2 * n) choose m) >= ((2 |^ (2 * n)) / (2 * n)) by Th5;

 hence thesis by A2, A3, NEWTON: 9;

 end;

 end;

 theorem :: NAT_4:7



 Th7: for n,p be Nat holds p > 0 & n divides p & n <> 1 & n <> p implies 1 < n & n 0 & n divides p;

 assume

 A2: n <> 1;

 assume

 A3: n <> p;

 n <> 0 by A1, INT_2: 3;

 hence 1 < n by A2, NAT_1: 25;

 n <= p by A1, NAT_D: 7;

 hence thesis by A3, XXREAL_0: 1;

 end;

 theorem :: NAT_4:8



 Th8: for p be Nat holds (ex n be Element of NAT st n divides p & 1 < n & n < p) implies ex n be Element of NAT st n divides p & 1 < n & (n * n) <= p

 proof

 let p be Nat;

 given n be Element of NAT such that

 A1: n divides p and

 A2: 1 < n and

 A3: n < p;

 per cases ;

 suppose

 A4: (n * n) <= p;

 take n;

 thus thesis by A1, A2, A4;

 end;

 suppose

 A5: (n * n) > p;

 consider k be Nat such that

 A6: p = (n * k) by A1, NAT_D:def 3;



 A7: (k * k) <= p

 proof

 assume (k * k) > p;

 then ((k * k) * (n * n)) > (p * p) by A5, XREAL_1: 96;

 hence contradiction by A6;

 end;

 take k;

 (n / n) < ((n * k) / n) by A2, A3, A6, XREAL_1: 74;

 then 1 < ((k * n) / n) by A2, XCMPLX_1: 60;

 hence thesis by A2, A6, A7, NAT_D:def 3, ORDINAL1:def 12, XCMPLX_1: 89;

 end;

 end;

 theorem :: NAT_4:9



 Th9: for i,j,k,l be Nat st i = ((j * k) + l) & l < j & 0 < l holds not j divides i

 proof

 let i,j,k,l be Nat;

 assume

 A1: i = ((j * k) + l);

 assume that

 A2: l < j and

 A3: 0 < l;

 assume j divides i;

 then i = (j * (i div j)) by NAT_D: 3;

 then (j * (i div j)) = ((j * (i div j)) + l) by A1, A2, NAT_D:def 1;

 hence contradiction by A3;

 end;

 theorem :: NAT_4:10

 for n,q,b be Nat holds (q gcd b) = 1 & q <> 0 & b <> 0 implies ((q |^ n) gcd b) = 1

 proof

 let n,q,b be Nat;

 assume that

 A1: (q gcd b) = 1 and

 A2: q <> 0 & b <> 0 ;

 (q,b) are_coprime by A1, INT_2:def 3;

 then ((q |^ n),b) are_coprime by A2, EULER_2: 17;

 hence thesis by INT_2:def 3;

 end;

 theorem :: NAT_4:11



 Th11: for a,b,c be Nat holds ((a |^ (2 * b)) mod c) = ((((a |^ b) mod c) * ((a |^ b) mod c)) mod c)

 proof

 let a,b,c be Nat;

 reconsider a, b, c as Element of NAT by ORDINAL1:def 12;

 ((a |^ (2 * b)) mod c) = ((a |^ (b + b)) mod c)

 .= (((a |^ b) * (a |^ b)) mod c) by NEWTON: 8

 .= ((((a |^ b) mod c) * ((a |^ b) mod c)) mod c) by EULER_2: 9;

 hence thesis;

 end;

 theorem :: NAT_4:12



 Th12: for p be Nat holds not p is prime iff p <= 1 or ex n be Element of NAT st n divides p & 1 < n & n < p

 proof

 now

 let p be Nat;

 assume that

 A1: not p is prime and

 A2: not p <= 1;

 consider n be Nat such that

 A3: n divides p and

 A4: n <> 1 & n <> p by A1, A2, INT_2:def 4;

 reconsider n as Element of NAT by ORDINAL1:def 12;

 take n;

 thus n divides p by A3;

 thus 1 < n & n < p by A2, A3, A4, Th7;

 end;

 hence thesis by INT_2:def 4;

 end;

 theorem :: NAT_4:13



 Th13: for n,k be Nat st n divides k & 1 < n holds ex p be Element of NAT st p divides k & p <= n & p is prime

 proof

 let n,k be Nat;

 assume

 A1: n divides k;

 assume

 A2: 1 < n;

 then (1 + 1) < (n + 1) by XREAL_1: 6;

 then 2 <= n by NAT_1: 13;

 then

 consider p be Element of NAT such that

 A3: p is prime and

 A4: p divides n by INT_2: 31;

 take p;

 thus p divides k by A1, A4, NAT_D: 4;

 thus p <= n by A2, A4, NAT_D: 7;

 thus thesis by A3;

 end;



 Lm1: for p be Nat holds not p is prime iff p <= 1 or ex n be Element of NAT st n divides p & 1 < n & (n * n) <= p & n is prime

 proof

 let p be Nat;

 A1:

 now

 assume

 A2: not p is prime;

 assume not p <= 1;

 then ex k be Element of NAT st k divides p & 1 < k & k < p by A2, Th12;

 then

 consider k be Element of NAT such that

 A3: k divides p & 1 < k and

 A4: (k * k) <= p by Th8;

 consider n be Element of NAT such that

 A5: n divides p and

 A6: n <= k and

 A7: n is prime by A3, Th13;

 take n;

 thus n divides p by A5;

 thus 1 < n by A7, Th12;

 (n * n) <= (k * k) by A6, XREAL_1: 66;

 hence (n * n) <= p by A4, XXREAL_0: 2;

 thus n is prime by A7;

 end;

 now

 assume

 A8: p <= 1 or ex n be Element of NAT st n divides p & 1 < n & (n * n) <= p;

 per cases by A8;

 suppose p <= 1;

 hence not p is prime by Th12;

 end;

 suppose ex n be Element of NAT st n divides p & 1 < n & (n * n) <= p;

 then

 consider n be Element of NAT such that

 A9: n divides p and

 A10: 1 < n and

 A11: (n * n) <= p;

 n < p by A10, A11, Th2;

 hence not p is prime by A9, A10, Th12;

 end;

 end;

 hence thesis by A1;

 end;

 theorem :: NAT_4:14



 Th14: for p be Nat holds p is prime iff p > 1 & for n be Element of NAT holds 1 < n & (n * n) <= p & n is prime implies not n divides p

 proof

 now

 let p be Nat;

 assume

 A1: p > 1;

 assume for n be Element of NAT holds not (1 < n & (n * n) <= p & n is prime) or not n divides p;

 then for n be Element of NAT holds not n divides p or not (1 < n & (n * n) <= p & n is prime);

 hence p is prime by A1, Lm1;

 end;

 hence thesis by Lm1;

 end;

 theorem :: NAT_4:15



 Th15: for a,p,k be Nat holds ((a |^ k) mod p) = 1 & k >= 1 & p is prime implies (a,p) are_coprime

 proof

 let a,p,k be Nat;

 assume that

 A1: ((a |^ k) mod p) = 1 and

 A2: k >= 1;

 assume

 A3: p is prime;

 assume

 A4: not (a,p) are_coprime ;

 reconsider a, p, k as Element of NAT by ORDINAL1:def 12;

 (a gcd p) = p by A3, A4, PEPIN: 2;

 then p divides a by NAT_D:def 5;

 then

 consider i be Nat such that

 A5: a = (p * i) by NAT_D:def 3;

 ((((p * i) mod p) |^ k) mod p) = 1 by A1, A5, PEPIN: 12;

 then (( 0 qua Nat |^ k) mod p) = 1 by NAT_D: 13;

 then ((p * 0 ) mod p) = 1 by A2, NEWTON: 11;

 hence contradiction by NAT_D: 13;

 end;

 theorem :: NAT_4:16



 Th16: for p be Prime, a be Element of NAT , x be set st a <> 0 & x = (p |^ (p |-count a)) holds ex b be Element of NAT st b = x & 1 <= b & b <= a

 proof

 let p be Prime, a be Element of NAT , x be set;

 assume

 A1: a <> 0 ;

 assume

 A2: x = (p |^ (p |-count a));

 then

 reconsider b = x as Element of NAT by ORDINAL1:def 12;

 take b;

 thus b = x;

 p >= 1 by INT_2:def 4;

 hence 1 <= b by A2, PREPOWER: 11;

 p <> 1 by INT_2:def 4;

 then b divides a by A1, A2, NAT_3:def 7;

 hence thesis by A1, NAT_D: 7;

 end;

 theorem :: NAT_4:17



 Th17: for k,q,n,d be Element of NAT holds q is prime & d divides (k * (q |^ (n + 1))) & not d divides (k * (q |^ n)) implies (q |^ (n + 1)) divides d

 proof

 defpred P[ Nat] means for k,q,d be Element of NAT holds q is prime & d divides (k * (q |^ ($1 + 1))) & not d divides (k * (q |^ $1)) implies (q |^ ($1 + 1)) divides d;



 A1: for n be Nat holds P[n] implies P[(n + 1)]

 proof

 let n be Nat;

 assume

 A2: for k,q,d be Element of NAT holds q is prime & d divides (k * (q |^ (n + 1))) & not d divides (k * (q |^ n)) implies (q |^ (n + 1)) divides d;

 for k,q,d be Element of NAT holds q is prime & d divides (k * (q |^ ((n + 1) + 1))) & not d divides (k * (q |^ (n + 1))) implies (q |^ ((n + 1) + 1)) divides d

 proof

 let k,q,d be Element of NAT ;

 assume

 A3: q is prime;

 assume

 A4: d divides (k * (q |^ ((n + 1) + 1)));

 then

 consider i be Nat such that

 A5: (k * (q |^ ((n + 1) + 1))) = (d * i) by NAT_D:def 3;

 assume

 A6: not d divides (k * (q |^ (n + 1)));

 then not d divides (k * (q * (q |^ n))) by NEWTON: 6;

 then

 A7: not d divides ((k * q) * (q |^ n));

 d divides (k * (q * (q |^ (n + 1)))) by A4, NEWTON: 6;

 then d divides ((k * q) * (q |^ (n + 1)));

 then (q |^ (n + 1)) divides d by A2, A3, A7;

 then

 consider j be Nat such that

 A8: d = ((q |^ (n + 1)) * j) by NAT_D:def 3;



 A9: not q divides i

 proof

 assume q divides i;

 then

 consider i1 be Nat such that

 A10: i = (q * i1) by NAT_D:def 3;

 (k * ((q |^ (n + 1)) * q)) = (d * (q * i1)) by A5, A10, NEWTON: 6;

 then ((k * (q |^ (n + 1))) * q) = ((d * i1) * q);

 then (k * (q |^ (n + 1))) = (d * i1) by A3, XCMPLX_1: 5;

 hence contradiction by A6, NAT_D:def 3;

 end;

 (k * (q |^ ((n + 1) + 1))) = (k * ((q |^ (n + 1)) * q)) by NEWTON: 6

 .= ((k * q) * (q |^ (n + 1)));

 then ((k * q) * (q |^ (n + 1))) = ((j * i) * (q |^ (n + 1))) by A5, A8;

 then (k * q) = (j * i) by A3, XCMPLX_1: 5;

 then q divides (j * i) by NAT_D:def 3;

 then q divides j by A3, A9, NEWTON: 80;

 then

 consider j1 be Nat such that

 A11: j = (q * j1) by NAT_D:def 3;

 d = (((q |^ (n + 1)) * q) * j1) by A8, A11;

 then d = ((q |^ ((n + 1) + 1)) * j1) by NEWTON: 6;

 hence thesis by NAT_D:def 3;

 end;

 hence thesis;

 end;



 A12: P[ 0 ]

 proof

 let k,q,d be Element of NAT ;

 assume that

 A13: q is prime and

 A14: d divides (k * (q |^ ( 0 + 1))) and

 A15: not d divides (k * (q |^ 0 ));

 d divides (k * q) by A14;

 then

 consider i be Nat such that

 A16: (k * q) = (d * i) by NAT_D:def 3;

 assume not (q |^ ( 0 + 1)) divides d;

 then

 A17: not q divides d;

 q divides (d * i) by A16, NAT_D:def 3;

 then q divides i by A13, A17, NEWTON: 80;

 then

 consider j be Nat such that

 A18: i = (q * j) by NAT_D:def 3;

 ((d * j) * q) = (k * q) by A16, A18;

 then

 A19: (d * j) = k by A13, XCMPLX_1: 5;

 not d divides (k * 1) by A15, NEWTON: 4;

 hence contradiction by A19, NAT_D:def 3;

 end;

 for n be Nat holds P[n] from NAT_1:sch 2( A12, A1);

 hence thesis;

 end;

 theorem :: NAT_4:18



 Th18: for q1,q,n1 be Element of NAT st q1 divides (q |^ n1) & q is prime & q1 is prime holds q = q1

 proof

 let q1,q,n1 be Element of NAT ;

 assume that

 A1: q1 divides (q |^ n1) and

 A2: q is prime;

 assume

 A3: q1 is prime;

 then q1 > 1 by INT_2:def 4;

 then

 consider k be Element of NAT such that

 A4: q1 = (q * k) by A1, A2, PEPIN: 32;



 A5: k <> q1

 proof

 assume k = q1;

 then q = 1 by A3, A4, XCMPLX_1: 7;

 hence contradiction by A2, INT_2:def 4;

 end;

 k divides q1 by A4, NAT_D:def 3;

 then k = 1 or k = q1 by A3, INT_2:def 4;

 hence thesis by A4, A5;

 end;

 theorem :: NAT_4:19



 Th19: for p be Prime, n be Nat st n < p holds not p divides (n ! )

 proof

 defpred P[ Nat] means for p be Prime st $1 < p holds not p divides ($1 ! );

 let p be Prime;

 let n be Nat;

 assume

 A1: n < p;



 A2: for n be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume

 A3: P[n];

 for p be Prime st (n + 1) < p holds not p divides ((n + 1) ! )

 proof

 let p be Prime;

 assume

 A4: (n + 1) < p;

 assume p divides ((n + 1) ! );

 then

 A5: p divides ((n ! ) * (n + 1)) by NEWTON: 15;

 (n + 0 ) < (n + 1) by XREAL_1: 6;

 then n < p by A4, XXREAL_0: 2;

 then not p divides (n ! ) by A3;

 then p divides (n + 1) by A5, NEWTON: 80;

 hence contradiction by A4, NAT_D: 7;

 end;

 hence thesis;

 end;



 A6: P[ 0 ] by NAT_D: 7, NEWTON: 12, INT_2:def 4;

 for n be Nat holds P[n] from NAT_1:sch 2( A6, A2);

 hence thesis by A1;

 end;

 theorem :: NAT_4:20



 Th20: for a,b be non zero Nat holds (for p be Element of NAT st p is prime holds (p |-count a) <= (p |-count b)) implies ex c be Element of NAT st b = (a * c)

 proof



 A1: for a,a1,b,b1 be non zero Nat, x be Prime st (for p be Element of NAT st p is prime holds (p |-count a) <= (p |-count b)) & a1 = (a div (x |^ (x |-count a))) & b1 = (b div (x |^ (x |-count b))) holds for p be Element of NAT st p is prime holds (p |-count a1) <= (p |-count b1)

 proof

 let a,a1,b,b1 be non zero Nat;

 let x be Prime;

 assume

 A2: for p be Element of NAT st p is prime holds (p |-count a) <= (p |-count b);

 set xcb = (x |-count b);

 set xca = (x |-count a);

 assume

 A3: a1 = (a div (x |^ (x |-count a)));

 assume

 A4: b1 = (b div (x |^ (x |-count b)));

 let p be Element of NAT ;

 assume

 A5: p is prime;

 then

 A6: p > 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 be non zero Nat, x be 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 be 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 be non zero Nat st ( card ( support ( pfexp b))) = $1 holds (for p be Element of NAT st p is prime holds (p |-count a) <= (p |-count b)) implies (ex c be Element of NAT st b = (a * c));

 let a,b be non zero Nat;

 assume

 A15: for p be Element of NAT st p is prime holds (p |-count a) <= (p |-count b);



 A16: ex n1 be Element of NAT st n1 = ( card ( support ( pfexp b)));



 A17: for n1,n2 be 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 be Nat st n2 = (n1 * a) by NAT_D:def 3;

 hence thesis by NAT_D: 18;

 end;



 A18: for b,b1 be non zero Nat, x be Prime, n be 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 be Nat holds P[n] implies P[(n + 1)]

 proof

 let n be Nat;

 assume

 A28: P[n];

 for a,b be non zero Nat st ( card ( support ( pfexp b))) = (n + 1) holds (for p be Element of NAT st p is prime holds (p |-count a) <= (p |-count b)) implies ex c be 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 be 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 be Element of NAT st p is prime holds (p |-count a) <= (p |-count b);

 then

 A32: for p be 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 be Element of NAT st p is prime holds (p |-count a) <= (p |-count b)) implies ex c be Element of NAT st b = (a * c)

 proof

 set d = 1;

 assume

 A39: for p be 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 be Nat holds P[n] from NAT_1:sch 2( A37, A27);

 hence thesis by A15, A16;

 end;

 theorem :: NAT_4:21



 Th21: for a,b be non zero Nat holds (for p be 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 be Element of NAT st p is prime holds (p |-count a) = (p |-count b);

 then for p be Element of NAT st p is prime holds (p |-count a) <= (p |-count b);

 then

 consider c be Element of NAT such that

 A2: b = (a * c) by Th20;

 for p be Element of NAT st p is prime holds (p |-count b) <= (p |-count a) by A1;

 then

 consider d be 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 :: NAT_4:22



 Th22: for p1,p2 be Prime, m be 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

 theorem :: NAT_4:23



 Th23: for n,k,q,p,n1,p,a be 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 be 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) < (nn + 1) by A5, XREAL_1: 233;

 then

 A19: 1 <= nn by NAT_1: 13;

 then

 A20: (a,p) are_coprime by A11, A18, Th15;



 A21: ( order (a,p)) divides (p -' 1) by A11, A18, A19, Th15, PEPIN: 49;

 (n -' 1) = (n - 1) by A5, XREAL_1: 233;

 then ( order (a,p)) divides (k * (q |^ ((n1 -' 1) + 1))) by A1, A16, A15, A18, A20, PEPIN: 47;

 then (q |^ n1) divides ( order (a,p)) by A4, A16, A20, A14, A9, A10, Th17, PEPIN: 48;

 then (q |^ n1) divides (p -' 1) by A21, NAT_D: 4;

 then

 A22: ((p -' 1) mod (q |^ n1)) = 0 by A4, PEPIN: 6;

 q > 1 by A4, INT_2:def 4;

 hence thesis by A3, A17, A22, NAT_D: 16, PEPIN: 25;

 end;

 theorem :: NAT_4:24



 Th24: for n,f,c be Element of NAT st (n - 1) = (f * c) & f > c & c > 0 & (for q be Element of NAT st q divides f & q is prime holds ex a be 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 be Element of NAT st q divides f & q is prime holds ex a be 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 be 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 be 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 be 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;

 ::$Notion-Name

 theorem :: NAT_4:25



 Th25: for n,f,d,n1,a,q be 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 be Element of NAT st q1 divides f & q1 is prime holds ex a be 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 be Element of NAT st 1 < n & n < 5 & n is prime holds n = 2 or n = 3

 proof

 let n be Element of NAT ;

 assume that

 A1: 1 < n & n < 5 and

 A2: n is prime;

 (1 + 1) < (n + 1) & n < (4 + 1) by A1, XREAL_1: 6;

 then 2 <= n & n <= (2 + 1) or 3 <= n & n <= (3 + 1) by NAT_1: 13;

 hence thesis by A2, INT_2: 29, NAT_1: 9;

 end;



 Lm3: for k be Element of NAT st k < 25 holds for n be Element of NAT st 1 < n & (n * n) <= k & n is prime holds n = 2 or n = 3

 proof

 let k be Element of NAT ;

 assume

 A1: k < 25;

 let n be Element of NAT ;

 assume that

 A2: 1 < n and

 A3: (n * n) <= k and

 A4: n is prime;

 (n * n) < (5 * 5) by A1, A3, XXREAL_0: 2;

 then n < 5 by Th1;

 hence thesis by A2, A4, Lm2;

 end;

 begin

 theorem :: NAT_4:26



 Th26: 7 is prime

 proof

 now

 let n be Element of NAT ;

 7 = ((2 * 3) + 1);

 then

 A1: not 2 divides 7 by Th9;

 7 = ((3 * 2) + 1);

 then

 A2: not 3 divides 7 by Th9;

 assume 1 < n & (n * n) <= 7 & n is prime;

 hence not n divides 7 by A1, A2, Lm3;

 end;

 hence thesis by Th14;

 end;

 theorem :: NAT_4:27

 11 is prime

 proof

 now

 let n be Element of NAT ;

 11 = ((2 * 5) + 1);

 then

 A1: not 2 divides 11 by Th9;

 11 = ((3 * 3) + 2);

 then

 A2: not 3 divides 11 by Th9;

 assume 1 < n & (n * n) <= 11 & n is prime;

 hence not n divides 11 by A1, A2, Lm3;

 end;

 hence thesis by Th14;

 end;

 theorem :: NAT_4:28



 Th28: 13 is prime

 proof

 now

 let n be Element of NAT ;

 13 = ((2 * 6) + 1);

 then

 A1: not 2 divides 13 by Th9;

 13 = ((3 * 4) + 1);

 then

 A2: not 3 divides 13 by Th9;

 assume 1 < n & (n * n) <= 13 & n is prime;

 hence not n divides 13 by A1, A2, Lm3;

 end;

 hence thesis by Th14;

 end;



 Lm4: not 6 is prime & not 8 is prime & not 9 is prime & not 10 is prime & not 12 is prime & not 14 is prime & not 15 is prime & not 16 is prime & not 18 is prime & not 20 is prime & not 21 is prime & not 22 is prime & not 24 is prime & not 25 is prime & not 26 is prime & not 27 is prime & not 28 is prime

 proof

 6 = (2 * 3);

 then 2 divides 6 by NAT_D:def 3;

 hence not 6 is prime by INT_2:def 4;

 8 = (2 * 4);

 then 2 divides 8 by NAT_D:def 3;

 hence not 8 is prime by INT_2:def 4;

 9 = (3 * 3);

 then 3 divides 9 by NAT_D:def 3;

 hence not 9 is prime by INT_2:def 4;

 10 = (2 * 5);

 then 2 divides 10 by NAT_D:def 3;

 hence not 10 is prime by INT_2:def 4;

 12 = (2 * 6);

 then 2 divides 12 by NAT_D:def 3;

 hence not 12 is prime by INT_2:def 4;

 14 = (2 * 7);

 then 2 divides 14 by NAT_D:def 3;

 hence not 14 is prime by INT_2:def 4;

 15 = (3 * 5);

 then 3 divides 15 by NAT_D:def 3;

 hence not 15 is prime by INT_2:def 4;

 16 = (4 * 4);

 then 4 divides 16 by NAT_D:def 3;

 hence not 16 is prime by INT_2:def 4;

 18 = (2 * 9);

 then 2 divides 18 by NAT_D:def 3;

 hence not 18 is prime by INT_2:def 4;

 20 = (4 * 5);

 then 4 divides 20 by NAT_D:def 3;

 hence not 20 is prime by INT_2:def 4;

 21 = (3 * 7);

 then 3 divides 21 by NAT_D:def 3;

 hence not 21 is prime by INT_2:def 4;

 22 = (2 * 11);

 then 2 divides 22 by NAT_D:def 3;

 hence not 22 is prime by INT_2:def 4;

 24 = (4 * 6);

 then 4 divides 24 by NAT_D:def 3;

 hence not 24 is prime by INT_2:def 4;

 25 = (5 * 5);

 then 5 divides 25 by NAT_D:def 3;

 hence not 25 is prime by INT_2:def 4;

 26 = (2 * 13);

 then 2 divides 26 by NAT_D:def 3;

 hence not 26 is prime by INT_2:def 4;

 27 = (3 * 9);

 then 3 divides 27 by NAT_D:def 3;

 hence not 27 is prime by INT_2:def 4;

 28 = (4 * 7);

 then 4 divides 28 by NAT_D:def 3;

 hence thesis by INT_2:def 4;

 end;

 theorem :: NAT_4:29

 19 is prime

 proof

 now

 let n be Element of NAT ;

 19 = ((2 * 9) + 1);

 then

 A1: not 2 divides 19 by Th9;

 19 = ((3 * 6) + 1);

 then

 A2: not 3 divides 19 by Th9;

 assume 1 < n & (n * n) <= 19 & n is prime;

 hence not n divides 19 by A1, A2, Lm3;

 end;

 hence thesis by Th14;

 end;

 theorem :: NAT_4:30



 Th30: 23 is prime

 proof

 now

 let n be Element of NAT ;

 23 = ((2 * 11) + 1);

 then

 A1: not 2 divides 23 by Th9;

 23 = ((3 * 7) + 2);

 then

 A2: not 3 divides 23 by Th9;

 assume 1 < n & (n * n) <= 23 & n is prime;

 hence not n divides 23 by A1, A2, Lm3;

 end;

 hence thesis by Th14;

 end;



 Lm5: for n be Element of NAT st 1 < n & n < 29 & n is prime holds n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or n = 23

 proof

 let n be Element of NAT ;

 assume that

 A1: 1 < n and

 A2: n < 29 and

 A3: n is prime;



 A4: (1 + 1) < (n + 1) & n < (28 + 1) by A1, A2, XREAL_1: 6;

 per cases by A4, NAT_1: 13;

 suppose 2 <= n & n < 5;

 hence thesis by A1, A3, Lm2;

 end;

 suppose

 A5: 5 <= n & n <= (27 + 1);

 per cases by A5;

 suppose 5 <= n & n <= (12 + 1);

 then 5 <= n & n <= (5 + 1) or 6 <= n & n <= (6 + 1) or 7 <= n & n <= (7 + 1) or 8 <= n & n <= (8 + 1) or 9 <= n & n <= (9 + 1) or 10 <= n & n <= (10 + 1) or 11 <= n & n <= (11 + 1) or 12 <= n & n <= (12 + 1);

 hence thesis by A3, Lm4, NAT_1: 9;

 end;

 suppose 13 <= n & n <= (20 + 1);

 then 13 <= n & n <= (13 + 1) or 14 <= n & n <= (14 + 1) or 15 <= n & n <= (15 + 1) or 16 <= n & n <= (16 + 1) or 17 <= n & n <= (17 + 1) or 18 <= n & n <= (18 + 1) or 19 <= n & n <= (19 + 1) or 20 <= n & n <= (20 + 1);

 hence thesis by A3, Lm4, NAT_1: 9;

 end;

 suppose 21 <= n & n <= (27 + 1);

 then 21 <= n & n <= (21 + 1) or 22 <= n & n <= (22 + 1) or 23 <= n & n <= (23 + 1) or 24 <= n & n <= (24 + 1) or 25 <= n & n <= (25 + 1) or 26 <= n & n <= (26 + 1) or 27 <= n & n <= (27 + 1);

 hence thesis by A3, Lm4, NAT_1: 9;

 end;

 end;

 end;



 Lm6: for k be Element of NAT st k < 841 holds for n be Element of NAT st 1 < n & (n * n) <= k & n is prime holds n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or n = 23

 proof

 let k be Element of NAT ;

 assume

 A1: k < 841;

 let n be Element of NAT ;

 assume that

 A2: 1 < n and

 A3: (n * n) <= k and

 A4: n is prime;

 (n * n) < (29 * 29) by A1, A3, XXREAL_0: 2;

 then n < 29 by Th1;

 hence thesis by A2, A4, Lm5;

 end;

 theorem :: NAT_4:31



 Th31: 37 is prime

 proof

 now

 let n be Element of NAT ;

 37 = ((2 * 18) + 1);

 then

 A1: not 2 divides 37 by Th9;

 37 = ((3 * 12) + 1);

 then

 A2: not 3 divides 37 by Th9;

 37 = ((13 * 2) + 11);

 then

 A3: not 13 divides 37 by Th9;

 37 = ((11 * 3) + 4);

 then

 A4: not 11 divides 37 by Th9;

 37 = ((19 * 1) + 18);

 then

 A5: not 19 divides 37 by Th9;

 37 = ((17 * 2) + 3);

 then

 A6: not 17 divides 37 by Th9;

 37 = ((23 * 1) + 14);

 then

 A7: not 23 divides 37 by Th9;

 37 = ((7 * 5) + 2);

 then

 A8: not 7 divides 37 by Th9;

 37 = ((5 * 7) + 2);

 then

 A9: not 5 divides 37 by Th9;

 assume 1 < n & (n * n) <= 37 & n is prime;

 hence not n divides 37 by A1, A2, A9, A8, A4, A3, A6, A5, A7, Lm6;

 end;

 hence thesis by Th14;

 end;

 theorem :: NAT_4:32



 Th32: 43 is prime

 proof

 now

 let n be Element of NAT ;

 43 = ((2 * 21) + 1);

 then

 A1: not 2 divides 43 by Th9;

 43 = ((3 * 14) + 1);

 then

 A2: not 3 divides 43 by Th9;

 43 = ((13 * 3) + 4);

 then

 A3: not 13 divides 43 by Th9;

 43 = ((11 * 3) + 10);

 then

 A4: not 11 divides 43 by Th9;

 43 = ((19 * 2) + 5);

 then

 A5: not 19 divides 43 by Th9;

 43 = ((17 * 2) + 9);

 then

 A6: not 17 divides 43 by Th9;

 43 = ((23 * 1) + 20);

 then

 A7: not 23 divides 43 by Th9;

 43 = ((7 * 6) + 1);

 then

 A8: not 7 divides 43 by Th9;

 43 = ((5 * 8) + 3);

 then

 A9: not 5 divides 43 by Th9;

 assume 1 < n & (n * n) <= 43 & n is prime;

 hence not n divides 43 by A1, A2, A9, A8, A4, A3, A6, A5, A7, Lm6;

 end;

 hence thesis by Th14;

 end;

 theorem :: NAT_4:33



 Th33: 83 is prime

 proof

 now

 let n be Element of NAT ;

 83 = ((2 * 41) + 1);

 then

 A1: not 2 divides 83 by Th9;

 83 = ((3 * 27) + 2);

 then

 A2: not 3 divides 83 by Th9;

 83 = ((13 * 6) + 5);

 then

 A3: not 13 divides 83 by Th9;

 83 = ((11 * 7) + 6);

 then

 A4: not 11 divides 83 by Th9;

 83 = ((19 * 4) + 7);

 then

 A5: not 19 divides 83 by Th9;

 83 = ((17 * 4) + 15);

 then

 A6: not 17 divides 83 by Th9;

 83 = ((23 * 3) + 14);

 then

 A7: not 23 divides 83 by Th9;

 83 = ((7 * 11) + 6);

 then

 A8: not 7 divides 83 by Th9;

 83 = ((5 * 16) + 3);

 then

 A9: not 5 divides 83 by Th9;

 assume 1 < n & (n * n) <= 83 & n is prime;

 hence not n divides 83 by A1, A2, A9, A8, A4, A3, A6, A5, A7, Lm6;

 end;

 hence thesis by Th14;

 end;

 theorem :: NAT_4:34



 Th34: 139 is prime

 proof

 now

 let n be Element of NAT ;

 139 = ((2 * 69) + 1);

 then

 A1: not 2 divides 139 by Th9;

 139 = ((3 * 46) + 1);

 then

 A2: not 3 divides 139 by Th9;

 139 = ((13 * 10) + 9);

 then

 A3: not 13 divides 139 by Th9;

 139 = ((11 * 12) + 7);

 then

 A4: not 11 divides 139 by Th9;

 139 = ((19 * 7) + 6);

 then

 A5: not 19 divides 139 by Th9;

 139 = ((17 * 8) + 3);

 then

 A6: not 17 divides 139 by Th9;

 139 = ((23 * 6) + 1);

 then

 A7: not 23 divides 139 by Th9;

 139 = ((7 * 19) + 6);

 then

 A8: not 7 divides 139 by Th9;

 139 = ((5 * 27) + 4);

 then

 A9: not 5 divides 139 by Th9;

 assume 1 < n & (n * n) <= 139 & n is prime;

 hence not n divides 139 by A1, A2, A9, A8, A4, A3, A6, A5, A7, Lm6;

 end;

 hence thesis by Th14;

 end;

 theorem :: NAT_4:35



 Th35: 163 is prime

 proof

 now

 let n be Element of NAT ;

 163 = ((2 * 81) + 1);

 then

 A1: not 2 divides 163 by Th9;

 163 = ((3 * 54) + 1);

 then

 A2: not 3 divides 163 by Th9;

 163 = ((13 * 12) + 7);

 then

 A3: not 13 divides 163 by Th9;

 163 = ((11 * 14) + 9);

 then

 A4: not 11 divides 163 by Th9;

 163 = ((19 * 8) + 11);

 then

 A5: not 19 divides 163 by Th9;

 163 = ((17 * 9) + 10);

 then

 A6: not 17 divides 163 by Th9;

 163 = ((23 * 7) + 2);

 then

 A7: not 23 divides 163 by Th9;

 163 = ((7 * 23) + 2);

 then

 A8: not 7 divides 163 by Th9;

 163 = ((5 * 32) + 3);

 then

 A9: not 5 divides 163 by Th9;

 assume 1 < n & (n * n) <= 163 & n is prime;

 hence not n divides 163 by A1, A2, A9, A8, A4, A3, A6, A5, A7, Lm6;

 end;

 hence thesis by Th14;

 end;

 theorem :: NAT_4:36



 Th36: 317 is prime

 proof

 now

 let n be Element of NAT ;

 317 = ((2 * 158) + 1);

 then

 A1: not 2 divides 317 by Th9;

 317 = ((3 * 105) + 2);

 then

 A2: not 3 divides 317 by Th9;

 317 = ((13 * 24) + 5);

 then

 A3: not 13 divides 317 by Th9;

 317 = ((11 * 28) + 9);

 then

 A4: not 11 divides 317 by Th9;

 317 = ((19 * 16) + 13);

 then

 A5: not 19 divides 317 by Th9;

 317 = ((17 * 18) + 11);

 then

 A6: not 17 divides 317 by Th9;

 317 = ((23 * 13) + 18);

 then

 A7: not 23 divides 317 by Th9;

 317 = ((7 * 45) + 2);

 then

 A8: not 7 divides 317 by Th9;

 317 = ((5 * 63) + 2);

 then

 A9: not 5 divides 317 by Th9;

 assume 1 < n & (n * n) <= 317 & n is prime;

 hence not n divides 317 by A1, A2, A9, A8, A4, A3, A6, A5, A7, Lm6;

 end;

 hence thesis by Th14;

 end;

 theorem :: NAT_4:37



 Th37: 631 is prime

 proof

 now

 let n be Element of NAT ;

 631 = ((2 * 315) + 1);

 then

 A1: not 2 divides 631 by Th9;

 631 = ((3 * 210) + 1);

 then

 A2: not 3 divides 631 by Th9;

 631 = ((13 * 48) + 7);

 then

 A3: not 13 divides 631 by Th9;

 631 = ((11 * 57) + 4);

 then

 A4: not 11 divides 631 by Th9;

 631 = ((19 * 33) + 4);

 then

 A5: not 19 divides 631 by Th9;

 631 = ((17 * 37) + 2);

 then

 A6: not 17 divides 631 by Th9;

 631 = ((23 * 27) + 10);

 then

 A7: not 23 divides 631 by Th9;

 631 = ((7 * 90) + 1);

 then

 A8: not 7 divides 631 by Th9;

 631 = ((5 * 126) + 1);

 then

 A9: not 5 divides 631 by Th9;

 assume 1 < n & (n * n) <= 631 & n is prime;

 hence not n divides 631 by A1, A2, A9, A8, A4, A3, A6, A5, A7, Lm6;

 end;

 hence thesis by Th14;

 end;

 theorem :: NAT_4:38



 Th38: 1259 is prime

 proof

 (1038 * 1038) = ((1259 * 855) + 999);

 then

 A1: ((1038 * 1038) mod 1259) = 999 by NAT_D:def 2;



 A2: (999 * 744) = ((1259 * 590) + 446);

 (847 * 847) = ((1259 * 569) + 1038);

 then

 A3: ((847 * 847) mod 1259) = 1038 by NAT_D:def 2;



 A4: (1038 * 1136) = ((1259 * 936) + 744);

 (999 * 999) = ((1259 * 792) + 873);

 then

 A5: ((999 * 999) mod 1259) = 873 by NAT_D:def 2;



 A6: (765 * 446) = ((1259 * 271) + 1);



 A7: 2128 = ((1259 * 1) + 869);



 A8: (847 * 4) = ((1259 * 2) + 870);

 (434 * 434) = ((1259 * 149) + 765);

 then

 A9: ((434 * 434) mod 1259) = 765 by NAT_D:def 2;



 A10: ((2 |^ 34) -' 1) = ((2 |^ 34) - 1) by PREPOWER: 11, XREAL_1: 233;

 (873 * 873) = ((1259 * 605) + 434);

 then

 A11: ((873 * 873) mod 1259) = 434 by NAT_D:def 2;



 A12: (1259 -' 1) = (1259 - 1) by XREAL_1: 233

 .= 1258;

 (68 * 68) = ((1259 * 3) + 847);

 then

 A13: ((68 * 68) mod 1259) = 847 by NAT_D:def 2;



 A14: (847 * 1024) = ((1259 * 688) + 1136);

 (256 * 256) = ((1259 * 52) + 68);

 then

 A15: ((256 * 256) mod 1259) = 68 by NAT_D:def 2;



 A16: (1259 - 1) = (37 * 34) & 37 = (37 |^ 1);



 A17: ((2 |^ 1) mod 1259) = 2 by NAT_D: 24;



 A18: ((2 |^ 2) mod 1259) = ((2 |^ (2 * 1)) mod 1259)

 .= ((2 * 2) mod 1259) by A17, Th11

 .= 4 by NAT_D: 24;



 A19: ((2 |^ 4) mod 1259) = ((2 |^ (2 * 2)) mod 1259)

 .= ((4 * 4) mod 1259) by A18, Th11

 .= 16 by NAT_D: 24;



 A20: ((2 |^ 8) mod 1259) = ((2 |^ (2 * 4)) mod 1259)

 .= ((16 * 16) mod 1259) by A19, Th11

 .= 256 by NAT_D: 24;



 A21: ((2 |^ 16) mod 1259) = ((2 |^ (2 * 8)) mod 1259)

 .= 68 by A20, A15, Th11;



 A22: ((2 |^ 32) mod 1259) = ((2 |^ (2 * 16)) mod 1259)

 .= 847 by A21, A13, Th11;



 A23: ((2 |^ 34) mod 1259) = ((2 |^ (32 + 2)) mod 1259)

 .= (((2 |^ 32) * (2 |^ 2)) mod 1259) by NEWTON: 8

 .= ((847 * 4) mod 1259) by A18, A22, EULER_2: 9

 .= 870 by A8, NAT_D:def 2;



 A24: ((2 |^ 64) mod 1259) = ((2 |^ (2 * 32)) mod 1259)

 .= 1038 by A22, A3, Th11;

 1258 = ((37 * 34) + 0 );



 then

 A25: (((2 |^ ((1259 -' 1) div 37)) -' 1) gcd 1259) = (((2 |^ 34) -' 1) gcd 1259) by A12, NAT_D:def 1

 .= ((((2 |^ 34) -' 1) + (1259 * 1)) gcd 1259) by EULER_1: 8

 .= (1259 gcd (((2 |^ 34) + 1258) mod 1259)) by A10, NAT_D: 28

 .= (1259 gcd ((870 + (1258 mod 1259)) mod 1259)) by A23, EULER_2: 6

 .= (1259 gcd ((870 + 1258) mod 1259)) by NAT_D: 24

 .= (((869 * 1) + 390) gcd 869) by A7, NAT_D:def 2

 .= (390 gcd ((390 * 2) + 89)) by EULER_1: 8

 .= (((89 * 4) + 34) gcd 89) by EULER_1: 8

 .= (34 gcd ((34 * 2) + 21)) by EULER_1: 8

 .= (((21 * 1) + 13) gcd 21) by EULER_1: 8

 .= (13 gcd ((13 * 1) + 8)) by EULER_1: 8

 .= (((8 * 1) + 5) gcd 8) by EULER_1: 8

 .= (5 gcd ((5 * 1) + 3)) by EULER_1: 8

 .= (((3 * 1) + 2) gcd 3) by EULER_1: 8

 .= (2 gcd ((2 * 1) + 1)) by EULER_1: 8

 .= (2 gcd 1) by EULER_1: 8

 .= 1 by NEWTON: 51;



 A26: ((2 |^ 128) mod 1259) = ((2 |^ (2 * 64)) mod 1259)

 .= 999 by A24, A1, Th11;



 A27: ((2 |^ 256) mod 1259) = ((2 |^ (2 * 128)) mod 1259)

 .= 873 by A26, A5, Th11;



 A28: ((2 |^ 512) mod 1259) = ((2 |^ (2 * 256)) mod 1259)

 .= 434 by A27, A11, Th11;



 A29: ((2 |^ 1024) mod 1259) = ((2 |^ (2 * 512)) mod 1259)

 .= 765 by A28, A9, Th11;

 ((2 |^ (1259 -' 1)) mod 1259) = ((2 |^ (1024 + 234)) mod 1259) by A12

 .= (((2 |^ 1024) * (2 |^ 234)) mod 1259) by NEWTON: 8

 .= ((((2 |^ 1024) mod 1259) * ((2 |^ (128 + 106)) mod 1259)) mod 1259) by EULER_2: 9

 .= ((765 * (((2 |^ 128) * (2 |^ 106)) mod 1259)) mod 1259) by A29, NEWTON: 8

 .= ((765 * ((999 * ((2 |^ (64 + 42)) mod 1259)) mod 1259)) mod 1259) by A26, EULER_2: 9

 .= ((765 * ((999 * (((2 |^ 64) * (2 |^ 42)) mod 1259)) mod 1259)) mod 1259) by NEWTON: 8

 .= ((765 * ((999 * ((1038 * ((2 |^ (32 + 10)) mod 1259)) mod 1259)) mod 1259)) mod 1259) by A24, EULER_2: 9

 .= ((765 * ((999 * ((1038 * (((2 |^ 32) * (2 |^ 10)) mod 1259)) mod 1259)) mod 1259)) mod 1259) by NEWTON: 8

 .= ((765 * ((999 * ((1038 * ((847 * ((2 |^ (8 + 2)) mod 1259)) mod 1259)) mod 1259)) mod 1259)) mod 1259) by A22, EULER_2: 9

 .= ((765 * ((999 * ((1038 * ((847 * (((2 |^ 8) * (2 |^ 2)) mod 1259)) mod 1259)) mod 1259)) mod 1259)) mod 1259) by NEWTON: 8

 .= ((765 * ((999 * ((1038 * ((847 * ((256 * 4) mod 1259)) mod 1259)) mod 1259)) mod 1259)) mod 1259) by A18, A20, EULER_2: 9

 .= ((765 * ((999 * ((1038 * ((847 * 1024) mod 1259)) mod 1259)) mod 1259)) mod 1259) by NAT_D: 24

 .= ((765 * ((999 * ((1038 * 1136) mod 1259)) mod 1259)) mod 1259) by A14, NAT_D:def 2

 .= ((765 * ((999 * 744) mod 1259)) mod 1259) by A4, NAT_D:def 2

 .= ((765 * 446) mod 1259) by A2, NAT_D:def 2

 .= 1 by A6, NAT_D:def 2;

 hence thesis by A16, A25, Th25, Th31;

 end;

 theorem :: NAT_4:39



 Th39: 2503 is prime

 proof

 (733 * 733) = ((2503 * 214) + 1647);

 then

 A1: ((733 * 733) mod 2503) = 1647 by NAT_D:def 2;



 A2: 4334 = ((2503 * 1) + 1831);

 (458 * 458) = ((2503 * 83) + 2015);

 then

 A3: ((458 * 458) mod 2503) = 2015 by NAT_D:def 2;



 A4: (359 * 64) = ((2503 * 9) + 449);

 (359 * 359) = ((2503 * 51) + 1228);

 then

 A5: ((359 * 359) mod 2503) = 1228 by NAT_D:def 2;



 A6: (1178 * 712) = ((2503 * 335) + 231);

 (2015 * 2015) = ((2503 * 1622) + 359);

 then

 A7: ((2015 * 2015) mod 2503) = 359 by NAT_D:def 2;



 A8: (1228 * 449) = ((2503 * 220) + 712);

 (1228 * 1228) = ((2503 * 602) + 1178);

 then

 A9: ((1228 * 1228) mod 2503) = 1178 by NAT_D:def 2;



 A10: (1647 * 231) = ((2503 * 152) + 1);

 (1178 * 1178) = ((2503 * 554) + 1022);

 then

 A11: ((1178 * 1178) mod 2503) = 1022 by NAT_D:def 2;



 A12: (2503 -' 1) = (2503 - 1) by XREAL_1: 233

 .= 2502;

 (1022 * 1022) = ((2503 * 417) + 733);

 then

 A13: ((1022 * 1022) mod 2503) = 733 by NAT_D:def 2;



 A14: ((2 |^ 18) -' 1) = ((2 |^ 18) - 1) by PREPOWER: 11, XREAL_1: 233;

 (256 * 256) = ((2503 * 26) + 458);

 then

 A15: ((256 * 256) mod 2503) = 458 by NAT_D:def 2;



 A16: (2503 - 1) = (139 * 18) & 139 = (139 |^ 1);



 A17: ((2 |^ 1) mod 2503) = 2 by NAT_D: 24;



 A18: ((2 |^ 2) mod 2503) = ((2 |^ (2 * 1)) mod 2503)

 .= ((2 * 2) mod 2503) by A17, Th11

 .= 4 by NAT_D: 24;



 A19: ((2 |^ 4) mod 2503) = ((2 |^ (2 * 2)) mod 2503)

 .= ((4 * 4) mod 2503) by A18, Th11

 .= 16 by NAT_D: 24;



 A20: ((2 |^ 8) mod 2503) = ((2 |^ (2 * 4)) mod 2503)

 .= ((16 * 16) mod 2503) by A19, Th11

 .= 256 by NAT_D: 24;



 A21: ((2 |^ 16) mod 2503) = ((2 |^ (2 * 8)) mod 2503)

 .= 458 by A20, A15, Th11;



 A22: ((2 |^ 32) mod 2503) = ((2 |^ (2 * 16)) mod 2503)

 .= 2015 by A21, A3, Th11;



 A23: ((2 |^ 64) mod 2503) = ((2 |^ (2 * 32)) mod 2503)

 .= 359 by A22, A7, Th11;



 A24: ((2 |^ 18) mod 2503) = ((2 |^ (16 + 2)) mod 2503)

 .= (((2 |^ 16) * (2 |^ 2)) mod 2503) by NEWTON: 8

 .= ((458 * 4) mod 2503) by A18, A21, EULER_2: 9

 .= 1832 by NAT_D: 24;



 A25: ((2 |^ 128) mod 2503) = ((2 |^ (2 * 64)) mod 2503)

 .= 1228 by A23, A5, Th11;



 A26: ((2 |^ 256) mod 2503) = ((2 |^ (2 * 128)) mod 2503)

 .= 1178 by A25, A9, Th11;

 2502 = ((139 * 18) + 0 );



 then

 A27: (((2 |^ ((2503 -' 1) div 139)) -' 1) gcd 2503) = (((2 |^ 18) -' 1) gcd 2503) by A12, NAT_D:def 1

 .= ((((2 |^ 18) -' 1) + (2503 * 1)) gcd 2503) by EULER_1: 8

 .= (2503 gcd (((2 |^ 18) + 2502) mod 2503)) by A14, NAT_D: 28

 .= (2503 gcd ((1832 + (2502 mod 2503)) mod 2503)) by A24, EULER_2: 6

 .= (2503 gcd ((1832 + 2502) mod 2503)) by NAT_D: 24

 .= (((1831 * 1) + 672) gcd 1831) by A2, NAT_D:def 2

 .= (672 gcd ((672 * 2) + 487)) by EULER_1: 8

 .= (((487 * 1) + 185) gcd 487) by EULER_1: 8

 .= (185 gcd ((185 * 2) + 117)) by EULER_1: 8

 .= (((117 * 1) + 68) gcd 117) by EULER_1: 8

 .= (68 gcd ((68 * 1) + 49)) by EULER_1: 8

 .= (((49 * 1) + 19) gcd 49) by EULER_1: 8

 .= (19 gcd ((19 * 2) + 11)) by EULER_1: 8

 .= (((11 * 1) + 8) gcd 11) by EULER_1: 8

 .= (8 gcd ((8 * 1) + 3)) by EULER_1: 8

 .= (((3 * 2) + 2) gcd 3) by EULER_1: 8

 .= (2 gcd ((2 * 1) + 1)) by EULER_1: 8

 .= (2 gcd 1) by EULER_1: 8

 .= 1 by NEWTON: 51;



 A28: ((2 |^ 512) mod 2503) = ((2 |^ (2 * 256)) mod 2503)

 .= 1022 by A26, A11, Th11;



 A29: ((2 |^ 1024) mod 2503) = ((2 |^ (2 * 512)) mod 2503)

 .= 733 by A28, A13, Th11;



 A30: ((2 |^ 2048) mod 2503) = ((2 |^ (2 * 1024)) mod 2503)

 .= 1647 by A29, A1, Th11;

 ((2 |^ (2503 -' 1)) mod 2503) = ((2 |^ (2048 + 454)) mod 2503) by A12

 .= (((2 |^ 2048) * (2 |^ 454)) mod 2503) by NEWTON: 8

 .= ((((2 |^ 2048) mod 2503) * ((2 |^ (256 + 198)) mod 2503)) mod 2503) by EULER_2: 9

 .= ((1647 * (((2 |^ 256) * (2 |^ 198)) mod 2503)) mod 2503) by A30, NEWTON: 8

 .= ((1647 * ((1178 * ((2 |^ (128 + 70)) mod 2503)) mod 2503)) mod 2503) by A26, EULER_2: 9

 .= ((1647 * ((1178 * (((2 |^ 128) * (2 |^ 70)) mod 2503)) mod 2503)) mod 2503) by NEWTON: 8

 .= ((1647 * ((1178 * ((1228 * ((2 |^ (64 + 6)) mod 2503)) mod 2503)) mod 2503)) mod 2503) by A25, EULER_2: 9

 .= ((1647 * ((1178 * ((1228 * (((2 |^ 64) * (2 |^ 6)) mod 2503)) mod 2503)) mod 2503)) mod 2503) by NEWTON: 8

 .= ((1647 * ((1178 * ((1228 * ((359 * ((2 |^ (4 + 2)) mod 2503)) mod 2503)) mod 2503)) mod 2503)) mod 2503) by A23, EULER_2: 9

 .= ((1647 * ((1178 * ((1228 * ((359 * (((2 |^ 4) * (2 |^ 2)) mod 2503)) mod 2503)) mod 2503)) mod 2503)) mod 2503) by NEWTON: 8

 .= ((1647 * ((1178 * ((1228 * ((359 * ((16 * 4) mod 2503)) mod 2503)) mod 2503)) mod 2503)) mod 2503) by A18, A19, EULER_2: 9

 .= ((1647 * ((1178 * ((1228 * ((359 * 64) mod 2503)) mod 2503)) mod 2503)) mod 2503) by NAT_D: 24

 .= ((1647 * ((1178 * ((1228 * 449) mod 2503)) mod 2503)) mod 2503) by A4, NAT_D:def 2

 .= ((1647 * ((1178 * 712) mod 2503)) mod 2503) by A8, NAT_D:def 2

 .= ((1647 * 231) mod 2503) by A6, NAT_D:def 2

 .= 1 by A10, NAT_D:def 2;

 hence thesis by A16, A27, Th25, Th34;

 end;

 theorem :: NAT_4:40



 Th40: 4001 is prime

 proof



 A1: ((2 |^ 1) mod 4001) = 2 by NAT_D: 24;



 A2: ((2 |^ 2) mod 4001) = ((2 |^ (2 * 1)) mod 4001)

 .= ((2 * 2) mod 4001) by A1, Th11

 .= 4 by NAT_D: 24;



 A3: ((2 |^ 4) mod 4001) = ((2 |^ (2 * 2)) mod 4001)

 .= ((4 * 4) mod 4001) by A2, Th11

 .= 16 by NAT_D: 24;



 A4: ((2 |^ 8) mod 4001) = ((2 |^ (2 * 4)) mod 4001)

 .= ((16 * 16) mod 4001) by A3, Th11

 .= 256 by NAT_D: 24;



 A5: (4001 - 1) = (((5 * 5) * 5) * 32);

 (256 * 256) = ((4001 * 16) + 1520);

 then

 A6: ((256 * 256) mod 4001) = 1520 by NAT_D:def 2;



 A7: ((5 * 5) * 5) = (((5 |^ 1) * 5) * 5)

 .= ((5 |^ (1 + 1)) * 5) by NEWTON: 6

 .= (5 |^ ((1 + 1) + 1)) by NEWTON: 6

 .= (5 |^ 3);

 (1023 * 1023) = ((4001 * 261) + 2268);

 then

 A8: ((1023 * 1023) mod 4001) = 2268 by NAT_D:def 2;



 A9: ((2 |^ 800) -' 1) = ((2 |^ 800) - 1) by PREPOWER: 11, XREAL_1: 233;



 A10: 6311 = ((4001 * 1) + 2310);



 A11: (3906 * 1913) = ((4001 * 1867) + 2311);



 A12: (1522 * 1823) = ((4001 * 693) + 1913);

 (3441 * 3441) = ((4001 * 2959) + 1522);

 then

 A13: ((3441 * 3441) mod 4001) = 1522 by NAT_D:def 2;



 A14: (1023 * 2164) = ((4001 * 553) + 1219);

 (2499 * 2499) = ((4001 * 1560) + 3441);

 then

 A15: ((2499 * 2499) mod 4001) = 3441 by NAT_D:def 2;



 A16: (3906 * 988) = ((4001 * 964) + 2164);

 (1823 * 1823) = ((4001 * 830) + 2499);

 then

 A17: ((1823 * 1823) mod 4001) = 2499 by NAT_D:def 2;



 A18: (1522 * 3376) = ((4001 * 1284) + 988);

 (1520 * 1520) = ((4001 * 577) + 1823);

 then

 A19: ((1520 * 1520) mod 4001) = 1823 by NAT_D:def 2;



 A20: (3441 * 1823) = ((4001 * 1567) + 3376);

 (1522 * 1522) = ((4001 * 578) + 3906);

 then

 A21: ((1522 * 1522) mod 4001) = 3906 by NAT_D:def 2;



 A22: (2268 * 1219) = ((4001 * 691) + 1);

 (3906 * 3906) = ((4001 * 3813) + 1023);

 then

 A23: ((3906 * 3906) mod 4001) = 1023 by NAT_D:def 2;



 A24: (4001 -' 1) = (4001 - 1) by XREAL_1: 233

 .= 4000;



 A25: ((2 |^ 16) mod 4001) = ((2 |^ (2 * 8)) mod 4001)

 .= 1520 by A4, A6, Th11;



 A26: ((2 |^ 32) mod 4001) = ((2 |^ (2 * 16)) mod 4001)

 .= 1823 by A25, A19, Th11;



 A27: ((2 |^ 64) mod 4001) = ((2 |^ (2 * 32)) mod 4001)

 .= 2499 by A26, A17, Th11;



 A28: ((2 |^ 128) mod 4001) = ((2 |^ (2 * 64)) mod 4001)

 .= 3441 by A27, A15, Th11;



 A29: ((2 |^ 256) mod 4001) = ((2 |^ (2 * 128)) mod 4001)

 .= 1522 by A28, A13, Th11;



 A30: ((2 |^ 512) mod 4001) = ((2 |^ (2 * 256)) mod 4001)

 .= 3906 by A29, A21, Th11;



 A31: ((2 |^ 1024) mod 4001) = ((2 |^ (2 * 512)) mod 4001)

 .= 1023 by A30, A23, Th11;



 A32: ((2 |^ 800) mod 4001) = ((2 |^ (512 + 288)) mod 4001)

 .= (((2 |^ 512) * (2 |^ 288)) mod 4001) by NEWTON: 8

 .= ((3906 * ((2 |^ (256 + 32)) mod 4001)) mod 4001) by A30, EULER_2: 9

 .= ((3906 * (((2 |^ 256) * (2 |^ 32)) mod 4001)) mod 4001) by NEWTON: 8

 .= ((3906 * ((1522 * 1823) mod 4001)) mod 4001) by A26, A29, EULER_2: 9

 .= ((3906 * 1913) mod 4001) by A12, NAT_D:def 2

 .= 2311 by A11, NAT_D:def 2;

 4000 = ((5 * 800) + 0 );



 then

 A33: (((2 |^ ((4001 -' 1) div 5)) -' 1) gcd 4001) = (((2 |^ 800) -' 1) gcd 4001) by A24, NAT_D:def 1

 .= ((((2 |^ 800) -' 1) + (4001 * 1)) gcd 4001) by EULER_1: 8

 .= (4001 gcd (((2 |^ 800) + 4000) mod 4001)) by A9, NAT_D: 28

 .= (4001 gcd ((2311 + (4000 mod 4001)) mod 4001)) by A32, EULER_2: 6

 .= (4001 gcd ((2311 + 4000) mod 4001)) by NAT_D: 24

 .= (((2310 * 1) + 1691) gcd 2310) by A10, NAT_D:def 2

 .= (1691 gcd ((1691 * 1) + 619)) by EULER_1: 8

 .= (((619 * 2) + 453) gcd 619) by EULER_1: 8

 .= (((453 * 1) + 166) gcd 453) by EULER_1: 8

 .= (166 gcd ((166 * 2) + 121)) by EULER_1: 8

 .= (((121 * 1) + 45) gcd 121) by EULER_1: 8

 .= (45 gcd ((45 * 2) + 31)) by EULER_1: 8

 .= (((31 * 1) + 14) gcd 31) by EULER_1: 8

 .= (14 gcd ((14 * 2) + 3)) by EULER_1: 8

 .= (((3 * 4) + 2) gcd 3) by EULER_1: 8

 .= (2 gcd ((2 * 1) + 1)) by EULER_1: 8

 .= (2 gcd 1) by EULER_1: 8

 .= 1 by NEWTON: 51;



 A34: ((2 |^ 2048) mod 4001) = ((2 |^ (2 * 1024)) mod 4001)

 .= 2268 by A31, A8, Th11;

 ((2 |^ (4001 -' 1)) mod 4001) = ((2 |^ (2048 + 1952)) mod 4001) by A24

 .= (((2 |^ 2048) * (2 |^ 1952)) mod 4001) by NEWTON: 8

 .= ((((2 |^ 2048) mod 4001) * ((2 |^ (1024 + 928)) mod 4001)) mod 4001) by EULER_2: 9

 .= ((2268 * (((2 |^ 1024) * (2 |^ 928)) mod 4001)) mod 4001) by A34, NEWTON: 8

 .= ((2268 * ((1023 * ((2 |^ (512 + 416)) mod 4001)) mod 4001)) mod 4001) by A31, EULER_2: 9

 .= ((2268 * ((1023 * (((2 |^ 512) * (2 |^ 416)) mod 4001)) mod 4001)) mod 4001) by NEWTON: 8

 .= ((2268 * ((1023 * ((3906 * ((2 |^ (256 + 160)) mod 4001)) mod 4001)) mod 4001)) mod 4001) by A30, EULER_2: 9

 .= ((2268 * ((1023 * ((3906 * (((2 |^ 256) * (2 |^ 160)) mod 4001)) mod 4001)) mod 4001)) mod 4001) by NEWTON: 8

 .= ((2268 * ((1023 * ((3906 * ((1522 * ((2 |^ (128 + 32)) mod 4001)) mod 4001)) mod 4001)) mod 4001)) mod 4001) by A29, EULER_2: 9

 .= ((2268 * ((1023 * ((3906 * ((1522 * (((2 |^ 128) * (2 |^ 32)) mod 4001)) mod 4001)) mod 4001)) mod 4001)) mod 4001) by NEWTON: 8

 .= ((2268 * ((1023 * ((3906 * ((1522 * ((3441 * 1823) mod 4001)) mod 4001)) mod 4001)) mod 4001)) mod 4001) by A26, A28, EULER_2: 9

 .= ((2268 * ((1023 * ((3906 * ((1522 * 3376) mod 4001)) mod 4001)) mod 4001)) mod 4001) by A20, NAT_D:def 2

 .= ((2268 * ((1023 * ((3906 * 988) mod 4001)) mod 4001)) mod 4001) by A18, NAT_D:def 2

 .= ((2268 * ((1023 * 2164) mod 4001)) mod 4001) by A16, NAT_D:def 2

 .= ((2268 * 1219) mod 4001) by A14, NAT_D:def 2

 .= 1 by A22, NAT_D:def 2;

 hence thesis by A5, A7, A33, Th25, PEPIN: 59;

 end;



 Lm7: for n be Element of NAT st 1 <= n & n < 4001 holds ex p be Prime st n < p & p <= (2 * n)

 proof

 let n be Element of NAT ;



 A1: for a,n,p be Element of NAT st a <= n & p <= (2 * a) holds p <= (2 * n)

 proof

 let a,n,p be Element of NAT ;

 assume that

 A2: a <= n and

 A3: p <= (2 * a);

 (2 * a) <= (2 * n) by A2, XREAL_1: 64;

 hence thesis by A3, XXREAL_0: 2;

 end;

 assume

 A4: 1 <= n & n < 4001;

 per cases by A4;

 suppose

 A5: 1 <= n & n < 2;

 2 <= (2 * 1);

 then 2 <= (2 * n) by A1, A5;

 hence thesis by A5, INT_2: 28;

 end;

 suppose

 A6: 2 <= n & n < 3;

 3 <= (2 * 2);

 then 3 <= (2 * n) by A1, A6;

 hence thesis by A6, PEPIN: 41;

 end;

 suppose

 A7: 3 <= n & n < 5;

 5 <= (2 * 3);

 then 5 <= (2 * n) by A1, A7;

 hence thesis by A7, PEPIN: 59;

 end;

 suppose

 A8: 5 <= n & n < 7;

 7 <= (2 * 5);

 then 7 <= (2 * n) by A1, A8;

 hence thesis by A8, Th26;

 end;

 suppose

 A9: 7 <= n & n < 13;

 13 <= (2 * 7);

 then 13 <= (2 * n) by A1, A9;

 hence thesis by A9, Th28;

 end;

 suppose

 A10: 13 <= n & n < 23;

 23 <= (2 * 13);

 then 23 <= (2 * n) by A1, A10;

 hence thesis by A10, Th30;

 end;

 suppose

 A11: 23 <= n & n < 43;

 43 <= (2 * 23);

 then 43 <= (2 * n) by A1, A11;

 hence thesis by A11, Th32;

 end;

 suppose

 A12: 43 <= n & n < 83;

 83 <= (2 * 43);

 then 83 <= (2 * n) by A1, A12;

 hence thesis by A12, Th33;

 end;

 suppose

 A13: 83 <= n & n < 163;

 163 <= (2 * 83);

 then 163 <= (2 * n) by A1, A13;

 hence thesis by A13, Th35;

 end;

 suppose

 A14: 163 <= n & n < 317;

 317 <= (2 * 163);

 then 317 <= (2 * n) by A1, A14;

 hence thesis by A14, Th36;

 end;

 suppose

 A15: 317 <= n & n < 631;

 631 <= (2 * 317);

 then 631 <= (2 * n) by A1, A15;

 hence thesis by A15, Th37;

 end;

 suppose

 A16: 631 <= n & n < 1259;

 1259 <= (2 * 631);

 then 1259 <= (2 * n) by A1, A16;

 hence thesis by A16, Th38;

 end;

 suppose

 A17: 1259 <= n & n < 2503;

 2503 <= (2 * 1259);

 then 2503 <= (2 * n) by A1, A17;

 hence thesis by A17, Th39;

 end;

 suppose

 A18: 2503 <= n & n < 4001;

 4001 <= (2 * 2503);

 then 4001 <= (2 * n) by A1, A18;

 hence thesis by A18, Th40;

 end;

 end;

 begin

 ::$Canceled

 theorem :: NAT_4:42



 Th41: for F be FinSequence of REAL st (for k be Element of NAT st k in ( dom F) holds (F . k) > 0 ) holds ( Product F) > 0

 proof

 defpred P[ Nat] means for F be FinSequence of REAL st (for k be 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 be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume

 A2: P[n];

 for F be FinSequence of REAL st (for k be 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 be Element of NAT st k in ( dom F) holds (F . k) > 0 ;

 assume

 A4: ( len F) = (n + 1);

 then

 consider F1,F2 be 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 be 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 be 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 be Nat holds P[n] from NAT_1:sch 2( A12, A1);



 A14: ex n be Element of NAT st n = ( len F);

 assume for k be Element of NAT st k in ( dom F) holds (F . k) > 0 ;

 hence thesis by A13, A14;

 end;

 theorem :: NAT_4:43



 Th42: for X1 be set, X2 be 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 be set, X2 be 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 be 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);



 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);

 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 be 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 be Nat holds P[n] from NAT_1:sch 2( A37, A1);

 hence thesis by A35, A36;

 end;

 theorem :: NAT_4:44



 Th43: for a,k be Element of NAT , X be set, F be FinSequence of SetPrimes , p be 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 be Element of NAT , X be set, F be FinSequence of SetPrimes , p be 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 be Element of NAT st n = ( len F);



 A2: for n be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume

 A3: P[n];

 for a,k be Element of NAT , X be set, F be FinSequence of SetPrimes , p be 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 be 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, FINSEQ_1: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 be Nat holds P[n] from NAT_1:sch 2( A43, A2);

 hence thesis by A1;

 end;

 theorem :: NAT_4:45



 Th44: for n be Element of NAT holds ( Product ( Sgm { p where p be prime Element of NAT : p <= (n + 1) })) <= (4 to_power n)

 proof

 defpred P[ Nat] means ( Product ( Sgm { p where p be prime Element of NAT : p <= ($1 + 1) })) <= (4 to_power $1);

 let n be Element of NAT ;



 A1: for m be Nat st (for n be Nat st n < m holds P[n]) holds P[m]

 proof

 let m be Nat;

 assume

 A2: for n be Nat st n < m holds P[n];

 per cases by XXREAL_0: 1;

 suppose

 A3: m < 1;

 A4:

 now

 assume { p where p be prime Element of NAT : p <= ( 0 + 1) } <> {} ;

 then

 consider y be object such that

 A5: y in { p where p be prime Element of NAT : p <= 1 } by XBOOLE_0:def 1;

 ex y9 be 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 be prime Element of NAT : p <= 2 };

 then

 consider y9 be 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 be object st y = 2 holds y in { p where p be prime Element of NAT : p <= 2 } by INT_2: 28;

 then

 A10: { p where p be prime Element of NAT : p <= 2 } = {2} by A8, TARSKI:def 1;

 ( Product ( Sgm {2})) = ( Product <*2*>) by FINSEQ_3: 44

 .= 2;

 hence thesis by A6, A10, A7;

 end;

 suppose

 A11: m > 1;

 per cases ;

 suppose (m + 1) is odd;

 then

 consider k be 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 be 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 be Nat holds Q[k] from NAT_1:sch 2( A23, A14);

 hence thesis;

 end;

 set Y = { p where p be 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 be 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 be object holds y in X implies y in ( Seg (k + 1))

 proof

 let y be object;

 assume y in X;

 then

 A26: ex y9 be 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 be 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 be 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 be 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 be prime Element of NAT st y9 = a & y9 <= (k + 1);

 assume b in Y;

 then ex y99 be prime Element of NAT st y99 = b & y99 > (k + 1) & y99 <= ((2 * k) + 1);

 hence thesis by A31, XXREAL_0: 2;

 end;

 for y be 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 be 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 be 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 be 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 be 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 be 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 be 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, NEWTON: 80;

 per cases by A41, A47, NEWTON: 80;

 suppose

 A48: p divides (k ! );

 (k + 0 ) < (k + 1) by XREAL_1: 6;

 then k < p by A44, XXREAL_0: 2;

 hence contradiction by A41, A48, Th19;

 end;

 suppose p divides (r ! );

 hence contradiction by A41, A44, Th19;

 end;

 end;

 p <> 1 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 be 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 be 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 be object holds y in { p where p be 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 be 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 be prime Element of NAT : p <= ((2 * k) + 1) } by A55;

 end;

 suppose y in Y;

 then ex y9 be prime Element of NAT st y9 = y & y9 > (k + 1) & y9 <= ((2 * k) + 1);

 hence y in { p where p be prime Element of NAT : p <= ((2 * k) + 1) };

 end;

 end;

 now

 assume y in { p where p be prime Element of NAT : p <= ((2 * k) + 1) };

 then

 consider y9 be 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 be 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;

 0 < ( Product SY) by A34, Th41;

 then ( Product (SX ^ SY)) = (( Product SX) * ( Product SY)) & (( Product SX) * ( Product SY)) <= ((4 to_power k) * (4 to_power k)) by A25, A59, A29, RVSUM_1: 97, XREAL_1: 66;

 then ( Product (SX ^ SY)) <= (4 to_power (k + k)) by POWER: 27;

 hence thesis by A12, A27, A33, A58, A30, FINSEQ_3: 42;

 end;

 suppose

 A60: (m + 1) is even;

 set k = (m - 1);

 (m - 1) > (1 - 1) by A11, XREAL_1: 9;

 then

 reconsider k as Element of NAT by INT_1: 3;

 for y be object holds y in { p where p be prime Element of NAT : p <= (m + 1) } iff y in { p where p be prime Element of NAT : p <= m }

 proof

 let y be object;

 A61:

 now

 assume y in { p where p be prime Element of NAT : p <= (m + 1) };

 then

 consider y9 be 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 < (m + 1) by A63, XXREAL_0: 1;

 then y9 <= m by NAT_1: 13;

 hence y in { p where p be prime Element of NAT : p <= m } by A62;

 end;

 now

 assume y in { p where p be prime Element of NAT : p <= m };

 then

 consider y9 be prime Element of NAT such that

 A64: y = y9 and

 A65: y9 <= m;

 ( 0 + m) <= (1 + m) by XREAL_1: 6;

 then y9 <= (m + 1) by A65, XXREAL_0: 2;

 hence y in { p where p be prime Element of NAT : p <= (m + 1) } by A64;

 end;

 hence thesis by A61;

 end;

 then

 A66: { p where p be prime Element of NAT : p <= (m + 1) } = { p where p be prime Element of NAT : p <= m } by TARSKI: 2;

 (k + 1) = m;

 then k < m by NAT_1: 13;

 then ( Product ( Sgm { p where p be prime Element of NAT : p <= (k + 1) })) <= (4 to_power k) & (4 to_power k) <= (4 to_power m) by A2, POWER: 39;

 hence thesis by A66, XXREAL_0: 2;

 end;

 end;

 end;

 for n be Nat holds P[n] from NAT_1:sch 4( A1);

 hence thesis;

 end;

 theorem :: NAT_4:46



 Th45: for x be Real st x >= 2 holds ( Product ( Sgm { p where p be prime Element of NAT : p <= x })) <= (4 to_power (x - 1))

 proof

 let x be Real;

 set A = { p where p be prime Element of NAT : p <= x };



 A1: A is finite

 proof

 ex m be Element of NAT st x < m

 proof

 set m = ( |. [/x\].| + 1);

 take m;

 [/x\] <= |. [/x\].| & |. [/x\].| < ( |. [/x\].| + 1) by ABSVALUE: 4, NAT_1: 13;

 then x <= [/x\] & [/x\] < ( |. [/x\].| + 1) by INT_1:def 7, XXREAL_0: 2;

 hence thesis by XXREAL_0: 2;

 end;

 then

 consider m be Element of NAT such that

 A2: x < m;

 set B = ( SetPrimenumber m);

 A c= B

 proof

 let y be object;

 assume y in { p where p be prime Element of NAT : p <= x };

 then

 consider y9 be prime Element of NAT such that

 A3: y9 = y and

 A4: y9 <= x;

 y9 < m by A2, A4, XXREAL_0: 2;

 hence thesis by A3, NEWTON:def 7;

 end;

 hence thesis;

 end;



 A5: A is real-membered

 proof

 let y be object;

 y in A implies y is real

 proof

 assume y in { p where p be prime Element of NAT : p <= x };

 then ex y9 be prime Element of NAT st y9 = y & y9 <= x;

 hence thesis;

 end;

 hence thesis;

 end;

 assume

 A6: 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 be prime Element of NAT st q9 = q & q9 <= x;

 then

 reconsider q as Prime;

 for y be object holds y in { p where p be prime Element of NAT : p <= q } iff y in { p where p be prime Element of NAT : p <= x }

 proof

 let y be object;

 hereby

 assume y in { p where p be prime Element of NAT : p <= q };

 then

 consider y9 be 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 be prime Element of NAT : p <= x } by A9;

 end;

 assume

 A11: y in { p where p be prime Element of NAT : p <= x };

 then

 consider y9 be 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 be prime Element of NAT : p <= q } = { p where p be 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 q < x;

 then (q - 1) < (x - 1) by XREAL_1: 14;

 hence thesis by POWER: 39;

 end;

 end;

 ( Product ( Sgm { p where p be prime Element of NAT : p <= x })) <= (4 to_power (x - 1))

 proof

 set b = (4 to_power (q - 1));

 set a = ( Product ( Sgm { p where p be prime Element of NAT : p <= q }));

 set n = (q -' 1);

 q > 1 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 :: NAT_4:47



 Th46: for n be Element of NAT , p be Prime st n <> 0 holds ex f be FinSequence of NAT st ( len f) = n & (for k be 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 be Nat st k in ( Seg n) holds ex x be 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 be FinSequence such that

 A9: ( dom f) = ( Seg n) and

 A10: for k be 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 be 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 be 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 < (p |-count n) by A20, XXREAL_0: 2;

 (i + 1) = x1 by A20;

 hence thesis by A22, A21, NAT_3: 4;

 end;

 end;

 (ff1 . x) = 1 by A18, FUNCOP_1: 7;

 then (f1 . x1) = 1 by A17, FINSEQ_1:def 7;

 hence thesis by A9, A10, A15, A19;

 end;

 suppose ex m be Nat st m in ( dom ff2) & x1 = (( len ff1) + m);

 then

 consider m be Nat such that

 A23: m in ( dom ff2) and

 A24: x = (( len ff1) + m);

 m in ( Seg n2) by A23, FUNCOP_1: 13;

 then m >= 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 be 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 :: NAT_4:48



 Th47: for n be Element of NAT , p be Prime holds ex f be FinSequence of NAT st ( len f) = n & (for k be 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 be Prime holds ex f be FinSequence of NAT st ( len f) = $1 & (for k be 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 be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume

 A2: P[n];

 for p be Prime holds ex f be FinSequence of NAT st ( len f) = (n + 1) & (for k be 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 be FinSequence of NAT such that

 A3: ( len fn) = n and

 A4: for k be 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 be FinSequence of NAT such that

 A6: ( len fn1) = (n + 1) and

 A7: for k be 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 be 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 be 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 be Nat st n1 in ( dom <* 0 *>) & k = (( len fn) + n1);

 then

 consider n1 be 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 be 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;

 m < (p |^ k) & ( 0 + (p |^ k)) < (1 + (p |^ k)) by NAT_D: 1, XREAL_1: 6;

 then m < ((p |^ k) + 1) by XXREAL_0: 2;

 then (m - 1) < (((p |^ k) + 1) - 1) by XREAL_1: 9;

 then ((m - 1) / (p |^ k)) < ((p |^ k) / (p |^ k)) by XREAL_1: 74;

 then

 A31: (((m - 1) / (p |^ k)) - 1) < (1 - 1) by A12, XREAL_1: 9;

 (m / (p |^ k)) < ((p |^ k) / (p |^ k)) by NAT_D: 1, XREAL_1: 74;

 then

 A32: ((m / (p |^ k)) - 1) < (1 - 1) by A12, XREAL_1: 9;



 A33: (fn1 . k) = 0 by A7, A23, A28;

 n = (((p |^ k) * d) + (m - 1)) by A29;



 then [\(n / (p |^ k))/] = [\((((p |^ k) * d) / (p |^ k)) + ((m - 1) / (p |^ k)))/] by XCMPLX_1: 62

 .= [\((d * ((p |^ k) / (p |^ k))) + ((m - 1) / (p |^ k)))/] by XCMPLX_1: 74

 .= [\((d * 1) + ((m - 1) / (p |^ k)))/] by XCMPLX_1: 60

 .= (d + [\((m - 1) / (p |^ k))/]) by INT_1: 28

 .= (d + 0 ) by A30, A31, INT_1:def 6

 .= (d + [\(m / (p |^ k))/]) by A32, INT_1:def 6

 .= [\((d * 1) + (m / (p |^ k)))/] by INT_1: 28

 .= [\((d * ((p |^ k) / (p |^ k))) + (m / (p |^ k)))/] by XCMPLX_1: 60

 .= [\((((p |^ k) * d) / (p |^ k)) + (m / (p |^ k)))/] by XCMPLX_1: 74

 .= [\((((p |^ k) * d) + m) / (p |^ k))/] by XCMPLX_1: 62

 .= [\((n + 1) / (p |^ k))/] by NAT_D: 2;

 hence thesis by A14, A16, A33;

 end;

 end;

 reconsider fn1 as Element of ((n + 1) -tuples_on REAL ) by A6, FINSEQ_2: 92;

 reconsider fn0 as Element of ((n + 1) -tuples_on REAL ) by A11, FINSEQ_2: 92;



 A34: ((p |-count (n ! )) + (p |-count (n + 1))) = (p |-count ((n ! ) * (n + 1))) by NAT_3: 28

 .= (p |-count ((n + 1) ! )) by NEWTON: 15;

 ( Sum f) = (( Sum fn0) + ( Sum fn1)) by RVSUM_1: 89

 .= ((( Sum fn) + 0 ) + (p |-count (n + 1))) by A8, RVSUM_1: 74

 .= ((p |-count (n ! )) + (p |-count (n + 1))) by A5;

 hence thesis by A34;

 end;

 hence thesis;

 end;



 A35: P[ 0 ]

 proof

 set f = ( <*> NAT );

 let p be Prime;

 take f;

 thus ( len f) = 0 ;

 thus for k be 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 be Nat holds P[n] from NAT_1:sch 2( A35, A1);

 then

 consider f be FinSequence of NAT such that

 A36: (( len f) = n & for k be 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 :: NAT_4:49



 Th48: for n be Element of NAT , p be Prime holds ex f be FinSequence of REAL st ( len f) = (2 * n) & (for k be 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 be FinSequence of NAT such that

 A1: ( len f1) = n and

 A2: for k be 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 be FinSequence of NAT such that

 A4: ( len f2) = (2 * n) and

 A5: for k be 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 be 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 be Nat st e in ( dom f0) & k = (( len f1) + e);

 then

 consider e be 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 be Element of NAT , p be Prime, f be FinSequence of REAL st (p |^ r) <= (2 * n) & (2 * n) < (p |^ (r + 1)) & ( len f) = (2 * n) & (for k be 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)) < (p to_power r) by A1, POWER: 39;

 then (p |^ (2 * n)) < (p to_power r) by POWER: 41;

 then (p |^ (2 * n)) < (p |^ r) by POWER: 41;

 then (p |^ (2 * n)) < (2 * n) by A2, XXREAL_0: 2;

 hence contradiction by A1, Th3;

 end;

 assume

 A4: (2 * n) < (p |^ (r + 1));

 assume

 A5: ( len f) = (2 * n);



 A6: ( len f0) = (( len (r |-> 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 be 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 be 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) < k or (r + 1) = k by A19, XXREAL_0: 1;

 then (p to_power (r + 1)) <= (p to_power k) by A1, POWER: 39;

 then (p |^ (r + 1)) <= (p to_power k) by POWER: 41;

 then (p |^ (r + 1)) <= (p |^ k1) by POWER: 41;

 then (2 * n) < (p |^ k) by A4, XXREAL_0: 2;

 then ((2 * n) / (p |^ k)) < ((p |^ k) / (p |^ k)) by XREAL_1: 74;

 then

 A20: ((2 * n) / (p |^ k)) < 1 by XCMPLX_1: 60;

 then (((2 * n) / (p |^ k)) / 2) < (1 / 2) by XREAL_1: 74;

 then (((2 * n) / 2) / (p |^ k)) < (1 / 2) by XCMPLX_1: 48;

 then (n / (p |^ k)) < 1 by XXREAL_0: 2;

 then ((n / (p |^ k)) - 1) < (1 - 1) by XREAL_1: 9;

 then

 A21: [\(n / (p |^ k))/] = 0 by INT_1:def 6;

 (((2 * n) / (p |^ k)) - 1) < (1 - 1) by A20, XREAL_1: 9;

 hence thesis by A10, A21, INT_1:def 6;

 end;

 end;



 A22: f0 = ((r |-> ( 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 be Element of NAT , p be Prime st n >= 3 holds (p > (2 * n) implies (p |-count ((2 * n) choose n)) = 0 ) & (n < p & p <= (2 * n) implies (p |-count ((2 * n) choose n)) <= 1) & (((2 * n) / 3) < p & p <= n implies (p |-count ((2 * n) choose n)) = 0 ) & (( sqrt (2 * n)) < p & p <= ((2 * n) / 3) implies (p |-count ((2 * n) choose n)) <= 1) & (p <= ( sqrt (2 * n)) implies (p |^ (p |-count ((2 * n) choose n))) <= (2 * n))

 proof

 let n be Element of NAT ;

 let p be Prime;

 assume

 A1: n >= 3;



 A2: for n,r be Element of NAT , p be 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 be 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 < p & p <= (2 * n) implies (p |-count ((2 * n) choose n)) <= 1

 proof

 set r = 1;

 assume

 A6: n < p;

 then

 A7: (n * 2) < (p * 2) by XREAL_1: 68;



 A8: n >= 2 by A1, XXREAL_0: 2;

 then 2 < p by A6, XXREAL_0: 2;

 then (2 * p) < (p * p) by XREAL_1: 68;

 then (2 * n) < (p * p) by A7, XXREAL_0: 2;

 then (2 * n) < ((p |^ 1) * p);

 then

 A9: (2 * n) < (p |^ (1 + 1)) by NEWTON: 6;

 assume p <= (2 * n);

 then (p |^ r) <= (2 * n);

 hence thesis by A2, A8, A9;

 end;

 thus ((2 * n) / 3) 0 );

 assume

 A10: ((2 * n) / 3) < p;

 consider f be FinSequence of REAL such that

 A11: ( len f) = (2 * n) and

 A12: for k be Element of NAT st k in ( dom f) holds (f . k) = ( [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/])) and

 A13: (p |-count ((2 * n) choose n)) = ( Sum f) by Th48;



 A14: ( dom f) = ( Seg (2 * n)) by A11, FINSEQ_1:def 3;

 assume

 A15: p <= n;



 A16: for k be Element of NAT st k in ( dom f) holds (f . k) = 0

 proof

 let k be Element of NAT ;



 A17: for m be Element of NAT holds ((m * p) / p) = m

 proof

 let m be Element of NAT ;

 (p / p) = 1 by XCMPLX_1: 60;

 then (m * (p / p)) = m;

 hence thesis by XCMPLX_1: 74;

 end;

 (p * 2) <= (n * 2) by A15, XREAL_1: 64;

 then ((2 * p) / p) <= ((2 * n) / p) by XREAL_1: 72;

 then

 A18: 2 <= ((2 * n) / p) by A17;

 assume

 A19: k in ( dom f);

 then

 A20: k in ( Seg ( len f)) by FINSEQ_1:def 3;

 then

 A21: 1 <= k by FINSEQ_1: 1;



 A22: (((2 * n) / 3) * 3) < (p * 3) by A10, XREAL_1: 68;

 then ((2 * n) / p) < ((3 * p) / p) by XREAL_1: 74;

 then ((2 * n) / p) < 3 by A17;

 then

 A23: (((2 * n) / p) - 1) < (3 - 1) by XREAL_1: 9;

 per cases by A11, A20, A21, FINSEQ_1: 1, XXREAL_0: 1;

 suppose

 A24: k = 1;

 (3 * p) < (4 * p) by XREAL_1: 68;

 then (2 * n) < (4 * p) by A22, XXREAL_0: 2;

 then ((n * 2) / 2) < (((2 * p) * 2) / 2) by XREAL_1: 74;

 then (n / p) < ((2 * p) / p) by XREAL_1: 74;

 then (n / p) < 2 by A17;

 then

 A25: ((n / p) - 1) < (2 - 1) by XREAL_1: 9;

 ((1 * p) / p) <= (n / p) by A15, XREAL_1: 72;

 then 1 <= (n / p) by A17;

 then

 A26: [\(n / p)/] = 1 by A25, INT_1:def 6;

 (f . k) = ( [\((2 * n) / (p |^ 1))/] - (2 * [\(n / (p |^ 1))/])) by A12, A19, A24

 .= ( [\((2 * n) / p)/] - (2 * [\(n / (p |^ 1))/]))

 .= ( [\((2 * n) / p)/] - (2 * [\(n / p)/]))

 .= (2 - (2 * 1)) by A18, A23, A26, INT_1:def 6;

 hence thesis;

 end;

 suppose 1 < k & k <= (2 * n);

 then (1 + 1) < (k + 1) by XREAL_1: 6;

 then 2 <= k by NAT_1: 13;

 then

 A27: k = 2 or 2 < k by XXREAL_0: 1;

 (3 * 2) <= (n * 2) by A1, XREAL_1: 64;

 then (2 * 3) < (3 * p) by A22, XXREAL_0: 2;

 then ((2 * 3) / 3) < ((p * 3) / 3) by XREAL_1: 74;

 then (2 + 1) < (p + 1) by XREAL_1: 6;

 then 3 <= p by NAT_1: 13;

 then (3 * p) <= (p * p) by XREAL_1: 64;

 then (2 * n) < (p * p) by A22, XXREAL_0: 2;

 then (2 * n) < ((p |^ 1) * p);

 then

 A28: (2 * n) < (p |^ (1 + 1)) by NEWTON: 6;

 p > 1 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 n < (p |^ 2) by A28, XXREAL_0: 2;

 then n < (p |^ k) by A29, XXREAL_0: 2;

 then (n / (p |^ k)) < ((p |^ k) / (p |^ k)) by XREAL_1: 74;

 then (n / (p |^ k)) < 1 by XCMPLX_1: 60;

 then

 A31: ((n / (p |^ k)) - 1) < (1 - 1) by XREAL_1: 9;

 (f . k) = ( [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/])) by A12, A19

 .= ( 0 qua Nat - (2 * 0 )) by A31, A30, INT_1:def 6;

 hence thesis;

 end;

 end;



 A32: for k be Nat st k in ( dom f) holds (f . k) = (q . k) by A16;

 ( dom q) = ( Seg (2 * n)) by FUNCOP_1: 13;

 then q = f by A14, A32, FINSEQ_1: 13;

 then ( Sum f) = ((2 * n) * 0 ) by RVSUM_1: 80;

 hence thesis by A13;

 end;

 thus ( sqrt (2 * n)) < p & p <= ((2 * n) / 3) implies (p |-count ((2 * n) choose n)) <= 1

 proof

 set r = 1;

 assume

 A33: ( sqrt (2 * n)) < p;

 then

 A34: (( sqrt (2 * n)) * p) < (p * p) by XREAL_1: 68;

 ( sqrt (2 * n)) > 0 by A1, SQUARE_1: 25;

 then (( sqrt (2 * n)) * ( sqrt (2 * n))) < (p * ( sqrt (2 * n))) by A33, XREAL_1: 68;

 then (( sqrt (2 * n)) ^2 ) < (p * p) by A34, XXREAL_0: 2;

 then (2 * n) < (p * p) by SQUARE_1:def 2;

 then (2 * n) < ((p |^ 1) * p);

 then

 A35: (2 * n) < (p |^ (1 + 1)) by NEWTON: 6;

 assume p <= ((2 * n) / 3);

 then ((1 / 3) * (2 * n)) <= (1 * (2 * n)) & (p |^ r) <= ((2 * n) / 3) by XREAL_1: 64;

 then

 A36: (p |^ r) <= (2 * n) by XXREAL_0: 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;

 :: NAT_4:def1

 func p |-count f -> FinSequence of NAT means

 : Def1: ( len it ) = ( len f) & for i be set st i in ( dom it ) holds (it . i) = (p |-count (f . i));

 existence

 proof

 deffunc F( Nat) = (p |-count (f . $1));

 consider g be FinSequence such that

 A1: ( len g) = ( len f) and

 A2: for k be 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 be set st i in ( dom g) holds (g . i) = (p |-count (f . i)) and

 A7: ( len h) = ( len f) and

 A8: for i be 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 be 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 :: NAT_4:50



 Th49: for p be Prime, f be 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 :: NAT_4:51



 Th50: for p be Prime, f1,f2 be 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 be 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 be 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 :: NAT_4:52



 Th51: for p be Prime, n be 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 be 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 :: NAT_4:53



 Th52: for f be FinSequence of NAT , p be 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 be FinSequence of NAT , p be 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 be Element of NAT st n = ( len f);



 A3: for n be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume

 A4: P[n];

 for f be FinSequence of NAT , p be 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 be FinSequence of NAT , d be 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 be Nat holds P[n] from NAT_1:sch 2( A12, A3);

 hence thesis by A1, A2;

 end;

 theorem :: NAT_4:54



 Th53: for f1,f2 be FinSequence of REAL st ( len f1) = ( len f2) & (for k be 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 be FinSequence of REAL st ( len f1) = ( len f2) & $1 = ( len f1) & (for k be 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 be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume

 A3: P[n];

 for f1,f2 be FinSequence of REAL st ( len f1) = ( len f2) & (n + 1) = ( len f1) & (for k be 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 be 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 be 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 be Nat holds P[n] from NAT_1:sch 2( A21, A2);

 assume for k be Element of NAT st k in ( dom f1) holds (f1 . k) <= (f2 . k) & (f1 . k) > 0 ;

 hence thesis by A22, A1;

 end;

 theorem :: NAT_4:55



 Th54: for n be Element of NAT , r be Real st r > 0 holds ( Product (n |-> r)) = (r to_power n)

 proof

 defpred P[ Nat] means for r be Real st r > 0 holds ( Product ($1 |-> r)) = (r to_power $1);



 A1: for n be 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 be Nat holds P[n] from NAT_1:sch 2( A4, A1);

 hence thesis;

 end;

 scheme :: NAT_4:sch1

 scheme1 { P[ set, set, set] } :

for p be Prime, n be Element of NAT , m be non zero Element of NAT , X be set st X = { (p9 |^ (p9 |-count m)) where p9 be prime Element of NAT : P[n, m, p9] } holds ( Product ( Sgm X)) > 0 ;

 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 be prime Element of NAT : P[n, m, p9] };



 A2: for k be 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 be prime Element of NAT st (y9 |^ (y9 |-count m)) = x & P[n, m, y9] by A1;

 then ex b be 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 be 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 be prime Element of NAT : P[n, m, p9] } by A3, FUNCT_1: 3;

 then ex y9 be 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 :: NAT_4:sch2

 scheme2 { P[ set, set, set] } :

for p be Prime, n be Element of NAT , m be non zero Element of NAT , X be set st X = { (p9 |^ (p9 |-count m)) where p9 be prime Element of NAT : P[n, m, p9] } & not (p |^ (p |-count m)) in X holds (p |-count ( Product ( Sgm X))) = 0 ;

 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 be 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 be 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 be prime Element of NAT st (y9 |^ (y9 |-count m)) = x & P[n, m, y9] by A1;

 then ex b be 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 be 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 be 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 be Prime, n be Element of NAT , m be non zero Element of NAT , X be set st X = { (p9 |^ (p9 |-count m)) where p9 be 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 :: NAT_4:sch3

 scheme3 { P[ set, set, set] } :

for p be Prime, n be Element of NAT , m be non zero Element of NAT , X be set st X = { (p9 |^ (p9 |-count m)) where p9 be prime Element of NAT : P[n, m, p9] } & (p |^ (p |-count m)) in X holds (p |-count ( Product ( Sgm X))) = (p |-count m);

 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 be prime Element of NAT : P1[n, m, p9] };

 set X2 = { (p9 |^ (p9 |-count m)) where p9 be 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 be prime Element of NAT st (p1 |^ (p1 |-count m)) = k1 & P1[n, m, p1]) & ex p2 be 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 be 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 be prime Element of NAT : P11[n, m, p9] };

 set X12 = { (p9 |^ (p9 |-count m)) where p9 be 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 be prime Element of NAT st (p1 |^ (p1 |-count m)) = k1 & P11[n, m, p1]) & ex p2 be 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 be 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 be prime Element of NAT : P[n, m, p9] };

 now

 let x be object;

 assume x in X;

 then ex y9 be prime Element of NAT st (y9 |^ (y9 |-count m)) = x & P[n, m, y9] by A6;

 then ex b be 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 be Prime, n be Element of NAT , m be non zero Element of NAT , X be set st X = { (p9 |^ (p9 |-count m)) where p9 be 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 be 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 be 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 be 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 be Prime, n be Element of NAT , m be non zero Element of NAT , X2 be set st X2 = { (p9 |^ (p9 |-count m)) where p9 be 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 be Prime, n be Element of NAT , m be non zero Element of NAT , X2 be set st X2 = { (p9 |^ (p9 |-count m)) where p9 be 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 be 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 be 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 be 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 be 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 be Prime, n be Element of NAT , m be non zero Element of NAT , X11 be set st X11 = { (p9 |^ (p9 |-count m)) where p9 be 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 be Prime, n be Element of NAT , m be non zero Element of NAT , X11 be set st X11 = { (p9 |^ (p9 |-count m)) where p9 be 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 be Element of NAT st m = ((2 * n) choose n) & n >= 3 holds m = ((( Product ( Sgm { (p |^ (p |-count m)) where p be prime Element of NAT : p <= ( sqrt (2 * n)) & (p |-count m) > 0 })) * ( Product ( Sgm { (p |^ (p |-count m)) where p be prime Element of NAT : ( sqrt (2 * n)) 0 }))) * ( Product ( Sgm { (p |^ (p |-count m)) where p be 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 be prime Element of NAT : P3[n, m, p] };

 set X2 = { (p |^ (p |-count m)) where p be prime Element of NAT : P2[n, m, p] };

 set X1 = { (p |^ (p |-count m)) where p be 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 be Prime, n be Element of NAT , m be non zero Element of NAT , X be set st X = { (p9 |^ (p9 |-count m)) where p9 be 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 be Prime, n be Element of NAT , m be non zero Element of NAT , X be set st X = { (p9 |^ (p9 |-count m)) where p9 be 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, SQUARE_1: 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 < ( sqrt (2 * n));

 hence contradiction by A9, SQUARE_1:def 2;

 end;

 (m * (2 * n)) >= (((4 |^ n) / (2 * n)) * (2 * n)) by A1, Th6, XREAL_1: 64;

 then

 A10: m <> 0 by A4;



 A11: for p be Prime, n be Element of NAT , m be non zero Element of NAT , X be set st X = { (p9 |^ (p9 |-count m)) where p9 be 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 be Prime, n be Element of NAT , m be non zero Element of NAT , X be set st X = { (p9 |^ (p9 |-count m)) where p9 be 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 be Prime, n be Element of NAT , m be non zero Element of NAT , X be set st X = { (p9 |^ (p9 |-count m)) where p9 be 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 be Prime, n be Element of NAT , m be non zero Element of NAT , X be set st X = { (p9 |^ (p9 |-count m)) where p9 be 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 be 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 be 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 be 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 be 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 be Prime st ((2 * n) / 3) < p & p <= n holds (p |-count n1) = 0 & (p |-count n2) = 0 & (p |-count n3) = 0

 proof

 let p be Prime;

 assume that

 A21: ((2 * n) / 3) < p and

 A22: p <= n;



 A23: (p |-count m) = 0 by A1, A4, A21, A22, Lm9;

 now

 assume (p |^ (p |-count m)) in X1;

 then ex p9 be prime Element of NAT st (p9 |^ (p9 |-count m)) = (p |^ (p |-count m)) & P1[n, m, p9];

 hence contradiction by A10, A23, Th22;

 end;

 hence (p |-count n1) = 0 by A10, A16;

 now

 assume (p |^ (p |-count m)) in X2;

 then ex p9 be prime Element of NAT st (p9 |^ (p9 |-count m)) = (p |^ (p |-count m)) & P2[n, m, p9];

 hence contradiction by A10, A21, Th22;

 end;

 hence (p |-count n2) = 0 by A10, A2;

 now

 assume (p |^ (p |-count m)) in X3;

 then ex p9 be prime Element of NAT st (p9 |^ (p9 |-count m)) = (p |^ (p |-count m)) & P3[n, m, p9];

 hence contradiction by A10, A22, Th22;

 end;

 hence thesis by A10, A15;

 end;



 A24: for p be Prime, n be Element of NAT , m be non zero Element of NAT , X be set st X = { (p9 |^ (p9 |-count m)) where p9 be prime Element of NAT : P2[n, m, p9] } & (p |^ (p |-count m)) in X holds (p |-count ( Product ( Sgm X))) = (p |-count m) from scheme3;



 A25: for p be Prime st ( sqrt (2 * n)) < p & p <= ((2 * n) / 3) holds (p |-count n1) = 0 & (p |-count n3) = 0 & (p |-count n2) = (p |-count m)

 proof

 let p be Prime;

 assume that

 A26: ( sqrt (2 * n)) < p and

 A27: p <= ((2 * n) / 3);

 now

 assume (p |^ (p |-count m)) in X1;

 then ex p9 be prime Element of NAT st (p9 |^ (p9 |-count m)) = (p |^ (p |-count m)) & P1[n, m, p9];

 hence contradiction by A10, A26, Th22;

 end;

 hence (p |-count n1) = 0 by A10, A16;

 now

 assume (p |^ (p |-count m)) in X3;

 then ex p9 be prime Element of NAT st (p9 |^ (p9 |-count m)) = (p |^ (p |-count m)) & P3[n, m, p9];

 then n < p by A10, Th22;

 hence contradiction by A5, A27, XXREAL_0: 2;

 end;

 hence (p |-count n3) = 0 by A10, A15;



 A28: p in NAT by ORDINAL1:def 12;

 per cases ;

 suppose (p |-count m) > 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 be 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 be Prime, n be Element of NAT , m be non zero Element of NAT , X be set st X = { (p9 |^ (p9 |-count m)) where p9 be 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 be Prime st n < p & p <= (2 * n) holds (p |-count n1) = 0 & (p |-count n2) = 0 & (p |-count n3) = (p |-count m)

 proof

 let p be Prime;

 assume that

 A32: n < p and

 A33: p <= (2 * n);

 now

 assume (p |^ (p |-count m)) in X1;

 then ex p9 be prime Element of NAT st (p9 |^ (p9 |-count m)) = (p |^ (p |-count m)) & P1[n, m, p9];

 then p <= ( sqrt (2 * n)) by A10, Th22;

 hence contradiction by A7, A32, XXREAL_0: 2;

 end;

 hence (p |-count n1) = 0 by A10, A16;

 now

 assume (p |^ (p |-count m)) in X2;

 then ex p9 be prime Element of NAT st (p9 |^ (p9 |-count m)) = (p |^ (p |-count m)) & P2[n, m, p9];

 then p <= ((2 * n) / 3) by A10, Th22;

 hence contradiction by A5, A32, XXREAL_0: 2;

 end;

 hence (p |-count n2) = 0 by A10, A2;



 A34: p in NAT by ORDINAL1:def 12;

 per cases ;

 suppose (p |-count m) > 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 be 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 be Prime, n be Element of NAT , m be non zero Element of NAT , X be set st X = { (p9 |^ (p9 |-count m)) where p9 be 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 be 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 be 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 be 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 be 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 be 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 < p & p <= (2 * n);

 then (p |-count n1) = 0 & (p |-count n2) = 0 by A31, A42;

 hence thesis by A31, A42, A43, A46;

 end;

 suppose

 A47: ((2 * n) / 3) < p & p <= n;

 then

 A48: (p |-count n2) = 0 by A20, A42;

 (p |-count m) = 0 & (p |-count n1) = 0 by A1, A4, A20, A42, A47, Lm9;

 hence thesis by A20, A42, A43, A47, A48;

 end;

 suppose

 A49: ( sqrt (2 * n)) < p & p <= ((2 * n) / 3);

 then (p |-count n1) = 0 & (p |-count n2) = (p |-count m) by A25, A42;

 hence thesis by A25, A42, A43, A49;

 end;

 suppose

 A50: p <= ( sqrt (2 * n));

 then (p |-count n1) = (p |-count m) & (p |-count n2) = 0 by A37, A42;

 hence thesis by A37, A42, A43, A50;

 end;

 end;

 ( Product f1) > 0 by A10, A3;

 hence thesis by A10, A14, A12, A41, Th21;

 end;

 scheme :: NAT_4:sch4

 scheme4 { A( set, set) -> set , P[ set, set] } :

for n,m be Element of NAT , r be Real, X be finite set st X = { A(p,m) where p be prime Element of NAT : p <= r & P[p, m] } & r >= 0 holds ( card X) <= [\r/];

 let n,m be Element of NAT ;

 defpred P1[ Nat] means for n,m be Element of NAT , r be Real, X be finite set st X = { A(p,m) where p be prime Element of NAT : p <= r & P[p, m] } & r >= 0 & $1 = [\r/] holds ( card X) <= [\r/];



 A1: for n be 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 be prime Element of NAT : p <= r1 & P[p, m] };

 set X2 = { A(p,m) where p be 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 be 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 be 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 be prime Element of NAT st A(p,m) = x & r1 = 0 ;

 now

 let x be object;

 assume x in X;

 then

 consider p be 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 < p & p <= r & P[p, m] by A10;

 then x in X1 or x in X2;

 hence x in (X1 \/ X2) by XBOOLE_0:def 3;

 end;

 then X c= (X1 \/ X2);

 then

 A11: X = (X1 \/ X2) by A9, XBOOLE_0:def 10;

 then

 reconsider X1 as finite set by FINSET_1: 1, XBOOLE_1: 7;

 assume

 A12: (n + 1) = [\r/];



 then

 A13: n = ( [\r/] + ( - 1))

 .= [\(r + ( - 1))/] by INT_1: 28

 .= [\r1/];

 then

 A14: r1 >= 0 by INT_1:def 6;

 then

 A15: ( card X1) <= [\r1/] by A2, A13;

 per cases ;

 suppose not ex x be 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 be 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 < p1 & p1 <= r and P[p1, m] by A17;



 A23: p1 = [\r/] by A22, INT_1:def 6;

 ex p2 be prime Element of NAT st A(p2,m) = y & r1 < p2 & p2 <= r & P[p2, m] by A19;

 hence contradiction by A20, A21, A23, INT_1:def 6;

 end;

 per cases ;

 suppose not x in X1;

 then ( card X) = (( card X1) + 1) by A11, A18, CARD_2: 41;

 hence ( card X) <= [\r/] by A12, A13, A15, XREAL_1: 6;

 end;

 suppose x in X1;

 then X2 c= X1 by A18, ZFMISC_1: 31;

 then ( card X) <= n by A2, A13, A14, A11, XBOOLE_1: 12;

 hence ( card X) <= [\r/] by A12, A3, XXREAL_0: 2;

 end;

 end;

 end;

 hence thesis;

 end;



 A24: P1[ 0 ]

 proof

 let n,m be Element of NAT ;

 let r be Real;

 let X be finite set;

 assume

 A25: X = { A(p,m) where p be prime Element of NAT : p <= r & P[p, m] };

 assume r >= 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 be 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 be 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 be Element of NAT st m = ((2 * n) choose n) & n >= 3 holds ( Product ( Sgm { (p |^ (p |-count m)) where p be 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 be Element of NAT , r be Real, X be finite set st X = { A(k,m) where k be 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 be 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 be prime Element of NAT st (p |^ (p |-count m)) = x & p <= ( sqrt (2 * n)) & (p |-count m) > 0 ;

 then ex b be 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 be 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

 ::$Notion-Name

 theorem :: NAT_4:56

 for n be Element of NAT st n >= 1 holds ex p be 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 be prime Element of NAT : p <= ( sqrt (2 * n)) & (p |-count m) > 0 };

 set X2 = { (p |^ (p |-count m)) where p be prime Element of NAT : ( sqrt (2 * n)) 0 };

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

 assume

 A3: not ex p be 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 be 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 be 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 be 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, POWER: 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;