:: Pocklington's Theorem and {B}ertrand's Postulate
:: by Marco Riccardi
::
:: Received May 17, 2006
:: Copyright (c) 2006-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XREAL_0, CARD_1, XXREAL_0, RELAT_1, ARYTM_3, NAT_1,
NEWTON, INT_1, SUBSET_1, ARYTM_1, REALSET1, ABIAN, FINSEQ_1, FINSEQ_2,
ORDINAL4, CARD_3, FUNCT_1, INT_2, NAT_3, XBOOLE_0, PRE_POLY, POWER,
PEPIN, SQUARE_1, TARSKI, FINSET_1, MEMBERED, REAL_1, COMPLEX1, PREPOWER,
FUNCT_7, XCMPLX_0, NUMBER09;
notations SUBSET_1, XXREAL_0, PREPOWER, TARSKI, XBOOLE_0, ORDINAL1, CARD_1,
NUMBERS, XCMPLX_0, XREAL_0, INT_1, ABIAN, SQUARE_1, NEWTON, FINSET_1,
PEPIN, NAT_3, RELAT_1, FUNCT_1, FINSEQ_1, RVSUM_1, WSIERP_1, TREES_4,
XXREAL_2, POWER, MEMBERED, INT_2, FINSEQ_2, RECDEF_1, PRE_POLY, REAL_1,
NAT_1, NAT_D;
constructors REAL_1, NAT_D, PREPOWER, POWER, WSIERP_1, ABIAN, PEPIN, NAT_3,
RECDEF_1, BINOP_2, XXREAL_2, RELSET_1, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_2,
RVSUM_1, NEWTON, NAT_3, VALUED_0, VALUED_1, XXREAL_2, CARD_1, SQUARE_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, MEMBERED;
equalities FINSEQ_2, NEWTON, SQUARE_1;
expansions TARSKI, MEMBERED;
theorems TARSKI, NAT_1, NAT_2, INT_1, FINSEQ_1, CARD_1, XBOOLE_1, CARD_2,
FINSET_1, SQUARE_1, EULER_1, EULER_2, PREPOWER, POWER, ABSVALUE, NEWTON,
XCMPLX_1, ORDINAL1, XREAL_1, PEPIN, NAT_3, XBOOLE_0, INT_2, ABIAN,
FINSEQ_3, RVSUM_1, FUNCT_1, FINSEQ_2, ZFMISC_1, FUNCOP_1, PROB_3,
INTEGRA5, COMPTRIG, XXREAL_0, NAT_D, VALUED_1, XXREAL_2, PRE_POLY,
XREAL_0, NUMBERS;
schemes NAT_1, FINSEQ_1;
begin :: Some theorems on Real and Nat.
theorem Th1:
for r,s being 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 Th2:
for r,s being 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 Th3:
for a,n being Nat st a > 1 holds a|^n > n
proof
defpred P[Nat] means for a being Nat st a>1 holds a|^$1 > $1;
A1: for n being 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 being Nat holds P[n] from NAT_1:sch 2(A6,A1);
hence thesis;
end;
theorem Th4:
for n,k,m being Nat st k <= n & m = [\ n/2 /] holds n choose m >= n choose k
proof
defpred P[Nat] means for k,m being Nat st k <= m & m = [\ $1/2 /] holds $1
choose m >= $1 choose k;
A1: 1/2 - 1 < 0;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: P[n];
for k,m1 being 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;
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
n is not 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
.= 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
XREAL_1:72;
then (n-k+1)/([\ n/2 /]+1)>=1 by 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];
A37: for n being Nat holds P[n] from NAT_1:sch 2(A35,A2);
for n,k,m being 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 /];
hence thesis by A37,A39,A41,A42,A44;
end;
suppose
n is not 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 Th5:
for n,m being 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 being 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;
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;
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 Th6:
for n being 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;
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,NEWTON:9;
end;
end;
theorem Th7:
for n,p being Nat holds p > 0 & n divides p & n <> 1 & n <> p
implies 1 < n & n < p
proof
let n,p be Nat;
assume
A1: p>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 Th8:
for p being Nat holds
(ex n being Element of NAT st n divides p & 1 < n & n < p)
implies ex n being 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 Th9:
for j,k,l being Nat st 0 < l < j holds not j divides j*k+l
proof
let j,k,l be Nat;
set i = j*k+l;
assume that
A3: 0<l and
A2: l<j;
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 A2,NAT_D:def 1;
hence contradiction by A3;
end;
theorem
for n,q,b being 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 Th11:
for a,b,c being 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 NAT_D:67;
hence thesis;
end;
theorem Th12:
for p being Nat holds not p is prime iff
p <= 1 or ex n being 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 being 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 Th13:
for n,k being Nat st n divides k & 1 < n
ex p being 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 being Nat holds not p is prime iff p<=1 or ex n being 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 being 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 being Element of NAT st n divides p & 1<n & n*n<=p;
then consider n being 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 Th14:
for p being Nat holds p is prime iff p > 1 &
for n being 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 being Element of NAT holds not (1<n & n*n<=p & n is prime)
or not n divides p;
then
for n being 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 Th15:
for a,p,k being 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 being 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;
then p*0 mod p = 1 by A2,NEWTON:11;
hence contradiction;
end;
theorem Th16:
for p being Prime, a being Element of NAT st a <> 0 holds
1 <= p |^ (p |-count a) <= a
proof
let p be Prime, a be Element of NAT;
assume
A1: a<>0;
set x = p |^ (p |-count a);
p >= 1 by INT_2:def 4;
hence 1 <= x by PREPOWER:11;
p <> 1 by INT_2:def 4;
then x divides a by A1,NAT_3:def 7;
hence thesis by A1,NAT_D:7;
end;
theorem Th17:
for k,q,n,d being 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 being 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 being Nat holds P[n] implies P[n+1]
proof
let n be Nat;
assume
A2: for k,q,d being 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 being 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 being Nat holds P[n] from NAT_1:sch 2(A12,A1);
hence thesis;
end;
theorem Th18:
for q1,q,n1 being 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 Th19:
for p being Prime, n being Nat st n < p holds not p divides n!
proof
defpred P[Nat] means for p being Prime st $1<p holds not p divides $1!;
let p be Prime;
let n be Nat;
assume
A1: n<p;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: P[n];
for p being 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 being Nat holds P[n] from NAT_1:sch 2(A6,A2);
hence thesis by A1;
end;
theorem Th20:
for a,b being non zero Nat holds
(for p being Element of NAT st p is prime holds p |-count a <= p |-count b)
implies ex c being Element of NAT st b = a*c
proof
A1: for a,a1,b,b1 being non zero Nat, x being Prime st (for p being
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 being 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 being 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 being non zero Nat, x being Prime holds a div (x|^(x|-count a))
is non zero Nat
proof
let a be non zero Nat;
let x be Prime;
assume
A13: not a div (x|^(x|-count a)) is non zero Nat;
set xca=x|^(x|-count a);
x>1 by INT_2:def 4;
then
A14: xca divides a by NAT_3:def 7;
ex t being Nat st a = xca * (0 qua Nat) + t & t < xca by A13,NAT_D:def 1;
hence contradiction by A14,NAT_D:7;
end;
defpred P[Nat] means for a,b being non zero Nat st card(support
pfexp b)=$1 holds (for p being Element of NAT st p is prime holds p |-count a
<= p |-count b) implies (ex c being Element of NAT st b=a*c);
let a,b be non zero Nat;
assume
A15: for p being Element of NAT st p is prime holds p |-count a <= p |-count b;
A16: ex n1 being Element of NAT st n1=card(support pfexp b);
A17: for n1,n2 being non zero Nat st n1 divides n2 holds (n2 div n1)*n1 = n2
proof
let n1,n2 be non zero Nat;
assume n1 divides n2;
then ex a being Nat st n2=n1*a by NAT_D:def 3;
hence thesis;
end;
A18: for b,b1 being non zero Nat, x being Prime, n being Element of NAT st
card(support pfexp b)=n+1 & b1=b div (x|^(x|-count b)) & x in support pfexp b
holds card(support pfexp b1)=n
proof
let b,b1 be non zero Nat;
let x be Prime;
let n be Element of NAT;
assume
A19: card(support pfexp b)=n+1;
set xcb=x|-count b;
assume
A20: b1=b div (x|^(x|-count b));
A21: x>1 by INT_2:def 4;
then x|^xcb divides b by NAT_3:def 7;
then
A22: b=b1*x|^xcb by A17,A20;
reconsider b1 as Element of NAT by ORDINAL1:def 12;
A23: b1,x are_coprime
proof
assume not b1,x are_coprime;
then b1 gcd x = x by PEPIN:2;
then x divides b1 by NAT_D:def 5;
then consider c be Nat such that
A24: b1=x*c by NAT_D:def 3;
A25: not x|^(xcb+1) divides b by A21,NAT_3:def 7;
x|^xcb divides b by A21,NAT_3:def 7;
then b = x*c*x|^xcb by A17,A20,A24
.= c*(x|^xcb*x)
.= c*x|^(xcb+1) by NEWTON:6;
hence contradiction by A25,NAT_D:def 3;
end;
assume x in support pfexp b;
then (pfexp b).x<>0 by PRE_POLY:def 7;
then
A26: xcb<>0 by NAT_3:def 8;
reconsider b1 as non zero Nat;
card support pfexp (x|^xcb*b1) = card support pfexp x|^xcb + card
support pfexp b1 by A23,EULER_2:17,NAT_3:47;
then n+1=card {x} + card support pfexp b1 by A19,A22,A26,NAT_3:42;
then n+1=1+card (support pfexp b1) by CARD_2:42;
hence thesis;
end;
A27: for n being Nat holds P[n] implies P[n+1]
proof
let n be Nat;
assume
A28: P[n];
for a,b being non zero Nat st card(support pfexp b)=n+1 holds (for p
being Element of NAT st p is prime holds p |-count a <= p |-count b) implies ex
c being Element of NAT st b=a*c
proof
let a,b be non zero Nat;
assume
A29: card(support pfexp b)=n+1;
then support pfexp b<>{};
then consider x being object such that
A30: x in support pfexp b;
reconsider x as Prime by A30,NAT_3:34;
set a1=a div (x|^(x|-count a));
set b1=b div (x|^(x|-count b));
reconsider a1,b1 as non zero Nat by A12;
assume
A31: for p being Element of NAT st p is prime holds p |-count a <= p
|-count b;
then
A32: for p being Element of NAT st p is prime holds p |-count a1 <= p
|-count b1 by A1;
set xca=x|-count a;
set xcb=x|-count b;
x in NAT by ORDINAL1:def 12;
then
A33: xcb-xca=xcb-'xca by A31,XREAL_1:233;
n in NAT by ORDINAL1:def 12;
then card(support pfexp b1)=n by A18,A29,A30;
then consider d be Element of NAT such that
A34: b1=a1*d by A28,A32;
reconsider e=d*x|^(xcb-'xca) as Element of NAT by ORDINAL1:def 12;
take e;
A35: x<>1 by INT_2:def 4;
then
A36: x|^(xca) divides a by NAT_3:def 7;
x|^(xcb) divides b by A35,NAT_3:def 7;
then b = d*(a div (x|^xca))*(x|^(xca+(xcb-'xca))) by A17,A34,A33
.= d*(a div (x|^xca))*(x|^xca*x|^(xcb-'xca)) by NEWTON:8
.= d*((a div (x|^xca))*x|^xca)*x|^(xcb-'xca)
.= d*a*x|^(xcb-'xca) by A17,A36
.= a*(d*x|^(xcb-'xca));
hence thesis;
end;
hence thesis;
end;
A37: P[0]
proof
let a,b be non zero Nat;
assume
A38: card support pfexp b=0;
(for p being Element of NAT st p is prime holds p |-count a <= p
|-count b) implies ex c being Element of NAT st b=a*c
proof
set d=1;
assume
A39: for p being Element of NAT st p is prime holds p |-count a <= p
|-count b;
take d;
A40: (support pfexp b)={} by A38;
(support pfexp a)={}
proof
assume (support pfexp a)<>{};
then consider x be object such that
A41: x in support pfexp a;
reconsider x as Prime by A41,NAT_3:34;
reconsider x as prime Element of NAT by ORDINAL1:def 12;
(pfexp a).x<>0 by A41,PRE_POLY:def 7;
then x|-count a<>0 by NAT_3:def 8;
then x|-count b>0 by A39;
then (pfexp b).x<>0 by NAT_3:def 8;
hence contradiction by A40,PRE_POLY:def 7;
end;
then a=1 by NAT_3:52;
hence thesis by A40,NAT_3:52;
end;
hence thesis;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A37,A27);
hence thesis by A15,A16;
end;
theorem Th21:
for a,b being non zero Nat holds
(for p being Element of NAT st p is prime holds p |-count a = p |-count b)
implies a = b
proof
let a,b be non zero Nat;
assume
A1: for p being Element of NAT st p is prime holds p |-count a = p |-count b;
then
for p being Element of NAT st p is prime holds p |-count a <= p |-count b;
then consider c being Element of NAT such that
A2: b=a*c by Th20;
for p being Element of NAT st p is prime holds p |-count b <= p |-count
a by A1;
then consider d being Element of NAT such that
A3: a=b*d by Th20;
a=a*(c*d) by A2,A3;
then c = 1 by NAT_1:15,XCMPLX_1:7;
hence thesis by A2;
end;
theorem Th22:
for p1,p2 being Prime, m being non zero Element of NAT st
p1|^(p1 |-count m) = p2|^(p2 |-count m) & p1 |-count m > 0 holds p1 = p2
proof
let p1,p2 be Prime;
let m be non zero Element of NAT;
assume
A1: p1|^(p1 |-count m) = p2|^(p2 |-count m);
A2: p1 > 1 by INT_2:def 4;
assume p1 |-count m > 0;
then p1 to_power (p1 |-count m) > 1 by A2,POWER:35;
then
A3: p1|^(p1|-count m) > 1 by POWER:41;
assume p1 <> p2;
then p1 <> 1 & not p1 divides p2|^(p2 |-count m) by INT_2:def 4,NAT_3:6;
then p1 |-count (p1|^(p1 |-count m)) = 0 by A1,NAT_3:27;
then p1 |-count m = 0 by A2,NAT_3:25;
hence contradiction by A3,NEWTON:4;
end;
begin :: Pocklington's theorem.
theorem Th23:
for n,k,q,p,n1,p,a being Element of NAT st n-1 = k*q|^n1 & k > 0 &
n1 > 0 & q is prime & a|^(n-'1) mod n = 1 & p is prime & p divides n holds
p divides (a|^((n-'1) div q) -' 1) or p mod q|^n1 = 1
proof
let n,k,q,p,n1,p,a be Element of NAT;
assume that
A1: n-1=k*q|^n1 and
A2: k>0 and
A3: n1>0 and
A4: q is prime;
A5: n-1+1 > 0+1 by A1,A2,A4,XREAL_1:6;
assume
A6: a|^(n-'1) mod n = 1;
a|^((n-'1) div q)>=1
proof
assume a|^((n-'1) div q)<1;
then
A7: a=0 by NAT_1:14;
n-'1 + 1 > 1 by A5,XREAL_1:233;
then n-'1 >= 1 by NAT_1:13;
then a|^(n-'1) mod n = 0*n mod n by A7,NEWTON:11
.= 0;
hence contradiction by A6;
end;
then
A8: a|^((n-'1) div q)-'1=a|^((n-'1) div q)-1 by XREAL_1:233;
n1+1 > 0+1 by A3,XREAL_1:6;
then n1>=1 by NAT_1:13;
then
A9: n1-'1=n1-1 by XREAL_1:233;
then
A10: (n-'1) div q = (q|^(n1-'1+1))*k div q by A1,A5,XREAL_1:233
.=q*q|^(n1-'1)*k div q by NEWTON:6
.=q*(q|^(n1-'1)*k) div q
.=k*q|^(n1-'1) by A4,NAT_D:18;
assume that
A11: p is prime and
A12: p divides n;
consider i being Nat such that
A13: n=p*i by A12,NAT_D:def 3;
assume not p divides (a|^((n-'1) div q)-'1);
then
A14: not a|^((n-'1) div q) mod p = 1 by A11,A8,PEPIN:8;
set nn=n-'1;
n1+1 > 0+1 by A3,XREAL_1:6;
then n1>=1 by NAT_1:13;
then
A15: n1-'1=n1-1 by XREAL_1:233;
A16: p > 1 by A11,INT_2:def 4;
then p-'1=p-1 by XREAL_1:233;
then
A17: p-'1+1=p;
reconsider i as Element of NAT by ORDINAL1:def 12;
i*p<>0 by A1,A13;
then
A18: a|^(n-'1) mod p = 1 by A6,A16,A13,PEPIN:9;
0+1<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 Th24:
for n,f,c being Element of NAT st n-1 = f*c & f > c & c > 0 &
(for q being Element of NAT st q divides f & q is prime
ex a being Element of NAT st a|^(n-'1) mod n = 1 &
(a|^((n-'1) div q)-'1) gcd n = 1)
holds n is prime
proof
let n,f,c be Element of NAT;
assume that
A1: n-1=f*c and
A2: f>c and
A3: c>0;
A4: n-1+1>0+1 by A1,A2,A3,XREAL_1:6;
assume
A5: for q being Element of NAT st q divides f & q is prime holds ex a
being Element of NAT st a|^(n-'1) mod n = 1 & (a|^((n-'1) div q)-'1) gcd n = 1;
assume not n is prime;
then consider p be Element of NAT such that
A6: p divides n and
A7: 1<p and
A8: p*p<=n and
A9: p is prime by A4,Lm1;
A10: p-1=p-'1 by A7,XREAL_1:233;
A11: p-1>1-1 by A7,XREAL_1:9;
then
A12: p-'1>0 by A7,XREAL_1:233;
A13: for q1 being Element of NAT st q1 in support (pfexp f) & q1 |-count f >
0 holds p mod q1|^(q1 |-count f) = 1
proof
let q1 be Element of NAT;
set n1=q1 |-count f;
assume
A14: q1 in support (pfexp f);
then
A15: q1 is prime by NAT_3:34;
A16: q1 is prime by A14,NAT_3:34;
then consider a be Element of NAT such that
A17: a|^(n-'1) mod n = 1 and
A18: (a|^((n-'1) div q1)-'1) gcd n = 1 by A5,A14,NAT_3:36;
assume
A19: q1 |-count f > 0;
A20: not p divides (a|^((n-'1) div q1)-'1)
by A6,NEWTON:50,A7,A18,NAT_D:7;
q1<>1 by A16,INT_2:def 4;
then q1|^(q1 |-count f) divides f by A2,NAT_3:def 7;
then consider d be Nat such that
A21: f=q1|^n1*d by NAT_D:def 3;
reconsider d as Element of NAT by ORDINAL1:def 12;
set k=d*c;
A22: k>0
proof
assume k<=0;
then d=0 by A3;
hence contradiction by A2,A21;
end;
n-1=k*q1|^n1 by A1,A21;
hence thesis by A6,A9,A19,A17,A22,A15,A20,Th23;
end;
for q1 being Element of NAT st q1 is prime holds q1 |-count f <= q1
|-count (p-'1)
proof
let q1 be Element of NAT;
assume
A23: q1 is prime;
per cases;
suppose
A24: q1 in support (pfexp f);
then (pfexp f).q1<>0 by PRE_POLY:def 7;
then q1 |-count f>0 by A23,NAT_3:def 8;
then p mod q1|^(q1 |-count f) = 1 by A13,A24;
then
A25: q1 |-count (q1|^(q1 |-count f)) <= q1 |-count (p-'1) by A11,A10,A23,
NAT_3:30,PEPIN:8;
q1>1 by A23,INT_2:def 4;
hence thesis by A25,NAT_3:25;
end;
suppose
not q1 in support (pfexp f);
then (pfexp f).q1=0 by PRE_POLY:def 7;
hence thesis by A23,NAT_3:def 8;
end;
end;
then ex n2 being Element of NAT st (p-'1)=f*n2 by A2,A12,Th20;
then f divides (p-'1) by NAT_D:def 3;
then f<=(p-'1) by A12,NAT_D:7;
then p-1+1>=f+1 by A10,XREAL_1:6;
then p>f by NAT_1:13;
then
A26: p^2>f^2 by SQUARE_1:16;
c>=0+1 by A3,NAT_1:13;
then
A27: c+1>=1+1 by XREAL_1:6;
f>=c+1 by A2,NAT_1:13;
then f>=2 by A27,XXREAL_0:2;
then f-1>=2-1 by XREAL_1:9;
then
A28: n+(f-1)>=n+1 by XREAL_1:6;
f>=c+1 by A2,NAT_1:13;
then f*f>=f*(c+1) by XREAL_1:64;
then p^2>f+(n-1) by A1,A26,XXREAL_0:2;
then p^2>=n+1 by A28,XXREAL_0:2;
hence contradiction by A8,NAT_1:13;
end;
::$N Pocklington's theorem
::$L https://en.wikipedia.org/wiki/Pocklington_primality_test Pocklington's theorem
theorem Th25:
for n,f,d,n1,a,q being Element of NAT st n-1 = q|^n1*d & q|^n1 > d &
d > 0 & q is prime & a|^(n-'1) mod n = 1 & (a|^((n-'1) div q)-'1) gcd n = 1
holds n is prime
proof
let n,f,d,n1,a,q be Element of NAT;
assume that
A1: n-1=q|^n1*d & q|^n1>d & d>0 and
A2: q is prime;
set f=q|^n1;
assume
A3: a|^(n-'1) mod n = 1;
assume
A4: (a|^((n-'1) div q)-'1) gcd n = 1;
for q1 being Element of NAT st q1 divides f & q1 is prime holds ex a
being Element of NAT st a|^(n-'1) mod n = 1 & (a|^((n-'1) div q1)-'1) gcd n = 1
proof
let q1 be Element of NAT;
assume
A5: q1 divides f;
assume
A6: q1 is prime;
consider a be Element of NAT such that
A7: a|^(n-'1) mod n = 1 & (a|^((n-'1) div q)-'1) gcd n = 1 by A3,A4;
take a;
thus thesis by A2,A5,A6,A7,Th18;
end;
hence thesis by A1,Th24;
end;
Lm2: for n being Nat st n<5 & n is prime holds n=2 or n=3
proof
let n be Nat;
assume that
A1: n<5 and
A2: n is prime;
1 < n by A2,INT_2:def 4;
then 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 being Nat st k<25 holds for n being Nat st
n*n<=k & n is prime holds n=2 or n=3
proof
let k be Nat;
assume
A1: k<25;
let n be Nat;
assume that
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 A4,Lm2;
end;
begin :: Some prime numbers.
theorem 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
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 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
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 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 being Nat st 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 Nat;
assume that
A2: n<29 and
A3: n is prime;
A1: 1<n by A3,INT_2:def 4;
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 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 being Nat st k<841 holds for n being Nat st
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 Nat;
assume
A1: k<841;
let n be Nat;
assume that
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 A4,Lm5;
end;
theorem 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 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 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 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 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 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 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 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,NAT_D:67
.= 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
.= (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,NAT_D:66
.= 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 NAT_D:67
.= (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,NAT_D:67
.= (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,NAT_D:67
.=(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,NAT_D:67
.=(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,NAT_D:67
.=(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 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,NAT_D:67
.= 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
.= (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,NAT_D:66
.= 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 NAT_D:67
.= (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,NAT_D:67
.= (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,NAT_D:67
.= (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,NAT_D:67
.= (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,NAT_D:67
.=(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 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,NAT_D:67
.= (3906*(2|^256*2|^32 mod 4001)) mod 4001 by NEWTON:8
.= (3906*(1522*1823 mod 4001)) mod 4001 by A26,A29,NAT_D:67
.= 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
.= (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,NAT_D:66
.= 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 NAT_D:67
.=(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,NAT_D:67
.=(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,NAT_D:67
.=(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,NAT_D:67
.=(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,NAT_D:67
.=(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 being Element of NAT st 1<=n & n<4001
ex p being Prime st n<p & p<=2*n
proof
let n be Element of NAT;
A1: for a,n,p being 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 :: Some theorems on finite sequence of numbers.
::$CT
theorem Th41:
for F being FinSequence of REAL st
(for k being Element of NAT st k in dom F holds F.k > 0) holds Product F > 0
proof
defpred P[Nat] means for F being FinSequence of REAL st (for k
being Element of NAT st k in dom F holds F.k > 0) & len F = $1 holds Product F
> 0;
let F be FinSequence of REAL;
A1: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
for F being FinSequence of REAL st (for k being Element of NAT st k in
dom F holds F.k > 0) & len F = n+1 holds Product F > 0
proof
let F be FinSequence of REAL;
assume
A3: for k being Element of NAT st k in dom F holds F.k > 0;
assume
A4: len F = n+1;
then consider F1,F2 being FinSequence of REAL such that
A5: len F1 = n and
A6: len F2 = 1 and
A7: F=F1^F2 by FINSEQ_2:23;
1 in Seg 1 by FINSEQ_1:3;
then 1 in dom F2 by A6,FINSEQ_1:def 3;
then
A8: F.(n+1) = F2.1 by A5,A7,FINSEQ_1:def 7;
for k being Element of NAT st k in dom F1 holds F1.k > 0
proof
let k be Element of NAT;
assume
A9: k in dom F1;
then F.k > 0 by A3,A7,FINSEQ_2:15;
hence thesis by A7,A9,FINSEQ_1:def 7;
end;
then
A10: Product F1 > 0 by A2,A5;
set x=F2.1;
Seg (n+1) = dom F by A4,FINSEQ_1:def 3;
then
A11: x > 0 by A3,A8,FINSEQ_1:3;
Product F = Product (F1^<*x*>) by A6,A7,FINSEQ_1:40
.= Product F1 * x by RVSUM_1:96;
hence thesis by A10,A11;
end;
hence thesis;
end;
A12: P[0] proof let F be FinSequence of REAL such that
for k being Element of NAT st k in dom F holds F.k > 0;
assume len F = 0;
then F = <*>REAL;
hence thesis by RVSUM_1:94;
end;
A13: for n being Nat holds P[n] from NAT_1:sch 2(A12,A1);
A14: ex n being Element of NAT st n = len F;
assume for k being Element of NAT st k in dom F holds F.k > 0;
hence thesis by A13,A14;
end;
theorem Th42:
for X1 being set, X2 being finite set st X1 c= X2 & X2 c= NAT &
not {} in X2 holds Product Sgm X1 <= Product Sgm X2
proof
let X1 be set;
defpred P[Nat] means for X1 being set, X2 being finite set st X1
c= X2 & X2 c= NAT & (not {} in X2) & card X2 = $1 holds Product Sgm X1 <=
Product Sgm X2;
A1: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
now
let X1 be set;
let X2 be finite set;
assume that
A3: X1 c= X2 and
A4: X2 c= NAT and
A5: not {} in X2 and
A6: card X2 = n+1;
set A=X2;
reconsider A as finite non empty real-membered set by A4,A6;
set m = max A;
set X11=X1 \ {m};
set X12=X2 \ {m};
A7: m in X2 by XXREAL_2:def 8;
then
A8: X12 \/ {m} = X2 by ZFMISC_1:116;
A9: X12 /\ {m} = (X2 /\ {m}) \ {m} by XBOOLE_1:49
.= {m} \ {m} by A7,ZFMISC_1:46
.= {} by XBOOLE_1:37;
card(X12\/{m})=card X12 + card {m} - card(X12 /\{m}) by CARD_2:45;
then
A10: card X2 = card X12 + 1 - card {} by A8,A9,CARD_1:30;
reconsider m as Element of NAT by A4,A7;
A11: X11 c= X12 by A3,XBOOLE_1:33;
A12: X12 c= X2 by XBOOLE_1:36;
then
A13: X12 c= NAT & not {} in X12 by A4,A5;
then
A14: Product Sgm X11 <= Product Sgm X12 by A2,A3,A6,A10,XBOOLE_1:33;
now
let x be object;
set r=x;
assume
A15: x in X12;
then x in A by A12;
then reconsider r as Element of NAT by A4;
not r=0 by A5,A12,A15;
then 0+1 < r+1 by XREAL_1:6;
then
A16: 1 <= r by NAT_1:13;
r <= m by A12,A15,XXREAL_2:def 8;
hence x in Seg m by A16,FINSEQ_1:1;
end;
then X12 c= Seg m;
then
a17: X12 is included_in_Seg by FINSEQ_1:def 13;
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 {m} c= Seg m by ZFMISC_1:31;
then
a20: {m} is included_in_Seg by FINSEQ_1:def 13;
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 X11 c= Seg m;
then
a34: X11 is included_in_Seg by FINSEQ_1:def 13;
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 being Element of NAT st card X2 = n;
A37: P[0]
proof
let X1 be set;
let X2 be finite set;
assume that
A38: X1 c= X2 and
X2 c= NAT and
not {} in X2 and
A39: card X2 = 0;
X2={} by A39;
hence thesis by A38,XBOOLE_1:3;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A37,A1);
hence thesis by A35,A36;
end;
theorem Th43:
for a being Element of NAT, X being included_in_Seg set,
F being FinSequence of SetPrimes, p being Prime st
X c= SetPrimes & 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 be Element of NAT, X be included_in_Seg set,
F be FinSequence of SetPrimes,
p be Prime;
defpred P[Nat] means for a being Element of NAT, X being included_in_Seg set,
F being FinSequence of SetPrimes, p being Prime st X c= SetPrimes &
F = Sgm X & a = Product F & len F = $1 holds (p in rng F implies p |-count a =
1) & (not( p in rng F) implies p |-count a = 0);
now
let F be FinSequence of SetPrimes;
rng F c= REAL;
hence F is FinSequence of REAL by FINSEQ_1:def 4;
end;
then reconsider F as FinSequence of REAL;
A1: ex n being Element of NAT st n = len F;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: P[n];
for a being Element of NAT, X being included_in_Seg set,
F being FinSequence of
SetPrimes, p being Prime st X c= SetPrimes & 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 be Element of NAT, X be included_in_Seg set,
F be FinSequence of SetPrimes, p be Prime;
assume that
A4: X c= SetPrimes 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;
A13: rng F = X by A6,FINSEQ_1:def 14;
A15: for m1,n1 being Nat st m1 in X1 & n1 in {x} holds m1 < n1
proof
set n9=n+1;
let m1,n1 be Nat;
assume that
A16: m1 in X1 and
A17: n1 in {x};
set l=(F").m1;
A18: F is one-to-one by 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 A6,A8,A21,A23,A22,FINSEQ_1:def 14;
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,A15,FINSEQ_3:42;
then rng F c= SetPrimes & rng F1 c= rng F by FINSEQ_1:29,def 4;
then
A28: rng F1 c= SetPrimes;
len F = len F1 + len F2 by A27,FINSEQ_1:22;
then
A29: n+1=len F1 + 1 by A8,A24,FINSEQ_1:39;
reconsider F1 as FinSequence of SetPrimes by A28,FINSEQ_1:def 4;
A30: F1 is FinSequence of REAL by FINSEQ_2:24,NUMBERS:19;
now
let k be Element of NAT;
assume k in dom F1;
then F1.k in rng F1 by FUNCT_1:def 3;
then F1.k is Prime by A28,NEWTON:def 6;
hence F1.k>0;
end;
then
A31: a1<>0 by Th41,A30;
Product F = Product (F1^F2) by A6,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 FINSEQ_1:def 14;
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,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,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,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 be Element of NAT, X be included_in_Seg set,
F be FinSequence of SetPrimes, p be Prime;
assume that
X c= SetPrimes and
F = Sgm X and
A44: a = Product F and
A45: len F = 0;
A46: F=<*>REAL by A45;
assume
A47: not(p in rng F implies p |-count a = 1) or not(not p in rng F
implies p |-count a = 0);
per cases by A47;
suppose
not(p in rng F implies p |-count a = 1);
hence contradiction by A46;
end;
suppose
A48: not(not p in rng F implies p |-count a = 0);
F = <*>SetPrimes by A45;
then a=1 & p<>1 by A44,INT_2:def 4,RVSUM_1:94;
hence contradiction by A48,NAT_3:21;
end;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A43,A2);
hence thesis by A1;
end;
theorem Th44:
for n being Element of NAT holds
Product Sgm {p where p is prime Element of NAT: p <= n+1} <= 4 to_power n
proof
defpred P[Nat] means Product Sgm{p where p is prime Element of NAT:p<=$1+1}
<=(4 to_power $1);
let n be Element of NAT;
A1: for m being Nat st (for n being Nat st n < m holds P[n]) holds P[m]
proof
let m be Nat;
assume
A2: for n being Nat st n < m holds P[n];
per cases by XXREAL_0:1;
suppose
A3: m<1;
A4: now
assume {p where p is prime Element of NAT:p<=0+1}<>{};
then consider y being object such that
A5: y in {p where p is prime Element of NAT:p<=1} by XBOOLE_0:def 1;
ex y9 being prime Element of NAT st y9=y & y9<=1 by A5;
hence contradiction by Lm1;
end;
m=0 by A3,NAT_1:14;
hence thesis by A4,FINSEQ_3:43,POWER:24,RVSUM_1:94;
end;
suppose
A6: m=1;
A7: 4 to_power 1=4 by POWER:25;
A8: now
let y be object;
assume y in {p where p is prime Element of NAT:p<=2};
then consider y9 being prime Element of NAT such that
A9: y9=y & y9<=2;
y9>1 by Lm1;
then y9>=1+1 by NAT_1:13;
hence y=2 by A9,XXREAL_0:1;
end;
for y being object st y = 2 holds y in {p where p is prime Element of
NAT:p<=2} by INT_2:28;
then
A10: {p where p is prime Element of NAT:p<=2}={2} by A8,TARSKI:def 1;
Product Sgm{2}=Product <*2*> by FINSEQ_3:44
.=2;
hence thesis by A6,A10,A7;
end;
suppose
A11: m>1;
per cases;
suppose
m+1 is odd;
then consider k being Nat such that
A12: m+1=2*k+1 by ABIAN:9;
A13: (2*k+1) choose k<=2 to_power (2*k)
proof
defpred Q[Nat] means (2*$1+1) choose $1<=2 to_power (2*$1
);
A14: for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
set r=2*k+1-k;
set r9=2*k+3-(k+1);
set r99=k+1;
A15: 2*((2 to_power (2*k))*2)= 2*((2 to_power (2*k))*(2 to_power
1)) by POWER:25
.= 2*(2 to_power (2*k+1)) by POWER:27
.= (2 to_power 1)*(2 to_power (2*k+1)) by POWER:25
.= (2 to_power (1+2*k+1)) by POWER:27;
A16: k+1>=0;
then reconsider r as Element of NAT;
A17: 2*k+1-k+k>=0+k by A16,XREAL_1:6;
2*k+3<2*k+4 by XREAL_1:6;
then (2*k+3)/(k+2)<(2*(k+2))/(k+2) by XREAL_1:74;
then (2*k+3)/(k+2)<2*((k+2)/(k+2)) by XCMPLX_1:74;
then
A18: (2*k+3)/(k+2)<2*1 by XCMPLX_1:60;
assume (2*k+1) choose k<=2 to_power (2*k);
then ((2*k+1) choose k)*((2*k+3)/(k+2))<=(2 to_power (2*k))*2 by
A18,XREAL_1:66;
then
A19: 2*(((2*k+1) choose k)*((2*k+3)/(k+2)))<=2*((2 to_power (2*k
))*2) by XREAL_1:64;
A20: k+2>=0;
then reconsider r9 as Element of NAT;
(r99!)*(r9!) = (k!)*(k+1)*((r+1)!) by NEWTON:15
.=(k!)*(k+1)*((r!)*(r+1)) by NEWTON:15
.=(k!)*(r!)*(k+1)*(r+1);
then
A21: ((k!)*(r!))/((r99!)*(r9!)) =((k!)*(r!))/(((k!)*(r!))*((k+1)*
(r+1)))
.=((k!)*(r!))/((k!)*(r!))/((k+1)*(r+1)) by XCMPLX_1:78
.= 1/((k+1)*(r+1)) by XCMPLX_1:60;
A22: (2*k+1)! = (2*k+1)!/((k!)*(r!))*((k!)*(r!)) by XCMPLX_1:87
.=((2*k+1) choose k)*((k!)*(r!)) by A17,NEWTON:def 3;
2*k+3-r99+r99>=0+r99 by A20,XREAL_1:6;
then
(2*(k+1)+1) choose (k+1) = (2*k+2+1)!/((r99!)*(r9!)) by NEWTON:def 3
.= (((2*k+1+1)!)*(2*k+3))/((r99!)*(r9!)) by NEWTON:15
.= (((2*k+1)!)*(2*k+2)*(2*k+3))/((r99!)*(r9!)) by NEWTON:15
.= ((2*k+2)*(2*k+3))*((2*k+1)!)/((r99!)*(r9!))
.= 2*(k+1)*(2*k+3)* ((((2*k+1) choose k)* ((k!)*(r!))/((r99!)*
(r9!)))) by A22,XCMPLX_1:74
.= 2*(k+1)*(2*k+3)*(((2*k+1) choose k)* ((((k!)*(r!))/((r99!)*
(r9!))))) by XCMPLX_1:74
.= 2*(k+1)*(2*k+3)*((2*k+1) choose k)*(1/((k+1)*(r+1))) by A21
.= (2*((2*k+1) choose k))* ((k+1)*(2*k+3))/((k+1)*(r+1)) by
XCMPLX_1:99
.= (2*((2*k+1) choose k))*(((k+1)*(2*k+3))/((k+1)*(r+1))) by
XCMPLX_1:74
.= 2*((2*k+1) choose k)*(((k+1)/(k+1))*((2*k+3)/(r+1))) by
XCMPLX_1:76
.= 2*((2*k+1) choose k)*(1*((2*k+3)/(r+1))) by XCMPLX_1:60
.= 2*((2*k+1) choose k)*((2*k+3)/(k+2));
hence thesis by A15,A19;
end;
(2*0+1) choose 0 = 1 by NEWTON:19;
then
A23: Q[0] by POWER:24;
for k being Nat holds Q[k] from NAT_1:sch 2(A23,A14);
hence thesis;
end;
set Y={p where p is prime Element of NAT:p>k+1 & p<=2*k+1};
set SY = Sgm Y;
A24: rng SY c= REAL;
set X={p where p is prime Element of NAT:p<=k+1};
set SX = Sgm X;
rng SX c= REAL;
then reconsider SX as FinSequence of REAL by FINSEQ_1:def 4;
m/2=(k*2)/2 by A12;
then
A25: Product SX<=(4 to_power k) by A2,A11,XREAL_1:216;
for y being object holds y in X implies y in Seg (k+1)
proof
let y be object;
assume y in X;
then
A26: ex y9 being prime Element of NAT st y9=y & y9<=k+1;
then reconsider y as prime Element of NAT;
y>=1 by Lm1;
hence thesis by A26,FINSEQ_1:1;
end;
then X c= Seg (k+1);
then
a27: X is included_in_Seg by FINSEQ_1:def 13;
for k9 being Element of NAT st k9 in dom SX holds SX.k9 > 0
proof
let k9 be Element of NAT;
assume
A28: k9 in dom SX;
rng SX = X by a27,FINSEQ_1:def 14;
then SX.k9 in X by A28,FUNCT_1:3;
then ex y9 being prime Element of NAT st y9=SX.k9 & y9<=k+1;
hence thesis;
end;
then
A29: 0<=Product SX by Th41;
reconsider SY as FinSequence of REAL by A24,FINSEQ_1:def 4;
A30: for a,b being Nat st a in X & b in Y holds a < b
proof
let a,b be Nat;
assume a in X;
then
A31: ex y9 being prime Element of NAT st y9=a & y9<=k+1;
assume b in Y;
then
ex y99 being prime Element of NAT st y99=b & y99>k+1 & y99<=2*k +1;
hence thesis by A31,XXREAL_0:2;
end;
for y being object holds y in Y implies y in Seg (2*k+1)
proof
let y be object;
assume y in Y;
then
A32: ex y9 being prime Element of NAT st y9=y & y9>k+1 & y9<=2*k+1;
then reconsider y as prime Element of NAT;
y>=1 by Lm1;
hence thesis by A32,FINSEQ_1:1;
end;
then Y c= Seg (2*k+1);
then
a33: Y is included_in_Seg by FINSEQ_1:def 13;
A34: for k9 being Element of NAT st k9 in dom SY holds SY.k9 > 0
proof
let k9 be Element of NAT;
assume
A35: k9 in dom SY;
rng SY = Y by a33,FINSEQ_1:def 14;
then SY.k9 in Y by A35,FUNCT_1:3;
then
ex y9 being prime Element of NAT st y9=SY.k9 & y9>k+1 & y9<=2*k +1;
hence thesis;
end;
A36: Product SY<=(2*k+1) choose k
proof
set r=2*k+1-k;
set b=(2*k+1) choose k;
reconsider SY as FinSequence of NAT;
set a=Product SY;
A37: k+1>=0;
then reconsider r as Element of NAT;
A38: 2*k+1-k+k>=0+k by A37,XREAL_1:6;
then
b = (2*k+1)!/((k!)*(r!)) by NEWTON:def 3;
then A39: b>0;
A40: for p being Element of NAT st p is prime holds p |-count a <= p
|-count b
proof
now
let y be object;
assume y in Y;
then
ex y9 being prime Element of NAT st y9=y & y9>k+1 & y9<=2*k +1;
hence y in SetPrimes by NEWTON:def 6;
end;
then Y c= SetPrimes;
then rng SY c= SetPrimes by a33,FINSEQ_1:def 14;
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 14;
A43: p divides a implies p>k+1 & p<=2*k+1
proof
assume p divides a;
then p in rng SY by A41,NAT_3:8;
then
ex y9 being prime Element of NAT st y9=p & y9>k+1 & y9<=2*k
+1 by A42;
hence thesis;
end;
per cases;
suppose
A44: p>k+1 & p<=2*k+1;
set c = ((k!)*(r!));
A45: b*c = ((2*k+1)!)/c*c by A38,NEWTON:def 3
.= (2*k+1)! by XCMPLX_1:87;
A46: p divides b
proof
assume not p divides b;
then
A47: p divides c by A41,A44,A45,NEWTON:41,80;
per cases by A41,A47,NEWTON:80;
suppose
A48: p divides k!;
k+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 being prime Element of NAT st y9=y & y9>k+1 & y9<=2 *k+1;
hence y in SetPrimes by NEWTON:def 6;
end;
then
A50: Y c= SetPrimes;
p in rng SY by A41,A42,A44;
hence thesis by a33,A41,A50,A49,Th43;
end;
suppose
not(p>k+1 & p<=2*k+1);
then
A51: not p |^ (0+1) divides a by A43;
1 divides a by NAT_D:6;
then
A52: p |^ 0 divides a by NEWTON:4;
p<>1 & a<>0 by A34,A41,Th41,INT_2:def 4;
hence thesis by A52,A51,NAT_3:def 7;
end;
end;
a is non zero Nat by A34,Th41;
then ex n being Element of NAT st b=a*n by A39,A40,Th20;
then a divides b by NAT_D:def 3;
hence thesis by A39,NAT_D:7;
end;
for y being object holds y in {p where p is prime Element of NAT:p<=
2*k+1} iff y in X \/ Y
proof
let y be object;
A53: now
assume
A54: y in X \/ Y;
per cases by A54,XBOOLE_0:def 3;
suppose
y in X;
then consider y9 being prime Element of NAT such that
A55: y9=y and
A56: y9<=k+1;
1*k<=2*k by XREAL_1:68;
then k+1<=2*k+1 by XREAL_1:6;
then y9<=2*k+1 by A56,XXREAL_0:2;
hence y in {p where p is prime Element of NAT:p<=2*k+1} by A55;
end;
suppose
y in Y;
then
ex y9 being prime Element of NAT st y9=y & y9>k+1 & y9<=2*k +1;
hence y in {p where p is prime Element of NAT:p<=2*k+1};
end;
end;
now
assume y in {p where p is prime Element of NAT:p<=2*k+1};
then consider y9 being prime Element of NAT such that
A57: y9=y & y9<=2*k+1;
y in X or y in Y
proof
per cases by A57;
suppose
y9=y & y9<=k+1;
hence thesis;
end;
suppose
y9=y & y9>k+1 & y9<=2*k+1;
hence thesis;
end;
end;
hence y in X \/ Y by XBOOLE_0:def 3;
end;
hence thesis by A53;
end;
then
A58: {p where p is prime Element of NAT: p<=2*k+1}=X \/ Y by TARSKI:2;
2 to_power (2*k)=2 to_power (k+k)
.=(2 to_power k)*(2 to_power k) by POWER:27
.=(2*2) to_power k by POWER:30;
then
A59: Product SY<=(4 to_power k) by A36,A13,XXREAL_0:2;
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 being object holds y in {p where p is prime Element of NAT:p
<=m+1 } iff y in {p where p is prime Element of NAT:p<=m}
proof
let y be object;
A61: now
assume y in {p where p is prime Element of NAT:p<=m+1};
then consider y9 being prime Element of NAT such that
A62: y=y9 and
A63: y9<=m+1;
m+1>1+1 by A11,XREAL_1:6;
then not m+1 is Prime by A60,PEPIN:17;
then y9<m+1 by A63,XXREAL_0:1;
then y9<=m by NAT_1:13;
hence y in {p where p is prime Element of NAT:p<=m} by A62;
end;
now
assume y in {p where p is prime Element of NAT:p<=m};
then consider y9 being 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 is prime Element of NAT:p<=m+1} by A64;
end;
hence thesis by A61;
end;
then
A66: {p where p is prime Element of NAT:p<=m+1}= {p where p is 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 is 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 being Nat holds P[n] from NAT_1:sch 4(A1);
hence thesis;
end;
theorem Th45:
for x being Real st x >= 2 holds
Product Sgm{p where p is prime Element of NAT:p <= x} <= 4 to_power (x-1)
proof
let x be Real;
set A={p where p is prime Element of NAT:p<=x};
A1: A is finite
proof
ex m being Element of NAT st x<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 being 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 is 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 is prime Element of NAT:p<=x};
then ex y9 being 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 being prime Element of NAT st q9=q & q9<=x;
then reconsider q as Prime;
for y being object holds y in {p where p is prime Element of NAT:p<=q} iff
y in {p where p is prime Element of NAT:p<=x}
proof
let y be object;
hereby
assume y in {p where p is prime Element of NAT:p<=q};
then consider y9 being prime Element of NAT such that
A9: y9=y and
A10: y9<=q;
y9<=x by A8,A10,XXREAL_0:2;
hence y in {p where p is prime Element of NAT:p<=x} by A9;
end;
assume
A11: y in {p where p is prime Element of NAT:p<=x};
then consider y9 being prime Element of NAT such that
A12: y9=y and
y9<=x;
y9<=q by A11,A12,XXREAL_2:def 8;
hence thesis by A12;
end;
then
A13: {p where p is prime Element of NAT:p<=q}= {p where p is prime Element
of NAT:p<=x} by TARSKI:2;
A14: 4 to_power (q-1)<=4 to_power (x-1)
proof
per cases by A8,XXREAL_0:1;
suppose
q=x;
hence thesis;
end;
suppose
q<x;
then q-1<x-1 by XREAL_1:14;
hence thesis by POWER:39;
end;
end;
Product Sgm{p where p is 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 is 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 Th46:
for n being Element of NAT, p being Prime st n <> 0
ex f being FinSequence of NAT st len f = n &
(for k being Element of NAT st k in dom f holds
(f.k = 1 iff p|^k divides n) & (f.k = 0 iff not p|^k divides n)) & p |-count
n = Sum f
proof
let n be Element of NAT;
let p be Prime;
defpred P[Nat,object] means ($2=1 iff p|^$1 divides n) & ($2=0 iff not p|^$1
divides n);
set f1 = ((p |-count n) |-> 1) ^ ((n -' p|-count n) |-> 0);
set n1 = p |-count n;
set n2 = n -' p|-count n;
set fa=(p |-count n) |-> 1;
set fb=(n -' p|-count n) |-> 0;
A1: Sum f1 = (Sum fa) + Sum fb by RVSUM_1:75
.= (p |-count n)*1 + Sum fb by RVSUM_1:80
.= p |-count n + (n -' p|-count n)*0 by RVSUM_1:80;
assume
A2: n<>0;
A3: now
p<>1 by INT_2:def 4;
then p|^(p |-count n) divides n by A2,NAT_3:def 7;
then
A4: p |^ (p |-count n) <= n by A2,NAT_D:7;
A5: p>1 by INT_2:def 4;
assume n < p |-count n;
then p to_power n < p to_power (p |-count n) by A5,POWER:39;
then p |^ n < p to_power (p |-count n) by POWER:41;
then p |^ n < p |^ (p |-count n) by POWER:41;
then p |^ n < n by A4,XXREAL_0:2;
hence contradiction by A5,Th3;
end;
A6: for k being Nat st k in Seg n ex x being object st P[k,x]
proof
let k be Nat;
assume k in Seg n;
per cases;
suppose
A7: p|^k divides n;
set x = 1;
take x;
thus thesis by A7;
end;
suppose
A8: not p|^k divides n;
set x = 0;
take x;
thus thesis by A8;
end;
end;
consider f being FinSequence such that
A9: dom f = Seg n and
A10: for k being Nat st k in Seg n holds P[k,f.k] from FINSEQ_1:sch 1(A6
);
now
let x be object;
assume x in rng f;
then consider k being object such that
A11: k in dom f and
A12: f.k=x by FUNCT_1:def 3;
reconsider k as Element of NAT by A11;
P[k,f.k] by A9,A10,A11;
hence x in NAT by A12;
end;
then rng f c= NAT;
then reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
A13: len f1 = len(n1 |-> 1)+len(n2 |-> 0) by FINSEQ_1:22
.= n1 + len(n2 |-> 0) by CARD_1:def 7
.= n1 + n2 by CARD_1:def 7
.= p |-count n + (n - p |-count n) by A3,XREAL_1:233;
A14: for x being object st x in dom f holds f.x=f1.x
proof
set ff2=n2 |-> 0;
set ff1=n1 |-> 1;
let x be object;
assume
A15: x in dom f;
then reconsider x1 = x as Element of NAT;
A16: x in dom f1 by A9,A13,A15,FINSEQ_1:def 3;
per cases by A16,FINSEQ_1:25;
suppose
A17: x1 in dom ff1;
then
A18: x in Seg n1 by FUNCOP_1:13;
A19: p |^ x1 divides n
proof
per cases;
suppose
x1=0;
then p |^ x1 = 1 by NEWTON:4;
hence thesis by NAT_D:6;
end;
suppose
x1>0;
then x1+1>0+1 by XREAL_1:6;
then x1>=1 by NAT_1:13;
then
A20: x1-'1=x1-1 by XREAL_1:233;
set j=p|-count n;
set i=x1-'1;
p<>1 by INT_2:def 4;
then
A21: p |^ j divides n by A2,NAT_3:def 7;
-1+x1<0+x1 & x1 <= p |-count n by A18,FINSEQ_1:1,XREAL_1:6;
then
A22: i<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 being Nat st m in dom ff2 & x1=len ff1 + m;
then consider m being 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 being Element of NAT st k in dom f holds (f.k=1 iff p|^k divides
n) & (f.k=0 iff not p|^k divides n) by A9,A10;
dom f = dom f1 by A9,A13,FINSEQ_1:def 3;
hence thesis by A14,A1,FUNCT_1:2;
end;
theorem Th47:
for n being Element of NAT, p being Prime
ex f being FinSequence of NAT st len f = n &
(for k being Element of NAT st k in dom f holds f.k = [\ n/ (p|^k) /]) &
p |-count (n!) = Sum f
proof
defpred P[Nat] means for p being Prime ex f being FinSequence of
NAT st len f = $1 & (for k being Element of NAT st k in dom f holds f.k=[\ $1/(
p|^k) /]) & p |-count ($1!) = Sum f;
let n be Element of NAT;
let p be Prime;
A1: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
for p being Prime ex f being FinSequence of NAT st len f = n+1 & (for
k being Element of NAT st k in dom f holds f.k=[\ (n+1)/(p|^k) /]) & p |-count
((n+1)!) = Sum f
proof
let p be Prime;
consider fn being FinSequence of NAT such that
A3: len fn = n and
A4: for k being Element of NAT st k in dom fn holds fn.k=[\ n/(p|^k) /] and
A5: p |-count (n!) = Sum fn by A2;
reconsider fnn=fn as FinSequence of REAL by FINSEQ_2:24,NUMBERS:19;
set fn0=fnn ^ <* In(0,REAL) *>;
consider fn1 being FinSequence of NAT such that
A6: len fn1 = n + 1 and
A7: for k being Element of NAT st k in dom fn1 holds (fn1.k=1 iff p
|^k divides (n+1)) & (fn1.k=0 iff not p|^k divides (n+1)) and
A8: p |-count (n+1) = Sum fn1 by Th46;
A9: Seg(n+1) = dom fn1 by A6,FINSEQ_1:def 3;
set f = (fn ^ <* 0 *>)+fn1;
for y being object st y in rng f holds y in NAT
by ORDINAL1:def 12;
then rng f c= NAT;
then reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
take f;
reconsider fn0 as FinSequence of REAL;
reconsider fn1 as FinSequence of REAL by FINSEQ_2:24,NUMBERS:19;
A10: dom f = dom fn0 /\ dom fn1 by VALUED_1:def 1;
A11: len fn0 = len fn + len <* 0 *> by FINSEQ_1:22
.= n + 1 by A3,FINSEQ_1:39;
then Seg(n+1) = dom fn0 by FINSEQ_1:def 3;
hence len f = n+1 by A10,A9,FINSEQ_1:def 3;
thus for k being Element of NAT st k in dom f holds f.k=[\ (n+1)/(p|^k)
/]
proof
let k be Element of NAT;
A12: (p|^k)/(p|^k)=1 by XCMPLX_1:60;
assume
A13: k in dom f;
then
A14: f.k = fn0.k + fn1.k by VALUED_1:def 1;
A15: k in dom fn0 by A10,A13,XBOOLE_0:def 4;
A16: fn0.k=[\ n/(p|^k) /]
proof
per cases by A15,FINSEQ_1:25;
suppose
A17: k in dom fn;
then fn.k=[\ n/(p|^k) /] by A4;
hence thesis by A17,FINSEQ_1:def 7;
end;
suppose
ex n1 being Nat st n1 in dom <* 0 *> & k=len fn + n1;
then consider n1 being Nat such that
A18: n1 in dom <* 0 *> and
A19: k=len fn + n1;
n1 in Seg 1 by A18,FINSEQ_1:38;
then
A20: n1=1 by FINSEQ_1:2,TARSKI:def 1;
p>1 by INT_2:def 4;
then
A21: p*p|^n>1*p|^n & p|^n>n by Th3,XREAL_1:68;
p|^(n+1)=p|^n*p by NEWTON:6;
then p|^k>n by A3,A19,A20,A21,XXREAL_0:2;
then n/(p|^k)<1 by XREAL_1:189;
then
A22: n/(p|^k)-1<1-1 by XREAL_1:9;
fn0.(n+1)=<* 0 *>.1 by A3,A18,A20,FINSEQ_1:def 7;
then fn0.k=0 by A3,A19,A20;
hence thesis by A22,INT_1:def 6;
end;
end;
A23: k in dom fn1 by A10,A13,XBOOLE_0:def 4;
per cases;
suppose
A24: p|^k divides (n+1);
then consider r being Nat such that
A25: n+1=(p|^k)*r by NAT_D:def 3;
A26: (n+1)/(p|^k) = r/((p|^k)/(p|^k)) by A25,XCMPLX_1:77
.= r/(1/1) by XCMPLX_1:60
.= r;
((p|^k)/(p|^k))+((-1)/(p|^k))-1<0 by A12;
then
A27: (p|^k+(-1))/(p|^k)-1<0 by XCMPLX_1:62;
[\ n/(p|^k) /] + 1 = [\ n/(p|^k) +1 /] by INT_1:28
.=[\ n/(p|^k) + (p|^k)/(p|^k) /] by XCMPLX_1:60
.=[\ (n+p|^k)/(p|^k) /] by XCMPLX_1:62
.=[\ ((n+1)+(p|^k -1))/(p|^k) /]
.=[\ (n+1)/(p|^k) + (p|^k-1)/(p|^k) /] by XCMPLX_1:62
.=(n+1)/(p|^k) + [\ (p|^k-1)/(p|^k) /] by A26,INT_1:28
.=(n+1)/(p|^k) + 0 by A27,INT_1:def 6
.=[\ (n+1)/(p|^k) /] by A26;
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 being Element of NAT st k in dom f holds f.k=[\ 0/(p|^k) /];
p<>1 by INT_2:def 4;
hence thesis by NAT_3:21,NEWTON:12,RVSUM_1:72;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A35,A1);
then consider f being FinSequence of NAT such that
A36: ( len f = n & for k being Element of NAT st k in dom f holds f.k=[\
n/(p|^k) /] )& p |-count (n!) = Sum f;
take f;
thus thesis by A36;
end;
theorem Th48:
for n being Element of NAT, p being Prime
ex f being FinSequence of REAL st len f = 2*n &
(for k being Element of NAT st k in dom f holds
f.k = [\(2*n)/(p|^k)/] - 2*[\n/(p|^k)/]) & p |-count (2*n choose n) = Sum f
proof
let n be Element of NAT;
let p be Prime;
set f0=n|->0;
consider f1 being FinSequence of NAT such that
A1: len f1 = n and
A2: for k being Element of NAT st k in dom f1 holds f1.k=[\ n/(p|^k) /] and
A3: p |-count (n!) = Sum f1 by Th47;
consider f2 being FinSequence of NAT such that
A4: len f2 = 2*n and
A5: for k being Element of NAT st k in dom f2 holds f2.k=[\ (2*n)/(p|^k) /] and
A6: p |-count ((2*n)!) = Sum f2 by Th47;
reconsider f2 as FinSequence of REAL by FINSEQ_2:24,NUMBERS:19;
set f = f2+((-(f1^f0))+(-(f1^f0)));
take f;
A7: dom (f1^f0) = Seg (len f1 + len f0) by FINSEQ_1:def 7
.= Seg (n+n) by A1,CARD_1:def 7
.= Seg (2*n);
A8: dom ((-(f1^f0))+(-(f1^f0))) = dom (-(f1^f0)) /\ dom (-(f1^f0))
by VALUED_1:def 1
.= Seg (2*n) by A7,VALUED_1:8;
A9: dom f = dom f2 /\ dom ((-(f1^f0))+(-(f1^f0))) by VALUED_1:def 1
.= Seg (2*n) /\ Seg (2*n) by A4,A8,FINSEQ_1:def 3;
hence len f = 2*n by FINSEQ_1:def 3;
thus for k being Element of NAT st k in dom f holds f.k=[\(2*n)/(p|^k)/]- 2*
[\n/(p|^k)/]
proof
let k be Element of NAT;
assume
A10: k in dom f;
then
A11: k in dom f2 by A4,A9,FINSEQ_1:def 3;
A12: f.k = f2.k+((-(f1^f0))+(-(f1^f0))).k by A10,VALUED_1:def 1
.=f2.k+((-(f1^f0)).k+(-(f1^f0)).k) by A8,A9,A10,VALUED_1:def 1
.=f2.k+2*(-(f1^f0)).k
.=f2.k+2*(-(f1^f0).k) by RVSUM_1:17
.=f2.k-2*(f1^f0).k
.=[\(2*n)/(p|^k)/]-2*(f1^f0).k by A5,A11;
per cases by A7,A9,A10,FINSEQ_1:25;
suppose
A13: k in dom f1;
then (f1^f0).k=f1.k by FINSEQ_1:def 7
.=[\n/(p|^k)/] by A2,A13;
hence thesis by A12;
end;
suppose
ex e being Nat st e in dom f0 & k=len f1 + e;
then consider e being Nat such that
A14: e in dom f0 and
A15: k=len f1 + e;
dom f0 = Seg n by FUNCOP_1:13;
then e >= 1 by A14,FINSEQ_1:1;
then e + len f1 >= 1 + len f1 by XREAL_1:6;
then
A16: k > 1 + n or k = 1 + n by A1,A15,XXREAL_0:1;
A17: (f1^f0).k = f0.e by A14,A15,FINSEQ_1:def 7
.= 0;
p>1 by INT_2:def 4;
then p to_power k >= p to_power (1+n) by A16,POWER:39;
then p|^k >= p to_power (1+n) by POWER:41;
then
A18: p|^k >= p|^(1+n) by POWER:41;
A19: p>1 by INT_2:def 4;
then p*p|^n>1*p|^n by XREAL_1:68;
then p|^(1+n)>p|^n by NEWTON:6;
then
A20: p|^k>p|^n by A18,XXREAL_0:2;
per cases;
suppose
n=0;
hence thesis by A12,A17;
end;
suppose
A21: n<>0;
(p|^n)/(p|^n)>n/(p|^n) by A19,Th3,XREAL_1:74;
then
A22: 1>n/(p|^n) by XCMPLX_1:60;
n/(p|^n)>n/(p|^k) by A20,A21,XREAL_1:76;
then 1>n/(p|^k) by A22,XXREAL_0:2;
then 1-1>n/(p|^k)-1 by XREAL_1:9;
hence thesis by A12,A17,INT_1:def 6;
end;
end;
end;
p |-count (2*n choose n) = Sum f
proof
per cases;
suppose
A23: n=0; then
A24: 2*n choose n = 1 by NEWTON:19;
p>1 by INT_2:def 4;
then
A25: p |-count (2*n choose n) = 0 by A24,NAT_3:21;
len f = 0 by A9,A23,FINSEQ_1:def 3;
hence thesis by A25,PROB_3:62;
end;
suppose
A26: n<>0;
A27: 2*n-n=n;
A28: n+n>n+0 by A26,XREAL_1:6;
then (2*n choose n)*((n!)*(n!)) = ((2*n)!)/((n!)*(n!))*((n!)*(n!)) by A27
,NEWTON:def 3
.= (2*n)! by XCMPLX_1:87;
then
A29: ((n!) * (n!)) divides ((2*n)!) by NAT_D:def 3;
2*n choose n = ((2*n)!)/((n!)*(n!)) by A28,A27,NEWTON:def 3;
then
A30: 2*n choose n = ((n!) * (n!)) * (((2*n)!) div ((n!) * (n!))) /((n!)*
(n!)) by A29,NAT_D:3
.= ((2*n)!) div ((n!) * (n!)) by XCMPLX_1:89;
A31: -(f1^f0) is Element of len(-(f1^f0))-tuples_on REAL by FINSEQ_2:92;
A32: p |-count (((2*n)!) div ((n!)*(n!))) = p |-count ((2*n)!) -' p
|-count ((n!)*(n!)) by A29,NAT_3:31
.= p |-count ((2*n)!) - p |-count ((n!)*(n!)) by A29,NAT_3:30
,XREAL_1:233;
A33: ((-(f1^f0))+(-(f1^f0))) is Element of len((-(f1^f0))+(-(f1^f0)))
-tuples_on REAL by FINSEQ_2:92;
len((-(f1^f0))+(-(f1^f0)))=len f2 & f2 is Element of len(f2)
-tuples_on REAL by A4,A8,FINSEQ_1:def 3,FINSEQ_2:92;
then Sum f = Sum f2 + Sum((-(f1^f0))+(-(f1^f0))) by A33,RVSUM_1:89
.= Sum f2 + (Sum(-(f1^f0)) + Sum(-(f1^f0))) by A31,RVSUM_1:89
.= Sum f2 + (- Sum(f1^f0) + Sum(-(f1^f0))) by RVSUM_1:88
.= Sum f2 + (- Sum(f1^f0) + (- Sum(f1^f0))) by RVSUM_1:88
.= Sum f2 - 2*Sum(f1^f0)
.= Sum f2 - 2*(Sum(f1) + Sum(f0)) by RVSUM_1:75
.= Sum f2 - 2*(Sum f1 + n*0) by RVSUM_1:80
.= p |-count ((2*n)!) -(p |-count (n!) + p |-count (n!)) by A3,A6
.= p |-count (((2*n)!) div ((n!)*(n!))) by A32,NAT_3:28;
hence thesis by A30;
end;
end;
hence thesis;
end;
Lm8: for n,r being Element of NAT, p being Prime, f being FinSequence of REAL
st p|^r <= 2*n & 2*n < p|^(r+1) & len f = 2*n & (for k being Element of NAT st
k in dom f holds f.k=[\(2*n)/(p|^k)/] - 2*[\n/(p|^k)/]) holds Sum f <= r
proof
let n,r be Element of NAT;
let p be Prime;
let f be FinSequence of REAL;
set f0 = (r |-> 1)^((2*n -' r)|-> 0);
A1: p>1 by INT_2:def 4;
assume
A2: p|^r <= 2*n;
A3: 2*n >= r
proof
assume 2*n < r;
then p to_power (2*n)<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 being Element of NAT st k in dom f holds f.k=[\(2*n)/(p|^k)/]
- 2*[\n/(p|^k)/];
A8: for k be Element of NAT st k in dom f holds f.k <= f0.k
proof
let k be Element of NAT;
assume
A9: k in dom f;
then
A10: f.k=[\(2*n)/(p|^k)/] - 2*[\n/(p|^k)/] by A7;
k in Seg (2*n) by A5,A9,FINSEQ_1:def 3;
then
A11: k in dom f0 by A5,A6,FINSEQ_1:def 3;
per cases by A11,FINSEQ_1:25;
suppose
A12: k in dom (r |-> 1);
[\n/(p|^k)/] <= n/(p|^k) by INT_1:def 6;
then -[\n/(p|^k)/] >= -n/(p|^k) by XREAL_1:24;
then
(2*n)/(p|^k) - 1 < [\(2*n)/(p|^k)/] & (-[\n/(p|^k)/])*2 >= (-n/(p|^
k))*2 by INT_1:def 6,XREAL_1:64;
then ((2*n)/(p|^k) - 1) + 2*(-n/(p|^k)) < [\(2*n)/(p|^k)/] + (-2*[\n/(p
|^k)/]) by XREAL_1:8;
then [\(2*n)/(p|^k)/] -2*[\n/(p|^k)/] > 2*(n/(p|^k)) -1 + 2*(-n/(p|^k))
by XCMPLX_1:74;
then f.k >= -1 +1 by A10,INT_1:7;
then
A13: f.k is Element of NAT by A10,INT_1:3;
n/(p|^k) - 1 < [\n/(p|^k)/] by INT_1:def 6;
then -[\n/(p|^k)/] < -(n/(p|^k) - 1) by XREAL_1:24;
then [\(2*n)/(p|^k)/] <= (2*n)/(p|^k) & (-[\n/(p|^k)/])*2 < (-(n/(p|^k)
- 1))*2 by INT_1:def 6,XREAL_1:68;
then
(2*n)/(p|^k)= 2*(n/(p|^k)) & -2*[\n/(p|^k)/] + [\(2*n)/(p|^k)/] < 2
*(-n/(p|^ k) + 1) + (2*n)/(p|^k) by XCMPLX_1:74,XREAL_1:8;
then
A14: f.k < 1+1 by A10;
A15: k in Seg r by A12,FUNCOP_1:13;
f0.k = (r |-> 1).k by A12,FINSEQ_1:def 7
.= 1 by A15,FUNCOP_1:7;
hence thesis by A13,A14,NAT_1:13;
end;
suppose
A16: ex n0 being Nat st n0 in dom ((2*n -' r)|-> 0) & k=len (r |-> 1 )+ n0;
reconsider k1=k as Element of NAT;
consider n0 be Nat such that
A17: n0 in dom ((2*n -' r)|-> 0) and
A18: k=len (r |-> 1)+ n0 by A16;
n0 in Seg (2*n -' r) by A17,FUNCOP_1:13;
then 1<=n0 by FINSEQ_1:1;
then
A19: 1+r<=n0+r by XREAL_1:6;
k=r + n0 by A18,CARD_1:def 7;
then r+1<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 being Element of NAT, p being 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 being Element of NAT, p being Prime st n>=2 & p|^r <= 2*n & 2*n
< p|^(r+1) holds p |-count (2*n choose n) <= r
proof
let n,r be Element of NAT;
let p be Prime;
assume that
n>=2 and
A3: p|^r <= 2*n & 2*n < p|^(r+1);
ex f be FinSequence of REAL st len f = 2*n &( for k being Element of
NAT st k in dom f holds f.k=[\(2*n)/(p|^k)/] - 2*[\n/(p|^k)/])& p |-count (2*n
choose n) = Sum f by Th48;
hence thesis by A3,Lm8;
end;
thus p>2*n implies p |-count (2*n choose n) = 0
proof
set r = 0;
assume p>2*n;
then
A4: p|^(r+1)>2*n;
A5: n>=2 by A1,XXREAL_0:2;
then n*2>=2*2 by XREAL_1:64;
then 2*n>=1 by XXREAL_0:2;
then p|^r <= 2*n by NEWTON:4;
hence thesis by A2,A5,A4;
end;
thus n<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<p & p<=n implies p |-count (2*n choose n) = 0
proof
set q = (2*n) |-> 0;
assume
A10: 2*n/3<p;
consider f be FinSequence of REAL such that
A11: len f = 2*n and
A12: for k being 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 being Element of NAT st k in dom f holds f.k=0
proof
let k be Element of NAT;
A17: for m being 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 being 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;
func p |-count f -> FinSequence of NAT means
:Def1:
len it = len f & for i being set st i in dom it holds it.i = p |-count f.i;
existence
proof
deffunc F(Nat) = p |-count f.$1;
consider g being FinSequence such that
A1: len g = len f and
A2: for k being Nat st k in dom g holds g.k = F(k) from FINSEQ_1:sch 2;
now
let y be object;
assume y in rng g;
then consider x be object such that
A3: x in dom g and
A4: y=g.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A3;
y=F(x) by A2,A3,A4;
hence y in NAT;
end;
then rng g c= NAT;
then reconsider g as FinSequence of NAT by FINSEQ_1:def 4;
take g;
thus len g = len f by A1;
let i be set;
assume i in dom g;
hence thesis by A2;
end;
uniqueness
proof
let g,h be FinSequence of NAT such that
A5: len g = len f and
A6: for i being set st i in dom g holds g.i = p |-count f.i and
A7: len h = len f and
A8: for i being set st i in dom h holds h.i = p |-count f.i;
A9: dom g = Seg len g & dom h = Seg len h by FINSEQ_1:def 3;
for k being Nat st k in dom g holds g.k = h.k
proof
let k be Nat;
assume
A10: k in dom g;
hence g.k = p |-count f.k by A6
.= h.k by A5,A7,A8,A9,A10;
end;
hence thesis by A5,A7,A9,FINSEQ_1:13;
end;
end;
theorem Th49:
for p being Prime, f being FinSequence of NAT st f = {} holds
p |-count f = {}
proof
let p be Prime;
let f be FinSequence of NAT;
assume f={};
then len (p |-count f) = len {} by Def1;
hence thesis;
end;
theorem Th50:
for p being Prime, f1,f2 being FinSequence of NAT holds
p |-count (f1^f2) = (p |-count f1)^(p |-count f2)
proof
let p be Prime;
let f1,f2 be FinSequence of NAT;
A1: len (p |-count f2) = len f2 by Def1;
A2: dom (p |-count (f1^f2)) = Seg len (p |-count (f1^f2)) by FINSEQ_1:def 3
.= Seg len (f1^f2) by Def1;
A3: for k being Nat st k in dom (p |-count (f1^f2)) holds (p |-count (f1^f2)
).k = ((p |-count f1)^(p |-count f2)).k
proof
let k be Nat;
assume
A4: k in dom (p |-count (f1^f2));
then
A5: k in dom (f1^f2) by A2,FINSEQ_1:def 3;
per cases by A5,FINSEQ_1:25;
suppose
A6: k in dom f1;
A7: dom f1 = Seg len f1 by FINSEQ_1:def 3
.= Seg len (p |-count f1) by Def1
.= dom (p |-count f1) by FINSEQ_1:def 3;
(p |-count (f1^f2)).k = p |-count (f1^f2).k by A4,Def1
.= p |-count (f1.k) by A6,FINSEQ_1:def 7
.= (p |-count f1).k by A6,A7,Def1;
hence thesis by A6,A7,FINSEQ_1:def 7;
end;
suppose
A8: ex n being Nat st n in dom f2 & k=len f1 + n;
A9: dom f2 = Seg len f2 by FINSEQ_1:def 3
.= Seg len (p |-count f2) by Def1
.= dom (p |-count f2) by FINSEQ_1:def 3;
consider n be Nat such that
A10: n in dom f2 and
A11: k=len f1 + n by A8;
A12: ((p |-count f1)^(p |-count f2)).k = ((p |-count f1)^(p |-count f2))
.(len (p |-count f1) + n) by A11,Def1
.= (p |-count f2).n by A10,A9,FINSEQ_1:def 7;
(f1^f2).k = f2.n by A10,A11,FINSEQ_1:def 7;
then (p |-count (f1^f2)).k = p |-count (f2.n) by A4,Def1
.= (p |-count f2).n by A10,A9,Def1;
hence thesis by A12;
end;
end;
Seg len (f1^f2) = Seg (len f1 + len f2) by FINSEQ_1:22
.= Seg (len (p |-count f1) + len (p |-count f2)) by A1,Def1
.= Seg len ((p |-count f1)^(p |-count f2)) by FINSEQ_1:22
.= dom ((p |-count f1)^(p |-count f2)) by FINSEQ_1:def 3;
hence thesis by A2,A3,FINSEQ_1:13;
end;
theorem Th51:
for p being Prime, n being non zero Element of NAT holds
p |-count <*n*> = <* (p |-count n) *>
proof
let p be Prime;
let n be non zero Element of NAT;
A1: dom (p |-count <*n*>) = Seg len (p |-count <*n*>) by FINSEQ_1:def 3
.= Seg len <*n*> by Def1
.= Seg 1 by FINSEQ_1:39;
A2: for k being Nat st k in dom (p |-count <*n*>) holds (p |-count <*n*>).k
= <* p |-count n *>.k
proof
let k be Nat;
assume
A3: k in dom (p |-count <*n*>);
then 1<=k & k<=1 by A1,FINSEQ_1:1;
then
A4: k=1 by XXREAL_0:1;
(p |-count <*n*>).k = p |-count <*n*>.k by A3,Def1;
then (p |-count <*n*>).k = p |-count n by A4;
hence thesis by A4;
end;
Seg 1 = Seg len <* p |-count n *> by FINSEQ_1:39;
then dom (p |-count <*n*>) = dom <* (p |-count n) *> by A1,FINSEQ_1:def 3;
hence thesis by A2,FINSEQ_1:13;
end;
theorem Th52:
for f being FinSequence of NAT, p being Prime st Product f <> 0
holds p |-count (Product f) = Sum (p |-count f)
proof
let f be FinSequence of NAT;
defpred P[Nat] means for f being FinSequence of NAT, p being
Prime st $1=len f & Product f <> 0 holds p |-count (Product f) = Sum (p |-count
f);
let p be Prime;
assume
A1: Product f<>0;
A2: ex n being Element of NAT st n=len f;
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A4: P[n];
for f being FinSequence of NAT, p being Prime st n+1=len f & Product f
<> 0 holds p |-count (Product f) = Sum (p |-count f)
proof
let f be FinSequence of NAT;
let p be Prime;
assume that
A5: n+1=len f and
A6: Product f <> 0;
consider g being FinSequence of NAT, d being Element of NAT such that
A7: f = g^<*d*> by A5,FINSEQ_2:19;
len f = len g + len <*d*> by A7,FINSEQ_1:22;
then
A8: n+1 = len g + 1 by A5,FINSEQ_1:39;
A9: (Product g) * d <> 0 by A6,A7,RVSUM_1:96;
then
A10: Product g <> 0;
A11: d <> 0 by A9;
p |-count (Product f) = p |-count ((Product g) * d) by A7,RVSUM_1:96
.= (p |-count (Product g)) + (p |-count d) by A10,A11,NAT_3:28
.= Sum (p |-count g) + (p |-count d) by A4,A10,A8
.= Sum ((p |-count g)^<*(p |-count d)*>) by RVSUM_1:74
.= Sum ((p |-count g)^(p |-count <*d*>)) by A11,Th51
.= Sum (p |-count (g^<*d*>)) by Th50;
hence thesis by A7;
end;
hence thesis;
end;
A12: P[0]
proof
let f be FinSequence of NAT;
let p be Prime;
assume that
A13: 0=len f and
Product f<>0;
A14: p<>1 by INT_2:def 4;
A15: f={} by A13;
then Sum (p |-count f) = 0 by Th49,RVSUM_1:72;
hence thesis by A15,A14,NAT_3:21,RVSUM_1:94;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A12,A3);
hence thesis by A1,A2;
end;
theorem Th53:
for f1,f2 being FinSequence of REAL st len f1 = len f2 &
(for k being Element of NAT st k in dom f1 holds f1.k <= f2.k & f1.k > 0)
holds Product f1 <= Product f2
proof
let f1,f2 be FinSequence of REAL;
defpred P[Nat] means for f1,f2 being FinSequence of REAL st len
f1 = len f2 & $1 = len f1 & (for k being Element of NAT st k in dom f1 holds f1
.k<=f2.k & f1.k>0) holds Product f1 <= Product f2;
assume
A1: len f1 = len f2;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: P[n];
for f1,f2 being FinSequence of REAL st len f1 = len f2 & n+1 = len f1
& (for k being Element of NAT st k in dom f1 holds f1.k<=f2.k & f1.k>0) holds
Product f1 <= Product f2
proof
let f1,f2 be FinSequence of REAL;
assume that
A4: len f1=len f2 and
A5: n+1=len f1;
consider g2 be FinSequence of REAL, r2 be Element of REAL such that
A6: f2 = g2^<*r2*> by A4,A5,FINSEQ_2:19;
len f2 = len g2 + len <* r2 *> by A6,FINSEQ_1:22;
then
A7: n+1 = len g2 + 1 by A4,A5,FINSEQ_1:39;
A8: Product f2 = (Product g2) * r2 by A6,RVSUM_1:96;
consider g1 be FinSequence of REAL, r1 be Element of REAL such that
A9: f1 = g1^<*r1*> by A5,FINSEQ_2:19;
set k1 = len g1+1;
A10: Product f1 = (Product g1) * r1 by A9,RVSUM_1:96;
len f1 = len g1 + len <* r1 *> by A9,FINSEQ_1:22;
then
A11: n+1 = len g1 + 1 by A5,FINSEQ_1:39;
assume
A12: for k being Element of NAT st k in dom f1 holds f1.k<=f2.k & f1. k>0;
A13: now
let k be Element of NAT;
A14: dom g1 c= dom f1 by A9,FINSEQ_1:26;
assume
A15: k in dom g1;
then k in Seg len g2 by A11,A7,FINSEQ_1:def 3;
then k in dom g2 by FINSEQ_1:def 3;
then
A16: f2.k=g2.k by A6,FINSEQ_1:def 7;
f1.k=g1.k by A9,A15,FINSEQ_1:def 7;
hence g1.k<=g2.k & g1.k>0 by A12,A15,A16,A14;
end;
then
A17: for k being Element of NAT st k in dom g1 holds g1.k > 0;
Product g1 <= Product g2 by A3,A11,A7,A13;
then
A18: Product g2 > 0 by A17,Th41;
n+1>=0+1 by XREAL_1:6;
then k1 in Seg (n+1) by A11,FINSEQ_1:1;
then
A19: k1 in dom f1 by A5,FINSEQ_1:def 3;
then f1.k1<=f2.k1 by A12;
then r1 <= f2.k1 by A9,FINSEQ_1:42;
then r1 <= r2 by A6,A11,A7,FINSEQ_1:42;
then
A20: r1 * (Product g2) <= r2 * (Product g2) by A18,XREAL_1:64;
f1.k1>0 by A12,A19;
then r1>0 by A9,FINSEQ_1:42;
then (Product g1) * r1 <= (Product g2) * r1 by A3,A11,A7,A13,XREAL_1:64;
hence thesis by A10,A8,A20,XXREAL_0:2;
end;
hence thesis;
end;
A21: P[0]
proof
let f1,f2 be FinSequence of REAL;
assume len f1 = len f2 & 0=len f1;
then f1={} & f2 = {};
hence thesis;
end;
A22: for n being Nat holds P[n] from NAT_1:sch 2(A21,A2);
assume for k being Element of NAT st k in dom f1 holds f1.k<=f2.k & f1.k>0;
hence thesis by A22,A1;
end;
theorem Th54:
for n being Element of NAT, r being Real st r > 0 holds
Product (n|-> r) = r to_power n
proof
defpred P[Nat] means for r being Real st r>0 holds Product ($1
|-> r) = r to_power $1;
A1: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
now
let r be Real;
assume
A3: r>0;
Product ((n+1)|-> r) = Product ((n |-> r) ^ <*r*>) by FINSEQ_2:60
.= Product (n |-> r) * r by RVSUM_1:96
.= (r to_power n) * r by A2,A3
.= (r to_power n) * (r to_power 1) by POWER:25;
hence Product ((n+1)|-> r) = r to_power (n+1) by A3,POWER:27;
end;
hence thesis;
end;
A4: P[0] by POWER:24,RVSUM_1:94;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
scheme
scheme1 { P[set,set,set] } : for p being Prime, n being Element of NAT, m
being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9
is prime Element of NAT: P[n,m,p9]} holds Product Sgm X > 0 proof
let p be Prime;
let n be Element of NAT;
let m be non zero Element of NAT;
let X be set;
set f = Sgm X;
assume
A1: X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]};
A2: for k being Element of NAT st k in dom f holds f.k > 0
proof
set XX=Seg m;
let k be Element of NAT;
now
let x be object;
assume x in X;
then consider y9 being prime Element of NAT such that
A4: y9|^(y9 |-count m) = x & P[n,m,y9] by A1;
1 <= y9|^(y9 |-count m) <= m by Th16;
hence x in XX by A4,FINSEQ_1:1;
end;
then X c= Seg m;
then X is included_in_Seg by FINSEQ_1:def 13;
then
A3: rng f = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,
p9]} by A1,FINSEQ_1:def 14;
assume k in dom f;
then
f.k in {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9
]} by A3,FUNCT_1:3;
then
ex y9 being prime Element of NAT st y9|^(y9 |-count m) = f.k & P[n,m, y9];
hence thesis;
end;
rng f c= REAL;
then f is FinSequence of REAL by FINSEQ_1:def 4;
hence thesis by A2,Th41;
end;
scheme
scheme2 { P[set,set,set] } : for p being Prime, n being Element of NAT, m
being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9
is prime Element of NAT: P[n,m,p9]} & not p|^(p |-count m) in X holds p |-count
(Product Sgm X) = 0 proof
let p be Prime;
let n be Element of NAT;
let m be non zero Element of NAT;
let X be set;
assume
A1: X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]};
set f=p |-count (Sgm X);
set g=(len f) |-> 0;
assume
A2: not p|^(p |-count m) in X;
A3: for k being Nat st 1 <=k & k <= len f holds f.k=g.k
proof
set XX=Seg m;
let k be Nat;
assume
A4: 1 <=k;
assume k <= len f;
then
A5: k in Seg len f by A4,FINSEQ_1:1;
then k in dom f by FINSEQ_1:def 3;
then
A6: f.k = p |-count (Sgm X).k by Def1;
now
let x be object;
assume x in X;
then consider y9 being prime Element of NAT such that
B1: y9|^(y9 |-count m) = x & P[n,m,y9] by A1;
1 <= y9|^(y9 |-count m) <= m by Th16;
hence x in XX by B1,FINSEQ_1:1;
end;
then X c= Seg m;
then X is included_in_Seg by FINSEQ_1:def 13;
then
A7: rng Sgm X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n
,m,p9]} by A1,FINSEQ_1:def 14;
len f = len (Sgm X) by Def1;
then k in dom Sgm X by A5,FINSEQ_1:def 3;
then
(Sgm X).k in {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[
n,m,p9]} by A7,FUNCT_1:3;
then consider p1 be prime Element of NAT such that
A8: p1|^(p1 |-count m) = (Sgm X).k and
A9: P[n,m,p1];
p1<>p by A1,A2,A9;
then p<>1 & not p divides p1|^(p1 |-count m) by INT_2:def 4,NAT_3:6;
then f.k = 0 by A6,A8,NAT_3:27;
hence thesis;
end;
for p being Prime, n being Element of NAT, m being non zero Element of
NAT , X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT:
P[n,m,p9]} holds Product Sgm X > 0 from scheme1;
then Product Sgm X <> 0 by A1;
then
A10: p |-count (Product Sgm X) = Sum (p |-count (Sgm X)) by Th52;
len f = len g & Sum g = (len f)*0 by CARD_1:def 7,RVSUM_1:80;
hence thesis by A10,A3,FINSEQ_1:14;
end;
scheme
scheme3 { P[set,set,set] } : for p being Prime, n being Element of NAT, m
being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9
is prime Element of NAT: P[n,m,p9]} & p|^(p |-count m) in X holds p |-count (
Product Sgm X) = p |-count m proof
let p be Prime;
let n be Element of NAT;
let m be non zero Element of NAT;
let X be set;
set XX=Seg m;
defpred P1[Element of NAT,Element of NAT,Prime] means P[$1,$2,$3] & $3|^($3
|-count $2) <= p|^(p |-count $2);
defpred P2[Element of NAT,Element of NAT,Prime] means P[$1,$2,$3] & $3|^($3
|-count $2) > p|^(p |-count $2);
set X1 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P1[n,m,p9]};
set X2 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P2[n,m,p9]};
A1: now
let k1,k2 be Nat;
assume k1 in X1 & k2 in X2;
then
( ex p1 being prime Element of NAT st p1|^(p1 |-count m)=k1 & P1[n, m
,p1])& ex p2 being prime Element of NAT st p2|^(p2 |-count m)=k2 & P2[n,m,p2];
hence k1 < k2 by XXREAL_0:2;
end;
A2: now
assume p|^(p |-count m) in X2;
then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count
m) & P2[n,m,p9];
hence contradiction;
end;
set m1=p|^(p |-count m);
defpred P12[Element of NAT,Element of NAT,Prime] means P[$1,$2,$3] & $3|^($3
|-count $2) = p|^(p |-count $2);
defpred P11[Element of NAT,Element of NAT,Prime] means P[$1,$2,$3] & $3|^($3
|-count $2) < p|^(p |-count $2);
set X11 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P11[n,m,p9]};
set X12 = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P12[n,m,p9]};
A3: now
let k1,k2 be Nat;
assume k1 in X11 & k2 in X12;
then
( ex p1 being prime Element of NAT st p1|^(p1 |-count m)=k1 & P11[n,m
,p1])& ex p2 being prime Element of NAT st p2|^(p2 |-count m)=k2 & P12[n,m,p2];
hence k1 < k2;
end;
now
let x be object;
assume x in X1;
then consider p9 being prime Element of NAT such that
A4: p9|^(p9 |-count m)=x & P1[n,m,p9];
p9|^(p9 |-count m)=x & P11[n,m,p9] or p9|^(p9 |-count m)=x & P12[n,m,
p9] by A4,XXREAL_0:1;
then x in X11 or x in X12;
hence x in X11 \/ X12 by XBOOLE_0:def 3;
end;
then
A5: X1 c= X11 \/ X12;
assume
A6: X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]};
now
let x be object;
assume x in X;
then consider y9 being prime Element of NAT such that
B1: y9|^(y9 |-count m) = x & P[n,m,y9] by A6;
1<= y9|^(y9 |-count m) <= m by Th16;
hence x in XX by B1,FINSEQ_1:1;
end;
then
A7: X c= Seg m;
now
let x be object;
assume x in X12;
then
ex p9 be prime Element of NAT st p9|^(p9 |-count m) = x & P12[n,m,p9];
hence x in {p|^(p |-count m)} by TARSKI:def 1;
end;
then
A8: X12 c= {p|^(p |-count m)};
for p being Prime, n being Element of NAT, m being non zero Element of
NAT , X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT:
P[n,m,p9]} holds Product Sgm X > 0 from scheme1;
then
A9: Product Sgm X <> 0 by A6;
A10: 1 < p by INT_2:def 4;
A11: p |-count (p|^(p |-count m)) = (p |-count m) * (p |-count p) by NAT_3:32
.= (p |-count m) * 1 by A10,NAT_3:22;
now
let x be object;
assume x in X1;
then
ex p9 being prime Element of NAT st p9|^(p9 |-count m)=x & P1[n,m,p9];
hence x in X by A6;
end;
then
A12: X1 c= X;
then
A13: X1 c= Seg m by A7;
then
a13: X1 is included_in_Seg by FINSEQ_1:def 13;
now
let x be object;
assume x in X12;
then
ex p9 being prime Element of NAT st p9|^(p9 |-count m)=x & P12[n,m,p9 ];
hence x in X1;
end;
then
A14: X12 c= X1;
then X12 c= Seg m by A13;
then
a15: X12 is included_in_Seg by FINSEQ_1:def 13;
now
let x be object;
assume x in X11;
then
ex p9 being prime Element of NAT st p9|^(p9 |-count m)=x & P11[n,m,p9 ];
hence x in X1;
end;
then
A16: X11 c= X1;
then X11 c= Seg m by A13;
then
a17: X11 is included_in_Seg by FINSEQ_1:def 13;
X11 \/ X12 c= X1 \/ X1 by A16,A14,XBOOLE_1:13;
then
A18: Sum (p |-count (Sgm X1)) = Sum (p |-count (Sgm (X11 \/ X12))) by A5,
XBOOLE_0:def 10
.= Sum (p |-count (Sgm(X11) ^ Sgm(X12))) by a17,a15,A3,FINSEQ_3:42
.= Sum ((p |-count Sgm(X11)) ^ (p |-count Sgm(X12))) by Th50
.= Sum (p |-count Sgm(X11)) + Sum (p |-count Sgm(X12)) by RVSUM_1:75;
for p being Prime, n being Element of NAT, m being non zero Element of
NAT , X2 being set st X2 = {p9|^(p9 |-count m) where p9 is prime Element of NAT
: P2[n,m,p9]} & not p|^(p |-count m) in X2 holds p |-count (Product Sgm X2) = 0
from scheme2;
then
A19: p |-count (Product Sgm X2) = 0 by A2;
for p being Prime, n being Element of NAT, m being non zero Element of
NAT , X2 being set st X2 = {p9|^(p9 |-count m) where p9 is prime Element of NAT
: P2[n,m,p9]} holds Product Sgm X2 > 0 from scheme1;
then
A20: Product Sgm(X2) <> 0;
now
let x be object;
assume x in X;
then consider p9 being prime Element of NAT such that
A21: p9|^(p9 |-count m)=x & P[n,m,p9] by A6;
p9|^(p9 |-count m)=x & P1[n,m,p9] or p9|^(p9 |-count m)=x & P2[n,m,p9
] by A21;
then x in X1 or x in X2;
hence x in X1 \/ X2 by XBOOLE_0:def 3;
end;
then
A22: X c= X1 \/ X2;
now
let x be object;
assume x in X2;
then
ex p9 being prime Element of NAT st p9|^(p9 |-count m)=x & P2[n,m,p9];
hence x in X by A6;
end;
then
A23: X2 c= X;
then X2 c= Seg m by A7;
then
a24: X2 is included_in_Seg by FINSEQ_1:def 13;
reconsider m1 as non zero Element of NAT by ORDINAL1:def 12;
A25: now
assume p|^(p |-count m) in X11;
then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p |-count
m) & P11[n,m,p9];
hence contradiction;
end;
assume p|^(p |-count m) in X;
then p|^(p |-count m) in X1 by A22,A2,XBOOLE_0:def 3;
then p|^(p |-count m) in X12 by A5,A25,XBOOLE_0:def 3;
then for x being object st x in {p|^(p |-count m)} holds x in X12 by
TARSKI:def 1;
then
A26: {p|^(p |-count m)} c= X12;
for p being Prime, n being Element of NAT, m being non zero Element of
NAT , X11 being set st X11 = {p9|^(p9 |-count m) where p9 is prime Element of
NAT: P11[n,m,p9]} & not p|^(p |-count m) in X11 holds p |-count (Product Sgm
X11) = 0 from scheme2;
then
A27: p |-count (Product Sgm X11) = 0 by A25;
for p being Prime, n being Element of NAT, m being non zero Element of
NAT , X11 being set st X11 = {p9|^(p9 |-count m) where p9 is prime Element of
NAT: P11[n,m,p9]} holds Product Sgm X11 > 0 from scheme1;
then
A28: Product Sgm(X11) <> 0;
X1 \/ X2 c= X \/ X by A12,A23,XBOOLE_1:13;
then Sum (p |-count (Sgm X)) = Sum (p |-count (Sgm (X1 \/ X2))) by A22,
XBOOLE_0:def 10
.= Sum (p |-count (Sgm(X1) ^ Sgm(X2))) by a13,a24,A1,FINSEQ_3:42
.= Sum ((p |-count Sgm(X1)) ^ (p |-count Sgm(X2))) by Th50
.= Sum (p |-count Sgm(X1)) + Sum (p |-count Sgm(X2)) by RVSUM_1:75;
then p |-count (Product Sgm X) = Sum (p |-count Sgm(X1)) + Sum (p |-count
Sgm(X2)) by A9,Th52
.= Sum (p |-count Sgm(X1)) + 0 by A20,A19,Th52
.= 0 + Sum (p |-count Sgm(X12)) by A18,A28,A27,Th52
.= Sum (p |-count Sgm({p|^(p |-count m)})) by A26,A8,XBOOLE_0:def 10
.= Sum (p |-count <* m1 *>) by FINSEQ_3:44
.= Sum <* p |-count m1 *> by Th51
.= p |-count m1 by RVSUM_1:73;
hence thesis by A11;
end;
Lm10: for n, m being Element of NAT st m = 2*n choose n & n>=3 holds m =
Product Sgm {p|^(p |-count m) where p is prime Element of NAT: p<=sqrt(2*n) & p
|-count m>0} * Product Sgm {p|^(p |-count m) where p is prime Element of NAT:
sqrt(2*n)<p & p<=2*n/3 & p |-count m>0} * Product Sgm {p|^(p |-count m) where p
is prime Element of NAT: n<p & p<=2*n & p |-count m>0}
proof
defpred P3[Element of NAT,Element of NAT,Prime] means $1<$3 & $3<=2*$1 & $3
|-count $2>0;
defpred P2[Element of NAT,Element of NAT,Prime] means sqrt(2*$1)<$3 & $3<=2*
$1/3 & $3 |-count $2>0;
defpred P1[Element of NAT,Element of NAT,Prime] means $3<=sqrt(2*$1) & $3
|-count $2>0;
let n, m be Element of NAT;
assume
A1: m = 2*n choose n;
set X3 = {p|^(p |-count m) where p is prime Element of NAT: P3[n,m,p]};
set X2 = {p|^(p |-count m) where p is prime Element of NAT: P2[n,m,p]};
set X1 = {p|^(p |-count m) where p is prime Element of NAT: P1[n,m,p]};
set f1 = Sgm X1;
set f2 = Sgm X2;
set f3 = Sgm X3;
set n1=Product f1;
set n2=Product f2;
set n3=Product f3;
A2: for p being Prime, n being Element of NAT, m being non zero Element of
NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT:
P2[n,m,p9]} & not p|^(p |-count m) in X holds p |-count (Product Sgm X) = 0
from scheme2;
set k = Product f1 * Product f2 * Product f3;
A3: for p being Prime, n being Element of NAT, m being non zero Element of
NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT:
P1[n,m,p9]} holds Product Sgm X > 0 from scheme1;
assume
A4: n >= 3;
A5: now
2*n<3*n by A4,XREAL_1:68;
then
A6: 2*n/3<3*n/3 by XREAL_1:74;
assume n<2*n/3;
hence contradiction by A6;
end;
A7: now
sqrt 2 < sqrt 3 & sqrt 3 <= sqrt n by A4,SQUARE_1:26,27;
then
A8: sqrt 2 < sqrt n by XXREAL_0:2;
sqrt n > 0 by A4,SQUARE_1:25;
then (sqrt 2)*(sqrt n) < (sqrt n)*(sqrt n) by A8,XREAL_1:68;
then sqrt(2*n) < (sqrt n)*(sqrt n) by SQUARE_1:29;
then
A9: sqrt(2*n) < sqrt(n^2) by SQUARE_1:29;
assume n<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 being Prime, n being Element of NAT, m being non zero Element of
NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT:
P3[n,m,p9]} holds Product Sgm X > 0 from scheme1;
then
A12: Product f3 > 0 by A10;
A13: for p being Prime, n being Element of NAT, m being non zero Element of
NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT:
P2[n,m,p9]} holds Product Sgm X > 0 from scheme1;
then
A14: Product f2 > 0 by A10;
A15: for p being Prime, n being Element of NAT, m being non zero Element of
NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT:
P3[n,m,p9]} & not p|^(p |-count m) in X holds p |-count (Product Sgm X) = 0
from scheme2;
A16: for p being Prime, n being Element of NAT, m being non zero Element of
NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT:
P1[n,m,p9]} & not p|^(p |-count m) in X holds p |-count (Product Sgm X) = 0
from scheme2;
A17: for p being Prime st p>2*n holds p |-count n1 = 0 & p |-count n2 = 0 &
p |-count n3 = 0
proof
let p be Prime;
assume
A18: p>2*n;
then
A19: p |-count m = 0 by A1,A4,Lm9;
now
assume p|^(p |-count m) in X1;
then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p
|-count m) & P1[n,m,p9];
hence contradiction by A10,A19,Th22;
end;
hence p |-count n1 = 0 by A10,A16;
now
assume p|^(p |-count m) in X2;
then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p
|-count m) & P2[n,m,p9];
hence contradiction by A10,A19,Th22;
end;
hence p |-count n2 = 0 by A10,A2;
now
assume p|^(p |-count m) in X3;
then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p
|-count m) & P3[n,m,p9];
hence contradiction by A10,A18,Th22;
end;
hence thesis by A10,A15;
end;
A20: for p being Prime st 2*n/3<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 being 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 being 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 being 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 being Prime, n being Element of NAT, m being non zero Element of
NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT:
P2[n,m,p9]} & p|^(p |-count m) in X holds p |-count (Product Sgm X) = p |-count
m from scheme3;
A25: for p being 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 being 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 being 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 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p
|-count m)& P2[n,m,p9];
hence contradiction by A10,A29,Th22;
end;
hence thesis by A10,A2,A29;
end;
end;
A30: for p being Prime, n being Element of NAT, m being non zero Element of
NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT:
P3[n,m,p9]} & p|^(p |-count m) in X holds p |-count (Product Sgm X) = p |-count
m from scheme3;
A31: for p being Prime st n<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 being 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 being 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 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p
|-count m)& P3[n,m,p9];
hence contradiction by A10,A35,Th22;
end;
hence thesis by A10,A15,A35;
end;
end;
A36: for p being Prime, n being Element of NAT, m being non zero Element of
NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT:
P1[n,m,p9]} & p|^(p |-count m) in X holds p |-count (Product Sgm X) = p |-count
m from scheme3;
A37: for p being Prime st p<=sqrt(2*n) holds p |-count n2 = 0 & p |-count n3
= 0 & p |-count n1 = p |-count m
proof
let p be Prime;
A38: p in NAT by ORDINAL1:def 12;
assume
A39: p<=sqrt(2*n);
now
assume p|^(p |-count m) in X2;
then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p
|-count m) & P2[n,m,p9];
hence contradiction by A10,A39,Th22;
end;
hence p |-count n2 = 0 by A10,A2;
now
assume p|^(p |-count m) in X3;
then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p
|-count m) & P3[n,m,p9];
then n<p by A10,Th22;
hence contradiction by A7,A39,XXREAL_0:2;
end;
hence p |-count n3 = 0 by A10,A15;
per cases;
suppose
p |-count m > 0;
then p|^(p |-count m) in X1 by A39,A38;
hence thesis by A10,A36;
end;
suppose
A40: p |-count m = 0;
now
assume p|^(p |-count m) in X1;
then ex p9 being prime Element of NAT st p9|^(p9 |-count m)=p|^(p
|-count m)& P1[n,m,p9];
hence contradiction by A10,A40,Th22;
end;
hence thesis by A10,A16,A40;
end;
end;
A41: for p being Element of NAT st p is prime holds p |-count m = p |-count k
proof
reconsider n3 as non zero Element of NAT by A10,A11;
reconsider n2 as non zero Element of NAT by A10,A13;
reconsider n1 as non zero Element of NAT by A10,A3;
let p be Element of NAT;
assume
A42: p is prime;
then
A43: p |-count k = (p |-count (n1*n2)) + (p |-count n3) by NAT_3:28
.= (p |-count n1)+(p |-count n2)+(p |-count n3) by A42,NAT_3:28;
per cases;
suppose
A44: p>2*n;
then
A45: p |-count n2 = 0 by A17,A42;
p |-count m = 0 & p |-count n1 = 0 by A1,A4,A17,A42,A44,Lm9;
hence thesis by A17,A42,A43,A44,A45;
end;
suppose
A46: n<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
scheme4 { A(set,set) -> set, P[set,set] } : for n,m being Element of NAT, r
being Real, X being finite set st X = {A(p,m) where p is prime Element of NAT:
p <= r & P[p,m]} & r>=0 holds card X <= [\ r /] proof
let n,m be Element of NAT;
defpred P1[Nat] means for n,m being Element of NAT, r being Real,
X being finite set st X = {A(p,m) where p is prime Element of NAT: p <= r & P[p
,m]} & r>=0 & $1 = [\ r /] holds card X <= [\ r /];
A1: for n being Nat st P1[n] holds P1[n+1]
proof
let n be Nat;
assume
A2: P1[n];
now
let m be Element of NAT;
let r be Real;
let X be finite set;
set r1 = r - 1;
set X1 = {A(p,m) where p is prime Element of NAT: p <= r1 & P[p,m]};
set X2 = {A(p,m) where p is prime Element of NAT: r1 < p & p <= r & P[p,
m]};
A3: 0+n <= 1+n by XREAL_1:6;
assume
A4: X = {A(p,m) where p is prime Element of NAT: p <= r & P[p,m]};
now
let x be object;
assume
A5: x in X1 \/ X2;
per cases by A5,XBOOLE_0:def 3;
suppose
x in X1;
then consider p being prime Element of NAT such that
A6: A(p,m)=x and
A7: p<=r1 and
A8: P[p,m];
-1+r<=0+r by XREAL_1:6;
then p<=r by A7,XXREAL_0:2;
hence x in X by A4,A6,A8;
end;
suppose
x in X2;
then
ex p being prime Element of NAT st A(p,m)=x & r1 < p & p<=r & P
[p,m];
hence x in X by A4;
end;
end;
then
A9: X1 \/ X2 c= X;
assume r >= 0;
now
let x be object;
assume x in X;
then consider p being prime Element of NAT such that
A10: A(p,m)=x & p<=r & P[p,m] by A4;
A(p,m)=x & p<=r1 & P[p,m] or A(p,m)=x & r1<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;
then
A15: card X1 <= [\ r1 /] by A2,A13;
per cases;
suppose
not ex x being object st x in X2;
then X2={} by XBOOLE_0:def 1;
hence card X <= [\ r /] by A12,A13,A11,A15,A3,XXREAL_0:2;
end;
suppose
A16: ex x being set st x in X2;
then consider x be set such that
A17: x in X2;
A18: now
assume X2<>{x};
then consider y be object such that
A19: y in X2 and
A20: y<>x by A16,ZFMISC_1:35;
consider p1 be prime Element of NAT such that
A21: A(p1,m)=x and
A22: r1<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 is 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 being Nat holds P1[n] from NAT_1:sch 2(A24,A1);
let r be Real;
let X be finite set;
assume that
A30: X = {A(p,m) where p is prime Element of NAT: p <= r & P[p,m]} and
A31: r>=0;
[\ r /] is Element of NAT by A31,INT_1:53;
hence thesis by A29,A30,A31;
end;
Lm11: for n, m being Element of NAT st m = 2*n choose n & n>=3 holds Product
Sgm {p|^(p |-count m) where p is prime Element of NAT: p<=sqrt(2*n) & p |-count
m>0} <= (2*n) to_power sqrt(2*n)
proof
deffunc A(Element of NAT,Element of NAT) = $1|^($1 |-count $2);
defpred P[Element of NAT,Element of NAT] means $1 |-count $2 > 0;
let n, m be Element of NAT;
assume
A1: m = 2*n choose n;
set r = sqrt(2*n);
A2: r>=0 by SQUARE_1:def 2;
A3: for n,m being Element of NAT, r being Real, X being finite set st X = {
A(k,m) where k is prime Element of NAT: k <= r & P[k,m]} & r>=0 holds card X <=
[\ r /] from scheme4;
set XX=Seg m;
set X = {p|^(p |-count m) where p is prime Element of NAT: p<=sqrt(2*n) & p
|-count m>0};
assume
A4: n>=3;
set f1 = Sgm X;
set f2 = (len f1) |-> (2*n);
m * (2*n) >= 4|^n / (2*n) * (2*n) by A1,Th6,XREAL_1:64;
then
A5: m<>0 by A4;
now
let x be object;
assume x in X;
then consider p being prime Element of NAT such that
B1: p|^(p |-count m) = x & p<=sqrt(2*n) & p |-count m>0;
1 <= p|^(p |-count m) <= m by A5,Th16;
hence x in XX by B1,FINSEQ_1:1;
end;
then
A6: X c= Seg m;
then
a6: X is included_in_Seg by FINSEQ_1:def 13;
A7: now
let k be Element of NAT;
assume
A8: k in dom f1;
rng f1 = X by a6,FINSEQ_1:def 14;
then f1.k in X by A8,FUNCT_1:3;
then
A9: ex p being prime Element of NAT st p|^(p |-count m)=f1.k & p<=sqrt(2*
n) & p |-count m>0;
k in Seg len f1 by A8,FINSEQ_1:def 3;
then f2.k = 2*n by FUNCOP_1:7;
hence f1.k<=f2.k & f1.k>0 by A1,A4,A9,Lm9;
end;
reconsider X as finite set by A6;
A10: len f1 = len f2 by CARD_1:def 7;
rng f1 c= REAL;
then reconsider f1 as FinSequence of REAL by FINSEQ_1:def 4;
A11: rng f2 c= REAL;
reconsider rr=r as Real;
A12: rr >= 0 by A2;
len f1 = card X by a6,FINSEQ_3:39;
then [\ sqrt(2*n) /] <= sqrt(2*n) & len f1 <= [\ sqrt(2*n) /] by A12,A3,
INT_1:def 6;
then len f1 <= sqrt(2*n) by XXREAL_0:2;
then
A13: len f1 < sqrt(2*n) or len f1 = sqrt(2*n) by XXREAL_0:1;
reconsider f2 as FinSequence of REAL by A11,FINSEQ_1:def 4;
Product f1 <= Product f2 by A10,A7,Th53;
then
A14: Product f1 <= (2*n) to_power len(f1) by A4,Th54;
n*2 >= 3*2 by A4,XREAL_1:64;
then 2*n > 1 by XXREAL_0:2;
then (2*n) to_power len f1 <= (2*n) to_power sqrt(2*n) by A13,POWER:39;
hence thesis by A14,XXREAL_0:2;
end;
begin :: Bertrand's postulate.
::$N Bertrand's postulate
::$L https://en.wikipedia.org/wiki/Bertrand's_postulate Bertrand's postulate
theorem
for n being Nat st n >= 1 ex p being Prime st n < p & p <= 2*n
proof
let n be Nat;
assume
A1: n>=1;
AA: n in NAT by ORDINAL1:def 12;
per cases;
suppose
n<4000;
then n<4001 by XXREAL_0:2;
hence thesis by A1,AA,Lm7;
end;
suppose
A2: n>=4000;
set m = 2*n choose n;
set X1={p|^(p |-count m) where p is prime Element of NAT: p<=sqrt(2*n) & p
|-count m>0};
set X2={p|^(p |-count m) where p is prime Element of NAT: sqrt(2*n)<p & p
<=2*n/3 & p |-count m>0};
set X3={p|^(p |-count m) where p is prime Element of NAT: n<p & p<=2*n & p
|-count m>0};
assume
A3: not ex p being Prime st n<p & p<=2*n;
now
assume X3<>{};
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<p & p<=2*n &
p |-count m>0 by A4;
hence contradiction by A3;
end;
then
A5: m = (Product Sgm X1)*(Product Sgm X2)*1
by AA,A2,Lm10,FINSEQ_3:43,RVSUM_1:94,XXREAL_0:2;
A6: 4|^n / (2*n) <= m by Th6;
set X = {p where p is prime Element of NAT: p<=2*n/3};
A7: n>=3 by A2,XXREAL_0:2;
then n/3>=3/3 by XREAL_1:72;
then (n/3)*2>=1*2 by XREAL_1:64;
then
A8: Product Sgm X <= (4 to_power ((2*n/3)-1)) by Th45;
set mm=[/ 2*n/3 \];
reconsider mm as Element of NAT by INT_1:53;
set XX=Seg mm;
A9: now
assume {} in X;
then ex p being prime Element of NAT st p = {} & p<=2*n/3;
hence contradiction;
end;
-1+(2*n/3)<0+(2*n/3) by XREAL_1:6;
then
A10: 4 to_power ((2*n/3)-1) < 4 to_power (2*n/3) by POWER:39;
now
let x be object;
assume x in X2;
then consider p be prime Element of NAT such that
A11: p|^(p |-count m)=x and
A12: sqrt(2*n)<p and
A13: p<=2*n/3 and
A14: p |-count m>0;
p |-count m <= 1 by AA,A7,A12,A13,Lm9;
then p |-count m < 1+1 by NAT_1:13;
then p |-count m = 1 by A14,NAT_1:23;
then p=x by A11;
hence x in X by A13;
end;
then
A15: X2 c= X;
now
let x be object;
assume x in X;
then consider p being prime Element of NAT such that
A16: p = x and
A17: p<=2*n/3;
A18: 1<=p by INT_2:def 4;
2*n/3<=[/ 2*n/3 \] by INT_1:def 7;
then p<=[/ 2*n/3 \] by A17,XXREAL_0:2;
hence x in XX by A16,A18,FINSEQ_1:1;
end;
then
A19: X c= Seg mm;
then X c= NAT by XBOOLE_1:1;
then Product Sgm X2 <= Product Sgm X by A19,A9,A15,Th42;
then
A20: Product Sgm X2 <= (4 to_power ((2*n/3)-1)) by A8,XXREAL_0:2;
n>=3 by A2,XXREAL_0:2;
then Product Sgm X1 <= (2*n) to_power sqrt(2*n) by AA,Lm11;
then m <= ((2*n) to_power sqrt(2*n))*(4 to_power ((2*n/3)-1)) by A20,A5,
XREAL_1:66;
then
A21: 4|^n / (2*n) <= ((2*n) to_power sqrt(2*n))*(4 to_power ((2*n/3)-1 ))
by A6,XXREAL_0:2;
A22: 4 to_power (2*n/3)>0 by POWER:34;
(2*n) to_power sqrt(2*n)>0 by A2,POWER:34;
then
(4 to_power ((2*n/3)-1))*((2*n) to_power sqrt(2*n)) < (4 to_power (2*
n/3))*((2*n) to_power sqrt(2*n)) by A10,XREAL_1:68;
then 4|^n / (2*n) <= ((2*n) to_power sqrt(2*n))*(4 to_power (2*n/3)) by A21
,XXREAL_0:2;
then
4|^n/(2*n)*(2*n)<=((2*n) to_power sqrt(2*n))*(4 to_power (2*n/3))*(2*
n) by XREAL_1:64;
then
4|^n = 4 to_power (3*n/3) & 4|^n<=((2*n) to_power sqrt(2*n))*(2*n)*(4
to_power (2*n/3)) by A2,POWER:41,XCMPLX_1:87;
then
(4 to_power (3*n/3))/(4 to_power (2*n/3)) <= (((2*n) to_power sqrt(2*
n))*(2*n))* (4 to_power (2*n/3))/(4 to_power (2*n/3)) by A22,XREAL_1:72;
then
(4 to_power (3*n/3))/(4 to_power (2*n/3)) <= ((2*n) to_power sqrt(2*n
))*(2*n) by A22,XCMPLX_1:89;
then 4 to_power ((3*n/3)-(2*n/3)) <= ((2*n) to_power sqrt(2*n))*(2*n) by
POWER:29;
then 4 to_power (n/3) <= ((2*n) to_power sqrt(2*n))*((2*n) to_power 1) by
POWER:25;
then 4 to_power (n/3) <= (2*n) to_power (sqrt(2*n)+1) by A2,POWER:27;
then
A23: 4 to_power (n/3) < (2*n) to_power (sqrt(2*n)+1) or 4 to_power (n/3) =
(2*n) to_power (sqrt(2*n)+1) by XXREAL_0:1;
4 to_power (n/3)>0 by POWER:34;
then (4 to_power (n/3)) to_power 3 <= ((2*n) to_power (sqrt(2*n)+1))
to_power 3 by A23,POWER:37;
then 4 to_power ((n/3)*3) <= ((2*n) to_power (sqrt(2*n)+1)) to_power 3 by
POWER:33;
then
A24: 4 to_power n <= (2*n) to_power ((sqrt(2*n)+1)*3) by A2,POWER:33;
reconsider 2n=2*n as Real;
A25: 6-root(2*n) to_power 6 = 6-root(2n) |^ 6 by POWER:41
.= 2n by COMPTRIG:4;
2 to_power 2 = 2|^2 by POWER:41
.= Product <* 2, 2 *> by FINSEQ_2:61
.= 2*2 by RVSUM_1:99;
then
A26: 2 to_power (2*n)>0 & 4 to_power n = 2 to_power (2*n) by POWER:33,34;
set n1=[\ 6-root(2*n) /];
6-root(2*n) -1 < n1 by INT_1:def 6;
then
A27: 6-root(2*n) -1 +1 < n1 +1 by XREAL_1:6;
6-root(2*n) > 6-root 0 by A2,POWER:17;
then
A28: 6-root(2*n) > 0 by POWER:5;
then reconsider n1 as Element of NAT by INT_1:53;
n1 <= 6-root(2*n) by INT_1:def 6;
then n1 < 6-root(2*n) or n1 = 6-root(2*n) by XXREAL_0:1;
then
A29: 2 to_power n1 <= 2 to_power (6-root(2*n)) by POWER:39;
n1+1 <= 2|^n1 by NEWTON:85;
then n1+1 <= 2 to_power n1 by POWER:41;
then n1+1 <= 2 to_power (6-root(2*n)) by A29,XXREAL_0:2;
then
n1+1 < 2 to_power (6-root(2*n)) or n1+1 = 2 to_power (6-root(2*n)) by
XXREAL_0:1;
then
A30: (n1+1) to_power 6 <= (2 to_power (6-root(2*n))) to_power 6 by POWER:37;
6-root(2*n) to_power 6 < (n1+1) to_power 6 by A27,A28,POWER:37;
then 2*n < (2 to_power (6-root(2*n))) to_power 6 by A30,A25,XXREAL_0:2;
then
A31: 2*n < 2 to_power ((6-root(2*n))*6) by POWER:33;
sqrt(2*n)>0 by A2,SQUARE_1:25;
then (2*n) to_power ((sqrt(2*n)+1)*3) < (2 to_power ((6-root(2*n))*6))
to_power ((sqrt(2*n)+1)*3) by A2,A31,POWER:37;
then
4 to_power n < (2 to_power ((6-root(2*n))*6)) to_power ((sqrt(2*n)+1)
*3) by A24,XXREAL_0:2;
then 4 to_power n < 2 to_power (((6-root(2*n))*6)*((sqrt(2*n)+1)*3)) by
POWER:33;
then
log(2,2 to_power (2*n)) < log(2,2 to_power (((6-root(2*n))*6)*((sqrt(
2*n)+1)*3))) by A26,POWER:57;
then
(2*n)*log(2,2) < log(2,2 to_power (((6-root(2*n))*6)*((sqrt(2*n)+1)*3
))) by POWER:55;
then (2*n)*log(2,2) < (((6-root(2*n))*6)*((sqrt(2*n)+1)*3))*log(2,2) by
POWER:55;
then (2*n)*1 < (((6-root(2*n))*6)*((sqrt(2*n)+1)*3))*log(2,2) by POWER:52;
then
A32: 2*n < (((6-root(2*n))*6)*((sqrt(2*n)+1)*3))*1 by POWER:52;
42 < n by A2,XXREAL_0:2;
then 42*2 < n*2 by XREAL_1:68;
then 81 < 2*n by XXREAL_0:2;
then
A33: sqrt(81) < sqrt(2*n) by SQUARE_1:27;
81=9^2;
then sqrt 81 = 9 by SQUARE_1:22;
then 9*2 < sqrt(2*n)*2 by A33,XREAL_1:68;
then 18 + 18*sqrt(2*n) < 2*sqrt(2*n)+18*sqrt(2*n) by XREAL_1:6;
then
(18 + 18*sqrt(2*n))*(6-root(2*n)) < 20*sqrt(2*n)*(6-root(2*n)) by A28,
XREAL_1:68;
then 2*n < 20*(sqrt(2*n)*(6-root(2*n))) by A32,XXREAL_0:2;
then 2*n < 20*((2-Root(2*n))*(6-root(2*n))) by PREPOWER:32;
then 2*n < 20*((2-root(2*n))*(6-root(2*n))) by POWER:def 1;
then 2*n < 20*(((2*n) to_power (1/2))*(6-root(2*n))) by POWER:45;
then 2*n < 20*(((2*n) to_power (1/2))*((2*n) to_power (1/6))) by POWER:45;
then
A34: 2*n < 20*((2*n) to_power (1/2+1/6)) by A2,POWER:27;
A35: (2*n) to_power (2/3)<>0 by A2,POWER:34;
(2*n) to_power (2/3)>0 by A2,POWER:34;
then (2*n)/((2*n) to_power (2/3)) < 20*((2*n) to_power (2/3))/((2*n)
to_power (2/3)) by A34,XREAL_1:74;
then (2*n)/((2*n) to_power (2/3)) < 20 by A35,XCMPLX_1:89;
then ((2*n) to_power 1)/((2*n) to_power (2/3)) < 20 by POWER:25;
then
A36: ((2*n) to_power (1-(2/3))) < 20 by A2,POWER:29;
(2*n) to_power (1/3)>0 by A2,POWER:34;
then ((2*n) to_power (1/3)) to_power 3 < 20 to_power 3 by A36,POWER:37;
then ((2*n) to_power ((1/3)*3)) < 20 to_power 3 by A2,POWER:33;
then 2*n < 20 to_power (2+1) by POWER:25;
then 2*n < (20 to_power 2)*(20 to_power 1) by POWER:27;
then 2*n < (20 to_power (1+1))*20 by POWER:25;
then 2*n < (20 to_power 1)*(20 to_power 1)*20 by POWER:27;
then 2*n < (20 to_power 1)*20*20 by POWER:25;
then 2*n < 20*20*20 by POWER:25;
then 2*n/2 < 8000/2 by XREAL_1:74;
hence contradiction by A2;
end;
end;
theorem
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 by Lm4;
theorem
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 by Lm4;
theorem
for n being Nat st n < 5 & n is prime holds n = 2 or n = 3 by Lm2;
theorem
for k being Nat st k < 25 holds
for n being Nat st n*n <= k & n is prime holds n = 2 or n = 3 by Lm3;
theorem
for n being Nat st 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
by Lm5;
theorem
for k being Nat st k < 841 holds
for n being Nat st 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
by Lm6;
theorem
for p being Nat holds not p is prime iff p <= 1 or
ex n being Element of NAT st n divides p & 1 < n & n*n <= p
proof
let p be Nat;
thus not p is prime implies p <= 1 or
ex n being Element of NAT st n divides p & 1 < n & n*n <= p
proof
assume not p is prime;
then per cases by Th12;
suppose p <= 1;
hence thesis;
end;
suppose ex n being Element of NAT st n divides p & 1 < n & n < p;
hence thesis by Th8;
end;
end;
assume p <= 1 or
ex n being Element of NAT st n divides p & 1 < n & n*n <= p;
then per cases;
suppose p <= 1;
hence thesis by INT_2:def 4;
end;
suppose ex n being Element of NAT st n divides p & 1 < n & n*n <= p;
then consider n being Element of NAT such that
A1: n divides p and
A2: 1 < n and
A3: n*n <= p;
n*1 < n*n by A2,XREAL_1:68;
hence thesis by A1,A3,INT_2:def 4;
end;
end;