:: Public-Key Cryptography and Pepin's Test for the Primality ofFermat Numbers
:: by Yoshinori Fujisawa , Yasushi Fuwa and Hidetaka Shimizu
::
:: Received December 21, 1998
:: Copyright (c) 1998 Association of Mizar Users
Lm1:
for n, x, y being Nat st n > 1 & x >= 1 & y >= 0 & 1 = (((x * y) * n) + x) + y holds
( x = 1 & y = 0 )
Lm2:
for n being Nat holds 2 |^ (2 |^ n) > 1
Lm3:
for n being Nat st n <> 0 holds
n - 1 >= 0
Lm4:
for n being Nat st n <> 0 holds
(n -' 1) + 1 = (n + 1) -' 1
theorem :: PEPIN:1
theorem Th2: :: PEPIN:2
theorem Th3: :: PEPIN:3
theorem Th4: :: PEPIN:4
theorem :: PEPIN:5
theorem Th6: :: PEPIN:6
theorem Th7: :: PEPIN:7
theorem :: PEPIN:8
theorem :: PEPIN:9
theorem Th10: :: PEPIN:10
theorem Th11: :: PEPIN:11
theorem Th12: :: PEPIN:12
Lm5:
for k, n being Nat holds (k * (2 |^ (n + 1))) div 2 = k * (2 |^ n)
Lm6:
for k, n, m being Nat st k <= n holds
m |^ k divides m |^ n
Lm8:
2 |^ 3 = 8
by POWER:69;
Lm9:
2 |^ 4 = 16
by POWER:70;
Lm10:
2 |^ 8 = 256
theorem :: PEPIN:13
theorem :: PEPIN:14
theorem :: PEPIN:15
theorem :: PEPIN:16
theorem :: PEPIN:17
theorem :: PEPIN:18
theorem :: PEPIN:19
theorem :: PEPIN:20
theorem Th21: :: PEPIN:21
theorem :: PEPIN:22
theorem :: PEPIN:23
theorem Th24: :: PEPIN:24
theorem :: PEPIN:25
canceled;
theorem Th26: :: PEPIN:26
for
m,
n being
Nat st
m > 1 &
n > 0 holds
m |^ n > 1
Lm12:
for n being Nat holds (2 |^ (2 |^ n)) ^2 = 2 |^ (2 |^ (n + 1))
theorem Th27: :: PEPIN:27
theorem Th28: :: PEPIN:28
theorem Th29: :: PEPIN:29
theorem :: PEPIN:30
theorem Th31: :: PEPIN:31
for
k,
n,
m being
Nat st
k > 1 &
k |^ n = k |^ m holds
n = m
Lm13:
for k, n, x being Nat st k > n & x > 1 holds
x |^ k > x |^ n
Lm14:
for m, n being Nat st 2 |^ m divides 2 |^ n holds
m <= n
theorem :: PEPIN:32
theorem Th33: :: PEPIN:33
theorem Th34: :: PEPIN:34
theorem Th35: :: PEPIN:35
theorem Th36: :: PEPIN:36
theorem Th37: :: PEPIN:37
theorem Th38: :: PEPIN:38
theorem Th39: :: PEPIN:39
theorem Th40: :: PEPIN:40
Lm15:
for n, m being Nat st n > 1 & m > 1 & m,1 are_congruent_mod n holds
m mod n = 1
theorem :: PEPIN:41
canceled;
theorem :: PEPIN:42
canceled;
theorem Th43: :: PEPIN:43
theorem Th44: :: PEPIN:44
theorem Th45: :: PEPIN:45
theorem :: PEPIN:46
for
n being
Nat st
n <> 0 holds
- n < n ;
theorem :: PEPIN:47
canceled;
theorem Th48: :: PEPIN:48
:: deftheorem defines Crypto PEPIN:def 1 :
theorem :: PEPIN:49
:: deftheorem Def2 defines order PEPIN:def 2 :
theorem :: PEPIN:50
theorem :: PEPIN:51
canceled;
theorem Th52: :: PEPIN:52
theorem Th53: :: PEPIN:53
theorem Th54: :: PEPIN:54
:: deftheorem defines Fermat PEPIN:def 3 :
theorem Th55: :: PEPIN:55
theorem Th56: :: PEPIN:56
theorem Th57: :: PEPIN:57
theorem Th58: :: PEPIN:58
theorem Th59: :: PEPIN:59
theorem Th60: :: PEPIN:60
Lm16:
for n being Nat holds Fermat n > 1
Lm17:
for n being Nat holds ((Fermat n) -' 1) mod 2 = 0
Lm18:
for n being Nat holds (Fermat n) -' 1 > 0
Lm19:
for n being Nat holds (Fermat n) mod (2 |^ (2 |^ n)) = 1
Lm20:
for n being Nat holds not Fermat n is even
theorem Th61: :: PEPIN:61
theorem Th62: :: PEPIN:62
theorem Th63: :: PEPIN:63
Lm21:
3 |^ 2 = 9
Lm22:
3 |^ 4 = 81
Lm23:
3 |^ 8 = 6561
Lm24:
3 |^ 16 = 6561 * 6561
Lm25:
for i being Nat holds Fermat 1 divides (3 |^ ((4 * i) + 2)) + 1
Lm26:
for n being Nat st n = 1 holds
3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n
Lm27:
for n being Nat holds Fermat 2 divides (3 |^ ((16 * n) + 8)) + 1
Lm28:
(3 |^ 1) mod (Fermat 3) = 3
Lm29:
(3 |^ 2) mod (Fermat 3) = 9
Lm30:
(3 |^ 4) mod (Fermat 3) = 81
Lm31:
(3 |^ 8) mod (Fermat 3) = 136
Lm32:
(3 |^ 16) mod (Fermat 3) = 83 * 3
Lm33:
(3 |^ 32) mod (Fermat 3) = 64
Lm34:
(3 |^ 64) mod (Fermat 3) = 241
Lm35:
(3 |^ 128) mod (Fermat 3) = 256
Lm36:
(3 |^ 1) mod (Fermat 4) = 3
Lm37:
(3 |^ 2) mod (Fermat 4) = 9
Lm38:
(3 |^ 4) mod (Fermat 4) = 81
Lm39:
(3 |^ 8) mod (Fermat 4) = 6561
Lm40:
(3 |^ 16) mod (Fermat 4) = (164 * 332) + 1
Lm41:
(3 |^ 32) mod (Fermat 4) = 123 * 503
Lm42:
(3 |^ 64) mod (Fermat 4) = (14 * 1367) + 1
Lm43:
(3 |^ 128) mod (Fermat 4) = 52 * 289
Lm44:
(3 |^ 256) mod (Fermat 4) = 282
Lm45:
(3 |^ (256 * 2)) mod (Fermat 4) = 71 * 197
Lm46:
(3 |^ (256 * 4)) mod (Fermat 4) = 32 * 257
Lm47:
(3 |^ (256 * 8)) mod (Fermat 4) = 81 * 809
Lm48:
(3 |^ (256 * 16)) mod (Fermat 4) = 64
Lm49:
(3 |^ (256 * 32)) mod (Fermat 4) = 256 * 16
Lm50:
(3 |^ (256 * 64)) mod (Fermat 4) = 673 * 97
Lm51:
(3 |^ (256 * 128)) mod (Fermat 4) = 256 * 256
Lm52:
Fermat 3 divides (3 |^ ((32 * 0 ) + 128)) + 1
Lm53:
Fermat 4 divides (3 |^ ((64 * 0 ) + (256 * 128))) + 1
theorem :: PEPIN:64
theorem :: PEPIN:65
theorem :: PEPIN:66
theorem :: PEPIN:67
theorem Th68: :: PEPIN:68
theorem :: PEPIN:69
theorem Th70: :: PEPIN:70
theorem :: PEPIN:71