:: PEPIN semantic presentation

Lemma1: for b₁, b₂ being Integer
for b₃, b₄ being Nat st b₁ = b₃ & b₂ = b₄ holds
( b₁ divides b₂ iff b₃ divides b₄ )

proof end;

Lemma2: for b₁ being Nat
for b₂ being Integer st b₁ > 1 & b₁ * b₂ > 0 holds
b₂ > 0
by XREAL_1:133;

Lemma3: for b₁, b₂, b₃ being Nat st b₁ > 1 & b₂ >= 1 & b₃ >= 0 & 1 = (((b₂ * b₃) * b₁) + b₂) + b₃ holds
( b₂ = 1 & b₃ = 0 )

proof end;

Lemma4: for b₁ being Nat holds 2 |^ (2 |^ b₁) > 1

proof end;

Lemma5: for b₁ being Nat st b₁ <> 0 holds
b₁ - 1 >= 0

proof end;

Lemma6: for b₁ being Nat st b₁ <> 0 holds
(b₁ -' 1) + 1 = (b₁ + 1) -' 1

proof end;

theorem Th1: :: PEPIN:1

for b₁ being Nat holds b₁,b₁ + 1 are_relative_prime

proof end;

theorem Th2: :: PEPIN:2

for b₁, b₂ being Nat holds
( not b₁ is prime or b₂,b₁ are_relative_prime or b₂ hcf b₁ = b₁ )

proof end;

theorem Th3: :: PEPIN:3

for b₁, b₂, b₃ being Nat st b₁ divides b₂ * b₃ & b₂,b₁ are_relative_prime holds
b₁ divides b₃

proof end;

theorem Th4: :: PEPIN:4

for b₁, b₂, b₃ being Nat st b₁ divides b₂ & b₃ divides b₂ & b₁,b₃ are_relative_prime holds
b₁ * b₃ divides b₂

proof end;

definition

let c₁ be Nat;
redefine func ^2 as c₁ ^2 -> Nat;
coherence

proof end;

end;

theorem Th5: :: PEPIN:5

for b₁ being Integer st b₁ > 1 holds
1 mod b₁ = 1

proof end;

theorem Th6: :: PEPIN:6

for b₁, b₂ being Nat st b₂ <> 0 holds
( b₂ divides b₁ iff b₁ mod b₂ = 0 )

proof end;

theorem Th7: :: PEPIN:7

for b₁, b₂ being Nat st b₁ <> 0 & b₁ divides b₂ mod b₁ holds
b₁ divides b₂

proof end;

theorem Th8: :: PEPIN:8

for b₁, b₂, b₃ being Nat st 0 < b₁ & b₂ mod b₁ = b₃ holds
b₁ divides b₂ - b₃

proof end;

theorem Th9: :: PEPIN:9

for b₁, b₂, b₃ being Nat st b₁ * b₂ <> 0 & b₂ is prime & b₃ mod (b₁ * b₂) < b₂ holds
b₃ mod (b₁ * b₂) = b₃ mod b₂

proof end;

theorem Th10: :: PEPIN:10

for b₁ being Nat
for b₂ being Integer holds ((b₂ * b₁) + 1) mod b₁ = 1 mod b₁

proof end;

theorem Th11: :: PEPIN:11

for b₁, b₂, b₃ being Nat st 1 < b₁ & (b₂ * b₃) mod b₁ = b₃ mod b₁ & b₃,b₁ are_relative_prime holds
b₂ mod b₁ = 1

proof end;

theorem Th12: :: PEPIN:12

for b₁, b₂, b₃ being Nat holds (b₁ |^ b₂) mod b₃ = ((b₁ mod b₃) |^ b₂) mod b₃

proof end;

Lemma15: for b₁, b₂ being Nat holds (b₁ * (2 |^ (b₂ + 1))) div 2 = b₁ * (2 |^ b₂)

proof end;

Lemma16: for b₁, b₂, b₃ being Nat st b₁ <= b₂ holds
b₃ |^ b₁ divides b₃ |^ b₂

proof end;

Lemma17: 2 |^ 2 = 4

proof end;

Lemma18: 2 |^ 3 = 8

proof end;

Lemma19: 2 |^ 4 = 16

proof end;

Lemma20: 2 |^ 8 = 256

proof end;

theorem Th13: :: PEPIN:13

for b₁ being Nat st b₁ <> 0 holds
(b₁ ^2 ) mod (b₁ + 1) = 1

proof end;

theorem Th14: :: PEPIN:14

for b₁, b₂, b₃ being Nat st b₁ ^2 < b₂ & b₃ mod b₂ = b₁ holds
(b₃ ^2 ) mod b₂ = b₁ ^2

proof end;

theorem Th15: :: PEPIN:15

for b₁, b₂ being Nat st b₁ is prime & b₂ mod b₁ = - 1 holds
(b₂ ^2 ) mod b₁ = 1

proof end;

theorem Th16: :: PEPIN:16

for b₁ being Nat st b₁ is even holds
not b₁ + 1 is even

proof end;

theorem Th17: :: PEPIN:17

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

proof end;

theorem Th18: :: PEPIN:18

for b₁ being Nat st b₁ > 0 holds
2 to_power b₁ is even

proof end;

Lemma22: for b₁, b₂ being Nat st b₁ is even & b₂ is even holds
b₁ * b₂ is even

proof end;

theorem Th19: :: PEPIN:19

for b₁, b₂ being Nat st not b₁ is even & not b₂ is even holds
not b₁ * b₂ is even

proof end;

theorem Th20: :: PEPIN:20

for b₁, b₂ being Nat st not b₁ is even holds
not b₁ |^ b₂ is even

proof end;

theorem Th21: :: PEPIN:21

for b₁, b₂ being Nat st b₁ > 0 & b₂ is even holds
b₂ |^ b₁ is even

proof end;

theorem Th22: :: PEPIN:22

for b₁ being Nat holds
( 2 divides b₁ iff b₁ is even )

proof end;

theorem Th23: :: PEPIN:23

for b₁, b₂ being Nat holds
( not b₁ * b₂ is even or b₁ is even or b₂ is even ) by Th19;

theorem Th24: :: PEPIN:24

for b₁ being Nat holds b₁ |^ 2 = b₁ ^2

proof end;

theorem Th25: :: PEPIN:25

canceled;

theorem Th26: :: PEPIN:26

for b₁, b₂ being Nat st b₁ > 1 & b₂ > 0 holds
b₁ |^ b₂ > 1

proof end;

Lemma27: for b₁ being Nat holds (2 |^ (2 |^ b₁)) ^2 = 2 |^ (2 |^ (b₁ + 1))

proof end;

theorem Th27: :: PEPIN:27

for b₁, b₂ being Nat st b₁ <> 0 & b₂ <> 0 holds
b₁ |^ b₂ = b₁ * (b₁ |^ (b₂ -' 1))

proof end;

theorem Th28: :: PEPIN:28

for b₁, b₂ being Nat st b₂ mod 2 = 0 holds
(b₁ |^ (b₂ div 2)) ^2 = b₁ |^ b₂

proof end;

theorem Th29: :: PEPIN:29

for b₁, b₂ being Nat st b₁ <> 0 & 1 <= b₂ holds
(b₁ |^ b₂) div b₁ = b₁ |^ (b₂ -' 1)

proof end;

theorem Th30: :: PEPIN:30

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

proof end;

theorem Th31: :: PEPIN:31

for b₁, b₂, b₃ being Nat st b₁ > 1 & b₁ |^ b₂ = b₁ |^ b₃ holds
b₂ = b₃

proof end;

Lemma32: for b₁, b₂, b₃ being Nat st b₁ > b₂ & b₃ > 1 holds
b₃ |^ b₁ > b₃ |^ b₂

proof end;

Lemma33: for b₁, b₂ being Nat st 2 |^ b₁ divides 2 |^ b₂ holds
b₁ <= b₂

proof end;

theorem Th32: :: PEPIN:32

for b₁, b₂ being Nat holds
( b₁ <= b₂ iff 2 |^ b₁ divides 2 |^ b₂ ) by Lemma16, Lemma33;

theorem Th33: :: PEPIN:33

for b₁, b₂, b₃ being Nat st b₁ is prime & b₂ divides b₁ |^ b₃ & not b₂ = 1 holds
ex b₄ being Nat st b₂ = b₁ * b₄

proof end;

theorem Th34: :: PEPIN:34

for b₁, b₂, b₃ being Nat st b₃ <> 0 & b₁ is prime & b₃ < b₁ |^ (b₂ + 1) holds
( b₃ divides b₁ |^ (b₂ + 1) iff b₃ divides b₁ |^ b₂ )

proof end;

theorem Th35: :: PEPIN:35

for b₁, b₂, b₃ being Nat st b₁ is prime & b₂ divides b₁ |^ b₃ & b₂ <> 0 holds
ex b₄ being Nat st
( b₂ = b₁ |^ b₄ & b₄ <= b₃ )

proof end;

theorem Th36: :: PEPIN:36

for b₁, b₂, b₃ being Nat st b₁ > 1 & b₂ mod b₁ = 1 holds
(b₂ |^ b₃) mod b₁ = 1

proof end;

theorem Th37: :: PEPIN:37

for b₁, b₂ being natural number st b₁ > 0 holds
(b₂ |^ b₁) mod b₂ = 0

proof end;

theorem Th38: :: PEPIN:38

for b₁, b₂ being Nat st b₁ is prime & b₂,b₁ are_relative_prime holds
(b₂ |^ (b₁ -' 1)) mod b₁ = 1

proof end;

theorem Th39: :: PEPIN:39

for b₁, b₂, b₃ being Nat st b₁ is prime & b₂ > 1 & b₂ divides b₁ |^ b₃ & not b₂ divides (b₁ |^ b₃) div b₁ holds
b₂ = b₁ |^ b₃

proof end;

definition

let c₁ be Integer;
redefine func ^2 as c₁ ^2 -> Nat;
coherence

proof end;

end;

theorem Th40: :: PEPIN:40

for b₁, b₂ being Nat st b₂ > 1 holds
( b₁ mod b₂ = 1 iff b₁,1 are_congruent_mod b₂ )

proof end;

Lemma41: for b₁, b₂ being Nat st b₁ > 1 & b₂ > 1 & b₂,1 are_congruent_mod b₁ holds
b₂ mod b₁ = 1

proof end;

theorem Th41: :: PEPIN:41

for b₁, b₂, b₃ being Integer st b₁,b₂ are_congruent_mod b₃ holds
b₁ ^2 ,b₂ ^2 are_congruent_mod b₃ by INT_1:39;

theorem Th42: :: PEPIN:42

canceled;

theorem Th43: :: PEPIN:43

for b₁, b₂, b₃, b₄ being Integer st b₁,b₂ are_congruent_mod b₃ & b₁,b₄ are_congruent_mod b₃ holds
b₂,b₄ are_congruent_mod b₃

proof end;

theorem Th44: :: PEPIN:44

3 is prime

proof end;

theorem Th45: :: PEPIN:45

for b₁ being Nat st b₁ <> 0 holds
Euler b₁ <> 0

proof end;

theorem Th46: :: PEPIN:46

for b₁ being Nat st b₁ <> 0 holds
- b₁ < b₁ ;

theorem Th47: :: PEPIN:47

canceled;

theorem Th48: :: PEPIN:48

for b₁ being Nat st b₁ <> 0 holds
b₁ div b₁ = 1

proof end;

definition

let c₁, c₂, c₃ be Nat;
func Crypto c₂,c₃,c₁ -> Nat equals :: PEPIN:def 1
(a₂ |^ a₁) mod a₃;
coherence ;

end;

:: deftheorem Def1 defines Crypto PEPIN:def 1 :

theorem Th49: :: PEPIN:49

for b₁, b₂, b₃, b₄, b₅ being Nat st b₁ is prime & b₂ is prime & b₁ <> b₂ & b₃ = b₁ * b₂ & b₄, Euler b₃ are_relative_prime & (b₄ * b₅) mod (Euler b₃) = 1 holds
for b₆ being Nat st b₆ < b₃ holds
Crypto (Crypto b₆,b₃,b₄),b₃,b₅ = b₆

proof end;

definition

let c₁, c₂ be Nat;
assume E47: ( c₂ > 1 & c₁,c₂ are_relative_prime ) ;
func order c₁,c₂ -> Nat means :Def2: :: PEPIN:def 2
( a₃ > 0 & (a₁ |^ a₃) mod a₂ = 1 & ( for b₁ being Nat st b₁ > 0 & (a₁ |^ b₁) mod a₂ = 1 holds
( 0 < a₃ & a₃ <= b₁ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines order PEPIN:def 2 :

theorem Th50: :: PEPIN:50

for b₁ being Nat st b₁ > 1 holds
order 1,b₁ = 1

proof end;

theorem Th51: :: PEPIN:51

canceled;

theorem Th52: :: PEPIN:52

for b₁, b₂, b₃ being Nat st b₁ > 1 & b₂ > 0 & (b₃ |^ b₂) mod b₁ = 1 & b₃,b₁ are_relative_prime holds
order b₃,b₁ divides b₂

proof end;

theorem Th53: :: PEPIN:53

for b₁, b₂, b₃ being Nat st b₁ > 1 & b₂,b₁ are_relative_prime & order b₂,b₁ divides b₃ holds
(b₂ |^ b₃) mod b₁ = 1

proof end;

theorem Th54: :: PEPIN:54

for b₁, b₂ being Nat st b₁ is prime & b₂,b₁ are_relative_prime holds
order b₂,b₁ divides b₁ -' 1

proof end;

definition

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

end;

:: deftheorem Def3 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 b₁ being Nat holds Fermat b₁ > 2

proof end;

Lemma57: for b₁ being Nat holds Fermat b₁ > 1

proof end;

Lemma58: for b₁ being Nat holds ((Fermat b₁) -' 1) mod 2 = 0

proof end;

Lemma59: for b₁ being Nat holds (Fermat b₁) -' 1 > 0

proof end;

Lemma60: for b₁ being Nat holds (Fermat b₁) mod (2 |^ (2 |^ b₁)) = 1

proof end;

Lemma61: for b₁ being Nat holds not Fermat b₁ is even

proof end;

theorem Th61: :: PEPIN:61

for b₁, b₂ being Nat st b₁ is prime & b₁ > 2 & b₁ divides Fermat b₂ holds
ex b₃ being Nat st b₁ = (b₃ * (2 |^ (b₂ + 1))) + 1

proof end;

theorem Th62: :: PEPIN:62

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

proof end;

theorem Th63: :: PEPIN:63

for b₁ being Nat st 3 |^ (((Fermat b₁) -' 1) div 2), - 1 are_congruent_mod Fermat b₁ holds
Fermat b₁ is prime

proof end;

Lemma65: 3 |^ 2 = 9

proof end;

Lemma66: 3 |^ 4 = 81

proof end;

Lemma67: 3 |^ 8 = 6561

proof end;

Lemma68: 3 |^ 16 = 6561 * 6561

proof end;

Lemma69: for b₁ being Nat holds Fermat 1 divides (3 |^ ((4 * b₁) + 2)) + 1

proof end;

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

proof end;

Lemma71: for b₁ being Nat holds Fermat 2 divides (3 |^ ((16 * b₁) + 8)) + 1

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

Lemma97: Fermat 4 divides (3 |^ ((64 * 0) + (256 * 128))) + 1

proof end;

theorem Th64: :: PEPIN:64

5 is prime

proof end;

theorem Th65: :: PEPIN:65

17 is prime

proof end;

theorem Th66: :: PEPIN:66

257 is prime

proof end;

theorem Th67: :: PEPIN:67

(256 * 256) + 1 is prime

proof end;