:: 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 ) proofend; Lm2: for n being Nat holds 2 |^ (2 |^ n) > 1 proofend; Lm3: for n being Nat st n <> 0 holds n - 1 >= 0 proofend; Lm4: for n being Nat st n <> 0 holds (n -' 1) + 1 = (n + 1) -' 1 proofend; theorem :: PEPIN:1 for i being Nat holds i,i + 1 are_relative_prime proofend; 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 ) proofend; theorem Th3: :: PEPIN:3 for k, m, n being Nat st k divides n * m & n,k are_relative_prime holds k divides m proofend; 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 proofend; registration let i be Integer; clusteri ^2 -> natural ; coherence i ^2 is natural proofend; end; theorem :: PEPIN:5 for c being Integer st c > 1 holds 1 mod c = 1 proofend; theorem Th6: :: PEPIN:6 for i, n being Nat st i <> 0 holds ( i divides n iff n mod i = 0 ) proofend; theorem Th7: :: PEPIN:7 for m, n being Nat st m <> 0 & m divides n mod m holds m divides n proofend; theorem :: PEPIN:8 for m, n, k being Nat st 0 < n & m mod n = k holds n divides m - k proofend; 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 proofend; theorem Th10: :: PEPIN:10 for p being Nat for a being Integer holds ((a * p) + 1) mod p = 1 mod p proofend; 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 proofend; theorem Th12: :: PEPIN:12 for p, k, m being Nat holds (p |^ k) mod m = ((p mod m) |^ k) mod m proofend; Lm5: for k, n being Nat holds (k * (2 |^ (n + 1))) div 2 = k * (2 |^ n) proofend; Lm6: for k, n, m being Nat st k <= n holds m |^ k divides m |^ n proofend; Lm7: 2 |^ 8 = 256 proofend; theorem :: PEPIN:13 for i being Nat st i <> 0 holds (i ^2) mod (i + 1) = 1 proofend; theorem :: PEPIN:14 for k, j, i being Nat st k ^2 < j & i mod j = k holds (i ^2) mod j = k ^2 proofend; theorem :: PEPIN:15 for p, i being Nat st p is prime & i mod p = - 1 holds (i ^2) mod p = 1 proofend; 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 proofend; theorem :: PEPIN:18 for n being Nat st n > 0 holds 2 to_power n is even proofend; 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 proofend; theorem Th21: :: PEPIN:21 for k, i being Nat st k > 0 & i is even holds i |^ k is even proofend; theorem :: PEPIN:22 for n being Nat holds ( 2 divides n iff n is even ) proofend; 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 proofend; theorem Th25: :: PEPIN:25 for m, n being Nat st m > 1 & n > 0 holds m |^ n > 1 proofend; Lm8: for n being Nat holds (2 |^ (2 |^ n)) ^2 = 2 |^ (2 |^ (n + 1)) proofend; theorem Th26: :: PEPIN:26 for n, p being Nat st n <> 0 & p <> 0 holds n |^ p = n * (n |^ (p -' 1)) proofend; theorem Th27: :: PEPIN:27 for n, m being Nat st m mod 2 = 0 holds (n |^ (m div 2)) ^2 = n |^ m proofend; theorem Th28: :: PEPIN:28 for n, k being Nat st n <> 0 & 1 <= k holds (n |^ k) div n = n |^ (k -' 1) proofend; theorem :: PEPIN:29 for n being Nat holds 2 |^ (n + 1) = (2 |^ n) + (2 |^ n) proofend; theorem Th30: :: PEPIN:30 for k, n, m being Nat st k > 1 & k |^ n = k |^ m holds n = m proofend; Lm9: for k, n, x being Nat st k > n & x > 1 holds x |^ k > x |^ n proofend; Lm10: for m, n being Nat st 2 |^ m divides 2 |^ n holds m <= n proofend; 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 proofend; 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 ) proofend; 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 ) proofend; theorem Th35: :: PEPIN:35 for p, i, n being Nat st p > 1 & i mod p = 1 holds (i |^ n) mod p = 1 proofend; theorem Th36: :: PEPIN:36 for m, n being Nat st m > 0 holds (n |^ m) mod n = 0 proofend; 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 proofend; 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 proofend; definition let i be Integer; :: original:^2 redefine funci ^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 ) proofend; Lm11: for n, m being Nat st n > 1 & m > 1 & m,1 are_congruent_mod n holds m mod n = 1 proofend; 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 proofend; theorem Th41: :: PEPIN:41 3 is prime proofend; theorem Th42: :: PEPIN:42 for n being Nat st n <> 0 holds Euler n <> 0 proofend; 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 proofend; 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 proofend; 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 ) ) ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th51: :: PEPIN:51 Fermat 1 = 5 proofend; theorem Th52: :: PEPIN:52 Fermat 2 = 17 proofend; theorem Th53: :: PEPIN:53 Fermat 3 = 257 proofend; theorem Th54: :: PEPIN:54 Fermat 4 = (256 * 256) + 1 proofend; theorem Th55: :: PEPIN:55 for n being Nat holds Fermat n > 2 proofend; Lm12: for n being Nat holds Fermat n > 1 proofend; Lm13: for n being Nat holds ((Fermat n) -' 1) mod 2 = 0 proofend; Lm14: for n being Nat holds (Fermat n) -' 1 > 0 proofend; Lm15: for n being Nat holds (Fermat n) mod (2 |^ (2 |^ n)) = 1 proofend; Lm16: for n being Nat holds Fermat n is odd proofend; 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 proofend; theorem Th57: :: PEPIN:57 for n being Nat st n <> 0 holds 3, Fermat n are_relative_prime proofend; 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 proofend; Lm17: 3 |^ 2 = 9 proofend; Lm18: 3 |^ 4 = 81 proofend; Lm19: 3 |^ 8 = 6561 proofend; Lm20: 3 |^ 16 = 6561 * 6561 proofend; Lm21: for i being Nat holds Fermat 1 divides (3 |^ ((4 * i) + 2)) + 1 proofend; Lm22: for n being Nat st n = 1 holds 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n proofend; Lm23: for n being Nat holds Fermat 2 divides (3 |^ ((16 * n) + 8)) + 1 proofend; Lm24: (3 |^ 1) mod (Fermat 3) = 3 proofend; Lm25: (3 |^ 2) mod (Fermat 3) = 9 proofend; Lm26: (3 |^ 4) mod (Fermat 3) = 81 proofend; Lm27: (3 |^ 8) mod (Fermat 3) = 136 proofend; Lm28: (3 |^ 16) mod (Fermat 3) = 83 * 3 proofend; Lm29: (3 |^ 32) mod (Fermat 3) = 64 proofend; Lm30: (3 |^ 64) mod (Fermat 3) = 241 proofend; Lm31: (3 |^ 128) mod (Fermat 3) = 256 proofend; Lm32: (3 |^ 1) mod (Fermat 4) = 3 proofend; Lm33: (3 |^ 2) mod (Fermat 4) = 9 proofend; Lm34: (3 |^ 4) mod (Fermat 4) = 81 proofend; Lm35: (3 |^ 8) mod (Fermat 4) = 6561 proofend; Lm36: (3 |^ 16) mod (Fermat 4) = (164 * 332) + 1 proofend; Lm37: (3 |^ 32) mod (Fermat 4) = 123 * 503 proofend; Lm38: (3 |^ 64) mod (Fermat 4) = (14 * 1367) + 1 proofend; Lm39: (3 |^ 128) mod (Fermat 4) = 52 * 289 proofend; Lm40: (3 |^ 256) mod (Fermat 4) = 282 proofend; Lm41: (3 |^ (256 * 2)) mod (Fermat 4) = 71 * 197 proofend; Lm42: (3 |^ (256 * 4)) mod (Fermat 4) = 32 * 257 proofend; Lm43: (3 |^ (256 * 8)) mod (Fermat 4) = 81 * 809 proofend; Lm44: (3 |^ (256 * 16)) mod (Fermat 4) = 64 proofend; Lm45: (3 |^ (256 * 32)) mod (Fermat 4) = 256 * 16 proofend; Lm46: (3 |^ (256 * 64)) mod (Fermat 4) = 673 * 97 proofend; Lm47: (3 |^ (256 * 128)) mod (Fermat 4) = 256 * 256 proofend; Lm48: Fermat 3 divides (3 |^ ((32 * 0) + 128)) + 1 proofend; Lm49: Fermat 4 divides (3 |^ ((64 * 0) + (256 * 128))) + 1 proofend; theorem :: PEPIN:59 5 is prime proofend; theorem :: PEPIN:60 17 is prime proofend; theorem :: PEPIN:61 257 is prime proofend; theorem :: PEPIN:62 (256 * 256) + 1 is prime proofend; :: 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 proofend; theorem :: PEPIN:64 for i, n being Nat st n > 0 holds (i |^ n) div i = (i |^ n) / i proofend; theorem Th65: :: PEPIN:65 for r being real number for n being Nat st 0 < n & 1 < r holds 1 < r |^ n proofend; theorem :: PEPIN:66 for r being real number for m, n being Nat st r > 1 & m > n holds r |^ m > r |^ n proofend;