:: Public-Key Cryptography and Pepin's Test for the Primality of
:: Fermat Numbers
:: by Yoshinori Fujisawa , Yasushi Fuwa and Hidetaka Shimizu
::
:: Received December 21, 1998
:: Copyright (c) 1998-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, NAT_1, INT_1, XXREAL_0, RELAT_1, ARYTM_3, CARD_1,
NEWTON, ARYTM_1, INT_2, SUBSET_1, SQUARE_1, ORDINAL1, ABIAN, POWER,
EULER_1, TARSKI, SETWOP_2, FINSET_1, XBOOLE_0, PEPIN, REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
XREAL_0, INT_1, INT_2, NAT_1, NAT_D, SETWOP_2, POWER, ABIAN, SQUARE_1,
NEWTON, EULER_1, FINSET_1, XXREAL_0;
constructors SQUARE_1, NAT_1, NAT_D, SETWOP_2, NEWTON, SERIES_1, BINARITH,
EULER_1, ABIAN, VALUED_1, XXREAL_2;
registrations ORDINAL1, FINSET_1, FINSUB_1, XXREAL_0, XREAL_0, NAT_1, INT_1,
NEWTON, ABIAN, SERIES_1, POWER, CARD_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, INT_1;
equalities INT_1, SQUARE_1, XCMPLX_0;
expansions INT_1;
theorems NAT_1, NAT_2, INT_1, INT_2, FINSEQ_1, EULER_1, EULER_2, PREPOWER,
PRE_FF, POWER, NEWTON, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1,
NAT_D, XREAL_0;
schemes NAT_1;
begin :: Some selected Basic Theorems
reserve d,i,j,k,m,n,p,q,x,k1,k2 for Nat,
a,c,i1,i2,i3,i5 for Integer;
Lm1: for n,x,y be Nat holds n > 1 & x >= 1 & 1 = (x*y*n + x + y) implies x = 1
& y = 0
proof
let n,x,y be Nat;
assume that
A1: n > 1 and
A2: x >= 1 and
A3: 1 = (x*y*n + x + y);
now
per cases by A2,XXREAL_0:1;
suppose
A4: x > 1;
now
per cases;
suppose
A5: y > 0;
then x*y > 1*y by A4,XREAL_1:68;
then (x*y)*n > 1*(x*y) by A1,XREAL_1:68;
then x*y*n + x > 0 + x by XREAL_1:6;
then
A6: x*y*n + x > 1 by A4,XXREAL_0:2;
y + 1 > 0 + 1 by A5,XREAL_1:6;
hence thesis by A3,A6,XREAL_1:6;
end;
suppose
y = 0;
hence thesis by A3;
end;
end;
hence thesis;
end;
suppose
A7: x = 1;
now
per cases;
suppose
A8: y > 0;
then x*y*n > 0 by A1,A7,XREAL_1:68;
then
A9: x*y*n + x > 0 + 1 by A7,XREAL_1:6;
y + 1 > 0 + 1 by A8,XREAL_1:6;
hence thesis by A3,A9,XREAL_1:6;
end;
suppose
y = 0;
hence thesis by A7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Lm2: 2 |^ (2 |^ n) > 1
proof
defpred P[Nat] means 2 |^ (2 |^ $1) > 1;
A1: for k holds P[k] implies P[k+1]
proof
let k;
assume
A2: 2 |^ (2 |^ k) > 1;
then 2 |^ (2 |^ k) < (2 |^ (2 |^ k)) |^ 2 by PREPOWER:13;
then 2 |^ (k + 1) = (2 |^ k)*2 & 1 < (2 |^ (2 |^ k)) |^ 2 by A2,NEWTON:6
,XXREAL_0:2;
hence thesis by NEWTON:9;
end;
2 |^ 0 = 1 by NEWTON:4;
then 2 |^ (2 |^ 0) = 2;
then
A3: P[0];
for n holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
Lm4: n <> 0 implies n -'1 + 1 = (n + 1) -' 1
proof
assume n <> 0;
then n >= 1 by NAT_1:14;
then n - 1 >= 1 - 1 by XREAL_1:9;
then n -' 1 + 1 = n + -1 + 1 by XREAL_0:def 2
.= n + 1 - 1;
hence thesis by XREAL_0:def 2;
end;
theorem
for i being Nat holds i,i+1 are_coprime
proof
let k be Nat;
k gcd (k+1) = (1+k*1) gcd k .= 1 gcd k by EULER_1:8
.= 1 by NEWTON:51;
hence thesis by INT_2:def 3;
end;
theorem Th2:
for p being Nat holds p is prime implies m,p are_coprime or m gcd p = p
proof
let p be Nat;
A1: m gcd p divides p by NAT_D:def 5;
assume p is prime;
then m gcd p = 1 or m gcd p = p by A1,INT_2:def 4;
hence thesis by INT_2:def 3;
end;
theorem Th3:
for k,m,n being Nat holds k divides n*m & n,k are_coprime implies k divides m
proof
let k,m,n be Nat;
assume that
A1: k divides n*m and
A2: n,k are_coprime;
reconsider k,m,n as Element of NAT by ORDINAL1:def 12;
n gcd k = 1 by A2,INT_2:def 3;
then
A3: (n*m gcd k*m) = m by EULER_1:5;
k divides k*m;
hence thesis by A1,A3,NEWTON:50;
end;
theorem Th4:
n divides m & k divides m & n,k are_coprime implies (n*k) divides m
proof
assume that
A1: n divides m and
A2: k divides m & n,k are_coprime;
consider t1 be Nat such that
A3: m = n*t1 by A1,NAT_D:def 3;
k divides t1 by A2,A3,Th3;
then consider t2 be Nat such that
A4: t1 = k*t2 by NAT_D:def 3;
m = (n*k)*t2 by A3,A4;
hence thesis;
end;
registration
let i be Integer;
cluster i^2 -> natural;
coherence
proof
i^2 in NAT by INT_1:3,XREAL_1:63;
hence thesis;
end;
end;
theorem
c > 1 implies 1 mod c = 1
proof
assume
A1: c > 1;
then 1 div c = 0 by PRE_FF:4;
then 1 mod c = 1 - 0*c by A1,INT_1:def 10;
hence thesis;
end;
theorem Th6:
for i,n be Nat st i <> 0 holds i divides n iff n mod i = 0
proof
let i,n be Nat;
assume
A1: i <> 0;
A2: n mod i = 0 implies i divides n
proof
assume n mod i = 0;
then ex t being Nat st n = i*t + 0 & 0 < i by A1,NAT_D:def 2;
hence thesis;
end;
i divides n implies n mod i = 0
proof
assume i divides n;
then ex t being Nat st n = i*t by NAT_D:def 3;
hence thesis;
end;
thus thesis by A2;
end;
theorem Th7:
for m,n being Nat holds m <> 0 & m divides n mod m implies m divides n
proof
let m,n be Nat;
assume that
A1: m <> 0 and
A2: m divides n mod m;
consider x be Nat such that
A3: n mod m = m * x by A2,NAT_D:def 3;
n mod m + m * (n div m) = m * (x + (n div m)) by A3;
then n = m * (x + (n div m)) by A1,NAT_D:2;
hence thesis;
end;
theorem
for m,n,k being Nat holds 0 < n & m mod n = k implies n divides (m - k)
proof
let m,n,k be Nat;
assume
A1: 0 < n & m mod n = k;
take m div n;
m = n*(m div n) + k by A1,NAT_D:2;
hence thesis;
end;
theorem
i*p <> 0 & k mod i*p < p implies k mod i*p = k mod p
proof
assume that
A1: i*p <> 0 and
A2: k mod i*p < p;
set T = k mod i*p;
consider n being Nat such that
A3: k = (i*p)*n + T and
T < i*p by A1,NAT_D:def 2;
k = p*(i*n) + T by A3;
then k mod p = T mod p by NAT_D:21
.= T by A2,NAT_D:24;
hence thesis;
end;
theorem Th10:
(a*p + 1) mod p = 1 mod p
proof
per cases;
suppose
A1: p <> 0;
reconsider p as Integer;
(a*p + 1) mod p = (a*p + 1) - ((a*p + 1) div p)*p by A1,INT_1:def 10
.= (a*p + 1) - ([\(a*p/p)+(1/p)/])*p
.= (a*p + 1) - ([\(a)+(1/p)/])*p by A1,XCMPLX_1:89
.= (a*p + 1) - (a+[\(1/p)/])*p by INT_1:28
.= 1 - (1 div p)*p;
hence thesis by A1,INT_1:def 10;
end;
suppose
p = 0;
hence thesis;
end;
end;
theorem Th11:
1 < m & (n*k) mod m = k mod m & k,m are_coprime implies n mod m = 1
proof
assume that
A1: 1 < m and
A2: (n*k) mod m = k mod m and
A3: k,m are_coprime;
consider t2 being Nat such that
A4: k = m*t2 + (k mod m) and
(k mod m) < m by A1,NAT_D:def 2;
consider t1 being Nat such that
A5: n*k = m*t1 + ((n*k) mod m) and
((n*k) mod m) < m by A1,NAT_D:def 2;
n*k - 1*k = m*(t1 - t2) by A2,A5,A4;
then
A6: m divides k*(n - 1);
reconsider n,m as Integer;
m divides (n - 1) by A3,A6,INT_2:25;
then consider tt being Integer such that
A7: n - 1 = m*tt;
n = m*tt + 1 by A7;
then n mod m = (1 qua Integer) mod m by NAT_D:61
.= 1 by A1,NAT_D:14;
hence thesis;
end;
theorem
(p |^ k) mod m = ((p mod m) |^ k) mod m by EULER_2:22;
Lm5: k*(2 |^ (n+1)) div 2 = k*(2 |^ n)
proof
k*(2 |^ (n+1)) = k*(2 |^ n*2) by NEWTON:6
.= k*2 |^ n*2;
hence thesis;
end;
Lm6: k <= n implies m |^ k divides m |^ n
proof
assume k <= n;
then consider t being Nat such that
A1: n = k + t by NAT_1:10;
m |^ n = (m |^ k)*(m |^ t) by A1,NEWTON:8;
hence thesis;
end;
theorem
i <> 0 implies i^2 mod (i+1) = 1
proof
assume
A1: i <> 0;
then
A2: i+1 > 0+1 by XREAL_1:6;
i >= 1 by A1,NAT_1:14;
then i-1 >= 1-1 by XREAL_1:9;
then reconsider I = i-1 as Element of NAT by INT_1:3;
reconsider II = (i+1)*I as Element of NAT;
i^2 mod (i+1) = (II + 1) mod (i+1)
.= (II mod (i+1) + 1) mod (i+1) by NAT_D:22
.= (0 + 1) mod (i+1)
.= 1 by A2,NAT_D:24;
hence thesis;
end;
theorem
k^2 < j & i mod j = k implies i^2 mod j = k^2
proof
assume that
A1: k^2 < j and
A2: i mod j = k;
consider n being Nat such that
A3: i = j*n + k and
k < j by A1,A2,NAT_D:def 2;
i^2 = j*((n*j*n) + (k*n) + (n*k)) + k^2 by A3;
then i^2 mod j = k^2 mod j by NAT_D:21;
hence thesis by A1,NAT_D:24;
end;
theorem
p is prime & i mod p = -1 implies i^2 mod p = 1
proof
assume that
A1: p is prime and
A2: i mod p = -1;
A3: p > 1 by A1,INT_2:def 4;
p <> 0 by A1,INT_2:def 4;
then i mod p = i - (i div p)*p by INT_1:def 10;
then i = (i div p)*p - 1 by A2;
then i^2 = ((((i div p)*p) - 2)*(i div p))*p + 1;
then i^2 mod p = 1 mod p by Th10
.= 1 by A3,NAT_D:24;
hence thesis;
end;
theorem
n is even implies n + 1 is odd;
theorem
for p being Nat holds p > 2 & p is prime implies p is odd
proof
let p be Nat;
assume
A1: p > 2 & p is prime;
assume p is even;
then p mod 2 = 0 by NAT_2:21;
then ex k being Nat st p = 2*k + 0 & 0 < 2 by NAT_D:def 2;
then 2 divides p;
hence contradiction by A1,INT_2:def 4;
end;
theorem
n > 0 implies 2 to_power(n) is even
proof
assume n > 0;
then 2 to_power(n) mod 2 = 0 by NAT_2:17;
hence thesis by NAT_2:21;
end;
theorem
i is odd & j is odd implies i*j is odd;
theorem
i is odd implies i |^ k is odd
proof
defpred P[Nat] means i |^ $1 is odd;
assume
A1: i is odd;
A2: for n holds P[n] implies P[n+1]
proof
let n;
A3: i |^ (n+1) = i |^ n * i by NEWTON:6;
assume i |^ n is odd;
hence thesis by A1,A3;
end;
i |^ 0 = 1 & 1 mod 2 = 1 by NAT_D:24,NEWTON:4;
then
A4: P[0] by NAT_2:22;
for n holds P[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th21:
k > 0 & i is even implies i |^ k is even
proof
assume that
A1: k > 0 and
A2: i is even;
defpred P[Nat] means $1 > 0 & i is even implies i |^ $1 is even;
A3: for n holds P[n] implies P[n+1]
proof
let n;
assume P[n];
P[n+1]
proof
now
(i |^ n)*i is even by A2;
hence thesis by NEWTON:6;
end;
hence thesis;
end;
hence thesis;
end;
A4: P[0];
for n holds P[n] from NAT_1:sch 2(A4,A3);
hence thesis by A1,A2;
end;
theorem
2 divides n iff n is even
proof
A1: n is even implies 2 divides n
proof
assume n is even;
then n mod 2 = 0 by NAT_2:21;
then ex k being Nat st n = 2*k + 0 & 0 < 2 by NAT_D:def 2;
hence thesis;
end;
thus thesis by A1;
end;
theorem
m*n is even implies m is even or n is even;
theorem Th24:
n |^ 2 = n^2
proof
n |^ 2 = n |^ (1 + 1) .= n |^ 1*n |^ 1 by NEWTON:8
.= n^2;
hence thesis;
end;
theorem Th25:
m > 1 & n > 0 implies m |^ n > 1
proof
assume that
A1: m > 1 and
A2: n > 0;
defpred P[Nat] means $1 > 0 implies m |^ $1 > 1;
A3: for n holds P[n] implies P[n+1]
proof
let n;
A4: m |^ (n+1) = (m |^ n)*(m |^ 1) by NEWTON:8
.= (m |^ n)*m;
assume
A5: P[n];
P[n+1]
proof
now
per cases;
suppose
n = 0;
hence thesis by A1;
end;
suppose
n <> 0;
then (m |^ n)*m > 1*m by A1,A5,XREAL_1:68;
hence thesis by A1,A4,XXREAL_0:2;
end;
end;
hence thesis;
end;
hence thesis;
end;
A6: P[0];
for n holds P[n] from NAT_1:sch 2(A6,A3);
hence thesis by A2;
end;
Lm8: (2 |^ (2 |^ n))^2 = (2 |^ (2 |^ (n + 1)))
proof
defpred P[Nat] means (2 |^ (2 |^ $1))^2 = (2 |^ (2 |^ ($1 + 1)));
A1: 2 |^ (2 |^ (0 + 1)) = 2 to_power 2
.= 2^2 by POWER:46;
A2: for k st P[k] holds P[k+1]
proof
let x;
assume
A3: (2 |^ (2 |^ x))^2 = (2 |^ (2 |^ (x + 1)));
(2 |^ (2 |^ (x + 1)))^2 = (2 |^ ((2 |^ x)*2))^2 by NEWTON:6
.= ((2 |^ (2 |^ x)) |^ 2)^2 by NEWTON:9
.= ((2 |^ (2 |^ x))^2)^2 by Th24
.= (2 |^ (2 |^ (x + 1))) |^ 2 by A3,Th24
.= 2 |^ ((2 |^ (x + 1))*2) by NEWTON:9
.= 2 |^ (2 |^ ((x + 1) + 1)) by NEWTON:6;
hence thesis;
end;
2 |^ 0 = 1 by NEWTON:4;
then
A4: P[0] by A1;
for k holds P[k] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th26:
n <> 0 & p <> 0 implies n |^ p = n*(n |^ (p -'1))
proof
assume
A1: n <> 0 & p <> 0;
defpred P[Nat] means n <> 0 & $1 <> 0 implies n |^ $1 = n*(n |^ ($1 -' 1));
A2: for m holds P[m] implies P[m+1]
proof
let m;
assume P[m];
now
per cases;
suppose
A3: m = 0;
n*(n |^ ((0+1) -' 1)) = n*(n |^ 0) by XREAL_1:232
.= n*1 by NEWTON:4;
hence thesis by A3;
end;
suppose
A4: m <> 0;
n |^ (m+1) = (n |^ m) * n by NEWTON:6
.= (n |^ (m -' 1 + 1))*n by A4,NAT_1:14,XREAL_1:235
.= n*(n |^ ((m + 1) -' 1)) by A4,Lm4;
hence thesis;
end;
end;
hence thesis;
end;
A5: P[0];
for m holds P[m] from NAT_1:sch 2(A5,A2);
hence thesis by A1;
end;
theorem Th27:
for n,m st m mod 2 = 0 holds (n |^ (m div 2))^2 = n |^ m
proof
let n,m;
assume
A1: m mod 2 = 0;
(n |^ (m div 2))^2 = n |^ ((m div 2) + (m div 2)) by NEWTON:8
.= n |^ ((m + m) div 2) by A1,NAT_D:19
.= n |^ ((2*m) div 2)
.= n |^ m;
hence thesis;
end;
theorem Th28:
n <> 0 & 1 <= k implies (n |^ k) div n = n |^ (k -'1)
proof
assume that
A1: n <> 0 and
A2: 1 <= k;
A3: k - 1 >= 1 - 1 by A2,XREAL_1:9;
k = k - 1 + 1 .= (k -'1) + 1 by A3,XREAL_0:def 2;
then n |^ k = n*(n |^ (k -'1)) by NEWTON:6;
hence thesis by A1,NAT_D:18;
end;
theorem
2 |^ (n + 1) = (2 |^ n)+(2 |^ n)
proof
defpred P[Nat] means 2 |^ ($1+1) = (2 |^ $1)+(2 |^ $1);
A1: for m st P[m] holds P[m+1]
proof
let m;
assume
A2: 2 |^ (m+1) = (2 |^ m)+(2 |^ m);
(2 |^ (m+1))+(2 |^ (m+1)) = 2*(2 |^ m)+(2 |^ (m+1)) by NEWTON:6
.= 2*(2 |^ m)+2*(2 |^ m) by NEWTON:6
.= 2*((2 |^ m)+(2 |^ m))
.= 2 |^ ((m+1)+1) by A2,NEWTON:6;
hence thesis;
end;
2 |^ (0+1) = 1 + 1
.= (2 |^ 0)+1 by NEWTON:4
.= (2 |^ 0)+(2 |^ 0) by NEWTON:4;
then
A3: P[0];
for n holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th30:
k > 1 & k |^ n = k |^ m implies n = m
proof
assume that
A1: k > 1 and
A2: k |^ n = k |^ m;
now
per cases;
suppose
n = m;
hence thesis;
end;
suppose
n <> m;
then k to_power m <> k to_power n by A1,POWER:50;
hence thesis by A2;
end;
end;
hence thesis;
end;
Lm9: k > n & x > 1 implies x |^ k > x |^ n
proof
assume that
A1: k>n and
A2: x > 1;
consider m be Nat such that
A3: k = n + m by A1,NAT_1:10;
m + n - n > n - n by A1,A3,XREAL_1:9;
then m + 1 - 1 > 1 - 1;
then m + 1 > 1 by XREAL_1:9;
then
A4: m >= 1 by NAT_1:13;
1 |^ m = 1;
then
A5: x |^ m > 1 by A2,A4,PREPOWER:10;
A6: x |^ n >= 1 by A2,PREPOWER:11;
x |^ k = x |^ n * x |^ m by A3,NEWTON:8;
hence thesis by A6,A5,XREAL_1:155;
end;
Lm10: 2 |^ m divides 2 |^ n implies m <= n
proof
not m <= n implies not 2 |^ m divides 2 |^ n
proof
assume
A1: not m <= n;
not 2 |^ m divides 2 |^ n
proof
(2 |^ n) div (2 |^ m) = 0 by A1,Lm9,NAT_D:27;
then
A2: 2 |^ n > 2 |^ m * ((2 |^ n) div (2 |^ m)) by PREPOWER:6;
assume 2 |^ m divides 2 |^ n;
hence contradiction by A2,NAT_D:3;
end;
hence thesis;
end;
hence thesis;
end;
theorem
m <= n iff 2 |^ m divides 2 |^ n by Lm6,Lm10;
theorem Th32:
p is prime & i divides p |^ n implies
i = 1 or ex k being Element of NAT st i = p*k
proof
defpred P[Nat] means i divides p |^ $1 implies i = 1 or (ex k being Element
of NAT st i = p*k);
assume
A1: p is prime;
then
A2: p <> 0 by INT_2:def 4;
A3: for n holds P[n] implies P[n+1]
proof
let n;
assume
A4: P[n];
now
assume i divides p |^ (n+1);
then consider u1 being Nat such that
A5: p |^ (n+1) = i*u1 by NAT_D:def 3;
p*(p |^ n) = i*u1 by A5,NEWTON:6;
then
A6: p divides i*u1;
now
per cases by A1,A6,NEWTON:80;
suppose
p divides i;
then consider w1 being Nat such that
A7: i = p*w1 by NAT_D:def 3;
w1 in NAT by ORDINAL1:def 12;
hence thesis by A7;
end;
suppose
p divides u1;
then consider w2 being Nat such that
A8: u1 = p*w2 by NAT_D:def 3;
p*(p |^ n) = p*(i*w2) by A5,A8,NEWTON:6;
then p |^ n = p*(i*w2) div p by A2,NAT_D:18;
then p |^ n = i*w2 by A2,NAT_D:18;
hence thesis by A4,NAT_D:def 3;
end;
end;
hence thesis;
end;
hence thesis;
end;
A9: P[0]
proof
now
assume i divides p |^ 0;
then i divides 1 by NEWTON:4;
then ex t being Nat st 1 = i*t by NAT_D:def 3;
hence thesis by NAT_1:15;
end;
hence thesis;
end;
for n holds P[n] from NAT_1:sch 2(A9,A3);
hence thesis;
end;
theorem Th33:
for n st
p is prime & n < p |^ (k+1) holds n divides p |^ (k+1) iff n divides p |^ k
proof
let n;
assume that
A1: p is prime and
A2: n < p |^ (k+1);
A3: p <> 0 by A1,INT_2:def 4;
A4: n divides p |^ (k+1) implies n divides p |^ k
proof
assume
A5: n divides p |^ (k+1);
now
per cases by A1,A5,Th32;
suppose
n = 1;
hence thesis by NAT_D:6;
end;
suppose
ex i being Element of NAT st n = p*i;
then consider i being Element of NAT such that
A6: n = p*i;
consider u being Nat such that
A7: p |^ (k+1) = (p*i)*u by A5,A6,NAT_D:def 3;
p*(p |^ k) = p*(i*u) by A7,NEWTON:6;
then
A8: p |^ k = p*(i*u) div p by A3,NAT_D:18;
then
A9: p |^ k = i*u by A3,NAT_D:18;
then
A10: u divides p |^ k;
u <> 1 by A2,A6,A9,NEWTON:6;
then consider j being Element of NAT such that
A11: u = p*j by A1,A10,Th32;
p |^ k = n*j by A3,A6,A8,A11,NAT_D:18;
hence thesis;
end;
end;
hence thesis;
end;
n divides p |^ k implies n divides p |^ (k+1)
proof
assume n divides p |^ k;
then n divides (p |^ k)*p by NAT_D:9;
hence thesis by NEWTON:6;
end;
hence thesis by A4;
end;
theorem Th34:
for k holds p is prime & d divides (p |^ k) implies
ex t being Element of NAT st d = p |^ t & t <= k
proof
let n;
assume that
A1: p is prime and
A2: d divides (p |^ n);
defpred P[Nat] means d divides (p |^ $1) implies ex t being Element of NAT
st d = p |^ t & t <= $1;
A3: p > 0 by A1,INT_2:def 4;
A4: for n st P[n] holds P[n+1]
proof
let n;
assume
A5: P[n];
now
assume
A6: d divides (p |^ (n+1));
(p |^ (n+1)) > 0 by A3,PREPOWER:6;
then
A7: d <= p |^ (n+1) by A6,NAT_D:7;
now
per cases by A7,XXREAL_0:1;
suppose
d < p |^ (n+1);
then ex t being Element of NAT st d = p |^ t & t <= n by A1,A5,A6
,Th33;
hence thesis by NAT_1:12;
end;
suppose
d = p |^ (n+1);
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
A8: P[0]
proof
assume
A9: d divides (p |^ 0);
d = p |^ 0
proof
ex t being Nat st p |^ 0 = d*t by A9,NAT_D:def 3;
then d = 1 by NAT_1:15,NEWTON:4;
hence thesis by NEWTON:4;
end;
hence thesis;
end;
for n holds P[n] from NAT_1:sch 2(A8,A4);
hence thesis by A2;
end;
theorem Th35:
p > 1 & i mod p = 1 implies (i |^ n) mod p = 1
proof
assume that
A1: p > 1 and
A2: i mod p = 1;
defpred P[Nat] means (i |^ $1) mod p = 1;
A3: for k holds P[k] implies P[k+1]
proof
let k;
assume
A4: (i |^ k) mod p = 1;
(i |^ (k + 1)) mod p = ((i |^ k)*i) mod p by NEWTON:6
.= (((i |^ k) mod p)*i) mod p by EULER_2:8
.= 1 by A2,A4;
hence thesis;
end;
1 mod p = 1 by A1,NAT_D:24;
then
A5: P[0] by NEWTON:4;
for n holds P[n] from NAT_1:sch 2(A5,A3);
hence thesis;
end;
theorem Th36:
for m,n being Nat holds m > 0 implies (n |^ m) mod n = 0
proof
let m,n be Nat;
assume
A1: m > 0;
defpred P[Nat] means $1 > 0 implies (n |^ $1) mod n = 0;
A2: for m being Nat holds P[m] implies P[m+1]
proof
let m be Nat;
assume P[m];
P[m+1]
proof
reconsider m,n as Element of NAT by ORDINAL1:def 12;
n*(n |^ m) mod n = ((n mod n)*(n |^ m)) mod n by EULER_2:8
.= (0*(n |^ m)) mod n by NAT_D:25
.= 0 by NAT_D:26;
hence thesis by NEWTON:6;
end;
hence thesis;
end;
A3: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A3,A2);
hence thesis by A1;
end;
theorem Th37:
for p being Nat holds p is prime & n,p are_coprime
implies (n |^ (p -'1)) mod p = 1
proof
let p be Nat;
assume that
A1: p is prime and
A2: n,p are_coprime;
A3: p <> 0 by A1,INT_2:def 4;
A4: n <> 0
proof
assume n = 0;
then n gcd p = p by NEWTON:52;
then n gcd p > 1 by A1,INT_2:def 4;
hence contradiction by A2,INT_2:def 3;
end;
then
A5: (n |^ (p -'1)) <> 0 by PREPOWER:5;
(n |^ p) mod p = n mod p by A1,EULER_2:19;
then
A6: (n |^ (p -' 1))*n mod p = n mod p by A3,A4,Th26;
p > 1 by A1,INT_2:def 4;
hence thesis by A2,A6,A5,EULER_2:12;
end;
theorem Th38:
p is prime & d > 1 & d divides (p |^ k) & not d divides ((p |^ k) div p)
implies d = p |^ k
proof
assume that
A1: p is prime and
A2: d > 1 and
A3: d divides (p |^ k) and
A4: not d divides ((p |^ k) div p);
A5: k <> 0
proof
assume k = 0;
then p |^ k = 1 by NEWTON:4;
hence contradiction by A2,A3,NAT_D:7;
end;
then k >= 1 by NAT_1:14;
then
A6: k - 1 >= 1 - 1 by XREAL_1:9;
consider t being Element of NAT such that
A7: d = p |^ t and
A8: t <= k by A1,A3,Th34;
A9: p <> 0 by A1,INT_2:def 4;
not t < k
proof
assume t < k;
then t < k + -1 + 1;
then t < k -'1 + 1 by A6,XREAL_0:def 2;
then t <= k -'1 by NAT_1:13;
then d divides p |^ (k -'1) by A7,Lm6;
hence contradiction by A4,A9,A5,Th28,NAT_1:14;
end;
hence thesis by A7,A8,XXREAL_0:1;
end;
definition
let i be Integer;
redefine func i^2 -> Element of NAT; :: redefines ^2 (SQUARE_1, definition)
coherence by ORDINAL1:def 12;
end;
theorem Th39:
for n st n > 1 holds m mod n = 1 iff m,1 are_congruent_mod n
proof
let n;
assume
A1: n > 1;
A2: m,1 are_congruent_mod n implies m mod n = 1
proof
assume m,1 are_congruent_mod n;
then consider t being Integer such that
A3: n*t = m - 1;
reconsider m,n as Integer;
m mod n = (n*t + 1) mod n by A3
.= 1 mod n by NAT_D:61;
hence thesis by A1,NAT_D:14;
end;
m mod n = 1 implies m,1 are_congruent_mod n
proof
assume m mod n = 1;
then consider k being Nat such that
A4: m = n*k + 1 and
1 < n by NAT_D:def 2;
n*k = m - 1 by A4;
hence thesis;
end;
hence thesis by A2;
end;
Lm11: n > 1 & m > 1 & m,1 are_congruent_mod n implies m mod n = 1
proof
assume that
A1: n > 1 and
A2: m > 1 and
A3: m,1 are_congruent_mod n;
consider d being Integer such that
A4: n*d = m - 1 by A3;
m - 1 > 1 - 1 by A2,XREAL_1:9;
then d > 0 by A4;
then reconsider d as Element of NAT by INT_1:3;
m = n*d + 1 by A4;
then m mod n = 1 mod n by NAT_D:21
.= 1 by A1,NAT_D:14;
hence thesis;
end;
theorem Th40:
i1,i2 are_congruent_mod i5 & i1,i3 are_congruent_mod i5 implies
i2,i3 are_congruent_mod i5
proof
assume that
A1: i1,i2 are_congruent_mod i5 and
A2: i1,i3 are_congruent_mod i5;
i2,i1 are_congruent_mod i5 by A1,INT_1:14;
then consider t1 being Integer such that
A3: i5*t1 = i2 - i1;
i3,i1 are_congruent_mod i5 by A2,INT_1:14;
then consider t2 being Integer such that
A4: i5*t2 = i3 - i1;
i2 - i3 = i5*(t1 - t2) by A3,A4;
hence thesis;
end;
theorem Th41:
3 is prime
proof
for n being Nat holds n divides 3 implies n = 1 or n = 3
proof
let n be Nat;
assume
A1: n divides 3;
A2: n <> 2
proof
A3: 3 mod 2 = (2*1 + 1) mod 2 .= 1 mod 2 by NAT_D:21
.= 1 by NAT_D:24;
assume n = 2;
hence contradiction by A1,A3;
end;
n <= 3 by A1,NAT_D:7;
then n < 2 + 1 or n = 3 by XXREAL_0:1;
then n <= 2 or n = 3 by NAT_1:13;
then n < 1 + 1 or n = 2 or n = 3 by XXREAL_0:1;
then n <= 1 or n = 2 or n = 3 by NAT_1:13;
then
A4: n < 1 or n = 1 or n = 2 or n = 3 by XXREAL_0:1;
n <> 0 by A1;
hence thesis by A4,A2,NAT_1:14;
end;
hence thesis by INT_2:def 4;
end;
theorem Th42:
n <> 0 implies Euler n <> 0
proof
assume
A1: n <> 0;
set X = {k where k is Element of NAT : n,k are_coprime & k >= 1 & k
<= n};
A2: X c= finSeg n
proof
let x be object;
assume x in X;
then
ex xx being Element of NAT st x = xx & n,xx are_coprime & xx >=
1 & xx <= n;
hence thesis by FINSEQ_1:1;
end;
assume Euler n = 0;
then
A3: card X = 0 by EULER_1:def 1;
reconsider X as finite set by A2;
ex k st k in X
proof
take 1;
n gcd 1 = 1 by NEWTON:51;
then
A4: n,1 are_coprime by INT_2:def 3;
1 <= n by A1,NAT_1:14;
hence thesis by A4;
end;
hence contradiction by A3;
end;
theorem
n <> 0 implies -n < n;
theorem Th44:
n <> 0 implies n div n = 1
proof
assume n <> 0;
then n*1 div n = 1 by NAT_D:18;
hence thesis;
end;
begin :: Public Key Cryptography
definition
let k,m,n;
func Crypto(m,n,k) -> Element of NAT equals
(m |^ k) mod n;
coherence;
end;
theorem
p is prime & q is prime & p <> q & n = p*q & k1,Euler(n)
are_coprime & (k1*k2) mod Euler(n) = 1 implies for m be Element of NAT
st m < n holds Crypto(Crypto(m,n,k1),n,k2) = m
proof
assume that
A1: p is prime and
A2: q is prime and
A3: p <> q and
A4: n = p*q and
A5: k1,Euler(n) are_coprime and
A6: (k1*k2) mod Euler(n) = 1;
A7: q > 1 by A2,INT_2:def 4;
A8: p > 1 by A1,INT_2:def 4;
A9: Euler(n)= Euler(p)*Euler(q) by A1,A2,A3,A4,EULER_1:21,INT_2:30
.= (p-1)*Euler(q) by A1,EULER_1:20
.= (p-1)*(q-1) by A2,EULER_1:20;
A10: n > 1 by A4,A8,A7,XREAL_1:161;
A11: p <> 0 & q <> 0 by A1,A2,INT_2:def 4;
then reconsider p1 = p-1,q1 = q-1 as Element of NAT by INT_1:3;
n <> 0 by A4,A11,XCMPLX_1:6;
then
A12: Euler n <> 0 by Th42;
not(p1=1 & q1=1) by A3;
then
A13: p1*q1 <> 1 by NAT_1:15;
A14: k1 <> 0
proof
assume k1 = 0;
then k1 gcd Euler n = Euler n by NEWTON:52;
hence contradiction by A5,A9,A13,INT_2:def 3;
end;
A15: k2 <> 0 by A6,NAT_D:26;
A16: q > 0 by A2,INT_2:def 4;
let m be Element of NAT;
assume
A17: m < n;
A18: p > 0 by A1,INT_2:def 4;
now
per cases;
suppose
A19: m = 0;
then m |^ k1 = 0 by A14,NAT_1:14,NEWTON:11;
then m |^ k1 mod n = 0 by NAT_D:26;
then Crypto(m,n,k1) |^ k2 = 0 by A15,NAT_1:14,NEWTON:11;
hence thesis by A19,NAT_D:26;
end;
suppose
A20: m = 1;
then m |^ k1 = 1;
then m |^ k1 mod n = 1 by A10,NAT_D:14;
then Crypto(m,n,k1) |^ k2 = 1;
hence thesis by A10,A20,NAT_D:14;
end;
suppose
A21: m <> 0 & m <> 1;
A22: for t being Element of NAT holds m |^ (t*p1*q1 + 1) mod n = m
proof
let t be Element of NAT;
now
m |^ (t*p1*q1) >= 1 by A21,NAT_1:14,PREPOWER:11;
then (m |^ (t*p1*q1)) - 1 >= 1 - 1 by XREAL_1:9;
then reconsider a = m |^ (t*p1*q1) -1 as Element of NAT by INT_1:3;
A23: p divides m*a
proof
now
per cases;
suppose
m gcd p = 1;
then
A24: m,p are_coprime by INT_2:def 3;
((m |^ (t*q1)) |^ (p1+1)) mod p = (m |^ (t*q1)) mod p
by A1,EULER_2:19;
then
(((m |^ (t*q1)) |^ p1)*(m |^ (t*q1))) mod p = (m |^ (t*q1
)) mod p by NEWTON:6;
then ((m |^ (t*q1)) |^ p1) mod p = 1 by A8,A21,A24,Th11,
EULER_2:17;
then (m |^ (t*q1*p1)) mod p = 1 by NEWTON:9;
then
(m |^ (t*p1*q1)) = p*((m |^ (t*p1*q1)) div p) + 1 by A18,
NAT_D:2;
then p divides a;
hence thesis by NAT_D:9;
end;
suppose
m gcd p <> 1;
then not m,p are_coprime by INT_2:def 3;
then m gcd p = p by A1,Th2;
then p divides m by NAT_D:def 5;
hence thesis by NAT_D:9;
end;
end;
hence thesis;
end;
q divides m*a
proof
now
per cases;
suppose
m gcd q = 1;
then
A25: m,q are_coprime by INT_2:def 3;
((m |^ (t*p1)) |^ (q1+1)) mod q = (m |^ (t*p1)) mod q
by A2,EULER_2:19;
then
(((m |^ (t*p1)) |^ q1)*(m |^ (t*p1))) mod q = (m |^ (t*p1
)) mod q by NEWTON:6;
then ((m |^ (t*p1)) |^ q1) mod q = 1 by A7,A21,A25,Th11,
EULER_2:17;
then (m |^ (t*p1*q1)) mod q = 1 by NEWTON:9;
then
(m |^ (t*p1*q1)) = q*((m |^ (t*p1*q1)) div q) + 1 by A16,
NAT_D:2;
then q divides a;
hence thesis by NAT_D:9;
end;
suppose
m gcd q <> 1;
then not m,q are_coprime by INT_2:def 3;
then m gcd q = q by A2,Th2;
then q divides m by NAT_D:def 5;
hence thesis by NAT_D:9;
end;
end;
hence thesis;
end;
then (p*q) divides (m*a) by A1,A2,A3,A23,Th4,INT_2:30;
then consider k be Nat such that
A26: (m*a) = (p*q)*k by NAT_D:def 3;
m*(m |^ (t*p1*q1) -1 ) = m*(m |^ (t*p1*q1)) - m*1
.= m |^ (t*p1*q1 + 1) - m by NEWTON:6;
then m |^ (t*p1*q1 + 1) - (m - m) = n*k + m by A4,A26,XCMPLX_1:37;
hence thesis by A17,NAT_D:def 2;
end;
hence thesis;
end;
reconsider t = (k1*k2) div Euler(n) as Element of NAT;
k1*k2 = p1*q1*t + 1 by A6,A12,A9,NAT_D:2
.= t*p1*q1 + 1;
then m |^ (k1*k2) mod n = m by A22;
then ((m |^ k1) |^ k2) mod n = m by NEWTON:9;
hence thesis by EULER_2:22;
end;
end;
hence thesis;
end;
begin :: Order
definition
let i,p;
assume that
A1: p > 1 and
A2: i,p are_coprime;
func order(i,p) -> Element of NAT means
:Def2:
it > 0 & (i |^ it) mod p = 1
& for k st k > 0 & (i |^ k) mod p = 1 holds it <= k;
existence
proof
set A = {k where k is Element of NAT:k > 0 & (i |^ k) mod p = 1};
A3: A c= NAT
proof
let a be object;
assume a in A;
then ex k being Element of NAT st k = a & k > 0 & (i |^ k) mod p = 1;
hence thesis;
end;
i <> 0
proof
assume i = 0;
then i gcd p = p by NEWTON:52;
hence contradiction by A1,A2,INT_2:def 3;
end;
then
A4: (i |^ Euler p) mod p = 1 by A1,A2,EULER_2:18;
Euler p <> 0 by A1,Th42;
then Euler p in A by A4;
then reconsider A as non empty Subset of NAT by A3;
set a = the Element of A;
defpred P[set] means $1 in A;
a is Element of NAT;
then
A5: ex kk being Nat st P[kk];
consider kk being Nat such that
A6: P[kk] and
A7: for n being Nat st P[n] holds kk <= n from NAT_1:sch 5(A5);
take kk;
A8: for k st k > 0 & (i |^ k) mod p = 1 holds kk <= k
proof
let k;
assume
A9: k > 0 & (i |^ k) mod p = 1;
k in NAT by ORDINAL1:def 12;
then k in A by A9;
hence thesis by A7;
end;
ex k being Element of NAT st k = kk & k > 0 & (i |^ k) mod p = 1 by A6;
hence thesis by A8;
end;
uniqueness
proof
let k1,k2 be Element of NAT;
assume
k1 > 0 & (i |^ k1) mod p = 1 &
(for k st k > 0 & (i |^ k) mod p = 1 holds k1 <= k) &
k2 > 0 & (i |^ k2) mod p = 1 &
(for k st k > 0 & (i |^ k) mod p = 1 holds k2 <= k);
then k1 <= k2 & k2 <= k1;
hence thesis by XXREAL_0:1;
end;
end;
theorem
p > 1 implies order(1,p) = 1
proof
assume
A1: p > 1;
p gcd 1 = 1 by NEWTON:51;
then
A2: 1,p are_coprime by INT_2:def 3;
(1 |^ 1) mod p = 1 by A1,NAT_D:24;
then order(1,p) <= 1 by A1,A2,Def2;
then order(1,p) < 1 or order(1,p) = 1 by XXREAL_0:1;
then order(1,p) = 0 or order(1,p) = 1 by NAT_1:14;
hence thesis by A1,A2,Def2;
end;
theorem Th47:
p > 1 & (i |^ n) mod p = 1 & i,p are_coprime implies order(i,p) divides n
proof
assume that
A1: p > 1 and
A2: (i |^ n) mod p = 1 and
A3: i,p are_coprime;
A4: order(i,p) <> 0 by A1,A3,Def2;
A5: (i |^ order(i,p)) mod p = 1 by A1,A3,Def2;
n mod order(i,p) = 0
proof
set I = n mod order(i,p);
consider t being Nat such that
A6: n = order(i,p)*t + I and
A7: I < order(i,p) by A4,NAT_D:def 2;
reconsider t as Element of NAT by ORDINAL1:def 12;
(i |^ (order(i,p)*t))*(i |^ I) mod p = 1 by A2,A6,NEWTON:8;
then ((i |^ order(i,p)) |^ t)*(i |^ I) mod p = 1 by NEWTON:9;
then ((((i |^ order(i,p)) |^ t) mod p)*(i |^ I)) mod p = 1 by EULER_2:8;
then (1*(i |^ I)) mod p = 1 by A1,A5,Th35;
hence thesis by A1,A3,A7,Def2;
end;
hence thesis by A4,Th6;
end;
theorem Th48:
p > 1 & i,p are_coprime & order(i,p) divides n implies (i |^ n) mod p = 1
proof
assume that
A1: p > 1 and
A2: i,p are_coprime and
A3: order(i,p) divides n;
consider t being Nat such that
A4: n = order(i,p)*t by A3,NAT_D:def 3;
reconsider t as Element of NAT by ORDINAL1:def 12;
(i |^ n) mod p = ((i |^ order(i,p)) |^ t) mod p by A4,NEWTON:9
.= (((i |^ order(i,p)) mod p) |^ t ) mod p by EULER_2:22
.= ((1) |^ t) mod p by A1,A2,Def2
.= 1 by A1,NAT_D:24;
hence thesis;
end;
theorem Th49:
p is prime & i,p are_coprime implies order(i,p) divides p-'1
proof
assume that
A1: p is prime and
A2: i,p are_coprime;
(i |^ (p -'1)) mod p = 1 & p > 1 by A1,A2,Th37,INT_2:def 4;
hence thesis by A2,Th47;
end;
begin :: Fermat Number
definition
let n be Nat;
func Fermat(n) -> Element of NAT equals
2 |^ (2 |^ n) + 1;
correctness;
end;
theorem Th50:
Fermat(0) = 3
proof
Fermat(0) = 2 |^ 1 + 1 by NEWTON:4
.= 2 + 1;
hence thesis;
end;
theorem Th51:
Fermat(1) = 5
proof
Fermat(1) = 2 |^ (1 + 1) + 1
.= 2 |^ 1 * 2 + 1 by NEWTON:6
.= 2 * 2 + 1;
hence thesis;
end;
theorem Th52:
Fermat(2) = 17
proof
thus Fermat(2) = 2 |^ (2 |^ (1 + 1)) + 1
.= 2 |^ (2 |^ 1 * 2) + 1 by NEWTON:6
.= 2 |^ (3 + 1) + 1
.= 2 |^ (2 + 1) * 2 + 1 by NEWTON:6
.= 2 |^ (1 + 1) * 2 * 2 + 1 by NEWTON:6
.= 2 |^ 1 * 2 * 2 * 2 + 1 by NEWTON:6
.= 17;
end;
theorem Th53:
Fermat(3) = 257
proof
thus Fermat(3) = 2 |^ (4 + 4) + 1 by POWER:61
.= 2 |^ 4 * 2 |^ 4 + 1 by NEWTON:8
.= 257 by POWER:62;
end;
theorem Th54:
Fermat(4) = 256*256+1
proof
thus Fermat(4) = 2 |^ (8 + 8) + 1 by POWER:62
.= 2 |^ 8 * 2 |^ 8 + 1 by NEWTON:8
.= (2 |^ 4 * 2 |^ 4)*2 |^ (4 + 4) + 1 by NEWTON:8
.= 256*256+1 by NEWTON:8,POWER:62;
end;
theorem Th55:
Fermat(n) > 2
proof
set 2N = 2 |^ (2 |^ n);
2N > 1 by Lm2;
then 2N + 1 > 1 + 1 by XREAL_1:6;
hence thesis;
end;
Lm12: Fermat(n) > 1
proof
Fermat(n) <> 1 by Th55;
then Fermat(n) > 1 or Fermat(n) < 1 by XXREAL_0:1;
hence thesis by NAT_1:14;
end;
Lm13: (Fermat(n) -'1) mod 2 = 0
proof
2 mod 2 = 0 by NAT_D:25;
then Fermat(n) -'1 = 2 |^ (2 |^ n) & 2 is even by NAT_2:21,NAT_D:34;
then (Fermat(n) -'1) is even by Th21,PREPOWER:6;
hence thesis by NAT_2:21;
end;
Lm14: Fermat(n)-'1 > 0
proof
Fermat(n) > 1 by Lm12;
then Fermat(n) - 1 > 1 - 1 by XREAL_1:9;
hence thesis by XREAL_0:def 2;
end;
Lm15: Fermat(n) mod (2 |^ (2 |^ n)) = 1
proof
set 2N = 2 |^ (2 |^ n);
Fermat(n) mod 2N = (2N*1 + 1) mod 2N .= 1 mod 2N by NAT_D:21
.= 1 by Lm2,NAT_D:14;
hence thesis;
end;
Lm16: Fermat(n) is odd
proof
Fermat(n) - 1 = Fermat(n) -'1 & (Fermat(n) -'1) mod 2 = 0 by Lm13,
XREAL_0:def 2;
hence thesis by NAT_2:21;
end;
theorem Th56:
p is prime & p > 2 & p divides Fermat(n) implies
ex k being Element of NAT st p = k*(2 |^ (n + 1)) + 1
proof
assume that
A1: p is prime and
A2: p > 2 and
A3: p divides Fermat(n);
A4: p > 1 by A1,INT_2:def 4;
set t = Fermat(n) div p;
set 2N = 2 |^ (2 |^ n);
A5: (p*t + (-1)),(0 + (-1)) are_congruent_mod p;
A6: p*t = 2N + 1 by A3,NAT_D:3;
A7: 2N mod p <> 1
proof
assume 2N mod p = 1;
then 2N,1 are_congruent_mod p by A4,Th39;
then 1,2N are_congruent_mod p by INT_1:14;
then 1,(-1) are_congruent_mod p by A6,A5,INT_1:15;
then p divides (1 - -1);
hence contradiction by A2,NAT_D:7;
end;
A8: 2,p are_coprime by A1,A2,INT_2:28,30;
then order(2,p) <> 0 by A4,Def2;
then order(2,p) >= 1 by NAT_1:14;
then
A9: order(2,p) = 1 or order(2,p) > 1 by XXREAL_0:1;
A10: 2N > 1 by Th25,PREPOWER:6;
then (2N)*(2N) > 1*(2N) by XREAL_1:68;
then
A11: (2N)^2 > 1 by A10,XXREAL_0:2;
(2N)^2,(-1)^2 are_congruent_mod p by A6,A5,INT_1:18;
then (2N)^2 mod p = 1 by A4,A11,Lm11;
then (2 |^ (2 |^ (n + 1))) mod p = 1 by Lm8;
then
A12: order(2,p) divides (2 |^ (n + 1)) by A4,A8,Th47;
2 |^ (n + 1) div 2 = 2*(2 |^ n) div 2 by NEWTON:6
.= 2 |^ n;
then not order(2,p) divides (2 |^ (n + 1)) div 2 by A1,A2,A4,A7,Th48,INT_2:28
,30;
then order(2,p) = 2 |^ (n + 1) by A12,A9,Th38,INT_2:28,NAT_D:6;
then (2 |^ (n + 1)) divides (p -'1) by A1,A2,Th49,INT_2:28,30;
then consider t2 being Nat such that
A13: (p -'1) = (2 |^ (n + 1))*t2 by NAT_D:def 3;
reconsider t2 as Element of NAT by ORDINAL1:def 12;
p - 1 > 1 - 1 by A4,XREAL_1:9;
then p - 1 = (2 |^ (n + 1))*t2 by A13,XREAL_0:def 2;
then p = t2*(2 |^ (n + 1)) + 1;
hence thesis;
end;
theorem Th57:
n <> 0 implies 3,Fermat(n) are_coprime
proof
assume
A1: n <> 0;
Fermat(n) gcd 3 <> 3
proof
assume Fermat(n) gcd 3 = 3;
then 3 divides Fermat(n) by NAT_D:def 5;
then consider k being Element of NAT such that
A2: 3 = k*(2 |^ (n+1)) + 1 by Th41,Th56;
1 = k*(2 |^ (n+1)) div 2 by A2;
then 1 = k*(2 |^ n) by Lm5;
then 2 |^ n = 1 by NAT_1:15;
then 2 |^ n = 2 |^ 0 by NEWTON:4;
hence contradiction by A1,Th30;
end;
hence thesis by Th2,Th41;
end;
begin :: Pepin's Test
::$N Pepin's test
theorem Th58:
(3 |^ ((Fermat(n)-'1) div 2)),(-1) are_congruent_mod Fermat(n)
implies Fermat(n) is prime
proof
per cases;
suppose
n = 0;
hence thesis by Th41,Th50;
end;
suppose
A1: n > 0;
Fermat(n) > 2 by Th55;
then consider p being Element of NAT such that
A2: p is prime and
A3: p divides Fermat(n) by INT_2:31;
set d = order(3,p);
consider i being Nat such that
A4: Fermat(n) = p*i by A3,NAT_D:def 3;
A5: p > 2
proof
assume p <= 2;
then p = 2 or p < 1 + 1 by XXREAL_0:1;
then
A6: p = 2 or p <= 1 by NAT_1:13;
A7: p <> 0 by A2,INT_2:def 4;
Fermat(n) is odd by Lm16;
then Fermat(n) mod p = 1 by A2,A6,INT_2:def 4,NAT_2:22;
hence contradiction by A3;
end;
A8: Fermat(n) - 1 >= 0;
assume
A9: (3 |^ ((Fermat(n)-'1) div 2)),(-1) are_congruent_mod Fermat(n);
then
A10: (3 |^ ((Fermat(n)-'1) div 2))^2,(-1)^2 are_congruent_mod Fermat(n) by
INT_1:18;
(Fermat(n) -'1) mod 2 = 0 by Lm13;
then
A11: (3 |^ (Fermat(n)-'1)),(-1)^2 are_congruent_mod Fermat(n) by A10,Th27;
set 2N = 2 |^ (2 |^ n);
assume
A12: not Fermat(n) is prime;
reconsider i as Element of NAT by ORDINAL1:def 12;
A13: 1 < p by A2,INT_2:def 4;
A14: p <> 3
proof
1 gcd i = 1 by NEWTON:51;
then
A15: 3*1 gcd 3*i = 3 by EULER_1:5;
assume p = 3;
then not 3,Fermat(n) are_coprime by A4,A15,INT_2:def 3;
hence contradiction by A1,Th57;
end;
then d divides (p-'1) by A2,Th41,Th49,INT_2:30;
then consider x being Nat such that
A16: p -'1 = d*x by NAT_D:def 3;
A17: (3 |^ ((Fermat(n)-'1) div 2)),(-1) are_congruent_mod p by A9,A4,INT_1:20;
A18: not d divides ((Fermat(n) -'1) div 2)
proof
assume d divides ((Fermat(n) -'1) div 2);
then (3 |^ ((Fermat(n) -'1) div 2)) mod p = 1 by A2,A14,A13,Th41,Th48,
INT_2:30;
then (3 |^ ((Fermat(n) -'1) div 2)),1 are_congruent_mod p by A13,Th39;
then 1,-1 are_congruent_mod p by A17,Th40;
then p divides (1 - -1);
hence contradiction by A5,NAT_D:7;
end;
then
A19: not d divides (2N div 2) by A8,XREAL_0:def 2;
A20: 3,p are_coprime by A2,A14,Th41,INT_2:30;
then
A21: d <> 0 by A13,Def2;
A22: d > 1
proof
assume
A23: d <= 1;
now
per cases by A23,XXREAL_0:1;
suppose
d < 1;
hence thesis by A21,NAT_1:14;
end;
suppose
d = 1;
hence thesis by A18,NAT_D:6;
end;
end;
hence thesis;
end;
3 |^ (Fermat(n)-'1) > 1 by Lm14,Th25;
then (3 |^ (Fermat(n)-'1)) mod p = 1 by A4,A13,A11,Lm11,INT_1:20;
then d divides (Fermat(n)-'1) by A20,A13,Th47;
then d divides 2N by A8,XREAL_0:def 2;
then d = 2N by A19,A22,Th38,INT_2:28
.= Fermat(n) -'1 by A8,XREAL_0:def 2;
then
A24: d = 2N by A8,XREAL_0:def 2;
A25: p*i mod 2N = 1 by A4,Lm15;
p - 1 > 1 - 1 by A13,XREAL_1:9;
then
A26: p - 1 = x*d by A16,XREAL_0:def 2;
then
A27: p = x*2N + 1 by A24;
then p mod 2N = 1 mod 2N by NAT_D:21
.= 1 by Lm2,NAT_D:24;
then (1*i) mod 2N = 1 by A25,EULER_2:8;
then consider y being Nat such that
A28: i = 2N*y + 1 and
1 < 2N by NAT_D:def 2;
A29: 2N <> 0 by Lm2;
A30: x >= 1
proof
assume x < 1;
then p = 0*2N + 1 by A27,NAT_1:14;
hence contradiction by A2,INT_2:def 4;
end;
reconsider y as Element of NAT by ORDINAL1:def 12;
Fermat(n) = (x*2N + 1)*(y*2N + 1) by A4,A24,A26,A28
.= 2N*(x*y*2N + x + y) + 1;
then
A31: 1 = 2N*(x*y*2N + x + y) div 2N by A29,Th44
.= (x*y*2N + x + y) by A29,NAT_D:18;
2N > 1 by Lm2;
then p = 1*2N + 1 by A27,A30,A31,Lm1
.= Fermat(n);
hence contradiction by A12,A2;
end;
end;
:: LEMMA ::
Lm17: 3 |^ 2 = 9
proof
3 |^ 2 = 3 |^ (1+1) .= (3 |^ 1)*(3 |^ 1) by NEWTON:8
.= 3*3;
hence thesis;
end;
Lm18: 3 |^ 4 = 81
proof
3 |^ 4 = 3 |^ (2+2) .= (3 |^ 2)* (3 |^ 2) by NEWTON:8;
hence thesis by Lm17;
end;
Lm19: 3 |^ 8 = 6561
proof
3 |^ 8 = 3 |^ (4+4) .= (3 |^ 4)* (3 |^ 4) by NEWTON:8;
hence thesis by Lm18;
end;
Lm20: 3 |^ 16 = 6561*6561
proof
3 |^ 16 = 3 |^ (8+8) .= (3 |^ 8)* (3 |^ 8) by NEWTON:8;
hence thesis by Lm19;
end;
Lm21: Fermat(1) divides (3 |^ (4*i + 2)) + 1
proof
defpred P[Nat] means Fermat(1) divides (3 |^ (4*$1 + 2)) + 1;
A1: for n holds P[n] implies P[n+1]
proof
let n;
assume Fermat(1) divides (3 |^ (4*n + 2)) + 1;
then consider m being Nat such that
A2: (3 |^ (4*n + 2)) + 1 = Fermat(1)*m by NAT_D:def 3;
3 |^ (4*n) >= 3 |^ 0 by PREPOWER:93;
then 3 |^ (4*n) >= 1 by NEWTON:4;
then (3 |^ (4*n)) * 3 |^ 2 > 0 * 3 |^ 2 by Lm17,XREAL_1:68;
then (3 |^ (4*n + 2)) > 0 by NEWTON:8;
then (3 |^ (4*n + 2)) + 1 > 0 + 1 by XREAL_1:6;
then Fermat(1)*m*81 > 1*81 by A2,XREAL_1:68;
then Fermat(1)*m*81/Fermat(1) > 1*81/Fermat(1) by XREAL_1:74;
then m*Fermat(1)*81*Fermat(1)" > 1*81/Fermat(1);
then m*81*Fermat(1)"*Fermat(1) > 1*81/Fermat(1);
then m*81/Fermat(1)*Fermat(1) > 1*81/Fermat(1);
then m*81 > 81/5 by Th51;
then m*81 > 16 by XXREAL_0:2;
then
A3: m*81 + (- 16) > 16 + (- 16) by XREAL_1:6;
(3 |^ (4*(n+1) + 2)) + 1 = (3 |^ (4*n + 2 + 4)) + 1
.= ((Fermat(1)*m -1)*(3 |^ 4)) + 1 by A2,NEWTON:8
.= Fermat(1)*((m*81)-16) by Lm18,Th51
.= Fermat(1)*((m*81)-'16) by A3,XREAL_0:def 2;
hence thesis by NAT_D:def 3;
end;
3 |^ (4*0+2) + 1 = 5 * 2 by Lm17;
then
A4: P[0] by Th51,NAT_D:def 3;
for n holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
Lm23: n = 1 implies (3 |^ ((Fermat(n)-'1) div 2)),(-1) are_congruent_mod
Fermat(n)
proof
A2: 5 -'1 = 5 - 1 by XREAL_0:def 2
.= 4 + 0;
assume
A4: n = 1;
(Fermat(1) -'1) div 2 = 4*0 + 2 by A2,Th51;
then Fermat(1) divides (3 |^ ((Fermat(n)-'1) div 2)) + 1 by A4,Lm21;
then Fermat(1) divides ((3 |^ ((Fermat(n)-'1) div 2 )) - (-1));
hence thesis by A4;
end;
Lm24: Fermat(2) divides (3 |^ (16*n + 8)) + 1
proof
defpred P[Nat] means Fermat(2) divides (3 |^ (16*$1 + 8)) + 1;
A1: for n holds P[n] implies P[n+1]
proof
let n;
assume Fermat(2) divides (3 |^ (16*n + 8)) + 1;
then consider m being Nat such that
A2: (3 |^ (16*n + 8)) + 1 = Fermat(2)*m by NAT_D:def 3;
3 |^ (16*n) >= 3 |^ 0 by PREPOWER:93;
then 3 |^ (16*n) >= 1 by NEWTON:4;
then (3 |^ (16*n)) * 3 |^ 8 > 0 * 3 |^ 8 by Lm19,XREAL_1:68;
then (3 |^ (16*n + 8)) > 0 by NEWTON:8;
then (3 |^ (16*n + 8)) + 1 > 0 + 1 by XREAL_1:6;
then Fermat(2)*m*6561 > 1*6561 by A2,XREAL_1:68;
then Fermat(2)*m*6561*6561 > 6561*6561 by XREAL_1:68;
then Fermat(2)*m*6561*6561 > 6562*6560 by XXREAL_0:2;
then Fermat(2)*m*6561*6561/Fermat(2) > 6560*6562/Fermat(2) by XREAL_1:74;
then m*6561*Fermat(2)*6561*Fermat(2)" > 6560*6562/Fermat(2);
then m*6561*6561*Fermat(2)"*Fermat(2) > 6560*6562/Fermat(2);
then m*6561*6561/Fermat(2)*Fermat(2) > 6560*6562/Fermat(2);
then m*6561*6561 > 6560*6562/17 by Th52;
then
A3: m*6561*6561-386*6560 > 386*6560-386*6560 by XREAL_1:9;
(3 |^ (16*(n+1) + 8)) + 1 = (3 |^ (16*n + 8 + 16)) + 1
.= ((Fermat(2)*m -1)*(3 |^ 16)) + 1 by A2,NEWTON:8
.= Fermat(2)*((m*6561*6561)-386*6560) by Lm20,Th52
.= Fermat(2)*((m*6561*6561)-'386*6560) by A3,XREAL_0:def 2;
hence thesis by NAT_D:def 3;
end;
3 |^ (16*0 + 8) + 1 = 17 * 386 by Lm19;
then
A4: P[0] by Th52,NAT_D:def 3;
for n holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
Lm25: 3 |^ 2 mod Fermat(3) = 9
proof
A1: 9 = 0*257 + 9;
thus 3 |^ 2 mod Fermat(3) = (3 |^ (1+1)) mod Fermat(3)
.= (3 |^ 1*3 |^ 1) mod Fermat(3) by NEWTON:8
.= 9 by A1,Th53,NAT_D:def 2;
end;
Lm26: 3 |^ 4 mod Fermat(3) = 81
proof
A1: 81 = 0*257 + 81;
thus 3 |^ 4 mod Fermat(3) = (3 |^ (2+2)) mod Fermat(3)
.= (3 |^ 2*3 |^ 2) mod Fermat(3) by NEWTON:8
.= (((3 |^ 2) mod Fermat(3))*((3 |^ 2) mod Fermat(3))) mod Fermat(3) by
NAT_D:67
.= 81 by A1,Lm25,Th53,NAT_D:def 2;
end;
Lm27: 3 |^ 8 mod Fermat(3) = 136
proof
A1: 6561 = 25*257 + 136;
thus 3 |^ 8 mod Fermat(3) = (3 |^ (4+4)) mod Fermat(3)
.= (3 |^ 4*3 |^ 4) mod Fermat(3) by NEWTON:8
.= (((3 |^ 4) mod Fermat(3))*((3 |^ 4) mod Fermat(3))) mod Fermat(3) by
NAT_D:67
.= 136 by A1,Lm26,Th53,NAT_D:def 2;
end;
Lm28: 3 |^ 16 mod Fermat(3) = 83*3
proof
A1: 18496 = 71*257 + 249;
thus 3 |^ 16 mod Fermat(3) = (3 |^ (8+8)) mod Fermat(3)
.= (3 |^ 8*3 |^ 8) mod Fermat(3) by NEWTON:8
.= (136*136) mod Fermat(3) by Lm27,NAT_D:67
.= 83*3 by A1,Th53,NAT_D:def 2;
end;
Lm29: 3 |^ 32 mod Fermat(3) = 64
proof
A1: 83*3*83*3 = 241*257 + 64;
3 |^ 32 mod Fermat(3) = (3 |^ (16+16)) mod Fermat(3)
.= (3 |^ 16*3 |^ 16) mod Fermat(3) by NEWTON:8
.= (83*3*(83*3)) mod Fermat(3) by Lm28,NAT_D:67
.= 64 by A1,Th53,NAT_D:def 2;
hence thesis;
end;
Lm30: 3 |^ 64 mod Fermat(3) = 241
proof
A1: 4096 = 15*257 + 241;
thus 3 |^ 64 mod Fermat(3) = (3 |^ (32+32)) mod Fermat(3)
.= (3 |^ 32*3 |^ 32) mod Fermat(3) by NEWTON:8
.= (64*64) mod Fermat(3) by Lm29,NAT_D:67
.= 241 by A1,Th53,NAT_D:def 2;
end;
Lm31: 3 |^ 128 mod Fermat(3) = 256
proof
A1: 241*241 = 225*257 + 256;
thus 3 |^ 128 mod Fermat(3) = (3 |^ (64+64)) mod Fermat(3)
.= (3 |^ 64*3 |^ 64) mod Fermat(3) by NEWTON:8
.= (241*241) mod Fermat(3) by Lm30,NAT_D:67
.= 256 by A1,Th53,NAT_D:def 2;
end;
Lm32: 3 |^ 2 mod Fermat(4) = 9
proof
A1: 9 = 0*(256*256+1) + 9;
thus 3 |^ 2 mod Fermat(4) = (3 |^ (1+1)) mod Fermat(4)
.= (3 |^ 1*3 |^ 1) mod Fermat(4) by NEWTON:8
.= 9 by A1,Th54,NAT_D:def 2;
end;
Lm33: 3 |^ 4 mod Fermat(4) = 81
proof
A1: 81 = 0*(256*256+1) + 81;
thus 3 |^ 4 mod Fermat(4) = (3 |^ (2+2)) mod Fermat(4)
.= (3 |^ 2*3 |^ 2) mod Fermat(4) by NEWTON:8
.= (9*9) mod Fermat(4) by Lm32,NAT_D:67
.= 81 by A1,Th54,NAT_D:def 2;
end;
Lm34: 3 |^ 8 mod Fermat(4) = 6561
proof
A1: 6561 = 0*(256*256+1) + 6561;
thus 3 |^ 8 mod Fermat(4) = (3 |^ (4+4)) mod Fermat(4)
.= (3 |^ 4*3 |^ 4) mod Fermat(4) by NEWTON:8
.= (81*81) mod Fermat(4) by Lm33,NAT_D:67
.= 6561 by A1,Th54,NAT_D:def 2;
end;
Lm35: 3 |^ 16 mod Fermat(4) = 164*332+1
proof
A1: 6561*6561 = 656*(256*256+1) + (164*332+1);
3 |^ 16 mod Fermat(4) = (3 |^ (8+8)) mod Fermat(4)
.= (3 |^ 8*3 |^ 8) mod Fermat(4) by NEWTON:8
.= (6561*6561) mod Fermat(4) by Lm34,NAT_D:67
.= 164*332+1 by A1,Th54,NAT_D:def 2;
hence thesis;
end;
Lm36: 3 |^ 32 mod Fermat(4) = 123*503
proof
A1: (164*332+1)*(164*332+1) = 263*172*(256*256+1) + 123*503;
3 |^ 32 mod Fermat(4) = (3 |^ (16+16)) mod Fermat(4)
.= (3 |^ 16*3 |^ 16) mod Fermat(4) by NEWTON:8
.= ((164*332+1)*(164*332+1)) mod Fermat(4) by Lm35,NAT_D:67
.= 123*503 by A1,Th54,NAT_D:def 2;
hence thesis;
end;
Lm37: 3 |^ 64 mod Fermat(4) = 14*1367+1
proof
A1: (123*503)*(123*503) = (325+(241*241))*(256*256+1)+(14*1367+1);
3 |^ 64 mod Fermat(4) = (3 |^ (32+32)) mod Fermat(4)
.= (3 |^ 32*3 |^ 32) mod Fermat(4) by NEWTON:8
.= ((123*503)*(123*503)) mod Fermat(4) by Lm36,NAT_D:67
.= 14*1367+1 by A1,Th54,NAT_D:def 2;
hence thesis;
end;
Lm38: 3 |^ 128 mod Fermat(4) = 52*289
proof
A1: (14*1367+1)*(14*1367+1) = 5589*(256*256+1) + 52*289;
3 |^ 128 mod Fermat(4) = (3 |^ (64+64)) mod Fermat(4)
.= (3 |^ 64*3 |^ 64) mod Fermat(4) by NEWTON:8
.= ((14*1367+1)*(14*1367+1)) mod Fermat(4) by Lm37,NAT_D:67
.= 52*289 by A1,Th54,NAT_D:def 2;
hence thesis;
end;
Lm39: 3 |^ 256 mod Fermat(4) = 282
proof
A1: (52*289)*(52*289) = 3446*(256*256+1) + 282;
3 |^ 256 mod Fermat(4) = (3 |^ (128+128)) mod Fermat(4)
.= (3 |^ 128*3 |^ 128) mod Fermat(4) by NEWTON:8
.= ((52*289)*(52*289)) mod Fermat(4) by Lm38,NAT_D:67
.= 282 by A1,Th54,NAT_D:def 2;
hence thesis;
end;
Lm40: 3 |^ (256*2) mod Fermat(4) = 71*197
proof
A1: 282*282 = 1*(256*256+1) + 71*197;
(3 |^ 256)*(3 |^ 256) = 3 |^ (256+256) by NEWTON:8
.= 3 |^ 512;
then 3 |^ (256*2) mod Fermat(4) = (282*282) mod Fermat(4) by Lm39,NAT_D:67
.= 71*197 by A1,Th54,NAT_D:def 2;
hence thesis;
end;
Lm41: 3 |^ (256*4) mod Fermat(4) = 32*257
proof
A1: (71*197)*(71*197) = 2985*(256*256+1) + 32*257;
(3 |^ (256*2))*(3 |^ (256*2)) = 3 |^ ((256*2)+(256*2)) by NEWTON:8
.= 3 |^ (1024);
then 3 |^ (256*4) mod Fermat(4) = ((71*197)*(71*197)) mod Fermat(4) by Lm40,
NAT_D:67
.= 32*257 by A1,Th54,NAT_D:def 2;
hence thesis;
end;
Lm42: 3 |^ (256*8) mod Fermat(4) = 81*809
proof
A1: (32*257)*(32*257) = 1031*(256*256+1) + 81*809;
(3 |^ (256*4))*(3 |^ (256*4)) = 3 |^ ((256*4)+(256*4)) by NEWTON:8
.= 3 |^ (2048);
then 3 |^ (256*8) mod Fermat(4) = ((32*257)*(32*257)) mod (256*256+1) by Lm41
,Th54,NAT_D:67
.= 81*809 by A1,NAT_D:def 2;
hence thesis;
end;
Lm43: 3 |^ (256*16) mod Fermat(4) = 64
proof
A1: (81*809)*(81*809) = (256*255+241)*(256*256+1) + 64;
(3 |^ (256*8))*(3 |^ (256*8)) = 3 |^ ((256*8)+(256*8)) by NEWTON:8
.= 3 |^ (4096);
then 3 |^ (256*16) mod Fermat(4) = ((81*809)*(81*809)) mod Fermat(4) by Lm42,
NAT_D:67
.= 64 by A1,Th54,NAT_D:def 2;
hence thesis;
end;
Lm44: 3 |^ (256*32) mod Fermat(4) = 256*16
proof
A1: 64*64 = 0*(256*256+1) + 256*16;
(3 |^ (256*16))*(3 |^ (256*16)) = 3 |^ ((256*16)+(256*16)) by NEWTON:8
.= 3 |^ (8192);
then 3 |^ (256*32) mod Fermat(4) = (64*64) mod Fermat(4) by Lm43,NAT_D:67
.= 256*16 by A1,Th54,NAT_D:def 2;
hence thesis;
end;
Lm45: 3 |^ (256*64) mod Fermat(4) = 673*97
proof
A1: (256*16)*(256*16) = 255*(256*256+1) + 673*97;
(3 |^ (256*32))*(3 |^ (256*32)) = 3 |^ ((256*32)+(256*32)) by NEWTON:8
.= 3 |^ (256*(32+32));
then 3 |^ (256*64) mod Fermat(4) = ((256*16)*(256*16)) mod Fermat(4) by Lm44,
NAT_D:67
.= 673*97 by A1,Th54,NAT_D:def 2;
hence thesis;
end;
Lm46: 3 |^ (256*128) mod Fermat(4) = 256*256
proof
A1: (255*256+1)*(255*256+1) = 255*255*(256*256+1) + 256*256;
(3 |^ (256*64))*(3 |^ (256*64)) = 3 |^ ((256*64)+(256*64)) by NEWTON:8
.= 3 |^ (256*(64+64));
then 3 |^ (256*128) mod Fermat(4) = ((673*97)*(673*97)) mod Fermat(4) by Lm45
,NAT_D:67
.= 256*256 by A1,Th54,NAT_D:def 2;
hence thesis;
end;
Lm47: Fermat(3) divides (3 |^ (32*0 + 128)) + 1
proof
A1: 257 = 257*1 + 0;
1 = 257*0 + 1;
then 1 mod Fermat(3) = 1 by Th53,NAT_D:def 2;
then ((3 |^ (32*0 + 128)) + 1) mod Fermat(3) = (256 + 1) mod Fermat(3) by
Lm31,NAT_D:66
.= 0 by A1,Th53;
hence thesis by Th7,NAT_D:6;
end;
Lm48: Fermat(4) divides (3 |^ (64*0 + 256*128)) + 1
proof
(256*256+1) = (256*256+1)*1 + 0;
then
A1: (256*256+1) mod Fermat(4) = 0 by Th54;
1 = (256*256+1)*0 + 1;
then 1 mod Fermat(4) = 1 by Th54,NAT_D:def 2;
then (3 |^ (64*0 + 256*128) + 1) mod Fermat(4) = 0 by A1,Lm46,NAT_D:66;
hence thesis by Th7,NAT_D:6;
end;
theorem
5 is prime
proof
(3 |^ ((Fermat(1)-'1) div 2)),(-1) are_congruent_mod Fermat(1) by Lm23;
hence thesis by Th51,Th58;
end;
theorem
17 is prime
proof
A2: 17 -'1 = 17 - 1 by XREAL_0:def 2
.= 16 + 0;
(Fermat(2) -'1) div 2 = 16*0 + 8 by A2,Th52;
then Fermat(2) divides (3 |^ ((Fermat(2)-'1) div 2)) + 1 by Lm24;
then Fermat(2) divides ((3 |^ ((Fermat(2)-'1) div 2 )) - (-1));
then (3 |^ ((Fermat(2)-'1) div 2)), (-1) are_congruent_mod Fermat(2);
hence thesis by Th52,Th58;
end;
theorem
257 is prime
proof
257 -'1 = 257 - 1 by XREAL_0:def 2
.= 256 + 0;
then Fermat(3) divides ((3 |^ ((Fermat(3)-'1) div 2 )) - (-1)) by Lm47,Th53;
then (3 |^ ((Fermat(3)-'1) div 2)), (-1) are_congruent_mod Fermat(3);
hence thesis by Th53,Th58;
end;
theorem
256*256+1 is prime
proof
A2: 256*256 + 1 -'1 = 256*256 + 1 - 1 by XREAL_0:def 2
.= 256*256 + 0;
Fermat(4) divides ((3 |^ ((Fermat(4)-'1) div 2 )) - (-1)) by A2,Lm48,Th54;
then (3 |^ ((Fermat(4)-'1) div 2)), (-1) are_congruent_mod Fermat(4);
hence thesis by Th54,Th58;
end;
:: Moved from JORDAN1A, AK, 21.02.2006
theorem Th63:
for i,j being Integer holds i mod j = 0 implies i div j = i / j
proof
let i,j be Integer such that
A2: i mod j = 0;
per cases;
suppose
A1: j <> 0;
i = (i div j) * j + (i mod j) by A1,INT_1:59
.= (i div j) * j by A2;
hence thesis by A1,XCMPLX_1:89;
end;
suppose j = 0;
hence thesis by XCMPLX_1:49;
end;
end;
theorem
for i,n being Nat st n > 0 holds i |^ n div i = i |^ n / i
proof
let i,n be Nat;
assume n > 0;
then i |^ n mod i = 0 by Th36;
hence thesis by Th63;
end;
reserve r for Real;
theorem Th65:
for n being Nat holds 0 < n & 1 < r implies 1 < r|^n
proof
let n be Nat;
assume that
A1: 0 < n and
A2: r > 1;
defpred P[Nat] means 0 < $1 implies 1 < r|^$1;
A3: for k being Nat holds P[k] implies P[k+1]
proof
let k be Nat;
assume that
A4: P[k] and
0 < k+1;
per cases;
suppose
k > 0;
then
r|^(k+1) = (r|^k)*r & 1 * r <= (r|^k)*r by A2,A4,NEWTON:6,XREAL_1:64;
hence thesis by A2,XXREAL_0:2;
end;
suppose
k = 0;
hence thesis by A2;
end;
end;
A5: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A5,A3);
hence thesis by A1;
end;
theorem
for m,n being Nat holds r > 1 & m > n implies r|^m > r|^n
proof
let m,n be Nat;
assume that
A1: r > 1 and
A2: m > n;
reconsider m,n as Element of NAT by ORDINAL1:def 12;
(m-'n)+n = m by A2,XREAL_1:235;
then
A3: r|^m = r|^(m-'n)*r|^n by NEWTON:8;
m-'n <> 0 by A2,NAT_D:36;
then r|^(m-'n) > 1 by A1,Th65;
hence thesis by A1,A3,NEWTON:83,XREAL_1:155;
end;