Copyright (c) 1998 Association of Mizar Users
environ
vocabulary EULER_1, NAT_1, SQUARE_1, ARYTM_3, INT_1, FINSET_1, ARYTM_1,
ABSVALUE, FILTER_0, MATRIX_2, CARD_1, POWER, FINSEQ_1, PEPIN, RELAT_1,
GROUP_1;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, INT_1, INT_2,
NAT_1, CARD_1, SETWOP_2, SERIES_1, BINARITH, ABIAN, SQUARE_1, EULER_1,
EULER_2, FINSET_1, GROUP_1;
constructors REAL_1, SERIES_1, BINARITH, ABIAN, SQUARE_1, EULER_1, EULER_2,
SETWOP_2, GROUP_1, INT_2, MEMBERED;
clusters INT_1, XREAL_0, ABIAN, FINSET_1, FINSUB_1, SQUARE_1, MEMBERED,
NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, INT_1;
theorems REAL_2, REAL_1, NAT_1, NAT_2, NAT_LAT, INT_1, INT_2, FINSEQ_1,
AXIOMS, GOBOARD9, CARD_2, FINSET_1, SQUARE_1, GROUP_4, AMI_5, RLVECT_1,
GR_CY_1, EULER_1, EULER_2, BINARITH, PCOMPS_2, PREPOWER, PRE_FF, POWER,
ABSVALUE, JORDAN4, NEWTON, SCMFSA9A, XCMPLX_0, XCMPLX_1;
schemes NAT_1;
begin :: Some selected Basic Theorems
reserve d,i,j,k,m,n,p,q,x,y,n1,n2,k1,k2 for Nat,
a,b,c,i1,i2,i3,i5 for Integer;
Lm1:
for i1,i2,n1,n2 st i1 = n1 & i2 = n2
holds i1 divides i2 iff n1 divides n2
proof
let i1,i2 be Integer, n1,n2 be Nat;
assume A1:i1 = n1 & i2 = n2;
A2:n1 >= 0 by NAT_1:18;
A3:n2 >= 0 by NAT_1:18;
A4:abs i1 = n1 by A1,A2,ABSVALUE:def 1;
abs i2 = n2 by A1,A3,ABSVALUE:def 1;
hence thesis by A4,INT_2:21;
end;
Lm2:
n > 1 & n*a > 0 implies a > 0
proof
assume A1:n > 1 & n*a > 0;
assume A2:a <= 0;
n <> 0 by A1;
then n > 0 by NAT_1:19;
hence contradiction by A1,A2,REAL_2:123;
end;
Lm3:
n > 1 & x >= 1 & y >= 0 & 1 = (x*y*n + x + y) implies x = 1 & y = 0
proof
assume A1:n > 1 & x >= 1 & y >= 0 & 1 = (x*y*n + x + y);
now per cases by A1,AXIOMS:21;
suppose A2:x > 1;
now per cases by A1;
suppose A3:y > 0;
then A4: x*y > 1*y by A2,REAL_1:70;
then (x*y)*n > 1*(x*y) by A1,REAL_1:70;
then x*y*n > 0 by A3,A4,AXIOMS:22;
then x*y*n + x > 0 + x by REAL_1:53;
then A5:x*y*n + x > 1 by A2,AXIOMS:22;
y + 1 > 0 + 1 by A3,REAL_1:53;
hence thesis by A1,A5,AXIOMS:24;
suppose y = 0;
hence thesis by A1;
end;
hence thesis;
suppose A6:x = 1;
now per cases by A1;
suppose A7:y > 0;
then x*y*n > 0 by A1,A6,REAL_1:70;
then A8:x*y*n + x > 0 + 1 by A6,REAL_1:53;
y + 1 > 0 + 1 by A7,REAL_1:53;
hence thesis by A1,A8,AXIOMS:24;
suppose y = 0;
hence thesis by A6;
end;
hence thesis;
end;
hence thesis;
end;
Lm4:
2 |^ (2 |^ n) > 1
proof
defpred P[Nat] means 2 |^ (2 |^ $1) > 1;
2 |^ 0 = 1 by NEWTON:9;
then 2 |^ (2 |^ 0) = 2 by NEWTON:10;
then A1: P[0];
A2:for k being Nat holds P[k] implies P[k+1]
proof
let k;
assume A3:2 |^ (2 |^ k) > 1;
A4:2 |^ (k + 1) = (2 |^ k)*2 by NEWTON:11;
2 |^ (2 |^ k) < (2 |^ (2 |^ k)) |^ 2 by A3,PREPOWER:21;
then 1 < (2 |^ (2 |^ k)) |^ 2 by A3,AXIOMS:22;
hence thesis by A4,NEWTON:14;
end;
for n being Nat holds P[n] from Ind(A1,A2);
hence thesis;
end;
Lm5:
n <> 0 implies n - 1 >= 0
proof
assume n <> 0;
then n >= 1 by RLVECT_1:99;
then n-1 >= 1-1 by REAL_1:49;
hence thesis;
end;
Lm6:
n <> 0 implies n -'1 + 1 = (n + 1) -'1
proof
assume n <> 0;
then A1:n >= 1 by RLVECT_1:99;
then n - 1 >= 1 - 1 by REAL_1:49;
then A2:n -' 1 + 1 = n - 1 + 1 by BINARITH:def 3
.= n + -1 + 1 by XCMPLX_0:def 8
.= n + 1 + -1 by XCMPLX_1:1
.= n + 1 - 1 by XCMPLX_0:def 8;
n + 1 >= 1 by A1,NAT_1:38;
then (n + 1) - 1 >= 1 - 1 by REAL_1:49;
hence thesis by A2,BINARITH:def 3;
end;
Lm7:
i,j are_relative_prime implies j,i are_relative_prime
proof
assume i,j are_relative_prime;
then i hcf j = 1 by INT_2:def 6;
hence thesis by INT_2:def 6;
end;
theorem
for i holds i,i+1 are_relative_prime
proof
let k be Nat;
k hcf (k+1) = (1+k*1) hcf k
.= 1 hcf k by EULER_1:9
.= 1 by NAT_LAT:35;
hence thesis by INT_2:def 6;
end;
theorem Th2:
for p holds p is prime implies m,p are_relative_prime or m hcf p = p
proof
let p be Nat;
assume A1:p is prime;
m hcf p divides p by NAT_1:def 5;
then m hcf p = 1 or m hcf p = p by A1,INT_2:def 5;
hence thesis by INT_2:def 6;
end;
theorem Th3:
k divides n*m & n,k are_relative_prime implies k divides m
proof
assume A1:k divides n*m & n,k are_relative_prime;
then n hcf k = 1 by INT_2:def 6;
then A2:(n*m hcf k*m) = m by EULER_1:6;
k divides k*m by NAT_1:56;
hence thesis by A1,A2,NAT_LAT:32;
end;
theorem Th4:
n divides m & k divides m & n,k are_relative_prime implies (n*k) divides m
proof
assume A1: n divides m & k divides m & n,k are_relative_prime;
then consider t1 be Nat such that
A2:m = n*t1 by NAT_1:def 3;
k divides t1 by A1,A2,Th3;
then consider t2 be Nat such that
A3:t1 = k*t2 by NAT_1:def 3;
m = (n*k)*t2 by A2,A3,XCMPLX_1:4;
hence thesis by NAT_1:def 3;
end;
definition let n be Nat;
redefine func n^2 -> Nat;
coherence
proof
defpred P[Nat] means $1^2 is Nat;
A1:P[0] by SQUARE_1:60;
A2:for k be Nat st P[k] holds P[k+1]
proof
let kk be Nat;
assume A3:kk^2 is Nat;
A4:i + j + k is Nat;
(kk+1)^2 = kk^2 + 2*kk + 1 by SQUARE_1:65;
hence thesis by A3,A4;
end;
for k being Nat holds P[k] from Ind(A1,A2);
hence thesis;
end;
end;
theorem
c > 1 implies 1 mod c = 1
proof
assume A1:c > 1;
then A2:c <> 0;
1 div c = 0 by A1,PRE_FF:4;
then 1 mod c = 1 - 0*c by A2,INT_1:def 8
.= 1;
hence thesis;
end;
theorem Th6:
for i st i <> 0 holds i divides n iff n mod i = 0
proof
let i;
assume A1:i <> 0;
A2:i divides n implies n mod i = 0
proof
assume i divides n;
then consider t being Nat such that
A3:n = i*t by NAT_1:def 3;
thus thesis by A3,GROUP_4:101;
end;
n mod i = 0 implies i divides n
proof
assume n mod i = 0;
then consider t being Nat such that
A4:n = i*t + 0 & 0 < i by A1,NAT_1:def 2;
thus thesis by A4,NAT_1:def 3;
end;
hence thesis by A2;
end;
theorem Th7:
m <> 0 & m divides n mod m implies m divides n
proof
assume A1:m <> 0 & m divides n mod m;
then consider x such that A2:n mod m = m * x by NAT_1:def 3;
A3:m > 0 by A1,NAT_1:19;
n mod m + m * (n div m) = m * (x + (n div m)) by A2,XCMPLX_1:8;
then n = m * (x + (n div m)) by A3,NAT_1:47;
hence thesis by NAT_1:def 3;
end;
theorem
0 < n & m mod n = k implies n divides (m - k)
proof
assume 0 < n & m mod n = k;
then A1:m = n*(m div n) + k by NAT_1:47;
take m div n;
thus thesis by A1,XCMPLX_1:26;
end;
theorem
i*p <> 0 & p is prime & k mod i*p < p
implies k mod i*p = k mod p
proof
assume A1:i*p <> 0 & p is prime & k mod i*p < p;
set T = k mod i*p;
consider n being Nat such that
A2:k = (i*p)*n + T & T < i*p by A1,NAT_1:def 2;
k = p*(i*n) + T by A2,XCMPLX_1:4;
then k mod p = T mod p by GR_CY_1:1
.= T by A1,GR_CY_1:4;
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 8
.= (a*p + 1) - ([\(a*p + 1)/p/])*p by INT_1:def 7
.= (a*p + 1) - ([\(a*p/p)+(1/p)/])*p by XCMPLX_1:63
.= (a*p + 1) - ([\(a)+(1/p)/])*p by A1,XCMPLX_1:90
.= (a*p + 1) - (a+[\(1/p)/])*p by INT_1:51
.= (a*p + 1) - (a*p + [\(1/p)/]*p) by XCMPLX_1:8
.= (a*p + 1) - a*p - [\(1/p)/]*p by XCMPLX_1:36
.= (a*p - a*p + 1) - [\(1/p)/]*p by XCMPLX_1:29
.= (0 + 1) - [\(1/p)/]*p by XCMPLX_1:14
.= 1 - (1 div p)*p by INT_1:def 7;
then (a*p + 1) mod p = 1 mod p by A1,INT_1:def 8;
hence thesis by SCMFSA9A:5;
suppose A2: p = 0;
hence (a*p + 1) mod p = 0 by INT_1:def 8
.= 1 mod p by A2,NAT_1:def 2;
end;
theorem Th11:
1 < m & (n*k) mod m = k mod m & k,m are_relative_prime
implies n mod m = 1
proof
assume A1:1 < m & (n*k) mod m = k mod m & k,m are_relative_prime;
then A2:m <> 0;
then consider t1 being Nat such that
A3:n*k = m*t1 + ((n*k) mod m) & ((n*k) mod m) < m by NAT_1:def 2;
A4:(n*k) mod m = n*k - m*t1 by A3,XCMPLX_1:26;
consider t2 being Nat such that
A5:k = m*t2 + (k mod m) & (k mod m) < m by A2,NAT_1:def 2;
n*k - m*t1 = k - m*t2 by A1,A4,A5,XCMPLX_1:26;
then n*k - k = m*t1 - m*t2 by XCMPLX_1:24
.= m*(t1 - t2) by XCMPLX_1:40;
then n*k - 1*k = m*(t1 - t2);
then k*(n - 1) = m*(t1 - t2) by XCMPLX_1:40;
then A6:m divides k*(n - 1) by INT_1:def 9;
reconsider n,m,k as Integer;
k,m are_relative_prime by A1,EULER_2:1;
then m divides (n - 1) by A6,INT_2:40;
then consider tt being Integer such that
A7:n - 1 = m*tt by INT_1:def 9;
A8:n = m*tt + 1 by A7,XCMPLX_1:27;
reconsider n,m as Nat;
n mod m = (n qua Integer) mod m by SCMFSA9A:5
.= (1 qua Integer) mod m by A8,EULER_1:13
.= 1 mod m by SCMFSA9A:5
.= 1 by A1,GROUP_4:102;
hence thesis;
end;
theorem Th12:
(p |^ k) mod m = ((p mod m) |^ k) mod m
proof
defpred P[Nat] means
(p |^ $1) mod m = ((p mod m) |^ $1) mod m;
A1:P[0]
proof
(p |^ 0) mod m = 1 mod m by NEWTON:9;
hence thesis by NEWTON:9;
end;
A2:for n st P[n] holds P[n+1]
proof
let n;
assume A3:P[n];
(p |^ (n+1)) mod m = ((p |^ n)*(p |^ 1)) mod m by NEWTON:13
.= ((p |^ n)*p) mod m by NEWTON:10
.= (((p |^ n) mod m)*(p mod m)) mod m by EULER_2:11
.= (((p mod m) |^ n)*(p mod m)) mod m
by A3,EULER_2:10
.= ((p mod m) |^ (n + 1)) mod m by NEWTON:11;
hence thesis;
end;
for n holds P[n] from Ind(A1,A2);
hence thesis;
end;
Lm8:
i^2 = (i+1)*(i-1) + 1
proof
(i+1)*(i-1) = i^2 - 1 by SQUARE_1:59,67;
then (i+1)*(i-1) + 1 = i^2 - (1 - 1) by XCMPLX_1:37
.= i^2;
hence thesis;
end;
Lm9:
k*(2 |^ (n+1)) div 2 = k*(2 |^ n)
proof
k*(2 |^ (n+1)) = k*(2 |^ n*2) by NEWTON:11
.= k*2 |^ n*2 by XCMPLX_1:4;
hence thesis by AMI_5:3;
end;
Lm10:
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:28;
m |^ n = (m |^ k)*(m |^ t) by A1,NEWTON:13;
hence thesis by NAT_1:def 3;
end;
Lm11:
2 |^ 2 = 4
proof
2 |^ 2 = 2 |^ (1+1)
.= 2 |^ 1 * 2 by NEWTON:11
.= 2 * 2 by NEWTON:10;
hence thesis;
end;
Lm12:
2 |^ 3 = 8
proof
2 |^ 3 = 2 |^ (2+1)
.= 4 * 2 by Lm11,NEWTON:11;
hence thesis;
end;
Lm13:
2 |^ 4 = 16
proof
2 |^ 4 = 2 |^ (2+2)
.= 4 * 4 by Lm11,NEWTON:13;
hence thesis;
end;
Lm14:
2 |^ 8 = 256
proof
2 |^ 8 = 2 |^ (4+4)
.= 16*16 by Lm13,NEWTON:13;
hence thesis;
end;
theorem
i <> 0 implies i^2 mod (i+1) = 1
proof
assume A1:i <> 0;
then i > 0 by NAT_1:19;
then A2:i+1 > 0+1 by REAL_1:53;
i >= 1 by A1,RLVECT_1:99;
then i-1 >= 1-1 by REAL_1:49;
then reconsider I = i-1 as Nat by INT_1:16;
reconsider II = (i+1)*I as Nat;
i^2 mod (i+1) = (II + 1) mod (i+1) by Lm8
.= (II mod (i+1) + 1) mod (i+1) by GR_CY_1:2
.= (0 + 1) mod (i+1) by GROUP_4:101
.= 1 by A2,GR_CY_1:4;
hence thesis;
end;
theorem
k^2 < j & i mod j = k implies i^2 mod j = k^2
proof
assume A1: k^2 < j & i mod j = k;
per cases;
suppose
j <> 0;
then consider n being Nat such that
A2:i = j*n + k & k < j by A1,NAT_1:def 2;
i^2 = i*i by SQUARE_1:def 3
.= (j*n + k)*(j*n) + (j*n + k)*k by A2,XCMPLX_1:8
.= (j*n)*(j*n) + k*(j*n) + (j*n + k)*k by XCMPLX_1:8
.= (j*n)*(j*n) + k*(j*n) + ((j*n)*k + k*k) by XCMPLX_1:8
.= j*(n*j*n) + k*(j*n) + ((j*n)*k + k*k) by XCMPLX_1:4
.= j*(n*j*n) + j*(k*n) + ((j*n)*k + k*k) by XCMPLX_1:4
.= j*(n*j*n) + j*(k*n) + (j*(n*k) + k*k) by XCMPLX_1:4
.= j*(n*j*n) + j*(k*n) + j*(n*k) + k*k by XCMPLX_1:1
.= j*((n*j*n) + (k*n)) + j*(n*k) + k*k by XCMPLX_1:8
.= j*((n*j*n) + (k*n) + (n*k)) + k*k by XCMPLX_1:8
.= j*((n*j*n) + (k*n) + (n*k)) + k^2 by SQUARE_1:def 3;
then i^2 mod j = k^2 mod j by GR_CY_1:1;
hence thesis by A1,GR_CY_1:4;
suppose
j = 0;
hence i^2 mod j = k^2 by A1,NAT_1:def 2,SQUARE_1:60;
end;
theorem
p is prime & i mod p = -1 implies i^2 mod p = 1
proof
assume A1:p is prime & i mod p = -1;
then A2:p > 1 by INT_2:def 5;
A3:p <> 0 by A1,INT_2:def 5;
reconsider i as Integer;
i mod p = i - (i div p)*p by A3,INT_1:def 8;
then i = i mod p + (i div p)*p by XCMPLX_1:27
.= -1 + (i div p)*p by A1,SCMFSA9A:5
.= (i div p)*p - 1 by XCMPLX_0:def 8;
then A4:i^2
= ((i div p)*p)^2 - 2*((i div p)*p) + 1 by SQUARE_1:66
.= ((i div p)*p)*((i div p)*p) - 2*((i div p)*p) + 1 by SQUARE_1:def 3
.= (((i div p)*p) - 2)*((i div p)*p) + 1 by XCMPLX_1:40
.= ((((i div p)*p) - 2)*(i div p))*p + 1 by XCMPLX_1:4;
reconsider ii = (((i div p)*p) - 2)*(i div p) as Integer;
reconsider i as Nat;
i^2 mod p = (ii*p + 1) mod p by A4,SCMFSA9A:5
.= 1 mod p by Th10
.= 1 by A2,GR_CY_1:4;
hence thesis;
end;
theorem Th16:
n is even implies n + 1 is odd
proof
assume n is even;
then n mod 2 = 0 by NAT_2:23;
then consider k being Nat such that
A1:n = 2*k + 0 & 0 < 2 by NAT_1:def 2;
(n + 1) mod 2 = 1 mod 2 by A1,GR_CY_1:1
.= 1 by GROUP_4:102;
hence thesis by NAT_2:24;
end;
theorem
p > 2 & p is prime implies p is odd
proof
assume A1:p > 2 & p is prime;
assume p is even;
then p mod 2 = 0 by NAT_2:23;
then consider k being Nat such that
A2:p = 2*k + 0 & 0 < 2 by NAT_1:def 2;
2 divides p by A2,NAT_1:def 3;
hence contradiction by A1,INT_2:def 5;
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:19;
hence thesis by NAT_2:23;
end;
Lm15:
i is even & j is even implies i*j is even
proof
assume i is even & j is even;
then reconsider i'=i, j'=j as even Nat;
i'*j' is even;
hence thesis;
end;
theorem Th19:
i is odd & j is odd implies i*j is odd
proof
assume i is odd & j is odd;
then A1:i mod 2 = 1 & j mod 2 = 1 by NAT_2:24;
then consider k being Nat such that
A2:i = 2*k+1 & 1 < 2 by NAT_1:def 2;
consider t being Nat such that
A3:j = 2*t+1 & 1 < 2 by A1,NAT_1:def 2;
i*j = (2*k)*(2*t)+(2*k)*1+1*(2*t)+1*1 by A2,A3,XCMPLX_1:10
.= (2*k)*(2*t)+(2*k)+(2*t)+1;
hence thesis;
end;
theorem
for k holds i is odd implies i |^ k is odd
proof
let k;
assume A1:i is odd;
A2:i |^ 0 = 1 by NEWTON:9;
defpred P[Nat] means i |^ $1 is odd;
1 mod 2 = 1 by GR_CY_1:4;
then A3: P[0] by A2,NAT_2:24;
A4: for n being Nat holds P[n] implies P[n+1]
proof
let n be Nat;
assume A5:i |^ n is odd;
i |^ (n+1) = i |^ n * i by NEWTON:11;
hence thesis by A1,A5,Th19;
end;
for n being Nat holds P[n] from Ind(A3,A4);
hence thesis;
end;
theorem Th21:
k > 0 & i is even implies i |^ k is even
proof
assume A1:k > 0 & i is even;
defpred P[Nat] means
$1 > 0 & i is even implies i |^ $1 is even;
A2:P[0];
A3:for n being Nat holds P[n] implies P[n+1]
proof
let n be Nat;
assume A4:P[n];
P[n+1]
proof
now per cases;
suppose n = 0;
hence thesis by NEWTON:10;
suppose n <> 0;
then (i |^ n)*i is even by A1,A4,Lm15,NAT_1:19;
hence thesis by NEWTON:11;
end;
hence thesis;
end;
hence thesis;
end;
for n being Nat holds P[n] from Ind(A2,A3);
hence thesis by A1;
end;
theorem
2 divides n iff n is even
proof
A1:2 divides n implies n is even
proof
assume 2 divides n;
then consider k being Nat such that
A2:n = 2*k by NAT_1:def 3;
thus thesis by A2;
end;
n is even implies 2 divides n
proof
assume n is even;
then n mod 2 = 0 by NAT_2:23;
then consider k being Nat such that
A3:n = 2*k + 0 & 0 < 2 by NAT_1:def 2;
thus thesis by A3,NAT_1:def 3;
end;
hence thesis by A1;
end;
theorem
m*n is even implies m is even or n is even by Th19;
theorem Th24:
n |^ 2 = n^2
proof
n |^ 2 = n |^ (1 + 1)
.= n |^ 1*n |^ 1 by NEWTON:13
.= n*n |^ 1 by NEWTON:10
.= n*n by NEWTON:10
.= n^2 by SQUARE_1:def 3;
hence thesis;
end;
canceled;
theorem Th26:
m > 1 & n > 0 implies m |^ n > 1
proof
assume A1:m > 1 & n > 0;
then m <> 0;
then A2:m > 0 by NAT_1:19;
defpred P[Nat] means
$1 > 0 implies m |^ $1 > 1;
A3: P[0];
A4: for n being Nat holds P[n] implies P[n+1]
proof
let n;
assume A5:P[n];
A6:m |^ (n+1) = (m |^ n)*(m |^ 1) by NEWTON:13
.= (m |^ n)*m by NEWTON:10;
P[n+1]
proof
now per cases;
suppose n = 0;
hence thesis by A1,NEWTON:10;
suppose n <> 0;
then (m |^ n)*m > 1*m by A2,A5,NAT_1:19,REAL_1:70;
hence thesis by A1,A6,AXIOMS:22;
end;
hence thesis;
end;
hence thesis;
end;
for n being Nat holds P[n] from Ind(A3,A4);
hence thesis by A1;
end;
Lm16:
(2 |^ (2 |^ n))^2 = (2 |^ (2 |^ (n + 1)))
proof
defpred P[Nat] means (2 |^ (2 |^ $1))^2 = (2 |^ (2 |^ ($1 + 1)));
A1: P[0]
proof
A2:2 |^ 0 = 1 by NEWTON:9;
2 |^ (0 + 1) = 2 by NEWTON:10;
then 2 |^ (2 |^ (0 + 1)) = 2 to_power 2 by POWER:46
.= 2^2 by POWER:53;
hence thesis by A2,NEWTON:10;
end;
A3:for k being Nat st P[k] holds P[k+1]
proof
let x be Nat;
assume A4:(2 |^ (2 |^ x))^2 = (2 |^ (2 |^ (x + 1)));
(2 |^ (2 |^ (x + 1)))^2 = (2 |^ ((2 |^ x)*2))^2 by NEWTON:11
.= ((2 |^ (2 |^ x)) |^ 2)^2 by NEWTON:14
.= ((2 |^ (2 |^ x))^2)^2 by Th24
.= (2 |^ (2 |^ (x + 1))) |^ 2 by A4,Th24
.= 2 |^ ((2 |^ (x + 1))*2) by NEWTON:14
.= 2 |^ (2 |^ ((x + 1) + 1)) by NEWTON:11;
hence thesis;
end;
for k being Nat holds P[k] from Ind(A1,A3);
hence thesis;
end;
theorem Th27:
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:P[0];
A3:for m being Nat holds P[m] implies P[m+1]
proof
let m be Nat;
assume P[m];
now per cases;
suppose A4:m = 0;
n*(n |^ ((0+1) -' 1)) = n*(n |^ 0) by GOBOARD9:1
.= n*1 by NEWTON:9;
hence thesis by A4,NEWTON:10;
suppose A5:m <> 0;
then A6:m >= 1 by RLVECT_1:99;
n |^ (m+1) = (n |^ m) * n by NEWTON:11
.= (n |^ (m -' 1 + 1))*n by A6,AMI_5:4
.= n*(n |^ ((m + 1) -' 1)) by A5,Lm6;
hence thesis;
end;
hence thesis;
end;
for m being Nat holds P[m] from Ind(A2,A3);
hence thesis by A1;
end;
theorem Th28:
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))*(n |^ (m div 2)) by SQUARE_1:def 3
.= n |^ ((m div 2) + (m div 2)) by NEWTON:13
.= n |^ ((m + m) div 2) by A1,GROUP_4:106
.= n |^ ((2*m) div 2) by XCMPLX_1:11
.= n |^ m by GROUP_4:107;
hence thesis;
end;
theorem Th29:
n <> 0 & 1 <= k implies (n |^ k) div n = n |^ (k -'1)
proof
assume A1:n <> 0 & 1 <= k;
then A2: k - 1 >= 1 - 1 by REAL_1:49;
k = k + (1 - 1)
.= k + 1 - 1 by XCMPLX_1:29
.= k - 1 + 1 by XCMPLX_1:29
.= (k -'1) + 1 by A2,BINARITH:def 3;
then n |^ k = n*(n |^ (k -'1)) by NEWTON:11;
hence thesis by A1,GROUP_4:107;
end;
theorem
2 |^ (n + 1) = (2 |^ n)+(2 |^ n)
proof
defpred P[Nat] means 2 |^ ($1+1) = (2 |^ $1)+(2 |^ $1);
A1: P[0]
proof
2 |^ (0+1) = 1 + 1 by NEWTON:10
.= (2 |^ 0)+1 by NEWTON:9
.= (2 |^ 0)+(2 |^ 0) by NEWTON:9;
hence thesis;
end;
A2:for m st P[m] holds P[m+1]
proof
let m;
assume A3:2 |^ (m+1) = (2 |^ m)+(2 |^ m);
(2 |^ (m+1))+(2 |^ (m+1)) = 2*(2 |^ m)+(2 |^ (m+1)) by NEWTON:11
.= 2*(2 |^ m)+2*(2 |^ m) by NEWTON:11
.= 2*((2 |^ m)+(2 |^ m)) by XCMPLX_1:8
.= 2 |^ ((m+1)+1) by A3,NEWTON:11;
hence thesis;
end;
for n holds P[n] from Ind(A1,A2);
hence thesis;
end;
theorem Th31:
k > 1 & k |^ n = k |^ m implies n = m
proof
assume A1:k > 1 & k |^ n = k |^ m;
then A2:k <> 0;
then A3:k > 0 by NAT_1:19;
now per cases;
suppose n = m;
hence thesis;
suppose not (n = m);
then A4:k to_power m <> k to_power n by A1,A3,POWER:57;
k to_power n = k |^ n by A2,POWER:46;
hence thesis by A1,A2,A4,POWER:46;
end;
hence thesis;
end;
Lm17:
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:28;
m + n - n > n - n by A1,A3,REAL_1:54;
then m + n - n > 0 by XCMPLX_1:14;
then m + n + -n > 0 by XCMPLX_0:def 8;
then m + (n + -n) > 0 by XCMPLX_1:1;
then m + (1 + -1) > 0 by XCMPLX_0:def 6;
then m + 1 + -1 > 0 by XCMPLX_1:1;
then m + 1 - 1 > 1 - 1 by XCMPLX_0:def 8;
then m + 1 > 1 by REAL_1:49;
then A4:m >= 1 by NAT_1:38;
A5: x |^ k = x |^ n * x |^ m by A3,NEWTON:13;
x |^ n >= 1 by A2,PREPOWER:19;
then A6: x |^ n > 0 by AXIOMS:22;
1 |^ m = 1 by NEWTON:15;
then x |^ m > 1 by A2,A4,PREPOWER:18;
hence thesis by A5,A6,REAL_2:144;
end;
Lm18:
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
assume A2:2 |^ m divides 2 |^ n;
2 |^ n < 2 |^ m by A1,Lm17;
then (2 |^ n) div (2 |^ m) = 0 by JORDAN4:5;
then 2 |^ n > 2 |^ m * ((2 |^ n) div (2 |^ m)) by PREPOWER:13;
hence contradiction by A2,NAT_1:49;
end;
hence thesis;
end;
hence thesis;
end;
theorem
m <= n iff 2 |^ m divides 2 |^ n by Lm10,Lm18;
theorem Th33:
p is prime & i divides p |^ n implies i = 1 or (ex k being Nat st i = p*k)
proof
assume A1:p is prime;
then A2:p <> 0 by INT_2:def 5;
defpred P[Nat] means
i divides p |^ $1 implies i = 1 or (ex k being Nat st i = p*k);
A3:P[0]
proof
now assume i divides p |^ 0;
then i divides 1 by NEWTON:9;
then consider t being Nat such that
A4:1 = i*t by NAT_1:def 3;
thus thesis by A4,NAT_1:40;
end;
hence thesis;
end;
A5:for n holds P[n] implies P[n+1]
proof
let n;
assume A6:P[n];
now assume i divides p |^ (n+1);
then consider u1 being Nat such that
A7:p |^ (n+1) = i*u1 by NAT_1:def 3;
p*(p |^ n) = i*u1 by A7,NEWTON:11;
then A8:p divides i*u1 by NAT_1:def 3;
now per cases by A1,A8,NAT_LAT:95;
suppose p divides i;
then consider w1 being Nat such that
A9:i = p*w1 by NAT_1:def 3;
thus thesis by A9;
suppose p divides u1;
then consider w2 being Nat such that
A10:u1 = p*w2 by NAT_1:def 3;
p*(p |^ n) = i*(p*w2) by A7,A10,NEWTON:11
.= p*(i*w2) by XCMPLX_1:4;
then p |^ n = p*(i*w2) div p by A2,GROUP_4:107;
then p |^ n = i*w2 by A2,GROUP_4:107;
then consider w3 being Nat such that
A11:i = p*w3 or i = 1 by A6,NAT_1:def 3;
thus thesis by A11;
end;
hence thesis;
end;
hence thesis;
end;
for n holds P[n] from Ind(A3,A5);
hence thesis;
end;
theorem Th34:
for n st n <> 0 & p is prime & n < p |^ (k+1) holds
n divides p |^ (k+1) iff n divides p |^ k
proof
let n;
assume A1:n <> 0 & p is prime & n < p |^ (k+1);
then A2:p <> 0 by INT_2:def 5;
A3:n divides p |^ (k+1) implies n divides p |^ k
proof
assume A4:n divides p |^ (k+1);
now per cases by A1,A4,Th33;
suppose n = 1;
hence thesis by NAT_1:53;
suppose ex i being Nat st n = p*i;
then consider i being Nat such that
A5:n = p*i;
consider u being Nat such that
A6:p |^ (k+1) = (p*i)*u by A4,A5,NAT_1:def 3;
p*(p |^ k) = (p*i)*u by A6,NEWTON:11
.= p*(i*u) by XCMPLX_1:4;
then A7:p |^ k = p*(i*u) div p by A2,GROUP_4:107;
then A8:p |^ k = i*u by A2,GROUP_4:107;
then A9:u divides p |^ k by NAT_1:def 3;
u <> 1 by A1,A5,A8,NEWTON:11;
then consider j being Nat such that
A10:u = p*j by A1,A9,Th33;
p |^ k = i*(p*j) by A2,A7,A10,GROUP_4:107
.= n*j by A5,XCMPLX_1:4;
hence thesis by NAT_1:def 3;
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_1:56;
hence thesis by NEWTON:11;
end;
hence thesis by A3;
end;
theorem Th35:
for k holds p is prime & d divides (p |^ k) & d <> 0
implies ex t being Nat st d = p |^ t & t <= k
proof
let n;
assume A1:p is prime & d divides (p |^ n) & d <> 0;
then p <> 0 by INT_2:def 5;
then A2:p > 0 by NAT_1:19;
defpred P[Nat] means
d divides (p |^ $1) implies ex t being Nat st d = p |^ t & t <= $1;
A3:P[0]
proof
assume A4:d divides (p |^ 0);
d = p |^ 0
proof
consider t being Nat such that
A5:p |^ 0 = d*t by A4,NAT_1:def 3;
d*t = 1 by A5,NEWTON:9;
then d = 1 by NAT_1:40;
hence thesis by NEWTON:9;
end;
hence thesis;
end;
A6:for n st P[n] holds P[n+1]
proof
let n;
assume A7:P[n];
now assume A8:d divides (p |^ (n+1));
(p |^ (n+1)) > 0 by A2,PREPOWER:13;
then A9:d <= p |^ (n+1) by A8,NAT_1:54;
now per cases by A9,AXIOMS:21;
suppose d < p |^ (n+1);
then consider t being Nat such that
A10:d = p |^ t & t <= n by A1,A7,A8,Th34;
t <= n + 1 by A10,NAT_1:37;
hence thesis by A10;
suppose d = p |^ (n+1);
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
for n holds P[n] from Ind(A3,A6);
hence thesis by A1;
end;
theorem Th36:
p > 1 & i mod p = 1 implies (i |^ n) mod p = 1
proof
assume A1:p > 1 & i mod p = 1;
defpred P[Nat] means (i |^ $1) mod p = 1;
1 mod p = 1 by A1,GR_CY_1:4;
then A2: P[0] by NEWTON:9;
A3:for k being Nat 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:11
.= (((i |^ k) mod p)*i) mod p by EULER_2:10
.= 1 by A1,A4;
hence thesis;
end;
for n being Nat holds P[n] from Ind(A2,A3);
hence thesis;
end;
theorem
m > 0 implies (n |^ m) mod n = 0
proof
assume A1:m > 0;
defpred P[Nat] means
$1 > 0 implies (n |^ $1) mod n = 0;
A2:P[0];
A3:for m being Nat holds P[m] implies P[m+1]
proof
let m;
assume P[m];
P[m+1]
proof
n*(n |^ m) mod n = ((n mod n)*(n |^ m)) mod n by EULER_2:10
.= (0*(n |^ m)) mod n by GR_CY_1:5
.= 0 by GR_CY_1:6;
hence thesis by NEWTON:11;
end;
hence thesis;
end;
for n being Nat holds P[n] from Ind(A2,A3);
hence thesis by A1;
end;
theorem Th38:
p is prime & n,p are_relative_prime
implies (n |^ (p -'1)) mod p = 1
proof
assume A1:p is prime & n,p are_relative_prime;
then A2:p > 1 by INT_2:def 5;
A3:p <> 0 by A1,INT_2:def 5;
A4:n <> 0
proof
assume n = 0;
then n hcf p = p by NAT_LAT:36;
then n hcf p > 1 by A1,INT_2:def 5;
hence contradiction by A1,INT_2:def 6;
end;
then (n |^ p) mod p = n mod p by A1,EULER_2:34;
then A5:(n |^ (p -' 1))*n mod p = n mod p by A3,A4,Th27;
A6:p,n are_relative_prime by A1,Lm7;
(n |^ (p -'1)) <> 0 by A4,PREPOWER:12;
hence thesis by A2,A4,A5,A6,EULER_2:27;
end;
theorem Th39:
p is prime & d > 1 & d divides (p |^ k) & not d divides ((p |^ k) div p)
implies d = p |^ k
proof
assume A1:p is prime & d > 1 & d divides (p |^ k) & not d divides
((p |^ k) div p);
then A2:d <> 0;
A3:p <> 0 by A1,INT_2:def 5;
k <> 0
proof
assume k = 0;
then p |^ k = 1 by NEWTON:9;
hence contradiction by A1,NAT_1:54;
end;
then A4:k >= 1 by RLVECT_1:99;
then A5: k - 1 >= 1 - 1 by REAL_1:49;
consider t being Nat such that
A6:d = p |^ t & t <= k by A1,A2,Th35;
not t < k
proof
assume t < k;
then t < k + (1 -1);
then t < k + 1 - 1 by XCMPLX_1:29;
then t < k + 1 + -1 by XCMPLX_0:def 8;
then t < k + -1 + 1 by XCMPLX_1:1;
then t < k - 1 + 1 by XCMPLX_0:def 8;
then t < k -'1 + 1 by A5,BINARITH:def 3;
then t <= k -'1 by NAT_1:38;
then d divides p |^ (k -'1) by A6,Lm10;
hence contradiction by A1,A3,A4,Th29;
end;
hence thesis by A6,AXIOMS:21;
end;
definition let a be Integer;
redefine func a^2 -> Nat;
coherence
proof
A1:a^2 = a*a by SQUARE_1:def 3;
a*a >= 0 by REAL_1:93;
hence thesis by A1,INT_1:16;
end;
end;
theorem Th40:
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 mod n = 1 implies m,1 are_congruent_mod n
proof
assume m mod n = 1;
then consider k being Nat such that
A3:m = n*k + 1 & 1 < n by NAT_1:def 2;
n*k = m - 1 by A3,XCMPLX_1:26;
hence thesis by INT_1:def 3;
end;
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
A4:n*t = m - 1 by INT_1:def 3;
reconsider m,n as Integer;
A5:m mod n = (n*t + 1) mod n by A4,XCMPLX_1:27
.= 1 mod n by EULER_1:13;
reconsider m,n,1' = 1 as Nat;
m mod n = (m qua Integer) mod n by SCMFSA9A:5
.= 1' mod n by A5,SCMFSA9A:5
.= 1' by A1,GROUP_4:102;
hence thesis;
end;
hence thesis by A2;
end;
Lm19:
n > 1 & m > 1 & m,1 are_congruent_mod n implies m mod n = 1
proof
assume A1:n > 1 & m > 1 & m,1 are_congruent_mod n;
then consider d being Integer such that
A2:n*d = m - 1 by INT_1:def 3;
m - 1 > 1 - 1 by A1,REAL_1:54;
then d > 0 by A1,A2,Lm2;
then reconsider d as Nat by INT_1:16;
m = n*d + 1 by A2,XCMPLX_1:27;
then m mod n = 1 mod n by GR_CY_1:1
.= 1 by A1,GROUP_4:102;
hence thesis;
end;
theorem Th41:
a,b are_congruent_mod c implies a^2,b^2 are_congruent_mod c
proof
assume a,b are_congruent_mod c;
then (a*a),(b*b) are_congruent_mod c by INT_1:39;
then a^2,(b*b) are_congruent_mod c by SQUARE_1:def 3;
hence thesis by SQUARE_1:def 3;
end;
canceled;
theorem Th43:
i1,i2 are_congruent_mod i5 & i1,i3 are_congruent_mod i5
implies i2,i3 are_congruent_mod i5
proof
assume i1,i2 are_congruent_mod i5 & i1,i3 are_congruent_mod i5;
then A1:i2,i1 are_congruent_mod i5 & i3,i1 are_congruent_mod i5 by INT_1:35;
then consider t1 being Integer such that
A2:i5*t1 = i2 - i1 by INT_1:def 3;
consider t2 being Integer such that
A3:i5*t2 = i3 - i1 by A1,INT_1:def 3;
i2 = i5*t1 + i1 by A2,XCMPLX_1:27;
then i2 - i3 = (i5*t1 + i1) - (i5*t2 + i1) by A3,XCMPLX_1:27
.= i5*t1 - i5*t2 by XCMPLX_1:32
.= i5*(t1 - t2) by XCMPLX_1:40;
hence thesis by INT_1:def 3;
end;
theorem Th44:
3 is prime
proof
for n holds n divides 3 implies n = 1 or n = 3
proof
let n;
assume A1:n divides 3;
then A2:n <> 0 by INT_2:3;
n <= 3 by A1,NAT_1:54;
then n < 2 + 1 or n = 3 by AXIOMS:21;
then n <= 2 or n = 3 by NAT_1:38;
then n < 1 + 1 or n = 2 or n = 3 by AXIOMS:21;
then n <= 1 or n = 2 or n = 3 by NAT_1:38;
then A3:n < 1 or n = 1 or n = 2 or n = 3 by AXIOMS:21;
n <> 2
proof
assume A4:n = 2;
3 mod 2 = (2*1 + 1) mod 2
.= 1 mod 2 by GR_CY_1:1
.= 1 by GR_CY_1:4;
hence contradiction by A1,A4,Th6;
end;
hence thesis by A2,A3,RLVECT_1:98;
end;
hence thesis by INT_2:def 5;
end;
theorem Th45:
n <> 0 implies Euler n <> 0
proof
assume A1:n <> 0;
assume A2:Euler n = 0;
set X = {k where k is Nat : n,k are_relative_prime & k >= 1 & k <= n};
A3:Card X = 0 by A2,EULER_1:def 1;
X c= Seg n
proof
let x be set;
assume x in X;
then consider xx being Nat such that
A4:x = xx and
n,xx are_relative_prime and
A5:xx >= 1 & xx <= n;
thus thesis by A4,A5,FINSEQ_1:3;
end;
then reconsider X as finite set by FINSET_1:13;
ex k st k in X
proof
A6:1 in X
proof
n hcf 1 = 1 by NAT_LAT:35;
then A7:n,1 are_relative_prime by INT_2:def 6;
1 <= n by A1,RLVECT_1:98;
hence thesis by A7;
end;
take 1;
thus thesis by A6;
end;
hence contradiction by A3,CARD_2:59;
end;
theorem
n <> 0 implies -n < n
proof
assume A1:n <> 0;
assume A2:-n >= n;
A3:n > 0 by A1,NAT_1:19;
then n + n > 0 + n by REAL_1:53;
then n + n > 0 by A3,AXIOMS:22;
hence contradiction by A2,REAL_2:109;
end;
canceled;
theorem Th48:
n <> 0 implies n div n = 1
proof
assume n <> 0;
then n*1 div n = 1 by GROUP_4:107;
hence thesis;
end;
begin :: Public Key Cryptography
definition
let k,m,n;
func Crypto(m,n,k) -> Nat equals
:Def1: (m |^ k) mod n;
coherence;
end;
theorem
p is prime & q is prime & p <> q & n = p*q &
k1,Euler(n) are_relative_prime & (k1*k2) mod Euler(n) = 1
implies for m be Nat st m < n holds Crypto(Crypto(m,n,k1),n,k2) = m
proof
assume A1:p is prime & q is prime & p <> q & n = p*q &
k1,Euler(n) are_relative_prime & (k1*k2) mod Euler(n) = 1;
let m be Nat;
assume A2: m < n;
A3:p <> 0 & q <> 0 by A1,INT_2:def 5;
then p-1 >= 0 & q-1 >= 0 by Lm5;
then reconsider p1 = p-1,q1 = q-1 as Nat by INT_1:16;
A4:p > 1 & q > 1 by A1,INT_2:def 5;
A5:n <> 0 by A1,A3,XCMPLX_1:6;
A6:p > 0 & q > 0 by A3,NAT_1:19;
A7: p,q are_relative_prime by A1,INT_2:47;
Euler n <> 0 by A5,Th45;
then A8:(Euler n) > 0 by NAT_1:19;
A9:p1 + 1 = p - (1 - 1) by XCMPLX_1:37
.= p;
A10:q1 + 1 = q - (1 - 1) by XCMPLX_1:37
.= q;
A11:Euler(n)= Euler(p)*Euler(q) by A1,A4,A7,EULER_1:22
.= (p-1)*Euler(q) by A1,EULER_1:21
.= (p-1)*(q-1) by A1,EULER_1:21;
not(p1=1 & q1=1) by A1,A9,A10;
then A12:p1*q1 <> 1 by NAT_1:40;
A13:k1 <> 0
proof
assume k1 = 0;
then k1 hcf Euler n = Euler n by NAT_LAT:36;
hence contradiction by A1,A11,A12,INT_2:def 6;
end;
k2 <> 0 by A1,GR_CY_1:6;
then A14:k1 >= 1 & k2 >= 1 by A13,RLVECT_1:99;
A15:n > 1 by A1,A4,REAL_2:137;
now per cases;
suppose A16:m = 0;
then m |^ k1 = 0 by A14,NEWTON:16;
then m |^ k1 mod n = 0 by GR_CY_1:6;
then Crypto(m,n,k1) = 0 by Def1;
then Crypto(m,n,k1) |^ k2 = 0 by A14,NEWTON:16;
then (Crypto(m,n,k1) |^ k2) mod n = 0 by GR_CY_1:6;
hence thesis by A16,Def1;
suppose A17:m = 1;
then m |^ k1 = 1 by NEWTON:15;
then m |^ k1 mod n = 1 by A15,GROUP_4:102;
then Crypto(m,n,k1) = 1 by Def1;
then Crypto(m,n,k1) |^ k2 = 1 by NEWTON:15;
then (Crypto(m,n,k1) |^ k2) mod n = 1 by A15,GROUP_4:102;
hence thesis by A17,Def1;
suppose A18: m <> 0 & m <> 1;
A19:for t being Nat holds m |^ (t*p1*q1 + 1) mod n = m
proof
let t be Nat;
now m >= 1 by A18,RLVECT_1:99;
then m |^ (t*p1*q1) >= 1 by PREPOWER:19;
then (m |^ (t*p1*q1)) - 1 >= 1 - 1 by REAL_1:49;
then reconsider a = m |^ (t*p1*q1) -1 as Nat by INT_1:16;
A20:q divides (m*a)
proof
now per cases;
suppose m hcf q = 1;
then m,q are_relative_prime by INT_2:def 6;
then A21:(m |^ (t*p1)),q are_relative_prime
by A3,A18,EULER_2:32;
m |^ (t*p1) <> 0 by A18,PREPOWER:12;
then ((m |^ (t*p1)) |^ (q1+1)) mod q
= (m |^ (t*p1)) mod q
by A1,A10,A21,EULER_2:34;
then (((m |^ (t*p1)) |^ q1)*(m |^ (t*p1))) mod q
= (m |^ (t*p1)) mod q by NEWTON:11;
then ((m |^ (t*p1)) |^ q1) mod q = 1 by A4,A21,Th11;
then (m |^ (t*p1*q1)) mod q = 1 by NEWTON:14;
then (m |^ (t*p1*q1)) = q*((m |^ (t*p1*q1)) div q) + 1
by A6,NAT_1:47;
then a = q*((m |^ (t*p1*q1)) div q) + (1-1) by XCMPLX_1:29;
then q divides a by NAT_1:def 3;
hence thesis by NAT_1:56;
suppose m hcf q <> 1;
then not m,q are_relative_prime by INT_2:def 6;
then m hcf q = q by A1,Th2;
then q divides m by NAT_1:def 5;
hence thesis by NAT_1:56;
end;
hence thesis;
end;
A22:p divides (m*a)
proof
now per cases;
suppose m hcf p = 1;
then m,p are_relative_prime by INT_2:def 6;
then A23:(m |^ (t*q1)),p are_relative_prime
by A3,A18,EULER_2:32;
m |^ (t*q1) <> 0 by A18,PREPOWER:12;
then ((m |^ (t*q1)) |^ (p1+1)) mod p
= (m |^ (t*q1)) mod p
by A1,A9,A23,EULER_2:34;
then (((m |^ (t*q1)) |^ p1)*(m |^ (t*q1))) mod p
= (m |^ (t*q1)) mod p by NEWTON:11;
then ((m |^ (t*q1)) |^ p1) mod p = 1 by A4,A23,Th11;
then (m |^ (t*q1*p1)) mod p = 1 by NEWTON:14;
then (m |^ (t*p1*q1)) mod p = 1 by XCMPLX_1:4;
then (m |^ (t*p1*q1))
= p*((m |^ (t*p1*q1)) div p) + 1 by A6,NAT_1:47;
then a = p*((m |^ (t*p1*q1)) div p) + (1-1) by XCMPLX_1:29;
then p divides a by NAT_1:def 3;
hence thesis by NAT_1:56;
suppose m hcf p <> 1;
then not m,p are_relative_prime by INT_2:def 6;
then m hcf p = p by A1,Th2;
then p divides m by NAT_1:def 5;
hence thesis by NAT_1:56;
end;
hence thesis;
end;
p,q are_relative_prime by A1,INT_2:47;
then (p*q) divides (m*a) by A20,A22,Th4;
then consider k be Nat
such that A24: (m*a) = (p*q)*k by NAT_1:def 3;
m*(m |^ (t*p1*q1) -1 )
= m*(m |^ (t*p1*q1)) - m*1 by XCMPLX_1:40
.= m |^ (t*p1*q1 + 1) - m by NEWTON:11;
then m |^ (t*p1*q1 + 1) - (m - m) = n*k + m by A1,A24,XCMPLX_1:37
;
then m |^ (t*p1*q1 + 1) - 0 = n*k + m by XCMPLX_1:14;
hence thesis by A2,NAT_1:def 2;
end;
hence thesis;
end;
reconsider t = (k1*k2) div Euler(n) as Nat;
k1*k2 = p1*q1*t + 1 by A1,A8,A11,NAT_1:47
.= t*p1*q1 + 1 by XCMPLX_1:4;
then m |^ (k1*k2) mod n = m by A19;
then ((m |^ k1) |^ k2) mod n = m by NEWTON:14;
then ((m |^ k1 mod n) |^ k2) mod n = m by Th12;
then (Crypto(m,n,k1) |^ k2) mod n = m by Def1;
hence thesis by Def1;
end;
hence thesis;
end;
begin :: Order
definition
let i,p;
assume A1:p > 1 & i,p are_relative_prime;
func order(i,p) -> Nat means
:Def2:
it > 0 & (i |^ it) mod p = 1 & for k st k > 0 & (i |^ k) mod p = 1
holds 0 < it & it <= k;
existence
proof
set A = {k where k is Nat:k > 0 & (i |^ k) mod p = 1};
A2:i <> 0
proof
assume i = 0;
then i hcf p = p by NAT_LAT:36;
hence contradiction by A1,INT_2:def 6;
end;
A3:A is non empty set
proof
A4:(i |^ Euler p) mod p = 1 by A1,A2,EULER_2:33;
p <> 0 by A1;
then Euler p <> 0 by Th45;
then Euler p > 0 by NAT_1:19;
then Euler p in A by A4;
hence thesis;
end;
A c= NAT
proof
let a be set;
assume a in A;
then consider k being Nat such that
A5:k = a & k > 0 & (i |^ k) mod p = 1;
thus thesis by A5;
end;
then reconsider A as non empty Subset of NAT by A3;
consider a being Element of A;
defpred P[set] means $1 in A;
a is Nat;
then A6: ex kk being Nat st P[kk];
consider kk being Nat such that
A7: P[kk] and
A8:for n being Nat st P[n] holds kk <= n from Min(A6);
consider k being Nat such that
A9:k = kk & k > 0 & (i |^ k) mod p = 1 by A7;
take kk;
for k st k > 0 & (i |^ k) mod p = 1 holds kk <= k
proof
let k;
assume k > 0 & (i |^ k) mod p = 1;
then k in A;
hence thesis by A8;
end;
hence thesis by A9;
end;
uniqueness
proof
let k1,k2 be Nat such that
A10:k1 > 0 & (i |^ k1) mod p = 1 & for k st k > 0 & (i |^ k) mod p = 1
holds 0 < k1 & k1 <= k and
A11:k2 > 0 & (i |^ k2) mod p = 1 & for k st k > 0 & (i |^ k) mod p = 1
holds 0 < k2 & k2 <= k;
k1 <= k2 & k2 <= k1 by A10,A11;
hence thesis by AXIOMS:21;
end;
end;
theorem
p > 1 implies order(1,p) = 1
proof
assume A1:p > 1;
assume A2:order(1,p) <> 1;
p hcf 1 = 1 by NAT_LAT:35;
then A3:1,p are_relative_prime by INT_2:def 6;
(1 |^ 1) mod p = 1 mod p by NEWTON:10
.= 1 by A1,GR_CY_1:4;
then order(1,p) <= 1 by A1,A3,Def2;
then order(1,p) < 1 or order(1,p) = 1 by AXIOMS:21;
then order(1,p) = 0 or order(1,p) = 1 by RLVECT_1:98;
hence contradiction by A1,A2,A3,Def2;
end;
canceled;
theorem Th52:
p > 1 & n > 0 & (i |^ n) mod p = 1 & i,p are_relative_prime
implies order(i,p) divides n
proof
assume A1:p > 1 & n > 0 & (i |^ n) mod p = 1 & i,p are_relative_prime;
then A2:(i |^ order(i,p)) mod p = 1 by Def2;
A3:order(i,p) <> 0 by A1,Def2;
n mod order(i,p) = 0
proof
assume A4:n mod order(i,p) <> 0;
set I = n mod order(i,p);
consider t being Nat such that
A5:n = order(i,p)*t + I & I < order(i,p) by A3,NAT_1:def 2;
(i |^ (order(i,p)*t))*(i |^ I) mod p = 1 by A1,A5,NEWTON:13;
then ((i |^ order(i,p)) |^ t)*(i |^ I) mod p = 1 by NEWTON:14;
then ((((i |^ order(i,p)) |^ t) mod p)*(i |^ I)) mod p = 1 by EULER_2:10;
then A6:(1*(i |^ I)) mod p = 1 by A1,A2,Th36;
I > 0 by A4,NAT_1:19;
hence contradiction by A1,A5,A6,Def2;
end;
hence thesis by A3,Th6;
end;
theorem Th53:
p > 1 & i,p are_relative_prime & order(i,p) divides n implies
(i |^ n) mod p = 1
proof
assume A1:p > 1 & i,p are_relative_prime & order(i,p) divides n;
then consider t being Nat such that
A2:n = order(i,p)*t by NAT_1:def 3;
(i |^ n) mod p = ((i |^ order(i,p)) |^ t) mod p by A2,NEWTON:14
.= (((i |^ order(i,p)) mod p) |^ t ) mod p by Th12
.= ((1) |^ t) mod p by A1,Def2
.= 1 mod p by NEWTON:15
.= 1 by A1,GR_CY_1:4;
hence thesis;
end;
theorem Th54:
p is prime & i,p are_relative_prime implies order(i,p) divides (p -'1)
proof
assume A1:p is prime & i,p are_relative_prime;
then A2:(i |^ (p -'1)) mod p = 1 by Th38;
A3:p > 1 by A1,INT_2:def 5;
then p - 1 > 1 - 1 by REAL_1:54;
then p -'1 > 0 by BINARITH:def 3;
hence thesis by A1,A2,A3,Th52;
end;
begin :: Fermat Number
definition
let n be Nat;
func Fermat(n) -> Nat equals
:Def3:
2 |^ (2 |^ n) + 1;
correctness;
end;
theorem Th55:
Fermat(0) = 3
proof
Fermat(0) = 2 |^ (2 |^ 0) + 1 by Def3
.= 2 |^ 1 + 1 by NEWTON:9
.= 2 + 1 by NEWTON:10;
hence thesis;
end;
theorem Th56:
Fermat(1) = 5
proof
Fermat(1) = 2 |^ (2 |^ 1) + 1 by Def3
.= 2 |^ (1 + 1) + 1 by NEWTON:10
.= 2 |^ 1 * 2 + 1 by NEWTON:11
.= 2 * 2 + 1 by NEWTON:10;
hence thesis;
end;
theorem Th57:
Fermat(2) = 17
proof
thus Fermat(2) = 2 |^ (2 |^ (1 + 1)) + 1 by Def3
.= 2 |^ (2 |^ 1 * 2) + 1 by NEWTON:11
.= 2 |^ (2 * 2) + 1 by NEWTON:10
.= 2 |^ (3 + 1) + 1
.= 2 |^ (2 + 1) * 2 + 1 by NEWTON:11
.= 2 |^ (1 + 1) * 2 * 2 + 1 by NEWTON:11
.= 2 |^ 1 * 2 * 2 * 2 + 1 by NEWTON:11
.= 2 * 2 * 2 * 2 + 1 by NEWTON:10
.= 17;
end;
theorem Th58:
Fermat(3) = 257
proof
thus Fermat(3) = 2 |^ (4 + 4) + 1 by Def3,Lm12
.= 2 |^ 4 * 2 |^ 4 + 1 by NEWTON:13
.= 257 by Lm13;
end;
theorem Th59:
Fermat(4) = 256*256+1
proof
thus Fermat(4) = 2 |^ (8 + 8) + 1 by Def3,Lm13
.= 2 |^ 8 * 2 |^ 8 + 1 by NEWTON:13
.= (2 |^ 4 * 2 |^ 4)*2 |^ (4 + 4) + 1 by NEWTON:13
.= 256*256+1 by Lm13,NEWTON:13;
end;
theorem Th60:
Fermat(n) > 2
proof
set 2N = 2 |^ (2 |^ n);
2N > 1 by Lm4;
then 2N + 1 > 1 + 1 by REAL_1:53;
hence thesis by Def3;
end;
Lm20:
Fermat(n) > 1
proof
Fermat(n) <> 1 by Th60;
then Fermat(n) > 1 or Fermat(n) < 1 by AXIOMS:21;
then Fermat(n) > 1 or Fermat(n) = 0 by RLVECT_1:98;
hence thesis by Th60;
end;
Lm21:
(Fermat(n) -'1) mod 2 = 0
proof
A1:Fermat(n) -'1 = 2 |^ (2 |^ n) + 1 -'1 by Def3
.= 2 |^ (2 |^ n) by BINARITH:39;
2 mod 2 = 0 by GR_CY_1:5;
then A2:2 is even by NAT_2:23;
2 |^ n > 0 by PREPOWER:13;
then (Fermat(n) -'1) is even by A1,A2,Th21;
hence thesis by NAT_2:23;
end;
Lm22:
Fermat(n)-'1 > 0
proof
Fermat(n) > 1 by Lm20;
then Fermat(n) - 1 > 1 - 1 by REAL_1:54;
hence thesis by BINARITH:def 3;
end;
Lm23:
Fermat(n) mod (2 |^ (2 |^ n)) = 1
proof
set 2N = 2 |^ (2 |^ n);
A1:2N > 1 by Lm4;
Fermat(n) mod 2N = (2N*1 + 1) mod 2N by Def3
.= 1 mod 2N by GR_CY_1:1
.= 1 by A1,GROUP_4:102;
hence thesis;
end;
Lm24:
Fermat(n) is odd
proof
A1:Fermat(n) = Fermat(n) + (1 - 1)
.= Fermat(n) + 1 - 1 by XCMPLX_1:29
.= Fermat(n) - 1 + 1 by XCMPLX_1:29;
Fermat(n) > 1 by Lm20;
then Fermat(n) - 1 > 1 - 1 by REAL_1:54;
then A2:Fermat(n) - 1 = Fermat(n) -'1 by BINARITH:def 3;
(Fermat(n) -'1) mod 2 = 0 by Lm21;
then (Fermat(n) -'1) is even by NAT_2:23;
hence thesis by A1,A2,Th16;
end;
theorem Th61:
p is prime & p > 2 & p divides Fermat(n) implies
ex k being Nat st p = k*(2 |^ (n + 1)) + 1
proof
assume A1:p is prime & p > 2 & p divides Fermat(n);
set 2N = 2 |^ (2 |^ n);
A2:p > 1 by A1,INT_2:def 5;
set t = Fermat(n) div p;
Fermat(n) = 2N + 1 by Def3;
then A3:p*t = 2N + 1 by A1,NAT_1:49;
2 |^ n > 0 by PREPOWER:13;
then A4:2N > 1 by Th26;
2N > 0 by PREPOWER:13;
then (2N)*(2N) > 1*(2N) by A4,REAL_1:70;
then (2N)^2 > (2N) by SQUARE_1:def 3;
then A5:(2N)^2 > 1 by A4,AXIOMS:22;
A6:(-1),(-1) are_congruent_mod p by INT_1:32;
p*t - 0 = p*t;
then p*t,0 are_congruent_mod p by INT_1:def 3;
then (p*t + (-1)),(0 + (-1)) are_congruent_mod p by A6,INT_1:37;
then A7:(2N),(-1) are_congruent_mod p by A3,XCMPLX_1:137;
then (2N)^2,(-1)^2 are_congruent_mod p by Th41;
then (2N)^2,1 are_congruent_mod p by SQUARE_1:59,61;
then (2N)^2 mod p = 1 by A2,A5,Lm19;
then A8:(2 |^ (2 |^ (n + 1))) mod p = 1 by Lm16;
A9:2N mod p <> 1
proof
assume 2N mod p = 1;
then 2N,1 are_congruent_mod p by A2,Th40;
then 1,2N are_congruent_mod p by INT_1:35;
then 1,(-1) are_congruent_mod p by A7,INT_1:36;
then p divides (1 - -1) by INT_2:19;
then p divides 2 by Lm1;
hence contradiction by A1,NAT_1:54;
end;
A10:2,p are_relative_prime by A1,INT_2:44,47;
2 |^ (n + 1) > 0 by PREPOWER:13;
then A11:order(2,p) divides (2 |^ (n + 1)) by A2,A8,A10,Th52;
order(2,p) <> 0 by A2,A10,Def2;
then order(2,p) >= 1 by RLVECT_1:99;
then A12:order(2,p) = 1 or order(2,p) > 1 by AXIOMS:21;
2 |^ (n + 1) div 2 = 2*(2 |^ n) div 2 by NEWTON:11
.= 2 |^ n by GROUP_4:107;
then not order(2,p) divides (2 |^ (n + 1)) div 2 by A2,A9,A10,Th53;
then order(2,p) = 2 |^ (n + 1)
by A11,A12,Th39,INT_2:44,NAT_1:53;
then (2 |^ (n + 1)) divides (p -'1) by A1,A10,Th54;
then consider t2 being Nat such that
A13:(p -'1) = (2 |^ (n + 1))*t2 by NAT_1:def 3;
p - 1 > 1 - 1 by A2,REAL_1:54;
then p - 1 = (2 |^ (n + 1))*t2 by A13,BINARITH:def 3;
then p = t2*(2 |^ (n + 1)) + 1 by XCMPLX_1:27;
hence thesis;
end;
theorem Th62:
n <> 0 implies 3,Fermat(n) are_relative_prime
proof
assume A1: n <> 0;
A2:Fermat(n),3 are_relative_prime or Fermat(n) hcf 3 = 3 by Th2,Th44;
Fermat(n) hcf 3 <> 3
proof
assume Fermat(n) hcf 3 = 3;
then 3 divides Fermat(n) by NAT_1:def 5;
then consider k being Nat such that
A3:3 = k*(2 |^ (n+1)) + 1 by Th44,Th61;
2 + 1 - 1 = k*(2 |^ (n+1)) + 1 - 1 by A3;
then 2 div 2 = k*(2 |^ (n+1)) div 2 by XCMPLX_1:26;
then 1 = k*(2 |^ (n+1)) div 2 by NAT_2:5;
then 1 = k*(2 |^ n) by Lm9;
then k = 1 & 2 |^ n = 1 by NAT_1:40;
then 2 |^ n = 2 |^ 0 by NEWTON:9;
hence contradiction by A1,Th31;
end;
hence thesis by A2,Lm7;
end;
begin :: Pepin's Test
theorem Th63:
(3 |^ ((Fermat(n)-'1) div 2)),(-1) are_congruent_mod Fermat(n)
implies Fermat(n) is prime
proof
per cases by NAT_1:19;
suppose n = 0;
hence thesis by Th44,Th55;
suppose A1:n > 0;
assume
A2: (3 |^ ((Fermat(n)-'1) div 2)),(-1) are_congruent_mod Fermat(n);
assume A3:not Fermat(n) is prime;
Fermat(n) > 2 by Th60;
then consider p being Nat such that
A4:p is prime and
A5:p divides Fermat(n) by INT_2:48;
consider i being Nat such that
A6:Fermat(n) = p*i by A5,NAT_1:def 3;
A7:(3 |^ ((Fermat(n)-'1) div 2)),(-1) are_congruent_mod p by A2,A6,INT_1:41;
p <> 3
proof
assume A8:p = 3;
1 hcf i = 1 by NAT_LAT:35;
then 3*1 hcf 3*i = 3 by EULER_1:6;
then not 3,Fermat(n) are_relative_prime by A6,A8,INT_2:def 6;
hence contradiction by A1,Th62;
end;
then A9:3,p are_relative_prime by A4,Th44,INT_2:47;
A10:Fermat(n)-'1 > 0 by Lm22;
then A11:3 |^ (Fermat(n)-'1) > 1 by Th26;
A12:1 < p by A4,INT_2:def 5;
A13:(Fermat(n) -'1) mod 2 = 0 by Lm21;
A14:p > 2
proof
assume p <= 2;
then p = 2 or p < 1 + 1 by AXIOMS:21;
then A15:p = 2 or p <= 1 by NAT_1:38;
Fermat(n) is odd by Lm24;
then A16:Fermat(n) mod p = 1 by A4,A15,INT_2:def 5,NAT_2:24;
p <> 0 by A4,INT_2:def 5;
hence contradiction by A5,A16,Th6;
end;
(3 |^ ((Fermat(n)-'1) div 2))^2,(-1)^2 are_congruent_mod Fermat(n)
by A2,Th41;
then (3 |^ (Fermat(n)-'1)),(-1)^2 are_congruent_mod Fermat(n)
by A13,Th28;
then (3 |^ (Fermat(n)-'1)),1 are_congruent_mod Fermat(n)
by SQUARE_1:59,61;
then (3 |^ (Fermat(n)-'1)),1 are_congruent_mod p by A6,INT_1:41;
then A17:(3 |^ (Fermat(n)-'1)) mod p = 1 by A11,A12,Lm19;
set d = order(3,p);
A18:d divides (Fermat(n)-'1) by A9,A10,A12,A17,Th52;
A19:d divides (p-'1) by A4,A9,Th54;
A20:d <> 0 by A9,A12,Def2;
A21: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 A9,A12,Th53;
then (3 |^ ((Fermat(n) -'1) div 2)),1 are_congruent_mod p by A12,Th40;
then 1,-1 are_congruent_mod p by A7,Th43;
then p divides (1 - -1) by INT_2:19;
then p divides 2 by Lm1;
hence contradiction by A14,NAT_1:54;
end;
set 2N = 2 |^ (2 |^ n);
A22:2N > 1 by Lm4;
A23:2N <> 0 by Lm4;
Fermat(n) = 2N + 1 by Def3;
then A24:Fermat(n) - 1 = 2N + (1 - 1) by XCMPLX_1:29
.= 2N + 0;
then A25:Fermat(n) - 1 >= 0 by NAT_1:19;
then A26:d divides 2N by A18,A24,BINARITH:def 3;
A27:not d divides (2N div 2) by A21,A24,A25,BINARITH:def 3;
d > 1
proof
assume A28:d <= 1;
now per cases by A28,AXIOMS:21;
suppose d < 1;
hence thesis by A20,RLVECT_1:98;
suppose d = 1;
hence thesis by A21,NAT_1:53;
end;
hence thesis;
end;
then d = 2N by A26,A27,Th39,INT_2:44
.= Fermat(n) -'1 by A24,A25,BINARITH:def 3;
then A29:d = 2N by A24,A25,BINARITH:def 3;
consider x being Nat such that
A30:p -'1 = d*x by A19,NAT_1:def 3;
p - 1 > 1 - 1 by A12,REAL_1:54;
then A31:p - 1 = x*d by A30,BINARITH:def 3;
then A32:p = x*2N + 1 by A29,XCMPLX_1:27;
then A33:p mod 2N = 1 mod 2N by GR_CY_1:1
.= 1 by A22,GR_CY_1:4;
A34:x >= 1
proof
assume x < 1;
then p = 0*2N + 1 by A32,RLVECT_1:98;
hence contradiction by A4,INT_2:def 5;
end;
p*i mod 2N = 1 by A6,Lm23;
then (1*i) mod 2N = 1 by A33,EULER_2:10;
then consider y being Nat such that
A35:i = 2N*y + 1 & 1 < 2N by NAT_1:def 2;
A36:y >= 0 by NAT_1:18;
Fermat(n) = (x*2N + 1)*(y*2N + 1) by A6,A29,A31,A35,XCMPLX_1:27
.= (x*2N)*(y*2N) + (x*2N)*1 + 1*(y*2N) + 1*1 by XCMPLX_1:10
.= (x*2N*y*2N) + x*2N + y*2N + 1 by XCMPLX_1:4
.= 2N*(x*y*2N) + 2N*x + 2N*y + 1 by XCMPLX_1:4
.= 2N*(x*y*2N) + (2N*x + 2N*y) + 1 by XCMPLX_1:1
.= 2N*(x*y*2N) + 2N*(x + y) + 1 by XCMPLX_1:8
.= 2N*((x*y*2N) + (x + y)) + 1 by XCMPLX_1:8
.= 2N*(x*y*2N + x + y) + 1 by XCMPLX_1:1;
then 2N + 1 - 1 = 2N*(x*y*2N + x + y) + 1 - 1 by Def3;
then 2N + (1 - 1) = 2N*(x*y*2N + x + y) + 1 - 1 by XCMPLX_1:29;
then 2N = 2N*(x*y*2N + x + y) + 0 by XCMPLX_1:29;
then 1 = 2N*(x*y*2N + x + y) div 2N by A23,Th48
.= (x*y*2N + x + y) by A23,GROUP_4:107;
then p = 1*2N + 1 by A22,A32,A34,A36,Lm3
.= Fermat(n) by Def3;
hence contradiction by A3,A4;
end;
:: LEMMA ::
Lm25:
3 |^ 2 = 9
proof
3 |^ 2 = 3 |^ (1+1)
.= (3 |^ 1)*(3 |^ 1) by NEWTON:13
.= 3*(3 |^ 1) by NEWTON:10
.= 3*3 by NEWTON:10;
hence thesis;
end;
Lm26:
3 |^ 4 = 81
proof
3 |^ 4 = 3 |^ (2+2)
.= (3 |^ 2)* (3 |^ 2) by NEWTON:13;
hence thesis by Lm25;
end;
Lm27:
3 |^ 8 = 6561
proof
3 |^ 8 = 3 |^ (4+4)
.= (3 |^ 4)* (3 |^ 4) by NEWTON:13;
hence thesis by Lm26;
end;
Lm28:
3 |^ 16 = 6561*6561
proof
3 |^ 16 = 3 |^ (8+8)
.= (3 |^ 8)* (3 |^ 8) by NEWTON:13;
hence thesis by Lm27;
end;
Lm29:
for i being Nat holds Fermat(1) divides (3 |^ (4*i + 2)) + 1
proof
let i;
defpred P[Nat] means Fermat(1) divides (3 |^ (4*$1 + 2)) + 1;
A1: P[0]
proof
10 = 5 * 2;
hence thesis by Lm25,Th56,NAT_1:def 3;
end;
A2: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
A3:(3 |^ (4*n + 2)) + 1 = Fermat(1)*m by NAT_1:def 3;
A4:3 |^ (4*n + 2) = Fermat(1)*m - 1 by A3,XCMPLX_1:26;
A5:(m*81)-16 > 0
proof
4*n>=0 by NAT_1:18;
then 3 |^ (4*n) >= 3 |^ 0 by PCOMPS_2:4;
then 3 |^ (4*n) >= 1 by NEWTON:9;
then 3 |^ (4*n) + 1 > 0 + 1 by NAT_1:38;
then 3 |^ (4*n) > 0 by AXIOMS:24;
then (3 |^ (4*n)) * 3 |^ 2 > 0 * 3 |^ 2 by Lm25,REAL_1:70;
then (3 |^ (4*n + 2)) > 0 by NEWTON:13;
then (3 |^ (4*n + 2)) + 1 > 0 + 1 by REAL_1:53;
then Fermat(1)*m*81 > 1*81 by A3,REAL_1:70;
then Fermat(1)*m*81/Fermat(1) > 1*81/Fermat(1) by Th56,REAL_1:73;
then m*Fermat(1)*81*Fermat(1)" > 1*81/Fermat(1) by XCMPLX_0:def 9;
then m*81*Fermat(1)*Fermat(1)" > 1*81/Fermat(1) by XCMPLX_1:4;
then m*81*Fermat(1)"*Fermat(1) > 1*81/Fermat(1) by XCMPLX_1:4;
then m*81/Fermat(1)*Fermat(1) > 1*81/Fermat(1) by XCMPLX_0:def 9;
then m*81 > 81/5 by Th56,XCMPLX_1:88;
then m*81 > 16 by AXIOMS:22;
then m*81 + (- 16) > 16 + (- 16) by REAL_1:53;
hence thesis by XCMPLX_0:def 8;
end;
(3 |^ (4*(n+1) + 2)) + 1
= (3 |^ (4*n + 4*1 + 2)) + 1 by XCMPLX_1:8
.= (3 |^ (4*n + 2 + 4)) + 1 by XCMPLX_1:1
.= ((Fermat(1)*m -1)*(3 |^ 4)) + 1 by A4,NEWTON:13
.= ((Fermat(1)*m)*(3 |^ 4) - (3 |^ 4)*1) + 1 by XCMPLX_1:40
.= (Fermat(1)*m)*81 - (81 - 1) by Lm26,XCMPLX_1:37
.= Fermat(1)*(m*81) - Fermat(1)*16 by Th56,XCMPLX_1:4
.= Fermat(1)*(m*81) + - Fermat(1)*16 by XCMPLX_0:def 8
.= Fermat(1)*(m*81) + Fermat(1)*(-16) by XCMPLX_1:175
.= Fermat(1)*((m*81)+ -16) by XCMPLX_1:8
.= Fermat(1)*((m*81)-16) by XCMPLX_0:def 8
.= Fermat(1)*((m*81)-'16) by A5,BINARITH:def 3;
hence thesis by NAT_1:def 3;
end;
for n holds P[n] from Ind(A1,A2);
hence thesis;
end;
Lm30:
n = 1 implies
(3 |^ ((Fermat(n)-'1) div 2)),(-1) are_congruent_mod Fermat(n)
proof
assume A1:n = 1;
A2:(3 |^ ((Fermat(n)-'1) div 2)) + 1
= (3 |^ ((Fermat(n)-'1) div 2)) - - 1 by XCMPLX_1:151;
A3:5 -'1 = 5 - 1 by BINARITH:def 3
.= 4 + 0;
A4:2 to_power 1 = 2 |^ 1 by POWER:46
.= 2 by NEWTON:10;
A5:2 -'1 = 2 - 1 by BINARITH:def 3
.= 1 + 0;
2 to_power 2 = 2 |^ (1+1) by POWER:46
.= 2 |^ 1*2 by NEWTON:11
.= 2*2 by NEWTON:10;
then 4 div 2 = (2 to_power (2-'1)) by A4,NAT_2:18
.= 2 |^ 1 by A5,POWER:46
.= 2 by NEWTON:10;
then (Fermat(1) -'1) div 2 = 4*0 + 2 by A3,Th56;
then Fermat(1) divides (3 |^ ((Fermat(n)-'1) div 2)) + 1 by A1,Lm29;
then Fermat(1) divides ((3 |^ ((Fermat(n)-'1) div 2 )) - (-1)) by A2,Lm1;
hence thesis by A1,INT_2:19;
end;
Lm31:
-(Fermat(2)*386)*6560 = Fermat(2)*(-386*6560)
proof
Fermat(2)*(-386*6560) = -386*6560*17 by Th57,XCMPLX_1:175;
hence thesis by Th57,XCMPLX_1:4;
end;
Lm32:
6561*6561 - 1 = (6561+1)*(6561-1)
proof
(6561+1)*(6561-1) = 6561*6561-6561*1+1*6561-1*1 by XCMPLX_1:45
.= 6561*6561+ -6561+6561 -1 by XCMPLX_0:def 8
.= 6561*6561+(-6561+6561) -1 by XCMPLX_1:1
.= 6561*6561 - 1;
hence thesis;
end;
Lm33:
for n being Nat holds Fermat(2) divides (3 |^ (16*n + 8)) + 1
proof
let n;
defpred P[Nat] means Fermat(2) divides (3 |^ (16*$1 + 8)) + 1;
A1: P[0]
proof
6562 = 17 * 386;
hence thesis by Lm27,Th57,NAT_1:def 3;
end;
A2: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
A3:(3 |^ (16*n + 8)) + 1 = Fermat(2)*m by NAT_1:def 3;
A4:3 |^ (16*n + 8) = Fermat(2)*m - 1 by A3,XCMPLX_1:26;
A5:m*6561*6561-386*6560 > 0
proof
16*n>=0 by NAT_1:18;
then 3 |^ (16*n) >= 3 |^ 0 by PCOMPS_2:4;
then 3 |^ (16*n) >= 1 by NEWTON:9;
then 3 |^ (16*n) + 1 > 0 + 1 by NAT_1:38;
then 3 |^ (16*n) > 0 by AXIOMS:24;
then (3 |^ (16*n)) * 3 |^ 8 > 0 * 3 |^ 8 by Lm27,REAL_1:70;
then (3 |^ (16*n + 8)) > 0 by NEWTON:13;
then (3 |^ (16*n + 8)) + 1 > 0 + 1 by REAL_1:53;
then Fermat(2)*m*6561 > 1*6561 by A3,REAL_1:70;
then Fermat(2)*m*6561*6561 > 6561*6561 by REAL_1:70;
then Fermat(2)*m*6561*6561 > 6562*6560 by AXIOMS:22;
then Fermat(2)*m*6561*6561/Fermat(2)
> 6560*6562/Fermat(2) by Th57,REAL_1:73;
then m*Fermat(2)*6561*6561*Fermat(2)"
> 6560*6562/Fermat(2) by XCMPLX_0:def 9;
then m*6561*Fermat(2)*6561*Fermat(2)"
> 6560*6562/Fermat(2) by XCMPLX_1:4;
then m*6561*6561*Fermat(2)*Fermat(2)"
> 6560*6562/Fermat(2) by XCMPLX_1:4;
then m*6561*6561*Fermat(2)"*Fermat(2)
> 6560*6562/Fermat(2) by XCMPLX_1:4;
then m*6561*6561/Fermat(2)*Fermat(2)
> 6560*6562/Fermat(2) by XCMPLX_0:def 9;
then A6:m*6561*6561 > 6560*6562/17 by Th57,XCMPLX_1:88;
6560*386 = 6560*(6562*17")
.= 6560*6562*17" by XCMPLX_1:4
.= 6560*6562/17 by XCMPLX_0:def 9;
then m*6561*6561-386*6560 > 386*6560-386*6560 by A6,REAL_1:54;
then m*6561*6561-386*6560 > 386*6560+(-386*6560) by XCMPLX_0:def 8;
hence thesis by XCMPLX_0:def 6;
end;
(3 |^ (16*(n+1) + 8)) + 1 = (3 |^ (16*n + 16*1 + 8)) + 1 by XCMPLX_1:8
.= (3 |^ (16*n + 8 + 16)) + 1 by XCMPLX_1:1
.= ((Fermat(2)*m -1)*(3 |^ 16)) + 1 by A4,NEWTON:13
.= ((Fermat(2)*m)*(3 |^ 16) - (3 |^ 16)*1) + 1 by XCMPLX_1:40
.= (Fermat(2)*m)*(6561*6561) - (6561*6561 - 1) by Lm28,XCMPLX_1:37
.= Fermat(2)*m*6561*6561 - (6561*6561 - 1) by XCMPLX_1:4
.= Fermat(2)*(m*6561)*6561 - (6561*6561 - 1) by XCMPLX_1:4
.= Fermat(2)*(m*6561*6561) - (6561+1)*(6561 - 1)
by Lm32,XCMPLX_1:4
.= Fermat(2)*(m*6561*6561) + -Fermat(2)*386*6560
by Th57,XCMPLX_0:def 8
.= Fermat(2)*(m*6561*6561 + (-386*6560)) by Lm31,XCMPLX_1:8
.= Fermat(2)*((m*6561*6561)-386*6560) by XCMPLX_0:def 8
.= Fermat(2)*((m*6561*6561)-'386*6560) by A5,BINARITH:def 3;
hence thesis by NAT_1:def 3;
end;
for n holds P[n] from Ind(A1,A2);
hence thesis;
end;
Lm34:
3 |^ 1 mod Fermat(3) = 3
proof
A1:3 = 0*257 + 3;
thus 3 |^ 1 mod Fermat(3) = 3 mod Fermat(3) by NEWTON:10
.= 3 by A1,Th58,NAT_1:def 2;
end;
Lm35:
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:13
.= (((3 |^ 1) mod Fermat(3))*((3 |^ 1) mod Fermat(3)))
mod Fermat(3) by EULER_2:11
.= 9 by A1,Lm34,Th58,NAT_1:def 2;
end;
Lm36:
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:13
.= (((3 |^ 2) mod Fermat(3))*((3 |^ 2) mod Fermat(3)))
mod Fermat(3) by EULER_2:11
.= 81 by A1,Lm35,Th58,NAT_1:def 2;
end;
Lm37:
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:13
.= (((3 |^ 4) mod Fermat(3))*((3 |^ 4) mod Fermat(3)))
mod Fermat(3) by EULER_2:11
.= 136 by A1,Lm36,Th58,NAT_1:def 2;
end;
Lm38:
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:13
.= (136*136) mod Fermat(3) by Lm37,EULER_2:11
.= 83*3 by A1,Th58,NAT_1:def 2;
end;
Lm39:
3 |^ 32 mod Fermat(3) = 64
proof
A1:83*3*83*3 = 241*257 + 64
proof
A2:64 = 9*7 + 1;
241*257 = (240+1)*257
.= 240*257 + 1*257 by XCMPLX_1:8
.= 240*257 + (240 + 17)
.= 240*257 + 240*1 + 17 by XCMPLX_1:1
.= 240*(257+1) + 17 by XCMPLX_1:8
.= 9*80*86 + 17;
then 241*257 + 64 = 9*80*86 + 17 + 9*7 + 1 by A2,XCMPLX_1:1
.= 9*80*86 + 9*7 + 17 + 1 by XCMPLX_1:1
.= 9*80*86 + 9*7 + (17 + 1) by XCMPLX_1:1
.= 9*(80*86) + 9*7 + 9*2
.= 9*(80*86 + 7) + 9*2 by XCMPLX_1:8
.= 9*(80*86 + 7 + 2) by XCMPLX_1:8
.= 83*3*3*83;
hence thesis;
end;
3 |^ 32 mod Fermat(3) = (3 |^ (16+16)) mod Fermat(3)
.= (3 |^ 16*3 |^ 16) mod Fermat(3) by NEWTON:13
.= (83*3*(83*3)) mod Fermat(3) by Lm38,EULER_2:11
.= 64 by A1,Th58,NAT_1:def 2;
hence thesis;
end;
Lm40:
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:13
.= (64*64) mod Fermat(3) by Lm39,EULER_2:11
.= 241 by A1,Th58,NAT_1:def 2;
end;
Lm41:
3 |^ 128 mod Fermat(3) = 256
proof
A1:241*241 = 225*257 + 256
proof
225*257 + 256 = 225*(241+16) + 256
.= 225*241 + 225*16 + 256 by XCMPLX_1:8
.= 225*241 + (3600 + 256) by XCMPLX_1:1
.= 225*241 + 16*241
.= (225+16)*241 by XCMPLX_1:8;
hence thesis;
end;
thus 3 |^ 128 mod Fermat(3) = (3 |^ (64+64)) mod Fermat(3)
.= (3 |^ 64*3 |^ 64) mod Fermat(3) by NEWTON:13
.= (241*241) mod Fermat(3) by Lm40,EULER_2:11
.= 256 by A1,Th58,NAT_1:def 2;
end;
Lm42:
Fermat(4) <> 0 by Th59,REAL_1:69;
Lm43:
3 |^ 1 mod Fermat(4) = 3
proof
A1:3 = 0*(256*256+1) + 3;
A2:3 < 256*256+1
proof
256*256 < 256*256 + 1 by REAL_1:69;
hence thesis by AXIOMS:22;
end;
thus 3 |^ 1 mod Fermat(4) = 3 mod Fermat(4) by NEWTON:10
.= 3 by A1,A2,Th59,NAT_1:def 2;
end;
Lm44:
3 |^ 2 mod Fermat(4) = 9
proof
A1:9 = 0*(256*256+1) + 9;
A2:9 < 256*256 + 1
proof
256*256 < 256*256 + 1 by REAL_1:69;
hence thesis by AXIOMS:22;
end;
thus 3 |^ 2 mod Fermat(4) = (3 |^ (1+1)) mod Fermat(4)
.= (3 |^ 1*3 |^ 1) mod Fermat(4) by NEWTON:13
.= (3*3) mod Fermat(4) by Lm43,EULER_2:11
.= 9 by A1,A2,Th59,NAT_1:def 2;
end;
Lm45:
3 |^ 4 mod Fermat(4) = 81
proof
A1:81 = 0*(256*256+1) + 81;
A2:81 < 256*256 + 1
proof
256*256 < 256*256 + 1 by REAL_1:69;
hence thesis by AXIOMS:22;
end;
thus 3 |^ 4 mod Fermat(4) = (3 |^ (2+2)) mod Fermat(4)
.= (3 |^ 2*3 |^ 2) mod Fermat(4) by NEWTON:13
.= (9*9) mod Fermat(4) by Lm44,EULER_2:11
.= 81 by A1,A2,Th59,NAT_1:def 2;
end;
Lm46:
3 |^ 8 mod Fermat(4) = 6561
proof
A1:6561 = 0*(256*256+1) + 6561;
A2:6561 < 256*256 + 1
proof
256*256 < 256*256 + 1 by REAL_1:69;
hence thesis by AXIOMS:22;
end;
thus 3 |^ 8 mod Fermat(4) = (3 |^ (4+4)) mod Fermat(4)
.= (3 |^ 4*3 |^ 4) mod Fermat(4) by NEWTON:13
.= (81*81) mod Fermat(4) by Lm45,EULER_2:11
.= 6561 by A1,A2,Th59,NAT_1:def 2;
end;
Lm47:
3 |^ 16 mod Fermat(4) = 164*332+1
proof
A1:6561*6561 = 656*(256*256+1) + (164*332+1)
proof
6561*6561 = (6560+1)*6561
.= 6560*6561+1*6561 by XCMPLX_1:8
.= 656*10*(4096+2465)+6561
.= 656*10*(256*16)+656*10*2465+6561 by XCMPLX_1:8
.= 656*10*256*16+656*10*2465+6561 by XCMPLX_1:4
.= 656*256*10*16+656*10*2465+6561 by XCMPLX_1:4
.= 656*256*(10*16)+656*10*2465+6561 by XCMPLX_1:4
.= 656*(24576+74)+656*256*160+6561
.= 656*(256*96)+656*74+656*256*160+6561 by XCMPLX_1:8
.= 656*256*96+656*74+656*256*160+6561 by XCMPLX_1:4
.= 656*256*96+656*256*160+656*74+6561 by XCMPLX_1:1
.= 656*256*(96+160)+656*74+6561 by XCMPLX_1:8
.= 656*(1+73)+656*256*256+6561
.= 656*1+656*73+656*256*256+6561 by XCMPLX_1:8
.= 656*1+656*256*256+656*73+6561 by XCMPLX_1:1
.= 656*1+656*(256*256)+656*73+6561 by XCMPLX_1:4
.= 656*(256*256+1)+164*292+(6560+1) by XCMPLX_1:8
.= 656*(256*256+1)+164*292+164*40+1 by XCMPLX_1:1
.= 656*(256*256+1)+(164*292+164*40)+1 by XCMPLX_1:1
.= 656*(256*256+1)+(164*(292+40))+1 by XCMPLX_1:8
.= 656*(256*256+1)+164*332+1;
hence thesis by XCMPLX_1:1;
end;
A2:164*332+1 < 256*256 + 1 by REAL_1:53;
3 |^ 16 mod Fermat(4) = (3 |^ (8+8)) mod Fermat(4)
.= (3 |^ 8*3 |^ 8) mod Fermat(4) by NEWTON:13
.= (6561*6561) mod Fermat(4) by Lm46,EULER_2:11
.= 164*332+1 by A1,A2,Th59,NAT_1:def 2;
hence thesis;
end;
Lm48:
164*332+1 = 212*256+177
proof
164*332+1 = 164*(76+256)+1
.= 164*76+164*256+1 by XCMPLX_1:8
.= 164*48+4592+1+164*256 by XCMPLX_1:1
.= 48*(92+164)+177+164*256
.= 48*256+164*256+177 by XCMPLX_1:1
.= 256*(48+164)+177 by XCMPLX_1:8;
hence thesis;
end;
Lm49:
3 |^ 32 mod Fermat(4) = 123*503
proof
A1:(164*332+1)*(164*332+1) = 263*172*(256*256+1) + 123*503
proof
A2:212*256*177+212*256*177 = 292*256*256+512*148
proof
212*256*177+212*256*177 = 212*256*(177+177) by XCMPLX_1:8
.= 212*256*(292+62)
.= 212*256*292+(212*256)*62 by XCMPLX_1:8
.= 212*256*292+256*(212*62) by XCMPLX_1:4
.= 212*256*292+(256*((292*44)+296))
.= 212*256*292+(256*(292*44)+256*296) by XCMPLX_1:8
.= 212*256*292+(256*292*44+256*296) by XCMPLX_1:4
.= 212*256*292+256*292*44+256*296 by XCMPLX_1:1
.= 212*(256*292)+256*292*44+256*296 by XCMPLX_1:4
.= (256*292)*(212+44)+256*296 by XCMPLX_1:8
.= 292*256*256+256*2*148;
hence thesis;
end;
A3:(212*256)*(212*256)+292*256*256 = 263*172*256*256
proof
(212*256)*(212*256)+292*256*256
= 256*212*256*212+292*256*256 by XCMPLX_1:4
.= 256*256*212*212+(292*256*256) by XCMPLX_1:4
.= 256*256*212*212+(256*256*292) by XCMPLX_1:4
.= 256*256*(212*212)+256*256*292 by XCMPLX_1:4
.= 256*256*(212*(172+40)+292) by XCMPLX_1:8
.= 256*256*(212*172+212*40+292) by XCMPLX_1:8
.= 256*256*(212*172+(8480+292)) by XCMPLX_1:1
.= 256*256*(172*212+172*51)
.= 256*256*(172*(212+51)) by XCMPLX_1:8
.= (172*263)*256*256 by XCMPLX_1:4;
hence thesis;
end;
A4:512*148+177*177 = 263*172+123*503
proof
512*148+177*177 = 512*(123+25)+177*177
.= 123*(503+9)+512*25+177*177 by XCMPLX_1:8
.= 123*503+123*9+512*25+177*177 by XCMPLX_1:8
.= 123*503+(1107+12800)+177*177 by XCMPLX_1:1
.= 123*503+13907+(177*172+177*5)
.= 123*503+13907+177*172+177*5 by XCMPLX_1:1
.= 123*503+177*172+13907+177*5 by XCMPLX_1:1
.= 123*503+177*172+(13907+885) by XCMPLX_1:1
.= 123*503+(172*177+172*86) by XCMPLX_1:1
.= 263*172+123*503;
hence thesis;
end;
(164*332+1)*(164*332+1)
= (212*256+177)*(212*256)+(212*256+177)*177 by Lm48,XCMPLX_1:8
.= (212*256)*(212*256)+(212*256)*177+((212*256+177)*177) by XCMPLX_1:8
.= (212*256)*(212*256)+(212*256)*177+(212*256*177+177*177) by XCMPLX_1:8
.= (212*256)*(212*256)+(212*256)*177+212*256*177+177*177 by XCMPLX_1:1
.= (212*256)*(212*256)+(292*256*256+512*148)+177*177 by A2,XCMPLX_1:1
.= (263*172*256*256)+512*148+177*177 by A3,XCMPLX_1:1
.= 263*172*256*256+(263*172+123*503) by A4,XCMPLX_1:1
.= 263*172*256*256+263*172+123*503 by XCMPLX_1:1
.= (263*172)*(256*256)+(263*172)*1+123*503 by XCMPLX_1:4
.= (263*172)*(256*256+1)+123*503 by XCMPLX_1:8;
hence thesis;
end;
A5:123*503 < 256*256 + 1
proof
123*503+0 < 256*256+1 by REAL_1:67;
hence thesis;
end;
3 |^ 32 mod Fermat(4) = (3 |^ (16+16)) mod Fermat(4)
.= (3 |^ 16*3 |^ 16) mod Fermat(4) by NEWTON:13
.= ((164*332+1)*(164*332+1)) mod Fermat(4) by Lm47,EULER_2:11
.= 123*503 by A1,A5,Th59,NAT_1:def 2;
hence thesis;
end;
Lm50:
3 |^ 64 mod Fermat(4) = 14*1367+1
proof
A1:(123*503)*(123*503) = (325+(241*241))*(256*256+1)+(14*1367+1)
proof
A2:123*503 = 256*241+173
proof
256*241+173 = 241*(246+10)+173
.= 241*246+241*10+173 by XCMPLX_1:8
.= 241*246+(2410+173) by XCMPLX_1:1
.= 123*482+123*21
.= 123*(482+21) by XCMPLX_1:8;
hence thesis;
end;
A3:(256*241)*173+173*(256*241)=346*256*241
proof
(256*241)*173+173*(256*241) = (256*241)*(173+173) by XCMPLX_1:8
.= 346*(256*241);
hence thesis by XCMPLX_1:4;
end;
A4:346*256*241 = 256*256*325+128*372
proof
346*256*241 = 256*241*(325+21) by XCMPLX_1:4
.= 256*241*325+256*241*21 by XCMPLX_1:8
.= 256*241*325+(256*(241*21)) by XCMPLX_1:4
.= 256*(325*15+186)+256*241*325
.= 256*(325*15)+256*186+256*241*325 by XCMPLX_1:8
.= 256*325*15+256*186+256*241*325 by XCMPLX_1:4
.= (256*325)*15+256*241*325+256*186 by XCMPLX_1:1
.= (256*325)*15+(256*325)*241+256*186 by XCMPLX_1:4
.= (256*325)*(15+241)+256*186 by XCMPLX_1:8
.= 256*256*325+128*(2*186) by XCMPLX_1:4;
hence thesis;
end;
A5:128*372+173*173 = (325+(241*241))*1+(14*1367+1)
proof
A6:68*414+14*1367+326=128*372
proof
68*414+14*1367+326 = 68*372+1694+1162+14*1367+326
.= 68*372+14*121+14*1367+1162+326 by XCMPLX_1:1
.= 372*(68+56)+(1162+326) by XCMPLX_1:1
.= 372*124+372*4
.= 372*(124+4) by XCMPLX_1:8
.= 372*128;
hence thesis;
end;
(325+(241*241))*1+(14*1367+1) = 325+(241*241)+14*1367+1 by XCMPLX_1:1
.= 241*241+14*1367+325+1 by XCMPLX_1:1
.= 241*241+14*1367+(325+1) by XCMPLX_1:1
.= 241*(173+68)+14*1367+326
.= 241*173+241*68+14*1367+326 by XCMPLX_1:8
.= 173*68+173*173+241*68+14*1367+326
.= 173*68+241*68+173*173+14*1367+326 by XCMPLX_1:1
.= 173*68+241*68+14*1367+173*173+326 by XCMPLX_1:1
.= 128*372+173*173 by A6,XCMPLX_1:1;
hence thesis;
end;
(123*503)*(123*503)
= ((256*241)+173)*(241*256)+((256*241)+173)*173 by A2,XCMPLX_1:8
.= (256*241)*(256*241)+(256*241)*173+173*((256*241)+173) by XCMPLX_1:8
.= 256*241*256*241+(256*241)*173+173*((256*241)+173) by XCMPLX_1:4
.= 256*256*241*241+(256*241)*173+173*((256*241)+173) by XCMPLX_1:4
.= (256*256)*(241*241)+(256*241)*173+(173*((256*241)+173)) by XCMPLX_1:4
.= (256*256)*(241*241)+(256*241)*173+(173*(256*241)+173*173)
by XCMPLX_1:8
.= (256*256)*(241*241)+(256*241)*173+173*(256*241)+173*173 by XCMPLX_1:1
.= 256*256*325+128*372+(256*256)*(241*241)+173*173 by A3,A4,XCMPLX_1:1
.= (256*256)*325+(256*256)*(241*241)+128*372+173*173 by XCMPLX_1:1
.= (256*256)*(325+(241*241))+128*372+173*173 by XCMPLX_1:8
.= (325+(241*241))*1+(14*1367+1)+(325+(241*241))*(256*256)
by A5,XCMPLX_1:1
.= (325+(241*241))*1+(325+(241*241))*(256*256)+(14*1367+1) by XCMPLX_1:1
.= (325+(241*241))*1+(325+(241*241))*(256*256)+14*1367+1 by XCMPLX_1:1
.= (325+(241*241))*(256*256+1)+14*1367+1 by XCMPLX_1:8;
hence thesis by XCMPLX_1:1;
end;
A7:14*1367+1 < 256*256+1 by REAL_1:53;
3 |^ 64 mod Fermat(4) = (3 |^ (32+32)) mod Fermat(4)
.= (3 |^ 32*3 |^ 32) mod Fermat(4) by NEWTON:13
.= ((123*503)*(123*503)) mod Fermat(4) by Lm49,EULER_2:11
.= 14*1367+1 by A1,A7,Th59,NAT_1:def 2;
hence thesis;
end;
Lm51:
256*74*390+195*195 = ((256*256)*113)+5589*1+52*289
proof
((256*256)*113)+5589*1+52*289 = 256*(256*113)+5589+52*289 by XCMPLX_1:4
.= 256*((74*390)+68)+5589+52*289
.= 256*(74*390)+256*68+5589+52*289 by XCMPLX_1:8
.= 256*74*390+(17408+5589)+15028 by XCMPLX_1:1
.= 256*74*390+(22815+182)+15028
.= 256*74*390+22815+182+15028 by XCMPLX_1:1
.= 256*74*390+22815+(182+15028) by XCMPLX_1:1
.= 256*74*390+(22815+15210) by XCMPLX_1:1
.= 256*74*390+(195*(117+78));
hence thesis;
end;
Lm52:
3 |^ 128 mod Fermat(4) = 52*289
proof
A1:(14*1367+1)*(14*1367+1) = 5589*(256*256+1) + 52*289
proof
(14*1367+1)*(14*1367+1)
= ((256*74)+195)*(256*74)+((256*74)+195)*195 by XCMPLX_1:8
.= (256*74)*(256*74)+(74*256)*195+((256*74)+195)*195 by XCMPLX_1:8
.= 256*74*256*74+(256*74)*195+((256*74)+195)*195 by XCMPLX_1:4
.= 256*256*74*74+(256*74)*195+((256*74)+195)*195 by XCMPLX_1:4
.= (256*256)*(74*74)+(256*74)*195+(((256*74)+195)*195) by XCMPLX_1:4
.= (256*256)*(74*74)+(256*74)*195+(195*(256*74)+195*195) by XCMPLX_1:8
.= (256*256)*(74*74)+(256*74)*195+(195*(256*74))+195*195 by XCMPLX_1:1
.= (256*256)*(74*74)+((256*74)*195+(256*74)*195)+195*195 by XCMPLX_1:1
.= (256*256)*(74*74)+((256*74)*(195+195))+195*195 by XCMPLX_1:8
.= ((256*256)*113)+5589*1+52*289+(256*256)*(74*74) by Lm51,XCMPLX_1:1
.= ((256*256)*113)+5589*1+(256*256)*(74*74)+52*289 by XCMPLX_1:1
.= ((256*256)*113)+(256*256)*(74*74)+5589*1+52*289 by XCMPLX_1:1
.= (256*256)*(74*74+113)+5589*1+52*289 by XCMPLX_1:8
.= 5589*(256*256)+5589*1+52*289;
hence thesis by XCMPLX_1:8;
end;
A2:52*289 < 256*256 + 1
proof
52*289+0 < 256*256+1 by REAL_1:67;
hence thesis;
end;
3 |^ 128 mod Fermat(4) = (3 |^ (64+64)) mod Fermat(4)
.= (3 |^ 64*3 |^ 64) mod Fermat(4) by NEWTON:13
.= ((14*1367+1)*(14*1367+1)) mod Fermat(4) by Lm50,EULER_2:11
.= 52*289 by A1,A2,Th59,NAT_1:def 2;
hence thesis;
end;
Lm53:
256*58*360+180*180 = (256*256*82)+3446*1+282
proof
(256*256*82)+3446*1+282 = 256*(256*82)+3446+282 by XCMPLX_1:4
.= 256*((58*360)+112)+3446+282
.= 256*(58*360)+256*112+3446+282 by XCMPLX_1:8
.= 256*58*360+(28672+3446)+282 by XCMPLX_1:1
.= 256*58*360+(32118+282) by XCMPLX_1:1
.= 256*58*360+180*180;
hence thesis;
end;
Lm54:
3 |^ 256 mod Fermat(4) = 282
proof
A1:(52*289)*(52*289) = 3446*(256*256+1) + 282
proof
(52*289)*(52*289)
= ((256*58)+180)*(256*58)+((256*58)+180)*180 by XCMPLX_1:8
.= (256*58)*(256*58)+(256*58)*180+((256*58)+180)*180 by XCMPLX_1:8
.= 256*58*256*58+(256*58)*180+((256*58)+180)*180 by XCMPLX_1:4
.= 256*256*58*58+(256*58)*180+((256*58)+180)*180 by XCMPLX_1:4
.= (256*256)*(58*58)+(256*58)*180+((256*58)+180)*180 by XCMPLX_1:4
.= (256*256)*(58*58)+(256*58)*180+(180*(256*58)+180*180) by XCMPLX_1:8
.= (256*256)*(58*58)+(256*58)*180+(180*(256*58))+180*180 by XCMPLX_1:1
.= (256*256)*(58*58)+((256*58)*180+(256*58)*180)+180*180 by XCMPLX_1:1
.= (256*256)*(58*58)+((256*58)*(180+180))+180*180 by XCMPLX_1:8
.= (256*256*82)+3446*1+282+(256*256)*(58*58) by Lm53,XCMPLX_1:1
.= (256*256*82)+3446*1+(256*256)*(58*58)+282 by XCMPLX_1:1
.= (256*256*82)+(256*256)*(58*58)+3446*1+282 by XCMPLX_1:1
.= (256*256)*(58*58+82)+3446*1+282 by XCMPLX_1:8
.= 3446*(256*256)+3446*1+282;
hence thesis by XCMPLX_1:8;
end;
A2:282 < 256*256 + 1
proof
282+0 < 256*256+1 by REAL_1:67;
hence thesis;
end;
3 |^ 256 mod Fermat(4) = (3 |^ (128+128)) mod Fermat(4)
.= (3 |^ 128*3 |^ 128) mod Fermat(4) by NEWTON:13
.= ((52*289)*(52*289)) mod Fermat(4) by Lm52,EULER_2:11
.= 282 by A1,A2,Th59,NAT_1:def 2;
hence thesis;
end;
Lm55:
3 |^ (256*2) mod Fermat(4) = 71*197
proof
A1:282*282 = 1*(256*256+1) + 71*197
proof
1*(256*256+1)+71*197 = 256*256+(1+13987) by XCMPLX_1:1
.= 256*256+(6656+7332)
.= 256*256+26*256+7332 by XCMPLX_1:1
.= (256+26)*256+7332 by XCMPLX_1:8
.= 256*282+26*282
.= (256+26)*282 by XCMPLX_1:8;
hence thesis;
end;
A2:71*197 < 256*256 + 1
proof
71*197+0 < 256*256+1 by REAL_1:67;
hence thesis;
end;
3 |^ (256*2) = (3 |^ 256)*(3 |^ 256)
proof
(3 |^ 256)*(3 |^ 256) = 3 |^ (256+256) by NEWTON:13
.= 3 |^ 512;
hence thesis;
end;
then 3 |^ (256*2) mod Fermat(4) = (282*282) mod Fermat(4)
by Lm54,EULER_2:11
.= 71*197 by A1,A2,Th59,NAT_1:def 2;
hence thesis;
end;
Lm56:
256*54*326+163*163 = (256*256*69)+2985*1+32*257
proof
(256*256*69)+2985*1+32*257 = 256*256*69+(2985+8224) by XCMPLX_1:1
.= 256*(256*69)+11209 by XCMPLX_1:4
.= 256*((54*326)+60)+11209
.= 256*(54*326)+256*60+11209 by XCMPLX_1:8
.= 256*54*326+(256*60+11209) by XCMPLX_1:1
.= 256*54*326+(163*163);
hence thesis;
end;
Lm57:
3 |^ (256*4) mod Fermat(4) = 32*257
proof
A1:(71*197)*(71*197) = 2985*(256*256+1) + 32*257
proof
(71*197)*(71*197)
= ((256*54)+163)*(256*54)+((256*54)+163)*163 by XCMPLX_1:8
.= (256*54)*(256*54)+(256*54)*163+((256*54)+163)*163 by XCMPLX_1:8
.= 256*54*256*54+(256*54)*163+((256*54)+163)*163 by XCMPLX_1:4
.= 256*256*54*54+(256*54)*163+((256*54)+163)*163 by XCMPLX_1:4
.= (256*256)*(54*54)+(256*54)*163+((256*54)+163)*163 by XCMPLX_1:4
.= (256*256)*(54*54)+(256*54)*163+(163*(256*54)+163*163) by XCMPLX_1:8
.= (256*256)*(54*54)+(256*54)*163+(163*(256*54))+163*163 by XCMPLX_1:1
.= (256*256)*(54*54)+((256*54)*163+(256*54)*163)+163*163 by XCMPLX_1:1
.= (256*256)*(54*54)+((256*54)*(163+163))+163*163 by XCMPLX_1:8
.= (256*256*69)+2985*1+32*257+(256*256)*(54*54) by Lm56,XCMPLX_1:1
.= (256*256*69)+2985*1+(256*256)*(54*54)+32*257 by XCMPLX_1:1
.= (256*256*69)+(256*256)*(54*54)+2985*1+32*257 by XCMPLX_1:1
.= (256*256)*(69+54*54)+2985*1+32*257 by XCMPLX_1:8
.= 2985*(256*256+1)+32*257 by XCMPLX_1:8;
hence thesis;
end;
A2:32*257 < 256*256 + 1
proof
32*257+0 < 256*256+1 by REAL_1:67;
hence thesis;
end;
3 |^ (256*4) = (3 |^ (256*2))*(3 |^ (256*2))
proof
(3 |^ (256*2))*(3 |^ (256*2))
= 3 |^ ((256*2)+(256*2)) by NEWTON:13
.= 3 |^ (1024);
hence thesis;
end;
then 3 |^ (256*4) mod Fermat(4)
= ((71*197)*(71*197)) mod Fermat(4) by Lm55,EULER_2:11
.= 32*257 by A1,A2,Th59,NAT_1:def 2;
hence thesis;
end;
Lm58:
256*32*64+32*32 = (256*256*7)+1031*1+81*809
proof
A1:256*256 = 81*809+7
proof
256*256 = 256*(243+13)
.= 256*(3*81)+256*13 by XCMPLX_1:8
.= 81*768+(81*41+7)
.= 81*768+81*41+7 by XCMPLX_1:1
.= 81*(768+41)+7 by XCMPLX_1:8;
hence thesis;
end;
256*32*64+32*32 = 256*32*(8*8)+32*32
.= 256*32*8*8+32*32 by XCMPLX_1:4
.= 256*256*(7+1)+32*32
.= 256*256*7+256*256*1+32*32 by XCMPLX_1:8
.= 256*256*7+81*809+7+32*32 by A1,XCMPLX_1:1
.= 256*256*7+81*809+(7+32*32) by XCMPLX_1:1
.= 256*256*7+81*809+(1031*1);
hence thesis by XCMPLX_1:1;
end;
Lm59:
3 |^ (256*8) mod Fermat(4) = 81*809
proof
A1:(32*257)*(32*257) = 1031*(256*256+1) + 81*809
proof
(32*257)*(32*257) = ((256*32)+32)*(256*32)+((256*32)+32)*32 by XCMPLX_1:8
.= (256*32)*(256*32)+(256*32)*32+((256*32)+32)*32 by XCMPLX_1:8
.= 256*32*256*32+(256*32)*32+((256*32)+32)*32 by XCMPLX_1:4
.= 256*256*32*32+(256*32)*32+((256*32)+32)*32 by XCMPLX_1:4
.= (256*256)*(32*32)+(256*32)*32+((256*32)+32)*32 by XCMPLX_1:4
.= (256*256)*(32*32)+(256*32)*32+(32*(256*32)+32*32) by XCMPLX_1:8
.= (256*256)*(32*32)+(256*32)*32+(32*(256*32))+32*32 by XCMPLX_1:1
.= (256*256)*(32*32)+((256*32)*32+(256*32)*32)+32*32 by XCMPLX_1:1
.= (256*256)*(32*32)+((256*32)*(32+32))+32*32 by XCMPLX_1:8
.= (256*256*7)+1031*1+81*809+(256*256)*(32*32) by Lm58,XCMPLX_1:1
.= (256*256*7)+1031*1+(256*256)*(32*32)+81*809 by XCMPLX_1:1
.= (256*256*7)+(256*256)*(32*32)+1031*1+81*809 by XCMPLX_1:1
.= (256*256)*(7+32*32)+1031*1+81*809 by XCMPLX_1:8
.= 1031*(256*256+1)+81*809 by XCMPLX_1:8;
hence thesis;
end;
A2:81*809 < 256*256 + 1
proof
A3:81*809 = 81*((3*256)+41)
.= 81*(3*256)+81*41 by XCMPLX_1:8
.= 243*256+3321;
A4:256*256 = 256*(243+13)
.= 256*243+256*13 by XCMPLX_1:8
.= 243*256+3328;
243*256+3321 < 243*256+3328 by REAL_1:53;
then 243*256+3321+0 < 243*256+3328+1 by REAL_1:67;
hence thesis by A3,A4;
end;
3 |^ (256*8) = (3 |^ (256*4))*(3 |^ (256*4))
proof
(3 |^ (256*4))*(3 |^ (256*4))
= 3 |^ ((256*4)+(256*4)) by NEWTON:13
.= 3 |^ (2048);
hence thesis;
end;
then 3 |^ (256*8) mod Fermat(4)
= ((32*257)*(32*257)) mod (256*256+1)
by Lm57,Th59,EULER_2:11
.= 81*809 by A1,A2,NAT_1:def 2;
hence thesis;
end;
Lm60:
256*255*498+249*249 = (256*256*496)+(256*255+241)*1+64
proof
256*255*498+249*249 = 256*255*(496+2)+249*249
.= 256*255*496+256*255*2+249*249 by XCMPLX_1:8
.= 256*255*496+256*(255*2)+249*249 by XCMPLX_1:4
.= 256*255*496+256*(496+14)+249*249
.= 256*255*496+(256*496+256*14)+249*249 by XCMPLX_1:8
.= 256*255*496+256*496+256*14+249*249 by XCMPLX_1:1
.= 256*496*255+256*496*1+256*14+249*249 by XCMPLX_1:4
.= 256*496*(255+1)+256*14+249*249 by XCMPLX_1:8
.= 249*7+(249*7+7*14)+249*249+256*496*256 by XCMPLX_1:1
.= 249*7+249*249+(249*7+7*14)+256*496*256 by XCMPLX_1:1
.= 249*(7+249)+(249*7+7*14)+256*496*256 by XCMPLX_1:8
.= 249*256+(1777+64)+256*496*256
.= 249*256+(1536+241)+64+256*496*256 by XCMPLX_1:1
.= 249*256+6*256+241+64+256*496*256 by XCMPLX_1:1
.= (249+6)*256+241+64+256*496*256 by XCMPLX_1:8
.= 255*256+241+256*496*256+64 by XCMPLX_1:1
.= 256*496*256+(255*256)+241+64 by XCMPLX_1:1
.= 256*256*496+256*255+241+64 by XCMPLX_1:4
.= 256*256*496+(256*255+241)*1+64 by XCMPLX_1:1;
hence thesis;
end;
Lm61:
3 |^ (256*16) mod Fermat(4) = 64
proof
A1:(81*809)*(81*809) = (256*255+241)*(256*256+1) + 64
proof
81*809=(256*255)+249
proof
(256*255)+249 = 256*((3*81)+12)+249
.= 256*(3*81)+256*12+249 by XCMPLX_1:8
.= 36*81+13*12+768*81+249
.= 36*81+768*81+13*12+249 by XCMPLX_1:1
.= (36+768)*81+13*12+249 by XCMPLX_1:8
.= (36+768)*81+(156+249) by XCMPLX_1:1
.= (36+768)*81+5*81
.= (36+768+5)*81 by XCMPLX_1:8;
hence thesis;
end;
then (81*809)*(81*809)
= ((256*255)+249)*(256*255)+((256*255)+249)*249 by XCMPLX_1:8
.= (256*255)*(256*255)+(256*255)*249+((256*255)+249)*249 by XCMPLX_1:8
.= 256*255*256*255+(256*255)*249+((256*255)+249)*249 by XCMPLX_1:4
.= 256*256*255*255+(256*255)*249+((256*255)+249)*249 by XCMPLX_1:4
.= (256*256)*(255*255)+(256*255)*249+((256*255)+249)*249 by XCMPLX_1:4
.= (256*256)*(255*255)+(256*255)*249+(249*(256*255)+249*249)
by XCMPLX_1:8
.= (256*256)*(255*255)+(256*255)*249+(249*(256*255))+249*249
by XCMPLX_1:1
.= (256*256)*(255*255)+((256*255)*249+(256*255)*249)+249*249
by XCMPLX_1:1
.= (256*256)*(255*255)+((256*255)*(249+249))+249*249 by XCMPLX_1:8
.= (256*256*496)+(256*255+241)*1+64+(256*256)*(255*255)
by Lm60,XCMPLX_1:1
.= (256*256*496)+(256*255+241)*1+(256*256)*(255*255)+64 by XCMPLX_1:1
.= (256*256*496)+(256*256)*(255*255)+(256*255+241)*1+64 by XCMPLX_1:1
.= (256*256)*(255*255+(255+241))+(256*255+241)*1+64 by XCMPLX_1:8
.= (256*256)*(255*255+1*255+241)+(256*255+241)*1+64 by XCMPLX_1:1
.= (256*256)*((255+1)*255+241)+(256*255+241)*1+64 by XCMPLX_1:8
.= (256*255+241)*(256*256+1)+64 by XCMPLX_1:8;
hence thesis;
end;
A2:64 < 256*256 + 1
proof
64+0 < 256*256+1 by REAL_1:67;
hence thesis;
end;
3 |^ (256*16) = (3 |^ (256*8))*(3 |^ (256*8))
proof
(3 |^ (256*8))*(3 |^ (256*8))
= 3 |^ ((256*8)+(256*8)) by NEWTON:13
.= 3 |^ (4096);
hence thesis;
end;
then 3 |^ (256*16) mod Fermat(4)
= ((81*809)*(81*809)) mod Fermat(4) by Lm59,EULER_2:11
.= 64 by A1,A2,Th59,NAT_1:def 2;
hence thesis;
end;
Lm62:
3 |^ (256*32) mod Fermat(4) = 256*16
proof
A1:64*64 = 0*(256*256+1) + 256*16;
A2:256*16 < 256*256 + 1
proof
256*16+0 < 256*256+1 by REAL_1:67;
hence thesis;
end;
3 |^ (256*32) = (3 |^ (256*16))*(3 |^ (256*16))
proof
(3 |^ (256*16))*(3 |^ (256*16))
= 3 |^ ((256*16)+(256*16)) by NEWTON:13
.= 3 |^ (8192);
hence thesis;
end;
then 3 |^ (256*32) mod Fermat(4)
= (64*64) mod Fermat(4) by Lm61,EULER_2:11
.= 256*16 by A1,A2,Th59,NAT_1:def 2;
hence thesis;
end;
Lm63:
673*97 = 255*256+1
proof
thus 673*97 = 97*(512+161)
.= 97*512+97*161 by XCMPLX_1:8
.= 194*256+(61*256+1)
.= 194*256+61*256+1 by XCMPLX_1:1
.= (194+61)*256+1 by XCMPLX_1:8
.= 255*256+1;
end;
Lm64:
3 |^ (256*64) mod Fermat(4) = 673*97
proof
A1:673*97 = 97*(512+161)
.= 97*512+97*161 by XCMPLX_1:8
.= 194*256+(61*256+1)
.= 194*256+61*256+1 by XCMPLX_1:1
.= (194+61)*256+1 by XCMPLX_1:8
.= 255*256+1;
A2:(256*16)*(256*16) = 255*(256*256+1) + 673*97
proof
(256*16)*(256*16) = 256*16*256*16 by XCMPLX_1:4
.= 256*256*16*16 by XCMPLX_1:4
.= (256*256)*(16*16) by XCMPLX_1:4
.= (256*256)*(255+1)
.= (256*256)*255+(256*256)*1 by XCMPLX_1:8
.= 256*255*256+((1+255)*256) by XCMPLX_1:4
.= 256*255*256+(1*256+255*256) by XCMPLX_1:8
.= 256*255*256+((255+1)+255*256)
.= 256*255*256+(255+673*97) by A1,XCMPLX_1:1
.= 256*255*256+255+673*97 by XCMPLX_1:1
.= 256*256*255+1*255+673*97 by XCMPLX_1:4
.= (256*256+1)*255+673*97 by XCMPLX_1:8;
hence thesis;
end;
A3:673*97 < 256*256 + 1 by A1,REAL_1:53;
3 |^ (256*64) = (3 |^ (256*32))*(3 |^ (256*32))
proof
(3 |^ (256*32))*(3 |^ (256*32))
= 3 |^ ((256*32)+(256*32)) by NEWTON:13
.= 3 |^ (256*(32+32));
hence thesis;
end;
then 3 |^ (256*64) mod Fermat(4)
= ((256*16)*(256*16)) mod Fermat(4) by Lm62,EULER_2:11
.= 673*97 by A2,A3,Th59,NAT_1:def 2;
hence thesis;
end;
Lm65:
3 |^ (256*128) mod Fermat(4) = 256*256
proof
A1:(255*256+1)*(255*256+1) = 255*255*(256*256+1) + 256*256
proof
(255*256+1)*(255*256+1) = ((255*256)+1)*(255*256)+((255*256)+1)*1
by XCMPLX_1:8
.= ((255*256)+1)*(255*256)+(255*256)+1 by XCMPLX_1:1
.= (255*256)*(255*256)+1*(255*256)+(255*256)+1 by XCMPLX_1:8
.= 255*256*255*256+1*(255*256)+(255*256)+1 by XCMPLX_1:4
.= 255*255*256*256+(255*(255+1))+255*256+1 by XCMPLX_1:4
.= 255*255*256*256+(255*255+255*1)+255*256+1 by XCMPLX_1:8
.= 255*255*256*256+255*255+255*1+255*256+1 by XCMPLX_1:1
.= 255*255*256*256+255*255+255*256+255+1 by XCMPLX_1:1
.= (255*255)*(256*256)+(255*255)*1+255*256+255+1 by XCMPLX_1:4
.= (255*255)*((256*256)+1)+255*256+255+1 by XCMPLX_1:8
.= (255*255)*(256*256+1)+255*256+(255+1) by XCMPLX_1:1
.= (255*255)*(256*256+1)+(255*256+1*256) by XCMPLX_1:1
.= (255*255)*(256*256+1)+(255+1)*256 by XCMPLX_1:8;
hence thesis;
end;
A2:256*256 < 256*256 + 1 by REAL_1:69;
3 |^ (256*128) = (3 |^ (256*64))*(3 |^ (256*64))
proof
(3 |^ (256*64))*(3 |^ (256*64))
= 3 |^ ((256*64)+(256*64)) by NEWTON:13
.= 3 |^ (256*(64+64));
hence thesis;
end;
then 3 |^ (256*128) mod Fermat(4)
= ((673*97)*(673*97)) mod Fermat(4) by Lm64,EULER_2:11
.= 256*256 by A1,A2,Lm63,Th59,NAT_1:def 2;
hence thesis;
end;
Lm66:
Fermat(3) divides (3 |^ (32*0 + 128)) + 1
proof
A1:1 mod Fermat(3) = 1
proof
1 = 257*0 + 1;
hence thesis by Th58,NAT_1:def 2;
end;
A2:257 mod Fermat(3) = 0
proof
257 = 257*1 + 0;
hence thesis by Th58,NAT_1:def 2;
end;
((3 |^ (32*0 + 128)) + 1) mod Fermat(3)
= (256 + 1) mod Fermat(3) by A1,Lm41,EULER_2:8
.= 0 by A2;
then Fermat(3) divides ((3 |^ (32*0 + 128)) + 1) mod Fermat(3) by NAT_1:53;
hence thesis by Th7,Th58;
end;
Lm67:
Fermat(4) divides (3 |^ (64*0 + 256*128)) + 1
proof
A1:Fermat(4) > 0 by Lm42,NAT_1:19;
A2:1 < 256*256 + 1 by REAL_1:69;
A3:1 mod Fermat(4) = 1
proof
1 = (256*256+1)*0 + 1;
hence thesis by A2,Th59,NAT_1:def 2;
end;
(256*256+1) mod Fermat(4) = 0
proof
(256*256+1) = (256*256+1)*1 + 0;
hence thesis by A1,Th59,NAT_1:def 2;
end;
then (3 |^ (64*0 + 256*128) + 1) mod Fermat(4) = 0 by A3,Lm65,EULER_2:8;
then Fermat(4) divides (3 |^ (64*0 + 256*128) + 1) mod Fermat(4) by NAT_1:53
;
hence thesis by Lm42,Th7;
end;
theorem
5 is prime
proof
(3 |^ ((Fermat(1)-'1) div 2)),(-1) are_congruent_mod Fermat(1) by Lm30;
hence thesis by Th56,Th63;
end;
theorem
17 is prime
proof
A1:(3 |^ ((Fermat(2)-'1) div 2)) + 1
= (3 |^ ((Fermat(2)-'1) div 2)) - - 1 by XCMPLX_1:151;
A2:17 -'1 = 17 - 1 by BINARITH:def 3
.= 16 + 0;
A3:2 to_power 4 = 16 by Lm13,POWER:46;
A4:4 -'1 = 4 - 1 by BINARITH:def 3
.= 3 + 0;
2 to_power 1 = 2 |^ 1 by POWER:46
.= 2 by NEWTON:10;
then 16 div 2 = (2 to_power (4-'1)) by A3,NAT_2:18
.= 8 by A4,Lm12,POWER:46;
then (Fermat(2) -'1) div 2 = 16*0 + 8 by A2,Th57;
then Fermat(2) divides (3 |^ ((Fermat(2)-'1) div 2)) + 1 by Lm33;
then Fermat(2) divides ((3 |^ ((Fermat(2)-'1) div 2 )) - (-1)) by A1,Lm1;
then (3 |^ ((Fermat(2)-'1) div 2)),
(-1) are_congruent_mod Fermat(2) by INT_2:19;
hence thesis by Th57,Th63;
end;
theorem
257 is prime
proof
A1:(3 |^ ((Fermat(3)-'1) div 2)) + 1
= (3 |^ ((Fermat(3)-'1) div 2)) - - 1 by XCMPLX_1:151;
A2:257 -'1 = 257 - 1 by BINARITH:def 3
.= 256 + 0;
A3:2 to_power 8 = 2 |^ (4+4) by POWER:46
.= 16*16 by Lm13,NEWTON:13
.=256;
A4:8 -'1 = 8 - 1 by BINARITH:def 3
.= 7 + 0;
2 to_power 1 = 2 |^ 1 by POWER:46
.= 2 by NEWTON:10;
then 256 div 2 = (2 to_power (8-'1)) by A3,NAT_2:18
.= 2 |^ (4+3) by A4,POWER:46
.= 16*8 by Lm12,Lm13,NEWTON:13
.= 128;
then Fermat(3) divides ((3 |^ ((Fermat(3)-'1) div 2 )) - (-1))
by A1,A2,Lm1,Lm66,Th58;
then (3 |^ ((Fermat(3)-'1) div 2)),
(-1) are_congruent_mod Fermat(3) by INT_2:19;
hence thesis by Th58,Th63;
end;
theorem
256*256+1 is prime
proof
A1:(3 |^ ((Fermat(4)-'1) div 2)) + 1
= (3 |^ ((Fermat(4)-'1) div 2)) - - 1 by XCMPLX_1:151;
256*256 + 1 > 0 + 1 by REAL_1:53;
then 256*256 + 1 - 1 > 1 - 1 by REAL_1:54;
then A2:256*256 + 1 -'1 = 256*256 + 1 - 1 by BINARITH:def 3
.= 256*256 + 1 + (-1) by XCMPLX_0:def 8
.= 256*256 + (1 + -1) by XCMPLX_1:1
.= 256*256 + 0;
A3:2 to_power 16 = 2 |^ (8+8) by POWER:46
.= 256*256 by Lm14,NEWTON:13;
A4:16 -'1 = 16 - 1 by BINARITH:def 3
.= 15 + 0;
2 to_power 1 = 2 |^ 1 by POWER:46
.= 2 by NEWTON:10;
then 256*256 div 2 = (2 to_power (16-'1)) by A3,NAT_2:18
.= 2 |^ (8+7) by A4,POWER:46
.= 256*2 |^ (4+3) by Lm14,NEWTON:13
.= 256*(16*8) by Lm12,Lm13,NEWTON:13
.= 256*128;
then Fermat(4) divides
((3 |^ ((Fermat(4)-'1) div 2 )) - (-1)) by A1,A2,Lm1,Lm67,Th59;
then (3 |^ ((Fermat(4)-'1) div 2)),
(-1) are_congruent_mod Fermat(4) by INT_2:19;
hence thesis by Th59,Th63;
end;