:: Proth Numbers
:: by Christoph Schwarzweller
::
:: Received June 4, 2014
:: Copyright (c) 2014 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, 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, RELSET_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions NAT_1, NAT_2, NAT_D, INT_1, NEWTON, EC_PF_2, XREAL_0, XCMPLX_0,
ALGSTR_0, INT_3, INT_7;
equalities NEWTON, NAT_1, NAT_2, INT_1, INT_2, SQUARE_1;
expansions NEWTON, NAT_1, NAT_2, INT_1, INT_2, EC_PF_2, TARSKI, MEMBERED,
ABIAN, SQUARE_1, XCMPLX_0;
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;
schemes NAT_1;
begin :: Preliminaries
registration
let n be positive natural number;
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 natural number;
cluster n - 1 -> positive;
coherence
proof
n - 1 >= 2 - 1 by NAT_2:29,XREAL_1:9;
hence thesis;
end;
end;
registration
let x be integer number;
let n be natural number;
cluster x|^n -> integer;
coherence
proof
defpred P[Nat] means x|^($1) is integer;
A: P[0] by NEWTON:4;
B: now let k be Nat;
assume AS: P[k];
x|^(k+1) = x|^k * x by NEWTON:6;
hence P[k + 1] by AS;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A,B);
hence thesis;
end;
end;
red:
for n being natural number holds 1|^n = 1
proof
let n be natural number;
defpred P[Nat] means 1|^($1) = 1;
A: P[0] by NEWTON:4;
B: now let k be Nat;
assume AS: P[k];
1|^(k+1) = 1|^k * 1 by NEWTON:6;
hence P[k+1] by AS;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A,B);
hence thesis;
end;
registration
let n be natural number;
reduce 1|^n to 1;
reducibility by red;
end;
ev:
for n being even natural number holds (-1)|^n = 1
proof
let n be even natural number;
defpred P[Nat] means $1 is even implies (-1)|^($1) = 1;
A: now let k be Nat;
assume AS: for n being Nat st n < k holds P[n];
per cases;
suppose k is odd;
hence P[k];
end;
suppose S: k is even;
now per cases;
case k = 0;
hence P[k] by NEWTON:4;
end;
case B: k > 0;
0 is even & 0+1=1;
then k-2 in NAT by S,B,NAT_1:23,INT_1:5;
then reconsider k2 = k-2 as Nat;
H: k2 + 2 = k; then
E: k2 is even by S;
(-1)|^k = (-1)|^(k2+2)
.= ((-1)|^k2) * ((-1)|^2) by NEWTON:8
.= 1 * (-1)|^(1+1) by AS,E,H,NAT_1:16
.= (-1)|^1 * (-1) by NEWTON:6
.= (-1) * (-1) by NEWTON:5;
hence P[k];
end;
end;
hence P[k];
end;
end;
for k being Nat holds P[k] from NAT_1:sch 4(A);
hence thesis;
end;
registration
let n be even natural number;
reduce (-1)|^n to 1;
reducibility by ev;
end;
od:
for n being odd natural number holds (-1)|^n = -1
proof
let n be odd natural number;
defpred P[Nat] means $1 is odd implies (-1)|^($1) = -1;
A: now let k be Nat;
assume AS: for n being Nat st n < k holds P[n];
per cases;
suppose k is even;
hence P[k];
end;
suppose S: k is odd;
now per cases by NAT_1:23;
case k = 0;
hence P[k];
end;
case k = 1;
hence P[k] by NEWTON:5;
end;
case k >= 2;
then k-2 in NAT by INT_1:5;
then reconsider k2 = k-2 as Nat;
H: k2 + 2 = k; then
E: k2 is odd by S;
(-1)|^k = (-1)|^(k2+2)
.= ((-1)|^k2) * ((-1)|^2) by NEWTON:8
.= (-1) * (-1)|^(1+1) by AS,E,H,NAT_1:16
.= (-1) * (-1)|^1 * (-1) by NEWTON:6
.= (-1) * (-1) * (-1) by NEWTON:5;
hence P[k];
end;
end;
hence P[k];
end;
end;
for k being Nat holds P[k] from NAT_1:sch 4(A);
hence thesis;
end;
registration
let n be odd natural number;
reduce (-1)|^n to -1;
reducibility by od;
end;
theorem Th0:
for a being positive natural number,
n,m being natural number st n >= m holds a|^n >= a|^m
proof
let a be positive natural number;
let n,m be natural number;
assume n >= m;
then a|^m divides a|^n by NEWTON:89;
hence thesis by INT_2:27;
end;
theorem Th0a:
for a being non trivial natural number,
n,m being natural number st n > m holds a|^n > a|^m
proof
let a be non trivial natural number;
let n,m be natural number;
assume AS: n > m;
then consider k being Nat such that
H0: n = m + k by NAT_1:10;
k <> 0 by AS,H0;
then k + 1 > 0 + 1 by XREAL_1:6;
then k >= 1 by NAT_1:13;
then a|^k >= a|^1 by Th0;
then H6: a|^k >= a by NEWTON:5;
a >= 2 by NAT_2:29;
then a|^k >= 1 + 1 by H6,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 H0,NEWTON:8;
end;
theorem Thc:
for n being non zero natural number
ex k being natural number,
l being odd natural number st n = l * 2|^k
proof
let n be non zero natural number;
per cases;
suppose n is odd;
then reconsider l = n as odd natural number;
take k = 0, l;
thus l * 2|^k = l * 1 by NEWTON:4 .= n;
end;
suppose A: n is even;
defpred P[Nat] means 2|^($1) divides n;
A1: now let m be Nat;
assume P[m];
then 2|^m <= n by INT_2:27;
hence m <= n by NEWTON:86,XXREAL_0:2;
end;
2|^1 = 2 by NEWTON:5;
then A2: ex m being Nat st P[m] by A;
consider k being Nat such that
M: P[k] & for n being Nat st P[n] holds n <= k from NAT_1:sch 6(A1,A2);
consider l being Integer such that
H1: n = 2|^k * l by M,INT_1:def 3;
l >= 0 by H1;
then H2: l in NAT by INT_1:3;
now assume l is even;
then consider u being Integer such that
H3: l = 2 * u by INT_1:def 3;
n = 2|^k * 2 * u by H1,H3
.= 2|^(k+1) * u by NEWTON:6;
then 2|^(k+1) divides n;
hence contradiction by M,NAT_1:16;
end;
then reconsider l as odd natural number by H2;
take k,l;
thus thesis by H1;
end;
end;
theorem X1:
for n being even natural number holds n div 2 = n/2
proof
let n be even natural number;
consider k being Nat such that H: n = 2*k by ABIAN:def 2;
thus thesis by H,INT_1:25;
end;
theorem
for n being odd natural number holds n div 2 = (n-1)/2
proof
let n be odd natural number;
consider k being Integer such that H: n = 2*k+1 by ABIAN:1;
H0: (n-1)/2 = k by H;
(n-1)+1 = n; then
n-1 <= n by INT_1:6; then
H4: k <= n/2 by H0,XREAL_1:72;
(n/2) - (1/2) > (n/2) - 1 by XREAL_1:10;
hence thesis by H,H4,INT_1:def 6;
end;
registration
let n be even integer number;
cluster n/2 -> integer;
coherence
proof
consider k being Integer such that
A: n = 2 * k by ABIAN:def 1,INT_1:def 3;
thus thesis by A;
end;
end;
registration
let n be even natural number;
cluster n/2 -> natural;
coherence
proof
consider k being Integer such that
A: n = 2 * k by ABIAN:def 1,INT_1:def 3;
k >= 0 by A;
then k in NAT by INT_1:3; then
reconsider k as natural number;
n / 2 = k by A;
hence thesis;
end;
end;
begin :: Congruences and Prime Numbers
registration
cluster prime -> non trivial for natural number;
coherence;
end;
T4a:
for a being natural number,
b being integer number st a divides b holds a gcd b = a
proof
let a be natural number, b be integer number;
assume AS: a divides b;
for m being Integer st m divides a & m divides b holds m divides a;
hence thesis by AS,INT_2:def 2;
end;
theorem T4:
for p being prime natural number,
a being integer number holds a gcd p <> 1 iff p divides a
proof
let p be prime natural number,
a be integer number;
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 AS: p divides a;
p divides (a gcd p) by AS,INT_2:22;
hence a gcd p <> 1 by INT_2:27,INT_2:def 4;
end;
theorem THpr:
for i,j being integer number,
p being prime natural number
st p divides i * j holds p divides i or p divides j
proof
let i,j be integer number,
p be prime natural number;
assume A: p divides i * j;
assume not(p divides i);
then i gcd p = 1 by T4;
hence thesis by A,INT_2:25,INT_2:def 3;
end;
theorem T1:
for x,p being prime natural number,
k being non zero natural number holds x divides (p|^k) iff x = p
proof
let x,p be prime natural number;
let k be non zero natural number;
X: now assume AS: x divides (p|^k);
defpred P[Nat] means x divides p|^($1) implies x = p;
A: P[1]
proof
assume x divides p|^1;
then x divides p by NEWTON:5;
then x = 1 or x = p by INT_2:def 4;
hence x = p by NAT_2:def 1;
end;
B: now let k be non zero Nat;
assume A: P[k];
now assume B: x divides p|^(k+1);
C: p|^(k+1) = p * p|^k by NEWTON:6;
per cases by INT_2:30;
suppose x,p are_coprime;
hence x = p by A,B,C,INT_2:25;
end;
suppose x = p;
hence x = p;
end;
end;
hence P[k + 1];
end;
I: for k being non zero Nat holds P[k] from NAT_1:sch 10(A,B);
thus x = p by I,AS;
end;
now assume AS: x = p;
reconsider k1 = k-1 as natural number;
p * p|^k1 = p|^(k1+1) by NEWTON:6;
hence x divides (p|^k) by AS;
end;
hence thesis by X;
end;
theorem eul1:
for x,y,n being integer number
holds x,y are_congruent_mod n iff ex k being Integer st x = k * n + y
proof
let x,y,n be integer number;
now assume x,y are_congruent_mod n;
then consider k being integer Number such that
H: n * k = x - y;
x = n * k + y by H;
hence ex k being Integer st x = k * n + y;
end;
hence thesis;
end;
theorem T1d:
for i being integer number,
j being non zero integer number holds i, i mod j are_congruent_mod j
proof
let i be integer number;
let j be non zero integer number;
i = (i div j) * j + (i mod j) by INT_1:59;
hence i, i mod j are_congruent_mod j;
end;
theorem
for x,y being integer number,
n being positive integer number
holds x,y are_congruent_mod n iff x mod n = y mod n
proof
let x,y be integer number,
n being positive integer number;
A: now assume x,y are_congruent_mod n;
then consider k being Integer such that H: x = k * n + y by eul1;
thus x mod n = y mod n by H,EULER_1:12;
end;
now assume B: x mod n = y mod n;
C: x,x mod n are_congruent_mod n by T1d;
y mod n, y are_congruent_mod n by T1d,INT_1:14;
hence x,y are_congruent_mod n by B,C,INT_1:15;
end;
hence thesis by A;
end;
theorem T1c:
for i,j being integer number,
n being natural number
st n < j & i,n are_congruent_mod j holds i mod j = n
proof
let i,j be integer number,
n be natural number;
assume AS: n < j & i,n are_congruent_mod j;
then consider x being Integer such that
H1: j * x = i - n;
H3: i = (i div j) * j + (i mod j) by AS,INT_1:59;
H0: j in NAT by AS,INT_1:3;
per cases;
suppose n = 0;
hence i mod j = n by H0,AS,INT_1:62;
end;
suppose A: n <> 0;
H8: i/j = (j*x+n) * j" by H1,XCMPLX_0:def 9
.= x * (j * j") + n * j"
.= x * 1 + n * j" by AS,XCMPLX_0:def 7;
then H4: x <= i/j by A,AS,XREAL_1:29;
H9: i/j - 1 = x + (n*j" - 1) by H8;
H10: n/j < j/j by AS,XREAL_1:74;
j/j = j*j" by XCMPLX_0:def 9 .= 1 by AS,XCMPLX_0:def 7;
then n*j" < 1 by H10,XCMPLX_0:def 9;
then n*j" - 1 < 1 - 1 by XREAL_1:9;
then i/j - 1 < x by H9,XREAL_1:30;
then i div j = x by H4,INT_1:def 6;
hence i mod j = n by H1,H3;
end;
end;
theorem XXX:
for n being non zero natural number, x being integer number
holds x,0 are_congruent_mod n or ... or x,(n-1) are_congruent_mod n
proof
let n be non zero natural number, x be integer number;
x mod n in NAT by INT_1:3,INT_1:57;
then reconsider j = x mod n as Nat;
(x mod n) + 1 <= n by INT_1:7,INT_1:58;
then C: (x mod n) + 1 - 1 <= n - 1 by XREAL_1:9;
take j; thus thesis by T1d,C;
end;
theorem XXX1:
for n being non zero natural number,
x being integer number,
k,l being natural number
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 natural number,
x be integer number,
k,l be natural number;
assume AS: k < n & l < n &
x,k are_congruent_mod n & x,l are_congruent_mod n;
hence k = x mod n by T1c .= l by AS,T1c;
end;
theorem XXZ:
for x being integer number
holds x|^2, 0 are_congruent_mod 3 or x|^2, 1 are_congruent_mod 3
proof
let x be integer number;
x,0 are_congruent_mod 3 or ... or x,(3-1) are_congruent_mod 3 by XXX;
then H:
x,0 are_congruent_mod 3 or ... or x,2 are_congruent_mod 3;
per cases by H;
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 lemT1b:
for p being prime natural number,
x,y being Element of Z/Z*(p),
i,j being integer number
st x = i & y = j holds x * y = (i * j) mod p
proof
let p be prime natural number,
x,y be Element of Z/Z*(p), i,j be integer number;
assume AS: 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,AS,INT_3:def 10;
end;
theorem T1b:
for p being prime natural number,
x being Element of Z/Z*(p),
i being integer number,
n being natural number
st x = i holds x |^ n = (i |^ n) mod p
proof
let p be prime natural number,
x be Element of Z/Z*(p), i be integer number,
n be natural number;
assume AS: x = i;
A4: 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 A0: i in Segm(p) by A4,AS,XBOOLE_0:def 5;
reconsider i as Element of NAT by AS,A4,INT_1:3;
defpred P[Nat] means
x |^ ($1) = (i |^ ($1)) mod p;
A1: x|^0 = 1_(Z/Z*(p)) by GROUP_1:25;
1 < p by INT_2:def 4;
then A2: 1 div p <= 1-1 by INT_1:56,INT_1:52;
A3: 1 div p = 0 by A2;
i|^0 = 1 by NEWTON:4;
then (i |^ 0) mod p = 1 - (1 div p) * p by INT_1:def 10;
then A: P[0] by A1,A3,INT_7:21;
B: now let k be Nat;
assume B1: P[k];
x |^ (k+1) = x|^k * x by GROUP_1:34
.= ((i |^ k mod p) * i) mod p by AS,B1,lemT1b
.= ((i |^ k mod p) * (i mod p)) mod p by A0,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;
I: for k being Nat holds P[k] from NAT_1:sch 2(A,B);
thus thesis by I;
end;
theorem T1a:
for p being prime natural number,
x being integer number
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 natural number,
x be integer number;
A: now assume x|^2, 1 are_congruent_mod p;
then p divides (x^2 - 1^2) by NEWTON:81;
then A: p divides (x+1) * (x-1);
now per cases by A,THpr;
case p divides x+1;
then consider l being Integer such that
H0: p * l = x + 1;
thus x,-1 are_congruent_mod p by H0;
end;
case p divides x-1;
then consider l being Integer such that
H0: p * l = x - 1;
thus x,1 are_congruent_mod p by H0;
end;
end;
hence x,1 are_congruent_mod p or x,-1 are_congruent_mod p;
end;
now assume AS: x,1 are_congruent_mod p or x,-1 are_congruent_mod p;
now per cases by AS;
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 A;
end;
theorem T2:
for n being natural number holds
-1,1 are_congruent_mod n iff (n = 2 or n = 1)
proof
let n be natural number;
hereby assume -1,1 are_congruent_mod n;
then consider k being Integer such that H: n * k = -2;
k < 0 & n <> 0 by H;
then C: k <= -1 by INT_1:8;
now assume A: n <> 2;
now assume n <> 1;
then not(n=0 or ... or n = 2) by H,A;
then not(n <= 2);
then n >= 2+1 by NAT_1:13;
then n >= 3 & k < 0 by H;
then I: n * k <= 3 * k by XREAL_1:65;
3 * k <= 3 * (-1) by C,XREAL_1:64;
hence contradiction by H,I,XXREAL_0:2;
end;
hence n = 1;
end;
hence n = 2 or n = 1;
end;
assume A: n = 2 or n = 1;
per cases by A;
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 T2a:
for i being integer Number
holds -1,1 are_congruent_mod i iff (i = 2 or i = 1 or i = -2 or i = -1)
proof
let n be integer Number;
hereby assume AS: -1,1 are_congruent_mod n;
then consider k being Integer such that H: n * k = -2;
now per cases;
case n >= 0;
then n in NAT by INT_1:3;
then reconsider m = n as natural number;
m = 1 or m = 2 by AS,T2;
hence n = 2 or n = 1 or n = -2 or n = -1;
end;
case X: n < 0;
then Y: k > 0 by H;
then Y1: k >= 0 + 1 by INT_1:7;
now assume A: n <> -2;
now assume A1: n <> -1;
n <= -1 by X,INT_1:8;
then n < -1 by A1,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 A,XXREAL_0:1;
then n + 1 <= -2 by INT_1:7;
then n + 1 - 1 <= -2 - 1 by XREAL_1:9;
then I: n * k <= (-3) * k by Y,XREAL_1:64;
(-3) * k <= (-3) * 1 by Y1,XREAL_1:65;
hence contradiction by H,I,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 A: n = 2 or n = 1 or n = -2 or n = -1;
per cases by A;
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 natural number;
attr x is n_greater means :Defg2:
x > n;
end;
notation
let n,x be natural number;
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 natural number;
cluster n_greater odd for natural number;
existence
proof
per cases;
suppose n is even; then
consider k being Nat such that
H: 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 H;
end;
suppose n is odd;
then consider k being Integer such that
H: 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 H;
end;
end;
cluster n_greater even for natural number;
existence
proof
per cases;
suppose n is odd;
then consider k being Integer such that
H: 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 H;
end;
suppose n is even;
then consider k being Nat such that
H: 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 H;
end;
end;
end;
registration
let n be natural number;
cluster n_greater -> n_or_greater for natural number;
coherence;
end;
registration
let n be natural number;
cluster (n+1)_or_greater -> n_or_greater for natural number;
coherence
proof
let x be natural number;
assume H: x is (n+1)_or_greater;
n+1 >= n+0 by XREAL_1:6;
hence x is n_or_greater by H,XXREAL_0:2;
end;
cluster (n+1)_greater -> n_greater for natural number;
coherence
proof
let x be natural number;
assume H: x is (n+1)_greater;
n+1 > n+0 by XREAL_1:6;
hence x is n_greater by H,XXREAL_0:2;
end;
cluster n_greater -> (n+1)_or_greater for natural number;
coherence by NAT_1:13;
end;
registration
let m be non trivial natural number;
cluster m_or_greater-> non trivial for natural number;
coherence
proof
let n be natural number;
assume A: n is m_or_greater;
m >= 2 by NAT_2:29;
hence thesis by A,XXREAL_0:2;
end;
end;
registration
let a be positive natural number;
let m be natural number;
let n be m_or_greater natural number;
cluster a|^n -> (a|^m)_or_greater;
coherence by Th0,EC_PF_2:def 1;
end;
registration
let a be non trivial natural number;
let m be natural number;
let n be m_greater natural number;
cluster a|^n -> (a|^m)_greater;
coherence by Defg2,Th0a;
end;
registration
cluster 2_or_greater -> non trivial for natural number;
coherence;
cluster non trivial -> 2_or_greater for natural number;
coherence
proof
let n be natural number;
assume A: n is non trivial;
n <= 1 implies n = 0 or ... or n = 1;
then n >= 1 + 1 by A,NAT_1:13;
hence thesis;
end;
cluster non trivial odd -> 2_greater for natural number;
coherence
proof
let n be natural number;
assume A: n is non trivial odd;
n <= 2 implies n = 0 or ... or n = 2;
hence thesis by A;
end;
end;
registration
let n be 2_greater natural number;
cluster n - 1 -> non trivial;
coherence
proof
n - 1 > 2 - 1 by Defg2,XREAL_1:9;
hence thesis by NAT_2:def 1;
end;
end;
registration
let n be 2_or_greater natural number;
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 natural number;
let n be m_or_greater natural number;
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 natural number;
coherence by INT_2:def 4;
end;
registration
let n be natural number;
cluster n_greater prime for natural number;
existence
proof
now assume A: not(ex p being natural number st p is n_greater prime);
B: now let p be prime natural number;
not(p is n_greater) by A;
hence p < n+1 by NAT_1:13;
end;
C: now let p be set;
assume C0: p in SetPrimes;
then reconsider p1 = p as Element of NAT;
C1: p1 is prime by C0,NEWTON:def 6;
then p1 < n+1 by B;
hence p in SetPrimenumber(n+1) by C1,NEWTON:def 7;
end;
now let p be set;
assume D: p in SetPrimenumber(n+1);
reconsider n1 = n + 1 as Nat;
SetPrimenumber(n1) c= SetPrimes by NEWTON:68;
hence p in SetPrimes by D;
end;
then SetPrimes = SetPrimenumber(n+1) by C;
hence contradiction;
end;
hence thesis;
end;
end;
begin :: Pocklington's theorem revisited
definition
let n be natural number;
mode Divisor of n -> natural number means :Def1:
it divides n;
existence;
end;
registration
let n be non trivial natural number;
cluster non trivial for Divisor of n;
existence
proof
reconsider m = n as Divisor of n by Def1;
take m;
thus thesis;
end;
end;
registration
let n be non zero natural number;
cluster -> non zero for Divisor of n;
coherence
proof
let x be Divisor of n;
consider k being Integer such that H: x * k = n by Def1,INT_1:def 3;
thus thesis by H;
end;
end;
registration
let n be positive natural number;
cluster -> positive for Divisor of n;
coherence;
end;
registration
let n be non zero natural number;
cluster -> n_or_smaller for Divisor of n;
coherence
proof
let x be Divisor of n;
consider k being Integer such that H: x * k = n by Def1,INT_1:def 3;
k >= 0 by H;
then reconsider k as Element of NAT by INT_1:3;
k <> 0 by H;
hence thesis by H,NAT_1:24;
end;
end;
registration let n be non trivial natural number;
cluster prime for Divisor of n;
existence
proof
consider p being Element of NAT such that
H: p is prime & p divides n by NAT_2:29,INT_2:31;
reconsider p as natural number;
take p;
thus thesis by H,Def1;
end;
end;
registration
let n be natural number;
let q be Divisor of n;
cluster n / q -> natural;
coherence
proof
per cases;
suppose n = 0;
hence thesis;
end;
suppose AS: n <> 0;
consider k being Integer such that H: q * k = n by Def1,INT_1:def 3;
0 <= k by H,AS;
then A: k in NAT by INT_1:3;
n/q = (q * k) * q" by H,XCMPLX_0:def 9
.= k * (q * q")
.= k * 1 by AS,XCMPLX_0:def 7;
hence thesis by A;
end;
end;
end;
registration
let n be natural number;
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 AS: n <> 0;
consider k being Integer such that H1: s * k = n by Def1,INT_1:def 3;
consider l being Integer such that H2: q * l = s by Def1,INT_1:def 3;
0 <= k by H1,AS;
then A1: k in NAT by INT_1:3;
0 <= l by H2,AS;
then A2: l in NAT by INT_1:3;
n/q = ((q * l) * k) * q" by H2,H1,XCMPLX_0:def 9
.= l * k * (q * q")
.= l * k * 1 by AS,XCMPLX_0:def 7;
hence thesis by A1,A2;
end;
end;
end;
::$N Pocklington's theorem
theorem Pock:
for n being 2_greater natural number,
s being non trivial Divisor of n - 1 st s > sqrt(n) &
ex a being natural number
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 natural number;
let s be non trivial Divisor of n - 1;
assume AS: s > sqrt(n) &
ex a being natural number
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 Defg2; then
H0: m >= 1 by NAT_1:13;
consider c being Integer such that A: m-1 = f * c by Def1,INT_1:def 3;
A1: sqrt n >= 0 by SQUARE_1:def 2;
B: now assume s <= c;
then c >= sqrt(n) by AS,XXREAL_0:2;
then s * c >= (sqrt(n))^2 by A1,AS,XREAL_1:66;
then s * c >= n by SQUARE_1:def 2;
then n - 1 - n >= n - n by A,XREAL_1:9;
then -1 >= 0;
hence contradiction;
end;
c > 0 by A;
then reconsider c as Element of NAT by INT_1:3;
D: m-1 = f*c & f > c & c > 0 by A,B;
now let p be Element of NAT;
assume E1: p divides f & p is prime;
reconsider q = p as natural number;
reconsider q as Divisor of s by E1,Def1;
reconsider q as prime Divisor of s by E1;
consider b being natural number such that
E2: 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 AS;
reconsider a = b as Element of NAT by ORDINAL1:def 12;
consider k1 being Integer such that H1: q * k1 = s by Def1,INT_1:def 3;
consider k2 being Integer such that H2: s * k2 = n-1 by Def1,INT_1:def 3;
consider l1 being Integer such that H3: p * l1 = f by E1;
H5: k2 = c by A,H2,XCMPLX_1:5;
X: (m-1)/p = (p * l1 * c) * p" by A,H3,XCMPLX_0:def 9
.= (l1 * c) * ( p * p")
.= (l1 * c) * 1 by E1,XCMPLX_0:def 7;
Z: n-1 >= 2-1 by Defg2,XREAL_1:9;
now assume a = 0;
then a |^ (n-1) = 0 by Z,NEWTON:11;
then n = 1 or n = -1 by E2,INT_2:13;
hence contradiction by Defg2;
end;
then a|^((m-'1) div p) + 1 > 0 + 1 by XREAL_1:6;
then Z: a|^((m-'1) div p) >= 1 by NAT_1:13;
(n-1)/q = ((q*k1)*k2) * q" by H1,H2,XCMPLX_0:def 9
.= (k1 * k2) * (q * q")
.= k1 * k2 * 1 by XCMPLX_0:def 7
.= (m-1)/p by H1,H3,H5,X,XCMPLX_1:5
.= [/ (m-1)/p \] by X,INT_1:30
.= [\ (m-1)/p /] by X,INT_1:34
.= (m-'1) div p by H0,XREAL_1:233; then
a|^((m-'1) div p)-'1 = b|^((n-1)/q) - 1 by Z,XREAL_1:233; then
E4: (a|^((m-'1) div p)-'1) gcd m = 1 by E2;
consider x being Integer such that
F1: n * x = a|^(n-1) - 1 by E2;
F6: a|^(n-1) / n = (n*x+1) * n" by F1,XCMPLX_0:def 9
.= n"*n*x + 1 *n"
.= 1 * x + n" by XCMPLX_0:def 7;
F5: x <= a|^(n-1)/n by F6,XREAL_1:29;
F7: a|^(n-1)/n - 1 = x + (n" - 1) by F6;
2 < n by Defg2;
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 F7,XREAL_1:30;
then a|^(n-1) div n = x by F5,INT_1:def 6;
then F2: a|^(n-1) mod n = a|^(n-1) - n * x by INT_1:def 10
.= 1 by F1;
a|^(m-'1) mod m = 1 by F2,H0,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 E4;
end;
hence thesis by D,NAT_4:24;
end;
begin :: Euler's criterion
notation
let a be integer number, p be natural number;
antonym a is_quadratic_non_residue_mod p for a is_quadratic_residue_mod p;
end;
theorem eul3:
for p being positive natural number,
a being integer number holds
a is_quadratic_residue_mod p iff
ex x being integer number st x|^2, a are_congruent_mod p
proof
let p be positive natural number,
a be integer number;
thus a is_quadratic_residue_mod p implies
ex x being integer number st x|^2, a are_congruent_mod p
proof assume a is_quadratic_residue_mod p;
then consider x being Integer such that
H: (x^2 - a) mod p = 0 by INT_5:def 2;
b: x^2 - a = ((x^2 - a) div p) * p + 0 by H,INT_1:59;
reconsider xx = x as integer number by TARSKI:1;
take xx;
xx^2 = xx|^2 by NEWTON:81;
hence thesis by b;
end;
assume ex x being integer number st x|^2, a are_congruent_mod p;
then consider x being integer number such that
H: x|^2, a are_congruent_mod p;
x^2 = x|^1 * x by NEWTON:5 .= x|^(1+1) by NEWTON:6;
then (x^2 - a) mod p = 0 by H,INT_1:62;
hence a is_quadratic_residue_mod p by INT_5:def 2;
end;
theorem qua0:
2 is_quadratic_non_residue_mod 3
proof
now assume ex x being integer number st x|^2, 2 are_congruent_mod 3;
then consider x being integer number such that
H: x|^2,2 are_congruent_mod 3;
now per cases by XXZ;
case x|^2, 0 are_congruent_mod 3;
hence contradiction by H,XXX1;
end;
case x|^2, 1 are_congruent_mod 3;
hence contradiction by H,XXX1;
end;
end;
hence contradiction;
end;
hence thesis by eul3;
end;
::$N Legendre symbol
definition
let p be natural number;
let a be integer number;
func LegendreSymbol(a,p) -> integer Number equals :defleg:
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 T4a;
end;
definition
let p be prime natural number;
let a be integer number;
redefine func LegendreSymbol(a,p) equals :deflegpr:
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
A: a gcd p = 1 & a is_quadratic_residue_mod p & p divides a implies
for z being integer number holds z = 1 iff z = 0
proof
assume A1: a gcd p = 1 & a is_quadratic_residue_mod p & p divides a;
then a gcd p = p by T4a;
hence thesis by A1,INT_2:def 4;
end;
a gcd p = 1 & a is_quadratic_non_residue_mod p & p divides a implies
for z being integer number holds z = -1 iff z = 0
proof
assume A1: a gcd p = 1 & a is_quadratic_non_residue_mod p & p divides a;
then a gcd p = p by T4a;
hence thesis by A1,INT_2:def 4;
end;
hence thesis by A;
end;
compatibility
proof
p <> 1 by INT_2:def 4;
hence thesis by defleg;
end;
end;
notation
let p be natural number;
let a be integer number;
synonym Leg(a,p) for LegendreSymbol(a,p);
end;
theorem leg00:
for p be prime natural number,
a be integer number
holds Leg(a,p) = 1 or Leg(a,p) = 0 or Leg(a,p) = -1
proof
let p be prime natural number;
let a be integer number;
assume AS: 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 AS,deflegpr,INT_2:21;
end;
hence Leg(a,p) = -1 by AS,deflegpr;
end;
theorem leg0a:
for p being prime natural number,
a being integer number 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 natural number,
a be integer number;
A:now assume H0: Leg(a,p) = 0;
now assume not p divides a;
then a gcd p = 1 by T4;
hence contradiction by H0,deflegpr;
end;
hence p divides a;
end;
now assume H0: Leg(a,p) = 1;
then a gcd p = 1 by T4,deflegpr;
hence a gcd p = 1 & a is_quadratic_residue_mod p by H0,deflegpr;
end;
hence Leg(a,p) = 1 iff a gcd p = 1 & a is_quadratic_residue_mod p by deflegpr;
now assume H0: Leg(a,p) = -1;
then a gcd p = 1 by T4,deflegpr;
hence a gcd p = 1 & a is_quadratic_non_residue_mod p by H0,deflegpr;
end;
hence thesis by A,deflegpr;
end;
theorem
for p being natural number holds Leg(p,p) = 0 by defleg;
theorem
for a being integer number holds Leg(a,2) = a mod 2
proof
let a be integer number;
per cases;
suppose A: a is even;
then a mod 2 = 0 by INT_1:62;
hence thesis by A,defleg;
end;
suppose X: a is odd;
reconsider amod2 = a mod 2 as Element of NAT by INT_1:3,INT_1:57;
C: amod2 = 0 or amod2 = 1 by NAT_1:23,INT_1:58;
a - 1 = (a div 2) * 2 + 1 - 1 by C,X,INT_1:62,INT_1:59;
then E: 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 G: a gcd 2 = 0 or ... or a gcd 2 = 2;
1|^(1+1) = 1;
hence thesis by E,INT_2:5,G,INT_2:21,C,X,INT_1:62,defleg,eul3;
end;
end;
thLege:
for a be integer number, p be prime natural number holds Lege(a,p) = Leg(a,p)
proof
let a be integer number, p be prime natural number;
per cases by leg00;
suppose A: Leg(a,p) = 1;
then not(p divides a) by leg0a;
then a mod p <> 0 by INT_1:62;
hence thesis by A,INT_5:def 3,leg0a;
end;
suppose A: Leg(a,p) = 0;
then C: p divides a by leg0a;
p divides (-a) by A,leg0a,INT_2:10;
then B: (0^2 - a) mod p = 0 by INT_1:62;
a mod p = 0 by C,INT_1:62;
hence thesis by A,B,INT_5:def 3,INT_5:def 2;
end;
suppose Leg(a,p) = -1;
hence thesis by leg0a,INT_5:def 3;
end;
end;
theorem leg1:
for p being 2_greater prime natural number,
a,b being integer number
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 natural number,
a,b be integer number;
assume AS: a gcd p = 1 & b gcd p = 1 & a,b are_congruent_mod p;
thus Leg(a,p) = Lege(a,p) by thLege .= Lege(b,p) by Defg2,AS,INT_5:29
.= Leg(b,p) by thLege;
end;
theorem
for p being 2_greater prime natural number,
a,b being integer number
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 natural number,
a,b be integer number;
assume AS: a gcd p = 1 & b gcd p = 1;
thus Leg(a*b,p) = Lege(a*b,p) by thLege
.= Lege(a,p) * Lege(b,p) by AS,Defg2,INT_5:30
.= Leg(a,p) * Lege(b,p) by thLege
.= Leg(a,p) * Leg(b,p) by thLege;
end;
theorem leg3:
for p,q being 2_greater prime natural number
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 natural number;
assume AS: p <> q;
A: p > 2 & q > 2 by Defg2;
p - 1 > 2 - 1 by Defg2,XREAL_1:9;
then p -' 1 = p - 1 by NAT_D:39;
then C: (p-'1) div 2 = (p-1)/2 by X1;
q - 1 > 2 - 1 by Defg2,XREAL_1:9;
then q -' 1 = q - 1 by NAT_D:39; then
B: (-1)|^(((p-'1) div 2)*((q-'1) div 2))
= (-1)|^( ((p-1)/2) * ((q-1)/2) ) by C,X1;
thus Leg(p,q) * Leg(q,p) = Leg(p,q) * Lege(q,p) by thLege
.= Lege(p,q) * Lege(q,p) by thLege
.= (-1)|^( ((p-1)/2) * ((q-1)/2) ) by AS,A,B,INT_5:49;
end;
::$N Euler's criterion
theorem euler:
for p being 2_greater prime natural number,
a being integer number
st a gcd p = 1
holds a|^((p-1)/2), LegendreSymbol(a,p) are_congruent_mod p
proof
let p be 2_greater prime natural number,
a be integer number;
p - 1 > 2 - 1 by Defg2,XREAL_1:9;
then C: 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 Defg2,INT_5:28;
then B: Lege (a,p),a|^((p-1)/2) are_congruent_mod p by C,X1;
Leg(a,p) = Lege(a,p) by thLege;
hence thesis by B,INT_1:14;
end;
begin :: Proth Numbers
::$N Proth numbers
definition
let p be natural number;
attr p is Proth means :defPr:
ex k being odd natural number,
n being positive natural number
st 2|^n > k & p = k * (2|^n) + 1;
end;
Lm0: 1 is odd
proof
1 = 2 * 0 + 1;
hence thesis;
end;
Lm1: 3 is Proth
proof
H: 2|^1 = 2 by NEWTON:5;
reconsider e = 1 as odd natural number by Lm0;
take e,1;
thus thesis by H;
end;
Lm1a: 9 is Proth
proof
H1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2 by NEWTON:5;
H: 2|^3 = 2|^(2+1) .= 4 * 2 by H1,NEWTON:6;
reconsider e = 1 as odd natural number by Lm0;
take e,3;
thus thesis by H;
end;
registration
cluster Proth prime for natural number;
existence by Lm1,PEPIN:41;
cluster Proth non prime for natural number;
existence
proof
3 * 3 = 9;
then 3 divides 9;
then 9 is non prime;
hence thesis by Lm1a;
end;
end;
registration
cluster Proth -> non trivial odd for natural number;
coherence
proof
let p be natural number;
assume AS: p is Proth; then
consider k being odd natural number,
n being positive natural number such that
H: 2|^n > k & p = k * 2|^n + 1;
thus p is non trivial by AS,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 H;
end;
end;
theorem
3 is Proth by Lm1;
theorem
5 is Proth
proof
H: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2 by NEWTON:5;
reconsider e = 1 as odd natural number by Lm0;
take e,2;
thus thesis by H;
end;
theorem
9 is Proth by Lm1a;
theorem
13 is Proth
proof
H: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2 by NEWTON:5;
3 = 2 * 1 + 1; then
reconsider e = 3 as odd natural number;
take e,2;
thus thesis by H;
end;
theorem
17 is Proth
proof
H1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2 by NEWTON:5;
H2: 2|^3 = 2|^(2+1) .= 2|^2 * 2 by NEWTON:6 .= 8 by H1;
H: 2|^4 = 2|^(3+1) .= 2|^3 * 2 by NEWTON:6 .= 16 by H2;
reconsider e = 1 as odd natural number by Lm0;
take e,4;
thus thesis by H;
end;
theorem P641:
641 is Proth
proof
H1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2 by NEWTON:5; then
2|^(2+2) = 4 * 4 by NEWTON:8; then
H3: 2|^(4+2) = 16 * 4 by H1,NEWTON:8;
H4: 2|^(6+1) = 2|^6 * 2|^1 by NEWTON:8 .= 64 * 2 by H3,NEWTON:5;
B: 5 = 2 * 2 + 1;
641 = 5 * 2|^7 + 1 by H4;
hence thesis by H4,B;
end;
theorem
11777 is Proth
proof
H1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2 by NEWTON:5;
H2: 2|^(2+2) = 4 * 4 by H1,NEWTON:8;
H3: 2|^(4+4) = 16 * 16 by H2,NEWTON:8;
H4: 2|^(8+1) = 2|^8 * 2|^1 by NEWTON:8 .= 256 * 2 by H3,NEWTON:5;
B: 23 = 2 * 11 + 1;
11777 = 23 * 2|^9 + 1 by H4;
hence thesis by H4,B;
end;
theorem
13313 is Proth
proof
H1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2 by NEWTON:5; then
2|^(2+2) = 4 * 4 by NEWTON:8; then
2|^(4+4) = 16 * 16 by NEWTON:8; then
H4: 2|^(8+2) = 256 * 4 by H1,NEWTON:8;
B: 13 = 2 * 6 + 1;
13313 = 13 * 2|^10 + 1 by H4;
hence thesis by H4,B;
end;
::$N Proth's theorem - version 1
theorem Proth1: :: Proth
for n being Proth natural number holds
n is prime iff
ex a being natural number st a|^((n-1)/2), -1 are_congruent_mod n
proof
let n be Proth natural number;
consider k being odd natural number,
l being positive natural number such that
P: 2|^l > k & n = k * (2|^l) + 1 by defPr;
set s = 2|^l;
P2: 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 P2,XXREAL_0:2;
then reconsider s as non trivial natural number by NAT_2:def 1;
reconsider s as non trivial Divisor of n-1 by P,INT_1:def 3,Def1;
A: now assume ex a being natural number
st a |^ ((n-1) / 2), -1 are_congruent_mod n;
then consider a being natural number such that
H1: a |^ ((n-1) / 2), -1 are_congruent_mod n;
H2: (a |^ ((n-1) / 2)) * (a |^ ((n-1) / 2))
= a |^ ( ((n-1) / 2) + ((n-1) / 2) ) by NEWTON:8
.= a|^(n-1);
B: (-1) * (-1) = 1;
H1a: l >= 1 by NAT_1:14;
(2|^l - 1) + 1 > k by P; then
H1b: k <= 2|^l - 1 by NAT_1:13;
then k * 2|^ l <= (2|^l - 1) * 2|^l by XREAL_1:64;
then C2: n <= (2|^l - 1) * 2|^l + 1 by P,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 C4: n < 2|^(l+l) - 2|^l + 1 + 1 by C2,NAT_1:13;
C: s > sqrt(n)
proof
per cases;
suppose l >= 2;
then U: 2|^l >= 2|^2 by Th0;
2|^(1+1) = 2|^1 * 2 by NEWTON:6 .= 2 * 2 by NEWTON:5;
then 2|^l > 2 by U,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 C1: n < 2|^(2*l) by C4,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 C1,SQUARE_1:27;
end;
suppose l < 2;
then l < 1 + 1;
then K1: l <= 1 by NAT_1:13;
then K: l = 1 by H1a,XXREAL_0:1;
then La: s = sqrt 4 by NEWTON:5,SQUARE_1:20;
M: n = k*2|^1 + 1 by K1,P,H1a,XXREAL_0:1 .= k*2 + 1 by NEWTON:5;
O: k <= 2 - 1 by H1b,K,NEWTON:5;
k >= 1 by NAT_1:14;
then k = 1 by O,XXREAL_0:1;
hence thesis by M,La,SQUARE_1:27;
end;
end;
now let q be prime Divisor of s;
B1: a|^((n-1)/q), -1 are_congruent_mod n by H1,T1,INT_2:28,Def1;
1 * (a|^((n-1)/q) - 1) = a|^((n-1)/q) - 1; then
C: 1 divides a|^((n-1)/q) - 1;
1 * n = n; then
D: 1 divides n;
now let m be Integer;
assume AS1: m divides a|^((n-1)/q) - 1 & m divides n;
then E: a|^((n-1)/q), 1 are_congruent_mod m;
consider j being Integer such that
H: m * j = n by AS1;
a|^((n-1)/q), -1 are_congruent_mod m by B1,H,INT_1:20;
then a|^((n-1)/q) - a|^((n-1)/q), (-1)- 1 are_congruent_mod m
by E,INT_1:17;
then 0+1,(-2)+1 are_congruent_mod m; then
K: m = 2 or m = 1 or m = -2 or m = -1 by T2a,INT_1:14;
L: now assume (-2) divides n;
then consider g being Integer such that
H: n = (-2) * g;
n = 2 * (-g) by H;
hence contradiction;
end;
1 * 1 = 1 & (-1) * (-1) = 1;
hence m divides 1 by L,AS1,K;
end;
hence a|^((n-1)/q) - 1 gcd n = 1 by C,D,INT_2:def 2;
end;
hence n is prime by H1,H2,INT_1:18,B,C,Pock;
end;
now assume n is prime;
then reconsider m = n as prime Proth natural number;
Z/Z*(m) is cyclic by INT_7:31;
then consider g being Element of Z/Z*(m) such that
H: ord(g) = card(Z/Z*(m)) by GR_CY_1:19;
A: ord g = m-1 by H,INT_7:23;
Z/Z*(m) = multMagma(#Segm0(m),multint0(m)#) by INT_7:def 4;
then reconsider g1 = g as natural number;
D: not(g is being_of_order_0) by H,GROUP_1:def 11;
A2: (g1 |^ (m-1)) mod m = g |^ (m-1) by T1b
.= 1_(Z/Z*(m)) by A,D,GROUP_1:def 11
.= 1 by INT_7:21;
B: g1 |^ (m-1), 1 are_congruent_mod m by T1d,A2;
C: (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)) by NEWTON:5
.= g1 |^ (((m-1) / 2) + ((m-1) / 2)) by NEWTON:8
.= g1 |^ (m-1);
now assume E1: g1 |^ ((m-1) / 2), 1 are_congruent_mod n;
E: 1_(Z/Z*(m)) = 1 by INT_7:21
.= (g1 |^ ((m-1) / 2)) mod m by E1,INT_2:def 4,T1c
.= g |^ ((m-1) / 2) by T1b;
F: m-1 <> 0;
(m-1) * 2 >= (m-1) * 1 & 0<2 by XREAL_1:64;
then G: (m-1) / 2 <= m-1 by XREAL_1:79;
m-1 <= (m-1)/2 by A,D,E,GROUP_1:def 11;
then m-1 = (m-1)/2 by G,XXREAL_0:1;
hence contradiction by F;
end;
hence ex a being natural number
st a |^ ((n-1) / 2), -1 are_congruent_mod n by C,B,T1a;
end;
hence thesis by A;
end;
::$N Proth's theorem - version 2
theorem Proth2: :: Proth
for l being 2_or_greater natural number,
k being positive natural number
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 natural number,
k be positive natural number;
assume AS: 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 H: n >= 2|^l + 1 by XREAL_1:7;
X3: (2|^l)/2 = 2|^((l-1)+1) * 2"
.= (2|^(l-1) * 2) * 2" by NEWTON:6
.= 2|^(l-1) * 1;
X4: 2 * (k * 2|^(l-1)) = k * (2 * 2|^(l-1))
.= k * 2|^((l-1)+1) by NEWTON:6;
H1a: l >= 1 by NAT_1:14;
H1: l + 1 >= 1 + 1 by NAT_1:14,XREAL_1:6;
H2: 2|^l >= l + 1 by NEWTON:85;
then 2|^l >= 1 + 1 by H1,XXREAL_0:2;
then 2|^l + 1 >= 2 + 1 by XREAL_1:7;
then n >= 2 + 1 by H,XXREAL_0:2;
then n > 2 by NAT_1:13;
then reconsider n as 2_greater odd natural number by X4,Defg2;
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 natural number;
H3: 3|^((n-1)/2) = 3|^(k*2|^(l-1)) by X3;
K:now assume AS1: 3|^(k*2|^(l-1)), -1 are_congruent_mod k* 2|^l + 1;
reconsider s as Divisor of n-1 by INT_2:2,Def1;
s <> 0 & s <> 1 by H2,H1,XXREAL_0:2;
then reconsider s as non trivial Divisor of n-1 by NAT_2:def 1;
B1: (3|^(k*2|^(l-1))) * (3|^(k*2|^(l-1))),(-1)*(-1) are_congruent_mod n
by AS1,INT_1:18;
B: (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);
C2: k * 2|^ l <= (2|^l - 1) * 2|^l by AS,XREAL_1:64;
C3a: (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 C2,XREAL_1:6; then
C4: n < 2|^(l+l) - 2|^l + 1 + 1 by C3a,NAT_1:13;
C: s > sqrt(n)
proof
per cases;
suppose l >= 2;
then U: 2|^l >= 2|^2 by Th0;
2|^(1+1) = 2|^1 * 2 by NEWTON:6 .= 2 * 2 by NEWTON:5;
then 2|^l > 2 by U,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 C1: n < 2|^(2*l) by C4,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 C1,SQUARE_1:27;
end;
suppose l < 2;
then l < 1 + 1;
then l <= 1 by NAT_1:13;
then K: l = 1 by H1a,XXREAL_0:1; then
M: n = k*2 + 1 by NEWTON:5;
O: k <= 2 - 1 by AS,K,NEWTON:5;
k >= 1 by NAT_1:14;
then k = 1 by O,XXREAL_0:1;
hence thesis by M,SQUARE_1:27,SQUARE_1:20;
end;
end;
now let q be prime Divisor of s;
B: a|^((n-1)/q), -1 are_congruent_mod n by H3,AS1,T1,INT_2:28,Def1;
1 * (a|^((n-1)/q) - 1) = a|^((n-1)/q) - 1; then
C: 1 divides a|^((n-1)/q) - 1;
1 * n = n; then
D: 1 divides n;
now let m be Integer;
assume AS1: m divides a|^((n-1)/q) - 1 & m divides n;
then E: a|^((n-1)/q), 1 are_congruent_mod m;
consider j being Integer such that
H: m * j = n by AS1;
a|^((n-1)/q), -1 are_congruent_mod m by B,H,INT_1:20;
then a|^((n-1)/q) - a|^((n-1)/q), (-1)- 1 are_congruent_mod m
by E,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 T2a,INT_1:14;
hence m divides 1 by AS1,INT_2:10,ABIAN:def 1;
end;
hence a|^((n-1)/q) - 1 gcd n = 1 by C,D,INT_2:def 2;
end;
hence k * 2|^l + 1 is prime by B,B1,C,Pock;
end;
now assume n is prime;
then reconsider n as 2_greater prime natural number;
reconsider two = 2 as prime natural number by INT_2:28;
reconsider three = 3 as 2_greater prime natural number by Defg2,PEPIN:41;
XXZ: 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 by NEWTON:5;
then A1: 3 <> n by XXZ,H,XXREAL_0:2;
A3a: not(n,0 are_congruent_mod 3) by A1,INT_2:def 4;
A3b: now assume A3d: n,1 are_congruent_mod 3;
not (three divides 2|^l) by T1,INT_2:28;
then 3 gcd (2|^l) = 1 by T4;
hence contradiction by AS,INT_2:25,A3d,INT_2:def 3;
end;
n,0 are_congruent_mod 3 or ... or n,(3-1) are_congruent_mod 3 by XXX;
then A3: n,0 are_congruent_mod 3 or ... or n,2 are_congruent_mod 3;
A6a: 2,2+1 are_coprime by PEPIN:1;
not(three divides n) by A1,INT_2:def 4;
then A2: n gcd 3 = 1 by T4;
A4: ((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 A5: (-1)|^((n-1)/2) = 1;
Leg(three,n) * Leg(n,three) = 1 by A4,A5,A1,leg3;
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 A2,A3,A3a,A3b,A6a,leg1
.= -1 by qua0,A6a,deflegpr;
hence 3|^(k*2|^(l-1)), -1 are_congruent_mod k* 2|^l + 1 by H3,A2,euler;
end;
hence thesis by K;
end;
theorem
641 is prime
proof
641 = 2 * 320 + 1; then
reconsider n = 641 as odd natural number;
A: 256 + 64 = 320;
K1: 3 * 3 = 3|^1 * 3 by NEWTON:5 .= 3|^1 * 3|^1 by NEWTON:5
.= 3|^(1+1) by NEWTON:8;
K2: 3|^2 * 3|^2 = 3|^(2+2) by NEWTON:8;
K3: 3|^4 * 3|^4 = 3|^(4+4) by NEWTON:8;
6561 = 10 * 641 + 151;
then 3|^8, 151 are_congruent_mod 641 by K3,K2,K1;
then (3|^8) * (3|^8), 151 * 151 are_congruent_mod 641 by INT_1:18;
then K6: 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 K6,INT_1:15;
then K8: (3|^16) * (3|^16), 366 * 366 are_congruent_mod 641 by INT_1:18;
K8a: 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 K8a,INT_1:18;
then (3|^16) * (3|^16),91 * 183 are_congruent_mod 641 by K8,INT_1:15;
then K9: 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 K9,INT_1:15;
then (3|^32) * (3|^32), (-13) * (-13) are_congruent_mod 641 by INT_1:18;
then B: 3 |^ (32+32), 169 are_congruent_mod 641 by NEWTON:8;
then K10: (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 K10,INT_1:15;
then 3|^(64+64), 357 are_congruent_mod 641 by NEWTON:8;
then K11: (3|^128) * (3|^128), 357 * 357 are_congruent_mod 641 by INT_1:18;
K11a: 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 K11a,INT_1:18;
then (3|^128) * (3|^128),430 * 119 are_congruent_mod 641 by K11,INT_1:15;
then K12: 3|^(128+128),3010 * 17 are_congruent_mod 641 by NEWTON:8;
K12a: 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 K12a,INT_1:18;
then K13: 3|^(128+128),446*17 are_congruent_mod 641 by K12,INT_1:15;
7582 = 12 * 641 + (-110);
then 7582,-110 are_congruent_mod 641;
then 3 |^ 256, -110 are_congruent_mod 641 by K13,INT_1:15;
then (3 |^ 256) * (3|^64), (-110) * 169 are_congruent_mod 641 by B,INT_1:18;
then C: 3 |^ 320, -18590 are_congruent_mod 641 by A,NEWTON:8;
D: -18590 = (-30) * 641 + 640;
E: 640,-1 are_congruent_mod 641;
-18590,640 are_congruent_mod 641 by D;
then -18590,-1 are_congruent_mod 641 by E,INT_1:15; then
ex a being natural number st a|^((n-1)/2),-1 are_congruent_mod n by C,INT_1:15;
hence thesis by Proth1,P641;
end;
begin :: Fermat Numbers
registration
let l be natural number;
cluster Fermat l -> Proth;
coherence
proof
reconsider p = Fermat l as natural number;
set k = 1, n = 2|^l;
n + 1 > 0 + 1 by XREAL_1:6;
then n >= 1 by NAT_1:13; then
A: 2|^n > k by NEWTON:86,XXREAL_0:2;
B: 2 * 0 + 1 = 1;
p = k * (2|^n) + 1 by PEPIN:def 3;
hence thesis by A,B;
end;
end;
::$N Pepin's theorem
theorem :: Pepin
for l being non zero natural number
holds Fermat l is prime iff
3|^((Fermat l - 1)/2), -1 are_congruent_mod Fermat l
proof
let l be non zero natural number;
set k = 1;
H: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2 by NEWTON:5;
l + 1 >= 0 + 1 by XREAL_1:6;
then l >= 1 by NAT_1:13;
then 2|^l >= 2|^1 by Th0;
then 2|^l >= 2 by NEWTON:5;
then reconsider l1 = 2|^l as 2_or_greater natural number by EC_PF_2:def 1;
X1: not(3 divides k) by INT_2:27;
2|^l1 - 1 >= 4 - 1 by H,XREAL_1:9,EC_PF_2:def 1;
then X2: 1 <= 2|^l1 - 1 by XXREAL_0:2;
A: 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 X1,X2,A,Proth2;
end;
theorem
Fermat 5 is non prime
proof
K1: 2|^7 * 2|^7 = 2|^(7+7) by NEWTON:8;
K2: 5 * 5 = 5|^1 * 5 by NEWTON:5 .= 5|^1 * 5|^1 by NEWTON:5
.= 5|^(1+1) by NEWTON:8;
K3: 5|^2 * 5|^2 = 5|^(2+2) by NEWTON:8;
K4: 2|^14 * 2|^14 = 2|^(14+14) by NEWTON:8;
K5: 2|^4 * 2|^28 = 2|^(4+28) by NEWTON:8;
H1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2 by NEWTON:5;
H2: 2|^3 = 2|^(2+1) .= 2|^2 * 2 by NEWTON:6 .= 8 by H1;
H3: 2|^4 = 2|^(3+1) .= 2|^3 * 2 by NEWTON:6 .= 16 by H2;
H4: 2|^(3+4) = 8 * 16 by H3,H2,NEWTON:8;
5 * 2|^7, -1 are_congruent_mod 641 by H4;
then (5 * 2|^7) * (5 * 2|^7), (-1)*(-1) are_congruent_mod 641 by INT_1:18;
then A: (5|^2*2|^14)*(5|^2*2|^14), 1*1 are_congruent_mod 641 by K1,K2,INT_1:18;
(5|^4 + 2|^4) - 2|^4, 0 - 2|^4 are_congruent_mod 641 by K2,K3,H3;
then B: -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 B,INT_1:18;
then C1: -2|^32, 1 are_congruent_mod 641 by K3,K4,K5,A,INT_1:15;
-1, -1 are_congruent_mod 641 by INT_1:11;
then C2: (-1) * (-2|^32), (-1) * 1 are_congruent_mod 641 by C1,INT_1:18;
E1: 5 * 2|^7 + 1 = 641 by H4;
2|^(4+1) = 16 * 2 by H3,NEWTON:6; then
E3: Fermat 5 = 2|^32 + 1 by PEPIN:def 3;
5 * 2|^7 < 2|^3 * 2|^7 by H2,XREAL_1:68;
then D3: 5 * 2|^7 < 2|^(3+7) by NEWTON:8;
2 is non trivial; then
2|^10 < 2|^32 by Th0a;
then 5* 2|^7 < 2|^32 by D3,XXREAL_0:2;
then 641 < 2|^32 + 1 by E1,XREAL_1:6;
hence thesis by E3,C2;
end;
begin :: Cullen numbers
::$N Cullen numbers
definition
let n be natural number;
func CullenNumber n -> natural number equals
n * 2|^n + 1;
coherence;
end;
registration
let n be non zero natural number;
cluster CullenNumber n -> Proth;
coherence
proof
consider k being natural number,
l being odd natural number such that
H: n = l * 2|^k by Thc;
A: n * 2|^n + 1 = l* (2|^k * 2|^n) + 1 by H
.= 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
C: 2|^k * l >= 1 * l by XREAL_1:64;
k + n >= n by NAT_1:11;
then k + n >= l by H,C,XXREAL_0:2;
then 2|^(k+n) > l by XXREAL_0:2,NEWTON:86;
hence thesis by A;
end;
end;