:: 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-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, NAT_1, INT_1, XXREAL_0, RELAT_1, ARYTM_3, CARD_1, NEWTON, ARYTM_1, INT_2, SUBSET_1, SQUARE_1, ORDINAL1, ABIAN, POWER, EULER_1, TARSKI, SETWOP_2, FINSET_1, XBOOLE_0, PEPIN, REAL_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, INT_1, INT_2, NAT_1, NAT_D, SETWOP_2, POWER, ABIAN, SQUARE_1, NEWTON, EULER_1, FINSET_1, XXREAL_0; constructors SQUARE_1, NAT_1, NAT_D, SETWOP_2, NEWTON, SERIES_1, BINARITH, EULER_1, ABIAN, VALUED_1, XXREAL_2; registrations ORDINAL1, FINSET_1, FINSUB_1, XXREAL_0, XREAL_0, NAT_1, INT_1, NEWTON, ABIAN, SERIES_1, POWER, CARD_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Some selected Basic Theorems reserve d,i,j,k,m,n,p,q,x,k1,k2 for Nat, a,c,i1,i2,i3,i5 for Integer; theorem :: PEPIN:1 for i being Nat holds i,i+1 are_coprime; theorem :: PEPIN:2 for p being Nat holds p is prime implies m,p are_coprime or m gcd p = p; theorem :: PEPIN:3 for k,m,n being Nat holds k divides n*m & n,k are_coprime implies k divides m; theorem :: PEPIN:4 n divides m & k divides m & n,k are_coprime implies (n*k) divides m; registration let i be Integer; cluster i^2 -> natural; end; theorem :: PEPIN:5 c > 1 implies 1 mod c = 1; theorem :: PEPIN:6 for i,n be Nat st i <> 0 holds i divides n iff n mod i = 0; theorem :: PEPIN:7 for m,n being Nat holds m <> 0 & m divides n mod m implies m divides n; theorem :: PEPIN:8 for m,n,k being Nat holds 0 < n & m mod n = k implies n divides (m - k); theorem :: PEPIN:9 i*p <> 0 & k mod i*p < p implies k mod i*p = k mod p; theorem :: PEPIN:10 (a*p + 1) mod p = 1 mod p; theorem :: PEPIN:11 1 < m & (n*k) mod m = k mod m & k,m are_coprime implies n mod m = 1; theorem :: PEPIN:12 (p |^ k) mod m = ((p mod m) |^ k) mod m; theorem :: PEPIN:13 i <> 0 implies i^2 mod (i+1) = 1; theorem :: PEPIN:14 k^2 < j & i mod j = k implies i^2 mod j = k^2; theorem :: PEPIN:15 p is prime & i mod p = -1 implies i^2 mod p = 1; theorem :: PEPIN:16 n is even implies n + 1 is odd; theorem :: PEPIN:17 for p being Nat holds p > 2 & p is prime implies p is odd; theorem :: PEPIN:18 n > 0 implies 2 to_power(n) is even; theorem :: PEPIN:19 i is odd & j is odd implies i*j is odd; theorem :: PEPIN:20 i is odd implies i |^ k is odd; theorem :: PEPIN:21 k > 0 & i is even implies i |^ k is even; theorem :: PEPIN:22 2 divides n iff n is even; theorem :: PEPIN:23 m*n is even implies m is even or n is even; theorem :: PEPIN:24 n |^ 2 = n^2; theorem :: PEPIN:25 m > 1 & n > 0 implies m |^ n > 1; theorem :: PEPIN:26 n <> 0 & p <> 0 implies n |^ p = n*(n |^ (p -'1)); theorem :: PEPIN:27 for n,m st m mod 2 = 0 holds (n |^ (m div 2))^2 = n |^ m; theorem :: PEPIN:28 n <> 0 & 1 <= k implies (n |^ k) div n = n |^ (k -'1); theorem :: PEPIN:29 2 |^ (n + 1) = (2 |^ n)+(2 |^ n); theorem :: PEPIN:30 k > 1 & k |^ n = k |^ m implies n = m; theorem :: PEPIN:31 m <= n iff 2 |^ m divides 2 |^ n; theorem :: PEPIN:32 p is prime & i divides p |^ n implies i = 1 or ex k being Element of NAT st i = p*k; theorem :: PEPIN:33 for n st p is prime & n < p |^ (k+1) holds n divides p |^ (k+1) iff n divides p |^ k; theorem :: PEPIN:34 for k holds p is prime & d divides (p |^ k) implies ex t being Element of NAT st d = p |^ t & t <= k; theorem :: PEPIN:35 p > 1 & i mod p = 1 implies (i |^ n) mod p = 1; theorem :: PEPIN:36 for m,n being Nat holds m > 0 implies (n |^ m) mod n = 0; theorem :: PEPIN:37 for p being Nat holds p is prime & n,p are_coprime implies (n |^ (p -'1)) mod p = 1; theorem :: PEPIN:38 p is prime & d > 1 & d divides (p |^ k) & not d divides ((p |^ k ) div p) implies d = p |^ k; definition let i be Integer; redefine func i^2 -> Element of NAT; end; theorem :: PEPIN:39 for n st n > 1 holds m mod n = 1 iff m,1 are_congruent_mod n; theorem :: PEPIN:40 i1,i2 are_congruent_mod i5 & i1,i3 are_congruent_mod i5 implies i2,i3 are_congruent_mod i5; theorem :: PEPIN:41 3 is prime; theorem :: PEPIN:42 n <> 0 implies Euler n <> 0; theorem :: PEPIN:43 n <> 0 implies -n < n; theorem :: PEPIN:44 n <> 0 implies n div n = 1; begin :: Public Key Cryptography definition let k,m,n; func Crypto(m,n,k) -> Element of NAT equals :: PEPIN:def 1 (m |^ k) mod n; end; theorem :: PEPIN:45 p is prime & q is prime & p <> q & n = p*q & k1,Euler(n) are_coprime & (k1*k2) mod Euler(n) = 1 implies for m be Element of NAT st m < n holds Crypto(Crypto(m,n,k1),n,k2) = m; begin :: Order definition let i,p; assume that p > 1 and i,p are_coprime; func order(i,p) -> Element of NAT means :: PEPIN:def 2 it > 0 & (i |^ it) mod p = 1 & for k st k > 0 & (i |^ k) mod p = 1 holds 0 < it & it <= k; end; theorem :: PEPIN:46 p > 1 implies order(1,p) = 1; theorem :: PEPIN:47 p > 1 & (i |^ n) mod p = 1 & i,p are_coprime implies order(i,p) divides n; theorem :: PEPIN:48 p > 1 & i,p are_coprime & order(i,p) divides n implies (i |^ n) mod p = 1; theorem :: PEPIN:49 p is prime & i,p are_coprime implies order(i,p) divides ( p -'1); begin :: Fermat Number definition let n be Nat; func Fermat(n) -> Element of NAT equals :: PEPIN:def 3 2 |^ (2 |^ n) + 1; end; theorem :: PEPIN:50 Fermat(0) = 3; theorem :: PEPIN:51 Fermat(1) = 5; theorem :: PEPIN:52 Fermat(2) = 17; theorem :: PEPIN:53 Fermat(3) = 257; theorem :: PEPIN:54 Fermat(4) = 256*256+1; theorem :: PEPIN:55 Fermat(n) > 2; theorem :: PEPIN:56 p is prime & p > 2 & p divides Fermat(n) implies ex k being Element of NAT st p = k*(2 |^ (n + 1)) + 1; theorem :: PEPIN:57 n <> 0 implies 3,Fermat(n) are_coprime; begin :: Pepin's Test ::\$N Pepin's test theorem :: PEPIN:58 (3 |^ ((Fermat(n)-'1) div 2)),(-1) are_congruent_mod Fermat(n) implies Fermat(n) is prime; theorem :: PEPIN:59 5 is prime; theorem :: PEPIN:60 17 is prime; theorem :: PEPIN:61 257 is prime; theorem :: PEPIN:62 256*256+1 is prime; :: Moved from JORDAN1A, AK, 21.02.2006 theorem :: PEPIN:63 for i,j being Integer holds j <> 0 & i mod j = 0 implies i div j = i / j; theorem :: PEPIN:64 for i,n being Nat st n > 0 holds i |^ n div i = i |^ n / i; reserve r for Real; theorem :: PEPIN:65 for n being Nat holds 0 < n & 1 < r implies 1 < r|^n; theorem :: PEPIN:66 for m,n being Nat holds r > 1 & m > n implies r|^m > r|^n;