:: PEPIN semantic presentation

Lm1: for i1, i2 being Integer
for n1, n2 being Nat st i1 = n1 & i2 = n2 holds
( i1 divides i2 iff n1 divides n2 )

proof end;

Lm2: for n being Nat
for a being Integer st n > 1 & n * a > 0 holds
a > 0
by XREAL_1:133;

Lm3: for n, x, y being Nat st n > 1 & x >= 1 & y >= 0 & 1 = (((x * y) * n) + x) + y holds
( x = 1 & y = 0 )

proof end;

Lm4: for n being Nat holds 2 |^ (2 |^ n) > 1

proof end;

Lm5: for n being Nat st n <> 0 holds
n - 1 >= 0

proof end;

Lm6: 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 p, m being Nat holds
( not p is prime or m,p are_relative_prime or m hcf p = p )

proof end;

theorem Th3: :: PEPIN:3

for k, n, m 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;

definition

let n be Nat;
:: original: ^2
redefine func n ^2 -> Nat;
coherence

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 n, i 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 n, m, 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 & p is prime & 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;

Lm7: for k, n being Nat holds (k * (2 |^ (n + 1))) div 2 = k * (2 |^ n)

proof end;

Lm8: for k, n, m being Nat st k <= n holds
m |^ k divides m |^ n

proof end;

Lm9: 2 |^ 2 = 4

proof end;

Lm10: 2 |^ 3 = 8

proof end;

Lm11: 2 |^ 4 = 16

proof end;

Lm12: 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 Th16: :: PEPIN:16

for n being Nat st n is even holds
not n + 1 is even

proof end;

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;

Lm13: for i, j being Nat st i is even & j is even holds
i * j is even

proof end;

theorem Th19: :: PEPIN:19

for i, j being Nat st not i is even & not j is even holds
not i * j is even

proof end;

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 ) by Th19;

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;

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

Lm15: for k, n, x being Nat st k > n & x > 1 holds
x |^ k > x |^ n

proof end;

Lm16: 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 Lm8, Lm16;

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 Nat st i = p * k

proof end;

theorem Th34: :: PEPIN:34

for p, k, n being Nat st n <> 0 & 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 & d <> 0 holds
ex t being 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 :: PEPIN:37

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

proof end;

theorem Th38: :: PEPIN:38

for p, n 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 -> Nat;
coherence

proof end;

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;

Lm17: for n, m being Nat st n > 1 & m > 1 & m,1 are_congruent_mod n holds
m mod n = 1

proof end;

theorem Th41: :: PEPIN:41

for a, b, c being Integer st a,b are_congruent_mod c holds
a ^2 ,b ^2 are_congruent_mod c by INT_1:39;

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;

definition

let k, m, n be Nat;
func Crypto m,n,k -> Nat equals :: PEPIN:def 1
(m |^ k) mod n;
coherence ;

end;

:: deftheorem defines Crypto PEPIN:def 1 :

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 Nat st m < n holds
Crypto (Crypto m,n,k1),n,k2 = m

proof end;

definition

let i, p be Nat;
assume A1: ( p > 1 & i,p are_relative_prime ) ;
func order i,p -> 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines order PEPIN:def 2 :

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, n, i being Nat st p > 1 & n > 0 & (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;

definition

let n be Nat;
func Fermat n -> Nat equals :: PEPIN:def 3
(2 |^ (2 |^ n)) + 1;
correctness ;

end;

:: deftheorem defines Fermat PEPIN:def 3 :

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;

Lm18: for n being Nat holds Fermat n > 1

proof end;

Lm19: for n being Nat holds ((Fermat n) -' 1) mod 2 = 0

proof end;

Lm20: for n being Nat holds (Fermat n) -' 1 > 0

proof end;

Lm21: for n being Nat holds (Fermat n) mod (2 |^ (2 |^ n)) = 1

proof end;

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

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;

Lm23: 3 |^ 2 = 9

proof end;

Lm24: 3 |^ 4 = 81

proof end;

Lm25: 3 |^ 8 = 6561

proof end;

Lm26: 3 |^ 16 = 6561 * 6561

proof end;

Lm27: for i being Nat holds Fermat 1 divides (3 |^ ((4 * i) + 2)) + 1

proof end;

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

proof end;

Lm29: for n being Nat holds Fermat 2 divides (3 |^ ((16 * n) + 8)) + 1

proof end;

Lm30: (3 |^ 1) mod (Fermat 3) = 3

proof end;

Lm31: (3 |^ 2) mod (Fermat 3) = 9

proof end;

Lm32: (3 |^ 4) mod (Fermat 3) = 81

proof end;

Lm33: (3 |^ 8) mod (Fermat 3) = 136

proof end;

Lm34: (3 |^ 16) mod (Fermat 3) = 83 * 3

proof end;

Lm35: (3 |^ 32) mod (Fermat 3) = 64

proof end;

Lm36: (3 |^ 64) mod (Fermat 3) = 241

proof end;

Lm37: (3 |^ 128) mod (Fermat 3) = 256

proof end;

Lm38: (3 |^ 1) mod (Fermat 4) = 3

proof end;

Lm39: (3 |^ 2) mod (Fermat 4) = 9

proof end;

Lm40: (3 |^ 4) mod (Fermat 4) = 81

proof end;

Lm41: (3 |^ 8) mod (Fermat 4) = 6561

proof end;

Lm42: (3 |^ 16) mod (Fermat 4) = (164 * 332) + 1

proof end;

Lm43: (3 |^ 32) mod (Fermat 4) = 123 * 503

proof end;

Lm44: (3 |^ 64) mod (Fermat 4) = (14 * 1367) + 1

proof end;

Lm45: (3 |^ 128) mod (Fermat 4) = 52 * 289

proof end;

Lm46: (3 |^ 256) mod (Fermat 4) = 282

proof end;

Lm47: (3 |^ (256 * 2)) mod (Fermat 4) = 71 * 197

proof end;

Lm48: (3 |^ (256 * 4)) mod (Fermat 4) = 32 * 257

proof end;

Lm49: (3 |^ (256 * 8)) mod (Fermat 4) = 81 * 809

proof end;

Lm50: (3 |^ (256 * 16)) mod (Fermat 4) = 64

proof end;

Lm51: (3 |^ (256 * 32)) mod (Fermat 4) = 256 * 16

proof end;

Lm52: (3 |^ (256 * 64)) mod (Fermat 4) = 673 * 97

proof end;

Lm53: (3 |^ (256 * 128)) mod (Fermat 4) = 256 * 256

proof end;

Lm54: Fermat 3 divides (3 |^ ((32 * 0) + 128)) + 1

proof end;

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