Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### 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
- MML identifier: PEPIN

- [ Mizar article, MML identifier index ]

environ vocabulary EULER_1, NAT_1, SQUARE_1, ARYTM_3, INT_1, FINSET_1, ARYTM_1, ABSVALUE, FILTER_0, MATRIX_2, CARD_1, POWER, FINSEQ_1, PEPIN, RELAT_1, GROUP_1; notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, INT_1, INT_2, NAT_1, CARD_1, SETWOP_2, SERIES_1, BINARITH, ABIAN, SQUARE_1, EULER_1, EULER_2, FINSET_1, GROUP_1; constructors REAL_1, SERIES_1, BINARITH, ABIAN, SQUARE_1, EULER_1, EULER_2, SETWOP_2, GROUP_1, INT_2, MEMBERED; clusters INT_1, XREAL_0, ABIAN, FINSET_1, FINSUB_1, SQUARE_1, MEMBERED, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Some selected Basic Theorems reserve d,i,j,k,m,n,p,q,x,y,n1,n2,k1,k2 for Nat, a,b,c,i1,i2,i3,i5 for Integer; theorem :: PEPIN:1 for i holds i,i+1 are_relative_prime; theorem :: PEPIN:2 for p holds p is prime implies m,p are_relative_prime or m hcf p = p; theorem :: PEPIN:3 k divides n*m & n,k are_relative_prime implies k divides m; theorem :: PEPIN:4 n divides m & k divides m & n,k are_relative_prime implies (n*k) divides m; definition let n be Nat; redefine func n^2 -> Nat; end; theorem :: PEPIN:5 c > 1 implies 1 mod c = 1; theorem :: PEPIN:6 for i st i <> 0 holds i divides n iff n mod i = 0; theorem :: PEPIN:7 m <> 0 & m divides n mod m implies m divides n; theorem :: PEPIN:8 0 < n & m mod n = k implies n divides (m - k); theorem :: PEPIN:9 i*p <> 0 & p is prime & 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_relative_prime 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 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 for k holds 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; canceled; theorem :: PEPIN:26 m > 1 & n > 0 implies m |^ n > 1; theorem :: PEPIN:27 n <> 0 & p <> 0 implies n |^ p = n*(n |^ (p -'1)); theorem :: PEPIN:28 for n,m st m mod 2 = 0 holds (n |^ (m div 2))^2 = n |^ m; theorem :: PEPIN:29 n <> 0 & 1 <= k implies (n |^ k) div n = n |^ (k -'1); theorem :: PEPIN:30 2 |^ (n + 1) = (2 |^ n)+(2 |^ n); theorem :: PEPIN:31 k > 1 & k |^ n = k |^ m implies n = m; theorem :: PEPIN:32 m <= n iff 2 |^ m divides 2 |^ n; theorem :: PEPIN:33 p is prime & i divides p |^ n implies i = 1 or (ex k being Nat st i = p*k); theorem :: PEPIN:34 for n st n <> 0 & p is prime & n < p |^ (k+1) holds n divides p |^ (k+1) iff n divides p |^ k; theorem :: PEPIN:35 for k holds p is prime & d divides (p |^ k) & d <> 0 implies ex t being Nat st d = p |^ t & t <= k; theorem :: PEPIN:36 p > 1 & i mod p = 1 implies (i |^ n) mod p = 1; theorem :: PEPIN:37 m > 0 implies (n |^ m) mod n = 0; theorem :: PEPIN:38 p is prime & n,p are_relative_prime implies (n |^ (p -'1)) mod p = 1; theorem :: PEPIN:39 p is prime & d > 1 & d divides (p |^ k) & not d divides ((p |^ k) div p) implies d = p |^ k; definition let a be Integer; redefine func a^2 -> Nat; end; theorem :: PEPIN:40 for n st n > 1 holds m mod n = 1 iff m,1 are_congruent_mod n; theorem :: PEPIN:41 a,b are_congruent_mod c implies a^2,b^2 are_congruent_mod c; canceled; theorem :: PEPIN:43 i1,i2 are_congruent_mod i5 & i1,i3 are_congruent_mod i5 implies i2,i3 are_congruent_mod i5; theorem :: PEPIN:44 3 is prime; theorem :: PEPIN:45 n <> 0 implies Euler n <> 0; theorem :: PEPIN:46 n <> 0 implies -n < n; canceled; theorem :: PEPIN:48 n <> 0 implies n div n = 1; begin :: Public Key Cryptography definition let k,m,n; func Crypto(m,n,k) -> Nat equals :: PEPIN:def 1 (m |^ k) mod n; end; theorem :: PEPIN:49 p is prime & q is prime & p <> q & n = p*q & k1,Euler(n) are_relative_prime & (k1*k2) mod Euler(n) = 1 implies for m be Nat st m < n holds Crypto(Crypto(m,n,k1),n,k2) = m; begin :: Order definition let i,p; assume p > 1 & i,p are_relative_prime; func order(i,p) -> 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:50 p > 1 implies order(1,p) = 1; canceled; theorem :: PEPIN:52 p > 1 & n > 0 & (i |^ n) mod p = 1 & i,p are_relative_prime implies order(i,p) divides n; theorem :: PEPIN:53 p > 1 & i,p are_relative_prime & order(i,p) divides n implies (i |^ n) mod p = 1; theorem :: PEPIN:54 p is prime & i,p are_relative_prime implies order(i,p) divides (p -'1); begin :: Fermat Number definition let n be Nat; func Fermat(n) -> Nat equals :: PEPIN:def 3 2 |^ (2 |^ n) + 1; end; theorem :: PEPIN:55 Fermat(0) = 3; theorem :: PEPIN:56 Fermat(1) = 5; theorem :: PEPIN:57 Fermat(2) = 17; theorem :: PEPIN:58 Fermat(3) = 257; theorem :: PEPIN:59 Fermat(4) = 256*256+1; theorem :: PEPIN:60 Fermat(n) > 2; theorem :: PEPIN:61 p is prime & p > 2 & p divides Fermat(n) implies ex k being Nat st p = k*(2 |^ (n + 1)) + 1; theorem :: PEPIN:62 n <> 0 implies 3,Fermat(n) are_relative_prime; begin :: Pepin's Test theorem :: PEPIN:63 (3 |^ ((Fermat(n)-'1) div 2)),(-1) are_congruent_mod Fermat(n) implies Fermat(n) is prime; theorem :: PEPIN:64 5 is prime; theorem :: PEPIN:65 17 is prime; theorem :: PEPIN:66 257 is prime; theorem :: PEPIN:67 256*256+1 is prime;

Back to top