:: Public-Key Cryptography and Pepin's Test for the Primality of Fermat Numbers
:: by Yoshinori Fujisawa , Yasushi Fuwa and Hidetaka Shimizu
::
:: Received December 21, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

Lm1: for n, x, y being Nat st n > 1 & x >= 1 & 1 = (((x * y) * n) + x) + y holds
( x = 1 & y = 0 )
proof end;

Lm2: for n being Nat holds 2 |^ (2 |^ n) > 1
proof end;

Lm3: for n being Nat st n <> 0 holds
n - 1 >= 0
proof end;

Lm4: for n being Nat st n <> 0 holds
(n -' 1) + 1 = (n + 1) -' 1
proof end;

theorem :: PEPIN:1
for i being Nat holds i,i + 1 are_relative_prime
proof end;

theorem Th2: :: PEPIN:2
for m, p being Nat holds
( not p is prime or m,p are_relative_prime or m gcd p = p )
proof end;

theorem Th3: :: PEPIN:3
for k, m, n being Nat st k divides n * m & n,k are_relative_prime holds
k divides m
proof end;

theorem Th4: :: PEPIN:4
for n, m, k being Nat st n divides m & k divides m & n,k are_relative_prime holds
n * k divides m
proof end;

registration
let i be Integer;
cluster i ^2 -> natural ;
coherence
i ^2 is natural
proof end;
end;

theorem :: PEPIN:5
for c being Integer st c > 1 holds
1 mod c = 1
proof end;

theorem Th6: :: PEPIN:6
for i, n being Nat st i <> 0 holds
( i divides n iff n mod i = 0 )
proof end;

theorem Th7: :: PEPIN:7
for m, n being Nat st m <> 0 & m divides n mod m holds
m divides n
proof end;

theorem :: PEPIN:8
for m, n, k being Nat st 0 < n & m mod n = k holds
n divides m - k
proof end;

theorem :: PEPIN:9
for i, p, k being Nat st i * p <> 0 & k mod (i * p) < p holds
k mod (i * p) = k mod p
proof end;

theorem Th10: :: PEPIN:10
for p being Nat
for a being Integer holds ((a * p) + 1) mod p = 1 mod p
proof end;

theorem Th11: :: PEPIN:11
for m, n, k being Nat st 1 < m & (n * k) mod m = k mod m & k,m are_relative_prime holds
n mod m = 1
proof end;

theorem Th12: :: PEPIN:12
for p, k, m being Nat holds (p |^ k) mod m = ((p mod m) |^ k) mod m
proof end;

Lm5: for k, n being Nat holds (k * (2 |^ (n + 1))) div 2 = k * (2 |^ n)
proof end;

Lm6: for k, n, m being Nat st k <= n holds
m |^ k divides m |^ n
proof end;

Lm7: 2 |^ 8 = 256
proof end;

theorem :: PEPIN:13
for i being Nat st i <> 0 holds
(i ^2) mod (i + 1) = 1
proof end;

theorem :: PEPIN:14
for k, j, i being Nat st k ^2 < j & i mod j = k holds
(i ^2) mod j = k ^2
proof end;

theorem :: PEPIN:15
for p, i being Nat st p is prime & i mod p = - 1 holds
(i ^2) mod p = 1
proof end;

theorem :: PEPIN:16
for n being Nat st n is even holds
n + 1 is odd ;

theorem :: PEPIN:17
for p being Nat st p > 2 & p is prime holds
p is odd
proof end;

theorem :: PEPIN:18
for n being Nat st n > 0 holds
2 to_power n is even
proof end;

theorem :: PEPIN:19
for i, j being Nat st i is odd & j is odd holds
i * j is odd ;

theorem :: PEPIN:20
for i, k being Nat st i is odd holds
i |^ k is odd
proof end;

theorem Th21: :: PEPIN:21
for k, i being Nat st k > 0 & i is even holds
i |^ k is even
proof end;

theorem :: PEPIN:22
for n being Nat holds
( 2 divides n iff n is even )
proof end;

theorem :: PEPIN:23
for m, n being Nat holds
( not m * n is even or m is even or n is even ) ;

theorem Th24: :: PEPIN:24
for n being Nat holds n |^ 2 = n ^2
proof end;

theorem Th25: :: PEPIN:25
for m, n being Nat st m > 1 & n > 0 holds
m |^ n > 1
proof end;

Lm8: for n being Nat holds (2 |^ (2 |^ n)) ^2 = 2 |^ (2 |^ (n + 1))
proof end;

theorem Th26: :: PEPIN:26
for n, p being Nat st n <> 0 & p <> 0 holds
n |^ p = n * (n |^ (p -' 1))
proof end;

theorem Th27: :: PEPIN:27
for n, m being Nat st m mod 2 = 0 holds
(n |^ (m div 2)) ^2 = n |^ m
proof end;

theorem Th28: :: PEPIN:28
for n, k being Nat st n <> 0 & 1 <= k holds
(n |^ k) div n = n |^ (k -' 1)
proof end;

theorem :: PEPIN:29
for n being Nat holds 2 |^ (n + 1) = (2 |^ n) + (2 |^ n)
proof end;

theorem Th30: :: PEPIN:30
for k, n, m being Nat st k > 1 & k |^ n = k |^ m holds
n = m
proof end;

Lm9: for k, n, x being Nat st k > n & x > 1 holds
x |^ k > x |^ n
proof end;

Lm10: for m, n being Nat st 2 |^ m divides 2 |^ n holds
m <= n
proof end;

theorem :: PEPIN:31
for m, n being Nat holds
( m <= n iff 2 |^ m divides 2 |^ n ) by Lm6, Lm10;

theorem Th32: :: PEPIN:32
for p, i, n being Nat st p is prime & i divides p |^ n & not i = 1 holds
ex k being Element of NAT st i = p * k
proof end;

theorem Th33: :: PEPIN:33
for p, k, n being Nat st p is prime & n < p |^ (k + 1) holds
( n divides p |^ (k + 1) iff n divides p |^ k )
proof end;

theorem Th34: :: PEPIN:34
for p, d, k being Nat st p is prime & d divides p |^ k holds
ex t being Element of NAT st
( d = p |^ t & t <= k )
proof end;

theorem Th35: :: PEPIN:35
for p, i, n being Nat st p > 1 & i mod p = 1 holds
(i |^ n) mod p = 1
proof end;

theorem Th36: :: PEPIN:36
for m, n being Nat st m > 0 holds
(n |^ m) mod n = 0
proof end;

theorem Th37: :: PEPIN:37
for n, p being Nat st p is prime & n,p are_relative_prime holds
(n |^ (p -' 1)) mod p = 1
proof end;

theorem Th38: :: PEPIN:38
for p, d, k being Nat st p is prime & d > 1 & d divides p |^ k & not d divides (p |^ k) div p holds
d = p |^ k
proof end;

definition
let i be Integer;
:: original: ^2
redefine func i ^2 -> Element of NAT ;
coherence
i ^2 is Element of NAT by ORDINAL1:def 12;
end;

theorem Th39: :: PEPIN:39
for m, n being Nat st n > 1 holds
( m mod n = 1 iff m,1 are_congruent_mod n )
proof end;

Lm11: for n, m being Nat st n > 1 & m > 1 & m,1 are_congruent_mod n holds
m mod n = 1
proof end;

theorem Th40: :: PEPIN:40
for i1, i2, i5, i3 being Integer st i1,i2 are_congruent_mod i5 & i1,i3 are_congruent_mod i5 holds
i2,i3 are_congruent_mod i5
proof end;

theorem Th41: :: PEPIN:41
3 is prime
proof end;

theorem Th42: :: PEPIN:42
for n being Nat st n <> 0 holds
Euler n <> 0
proof end;

theorem :: PEPIN:43
for n being Nat st n <> 0 holds
- n < n ;

theorem Th44: :: PEPIN:44
for n being Nat st n <> 0 holds
n div n = 1
proof end;

begin

definition
let k, m, n be Nat;
func Crypto (m,n,k) -> Element of NAT equals :: PEPIN:def 1
(m |^ k) mod n;
coherence
(m |^ k) mod n is Element of NAT ;
end;

:: deftheorem defines Crypto PEPIN:def 1 :
for k, m, n being Nat holds Crypto (m,n,k) = (m |^ k) mod n;

theorem :: PEPIN:45
for p, q, n, k1, k2 being Nat st p is prime & q is prime & p <> q & n = p * q & k1, Euler n are_relative_prime & (k1 * k2) mod (Euler n) = 1 holds
for m being Element of NAT st m < n holds
Crypto ((Crypto (m,n,k1)),n,k2) = m
proof end;

begin

definition
let i, p be Nat;
assume that
A1: p > 1 and
A2: i,p are_relative_prime ;
func order (i,p) -> Element of NAT means :Def2: :: PEPIN:def 2
( it > 0 & (i |^ it) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
( 0 < it & it <= k ) ) );
existence
ex b1 being Element of NAT st
( b1 > 0 & (i |^ b1) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
( 0 < b1 & b1 <= k ) ) )
proof end;
uniqueness
for b1, b2 being Element of NAT st b1 > 0 & (i |^ b1) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
( 0 < b1 & b1 <= k ) ) & b2 > 0 & (i |^ b2) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
( 0 < b2 & b2 <= k ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines order PEPIN:def 2 :
for i, p being Nat st p > 1 & i,p are_relative_prime holds
for b3 being Element of NAT holds
( b3 = order (i,p) iff ( b3 > 0 & (i |^ b3) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
( 0 < b3 & b3 <= k ) ) ) );

theorem :: PEPIN:46
for p being Nat st p > 1 holds
order (1,p) = 1
proof end;

theorem Th47: :: PEPIN:47
for p, i, n being Nat st p > 1 & (i |^ n) mod p = 1 & i,p are_relative_prime holds
order (i,p) divides n
proof end;

theorem Th48: :: PEPIN:48
for p, i, n being Nat st p > 1 & i,p are_relative_prime & order (i,p) divides n holds
(i |^ n) mod p = 1
proof end;

theorem Th49: :: PEPIN:49
for p, i being Nat st p is prime & i,p are_relative_prime holds
order (i,p) divides p -' 1
proof end;

begin

definition
let n be Nat;
func Fermat n -> Element of NAT equals :: PEPIN:def 3
(2 |^ (2 |^ n)) + 1;
correctness
coherence
(2 |^ (2 |^ n)) + 1 is Element of NAT ;
;
end;

:: deftheorem defines Fermat PEPIN:def 3 :
for n being Nat holds Fermat n = (2 |^ (2 |^ n)) + 1;

theorem Th50: :: PEPIN:50
Fermat 0 = 3
proof end;

theorem Th51: :: PEPIN:51
Fermat 1 = 5
proof end;

theorem Th52: :: PEPIN:52
Fermat 2 = 17
proof end;

theorem Th53: :: PEPIN:53
Fermat 3 = 257
proof end;

theorem Th54: :: PEPIN:54
Fermat 4 = (256 * 256) + 1
proof end;

theorem Th55: :: PEPIN:55
for n being Nat holds Fermat n > 2
proof end;

Lm12: for n being Nat holds Fermat n > 1
proof end;

Lm13: for n being Nat holds ((Fermat n) -' 1) mod 2 = 0
proof end;

Lm14: for n being Nat holds (Fermat n) -' 1 > 0
proof end;

Lm15: for n being Nat holds (Fermat n) mod (2 |^ (2 |^ n)) = 1
proof end;

Lm16: for n being Nat holds Fermat n is odd
proof end;

theorem Th56: :: PEPIN:56
for p, n being Nat st p is prime & p > 2 & p divides Fermat n holds
ex k being Element of NAT st p = (k * (2 |^ (n + 1))) + 1
proof end;

theorem Th57: :: PEPIN:57
for n being Nat st n <> 0 holds
3, Fermat n are_relative_prime
proof end;

begin

:: WP: Pepin's test
theorem Th58: :: PEPIN:58
for n being Nat st 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n holds
Fermat n is prime
proof end;

Lm17: 3 |^ 2 = 9
proof end;

Lm18: 3 |^ 4 = 81
proof end;

Lm19: 3 |^ 8 = 6561
proof end;

Lm20: 3 |^ 16 = 6561 * 6561
proof end;

Lm21: for i being Nat holds Fermat 1 divides (3 |^ ((4 * i) + 2)) + 1
proof end;

Lm22: for n being Nat st n = 1 holds
3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n
proof end;

Lm23: for n being Nat holds Fermat 2 divides (3 |^ ((16 * n) + 8)) + 1
proof end;

Lm24: (3 |^ 1) mod (Fermat 3) = 3
proof end;

Lm25: (3 |^ 2) mod (Fermat 3) = 9
proof end;

Lm26: (3 |^ 4) mod (Fermat 3) = 81
proof end;

Lm27: (3 |^ 8) mod (Fermat 3) = 136
proof end;

Lm28: (3 |^ 16) mod (Fermat 3) = 83 * 3
proof end;

Lm29: (3 |^ 32) mod (Fermat 3) = 64
proof end;

Lm30: (3 |^ 64) mod (Fermat 3) = 241
proof end;

Lm31: (3 |^ 128) mod (Fermat 3) = 256
proof end;

Lm32: (3 |^ 1) mod (Fermat 4) = 3
proof end;

Lm33: (3 |^ 2) mod (Fermat 4) = 9
proof end;

Lm34: (3 |^ 4) mod (Fermat 4) = 81
proof end;

Lm35: (3 |^ 8) mod (Fermat 4) = 6561
proof end;

Lm36: (3 |^ 16) mod (Fermat 4) = (164 * 332) + 1
proof end;

Lm37: (3 |^ 32) mod (Fermat 4) = 123 * 503
proof end;

Lm38: (3 |^ 64) mod (Fermat 4) = (14 * 1367) + 1
proof end;

Lm39: (3 |^ 128) mod (Fermat 4) = 52 * 289
proof end;

Lm40: (3 |^ 256) mod (Fermat 4) = 282
proof end;

Lm41: (3 |^ (256 * 2)) mod (Fermat 4) = 71 * 197
proof end;

Lm42: (3 |^ (256 * 4)) mod (Fermat 4) = 32 * 257
proof end;

Lm43: (3 |^ (256 * 8)) mod (Fermat 4) = 81 * 809
proof end;

Lm44: (3 |^ (256 * 16)) mod (Fermat 4) = 64
proof end;

Lm45: (3 |^ (256 * 32)) mod (Fermat 4) = 256 * 16
proof end;

Lm46: (3 |^ (256 * 64)) mod (Fermat 4) = 673 * 97
proof end;

Lm47: (3 |^ (256 * 128)) mod (Fermat 4) = 256 * 256
proof end;

Lm48: Fermat 3 divides (3 |^ ((32 * 0) + 128)) + 1
proof end;

Lm49: Fermat 4 divides (3 |^ ((64 * 0) + (256 * 128))) + 1
proof end;

theorem :: PEPIN:59
5 is prime
proof end;

theorem :: PEPIN:60
17 is prime
proof end;

theorem :: PEPIN:61
257 is prime
proof end;

theorem :: PEPIN:62
(256 * 256) + 1 is prime
proof end;

:: Moved from JORDAN1A, AK, 21.02.2006
theorem Th63: :: PEPIN:63
for i, j being Nat st j > 0 & i mod j = 0 holds
i div j = i / j
proof end;

theorem :: PEPIN:64
for i, n being Nat st n > 0 holds
(i |^ n) div i = (i |^ n) / i
proof end;

theorem Th65: :: PEPIN:65
for r being real number
for n being Nat st 0 < n & 1 < r holds
1 < r |^ n
proof end;

theorem :: PEPIN:66
for r being real number
for m, n being Nat st r > 1 & m > n holds
r |^ m > r |^ n
proof end;