:: Proth Numbers
:: by Christoph Schwarzweller
::
:: Received June 4, 2014
:: Copyright (c) 2014-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, ORDINAL1, CARD_1, XXREAL_0, RELAT_1, ARYTM_3, NEWTON,
INT_1, SUBSET_1, ARYTM_1, ABIAN, TARSKI, XBOOLE_0, INT_2, NAT_1, EC_PF_2,
INT_7, INT_5, INT_3, PEPIN, SQUARE_1, ZFMISC_1, GRAPH_1, GROUP_1,
ALGSTR_0, FUNCT_7, FUNCT_1, BINOP_2, XCMPLX_0, REAL_1, NAT_6;
notations SUBSET_1, TARSKI, XBOOLE_0, ORDINAL1, STRUCT_0, NUMBERS, CARD_1,
XCMPLX_0, XREAL_0, ALGSTR_0, GR_CY_1, INT_5, INT_1, ABIAN, SQUARE_1,
GROUP_1, PEPIN, NAT_3, BINOP_1, MEMBERED, INT_2, INT_3, EC_PF_2, INT_7,
NAT_D, XXREAL_0, NEWTON;
constructors REAL_1, NAT_D, POWER, DOMAIN_1, ABIAN, PEPIN, NAT_3, NUMBERS,
NAT_4, NEWTON, EC_PF_2, SUBSET_1, ALGSTR_0, INT_5, INT_7, XXREAL_0,
GROUP_1, GR_CY_1, BINOP_2, RELSET_1, XTUPLE_0, BINOP_1, INT_3;
registrations ORDINAL1, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED,
NEWTON, NAT_2, NAT_3, SQUARE_1, INT_7, ABIAN, STRUCT_0, WSIERP_1,
INT_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities INT_1, SQUARE_1;
expansions NAT_2, INT_1, INT_2, EC_PF_2, MEMBERED, ABIAN;
theorems ABIAN, INT_1, INT_2, NAT_1, NAT_2, NEWTON, XREAL_1, XCMPLX_0,
XCMPLX_1, XXREAL_0, NAT_4, ORDINAL1, PEPIN, SQUARE_1, EC_PF_2, INT_3,
XBOOLE_0, NAT_D, INT_5, INT_7, GROUP_1, GR_CY_1, EULER_1, ALGSTR_0,
TARSKI, NAGATA_2;
schemes NAT_1;
begin :: Preliminaries
registration
let n be positive Nat;
cluster n - 1 -> natural;
coherence
proof
n + 1 > 0 + 1 by XREAL_1:6;
then n >= 1 by NAT_1:13;
then n - 1 >= 1 - 1 by XREAL_1:9;
then n - 1 in NAT by INT_1:3;
hence thesis;
end;
end;
registration
let n be non trivial Nat;
cluster n - 1 -> positive;
coherence
proof
n - 1 >= 2 - 1 by NAT_2:29,XREAL_1:9;
hence thesis;
end;
end;
registration
let n be Nat;
reduce 1|^n to 1;
reducibility;
end;
Lm1:
for n being even Nat holds (-1)|^n = 1
proof
let n be even Nat;
defpred P[Nat] means $1 is even implies (-1)|^($1) = 1;
A1: now let k be Nat;
assume A2: for n being Nat st n < k holds P[n];
per cases;
suppose k is odd;
hence P[k];
end;
suppose A3: k is even;
now per cases;
case k = 0;
hence P[k] by NEWTON:4;
end;
case A4: k > 0;
0 is even & 0+1=1;
then k-2 in NAT by A3,A4,NAT_1:23,INT_1:5;
then reconsider k2 = k-2 as Nat;
A5: k2 + 2 = k; then
A6: k2 is even by A3;
(-1)|^k = (-1)|^(k2+2)
.= ((-1)|^k2) * ((-1)|^2) by NEWTON:8
.= 1 * (-1)|^(1+1) by A2,A6,A5,NAT_1:16
.= (-1)|^1 * (-1) by NEWTON:6
.= (-1) * (-1);
hence P[k];
end;
end;
hence P[k];
end;
end;
for k being Nat holds P[k] from NAT_1:sch 4(A1);
hence thesis;
end;
registration
let n be even Nat;
reduce (-1)|^n to 1;
reducibility by Lm1;
end;
Lm2:
for n being odd Nat holds (-1)|^n = -1
proof
let n be odd Nat;
defpred P[Nat] means $1 is odd implies (-1)|^($1) = -1;
A1: now let k be Nat;
assume A2: for n being Nat st n < k holds P[n];
per cases;
suppose k is even;
hence P[k];
end;
suppose A3: k is odd;
now per cases by NAT_1:23;
case k = 0;
hence P[k];
end;
case k = 1;
hence P[k];
end;
case k >= 2;
then k-2 in NAT by INT_1:5;
then reconsider k2 = k-2 as Nat;
A4: k2 + 2 = k; then
A5: k2 is odd by A3;
(-1)|^k = (-1)|^(k2+2)
.= ((-1)|^k2) * ((-1)|^2) by NEWTON:8
.= (-1) * (-1)|^(1+1) by A2,A5,A4,NAT_1:16
.= (-1) * (-1)|^1 * (-1) by NEWTON:6
.= (-1) * (-1) * (-1);
hence P[k];
end;
end;
hence P[k];
end;
end;
for k being Nat holds P[k] from NAT_1:sch 4(A1);
hence thesis;
end;
registration
let n be odd Nat;
reduce (-1)|^n to -1;
reducibility by Lm2;
end;
theorem Th1:
for a being positive Nat,
n,m being Nat st n >= m holds a|^n >= a|^m
proof
let a be positive Nat;
let n,m be Nat;
assume n >= m;
then a|^m divides a|^n by NEWTON:89;
hence thesis by INT_2:27;
end;
theorem Th2:
for a being non trivial Nat,
n,m being Nat st n > m holds a|^n > a|^m
proof
let a be non trivial Nat;
let n,m be Nat;
assume A1: n > m;
then consider k being Nat such that
A2: n = m + k by NAT_1:10;
k <> 0 by A1,A2;
then k + 1 > 0 + 1 by XREAL_1:6;
then k >= 1 by NAT_1:13;
then a|^k >= a|^1 by Th1;
then A3: a|^k >= a;
a >= 2 by NAT_2:29;
then a|^k >= 1 + 1 by A3,XXREAL_0:2;
then a|^k > 1 by NAT_1:13;
then 1 * a|^m < a|^k * a|^m by XREAL_1:68;
hence thesis by A2,NEWTON:8;
end;
theorem Th3:
for n being non zero Nat
ex k being Nat,
l being odd Nat st n = l * 2|^k
proof
let n be non zero Nat;
consider a,b being Nat such that
A1: n = (2|^a)*(2*b+1) by NAGATA_2:1;
take a,2*b+1;
thus thesis by A1;
end;
theorem
for n being even Nat holds n div 2 = n/2
proof
let n be even Nat;
ex k being Nat st n = 2*k by ABIAN:def 2;
hence thesis;
end;
theorem
for n being odd Nat holds n div 2 = (n-1)/2
proof
let n be odd Nat;
consider k being Integer such that A1: n = 2*k+1 by ABIAN:1;
A2: (n-1)/2 = k by A1;
(n-1)+1 = n; then
n-1 <= n by INT_1:6; then
A3: k <= n/2 by A2,XREAL_1:72;
(n/2) - (1/2) > (n/2) - 1 by XREAL_1:10;
hence thesis by A1,A3,INT_1:def 6;
end;
registration
let n be even Integer;
cluster n/2 -> integer;
coherence
proof
ex k being Integer st n = 2 * k by ABIAN:def 1,INT_1:def 3;
hence thesis;
end;
end;
registration
let n be even Nat;
cluster n/2 -> natural;
coherence
proof
consider k being Integer such that
A1: n = 2 * k by ABIAN:def 1,INT_1:def 3;
k >= 0 by A1;
then k in NAT by INT_1:3; then
reconsider k as Nat;
n / 2 = k by A1;
hence thesis;
end;
end;
begin :: Congruences and Prime Numbers
registration
cluster prime -> non trivial for Nat;
coherence;
end;
Lm3:
for a being Nat,
b being Integer st a divides b holds a gcd b = a
proof
let a be Nat, b be Integer;
assume A1: a divides b;
for m being Integer st m divides a & m divides b holds m divides a;
hence thesis by A1,INT_2:def 2;
end;
theorem Th6:
for p being Prime,
a being Integer holds a gcd p <> 1 iff p divides a
proof
let p be Prime,
a be Integer;
hereby assume a gcd p <> 1;
then a gcd p = p by INT_2:21,INT_2:def 4;
hence p divides a by INT_2:21;
end;
assume A1: p divides a;
p divides (a gcd p) by A1,INT_2:22;
hence a gcd p <> 1 by INT_2:27,INT_2:def 4;
end;
theorem Th7:
for i,j being Integer,
p being Prime
st p divides i * j holds p divides i or p divides j
proof
let i,j be Integer,
p be Prime;
assume A1: p divides i * j;
assume not(p divides i);
then i gcd p = 1 by Th6;
hence thesis by A1,INT_2:25,INT_2:def 3;
end;
theorem Th8:
for x,p being Prime,
k being non zero Nat holds x divides (p|^k) iff x = p
proof
let x,p be Prime;
let k be non zero Nat;
A1: now assume A2: x divides (p|^k);
defpred P[Nat] means x divides p|^($1) implies x = p;
A3: P[1]
proof
assume x divides p|^1;
then x divides p;
then x = 1 or x = p by INT_2:def 4;
hence x = p by NAT_2:def 1;
end;
A4: now let k be non zero Nat;
assume A5: P[k];
now assume A6: x divides p|^(k+1);
A7: p|^(k+1) = p * p|^k by NEWTON:6;
per cases by INT_2:30;
suppose x,p are_coprime;
hence x = p by A5,A6,A7,INT_2:25;
end;
suppose x = p;
hence x = p;
end;
end;
hence P[k + 1];
end;
A8: for k being non zero Nat holds P[k] from NAT_1:sch 10(A3,A4);
thus x = p by A8,A2;
end;
now assume A9: x = p;
reconsider k1 = k-1 as Nat;
p * p|^k1 = p|^(k1+1) by NEWTON:6;
hence x divides (p|^k) by A9;
end;
hence thesis by A1;
end;
theorem
for x,y,n being Integer
holds x,y are_congruent_mod n iff ex k being Integer st x = k * n + y
proof
let x,y,n be Integer;
now assume x,y are_congruent_mod n;
then consider k being Integer such that
A1: n * k = x - y;
x = n * k + y by A1;
hence ex k being Integer st x = k * n + y;
end;
hence thesis;
end;
theorem Th10:
for i being Integer,
j being non zero Integer holds i, i mod j are_congruent_mod j
proof
let i be Integer;
let j be non zero Integer;
i = (i div j) * j + (i mod j) by INT_1:59;
hence i, i mod j are_congruent_mod j;
end;
::$CT
theorem Th12:
for i,j being Integer,
n being Nat
st n < j & i,n are_congruent_mod j holds i mod j = n
proof
let i,j be Integer,
n be Nat;
assume A1: n < j & i,n are_congruent_mod j;
then consider x being Integer such that
A2: j * x = i - n;
A3: i = (i div j) * j + (i mod j) by A1,INT_1:59;
per cases;
suppose n = 0;
hence i mod j = n by A1;
end;
suppose A5: n <> 0;
A6: i/j = (j*x+n) * j" by A2,XCMPLX_0:def 9
.= x * (j * j") + n * j"
.= x * 1 + n * j" by A1,XCMPLX_0:def 7;
then A7: x <= i/j by A5,A1,XREAL_1:29;
A8: i/j - 1 = x + (n*j" - 1) by A6;
A9: n/j < j/j by A1,XREAL_1:74;
j/j = j*j" by XCMPLX_0:def 9 .= 1 by A1,XCMPLX_0:def 7;
then n*j" < 1 by A9,XCMPLX_0:def 9;
then n*j" - 1 < 1 - 1 by XREAL_1:9;
then i/j - 1 < x by A8,XREAL_1:30;
then i div j = x by A7,INT_1:def 6;
hence i mod j = n by A2,A3;
end;
end;
theorem Th13:
for n being non zero Nat, x being Integer
holds x,0 are_congruent_mod n or ... or x,(n-1) are_congruent_mod n
proof
let n be non zero Nat, x be Integer;
x mod n in NAT by INT_1:3;
then reconsider j = x mod n as Nat;
(x mod n) + 1 <= n by INT_1:7,INT_1:58;
then A1: (x mod n) + 1 - 1 <= n - 1 by XREAL_1:9;
take j; thus thesis by Th10,A1;
end;
theorem Th14:
for n being non zero Nat,
x being Integer,
k,l being Nat
st k < n & l < n & x,k are_congruent_mod n & x,l are_congruent_mod n
holds k = l
proof
let n be non zero Nat,
x be Integer,
k,l be Nat;
assume A1: k < n & l < n &
x,k are_congruent_mod n & x,l are_congruent_mod n;
hence k = x mod n by Th12 .= l by A1,Th12;
end;
theorem Th15:
for x being Integer
holds x|^2, 0 are_congruent_mod 3 or x|^2, 1 are_congruent_mod 3
proof
let x be Integer;
x,0 are_congruent_mod 3 or ... or x,(3-1) are_congruent_mod 3 by Th13;
then A1:
x,0 are_congruent_mod 3 or ... or x,2 are_congruent_mod 3;
per cases by A1;
suppose x,0 are_congruent_mod 3;
then x*x, 0*0 are_congruent_mod 3 by INT_1:18;
hence thesis by NEWTON:81;
end;
suppose x,1 are_congruent_mod 3;
then x*x, 1*1 are_congruent_mod 3 by INT_1:18;
hence thesis by NEWTON:81;
end;
suppose x,2 are_congruent_mod 3;
then x*x, 2*2 are_congruent_mod 3 by INT_1:18;
then 4, x*x are_congruent_mod 3 by INT_1:14;
then (4-3),x*x are_congruent_mod 3 by INT_1:22;
then x*x, (4-3) are_congruent_mod 3 by INT_1:14;
hence thesis by NEWTON:81;
end;
end;
theorem Th16:
for p being Prime,
x,y being Element of Z/Z*(p),
i,j being Integer
st x = i & y = j holds x * y = (i * j) mod p
proof
let p be Prime,
x,y be Element of Z/Z*(p), i,j be Integer;
assume A1: x = i & y = j;
A2: INT.Ring(p) = doubleLoopStr(#Segm(p),addint(p),
multint(p),In (1,Segm(p)),In (0,Segm(p))#)
by INT_3:def 12;
A3: Z/Z*(p) = multMagma(#Segm0(p),multint0(p)#) by INT_7:def 4;
then x in Segm0(p);
then x in Segm(p)\{0} by INT_2:def 4,INT_7:def 2;
then reconsider xx = x as Element of Segm(p) by XBOOLE_0:def 5;
y in Segm0(p) by A3;
then y in Segm(p)\{0} by INT_2:def 4,INT_7:def 2;
then reconsider yy = y as Element of Segm(p) by XBOOLE_0:def 5;
reconsider x1 = xx, y1= yy as Element of INT.Ring(p) by A2;
A4: x * y = x1 * y1 by INT_7:20;
x1 * y1 = (multint(p)).(xx,yy) by A2,ALGSTR_0:def 18;
hence thesis by A4,A1,INT_3:def 10;
end;
theorem Th17:
for p being Prime,
x being Element of Z/Z*(p),
i being Integer,
n being Nat
st x = i holds x |^ n = (i |^ n) mod p
proof
let p be Prime,
x be Element of Z/Z*(p), i be Integer,
n be Nat;
assume A1: x = i;
A2: Z/Z*(p) = multMagma(#Segm0(p),multint0(p)#) by INT_7:def 4;
Segm0(p) = Segm(p) \ {0} by INT_2:def 4,INT_7:def 2;
then A3: i in Segm(p) by A2,A1,XBOOLE_0:def 5;
reconsider i as Element of NAT by A1,A2,INT_1:3;
defpred P[Nat] means
x |^ ($1) = (i |^ ($1)) mod p;
A4: x|^0 = 1_(Z/Z*(p)) by GROUP_1:25;
1 < p by INT_2:def 4;
then A5: 1 div p <= 1-1 by INT_1:56,INT_1:52;
A6: 1 div p = 0 by A5;
i|^0 = 1 by NEWTON:4;
then (i |^ 0) mod p = 1 - (1 div p) * p by INT_1:def 10;
then A7: P[0] by A4,A6,INT_7:21;
A8: now let k be Nat;
assume A9: P[k];
x |^ (k+1) = x|^k * x by GROUP_1:34
.= ((i |^ k mod p) * i) mod p by A1,A9,Th16
.= ((i |^ k mod p) * (i mod p)) mod p by A3,NAT_D:24,NAT_1:44
.= (i |^ k * i) mod p by NAT_D:67
.= (i |^ (k+1)) mod p by NEWTON:6;
hence P[k+1];
end;
A10: for k being Nat holds P[k] from NAT_1:sch 2(A7,A8);
thus thesis by A10;
end;
theorem Th18:
for p being Prime,
x being Integer
holds x|^2, 1 are_congruent_mod p iff
(x, 1 are_congruent_mod p or x, -1 are_congruent_mod p)
proof
let p be Prime,
x be Integer;
A1: now assume x|^2, 1 are_congruent_mod p;
then p divides (x^2 - 1^2) by NEWTON:81;
then A2: p divides (x+1) * (x-1);
now per cases by A2,Th7;
case p divides x+1;
then consider l being Integer such that
A3: p * l = x + 1;
thus x,-1 are_congruent_mod p by A3;
end;
case p divides x-1;
then consider l being Integer such that
A4: p * l = x - 1;
thus x,1 are_congruent_mod p by A4;
end;
end;
hence x,1 are_congruent_mod p or x,-1 are_congruent_mod p;
end;
now assume A5: x,1 are_congruent_mod p or x,-1 are_congruent_mod p;
now per cases by A5;
case x,1 are_congruent_mod p;
then x*x,1*1 are_congruent_mod p by INT_1:18;
hence x|^2, 1 are_congruent_mod p by NEWTON:81;
end;
case x,-1 are_congruent_mod p;
then x*x,(-1)*(-1) are_congruent_mod p by INT_1:18;
hence x|^2, 1 are_congruent_mod p by NEWTON:81;
end;
end;
hence x|^2, 1 are_congruent_mod p;
end;
hence thesis by A1;
end;
theorem Th19:
for n being Nat holds
-1,1 are_congruent_mod n iff (n = 2 or n = 1)
proof
let n be Nat;
hereby assume -1,1 are_congruent_mod n;
then consider k being Integer such that A1: n * k = -2;
k < 0 & n <> 0 by A1;
then A2: k <= -1 by INT_1:8;
now assume A3: n <> 2;
now assume n <> 1;
then not(n=0 or ... or n = 2) by A1,A3;
then not(n <= 2);
then n >= 2+1 by NAT_1:13;
then n >= 3 & k < 0 by A1;
then A4: n * k <= 3 * k by XREAL_1:65;
3 * k <= 3 * (-1) by A2,XREAL_1:64;
hence contradiction by A1,A4,XXREAL_0:2;
end;
hence n = 1;
end;
hence n = 2 or n = 1;
end;
assume A5: n = 2 or n = 1;
per cases by A5;
suppose n = 2;
then n * (-1) = -2;
hence -1,1 are_congruent_mod n;
end;
suppose n = 1;
hence -1,1 are_congruent_mod n by INT_1:13;
end;
end;
theorem Th20:
for i being Integer
holds -1,1 are_congruent_mod i iff (i = 2 or i = 1 or i = -2 or i = -1)
proof
let n be Integer;
hereby assume A1: -1,1 are_congruent_mod n;
then consider k being Integer such that A2: n * k = -2;
now per cases;
case n >= 0;
then n in NAT by INT_1:3;
then reconsider m = n as Nat;
m = 1 or m = 2 by A1,Th19;
hence n = 2 or n = 1 or n = -2 or n = -1;
end;
case A3: n < 0;
then A4: k > 0 by A2;
then A5: k >= 0 + 1 by INT_1:7;
now assume A6: n <> -2;
now assume A7: n <> -1;
n <= -1 by A3,INT_1:8;
then n < -1 by A7,XXREAL_0:1;
then n + 1 <= -1 by INT_1:7;
then n + 1 - 1 <= -1 - 1 by XREAL_1:9;
then n < -2 by A6,XXREAL_0:1;
then n + 1 <= -2 by INT_1:7;
then n + 1 - 1 <= -2 - 1 by XREAL_1:9;
then A8: n * k <= (-3) * k by A4,XREAL_1:64;
(-3) * k <= (-3) * 1 by A5,XREAL_1:65;
hence contradiction by A2,A8,XXREAL_0:2;
end;
hence n = -1;
end;
hence n = 2 or n = 1 or n = -2 or n = -1;
end;
end;
hence n = 2 or n = 1 or n = -2 or n = -1;
end;
assume A9: n = 2 or n = 1 or n = -2 or n = -1;
per cases by A9;
suppose n = 2;
then n * (-1) = -2;
hence -1,1 are_congruent_mod n;
end;
suppose n = 1;
hence -1,1 are_congruent_mod n by INT_1:13;
end;
suppose n = -2;
hence -1,1 are_congruent_mod n;
end;
suppose n = -1;
then n * (-1) = 1;
hence -1,1 are_congruent_mod n by INT_1:20,INT_1:13;
end;
end;
begin :: n_greater
definition
let n,x be Real;
attr x is n_greater means :Def1:
x > n;
end;
registration
let r be Real;
cluster r_greater for Real;
existence
proof
take r+1;
r+0 < r+1 by XREAL_1:8;
hence thesis;
end;
end;
notation
let n,x be Real;
antonym x is n_smaller for x is n_or_greater;
antonym x is n_or_smaller for x is n_greater;
end;
registration
let n be Nat;
cluster n_greater odd for Nat;
existence
proof
per cases;
suppose n is even; then
consider k being Nat such that
A1: n = 2 * k;
take n + 1;
n+1 > n+0 by XREAL_1:6;
hence n+1 is n_greater;
thus n+1 is odd by A1;
end;
suppose n is odd;
then consider k being Integer such that
A2: n = 2 * k + 1 by ABIAN:1;
take n + 2;
n+1 > n+0 by XREAL_1:6;
hence n+2 is n_greater by XREAL_1:6;
thus n+2 is odd by A2;
end;
end;
cluster n_greater even for Nat;
existence
proof
per cases;
suppose n is odd;
then consider k being Integer such that
A3: n = 2 * k + 1 by ABIAN:1;
take n + 1;
n+1 > n+0 by XREAL_1:6;
hence n+1 is n_greater;
thus n+1 is even by A3;
end;
suppose n is even;
then consider k being Nat such that
A4: n = 2 * k;
take n + 2;
n+1 > n+0 by XREAL_1:6;
hence n+2 is n_greater by XREAL_1:6;
thus n+2 is even by A4;
end;
end;
end;
registration
let n be Real;
cluster n_greater -> n_or_greater for Nat;
coherence;
end;
registration
let n be Real;
cluster (n+1)_or_greater -> n_or_greater for Nat;
coherence
proof
n+1 >= n+0 by XREAL_1:6;
hence thesis by XXREAL_0:2;
end;
cluster (n+1)_greater -> n_greater for Nat;
coherence
proof
n+1 > n+0 by XREAL_1:6;
hence thesis by XXREAL_0:2;
end;
end;
registration
let n be Nat;
cluster n_greater -> (n+1)_or_greater for Nat;
coherence by NAT_1:13;
end;
registration
let m be non trivial Nat;
cluster m_or_greater-> non trivial for Nat;
coherence
proof
let n be Nat;
assume A1: n is m_or_greater;
m >= 2 by NAT_2:29;
hence thesis by A1,XXREAL_0:2;
end;
end;
registration
let a be positive Nat;
let m be Nat;
let n be m_or_greater Nat;
cluster a|^n -> (a|^m)_or_greater;
coherence by Th1,EC_PF_2:def 1;
end;
registration
let a be non trivial Nat;
let m be Nat;
let n be m_greater Nat;
cluster a|^n -> (a|^m)_greater;
coherence by Def1,Th2;
end;
registration
cluster 2_or_greater -> non trivial for Nat;
coherence;
cluster non trivial -> 2_or_greater for Nat;
coherence
proof
let n be Nat;
assume A1: n is non trivial;
n <= 1 implies n = 0 or ... or n = 1;
then n >= 1 + 1 by A1,NAT_1:13;
hence thesis;
end;
cluster non trivial odd -> 2_greater for Nat;
coherence
proof
let n be Nat;
assume A2: n is non trivial odd;
n <= 2 implies n = 0 or ... or n = 2;
hence thesis by A2;
end;
end;
registration
let n be 2_greater Nat;
cluster n - 1 -> non trivial;
coherence
proof
n - 1 > 2 - 1 by Def1,XREAL_1:9;
hence thesis by NAT_2:def 1;
end;
end;
registration
let n be 2_or_greater Nat;
cluster n - 2 -> natural;
coherence
proof
n - 2 >= 2 - 2 by EC_PF_2:def 1,XREAL_1:9;
then n-2 in NAT by INT_1:3;
hence thesis;
end;
end;
registration
let m be non zero Nat;
let n be m_or_greater Nat;
cluster n - 1 -> natural;
coherence
proof
n >= m by EC_PF_2:def 1;
then reconsider nn = n - 1 as Element of NAT by INT_1:3;
n - 1 >= m-1 by EC_PF_2:def 1,XREAL_1:9;
then n-1 in NAT by INT_1:3;
hence thesis;
end;
end;
registration
cluster 2_greater -> odd for Prime;
coherence by INT_2:def 4;
end;
registration
let n be Nat;
cluster n_greater prime for Nat;
existence
proof
now assume A1: not(ex p being Nat st p is n_greater prime);
A2: now let p be Prime;
not(p is n_greater) by A1;
hence p < n+1 by NAT_1:13;
end;
A3: now let p be set;
assume A4: p in SetPrimes;
then reconsider p1 = p as Element of NAT;
A5: p1 is prime by A4,NEWTON:def 6;
then p1 < n+1 by A2;
hence p in SetPrimenumber(n+1) by A5,NEWTON:def 7;
end;
now let p be set;
assume A6: p in SetPrimenumber(n+1);
reconsider n1 = n + 1 as Nat;
SetPrimenumber(n1) c= SetPrimes by NEWTON:68;
hence p in SetPrimes by A6;
end;
then SetPrimes = SetPrimenumber(n+1) by A3;
hence contradiction;
end;
hence thesis;
end;
end;
begin :: Pocklington's theorem revisited
definition
let n be Nat;
mode Divisor of n -> Nat means :Def2:
it divides n;
existence;
end;
registration
let n be non trivial Nat;
cluster non trivial for Divisor of n;
existence
proof
reconsider m = n as Divisor of n by Def2;
take m;
thus thesis;
end;
end;
registration
let n be non zero Nat;
cluster -> non zero for Divisor of n;
coherence
proof
let x be Divisor of n;
consider k being Integer such that A1: x * k = n by Def2,INT_1:def 3;
thus thesis by A1;
end;
end;
registration
let n be positive Nat;
cluster -> positive for Divisor of n;
coherence;
end;
registration
let n be non zero Nat;
cluster -> n_or_smaller for Divisor of n;
coherence
proof
let x be Divisor of n;
consider k being Integer such that A1: x * k = n by Def2,INT_1:def 3;
k >= 0 by A1;
then reconsider k as Element of NAT by INT_1:3;
k <> 0 by A1;
hence thesis by A1,NAT_1:24;
end;
end;
registration let n be non trivial Nat;
cluster prime for Divisor of n;
existence
proof
consider p being Element of NAT such that
A1: p is prime & p divides n by NAT_2:29,INT_2:31;
reconsider p as Nat;
take p;
thus thesis by A1,Def2;
end;
end;
registration
let n be Nat;
let q be Divisor of n;
cluster n / q -> natural;
coherence
proof
per cases;
suppose n = 0;
hence thesis;
end;
suppose A1: n <> 0;
consider k being Integer such that A2: q * k = n by Def2,INT_1:def 3;
0 <= k by A2,A1;
then A3: k in NAT by INT_1:3;
n/q = (q * k) * q" by A2,XCMPLX_0:def 9
.= k * (q * q")
.= k * 1 by A1,XCMPLX_0:def 7;
hence thesis by A3;
end;
end;
end;
registration
let n be Nat;
let s be Divisor of n;
let q be Divisor of s;
cluster n / q -> natural;
coherence
proof
per cases;
suppose n = 0;
hence thesis;
end;
suppose A1: n <> 0;
consider k being Integer such that A2: s * k = n by Def2,INT_1:def 3;
consider l being Integer such that A3: q * l = s by Def2,INT_1:def 3;
0 <= k by A2,A1;
then A4: k in NAT by INT_1:3;
0 <= l by A3,A1;
then A5: l in NAT by INT_1:3;
n/q = ((q * l) * k) * q" by A3,A2,XCMPLX_0:def 9
.= l * k * (q * q")
.= l * k * 1 by A1,XCMPLX_0:def 7;
hence thesis by A4,A5;
end;
end;
end;
::$N Pocklington's theorem
theorem Th21:
for n being 2_greater Nat,
s being non trivial Divisor of n - 1 st s > sqrt(n) &
ex a being Nat
st a|^(n-1),1 are_congruent_mod n &
for q being prime Divisor of s holds a|^((n-1)/q) - 1 gcd n = 1
holds n is prime
proof
let n be 2_greater Nat;
let s be non trivial Divisor of n - 1;
assume A1: s > sqrt(n) &
ex a being Nat
st a|^(n-1),1 are_congruent_mod n &
for q being prime Divisor of s holds a|^((n-1)/q) - 1 gcd n = 1;
reconsider m = n as Element of NAT by ORDINAL1:def 12;
reconsider f = s as Element of NAT by ORDINAL1:def 12;
m > 1+1 by Def1; then
A2: m >= 1 by NAT_1:13;
consider c being Integer such that A3: m-1 = f * c by Def2,INT_1:def 3;
A4: sqrt n >= 0 by SQUARE_1:def 2;
A5: now assume s <= c;
then c >= sqrt(n) by A1,XXREAL_0:2;
then s * c >= (sqrt(n))^2 by A4,A1,XREAL_1:66;
then s * c >= n by SQUARE_1:def 2;
then n - 1 - n >= n - n by A3,XREAL_1:9;
then -1 >= 0;
hence contradiction;
end;
c > 0 by A3;
then reconsider c as Element of NAT by INT_1:3;
A6: m-1 = f*c & f > c & c > 0 by A3,A5;
now let p be Element of NAT;
assume A7: p divides f & p is prime;
reconsider q = p as Nat;
reconsider q as Divisor of s by A7,Def2;
reconsider q as prime Divisor of s by A7;
consider b being Nat such that
A8: b|^(n-1),1 are_congruent_mod n &
for q being prime Divisor of s holds b|^((n-1)/q) - 1 gcd n = 1
by A1;
reconsider a = b as Element of NAT by ORDINAL1:def 12;
consider k1 being Integer such that A9: q * k1 = s by Def2,INT_1:def 3;
consider k2 being Integer such that A10: s * k2 = n-1 by Def2,INT_1:def 3;
consider l1 being Integer such that A11: p * l1 = f by A7;
A12: k2 = c by A3,A10,XCMPLX_1:5;
A13: (m-1)/p = (p * l1 * c) * p" by A3,A11,XCMPLX_0:def 9
.= (l1 * c) * ( p * p")
.= (l1 * c) * 1 by A7,XCMPLX_0:def 7;
A14: n-1 >= 2-1 by Def1,XREAL_1:9;
now assume a = 0;
then a |^ (n-1) = 0 by A14,NEWTON:11;
then n = 1 or n = -1 by A8,INT_2:13;
hence contradiction by Def1;
end;
then a|^((m-'1) div p) + 1 > 0 + 1 by XREAL_1:6;
then A15: a|^((m-'1) div p) >= 1 by NAT_1:13;
(n-1)/q = ((q*k1)*k2) * q" by A9,A10,XCMPLX_0:def 9
.= (k1 * k2) * (q * q")
.= k1 * k2 * 1 by XCMPLX_0:def 7
.= (m-1)/p by A9,A11,A12,A13,XCMPLX_1:5
.= [/ (m-1)/p \] by A13
.= [\ (m-1)/p /] by A13
.= (m-'1) div p by A2,XREAL_1:233; then
a|^((m-'1) div p)-'1 = b|^((n-1)/q) - 1 by A15,XREAL_1:233; then
A16: (a|^((m-'1) div p)-'1) gcd m = 1 by A8;
consider x being Integer such that
A17: n * x = a|^(n-1) - 1 by A8;
A18: a|^(n-1) / n = (n*x+1) * n" by A17,XCMPLX_0:def 9
.= n"*n*x + 1 *n"
.= 1 * x + n" by XCMPLX_0:def 7;
A19: x <= a|^(n-1)/n by A18,XREAL_1:29;
A20: a|^(n-1)/n - 1 = x + (n" - 1) by A18;
2 < n by Def1;
then 2 - 1 < n - 0 by XREAL_1:15;
then n" < 1" by XREAL_1:88;
then n" - 1 < 0 by XREAL_1:49;
then a|^(n-1)/n - 1 < x by A20,XREAL_1:30;
then a|^(n-1) div n = x by A19,INT_1:def 6;
then A21: a|^(n-1) mod n = a|^(n-1) - n * x by INT_1:def 10
.= 1 by A17;
a|^(m-'1) mod m = 1 by A21,A2,XREAL_1:233;
hence ex a being Element of NAT st a|^(m-'1) mod m = 1 &
(a|^((m-'1) div p)-'1) gcd m = 1 by A16;
end;
hence thesis by A6,NAT_4:24;
end;
begin :: Euler's criterion
notation
let a be Integer, p be Nat;
antonym a is_quadratic_non_residue_mod p for a is_quadratic_residue_mod p;
end;
theorem Th22:
for p being positive Nat,
a being Integer holds
a is_quadratic_residue_mod p iff
ex x being Integer st x|^2, a are_congruent_mod p
proof
let p be positive Nat,
a be Integer;
thus a is_quadratic_residue_mod p implies
ex x being Integer st x|^2, a are_congruent_mod p
proof assume a is_quadratic_residue_mod p;
then consider x being Integer such that
A1: (x^2 - a) mod p = 0 by INT_5:def 2;
A2: x^2 - a = ((x^2 - a) div p) * p + 0 by A1,INT_1:59;
take x;
x^2 = x|^2 by NEWTON:81;
hence thesis by A2;
end;
assume ex x being Integer st x|^2, a are_congruent_mod p;
then consider x being Integer such that
A3: x|^2, a are_congruent_mod p;
x^2 = x|^1 * x .= x|^(1+1) by NEWTON:6;
then (x^2 - a) mod p = 0 by A3;
hence a is_quadratic_residue_mod p by INT_5:def 2;
end;
theorem Th23:
2 is_quadratic_non_residue_mod 3
proof
now assume ex x being Integer st x|^2, 2 are_congruent_mod 3;
then consider x being Integer such that
A1: x|^2,2 are_congruent_mod 3;
now per cases by Th15;
case x|^2, 0 are_congruent_mod 3;
hence contradiction by A1,Th14;
end;
case x|^2, 1 are_congruent_mod 3;
hence contradiction by A1,Th14;
end;
end;
hence contradiction;
end;
hence thesis by Th22;
end;
::$N Legendre symbol
definition
let p be Nat;
let a be Integer;
func LegendreSymbol(a,p) -> Integer equals :Def3:
1 if a gcd p = 1 & a is_quadratic_residue_mod p & p <> 1,
0 if p divides a,
-1 if a gcd p = 1 & a is_quadratic_non_residue_mod p & p <> 1;
coherence;
consistency by Lm3;
end;
definition
let p be Prime;
let a be Integer;
redefine func LegendreSymbol(a,p) equals :Def4: :: redefines LegendreSymbol (NAT_6, definition)
1 if a gcd p = 1 & a is_quadratic_residue_mod p,
0 if p divides a,
-1 if a gcd p = 1 & a is_quadratic_non_residue_mod p;
consistency
proof
A1: a gcd p = 1 & a is_quadratic_residue_mod p & p divides a implies
for z being Integer holds z = 1 iff z = 0
proof
assume A2: a gcd p = 1 & a is_quadratic_residue_mod p & p divides a;
then a gcd p = p by Lm3;
hence thesis by A2,INT_2:def 4;
end;
a gcd p = 1 & a is_quadratic_non_residue_mod p & p divides a implies
for z being Integer holds z = -1 iff z = 0
proof
assume A3: a gcd p = 1 & a is_quadratic_non_residue_mod p & p divides a;
then a gcd p = p by Lm3;
hence thesis by A3,INT_2:def 4;
end;
hence thesis by A1;
end;
compatibility
proof
p <> 1 by INT_2:def 4;
hence thesis by Def3;
end;
end;
notation
let p be Nat;
let a be Integer;
synonym Leg(a,p) for LegendreSymbol(a,p);
end;
theorem Th24:
for p be Prime,
a be Integer
holds Leg(a,p) = 1 or Leg(a,p) = 0 or Leg(a,p) = -1
proof
let p be Prime;
let a be Integer;
assume A1: Leg(a,p) <> 1 & Leg(a,p) <> 0;
a gcd p = 1
proof
a gcd p = 1 or a gcd p = p by INT_2:def 4,INT_2:21;
hence thesis by A1,Def4,INT_2:21;
end;
hence Leg(a,p) = -1 by A1,Def4;
end;
theorem Th25:
for p being Prime,
a being Integer holds
(Leg(a,p) = 1 iff a gcd p = 1 & a is_quadratic_residue_mod p) &
(Leg(a,p) = 0 iff p divides a) &
(Leg(a,p) = -1 iff a gcd p = 1 & a is_quadratic_non_residue_mod p)
proof
let p be Prime,
a be Integer;
A1:now assume A2: Leg(a,p) = 0;
now assume not p divides a;
then a gcd p = 1 by Th6;
hence contradiction by A2,Def4;
end;
hence p divides a;
end;
now assume A3: Leg(a,p) = 1;
then a gcd p = 1 by Th6,Def4;
hence a gcd p = 1 & a is_quadratic_residue_mod p by A3,Def4;
end;
hence Leg(a,p) = 1 iff a gcd p = 1 & a is_quadratic_residue_mod p by Def4;
now assume A4: Leg(a,p) = -1;
then a gcd p = 1 by Th6,Def4;
hence a gcd p = 1 & a is_quadratic_non_residue_mod p by A4,Def4;
end;
hence thesis by A1,Def4;
end;
theorem
for p being Nat holds Leg(p,p) = 0 by Def3;
theorem
for a being Integer holds Leg(a,2) = a mod 2
proof
let a be Integer;
per cases;
suppose A1: a is even;
then a mod 2 = 0 by INT_1:62;
hence thesis by A1,Def3;
end;
suppose A2: a is odd;
reconsider amod2 = a mod 2 as Element of NAT by INT_1:3;
A3: amod2 = 0 or amod2 = 1 by NAT_1:23,INT_1:58;
a - 1 = (a div 2) * 2 + 1 - 1 by A3,A2,INT_1:62,INT_1:59;
then A4: 1,a are_congruent_mod 2 by INT_1:def 5,INT_1:14;
a gcd 2 <= 2 by INT_2:27,INT_2:21;
then A5: a gcd 2 = 0 or ... or a gcd 2 = 2;
1|^(1+1) = 1;
hence thesis by A4,INT_2:5,A5,INT_2:21,A3,A2,INT_1:62,Def3,Th22;
end;
end;
Lm4:
for a be Integer, p be Prime holds Lege(a,p) = Leg(a,p)
proof
let a be Integer, p be Prime;
per cases by Th24;
suppose A1: Leg(a,p) = 1;
then not(p divides a) by Th25;
then a mod p <> 0 by INT_1:62;
hence thesis by A1,INT_5:def 3,Th25;
end;
suppose A2: Leg(a,p) = 0;
then A3: p divides a by Th25;
p divides (-a) by A2,Th25,INT_2:10;
then A4: (0^2 - a) mod p = 0;
a mod p = 0 by A3;
hence thesis by A2,A4,INT_5:def 3,INT_5:def 2;
end;
suppose Leg(a,p) = -1;
hence thesis by Th25,INT_5:def 3;
end;
end;
theorem Th28:
for p being 2_greater Prime,
a,b being Integer
st a gcd p = 1 & b gcd p = 1 & a,b are_congruent_mod p
holds Leg(a,p) = Leg(b,p)
proof
let p be 2_greater Prime,
a,b be Integer;
assume A1: a gcd p = 1 & b gcd p = 1 & a,b are_congruent_mod p;
thus Leg(a,p) = Lege(a,p) by Lm4 .= Lege(b,p) by Def1,A1,INT_5:29
.= Leg(b,p) by Lm4;
end;
theorem
for p being 2_greater Prime,
a,b being Integer
st a gcd p = 1 & b gcd p = 1 holds Leg(a*b,p) = Leg(a,p) * Leg(b,p)
proof
let p be 2_greater Prime,
a,b be Integer;
assume A1: a gcd p = 1 & b gcd p = 1;
thus Leg(a*b,p) = Lege(a*b,p) by Lm4
.= Lege(a,p) * Lege(b,p) by A1,Def1,INT_5:30
.= Leg(a,p) * Lege(b,p) by Lm4
.= Leg(a,p) * Leg(b,p) by Lm4;
end;
theorem Th30:
for p,q being 2_greater Prime
st p <> q
holds Leg(p,q) * Leg(q,p) = (-1)|^( ((p-1)/2) * ((q-1)/2) )
proof
let p,q be 2_greater Prime;
assume A1: p <> q;
A2: p > 2 & q > 2 by Def1;
p - 1 > 2 - 1 by Def1,XREAL_1:9;
then p -' 1 = p - 1 by NAT_D:39;
then A3: (p-'1) div 2 = (p-1)/2;
q - 1 > 2 - 1 by Def1,XREAL_1:9;
then q -' 1 = q - 1 by NAT_D:39; then
A4: (-1)|^(((p-'1) div 2)*((q-'1) div 2))
= (-1)|^( ((p-1)/2) * ((q-1)/2) ) by A3;
thus Leg(p,q) * Leg(q,p) = Leg(p,q) * Lege(q,p) by Lm4
.= Lege(p,q) * Lege(q,p) by Lm4
.= (-1)|^( ((p-1)/2) * ((q-1)/2) ) by A1,A2,A4,INT_5:49;
end;
::$N Euler's criterion
theorem Th31:
for p being 2_greater Prime,
a being Integer
st a gcd p = 1
holds a|^((p-1)/2), LegendreSymbol(a,p) are_congruent_mod p
proof
let p be 2_greater Prime,
a be Integer;
p - 1 > 2 - 1 by Def1,XREAL_1:9;
then A1: p -' 1 = p - 1 by NAT_D:39;
assume a gcd p = 1;
then Lege (a,p),a|^((p-'1) div 2) are_congruent_mod p by Def1,INT_5:28;
then A2: Lege (a,p),a|^((p-1)/2) are_congruent_mod p by A1;
Leg(a,p) = Lege(a,p) by Lm4;
hence thesis by A2,INT_1:14;
end;
begin :: Proth Numbers
::$N Proth numbers
definition
let p be Nat;
attr p is Proth means :Def5:
ex k being odd Nat,
n being positive Nat
st 2|^n > k & p = k * (2|^n) + 1;
end;
Lm5: 1 is odd
proof
1 = 2 * 0 + 1;
hence thesis;
end;
Lm6: 3 is Proth
proof
reconsider e = 1 as odd Nat by Lm5;
take e,1;
thus thesis;
end;
Lm7: 9 is Proth
proof
A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2;
A2: 2|^3 = 2|^(2+1) .= 4 * 2 by A1,NEWTON:6;
reconsider e = 1 as odd Nat by Lm5;
take e,3;
thus thesis by A2;
end;
registration
cluster Proth prime for Nat;
existence by Lm6,PEPIN:41;
cluster Proth non prime for Nat;
existence
proof
3 * 3 = 9;
then 3 divides 9;
then 9 is non prime;
hence thesis by Lm7;
end;
end;
registration
cluster Proth -> non trivial odd for Nat;
coherence
proof
let p be Nat;
assume A1: p is Proth; then
consider k being odd Nat,
n being positive Nat such that
A2: 2|^n > k & p = k * 2|^n + 1;
thus p is non trivial by A1,NAT_2:def 1;
reconsider n1 = n - 1 as Element of NAT by INT_1:3;
2 * 2|^n1 = 2|^(1+n1) by NEWTON:6 .= 2|^n;
hence thesis by A2;
end;
end;
theorem
3 is Proth by Lm6;
theorem
5 is Proth
proof
A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2;
reconsider e = 1 as odd Nat by Lm5;
take e,2;
thus thesis by A1;
end;
theorem
9 is Proth by Lm7;
theorem
13 is Proth
proof
A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2;
3 = 2 * 1 + 1; then
reconsider e = 3 as odd Nat;
take e,2;
thus thesis by A1;
end;
theorem
17 is Proth
proof
A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2;
A2: 2|^3 = 2|^(2+1) .= 2|^2 * 2 by NEWTON:6 .= 8 by A1;
A3: 2|^4 = 2|^(3+1) .= 2|^3 * 2 by NEWTON:6 .= 16 by A2;
reconsider e = 1 as odd Nat by Lm5;
take e,4;
thus thesis by A3;
end;
theorem Th37:
641 is Proth
proof
A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2; then
2|^(2+2) = 4 * 4 by NEWTON:8; then
A2: 2|^(4+2) = 16 * 4 by A1,NEWTON:8;
A3: 2|^(6+1) = 2|^6 * 2|^1 by NEWTON:8 .= 64 * 2 by A2;
A4: 5 = 2 * 2 + 1;
641 = 5 * 2|^7 + 1 by A3;
hence thesis by A3,A4;
end;
theorem
11777 is Proth
proof
A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2;
A2: 2|^(2+2) = 4 * 4 by A1,NEWTON:8;
A3: 2|^(4+4) = 16 * 16 by A2,NEWTON:8;
A4: 2|^(8+1) = 2|^8 * 2|^1 by NEWTON:8 .= 256 * 2 by A3;
A5: 23 = 2 * 11 + 1;
11777 = 23 * 2|^9 + 1 by A4;
hence thesis by A4,A5;
end;
theorem
13313 is Proth
proof
A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2; then
2|^(2+2) = 4 * 4 by NEWTON:8; then
2|^(4+4) = 16 * 16 by NEWTON:8; then
A2: 2|^(8+2) = 256 * 4 by A1,NEWTON:8;
A3: 13 = 2 * 6 + 1;
13313 = 13 * 2|^10 + 1 by A2;
hence thesis by A2,A3;
end;
::$N Proth's theorem
theorem Th40: :: Proth
for n being Proth Nat holds
n is prime iff
ex a being Nat st a|^((n-1)/2), -1 are_congruent_mod n
proof
let n be Proth Nat;
consider k being odd Nat,
l being positive Nat such that
A1: 2|^l > k & n = k * (2|^l) + 1 by Def5;
set s = 2|^l;
A2: l + 1 >= 1 + 1 by NAT_1:14,XREAL_1:6;
2|^l >= l + 1 by NEWTON:85;
then 2|^l <>0 & 2|^l <> 1 by A2,XXREAL_0:2;
then reconsider s as non trivial Nat by NAT_2:def 1;
reconsider s as non trivial Divisor of n-1 by A1,INT_1:def 3,Def2;
A3: now assume ex a being Nat
st a |^ ((n-1) / 2), -1 are_congruent_mod n;
then consider a being Nat such that
A4: a |^ ((n-1) / 2), -1 are_congruent_mod n;
A5: (a |^ ((n-1) / 2)) * (a |^ ((n-1) / 2))
= a |^ ( ((n-1) / 2) + ((n-1) / 2) ) by NEWTON:8
.= a|^(n-1);
A6: (-1) * (-1) = 1;
A7: l >= 1 by NAT_1:14;
(2|^l - 1) + 1 > k by A1; then
A8: k <= 2|^l - 1 by NAT_1:13;
then k * 2|^ l <= (2|^l - 1) * 2|^l by XREAL_1:64;
then A9: n <= (2|^l - 1) * 2|^l + 1 by A1,XREAL_1:6;
(2|^l - 1) * 2|^l + 1 = (2|^l) * (2|^l) - 2|^l + 1
.= 2|^(l+l) - 2|^l + 1 by NEWTON:8;
then A10: n < 2|^(l+l) - 2|^l + 1 + 1 by A9,NAT_1:13;
A11: s > sqrt(n)
proof
per cases;
suppose l >= 2;
then A12: 2|^l >= 2|^2 by Th1;
2|^(1+1) = 2|^1 * 2 by NEWTON:6 .= 2 * 2;
then 2|^l > 2 by A12,XXREAL_0:2;
then 2 - 2|^l < 2|^l - 2|^l by XREAL_1:9;
then 2|^(l+l) + (-2|^l + 2) < 2|^(l+l) + 0 by XREAL_1:6;
then A13: n < 2|^(2*l) by A10,XXREAL_0:2;
(2|^l)^2 = 2|^(l+l) by NEWTON:8;
then sqrt(2|^(2*l)) = 2|^l by SQUARE_1:def 2;
hence thesis by A13,SQUARE_1:27;
end;
suppose l < 2;
then l < 1 + 1;
then A14: l <= 1 by NAT_1:13;
then A15: l = 1 by A7,XXREAL_0:1;
then A16: s = sqrt 4 by SQUARE_1:20;
A17: n = k*2|^1 + 1 by A14,A1,A7,XXREAL_0:1 .= k*2 + 1;
A18: k <= 2 - 1 by A8,A15;
k >= 1 by NAT_1:14;
then k = 1 by A18,XXREAL_0:1;
hence thesis by A17,A16,SQUARE_1:27;
end;
end;
now let q be prime Divisor of s;
A19: a|^((n-1)/q), -1 are_congruent_mod n by A4,Th8,INT_2:28,Def2;
1 * (a|^((n-1)/q) - 1) = a|^((n-1)/q) - 1; then
A20: 1 divides a|^((n-1)/q) - 1;
1 * n = n; then
A21: 1 divides n;
now let m be Integer;
assume A22: m divides a|^((n-1)/q) - 1 & m divides n;
then A23: a|^((n-1)/q), 1 are_congruent_mod m;
consider j being Integer such that
A24: m * j = n by A22;
a|^((n-1)/q), -1 are_congruent_mod m by A19,A24,INT_1:20;
then a|^((n-1)/q) - a|^((n-1)/q), (-1)- 1 are_congruent_mod m
by A23,INT_1:17;
then 0+1,(-2)+1 are_congruent_mod m; then
A25: m = 2 or m = 1 or m = -2 or m = -1 by Th20,INT_1:14;
A26: now assume (-2) divides n;
then consider g being Integer such that
A27: n = (-2) * g;
n = 2 * (-g) by A27;
hence contradiction;
end;
1 * 1 = 1 & (-1) * (-1) = 1;
hence m divides 1 by A26,A22,A25;
end;
hence a|^((n-1)/q) - 1 gcd n = 1 by A20,A21,INT_2:def 2;
end;
hence n is prime by A4,A5,INT_1:18,A6,A11,Th21;
end;
now assume n is prime;
then reconsider m = n as prime Proth Nat;
Z/Z*(m) is cyclic by INT_7:31;
then consider g being Element of Z/Z*(m) such that
A28: ord(g) = card(Z/Z*(m)) by GR_CY_1:19;
A29: ord g = m-1 by A28,INT_7:23;
Z/Z*(m) = multMagma(#Segm0(m),multint0(m)#) by INT_7:def 4;
then reconsider g1 = g as Nat;
A30: not(g is being_of_order_0) by A28,GROUP_1:def 11;
A31: (g1 |^ (m-1)) mod m = g |^ (m-1) by Th17
.= 1_(Z/Z*(m)) by A29,A30,GROUP_1:def 11
.= 1 by INT_7:21;
A32: g1 |^ (m-1), 1 are_congruent_mod m by Th10,A31;
A33: (g1 |^ ((m-1) / 2)) |^ (1+1)
= (g1 |^ ((m-1) / 2)) |^ 1 * (g1 |^ ((m-1) / 2)) by NEWTON:6
.= (g1 |^ ((m-1) / 2)) * (g1 |^ ((m-1) / 2))
.= g1 |^ (((m-1) / 2) + ((m-1) / 2)) by NEWTON:8
.= g1 |^ (m-1);
now assume A34: g1 |^ ((m-1) / 2), 1 are_congruent_mod n;
A35: 1_(Z/Z*(m)) = 1 by INT_7:21
.= (g1 |^ ((m-1) / 2)) mod m by A34,INT_2:def 4,Th12
.= g |^ ((m-1) / 2) by Th17;
A36: m-1 <> 0;
(m-1) * 2 >= (m-1) * 1 & 0<2 by XREAL_1:64;
then A37: (m-1) / 2 <= m-1 by XREAL_1:79;
m-1 <= (m-1)/2 by A29,A30,A35,GROUP_1:def 11;
then m-1 = (m-1)/2 by A37,XXREAL_0:1;
hence contradiction by A36;
end;
hence ex a being Nat
st a |^ ((n-1) / 2), -1 are_congruent_mod n by A33,A32,Th18;
end;
hence thesis by A3;
end;
theorem Th41: :: Proth
for l being 2_or_greater Nat,
k being positive Nat
st not(3 divides k) & k <= 2|^l - 1
holds k * 2|^l + 1 is prime iff
3|^(k*2|^(l-1)), -1 are_congruent_mod k* 2|^l + 1
proof
let l be 2_or_greater Nat,
k be positive Nat;
assume A1: not 3 divides k & k <= 2|^l - 1;
set s = 2|^l, a = 3, n = k*2|^l + 1;
k >= 1 by NAT_1:14;
then k * 2|^l >= 1 * 2|^l by XREAL_1:66;
then A2: n >= 2|^l + 1 by XREAL_1:7;
A3: (2|^l)/2 = 2|^((l-1)+1) * 2"
.= (2|^(l-1) * 2) * 2" by NEWTON:6
.= 2|^(l-1) * 1;
A4: 2 * (k * 2|^(l-1)) = k * (2 * 2|^(l-1))
.= k * 2|^((l-1)+1) by NEWTON:6;
A5: l >= 1 by NAT_1:14;
A6: l + 1 >= 1 + 1 by NAT_1:14,XREAL_1:6;
A7: 2|^l >= l + 1 by NEWTON:85;
then 2|^l >= 1 + 1 by A6,XXREAL_0:2;
then 2|^l + 1 >= 2 + 1 by XREAL_1:7;
then n >= 2 + 1 by A2,XXREAL_0:2;
then n > 2 by NAT_1:13;
then reconsider n as 2_greater odd Nat by A4,Def1;
2 * (k * 2|^(l-1)) = k * (2 * 2|^(l-1))
.= k * 2|^((l-1)+1) by NEWTON:6;
then reconsider k2 = (k*2|^l)/2 as Nat;
A8: 3|^((n-1)/2) = 3|^(k*2|^(l-1)) by A3;
A9:now assume A10: 3|^(k*2|^(l-1)), -1 are_congruent_mod k* 2|^l + 1;
reconsider s as Divisor of n-1 by INT_2:2,Def2;
s <> 0 & s <> 1 by A7,A6,XXREAL_0:2;
then reconsider s as non trivial Divisor of n-1 by NAT_2:def 1;
A11: (3|^(k*2|^(l-1))) * (3|^(k*2|^(l-1))),(-1)*(-1) are_congruent_mod n
by A10,INT_1:18;
A12: (3|^(k*2|^(l-1))) * (3|^(k*2|^(l-1)))
= 3|^(k*2|^(l-1)+k*2|^(l-1)) by NEWTON:8
.= 3|^(k*(2|^(l-1)*2))
.= 3|^(k*(2|^(l-1+1))) by NEWTON:6
.= 3|^(k*2|^l);
A13: k * 2|^ l <= (2|^l - 1) * 2|^l by A1,XREAL_1:64;
A14: (2|^l - 1) * 2|^l + 1 = (2|^l) * (2|^l) - 2|^l + 1
.= 2|^(l+l) - 2|^l + 1 by NEWTON:8;
then n <= 2|^(l+l) - 2|^l + 1 by A13,XREAL_1:6; then
A15: n < 2|^(l+l) - 2|^l + 1 + 1 by A14,NAT_1:13;
A16: s > sqrt(n)
proof
per cases;
suppose l >= 2;
then A17: 2|^l >= 2|^2 by Th1;
2|^(1+1) = 2|^1 * 2 by NEWTON:6 .= 2 * 2;
then 2|^l > 2 by A17,XXREAL_0:2;
then 2 - 2|^l < 2|^l - 2|^l by XREAL_1:9;
then 2|^(l+l) + (-2|^l + 2) < 2|^(l+l) + 0 by XREAL_1:6;
then A18: n < 2|^(2*l) by A15,XXREAL_0:2;
(2|^l)^2 = 2|^(l+l) by NEWTON:8;
then sqrt(2|^(2*l)) = 2|^l by SQUARE_1:def 2;
hence thesis by A18,SQUARE_1:27;
end;
suppose l < 2;
then l < 1 + 1;
then l <= 1 by NAT_1:13;
then A19: l = 1 by A5,XXREAL_0:1; then
A20: n = k*2 + 1;
A21: k <= 2 - 1 by A1,A19;
k >= 1 by NAT_1:14;
then k = 1 by A21,XXREAL_0:1;
hence thesis by A20,SQUARE_1:27,SQUARE_1:20;
end;
end;
now let q be prime Divisor of s;
A22: a|^((n-1)/q), -1 are_congruent_mod n by A8,A10,Th8,INT_2:28,Def2;
1 * (a|^((n-1)/q) - 1) = a|^((n-1)/q) - 1; then
A23: 1 divides a|^((n-1)/q) - 1;
1 * n = n; then
A24: 1 divides n;
now let m be Integer;
assume A25: m divides a|^((n-1)/q) - 1 & m divides n;
then A26: a|^((n-1)/q), 1 are_congruent_mod m;
consider j being Integer such that
A27: m * j = n by A25;
a|^((n-1)/q), -1 are_congruent_mod m by A22,A27,INT_1:20;
then a|^((n-1)/q) - a|^((n-1)/q), (-1)- 1 are_congruent_mod m
by A26,INT_1:17;
then 0+1,(-2)+1 are_congruent_mod m;
then m = 2 or m = 1 or m = -2 or m = -1 by Th20,INT_1:14;
hence m divides 1 by A25,INT_2:10,ABIAN:def 1;
end;
hence a|^((n-1)/q) - 1 gcd n = 1 by A23,A24,INT_2:def 2;
end;
hence k * 2|^l + 1 is prime by A12,A11,A16,Th21;
end;
now assume n is prime;
then reconsider n as 2_greater Prime;
reconsider two = 2 as Prime by INT_2:28;
reconsider three = 3 as 2_greater Prime by Def1,PEPIN:41;
A28: 2|^l + 1 >= 2|^2 + 1 by XREAL_1:6,EC_PF_2:def 1;
2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2;
then A29: 3 <> n by A28,A2,XXREAL_0:2;
A30: not(n,0 are_congruent_mod 3) by A29,INT_2:def 4;
A31: now assume A32: n,1 are_congruent_mod 3;
not (three divides 2|^l) by Th8,INT_2:28;
then 3 gcd (2|^l) = 1 by Th6;
hence contradiction by A1,INT_2:25,A32,INT_2:def 3;
end;
n,0 are_congruent_mod 3 or ... or n,(3-1) are_congruent_mod 3 by Th13;
then A33: n,0 are_congruent_mod 3 or ... or n,2 are_congruent_mod 3;
A34: 2,2+1 are_coprime by PEPIN:1;
not(three divides n) by A29,INT_2:def 4;
then A35: n gcd 3 = 1 by Th6;
A36: ((3-1)/2) * ((n-1)/2) = 1 * ((n-1)/2);
(n-1)/2 = (k * 2|^((l-1)+1))/2
.= (k * (2|^(l-1) * 2))/2 by NEWTON:6
.= k * 2|^(l-2+1)
.= k * (2|^(l-2) * 2) by NEWTON:6
.= 2 * k * 2|^(l-2);
then A37: (-1)|^((n-1)/2) = 1;
Leg(three,n) * Leg(n,three) = 1 by A36,A37,A29,Th30;
then Leg(three,n) = 1 & Leg(n,three) = 1 or
Leg(three,n) = - 1 & Leg(n,three) = - 1 by INT_1:9;
then Leg(3,n) = Leg(two,three) by A35,A33,A30,A31,A34,Th28
.= -1 by Th23,A34,Def4;
hence 3|^(k*2|^(l-1)), -1 are_congruent_mod k* 2|^l + 1 by A8,A35,Th31;
end;
hence thesis by A9;
end;
theorem
641 is prime
proof
641 = 2 * 320 + 1; then
reconsider n = 641 as odd Nat;
A1: 256 + 64 = 320;
A2: 3 * 3 = 3|^1 * 3 .= 3|^1 * 3|^1
.= 3|^(1+1) by NEWTON:8;
A3: 3|^2 * 3|^2 = 3|^(2+2) by NEWTON:8;
A4: 3|^4 * 3|^4 = 3|^(4+4) by NEWTON:8;
6561 = 10 * 641 + 151;
then 3|^8, 151 are_congruent_mod 641 by A4,A3,A2;
then (3|^8) * (3|^8), 151 * 151 are_congruent_mod 641 by INT_1:18;
then A5: 3|^(8+8), 22801 are_congruent_mod 641 by NEWTON:8;
22801 = 35 * 641 + 366;
then 22801, 366 are_congruent_mod 641;
then 3|^16, 366 are_congruent_mod 641 by A5,INT_1:15;
then A6: (3|^16) * (3|^16), 366 * 366 are_congruent_mod 641 by INT_1:18;
A7: 183,183 are_congruent_mod 641 by INT_1:11;
732,91 are_congruent_mod 641;
then 732 * 183, 91 * 183 are_congruent_mod 641 by A7,INT_1:18;
then (3|^16) * (3|^16),91 * 183 are_congruent_mod 641 by A6,INT_1:15;
then A8: 3|^(16+16),91 * 183 are_congruent_mod 641 by NEWTON:8;
16653 = 26 * 641 + (-13);
then 16653,-13 are_congruent_mod 641;
then 3|^32, -13 are_congruent_mod 641 by A8,INT_1:15;
then (3|^32) * (3|^32), (-13) * (-13) are_congruent_mod 641 by INT_1:18;
then A9: 3 |^ (32+32), 169 are_congruent_mod 641 by NEWTON:8;
then A10: (3|^64) * (3|^64), 169 * 169 are_congruent_mod 641 by INT_1:18;
28561 = 44 * 641 + 357;
then 28561,357 are_congruent_mod 641;
then (3|^64) * (3|^64), 357 are_congruent_mod 641 by A10,INT_1:15;
then 3|^(64+64), 357 are_congruent_mod 641 by NEWTON:8;
then A11: (3|^128) * (3|^128), 357 * 357 are_congruent_mod 641 by INT_1:18;
A12: 119,119 are_congruent_mod 641 by INT_1:11;
1071,430 are_congruent_mod 641;
then 1071 * 119, 430 * 119 are_congruent_mod 641 by A12,INT_1:18;
then (3|^128) * (3|^128),430 * 119 are_congruent_mod 641 by A11,INT_1:15;
then A13: 3|^(128+128),3010 * 17 are_congruent_mod 641 by NEWTON:8;
A14: 17,17 are_congruent_mod 641 by INT_1:11;
3010 = 4 * 641 + 446;
then 3010,446 are_congruent_mod 641;
then 3010*17,446*17 are_congruent_mod 641 by A14,INT_1:18;
then A15: 3|^(128+128),446*17 are_congruent_mod 641 by A13,INT_1:15;
7582 = 12 * 641 + (-110);
then 7582,-110 are_congruent_mod 641;
then 3 |^ 256, -110 are_congruent_mod 641 by A15,INT_1:15;
then (3 |^ 256) * (3|^64), (-110) * 169 are_congruent_mod 641 by A9,INT_1:18;
then A16: 3 |^ 320, -18590 are_congruent_mod 641 by A1,NEWTON:8;
A17: -18590 = (-30) * 641 + 640;
A18: 640,-1 are_congruent_mod 641;
-18590,640 are_congruent_mod 641 by A17;
then -18590,-1 are_congruent_mod 641 by A18,INT_1:15; then
ex a being Nat st a|^((n-1)/2),-1 are_congruent_mod n by A16,INT_1:
15;
hence thesis by Th40,Th37;
end;
begin :: Fermat Numbers
registration
let l be Nat;
cluster Fermat l -> Proth;
coherence
proof
reconsider p = Fermat l as Nat;
set k = 1, n = 2|^l;
A3: 2|^n > n by NEWTON:86;
n + 1 > 0 + 1 by XREAL_1:6;
then n >= 1 by NAT_1:13; then
A1: 2|^n > k by A3,XXREAL_0:2;
A2: 2 * 0 + 1 = 1;
p = k * (2|^n) + 1 by PEPIN:def 3;
hence thesis by A1,A2;
end;
end;
::$N Pepin's theorem
theorem :: Pepin
for n being non zero Nat
holds Fermat n is prime iff
3|^((Fermat n - 1)/2), -1 are_congruent_mod Fermat n
proof
let l be non zero Nat;
set k = 1;
A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2;
l + 1 >= 0 + 1 by XREAL_1:6;
then l >= 1 by NAT_1:13;
then 2|^l >= 2|^1 by Th1;
then 2|^l >= 2;
then reconsider l1 = 2|^l as 2_or_greater Nat by EC_PF_2:def 1;
A2: not(3 divides k) by INT_2:27;
2|^l1 - 1 >= 4 - 1 by A1,XREAL_1:9,EC_PF_2:def 1;
then A3: 1 <= 2|^l1 - 1 by XXREAL_0:2;
A4: k * 2|^l1 + 1 = Fermat l by PEPIN:def 3;
(Fermat l - 1)/2 = (2 |^ (2 |^ l) + 1 - 1) / 2 by PEPIN:def 3
.= 2|^(l1-1+1) / 2
.= (2|^(l1 - 1) *2) / 2 by NEWTON:6
.= k * 2|^(l1-1);
hence thesis by A2,A3,A4,Th41;
end;
TT:
Fermat 5 is non prime & 641 divides Fermat 5
proof
A1: 2|^7 * 2|^7 = 2|^(7+7) by NEWTON:8;
A2: 5 * 5 = 5|^1 * 5 .= 5|^1 * 5|^1
.= 5|^(1+1) by NEWTON:8;
A3: 5|^2 * 5|^2 = 5|^(2+2) by NEWTON:8;
A4: 2|^14 * 2|^14 = 2|^(14+14) by NEWTON:8;
A5: 2|^4 * 2|^28 = 2|^(4+28) by NEWTON:8;
A6: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2;
A7: 2|^3 = 2|^(2+1) .= 2|^2 * 2 by NEWTON:6 .= 8 by A6;
A8: 2|^4 = 2|^(3+1) .= 2|^3 * 2 by NEWTON:6 .= 16 by A7;
A9: 2|^(3+4) = 8 * 16 by A8,A7,NEWTON:8;
5 * 2|^7, -1 are_congruent_mod 641 by A9;
then (5 * 2|^7) * (5 * 2|^7), (-1)*(-1) are_congruent_mod 641 by INT_1:18;
then A10: (5|^2*2|^14)*(5|^2*2|^14), 1*1 are_congruent_mod 641 by A1,A2,INT_1:
18;
(5|^4 + 2|^4) - 2|^4, 0 - 2|^4 are_congruent_mod 641 by A2,A3,A8;
then A11: -2|^4, 5|^4 are_congruent_mod 641 by INT_1:14;
2|^28, 2|^28 are_congruent_mod 641 by INT_1:11;
then (-2|^4) * 2|^28, 5|^4 * 2|^28 are_congruent_mod 641 by A11,INT_1:18;
then A12: -2|^32, 1 are_congruent_mod 641 by A3,A4,A5,A10,INT_1:15;
-1, -1 are_congruent_mod 641 by INT_1:11;
then A13: (-1) * (-2|^32), (-1) * 1 are_congruent_mod 641 by A12,INT_1:18;
A14: 5 * 2|^7 + 1 = 641 by A9;
2|^(4+1) = 16 * 2 by A8,NEWTON:6; then
A15: Fermat 5 = 2|^32 + 1 by PEPIN:def 3;
5 * 2|^7 < 2|^3 * 2|^7 by A7,XREAL_1:68;
then A16: 5 * 2|^7 < 2|^(3+7) by NEWTON:8;
2 is non trivial; then
2|^10 < 2|^32 by Th2;
then 5* 2|^7 < 2|^32 by A16,XXREAL_0:2;
then 641 < 2|^32 + 1 by A14,XREAL_1:6;
hence thesis by A15,A13;
end;
theorem
Fermat 5 is non prime by TT;
theorem
641 divides Fermat 5 by TT;
begin :: Cullen numbers
::$N Cullen numbers
definition
let n be Nat;
func CullenNumber n -> Nat equals
n * 2|^n + 1;
coherence;
end;
registration
let n be non zero Nat;
cluster CullenNumber n -> Proth;
coherence
proof
consider k being Nat,
l being odd Nat such that
A1: n = l * 2|^k by Th3;
A2: n * 2|^n + 1 = l* (2|^k * 2|^n) + 1 by A1
.= l * 2|^(k+n) + 1 by NEWTON:8;
2|^k + 1 > 0 + 1 by XREAL_1:6; then
2|^k >= 1 by NAT_1:13; then
A3: 2|^k * l >= 1 * l by XREAL_1:64;
A4: 2|^(k+n) > k+n by NEWTON:86;
k + n >= n by NAT_1:11;
then k + n >= l by A1,A3,XXREAL_0:2;
then 2|^(k+n) > l by A4,XXREAL_0:2;
hence thesis by A2;
end;
end;