:: 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 b₁ being natural number st b₁ is prime holds
not b₁ 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 b₁ being natural number st
( b₁ is n _greater & b₁ 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 b₁ being natural number st
( b₁ is n _greater & b₁ is even )

proof end;

end;

registration

let n be natural number ;

cluster natural n _greater -> natural n _or_greater for set ;

coherence
for b₁ being natural number st b₁ is n _greater holds
b₁ 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 b₁ being natural number st b₁ is n + 1 _or_greater holds
b₁ is n _or_greater

proof end;

cluster natural n + 1 _greater -> natural n _greater for set ;

coherence
for b₁ being natural number st b₁ is n + 1 _greater holds
b₁ is n _greater

proof end;

cluster natural n _greater -> natural n + 1 _or_greater for set ;

coherence
for b₁ being natural number st b₁ is n _greater holds
b₁ 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 b₁ being natural number st b₁ is m _or_greater holds
not b₁ 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 b₁ being natural number st b₁ is 2 _or_greater holds
not b₁ is trivial ;

cluster non trivial natural -> natural 2 _or_greater for set ;

coherence
for b₁ being natural number st not b₁ is trivial holds
b₁ is 2 _or_greater

proof end;

cluster non trivial natural odd -> natural 2 _greater for set ;

coherence
for b₁ being natural number st not b₁ is trivial & b₁ is odd holds
b₁ 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 b₁ being natural prime number st b₁ is 2 _greater holds
b₁ 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 b₁ being natural number st
( b₁ is n _greater & b₁ 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 b₁ being natural number st b₁ divides n ;

end;

:: deftheorem Def2 defines Divisor NAT_6:def 2 :
for n, b₂ being natural number holds
( b₂ is Divisor of n iff b₂ 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 b₁ being Divisor of n holds b₁ is trivial

proof end;

end;

registration

let n be natural non zero number ;

cluster -> non zero for Divisor of n;

coherence
for b₁ being Divisor of n holds not b₁ is zero

proof end;

end;

registration

let n be natural positive number ;

cluster -> positive for Divisor of n;

coherence
for b₁ being Divisor of n holds b₁ is positive ;

end;

registration

let n be natural non zero number ;

cluster -> n _or_smaller for Divisor of n;

coherence
for b₁ being Divisor of n holds b₁ 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 b₁ being Divisor of n st b₁ 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;

:: 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;

:: 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 b₁ being integer Number holds
( ( a gcd p = 1 & a is_quadratic_residue_mod p & p <> 1 & p divides a implies ( b₁ = 1 iff b₁ = 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 ( b₁ = 1 iff b₁ = - 1 ) ) & ( p divides a & a gcd p = 1 & a is_quadratic_non_residue_mod p & p <> 1 implies ( b₁ = 0 iff b₁ = - 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 b₁ being integer Number holds
( ( a gcd p = 1 & a is_quadratic_residue_mod p & p divides a implies ( b₁ = 1 iff b₁ = 0 ) ) & ( a gcd p = 1 & a is_quadratic_residue_mod p & a gcd p = 1 & a is_quadratic_non_residue_mod p implies ( b₁ = 1 iff b₁ = - 1 ) ) & ( p divides a & a gcd p = 1 & a is_quadratic_non_residue_mod p implies ( b₁ = 0 iff b₁ = - 1 ) ) )

proof end;

compatibility
for b₁ being integer Number holds
( ( a gcd p = 1 & a is_quadratic_residue_mod p implies ( b₁ = LegendreSymbol (a,p) iff b₁ = 1 ) ) & ( p divides a implies ( b₁ = LegendreSymbol (a,p) iff b₁ = 0 ) ) & ( a gcd p = 1 & a is_quadratic_non_residue_mod p implies ( b₁ = LegendreSymbol (a,p) iff b₁ = - 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;

:: 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;

:: 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 b₁ being natural number st
( b₁ is Proth & b₁ 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 b₁ being natural number st
( b₁ is Proth & not b₁ is prime )

proof end;

end;

registration

cluster natural Proth -> non trivial natural odd for set ;

coherence
for b₁ being natural number st b₁ is Proth holds
( not b₁ is trivial & b₁ 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;

:: 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;

:: 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;

:: 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;