:: Proth Numbers
:: by Christoph Schwarzweller
::
:: Received June 4, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users


registration
let n be natural positive number ;
cluster n - 1 -> natural ;
coherence
n - 1 is natural
proof end;
end;

registration
let n be non trivial natural number ;
cluster n - 1 -> positive ;
coherence
n - 1 is positive
proof end;
end;

registration
let n be natural number ;
reduce 1 |^ n to 1;
reducibility
1 |^ n = 1
;
end;

Lm1: for n being natural even number holds (- 1) |^ n = 1
proof end;

registration
let n be natural even number ;
reduce (- 1) |^ n to 1;
reducibility
(- 1) |^ n = 1
by Lm1;
end;

Lm2: for n being natural odd number holds (- 1) |^ n = - 1
proof end;

registration
let n be natural odd number ;
reduce (- 1) |^ n to - 1;
reducibility
(- 1) |^ n = - 1
by Lm2;
end;

theorem Th1: :: NAT_6:1
for a being natural positive number
for n, m being natural number st n >= m holds
a |^ n >= a |^ m
proof end;

theorem Th2: :: NAT_6:2
for a being non trivial natural number
for n, m being natural number st n > m holds
a |^ n > a |^ m
proof end;

theorem Th3: :: NAT_6:3
for n being natural non zero number ex k being natural number ex l being natural odd number st n = l * (2 |^ k)
proof end;

theorem Th4: :: NAT_6:4
for n being natural even number holds n div 2 = n / 2
proof end;

theorem :: NAT_6:5
for n being natural odd number holds n div 2 = (n - 1) / 2
proof end;

registration
let n be integer even number ;
cluster n / 2 -> integer ;
coherence
n / 2 is integer
proof end;
end;

registration
let n be natural even number ;
cluster n / 2 -> natural ;
coherence
n / 2 is natural
proof end;
end;

registration
cluster natural prime -> non trivial natural for set ;
coherence
for b1 being natural number st b1 is prime holds
not b1 is trivial
;
end;

Lm3: for a being natural number
for b being integer number st a divides b holds
a gcd b = a

proof end;

theorem Th6: :: NAT_6:6
for p being natural prime number
for a being integer number holds
( a gcd p <> 1 iff p divides a )
proof end;

theorem Th7: :: NAT_6:7
for i, j being integer number
for p being natural prime number holds
( not p divides i * j or p divides i or p divides j )
proof end;

theorem Th8: :: NAT_6:8
for x, p being natural prime number
for k being natural non zero number holds
( x divides p |^ k iff x = p )
proof end;

theorem Th9: :: NAT_6:9
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 end;

theorem Th10: :: NAT_6:10
for i being integer number
for j being non zero integer number holds i,i mod j are_congruent_mod j
proof end;

theorem :: NAT_6:11
for x, y being integer number
for n being integer positive number holds
( x,y are_congruent_mod n iff x mod n = y mod n )
proof end;

theorem Th12: :: NAT_6:12
for i, j being integer number
for n being natural number st n < j & i,n are_congruent_mod j holds
i mod j = n
proof end;

theorem Th13: :: NAT_6:13
for n being natural non zero number
for x being integer number holds
not not x, 0 are_congruent_mod n & ... & not x,n - 1 are_congruent_mod n
proof end;

theorem Th14: :: NAT_6:14
for n being natural non zero number
for x being integer number
for 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 end;

theorem Th15: :: NAT_6:15
for x being integer number holds
( x |^ 2, 0 are_congruent_mod 3 or x |^ 2,1 are_congruent_mod 3 )
proof end;

theorem Th16: :: NAT_6:16
for p being natural prime number
for x, y being Element of (Z/Z* p)
for i, j being integer number st x = i & y = j holds
x * y = (i * j) mod p
proof end;

theorem Th17: :: NAT_6:17
for p being natural prime number
for x being Element of (Z/Z* p)
for i being integer number
for n being natural number st x = i holds
x |^ n = (i |^ n) mod p
proof end;

theorem Th18: :: NAT_6:18
for p being natural prime number
for 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 end;

theorem Th19: :: NAT_6:19
for n being natural number holds
( - 1,1 are_congruent_mod n iff ( n = 2 or n = 1 ) )
proof end;

theorem Th20: :: NAT_6:20
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 end;

definition
let n, x be natural number ;
attr x is n _greater means :Def1: :: NAT_6:def 1
x > n;
end;

:: deftheorem Def1 defines _greater NAT_6:def 1 :
for n, x being natural number holds
( x is n _greater iff x > n );

notation
let n, x be natural number ;
antonym n _smaller x for n _or_greater ;
antonym n _or_smaller x for n _greater ;
end;

registration
let n be natural number ;
cluster epsilon-transitive epsilon-connected ordinal natural complex V20() integer dim-like odd ext-real non negative n _greater for set ;
existence
ex b1 being natural number st
( b1 is n _greater & b1 is odd )
proof end;
cluster epsilon-transitive epsilon-connected ordinal natural complex V20() integer dim-like even ext-real non negative n _greater for set ;
existence
ex b1 being natural number st
( b1 is n _greater & b1 is even )
proof end;
end;

registration
let n be natural number ;
cluster natural n _greater -> natural n _or_greater for set ;
coherence
for b1 being natural number st b1 is n _greater holds
b1 is n _or_greater
;
end;

registration
let n be natural number ;
cluster natural n + 1 _or_greater -> natural n _or_greater for set ;
coherence
for b1 being natural number st b1 is n + 1 _or_greater holds
b1 is n _or_greater
proof end;
cluster natural n + 1 _greater -> natural n _greater for set ;
coherence
for b1 being natural number st b1 is n + 1 _greater holds
b1 is n _greater
proof end;
cluster natural n _greater -> natural n + 1 _or_greater for set ;
coherence
for b1 being natural number st b1 is n _greater holds
b1 is n + 1 _or_greater
by NAT_1:13;
end;

registration
let m be non trivial natural number ;
cluster natural m _or_greater -> non trivial natural for set ;
coherence
for b1 being natural number st b1 is m _or_greater holds
not b1 is trivial
proof end;
end;

registration
let a be natural positive number ;
let m be natural number ;
let n be natural m _or_greater number ;
cluster a |^ n -> a |^ m _or_greater ;
coherence
not a |^ n is a |^ m _smaller
by Th1, EC_PF_2:def 1;
end;

registration
let a be non trivial natural number ;
let m be natural number ;
let n be natural m _greater number ;
cluster a |^ n -> a |^ m _greater ;
coherence
a |^ n is a |^ m _greater
by Def1, Th2;
end;

registration
cluster natural 2 _or_greater -> non trivial natural for set ;
coherence
for b1 being natural number st b1 is 2 _or_greater holds
not b1 is trivial
;
cluster non trivial natural -> natural 2 _or_greater for set ;
coherence
for b1 being natural number st not b1 is trivial holds
b1 is 2 _or_greater
proof end;
cluster non trivial natural odd -> natural 2 _greater for set ;
coherence
for b1 being natural number st not b1 is trivial & b1 is odd holds
b1 is 2 _greater
proof end;
end;

registration
let n be natural 2 _greater number ;
cluster n - 1 -> non trivial ;
coherence
not n - 1 is trivial
proof end;
end;

registration
let n be natural 2 _or_greater number ;
cluster n - 2 -> natural ;
coherence
n - 2 is natural
proof end;
end;

registration
let m be natural non zero number ;
let n be natural m _or_greater number ;
cluster n - 1 -> natural ;
coherence
n - 1 is natural
proof end;
end;

registration
cluster natural prime 2 _greater -> natural prime odd for set ;
coherence
for b1 being natural prime number st b1 is 2 _greater holds
b1 is odd
by INT_2:def 4;
end;

registration
let n be natural number ;
cluster epsilon-transitive epsilon-connected ordinal natural complex V20() integer dim-like prime ext-real non negative n _greater for set ;
existence
ex b1 being natural number st
( b1 is n _greater & b1 is prime )
proof end;
end;

definition
let n be natural number ;
mode Divisor of n -> natural number means :Def2: :: NAT_6:def 2
it divides n;
existence
ex b1 being natural number st b1 divides n
;
end;

:: deftheorem Def2 defines Divisor NAT_6:def 2 :
for n, b2 being natural number holds
( b2 is Divisor of n iff b2 divides n );

registration
let n be non trivial natural number ;
cluster non trivial epsilon-transitive epsilon-connected ordinal natural complex V20() integer dim-like ext-real non negative for Divisor of n;
existence
not for b1 being Divisor of n holds b1 is trivial
proof end;
end;

registration
let n be natural non zero number ;
cluster -> non zero for Divisor of n;
coherence
for b1 being Divisor of n holds not b1 is zero
proof end;
end;

registration
let n be natural positive number ;
cluster -> positive for Divisor of n;
coherence
for b1 being Divisor of n holds b1 is positive
;
end;

registration
let n be natural non zero number ;
cluster -> n _or_smaller for Divisor of n;
coherence
for b1 being Divisor of n holds b1 is n _or_smaller
proof end;
end;

registration
let n be non trivial natural number ;
cluster non empty epsilon-transitive epsilon-connected ordinal natural non zero complex V20() integer dim-like prime ext-real positive non negative n _or_smaller for Divisor of n;
existence
ex b1 being Divisor of n st b1 is prime
proof end;
end;

registration
let n be natural number ;
let q be Divisor of n;
cluster n / q -> natural ;
coherence
n / q is natural
proof 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
n / q is natural
proof end;
end;

:: WP: Pocklington's theorem
theorem Th21: :: NAT_6:21
for n being natural 2 _greater number
for 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 end;

notation
let a be integer number ;
let p be natural number ;
antonym a is_quadratic_non_residue_mod p for a is_quadratic_residue_mod p;
end;

theorem Th22: :: NAT_6:22
for p being natural positive number
for 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 end;

theorem Th23: :: NAT_6:23
2 is_quadratic_non_residue_mod 3
proof end;

:: WP: Legendre symbol
definition
let p be natural number ;
let a be integer number ;
func LegendreSymbol (a,p) -> integer Number equals :Def3: :: NAT_6:def 3
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
( ( a gcd p = 1 & a is_quadratic_residue_mod p & p <> 1 implies 1 is integer Number ) & ( p divides a implies 0 is integer Number ) & ( a gcd p = 1 & a is_quadratic_non_residue_mod p & p <> 1 implies - 1 is integer Number ) )
;
consistency
for b1 being integer Number holds
( ( a gcd p = 1 & a is_quadratic_residue_mod p & p <> 1 & p divides a implies ( b1 = 1 iff b1 = 0 ) ) & ( a gcd p = 1 & a is_quadratic_residue_mod p & p <> 1 & a gcd p = 1 & a is_quadratic_non_residue_mod p & p <> 1 implies ( b1 = 1 iff b1 = - 1 ) ) & ( p divides a & a gcd p = 1 & a is_quadratic_non_residue_mod p & p <> 1 implies ( b1 = 0 iff b1 = - 1 ) ) )
by Lm3;
end;

:: deftheorem Def3 defines LegendreSymbol NAT_6:def 3 :
for p being natural number
for a being integer number holds
( ( a gcd p = 1 & a is_quadratic_residue_mod p & p <> 1 implies LegendreSymbol (a,p) = 1 ) & ( p divides a implies LegendreSymbol (a,p) = 0 ) & ( a gcd p = 1 & a is_quadratic_non_residue_mod p & p <> 1 implies LegendreSymbol (a,p) = - 1 ) );

definition
let p be natural prime number ;
let a be integer number ;
redefine func LegendreSymbol (a,p) equals :Def4: :: NAT_6:def 4
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
for b1 being integer Number holds
( ( a gcd p = 1 & a is_quadratic_residue_mod p & p divides a implies ( b1 = 1 iff b1 = 0 ) ) & ( a gcd p = 1 & a is_quadratic_residue_mod p & a gcd p = 1 & a is_quadratic_non_residue_mod p implies ( b1 = 1 iff b1 = - 1 ) ) & ( p divides a & a gcd p = 1 & a is_quadratic_non_residue_mod p implies ( b1 = 0 iff b1 = - 1 ) ) )
proof end;
compatibility
for b1 being integer Number holds
( ( a gcd p = 1 & a is_quadratic_residue_mod p implies ( b1 = LegendreSymbol (a,p) iff b1 = 1 ) ) & ( p divides a implies ( b1 = LegendreSymbol (a,p) iff b1 = 0 ) ) & ( a gcd p = 1 & a is_quadratic_non_residue_mod p implies ( b1 = LegendreSymbol (a,p) iff b1 = - 1 ) ) )
proof end;
end;

:: deftheorem Def4 defines LegendreSymbol NAT_6:def 4 :
for p being natural prime number
for a being integer number holds
( ( a gcd p = 1 & a is_quadratic_residue_mod p implies LegendreSymbol (a,p) = 1 ) & ( p divides a implies LegendreSymbol (a,p) = 0 ) & ( a gcd p = 1 & a is_quadratic_non_residue_mod p implies LegendreSymbol (a,p) = - 1 ) );

notation
let p be natural number ;
let a be integer number ;
synonym Leg (a,p) for LegendreSymbol (a,p);
end;

theorem Th24: :: NAT_6:24
for p being natural prime number
for a being integer number holds
( Leg (a,p) = 1 or Leg (a,p) = 0 or Leg (a,p) = - 1 )
proof end;

theorem Th25: :: NAT_6:25
for p being natural prime number
for a being integer number holds
( ( Leg (a,p) = 1 implies ( a gcd p = 1 & a is_quadratic_residue_mod p ) ) & ( a gcd p = 1 & a is_quadratic_residue_mod p implies Leg (a,p) = 1 ) & ( Leg (a,p) = 0 implies p divides a ) & ( p divides a implies Leg (a,p) = 0 ) & ( Leg (a,p) = - 1 implies ( a gcd p = 1 & a is_quadratic_non_residue_mod p ) ) & ( a gcd p = 1 & a is_quadratic_non_residue_mod p implies Leg (a,p) = - 1 ) )
proof end;

theorem :: NAT_6:26
for p being natural number holds Leg (p,p) = 0 by Def3;

theorem :: NAT_6:27
for a being integer number holds Leg (a,2) = a mod 2
proof end;

Lm4: for a being integer number
for p being natural prime number holds Lege (a,p) = Leg (a,p)

proof end;

theorem Th28: :: NAT_6:28
for p being natural prime 2 _greater number
for 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 end;

theorem :: NAT_6:29
for p being natural prime 2 _greater number
for 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 end;

theorem Th30: :: NAT_6:30
for p, q being natural prime 2 _greater number st p <> q holds
(Leg (p,q)) * (Leg (q,p)) = (- 1) |^ (((p - 1) / 2) * ((q - 1) / 2))
proof end;

:: WP: Euler's criterion
theorem Th31: :: NAT_6:31
for p being natural prime 2 _greater number
for a being integer number st a gcd p = 1 holds
a |^ ((p - 1) / 2), LegendreSymbol (a,p) are_congruent_mod p
proof end;

:: WP: Proth numbers
definition
let p be natural number ;
attr p is Proth means :Def5: :: NAT_6:def 5
ex k being natural odd number ex n being natural positive number st
( 2 |^ n > k & p = (k * (2 |^ n)) + 1 );
end;

:: deftheorem Def5 defines Proth NAT_6:def 5 :
for p being natural number holds
( p is Proth iff ex k being natural odd number ex n being natural positive number st
( 2 |^ n > k & p = (k * (2 |^ n)) + 1 ) );

Lm5: 1 is odd
proof end;

Lm6: 3 is Proth
proof end;

Lm7: 9 is Proth
proof end;

registration
cluster epsilon-transitive epsilon-connected ordinal natural complex V20() integer dim-like prime ext-real non negative Proth for set ;
existence
ex b1 being natural number st
( b1 is Proth & b1 is prime )
by Lm6, PEPIN:41;
cluster epsilon-transitive epsilon-connected ordinal natural complex V20() integer dim-like non prime ext-real non negative Proth for set ;
existence
ex b1 being natural number st
( b1 is Proth & not b1 is prime )
proof end;
end;

registration
cluster natural Proth -> non trivial natural odd for set ;
coherence
for b1 being natural number st b1 is Proth holds
( not b1 is trivial & b1 is odd )
proof end;
end;

theorem :: NAT_6:32
3 is Proth by Lm6;

theorem :: NAT_6:33
5 is Proth
proof end;

theorem :: NAT_6:34
9 is Proth by Lm7;

theorem :: NAT_6:35
13 is Proth
proof end;

theorem :: NAT_6:36
17 is Proth
proof end;

theorem Th37: :: NAT_6:37
641 is Proth
proof end;

theorem :: NAT_6:38
11777 is Proth
proof end;

theorem :: NAT_6:39
13313 is Proth
proof end;

:: WP: Proth's theorem
theorem Th40: :: NAT_6:40
for n being natural Proth number holds
( n is prime iff ex a being natural number st a |^ ((n - 1) / 2), - 1 are_congruent_mod n )
proof end;

theorem Th41: :: NAT_6:41
for l being natural 2 _or_greater number
for k being natural positive 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 end;

theorem :: NAT_6:42
641 is prime
proof end;

registration
let l be natural number ;
cluster Fermat l -> Proth ;
coherence
Fermat l is Proth
proof end;
end;

:: WP: Pepin's theorem
theorem :: NAT_6:43
for l being natural non zero number holds
( Fermat l is prime iff 3 |^ (((Fermat l) - 1) / 2), - 1 are_congruent_mod Fermat l )
proof end;

theorem :: NAT_6:44
not Fermat 5 is prime
proof end;

:: WP: Cullen numbers
definition
let n be natural number ;
func CullenNumber n -> natural number equals :: NAT_6:def 6
(n * (2 |^ n)) + 1;
coherence
(n * (2 |^ n)) + 1 is natural number
;
end;

:: deftheorem defines CullenNumber NAT_6:def 6 :
for n being natural number holds CullenNumber n = (n * (2 |^ n)) + 1;

registration
let n be natural non zero number ;
cluster CullenNumber n -> natural Proth ;
coherence
CullenNumber n is Proth
proof end;
end;