:: by Christoph Schwarzweller

::

:: Received June 4, 2014

:: Copyright (c) 2014-2017 Association of Mizar Users

registration
end;

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

proof end;

registration
end;

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

proof end;

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

registration
end;

registration
end;

registration
end;

Lm3: for a being natural number

for b being integer number st a divides b holds

a gcd b = 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 )

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 )

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 )

( x,y are_congruent_mod n iff ex k being Integer st x = (k * n) + y )

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 )

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

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

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

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

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

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 ) )

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 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 ) )

( - 1,1 are_congruent_mod i iff ( i = 2 or i = 1 or i = - 2 or i = - 1 ) )

proof end;

:: deftheorem Def1 defines _greater NAT_6:def 1 :

for n, x being natural number holds

( x is n _greater iff x > n );

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;
antonym n _smaller x for n _or_greater ;

antonym n _or_smaller x for n _greater ;

registration

let n be natural number ;

ex b_{1} being natural number st

( b_{1} is n _greater & b_{1} is odd )

ex b_{1} being natural number st

( b_{1} is n _greater & b_{1} is even )

end;
cluster epsilon-transitive epsilon-connected ordinal natural complex V20() integer dim-like odd ext-real non negative n _greater for set ;

existence ex b

( b

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

( b

proof end;

registration

let n be natural number ;

coherence

for b_{1} being natural number st b_{1} is n _greater holds

b_{1} is n _or_greater
;

end;
coherence

for b

b

registration

let n be natural number ;

coherence

for b_{1} being natural number st b_{1} is n + 1 _or_greater holds

b_{1} is n _or_greater

for b_{1} being natural number st b_{1} is n + 1 _greater holds

b_{1} is n _greater

for b_{1} being natural number st b_{1} is n _greater holds

b_{1} is n + 1 _or_greater
by NAT_1:13;

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

registration

let m be non trivial natural number ;

coherence

for b_{1} being natural number st b_{1} is m _or_greater holds

not b_{1} is trivial

end;
coherence

for b

not b

proof end;

registration

let a be natural positive number ;

let m be natural number ;

let n be natural m _or_greater number ;

coherence

not a |^ n is a |^ m _smaller by Th1, EC_PF_2:def 1;

end;
let m be natural number ;

let n be natural m _or_greater number ;

coherence

not a |^ n is a |^ m _smaller by Th1, EC_PF_2:def 1;

registration

let a be non trivial natural number ;

let m be natural number ;

let n be natural m _greater number ;

coherence

a |^ n is a |^ m _greater by Def1, Th2;

end;
let m be natural number ;

let n be natural m _greater number ;

coherence

a |^ n is a |^ m _greater by Def1, Th2;

registration

coherence

for b_{1} being natural number st b_{1} is 2 _or_greater holds

not b_{1} is trivial
;

coherence

for b_{1} being natural number st not b_{1} is trivial holds

b_{1} is 2 _or_greater

for b_{1} being natural number st not b_{1} is trivial & b_{1} is odd holds

b_{1} is 2 _greater

end;
for b

not b

coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let m be natural non zero number ;

let n be natural m _or_greater number ;

coherence

n - 1 is natural

end;
let n be natural m _or_greater number ;

coherence

n - 1 is natural

proof end;

registration

coherence

for b_{1} being natural prime number st b_{1} is 2 _greater holds

b_{1} is odd
by INT_2:def 4;

end;
for b

b

registration

let n be natural number ;

ex b_{1} being natural number st

( b_{1} is n _greater & b_{1} is prime )

end;
cluster epsilon-transitive epsilon-connected ordinal natural complex V20() integer dim-like prime ext-real non negative n _greater for set ;

existence ex b

( b

proof end;

definition
end;

:: deftheorem Def2 defines Divisor NAT_6:def 2 :

for n, b_{2} being natural number holds

( b_{2} is Divisor of n iff b_{2} divides n );

for n, b

( b

registration

let n be non trivial natural number ;

not for b_{1} being Divisor of n holds b_{1} is trivial

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

proof end;

registration

let n be natural non zero number ;

coherence

for b_{1} being Divisor of n holds not b_{1} is zero

end;
coherence

for b

proof end;

registration
end;

registration

let n be natural non zero number ;

coherence

for b_{1} being Divisor of n holds b_{1} is n _or_smaller

end;
coherence

for b

proof end;

registration

let n be non trivial natural number ;

ex b_{1} being Divisor of n st b_{1} is prime

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

proof end;

registration
end;

registration

let n be natural number ;

let s be Divisor of n;

let q be Divisor of s;

coherence

n / q is natural

end;
let s be Divisor of n;

let q be Divisor of s;

coherence

n / q is natural

proof 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

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;
let p be natural number ;

antonym a is_quadratic_non_residue_mod p for a is_quadratic_residue_mod p;

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 )

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;

definition

let p be natural number ;

let a be integer number ;

( ( 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_{1} being integer Number holds

( ( a gcd p = 1 & a is_quadratic_residue_mod p & p <> 1 & p divides a implies ( b_{1} = 1 iff b_{1} = 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} = 1 iff b_{1} = - 1 ) ) & ( p divides a & a gcd p = 1 & a is_quadratic_non_residue_mod p & p <> 1 implies ( b_{1} = 0 iff b_{1} = - 1 ) ) )
by Lm3;

end;
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 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 )

;

( ( 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

( ( a gcd p = 1 & a is_quadratic_residue_mod p & p <> 1 & p divides a implies ( b

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

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 ;

for b_{1} being integer Number holds

( ( a gcd p = 1 & a is_quadratic_residue_mod p & p divides a implies ( b_{1} = 1 iff b_{1} = 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} = 1 iff b_{1} = - 1 ) ) & ( p divides a & a gcd p = 1 & a is_quadratic_non_residue_mod p implies ( b_{1} = 0 iff b_{1} = - 1 ) ) )

for b_{1} being integer Number holds

( ( a gcd p = 1 & a is_quadratic_residue_mod p implies ( b_{1} = LegendreSymbol (a,p) iff b_{1} = 1 ) ) & ( p divides a implies ( b_{1} = LegendreSymbol (a,p) iff b_{1} = 0 ) ) & ( a gcd p = 1 & a is_quadratic_non_residue_mod p implies ( b_{1} = LegendreSymbol (a,p) iff b_{1} = - 1 ) ) )

end;
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 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 )

;

for b

( ( a gcd p = 1 & a is_quadratic_residue_mod p & p divides a implies ( b

proof end;

compatibility for b

( ( a gcd p = 1 & a is_quadratic_residue_mod p implies ( b

proof 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 ) );

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
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 )

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 ) )

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;

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)

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))

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))

(Leg (p,q)) * (Leg (q,p)) = (- 1) |^ (((p - 1) / 2) * ((q - 1) / 2))

proof end;

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

for a being integer number st a gcd p = 1 holds

a |^ ((p - 1) / 2), LegendreSymbol (a,p) are_congruent_mod p

proof 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 ) );

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

ex b_{1} being natural number st

( b_{1} is Proth & b_{1} is prime )
by Lm6, PEPIN:41;

ex b_{1} being natural number st

( b_{1} is Proth & not b_{1} is prime )
end;

cluster epsilon-transitive epsilon-connected ordinal natural complex V20() integer dim-like prime ext-real non negative Proth for set ;

existence ex b

( b

cluster epsilon-transitive epsilon-connected ordinal natural complex V20() integer dim-like non prime ext-real non negative Proth for set ;

existence ex b

( b

proof end;

registration

coherence

for b_{1} being natural number st b_{1} is Proth holds

( not b_{1} is trivial & b_{1} is odd )

end;
for b

( not b

proof end;

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 )

( 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 )

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;

registration
end;

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 )

( Fermat l is prime iff 3 |^ (((Fermat l) - 1) / 2), - 1 are_congruent_mod Fermat l )

proof end;

:: deftheorem defines CullenNumber NAT_6:def 6 :

for n being natural number holds CullenNumber n = (n * (2 |^ n)) + 1;

for n being natural number holds CullenNumber n = (n * (2 |^ n)) + 1;