:: 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-2011 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 n be Nat;
cluster n ^2 -> natural ;
coherence
n ^2 is natural ;

end;

definition

let n be Element of NAT ;
:: original: ^2
redefine func n ^2 -> Element of NAT ;
coherence
n ^2 is Element of NAT by ORDINAL1:def 13;

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
not n + 1 is even ;

theorem :: PEPIN:17

for p being Nat st p > 2 & p is prime holds
not p is even

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 not i is even & not j is even holds
not i * j is even ;

theorem :: PEPIN:20

for i, k being Nat st not i is even holds
not i |^ k is even

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 :: PEPIN:25

canceled;

theorem Th26: :: PEPIN:26

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 Th27: :: PEPIN:27

for n, p being Nat st n <> 0 & p <> 0 holds
n |^ p = n * (n |^ (p -' 1))

proof end;

theorem Th28: :: PEPIN:28

for n, m being Nat st m mod 2 = 0 holds
(n |^ (m div 2)) ^2 = n |^ m

proof end;

theorem Th29: :: PEPIN:29

for n, k being Nat st n <> 0 & 1 <= k holds
(n |^ k) div n = n |^ (k -' 1)

proof end;

theorem :: PEPIN:30

for n being Nat holds 2 |^ (n + 1) = (2 |^ n) + (2 |^ n)

proof end;

theorem Th31: :: PEPIN:31

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

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

theorem Th33: :: PEPIN:33

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 Th34: :: PEPIN:34

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 Th35: :: PEPIN:35

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 Th36: :: PEPIN:36

for p, i, n being Nat st p > 1 & i mod p = 1 holds
(i |^ n) mod p = 1

proof end;

theorem Th37: :: PEPIN:37

for m, n being natural number st m > 0 holds
(n |^ m) mod n = 0

proof end;

theorem Th38: :: PEPIN:38

for n, p being Nat st p is prime & n,p are_relative_prime holds
(n |^ (p -' 1)) mod p = 1

proof end;

theorem Th39: :: PEPIN:39

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 a be Integer;
:: original: ^2
redefine func a ^2 -> Element of NAT ;
coherence
a ^2 is Element of NAT by INT_1:16, XREAL_1:65;

end;

theorem Th40: :: PEPIN:40

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 :: PEPIN:41

canceled;

theorem :: PEPIN:42

canceled;

theorem Th43: :: PEPIN:43

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 Th44: :: PEPIN:44

3 is prime

proof end;

theorem Th45: :: PEPIN:45

for n being Nat st n <> 0 holds
Euler n <> 0

proof end;

theorem :: PEPIN:46

for n being Nat st n <> 0 holds
- n < n ;

theorem :: PEPIN:47

canceled;

theorem Th48: :: PEPIN:48

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

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 b₁ being Element of NAT st
( b₁ > 0 & (i |^ b₁) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
( 0 < b₁ & b₁ <= k ) ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st b₁ > 0 & (i |^ b₁) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
( 0 < b₁ & b₁ <= k ) ) & b₂ > 0 & (i |^ b₂) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
( 0 < b₂ & b₂ <= k ) ) holds
b₁ = b₂

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 b₃ being Element of NAT holds
( b₃ = order (i,p) iff ( b₃ > 0 & (i |^ b₃) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
( 0 < b₃ & b₃ <= k ) ) ) );

theorem :: PEPIN:50

for p being Nat st p > 1 holds
order (1,p) = 1

proof end;

theorem :: PEPIN:51

canceled;

theorem Th52: :: PEPIN:52

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 Th53: :: PEPIN:53

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 Th54: :: PEPIN:54

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 Th55: :: PEPIN:55

Fermat 0 = 3

proof end;

theorem Th56: :: PEPIN:56

Fermat 1 = 5

proof end;

theorem Th57: :: PEPIN:57

Fermat 2 = 17

proof end;

theorem Th58: :: PEPIN:58

Fermat 3 = 257

proof end;

theorem Th59: :: PEPIN:59

Fermat 4 = (256 * 256) + 1

proof end;

theorem Th60: :: PEPIN:60

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 not Fermat n is even

proof end;

theorem Th61: :: PEPIN:61

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 Th62: :: PEPIN:62

for n being Nat st n <> 0 holds
3, Fermat n are_relative_prime

proof end;

begin

theorem Th63: :: PEPIN:63

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

5 is prime

proof end;

theorem :: PEPIN:65

17 is prime

proof end;

theorem :: PEPIN:66

257 is prime

proof end;

theorem :: PEPIN:67

(256 * 256) + 1 is prime

proof end;

theorem Th68: :: PEPIN:68

for i, j being natural number st j > 0 & i mod j = 0 holds
i div j = i / j

proof end;

theorem :: PEPIN:69

for i, n being natural number st n > 0 holds
(i |^ n) div i = (i |^ n) / i

proof end;

theorem Th70: :: PEPIN:70

for r being real number
for n being natural number st 0 < n & 1 < r holds
1 < r |^ n

proof end;

theorem :: PEPIN:71

for r being real number
for m, n being natural number st r > 1 & m > n holds
r |^ m > r |^ n

proof end;