:: 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 )

proof end;

Lm2: for n being Nat holds 2 |^ (2 |^ n) > 1

proof end;

Lm3: for n being Nat st n <> 0 holds

n - 1 >= 0

proof end;

Lm4: for n being Nat st n <> 0 holds

(n -' 1) + 1 = (n + 1) -' 1

proof end;

Lm5: for k, n being Nat holds (k * (2 |^ (n + 1))) div 2 = k * (2 |^ n)

proof end;

Lm6: for k, n, m being Nat st k <= n holds

m |^ k divides m |^ n

proof end;

Lm7: 2 |^ 8 = 256

proof end;

Lm8: for n being Nat holds (2 |^ (2 |^ n)) ^2 = 2 |^ (2 |^ (n + 1))

proof end;

Lm9: for k, n, x being Nat st k > n & x > 1 holds

x |^ k > x |^ n

proof end;

Lm10: for m, n being Nat st 2 |^ m divides 2 |^ n holds

m <= n

proof end;

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

ex k being Element of NAT st i = p * k

proof end;

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 )

( n divides p |^ (k + 1) iff n divides p |^ k )

proof end;

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 )

ex t being Element of NAT st

( d = p |^ t & t <= k )

proof end;

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

d = p |^ k

proof end;

definition

let i be Integer;

:: original: ^2

redefine func i ^2 -> Element of NAT ;

coherence

i ^2 is Element of NAT by ORDINAL1:def 12;

end;
:: original: ^2

redefine func i ^2 -> Element of NAT ;

coherence

i ^2 is Element of NAT by ORDINAL1:def 12;

Lm11: for n, m being Nat st n > 1 & m > 1 & m,1 are_congruent_mod n holds

m mod n = 1

proof end;

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

i2,i3 are_congruent_mod i5

proof end;

begin

:: deftheorem defines Crypto PEPIN:def 1 :

for k, m, n being Nat holds Crypto (m,n,k) = (m |^ k) mod n;

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

for m being Element of NAT st m < n holds

Crypto ((Crypto (m,n,k1)),n,k2) = m

proof end;

begin

definition

let i, p be Nat;

assume that

A1: p > 1 and

A2: i,p are_relative_prime ;

ex b_{1} being Element of NAT st

( b_{1} > 0 & (i |^ b_{1}) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds

( 0 < b_{1} & b_{1} <= k ) ) )

for b_{1}, b_{2} being Element of NAT st b_{1} > 0 & (i |^ b_{1}) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds

( 0 < b_{1} & b_{1} <= k ) ) & b_{2} > 0 & (i |^ b_{2}) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds

( 0 < b_{2} & b_{2} <= k ) ) holds

b_{1} = b_{2}

end;
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 ( it > 0 & (i |^ it) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds

( 0 < it & it <= k ) ) );

ex b

( b

( 0 < b

proof end;

uniqueness for b

( 0 < b

( 0 < b

b

proof end;

:: deftheorem Def2 defines order PEPIN:def 2 :

for i, p being Nat st p > 1 & i,p are_relative_prime holds

for b_{3} being Element of NAT holds

( b_{3} = order (i,p) iff ( b_{3} > 0 & (i |^ b_{3}) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds

( 0 < b_{3} & b_{3} <= k ) ) ) );

for i, p being Nat st p > 1 & i,p are_relative_prime holds

for b

( b

( 0 < b

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

order (i,p) divides n

proof end;

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

(i |^ n) mod p = 1

proof end;

begin

Lm12: for n being Nat holds Fermat n > 1

proof end;

Lm13: for n being Nat holds ((Fermat n) -' 1) mod 2 = 0

proof end;

Lm14: for n being Nat holds (Fermat n) -' 1 > 0

proof end;

Lm15: for n being Nat holds (Fermat n) mod (2 |^ (2 |^ n)) = 1

proof end;

Lm16: for n being Nat holds Fermat n is odd

proof end;

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

ex k being Element of NAT st p = (k * (2 |^ (n + 1))) + 1

proof end;

begin

:: 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

Fermat n is prime

proof end;

Lm17: 3 |^ 2 = 9

proof end;

Lm18: 3 |^ 4 = 81

proof end;

Lm19: 3 |^ 8 = 6561

proof end;

Lm20: 3 |^ 16 = 6561 * 6561

proof end;

Lm21: for i being Nat holds Fermat 1 divides (3 |^ ((4 * i) + 2)) + 1

proof end;

Lm22: for n being Nat st n = 1 holds

3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n

proof end;

Lm23: for n being Nat holds Fermat 2 divides (3 |^ ((16 * n) + 8)) + 1

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

:: Moved from JORDAN1A, AK, 21.02.2006