:: PEPIN semantic presentation 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 let n, x, y be Nat; ::_thesis: ( n > 1 & x >= 1 & 1 = (((x * y) * n) + x) + y implies ( x = 1 & y = 0 ) ) assume that A1: n > 1 and A2: x >= 1 and A3: 1 = (((x * y) * n) + x) + y ; ::_thesis: ( x = 1 & y = 0 ) now__::_thesis:_(_x_=_1_&_y_=_0_) percases ( x > 1 or x = 1 ) by A2, XXREAL_0:1; supposeA4: x > 1 ; ::_thesis: ( x = 1 & y = 0 ) now__::_thesis:_(_x_=_1_&_y_=_0_) percases ( y > 0 or y = 0 ) ; supposeA5: y > 0 ; ::_thesis: ( x = 1 & y = 0 ) then x * y > 1 * y by A4, XREAL_1:68; then (x * y) * n > 1 * (x * y) by A1, XREAL_1:68; then ((x * y) * n) + x > 0 + x by XREAL_1:6; then A6: ((x * y) * n) + x > 1 by A4, XXREAL_0:2; y + 1 > 0 + 1 by A5, XREAL_1:6; hence ( x = 1 & y = 0 ) by A3, A6, XREAL_1:6; ::_thesis: verum end; suppose y = 0 ; ::_thesis: ( x = 1 & y = 0 ) hence ( x = 1 & y = 0 ) by A3; ::_thesis: verum end; end; end; hence ( x = 1 & y = 0 ) ; ::_thesis: verum end; supposeA7: x = 1 ; ::_thesis: ( x = 1 & y = 0 ) now__::_thesis:_(_x_=_1_&_y_=_0_) percases ( y > 0 or y = 0 ) ; supposeA8: y > 0 ; ::_thesis: ( x = 1 & y = 0 ) then (x * y) * n > 0 by A1, A7, XREAL_1:68; then A9: ((x * y) * n) + x > 0 + 1 by A7, XREAL_1:6; y + 1 > 0 + 1 by A8, XREAL_1:6; hence ( x = 1 & y = 0 ) by A3, A9, XREAL_1:6; ::_thesis: verum end; suppose y = 0 ; ::_thesis: ( x = 1 & y = 0 ) hence ( x = 1 & y = 0 ) by A7; ::_thesis: verum end; end; end; hence ( x = 1 & y = 0 ) ; ::_thesis: verum end; end; end; hence ( x = 1 & y = 0 ) ; ::_thesis: verum end; Lm2: for n being Nat holds 2 |^ (2 |^ n) > 1 proof let n be Nat; ::_thesis: 2 |^ (2 |^ n) > 1 defpred S1[ Nat] means 2 |^ (2 |^ $1) > 1; A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: 2 |^ (2 |^ k) > 1 ; ::_thesis: S1[k + 1] then 2 |^ (2 |^ k) < (2 |^ (2 |^ k)) |^ 2 by PREPOWER:13; then ( 2 |^ (k + 1) = (2 |^ k) * 2 & 1 < (2 |^ (2 |^ k)) |^ 2 ) by A2, NEWTON:6, XXREAL_0:2; hence S1[k + 1] by NEWTON:9; ::_thesis: verum end; 2 |^ 0 = 1 by NEWTON:4; then 2 |^ (2 |^ 0) = 2 by NEWTON:5; then A3: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence 2 |^ (2 |^ n) > 1 ; ::_thesis: verum end; Lm3: for n being Nat st n <> 0 holds n - 1 >= 0 proof let n be Nat; ::_thesis: ( n <> 0 implies n - 1 >= 0 ) assume n <> 0 ; ::_thesis: n - 1 >= 0 then n >= 1 by NAT_1:14; then n - 1 >= 1 - 1 by XREAL_1:9; hence n - 1 >= 0 ; ::_thesis: verum end; Lm4: for n being Nat st n <> 0 holds (n -' 1) + 1 = (n + 1) -' 1 proof let n be Nat; ::_thesis: ( n <> 0 implies (n -' 1) + 1 = (n + 1) -' 1 ) assume n <> 0 ; ::_thesis: (n -' 1) + 1 = (n + 1) -' 1 then n >= 1 by NAT_1:14; then n - 1 >= 1 - 1 by XREAL_1:9; then (n -' 1) + 1 = (n + (- 1)) + 1 by XREAL_0:def_2 .= (n + 1) - 1 ; hence (n -' 1) + 1 = (n + 1) -' 1 by XREAL_0:def_2; ::_thesis: verum end; theorem :: PEPIN:1 for i being Nat holds i,i + 1 are_relative_prime proof let k be Nat; ::_thesis: k,k + 1 are_relative_prime k gcd (k + 1) = (1 + (k * 1)) gcd k .= 1 gcd k by EULER_1:8 .= 1 by NEWTON:51 ; hence k,k + 1 are_relative_prime by INT_2:def_3; ::_thesis: verum end; 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 ) proof let m, p be Nat; ::_thesis: ( not p is prime or m,p are_relative_prime or m gcd p = p ) A1: m gcd p divides p by NAT_D:def_5; assume p is prime ; ::_thesis: ( m,p are_relative_prime or m gcd p = p ) then ( m gcd p = 1 or m gcd p = p ) by A1, INT_2:def_4; hence ( m,p are_relative_prime or m gcd p = p ) by INT_2:def_3; ::_thesis: verum end; theorem Th3: :: PEPIN:3 for k, m, n being Nat st k divides n * m & n,k are_relative_prime holds k divides m proof let k, m, n be Nat; ::_thesis: ( k divides n * m & n,k are_relative_prime implies k divides m ) assume that A1: k divides n * m and A2: n,k are_relative_prime ; ::_thesis: k divides m reconsider k = k, m = m, n = n as Element of NAT by ORDINAL1:def_12; n gcd k = 1 by A2, INT_2:def_3; then A3: (n * m) gcd (k * m) = m by EULER_1:5; k divides k * m by NAT_D:9; hence k divides m by A1, A3, NEWTON:50; ::_thesis: verum end; 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 proof let n, m, k be Nat; ::_thesis: ( n divides m & k divides m & n,k are_relative_prime implies n * k divides m ) assume that A1: n divides m and A2: ( k divides m & n,k are_relative_prime ) ; ::_thesis: n * k divides m consider t1 being Nat such that A3: m = n * t1 by A1, NAT_D:def_3; k divides t1 by A2, A3, Th3; then consider t2 being Nat such that A4: t1 = k * t2 by NAT_D:def_3; m = (n * k) * t2 by A3, A4; hence n * k divides m by NAT_D:def_3; ::_thesis: verum end; registration let i be Integer; clusteri ^2 -> natural ; coherence i ^2 is natural proof i ^2 in NAT by INT_1:3, XREAL_1:63; hence i ^2 is natural ; ::_thesis: verum end; end; theorem :: PEPIN:5 for c being Integer st c > 1 holds 1 mod c = 1 proof let c be Integer; ::_thesis: ( c > 1 implies 1 mod c = 1 ) assume A1: c > 1 ; ::_thesis: 1 mod c = 1 then 1 div c = 0 by PRE_FF:4; then 1 mod c = 1 - (0 * c) by A1, INT_1:def_10; hence 1 mod c = 1 ; ::_thesis: verum end; theorem Th6: :: PEPIN:6 for i, n being Nat st i <> 0 holds ( i divides n iff n mod i = 0 ) proof let i, n be Nat; ::_thesis: ( i <> 0 implies ( i divides n iff n mod i = 0 ) ) assume A1: i <> 0 ; ::_thesis: ( i divides n iff n mod i = 0 ) A2: ( n mod i = 0 implies i divides n ) proof assume n mod i = 0 ; ::_thesis: i divides n then ex t being Nat st ( n = (i * t) + 0 & 0 < i ) by A1, NAT_D:def_2; hence i divides n by NAT_D:def_3; ::_thesis: verum end; ( i divides n implies n mod i = 0 ) proof assume i divides n ; ::_thesis: n mod i = 0 then ex t being Nat st n = i * t by NAT_D:def_3; hence n mod i = 0 by NAT_D:13; ::_thesis: verum end; hence ( i divides n iff n mod i = 0 ) by A2; ::_thesis: verum end; theorem Th7: :: PEPIN:7 for m, n being Nat st m <> 0 & m divides n mod m holds m divides n proof let m, n be Nat; ::_thesis: ( m <> 0 & m divides n mod m implies m divides n ) assume that A1: m <> 0 and A2: m divides n mod m ; ::_thesis: m divides n consider x being Nat such that A3: n mod m = m * x by A2, NAT_D:def_3; (n mod m) + (m * (n div m)) = m * (x + (n div m)) by A3; then n = m * (x + (n div m)) by A1, NAT_D:2; hence m divides n by NAT_D:def_3; ::_thesis: verum end; theorem :: PEPIN:8 for m, n, k being Nat st 0 < n & m mod n = k holds n divides m - k proof let m, n, k be Nat; ::_thesis: ( 0 < n & m mod n = k implies n divides m - k ) assume A1: ( 0 < n & m mod n = k ) ; ::_thesis: n divides m - k take m div n ; :: according to INT_1:def_3 ::_thesis: m - k = n * (m div n) m = (n * (m div n)) + k by A1, NAT_D:2; hence m - k = n * (m div n) ; ::_thesis: verum end; 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 proof let i, p, k be Nat; ::_thesis: ( i * p <> 0 & k mod (i * p) < p implies k mod (i * p) = k mod p ) assume that A1: i * p <> 0 and A2: k mod (i * p) < p ; ::_thesis: k mod (i * p) = k mod p set T = k mod (i * p); consider n being Nat such that A3: k = ((i * p) * n) + (k mod (i * p)) and k mod (i * p) < i * p by A1, NAT_D:def_2; k = (p * (i * n)) + (k mod (i * p)) by A3; then k mod p = (k mod (i * p)) mod p by NAT_D:21 .= k mod (i * p) by A2, NAT_D:24 ; hence k mod (i * p) = k mod p ; ::_thesis: verum end; theorem Th10: :: PEPIN:10 for p being Nat for a being Integer holds ((a * p) + 1) mod p = 1 mod p proof let p be Nat; ::_thesis: for a being Integer holds ((a * p) + 1) mod p = 1 mod p let a be Integer; ::_thesis: ((a * p) + 1) mod p = 1 mod p percases ( p <> 0 or p = 0 ) ; supposeA1: p <> 0 ; ::_thesis: ((a * p) + 1) mod p = 1 mod p reconsider p = p as Integer ; ((a * p) + 1) mod p = ((a * p) + 1) - ((((a * p) + 1) div p) * p) by A1, INT_1:def_10 .= ((a * p) + 1) - ([\(((a * p) / p) + (1 / p))/] * p) by XCMPLX_1:62 .= ((a * p) + 1) - ([\(a + (1 / p))/] * p) by A1, XCMPLX_1:89 .= ((a * p) + 1) - ((a + [\(1 / p)/]) * p) by INT_1:28 .= 1 - ((1 div p) * p) ; hence ((a * p) + 1) mod p = 1 mod p by A1, INT_1:def_10; ::_thesis: verum end; suppose p = 0 ; ::_thesis: ((a * p) + 1) mod p = 1 mod p hence ((a * p) + 1) mod p = 1 mod p ; ::_thesis: verum end; end; end; 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 proof let m, n, k be Nat; ::_thesis: ( 1 < m & (n * k) mod m = k mod m & k,m are_relative_prime implies n mod m = 1 ) assume that A1: 1 < m and A2: (n * k) mod m = k mod m and A3: k,m are_relative_prime ; ::_thesis: n mod m = 1 consider t2 being Nat such that A4: k = (m * t2) + (k mod m) and k mod m < m by A1, NAT_D:def_2; consider t1 being Nat such that A5: n * k = (m * t1) + ((n * k) mod m) and (n * k) mod m < m by A1, NAT_D:def_2; (n * k) - (1 * k) = m * (t1 - t2) by A2, A5, A4; then A6: m divides k * (n - 1) by INT_1:def_3; reconsider n = n, m = m as Integer ; m divides n - 1 by A3, A6, INT_2:25; then consider tt being Integer such that A7: n - 1 = m * tt by INT_1:def_3; n = (m * tt) + 1 by A7; then n mod m = 1 mod m by EULER_1:12 .= 1 by A1, NAT_D:14 ; hence n mod m = 1 ; ::_thesis: verum end; theorem Th12: :: PEPIN:12 for p, k, m being Nat holds (p |^ k) mod m = ((p mod m) |^ k) mod m proof let p, k, m be Nat; ::_thesis: (p |^ k) mod m = ((p mod m) |^ k) mod m defpred S1[ Nat] means (p |^ $1) mod m = ((p mod m) |^ $1) mod m; A1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] (p |^ (n + 1)) mod m = ((p |^ n) * (p |^ 1)) mod m by NEWTON:8 .= ((p |^ n) * p) mod m by NEWTON:5 .= (((p |^ n) mod m) * (p mod m)) mod m by EULER_2:9 .= (((p mod m) |^ n) * (p mod m)) mod m by A2, EULER_2:8 .= ((p mod m) |^ (n + 1)) mod m by NEWTON:6 ; hence S1[n + 1] ; ::_thesis: verum end; (p |^ 0) mod m = 1 mod m by NEWTON:4; then A3: S1[ 0 ] by NEWTON:4; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence (p |^ k) mod m = ((p mod m) |^ k) mod m ; ::_thesis: verum end; Lm5: for k, n being Nat holds (k * (2 |^ (n + 1))) div 2 = k * (2 |^ n) proof let k, n be Nat; ::_thesis: (k * (2 |^ (n + 1))) div 2 = k * (2 |^ n) k * (2 |^ (n + 1)) = k * ((2 |^ n) * 2) by NEWTON:6 .= (k * (2 |^ n)) * 2 ; hence (k * (2 |^ (n + 1))) div 2 = k * (2 |^ n) by NAT_D:20; ::_thesis: verum end; Lm6: for k, n, m being Nat st k <= n holds m |^ k divides m |^ n proof let k, n, m be Nat; ::_thesis: ( k <= n implies m |^ k divides m |^ n ) assume k <= n ; ::_thesis: m |^ k divides m |^ n then consider t being Nat such that A1: n = k + t by NAT_1:10; m |^ n = (m |^ k) * (m |^ t) by A1, NEWTON:8; hence m |^ k divides m |^ n by NAT_D:def_3; ::_thesis: verum end; Lm7: 2 |^ 8 = 256 proof 2 |^ 8 = 2 |^ (4 + 4) .= 16 * 16 by NEWTON:8, POWER:62 ; hence 2 |^ 8 = 256 ; ::_thesis: verum end; theorem :: PEPIN:13 for i being Nat st i <> 0 holds (i ^2) mod (i + 1) = 1 proof let i be Nat; ::_thesis: ( i <> 0 implies (i ^2) mod (i + 1) = 1 ) assume A1: i <> 0 ; ::_thesis: (i ^2) mod (i + 1) = 1 then A2: i + 1 > 0 + 1 by XREAL_1:6; i >= 1 by A1, NAT_1:14; then i - 1 >= 1 - 1 by XREAL_1:9; then reconsider I = i - 1 as Element of NAT by INT_1:3; reconsider II = (i + 1) * I as Element of NAT ; (i ^2) mod (i + 1) = (II + 1) mod (i + 1) .= ((II mod (i + 1)) + 1) mod (i + 1) by NAT_D:22 .= (0 + 1) mod (i + 1) by NAT_D:13 .= 1 by A2, NAT_D:24 ; hence (i ^2) mod (i + 1) = 1 ; ::_thesis: verum end; theorem :: PEPIN:14 for k, j, i being Nat st k ^2 < j & i mod j = k holds (i ^2) mod j = k ^2 proof let k, j, i be Nat; ::_thesis: ( k ^2 < j & i mod j = k implies (i ^2) mod j = k ^2 ) assume that A1: k ^2 < j and A2: i mod j = k ; ::_thesis: (i ^2) mod j = k ^2 consider n being Nat such that A3: i = (j * n) + k and k < j by A1, A2, NAT_D:def_2; i ^2 = (j * ((((n * j) * n) + (k * n)) + (n * k))) + (k ^2) by A3; then (i ^2) mod j = (k ^2) mod j by NAT_D:21; hence (i ^2) mod j = k ^2 by A1, NAT_D:24; ::_thesis: verum end; theorem :: PEPIN:15 for p, i being Nat st p is prime & i mod p = - 1 holds (i ^2) mod p = 1 proof let p, i be Nat; ::_thesis: ( p is prime & i mod p = - 1 implies (i ^2) mod p = 1 ) assume that A1: p is prime and A2: i mod p = - 1 ; ::_thesis: (i ^2) mod p = 1 A3: p > 1 by A1, INT_2:def_4; p <> 0 by A1, INT_2:def_4; then i mod p = i - ((i div p) * p) by INT_1:def_10; then i = ((i div p) * p) - 1 by A2; then i ^2 = (((((i div p) * p) - 2) * (i div p)) * p) + 1 ; then (i ^2) mod p = 1 mod p by Th10 .= 1 by A3, NAT_D:24 ; hence (i ^2) mod p = 1 ; ::_thesis: verum end; 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 proof let p be Nat; ::_thesis: ( p > 2 & p is prime implies p is odd ) assume A1: ( p > 2 & p is prime ) ; ::_thesis: p is odd assume p is even ; ::_thesis: contradiction then p mod 2 = 0 by NAT_2:21; then ex k being Nat st ( p = (2 * k) + 0 & 0 < 2 ) by NAT_D:def_2; then 2 divides p by NAT_D:def_3; hence contradiction by A1, INT_2:def_4; ::_thesis: verum end; theorem :: PEPIN:18 for n being Nat st n > 0 holds 2 to_power n is even proof let n be Nat; ::_thesis: ( n > 0 implies 2 to_power n is even ) assume n > 0 ; ::_thesis: 2 to_power n is even then (2 to_power n) mod 2 = 0 by NAT_2:17; hence 2 to_power n is even by NAT_2:21; ::_thesis: verum end; 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 proof let i, k be Nat; ::_thesis: ( i is odd implies i |^ k is odd ) defpred S1[ Nat] means i |^ $1 is odd ; assume A1: i is odd ; ::_thesis: i |^ k is odd A2: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) A3: i |^ (n + 1) = (i |^ n) * i by NEWTON:6; assume i |^ n is odd ; ::_thesis: S1[n + 1] hence S1[n + 1] by A1, A3; ::_thesis: verum end; ( i |^ 0 = 1 & 1 mod 2 = 1 ) by NAT_D:24, NEWTON:4; then A4: S1[ 0 ] by NAT_2:22; for n being Nat holds S1[n] from NAT_1:sch_2(A4, A2); hence i |^ k is odd ; ::_thesis: verum end; theorem Th21: :: PEPIN:21 for k, i being Nat st k > 0 & i is even holds i |^ k is even proof let k, i be Nat; ::_thesis: ( k > 0 & i is even implies i |^ k is even ) assume that A1: k > 0 and A2: i is even ; ::_thesis: i |^ k is even defpred S1[ Nat] means ( $1 > 0 & i is even implies i |^ $1 is even ); A3: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] S1[n + 1] proof now__::_thesis:_S1[n_+_1] (i |^ n) * i is even by A2; hence S1[n + 1] by NEWTON:6; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; A4: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A4, A3); hence i |^ k is even by A1, A2; ::_thesis: verum end; theorem :: PEPIN:22 for n being Nat holds ( 2 divides n iff n is even ) proof let n be Nat; ::_thesis: ( 2 divides n iff n is even ) A1: ( n is even implies 2 divides n ) proof assume n is even ; ::_thesis: 2 divides n then n mod 2 = 0 by NAT_2:21; then ex k being Nat st ( n = (2 * k) + 0 & 0 < 2 ) by NAT_D:def_2; hence 2 divides n by NAT_D:def_3; ::_thesis: verum end; ( 2 divides n implies n is even ) proof assume 2 divides n ; ::_thesis: n is even then ex k being Nat st n = 2 * k by NAT_D:def_3; hence n is even ; ::_thesis: verum end; hence ( 2 divides n iff n is even ) by A1; ::_thesis: verum end; 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 proof let n be Nat; ::_thesis: n |^ 2 = n ^2 n |^ 2 = n |^ (1 + 1) .= (n |^ 1) * (n |^ 1) by NEWTON:8 .= n * (n |^ 1) by NEWTON:5 .= n ^2 by NEWTON:5 ; hence n |^ 2 = n ^2 ; ::_thesis: verum end; theorem Th25: :: PEPIN:25 for m, n being Nat st m > 1 & n > 0 holds m |^ n > 1 proof let m, n be Nat; ::_thesis: ( m > 1 & n > 0 implies m |^ n > 1 ) assume that A1: m > 1 and A2: n > 0 ; ::_thesis: m |^ n > 1 defpred S1[ Nat] means ( $1 > 0 implies m |^ $1 > 1 ); A3: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) A4: m |^ (n + 1) = (m |^ n) * (m |^ 1) by NEWTON:8 .= (m |^ n) * m by NEWTON:5 ; assume A5: S1[n] ; ::_thesis: S1[n + 1] S1[n + 1] proof now__::_thesis:_S1[n_+_1] percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: S1[n + 1] hence S1[n + 1] by A1, NEWTON:5; ::_thesis: verum end; suppose n <> 0 ; ::_thesis: S1[n + 1] then (m |^ n) * m > 1 * m by A1, A5, XREAL_1:68; hence S1[n + 1] by A1, A4, XXREAL_0:2; ::_thesis: verum end; end; end; hence S1[n + 1] ; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; A6: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A6, A3); hence m |^ n > 1 by A2; ::_thesis: verum end; Lm8: for n being Nat holds (2 |^ (2 |^ n)) ^2 = 2 |^ (2 |^ (n + 1)) proof let n be Nat; ::_thesis: (2 |^ (2 |^ n)) ^2 = 2 |^ (2 |^ (n + 1)) defpred S1[ Nat] means (2 |^ (2 |^ $1)) ^2 = 2 |^ (2 |^ ($1 + 1)); A1: 2 |^ (2 |^ (0 + 1)) = 2 to_power 2 by NEWTON:5 .= 2 ^2 by POWER:46 ; A2: for k being Nat st S1[k] holds S1[k + 1] proof let x be Nat; ::_thesis: ( S1[x] implies S1[x + 1] ) assume A3: (2 |^ (2 |^ x)) ^2 = 2 |^ (2 |^ (x + 1)) ; ::_thesis: S1[x + 1] (2 |^ (2 |^ (x + 1))) ^2 = (2 |^ ((2 |^ x) * 2)) ^2 by NEWTON:6 .= ((2 |^ (2 |^ x)) |^ 2) ^2 by NEWTON:9 .= ((2 |^ (2 |^ x)) ^2) ^2 by Th24 .= (2 |^ (2 |^ (x + 1))) |^ 2 by A3, Th24 .= 2 |^ ((2 |^ (x + 1)) * 2) by NEWTON:9 .= 2 |^ (2 |^ ((x + 1) + 1)) by NEWTON:6 ; hence S1[x + 1] ; ::_thesis: verum end; 2 |^ 0 = 1 by NEWTON:4; then A4: S1[ 0 ] by A1, NEWTON:5; for k being Nat holds S1[k] from NAT_1:sch_2(A4, A2); hence (2 |^ (2 |^ n)) ^2 = 2 |^ (2 |^ (n + 1)) ; ::_thesis: verum end; theorem Th26: :: PEPIN:26 for n, p being Nat st n <> 0 & p <> 0 holds n |^ p = n * (n |^ (p -' 1)) proof let n, p be Nat; ::_thesis: ( n <> 0 & p <> 0 implies n |^ p = n * (n |^ (p -' 1)) ) assume A1: ( n <> 0 & p <> 0 ) ; ::_thesis: n |^ p = n * (n |^ (p -' 1)) defpred S1[ Nat] means ( n <> 0 & $1 <> 0 implies n |^ $1 = n * (n |^ ($1 -' 1)) ); A2: for m being Nat st S1[m] holds S1[m + 1] proof let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] ) assume S1[m] ; ::_thesis: S1[m + 1] now__::_thesis:_S1[m_+_1] percases ( m = 0 or m <> 0 ) ; supposeA3: m = 0 ; ::_thesis: S1[m + 1] n * (n |^ ((0 + 1) -' 1)) = n * (n |^ 0) by XREAL_1:232 .= n * 1 by NEWTON:4 ; hence S1[m + 1] by A3, NEWTON:5; ::_thesis: verum end; supposeA4: m <> 0 ; ::_thesis: S1[m + 1] n |^ (m + 1) = (n |^ m) * n by NEWTON:6 .= (n |^ ((m -' 1) + 1)) * n by A4, NAT_1:14, XREAL_1:235 .= n * (n |^ ((m + 1) -' 1)) by A4, Lm4 ; hence S1[m + 1] ; ::_thesis: verum end; end; end; hence S1[m + 1] ; ::_thesis: verum end; A5: S1[ 0 ] ; for m being Nat holds S1[m] from NAT_1:sch_2(A5, A2); hence n |^ p = n * (n |^ (p -' 1)) by A1; ::_thesis: verum end; theorem Th27: :: PEPIN:27 for n, m being Nat st m mod 2 = 0 holds (n |^ (m div 2)) ^2 = n |^ m proof let n, m be Nat; ::_thesis: ( m mod 2 = 0 implies (n |^ (m div 2)) ^2 = n |^ m ) assume A1: m mod 2 = 0 ; ::_thesis: (n |^ (m div 2)) ^2 = n |^ m (n |^ (m div 2)) ^2 = n |^ ((m div 2) + (m div 2)) by NEWTON:8 .= n |^ ((m + m) div 2) by A1, NAT_D:19 .= n |^ ((2 * m) div 2) .= n |^ m by NAT_D:18 ; hence (n |^ (m div 2)) ^2 = n |^ m ; ::_thesis: verum end; theorem Th28: :: PEPIN:28 for n, k being Nat st n <> 0 & 1 <= k holds (n |^ k) div n = n |^ (k -' 1) proof let n, k be Nat; ::_thesis: ( n <> 0 & 1 <= k implies (n |^ k) div n = n |^ (k -' 1) ) assume that A1: n <> 0 and A2: 1 <= k ; ::_thesis: (n |^ k) div n = n |^ (k -' 1) A3: k - 1 >= 1 - 1 by A2, XREAL_1:9; k = (k - 1) + 1 .= (k -' 1) + 1 by A3, XREAL_0:def_2 ; then n |^ k = n * (n |^ (k -' 1)) by NEWTON:6; hence (n |^ k) div n = n |^ (k -' 1) by A1, NAT_D:18; ::_thesis: verum end; theorem :: PEPIN:29 for n being Nat holds 2 |^ (n + 1) = (2 |^ n) + (2 |^ n) proof let n be Nat; ::_thesis: 2 |^ (n + 1) = (2 |^ n) + (2 |^ n) defpred S1[ Nat] means 2 |^ ($1 + 1) = (2 |^ $1) + (2 |^ $1); A1: for m being Nat st S1[m] holds S1[m + 1] proof let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A2: 2 |^ (m + 1) = (2 |^ m) + (2 |^ m) ; ::_thesis: S1[m + 1] (2 |^ (m + 1)) + (2 |^ (m + 1)) = (2 * (2 |^ m)) + (2 |^ (m + 1)) by NEWTON:6 .= (2 * (2 |^ m)) + (2 * (2 |^ m)) by NEWTON:6 .= 2 * ((2 |^ m) + (2 |^ m)) .= 2 |^ ((m + 1) + 1) by A2, NEWTON:6 ; hence S1[m + 1] ; ::_thesis: verum end; 2 |^ (0 + 1) = 1 + 1 by NEWTON:5 .= (2 |^ 0) + 1 by NEWTON:4 .= (2 |^ 0) + (2 |^ 0) by NEWTON:4 ; then A3: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence 2 |^ (n + 1) = (2 |^ n) + (2 |^ n) ; ::_thesis: verum end; theorem Th30: :: PEPIN:30 for k, n, m being Nat st k > 1 & k |^ n = k |^ m holds n = m proof let k, n, m be Nat; ::_thesis: ( k > 1 & k |^ n = k |^ m implies n = m ) assume that A1: k > 1 and A2: k |^ n = k |^ m ; ::_thesis: n = m now__::_thesis:_n_=_m percases ( n = m or n <> m ) ; suppose n = m ; ::_thesis: n = m hence n = m ; ::_thesis: verum end; suppose n <> m ; ::_thesis: n = m then k to_power m <> k to_power n by A1, POWER:50; hence n = m by A2; ::_thesis: verum end; end; end; hence n = m ; ::_thesis: verum end; Lm9: for k, n, x being Nat st k > n & x > 1 holds x |^ k > x |^ n proof let k, n, x be Nat; ::_thesis: ( k > n & x > 1 implies x |^ k > x |^ n ) assume that A1: k > n and A2: x > 1 ; ::_thesis: x |^ k > x |^ n consider m being Nat such that A3: k = n + m by A1, NAT_1:10; (m + n) - n > n - n by A1, A3, XREAL_1:9; then (m + 1) - 1 > 1 - 1 ; then m + 1 > 1 by XREAL_1:9; then A4: m >= 1 by NAT_1:13; 1 |^ m = 1 by NEWTON:10; then A5: x |^ m > 1 by A2, A4, PREPOWER:10; A6: x |^ n >= 1 by A2, PREPOWER:11; x |^ k = (x |^ n) * (x |^ m) by A3, NEWTON:8; hence x |^ k > x |^ n by A6, A5, XREAL_1:155; ::_thesis: verum end; Lm10: for m, n being Nat st 2 |^ m divides 2 |^ n holds m <= n proof let m, n be Nat; ::_thesis: ( 2 |^ m divides 2 |^ n implies m <= n ) ( not m <= n implies not 2 |^ m divides 2 |^ n ) proof assume A1: not m <= n ; ::_thesis: not 2 |^ m divides 2 |^ n not 2 |^ m divides 2 |^ n proof (2 |^ n) div (2 |^ m) = 0 by A1, Lm9, NAT_D:27; then A2: 2 |^ n > (2 |^ m) * ((2 |^ n) div (2 |^ m)) by PREPOWER:6; assume 2 |^ m divides 2 |^ n ; ::_thesis: contradiction hence contradiction by A2, NAT_D:3; ::_thesis: verum end; hence not 2 |^ m divides 2 |^ n ; ::_thesis: verum end; hence ( 2 |^ m divides 2 |^ n implies m <= n ) ; ::_thesis: verum end; 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 proof let p, i, n be Nat; ::_thesis: ( p is prime & i divides p |^ n & not i = 1 implies ex k being Element of NAT st i = p * k ) defpred S1[ Nat] means ( not i divides p |^ $1 or i = 1 or ex k being Element of NAT st i = p * k ); assume A1: p is prime ; ::_thesis: ( not i divides p |^ n or i = 1 or ex k being Element of NAT st i = p * k ) then A2: p <> 0 by INT_2:def_4; A3: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A4: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_(_i_divides_p_|^_(n_+_1)_implies_S1[n_+_1]_) assume i divides p |^ (n + 1) ; ::_thesis: S1[n + 1] then consider u1 being Nat such that A5: p |^ (n + 1) = i * u1 by NAT_D:def_3; p * (p |^ n) = i * u1 by A5, NEWTON:6; then A6: p divides i * u1 by NAT_D:def_3; now__::_thesis:_S1[n_+_1] percases ( p divides i or p divides u1 ) by A1, A6, NEWTON:80; suppose p divides i ; ::_thesis: S1[n + 1] then consider w1 being Nat such that A7: i = p * w1 by NAT_D:def_3; w1 in NAT by ORDINAL1:def_12; hence S1[n + 1] by A7; ::_thesis: verum end; suppose p divides u1 ; ::_thesis: S1[n + 1] then consider w2 being Nat such that A8: u1 = p * w2 by NAT_D:def_3; p * (p |^ n) = p * (i * w2) by A5, A8, NEWTON:6; then p |^ n = (p * (i * w2)) div p by A2, NAT_D:18; then p |^ n = i * w2 by A2, NAT_D:18; hence S1[n + 1] by A4, NAT_D:def_3; ::_thesis: verum end; end; end; hence S1[n + 1] ; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; A9: S1[ 0 ] proof now__::_thesis:_(_i_divides_p_|^_0_implies_S1[_0_]_) assume i divides p |^ 0 ; ::_thesis: S1[ 0 ] then i divides 1 by NEWTON:4; then ex t being Nat st 1 = i * t by NAT_D:def_3; hence S1[ 0 ] by NAT_1:15; ::_thesis: verum end; hence S1[ 0 ] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A9, A3); hence ( not i divides p |^ n or i = 1 or ex k being Element of NAT st i = p * k ) ; ::_thesis: verum 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 ) proof let p, k, n be Nat; ::_thesis: ( p is prime & n < p |^ (k + 1) implies ( n divides p |^ (k + 1) iff n divides p |^ k ) ) assume that A1: p is prime and A2: n < p |^ (k + 1) ; ::_thesis: ( n divides p |^ (k + 1) iff n divides p |^ k ) A3: p <> 0 by A1, INT_2:def_4; A4: ( n divides p |^ (k + 1) implies n divides p |^ k ) proof assume A5: n divides p |^ (k + 1) ; ::_thesis: n divides p |^ k now__::_thesis:_n_divides_p_|^_k percases ( n = 1 or ex i being Element of NAT st n = p * i ) by A1, A5, Th32; suppose n = 1 ; ::_thesis: n divides p |^ k hence n divides p |^ k by NAT_D:6; ::_thesis: verum end; suppose ex i being Element of NAT st n = p * i ; ::_thesis: n divides p |^ k then consider i being Element of NAT such that A6: n = p * i ; consider u being Nat such that A7: p |^ (k + 1) = (p * i) * u by A5, A6, NAT_D:def_3; p * (p |^ k) = p * (i * u) by A7, NEWTON:6; then A8: p |^ k = (p * (i * u)) div p by A3, NAT_D:18; then A9: p |^ k = i * u by A3, NAT_D:18; then A10: u divides p |^ k by NAT_D:def_3; u <> 1 by A2, A6, A9, NEWTON:6; then consider j being Element of NAT such that A11: u = p * j by A1, A10, Th32; p |^ k = n * j by A3, A6, A8, A11, NAT_D:18; hence n divides p |^ k by NAT_D:def_3; ::_thesis: verum end; end; end; hence n divides p |^ k ; ::_thesis: verum end; ( n divides p |^ k implies n divides p |^ (k + 1) ) proof assume n divides p |^ k ; ::_thesis: n divides p |^ (k + 1) then n divides (p |^ k) * p by NAT_D:9; hence n divides p |^ (k + 1) by NEWTON:6; ::_thesis: verum end; hence ( n divides p |^ (k + 1) iff n divides p |^ k ) by A4; ::_thesis: verum 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 ) proof let p, d, n be Nat; ::_thesis: ( p is prime & d divides p |^ n implies ex t being Element of NAT st ( d = p |^ t & t <= n ) ) assume that A1: p is prime and A2: d divides p |^ n ; ::_thesis: ex t being Element of NAT st ( d = p |^ t & t <= n ) defpred S1[ Nat] means ( d divides p |^ $1 implies ex t being Element of NAT st ( d = p |^ t & t <= $1 ) ); A3: p > 0 by A1, INT_2:def_4; A4: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A5: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_(_d_divides_p_|^_(n_+_1)_implies_S1[n_+_1]_) assume A6: d divides p |^ (n + 1) ; ::_thesis: S1[n + 1] p |^ (n + 1) > 0 by A3, PREPOWER:6; then A7: d <= p |^ (n + 1) by A6, NAT_D:7; now__::_thesis:_S1[n_+_1] percases ( d < p |^ (n + 1) or d = p |^ (n + 1) ) by A7, XXREAL_0:1; suppose d < p |^ (n + 1) ; ::_thesis: S1[n + 1] then ex t being Element of NAT st ( d = p |^ t & t <= n ) by A1, A5, A6, Th33; hence S1[n + 1] by NAT_1:12; ::_thesis: verum end; suppose d = p |^ (n + 1) ; ::_thesis: S1[n + 1] hence S1[n + 1] ; ::_thesis: verum end; end; end; hence S1[n + 1] ; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; A8: S1[ 0 ] proof assume A9: d divides p |^ 0 ; ::_thesis: ex t being Element of NAT st ( d = p |^ t & t <= 0 ) d = p |^ 0 proof ex t being Nat st p |^ 0 = d * t by A9, NAT_D:def_3; then d = 1 by NAT_1:15, NEWTON:4; hence d = p |^ 0 by NEWTON:4; ::_thesis: verum end; hence ex t being Element of NAT st ( d = p |^ t & t <= 0 ) ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A8, A4); hence ex t being Element of NAT st ( d = p |^ t & t <= n ) by A2; ::_thesis: verum end; theorem Th35: :: PEPIN:35 for p, i, n being Nat st p > 1 & i mod p = 1 holds (i |^ n) mod p = 1 proof let p, i, n be Nat; ::_thesis: ( p > 1 & i mod p = 1 implies (i |^ n) mod p = 1 ) assume that A1: p > 1 and A2: i mod p = 1 ; ::_thesis: (i |^ n) mod p = 1 defpred S1[ Nat] means (i |^ $1) mod p = 1; A3: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: (i |^ k) mod p = 1 ; ::_thesis: S1[k + 1] (i |^ (k + 1)) mod p = ((i |^ k) * i) mod p by NEWTON:6 .= (((i |^ k) mod p) * i) mod p by EULER_2:8 .= 1 by A2, A4 ; hence S1[k + 1] ; ::_thesis: verum end; 1 mod p = 1 by A1, NAT_D:24; then A5: S1[ 0 ] by NEWTON:4; for n being Nat holds S1[n] from NAT_1:sch_2(A5, A3); hence (i |^ n) mod p = 1 ; ::_thesis: verum end; theorem Th36: :: PEPIN:36 for m, n being Nat st m > 0 holds (n |^ m) mod n = 0 proof let m, n be Nat; ::_thesis: ( m > 0 implies (n |^ m) mod n = 0 ) assume A1: m > 0 ; ::_thesis: (n |^ m) mod n = 0 defpred S1[ Nat] means ( $1 > 0 implies (n |^ $1) mod n = 0 ); A2: for m being Nat st S1[m] holds S1[m + 1] proof let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] ) assume S1[m] ; ::_thesis: S1[m + 1] S1[m + 1] proof reconsider m = m, n = n as Element of NAT by ORDINAL1:def_12; (n * (n |^ m)) mod n = ((n mod n) * (n |^ m)) mod n by EULER_2:8 .= (0 * (n |^ m)) mod n by NAT_D:25 .= 0 by NAT_D:26 ; hence S1[m + 1] by NEWTON:6; ::_thesis: verum end; hence S1[m + 1] ; ::_thesis: verum end; A3: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A2); hence (n |^ m) mod n = 0 by A1; ::_thesis: verum end; 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 proof let n, p be Nat; ::_thesis: ( p is prime & n,p are_relative_prime implies (n |^ (p -' 1)) mod p = 1 ) assume that A1: p is prime and A2: n,p are_relative_prime ; ::_thesis: (n |^ (p -' 1)) mod p = 1 A3: p <> 0 by A1, INT_2:def_4; A4: n <> 0 proof assume n = 0 ; ::_thesis: contradiction then n gcd p = p by NEWTON:52; then n gcd p > 1 by A1, INT_2:def_4; hence contradiction by A2, INT_2:def_3; ::_thesis: verum end; then A5: n |^ (p -' 1) <> 0 by PREPOWER:5; (n |^ p) mod p = n mod p by A1, A2, A4, EULER_2:19; then A6: ((n |^ (p -' 1)) * n) mod p = n mod p by A3, A4, Th26; p > 1 by A1, INT_2:def_4; hence (n |^ (p -' 1)) mod p = 1 by A2, A6, A5, EULER_2:12; ::_thesis: verum 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 proof let p, d, k be Nat; ::_thesis: ( p is prime & d > 1 & d divides p |^ k & not d divides (p |^ k) div p implies d = p |^ k ) assume that A1: p is prime and A2: d > 1 and A3: d divides p |^ k and A4: not d divides (p |^ k) div p ; ::_thesis: d = p |^ k A5: k <> 0 proof assume k = 0 ; ::_thesis: contradiction then p |^ k = 1 by NEWTON:4; hence contradiction by A2, A3, NAT_D:7; ::_thesis: verum end; then k >= 1 by NAT_1:14; then A6: k - 1 >= 1 - 1 by XREAL_1:9; consider t being Element of NAT such that A7: d = p |^ t and A8: t <= k by A1, A3, Th34; A9: p <> 0 by A1, INT_2:def_4; not t < k proof assume t < k ; ::_thesis: contradiction then t < (k + (- 1)) + 1 ; then t < (k -' 1) + 1 by A6, XREAL_0:def_2; then t <= k -' 1 by NAT_1:13; then d divides p |^ (k -' 1) by A7, Lm6; hence contradiction by A4, A9, A5, Th28, NAT_1:14; ::_thesis: verum end; hence d = p |^ k by A7, A8, XXREAL_0:1; ::_thesis: verum end; 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 ) proof let m, n be Nat; ::_thesis: ( n > 1 implies ( m mod n = 1 iff m,1 are_congruent_mod n ) ) assume A1: n > 1 ; ::_thesis: ( m mod n = 1 iff m,1 are_congruent_mod n ) A2: ( m,1 are_congruent_mod n implies m mod n = 1 ) proof assume m,1 are_congruent_mod n ; ::_thesis: m mod n = 1 then consider t being Integer such that A3: n * t = m - 1 by INT_1:def_5; reconsider m = m, n = n as Integer ; m mod n = ((n * t) + 1) mod n by A3 .= 1 mod n by EULER_1:12 ; hence m mod n = 1 by A1, NAT_D:14; ::_thesis: verum end; ( m mod n = 1 implies m,1 are_congruent_mod n ) proof assume m mod n = 1 ; ::_thesis: m,1 are_congruent_mod n then consider k being Nat such that A4: m = (n * k) + 1 and 1 < n by NAT_D:def_2; n * k = m - 1 by A4; hence m,1 are_congruent_mod n by INT_1:def_5; ::_thesis: verum end; hence ( m mod n = 1 iff m,1 are_congruent_mod n ) by A2; ::_thesis: verum end; Lm11: for n, m being Nat st n > 1 & m > 1 & m,1 are_congruent_mod n holds m mod n = 1 proof let n, m be Nat; ::_thesis: ( n > 1 & m > 1 & m,1 are_congruent_mod n implies m mod n = 1 ) assume that A1: n > 1 and A2: m > 1 and A3: m,1 are_congruent_mod n ; ::_thesis: m mod n = 1 consider d being Integer such that A4: n * d = m - 1 by A3, INT_1:def_5; m - 1 > 1 - 1 by A2, XREAL_1:9; then d > 0 by A4; then reconsider d = d as Element of NAT by INT_1:3; m = (n * d) + 1 by A4; then m mod n = 1 mod n by NAT_D:21 .= 1 by A1, NAT_D:14 ; hence m mod n = 1 ; ::_thesis: verum 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 proof let i1, i2, i5, i3 be Integer; ::_thesis: ( i1,i2 are_congruent_mod i5 & i1,i3 are_congruent_mod i5 implies i2,i3 are_congruent_mod i5 ) assume that A1: i1,i2 are_congruent_mod i5 and A2: i1,i3 are_congruent_mod i5 ; ::_thesis: i2,i3 are_congruent_mod i5 i2,i1 are_congruent_mod i5 by A1, INT_1:14; then consider t1 being Integer such that A3: i5 * t1 = i2 - i1 by INT_1:def_5; i3,i1 are_congruent_mod i5 by A2, INT_1:14; then consider t2 being Integer such that A4: i5 * t2 = i3 - i1 by INT_1:def_5; i2 - i3 = i5 * (t1 - t2) by A3, A4; hence i2,i3 are_congruent_mod i5 by INT_1:def_5; ::_thesis: verum end; theorem Th41: :: PEPIN:41 3 is prime proof for n being Nat holds ( not n divides 3 or n = 1 or n = 3 ) proof let n be Nat; ::_thesis: ( not n divides 3 or n = 1 or n = 3 ) assume A1: n divides 3 ; ::_thesis: ( n = 1 or n = 3 ) A2: n <> 2 proof A3: 3 mod 2 = ((2 * 1) + 1) mod 2 .= 1 mod 2 by NAT_D:21 .= 1 by NAT_D:24 ; assume n = 2 ; ::_thesis: contradiction hence contradiction by A1, A3, Th6; ::_thesis: verum end; n <= 3 by A1, NAT_D:7; then ( n < 2 + 1 or n = 3 ) by XXREAL_0:1; then ( n <= 2 or n = 3 ) by NAT_1:13; then ( n < 1 + 1 or n = 2 or n = 3 ) by XXREAL_0:1; then ( n <= 1 or n = 2 or n = 3 ) by NAT_1:13; then A4: ( n < 1 or n = 1 or n = 2 or n = 3 ) by XXREAL_0:1; n <> 0 by A1, INT_2:3; hence ( n = 1 or n = 3 ) by A4, A2, NAT_1:14; ::_thesis: verum end; hence 3 is prime by INT_2:def_4; ::_thesis: verum end; theorem Th42: :: PEPIN:42 for n being Nat st n <> 0 holds Euler n <> 0 proof let n be Nat; ::_thesis: ( n <> 0 implies Euler n <> 0 ) assume A1: n <> 0 ; ::_thesis: Euler n <> 0 set X = { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } ; A2: { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } c= finSeg n proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } or x in finSeg n ) assume x in { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } ; ::_thesis: x in finSeg n then ex xx being Element of NAT st ( x = xx & n,xx are_relative_prime & xx >= 1 & xx <= n ) ; hence x in finSeg n by FINSEQ_1:1; ::_thesis: verum end; assume Euler n = 0 ; ::_thesis: contradiction then A3: card { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } = 0 by EULER_1:def_1; reconsider X = { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } as finite set by A2; ex k being Nat st k in X proof take 1 ; ::_thesis: 1 in X n gcd 1 = 1 by NEWTON:51; then A4: n,1 are_relative_prime by INT_2:def_3; 1 <= n by A1, NAT_1:14; hence 1 in X by A4; ::_thesis: verum end; hence contradiction by A3; ::_thesis: verum end; 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 proof let n be Nat; ::_thesis: ( n <> 0 implies n div n = 1 ) assume n <> 0 ; ::_thesis: n div n = 1 then (n * 1) div n = 1 by NAT_D:18; hence n div n = 1 ; ::_thesis: verum end; 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 proof let p, q, n, k1, k2 be Nat; ::_thesis: ( 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 being Element of NAT st m < n holds Crypto ((Crypto (m,n,k1)),n,k2) = m ) assume that A1: p is prime and A2: q is prime and A3: p <> q and A4: n = p * q and A5: k1, Euler n are_relative_prime and A6: (k1 * k2) mod (Euler n) = 1 ; ::_thesis: for m being Element of NAT st m < n holds Crypto ((Crypto (m,n,k1)),n,k2) = m A7: q > 1 by A2, INT_2:def_4; A8: p > 1 by A1, INT_2:def_4; then A9: Euler n = (Euler p) * (Euler q) by A1, A2, A3, A4, A7, EULER_1:21, INT_2:30 .= (p - 1) * (Euler q) by A1, EULER_1:20 .= (p - 1) * (q - 1) by A2, EULER_1:20 ; A10: n > 1 by A4, A8, A7, XREAL_1:161; A11: ( p <> 0 & q <> 0 ) by A1, A2, INT_2:def_4; then reconsider p1 = p - 1, q1 = q - 1 as Element of NAT by Lm3, INT_1:3; n <> 0 by A4, A11, XCMPLX_1:6; then A12: Euler n <> 0 by Th42; ( not p1 = 1 or not q1 = 1 ) by A3; then A13: p1 * q1 <> 1 by NAT_1:15; A14: k1 <> 0 proof assume k1 = 0 ; ::_thesis: contradiction then k1 gcd (Euler n) = Euler n by NEWTON:52; hence contradiction by A5, A9, A13, INT_2:def_3; ::_thesis: verum end; A15: k2 <> 0 by A6, NAT_D:26; A16: q > 0 by A2, INT_2:def_4; let m be Element of NAT ; ::_thesis: ( m < n implies Crypto ((Crypto (m,n,k1)),n,k2) = m ) assume A17: m < n ; ::_thesis: Crypto ((Crypto (m,n,k1)),n,k2) = m A18: p > 0 by A1, INT_2:def_4; now__::_thesis:_Crypto_((Crypto_(m,n,k1)),n,k2)_=_m percases ( m = 0 or m = 1 or ( m <> 0 & m <> 1 ) ) ; supposeA19: m = 0 ; ::_thesis: Crypto ((Crypto (m,n,k1)),n,k2) = m then m |^ k1 = 0 by A14, NAT_1:14, NEWTON:11; then (m |^ k1) mod n = 0 by NAT_D:26; then (Crypto (m,n,k1)) |^ k2 = 0 by A15, NAT_1:14, NEWTON:11; hence Crypto ((Crypto (m,n,k1)),n,k2) = m by A19, NAT_D:26; ::_thesis: verum end; supposeA20: m = 1 ; ::_thesis: Crypto ((Crypto (m,n,k1)),n,k2) = m then m |^ k1 = 1 by NEWTON:10; then (m |^ k1) mod n = 1 by A10, NAT_D:14; then (Crypto (m,n,k1)) |^ k2 = 1 by NEWTON:10; hence Crypto ((Crypto (m,n,k1)),n,k2) = m by A10, A20, NAT_D:14; ::_thesis: verum end; supposeA21: ( m <> 0 & m <> 1 ) ; ::_thesis: Crypto ((Crypto (m,n,k1)),n,k2) = m A22: for t being Element of NAT holds (m |^ (((t * p1) * q1) + 1)) mod n = m proof let t be Element of NAT ; ::_thesis: (m |^ (((t * p1) * q1) + 1)) mod n = m now__::_thesis:_(m_|^_(((t_*_p1)_*_q1)_+_1))_mod_n_=_m m |^ ((t * p1) * q1) >= 1 by A21, NAT_1:14, PREPOWER:11; then (m |^ ((t * p1) * q1)) - 1 >= 1 - 1 by XREAL_1:9; then reconsider a = (m |^ ((t * p1) * q1)) - 1 as Element of NAT by INT_1:3; A23: p divides m * a proof now__::_thesis:_p_divides_m_*_a percases ( m gcd p = 1 or m gcd p <> 1 ) ; suppose m gcd p = 1 ; ::_thesis: p divides m * a then A24: m,p are_relative_prime by INT_2:def_3; m |^ (t * q1) <> 0 by A21, PREPOWER:5; then ((m |^ (t * q1)) |^ (p1 + 1)) mod p = (m |^ (t * q1)) mod p by A1, A21, A24, EULER_2:17, EULER_2:19; then (((m |^ (t * q1)) |^ p1) * (m |^ (t * q1))) mod p = (m |^ (t * q1)) mod p by NEWTON:6; then ((m |^ (t * q1)) |^ p1) mod p = 1 by A8, A21, A24, Th11, EULER_2:17; then (m |^ ((t * q1) * p1)) mod p = 1 by NEWTON:9; then m |^ ((t * p1) * q1) = (p * ((m |^ ((t * p1) * q1)) div p)) + 1 by A18, NAT_D:2; then p divides a by NAT_D:def_3; hence p divides m * a by NAT_D:9; ::_thesis: verum end; suppose m gcd p <> 1 ; ::_thesis: p divides m * a then not m,p are_relative_prime by INT_2:def_3; then m gcd p = p by A1, Th2; then p divides m by NAT_D:def_5; hence p divides m * a by NAT_D:9; ::_thesis: verum end; end; end; hence p divides m * a ; ::_thesis: verum end; q divides m * a proof now__::_thesis:_q_divides_m_*_a percases ( m gcd q = 1 or m gcd q <> 1 ) ; suppose m gcd q = 1 ; ::_thesis: q divides m * a then A25: m,q are_relative_prime by INT_2:def_3; m |^ (t * p1) <> 0 by A21, PREPOWER:5; then ((m |^ (t * p1)) |^ (q1 + 1)) mod q = (m |^ (t * p1)) mod q by A2, A21, A25, EULER_2:17, EULER_2:19; then (((m |^ (t * p1)) |^ q1) * (m |^ (t * p1))) mod q = (m |^ (t * p1)) mod q by NEWTON:6; then ((m |^ (t * p1)) |^ q1) mod q = 1 by A7, A21, A25, Th11, EULER_2:17; then (m |^ ((t * p1) * q1)) mod q = 1 by NEWTON:9; then m |^ ((t * p1) * q1) = (q * ((m |^ ((t * p1) * q1)) div q)) + 1 by A16, NAT_D:2; then q divides a by NAT_D:def_3; hence q divides m * a by NAT_D:9; ::_thesis: verum end; suppose m gcd q <> 1 ; ::_thesis: q divides m * a then not m,q are_relative_prime by INT_2:def_3; then m gcd q = q by A2, Th2; then q divides m by NAT_D:def_5; hence q divides m * a by NAT_D:9; ::_thesis: verum end; end; end; hence q divides m * a ; ::_thesis: verum end; then p * q divides m * a by A1, A2, A3, A23, Th4, INT_2:30; then consider k being Nat such that A26: m * a = (p * q) * k by NAT_D:def_3; m * ((m |^ ((t * p1) * q1)) - 1) = (m * (m |^ ((t * p1) * q1))) - (m * 1) .= (m |^ (((t * p1) * q1) + 1)) - m by NEWTON:6 ; then (m |^ (((t * p1) * q1) + 1)) - (m - m) = (n * k) + m by A4, A26, XCMPLX_1:37; hence (m |^ (((t * p1) * q1) + 1)) mod n = m by A17, NAT_D:def_2; ::_thesis: verum end; hence (m |^ (((t * p1) * q1) + 1)) mod n = m ; ::_thesis: verum end; reconsider t = (k1 * k2) div (Euler n) as Element of NAT ; k1 * k2 = ((p1 * q1) * t) + 1 by A6, A12, A9, NAT_D:2 .= ((t * p1) * q1) + 1 ; then (m |^ (k1 * k2)) mod n = m by A22; then ((m |^ k1) |^ k2) mod n = m by NEWTON:9; hence Crypto ((Crypto (m,n,k1)),n,k2) = m by Th12; ::_thesis: verum end; end; end; hence Crypto ((Crypto (m,n,k1)),n,k2) = m ; ::_thesis: verum end; 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 ) ) ) proof set A = { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } ; A3: { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } c= NAT proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } or a in NAT ) assume a in { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } ; ::_thesis: a in NAT then ex k being Element of NAT st ( k = a & k > 0 & (i |^ k) mod p = 1 ) ; hence a in NAT ; ::_thesis: verum end; i <> 0 proof assume i = 0 ; ::_thesis: contradiction then i gcd p = p by NEWTON:52; hence contradiction by A1, A2, INT_2:def_3; ::_thesis: verum end; then A4: (i |^ (Euler p)) mod p = 1 by A1, A2, EULER_2:18; Euler p <> 0 by A1, Th42; then Euler p in { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } by A4; then reconsider A = { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } as non empty Subset of NAT by A3; set a = the Element of A; defpred S1[ set ] means $1 in A; the Element of A is Element of NAT ; then A5: ex kk being Nat st S1[kk] ; consider kk being Nat such that A6: S1[kk] and A7: for n being Nat st S1[n] holds kk <= n from NAT_1:sch_5(A5); take kk ; ::_thesis: ( kk is Element of NAT & kk > 0 & (i |^ kk) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds ( 0 < kk & kk <= k ) ) ) A8: for k being Nat st k > 0 & (i |^ k) mod p = 1 holds kk <= k proof let k be Nat; ::_thesis: ( k > 0 & (i |^ k) mod p = 1 implies kk <= k ) assume A9: ( k > 0 & (i |^ k) mod p = 1 ) ; ::_thesis: kk <= k k in NAT by ORDINAL1:def_12; then k in A by A9; hence kk <= k by A7; ::_thesis: verum end; ex k being Element of NAT st ( k = kk & k > 0 & (i |^ k) mod p = 1 ) by A6; hence ( kk is Element of NAT & kk > 0 & (i |^ kk) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds ( 0 < kk & kk <= k ) ) ) by A8; ::_thesis: verum end; 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 proof let k1, k2 be Element of NAT ; ::_thesis: ( k1 > 0 & (i |^ k1) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds ( 0 < k1 & k1 <= k ) ) & k2 > 0 & (i |^ k2) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds ( 0 < k2 & k2 <= k ) ) implies k1 = k2 ) assume ( k1 > 0 & (i |^ k1) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds ( 0 < k1 & k1 <= k ) ) & k2 > 0 & (i |^ k2) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds ( 0 < k2 & k2 <= k ) ) ) ; ::_thesis: k1 = k2 then ( k1 <= k2 & k2 <= k1 ) ; hence k1 = k2 by XXREAL_0:1; ::_thesis: verum end; 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 proof let p be Nat; ::_thesis: ( p > 1 implies order (1,p) = 1 ) assume A1: p > 1 ; ::_thesis: order (1,p) = 1 p gcd 1 = 1 by NEWTON:51; then A2: 1,p are_relative_prime by INT_2:def_3; (1 |^ 1) mod p = 1 mod p by NEWTON:5 .= 1 by A1, NAT_D:24 ; then order (1,p) <= 1 by A1, A2, Def2; then ( order (1,p) < 1 or order (1,p) = 1 ) by XXREAL_0:1; then A3: ( order (1,p) = 0 or order (1,p) = 1 ) by NAT_1:14; assume order (1,p) <> 1 ; ::_thesis: contradiction hence contradiction by A1, A2, A3, Def2; ::_thesis: verum end; 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 proof let p, i, n be Nat; ::_thesis: ( p > 1 & (i |^ n) mod p = 1 & i,p are_relative_prime implies order (i,p) divides n ) assume that A1: p > 1 and A2: (i |^ n) mod p = 1 and A3: i,p are_relative_prime ; ::_thesis: order (i,p) divides n A4: order (i,p) <> 0 by A1, A3, Def2; A5: (i |^ (order (i,p))) mod p = 1 by A1, A3, Def2; n mod (order (i,p)) = 0 proof set I = n mod (order (i,p)); consider t being Nat such that A6: n = ((order (i,p)) * t) + (n mod (order (i,p))) and A7: n mod (order (i,p)) < order (i,p) by A4, NAT_D:def_2; reconsider t = t as Element of NAT by ORDINAL1:def_12; ((i |^ ((order (i,p)) * t)) * (i |^ (n mod (order (i,p))))) mod p = 1 by A2, A6, NEWTON:8; then (((i |^ (order (i,p))) |^ t) * (i |^ (n mod (order (i,p))))) mod p = 1 by NEWTON:9; then ((((i |^ (order (i,p))) |^ t) mod p) * (i |^ (n mod (order (i,p))))) mod p = 1 by EULER_2:8; then A8: (1 * (i |^ (n mod (order (i,p))))) mod p = 1 by A1, A5, Th35; assume n mod (order (i,p)) <> 0 ; ::_thesis: contradiction hence contradiction by A1, A3, A7, A8, Def2; ::_thesis: verum end; hence order (i,p) divides n by A4, Th6; ::_thesis: verum 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 proof let p, i, n be Nat; ::_thesis: ( p > 1 & i,p are_relative_prime & order (i,p) divides n implies (i |^ n) mod p = 1 ) assume that A1: p > 1 and A2: i,p are_relative_prime and A3: order (i,p) divides n ; ::_thesis: (i |^ n) mod p = 1 consider t being Nat such that A4: n = (order (i,p)) * t by A3, NAT_D:def_3; reconsider t = t as Element of NAT by ORDINAL1:def_12; (i |^ n) mod p = ((i |^ (order (i,p))) |^ t) mod p by A4, NEWTON:9 .= (((i |^ (order (i,p))) mod p) |^ t) mod p by Th12 .= (1 |^ t) mod p by A1, A2, Def2 .= 1 mod p by NEWTON:10 .= 1 by A1, NAT_D:24 ; hence (i |^ n) mod p = 1 ; ::_thesis: verum end; 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 proof let p, i be Nat; ::_thesis: ( p is prime & i,p are_relative_prime implies order (i,p) divides p -' 1 ) assume that A1: p is prime and A2: i,p are_relative_prime ; ::_thesis: order (i,p) divides p -' 1 ( (i |^ (p -' 1)) mod p = 1 & p > 1 ) by A1, A2, Th37, INT_2:def_4; hence order (i,p) divides p -' 1 by A2, Th47; ::_thesis: verum end; 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 proof Fermat 0 = (2 |^ 1) + 1 by NEWTON:4 .= 2 + 1 by NEWTON:5 ; hence Fermat 0 = 3 ; ::_thesis: verum end; theorem Th51: :: PEPIN:51 Fermat 1 = 5 proof Fermat 1 = (2 |^ (1 + 1)) + 1 by NEWTON:5 .= ((2 |^ 1) * 2) + 1 by NEWTON:6 .= (2 * 2) + 1 by NEWTON:5 ; hence Fermat 1 = 5 ; ::_thesis: verum end; theorem Th52: :: PEPIN:52 Fermat 2 = 17 proof thus Fermat 2 = (2 |^ (2 |^ (1 + 1))) + 1 .= (2 |^ ((2 |^ 1) * 2)) + 1 by NEWTON:6 .= (2 |^ (2 * 2)) + 1 by NEWTON:5 .= (2 |^ (3 + 1)) + 1 .= ((2 |^ (2 + 1)) * 2) + 1 by NEWTON:6 .= (((2 |^ (1 + 1)) * 2) * 2) + 1 by NEWTON:6 .= ((((2 |^ 1) * 2) * 2) * 2) + 1 by NEWTON:6 .= (((2 * 2) * 2) * 2) + 1 by NEWTON:5 .= 17 ; ::_thesis: verum end; theorem Th53: :: PEPIN:53 Fermat 3 = 257 proof thus Fermat 3 = (2 |^ (4 + 4)) + 1 by POWER:61 .= ((2 |^ 4) * (2 |^ 4)) + 1 by NEWTON:8 .= 257 by POWER:62 ; ::_thesis: verum end; theorem Th54: :: PEPIN:54 Fermat 4 = (256 * 256) + 1 proof thus Fermat 4 = (2 |^ (8 + 8)) + 1 by POWER:62 .= ((2 |^ 8) * (2 |^ 8)) + 1 by NEWTON:8 .= (((2 |^ 4) * (2 |^ 4)) * (2 |^ (4 + 4))) + 1 by NEWTON:8 .= (256 * 256) + 1 by NEWTON:8, POWER:62 ; ::_thesis: verum end; theorem Th55: :: PEPIN:55 for n being Nat holds Fermat n > 2 proof let n be Nat; ::_thesis: Fermat n > 2 set 2N = 2 |^ (2 |^ n); 2 |^ (2 |^ n) > 1 by Lm2; then (2 |^ (2 |^ n)) + 1 > 1 + 1 by XREAL_1:6; hence Fermat n > 2 ; ::_thesis: verum end; Lm12: for n being Nat holds Fermat n > 1 proof let n be Nat; ::_thesis: Fermat n > 1 Fermat n <> 1 by Th55; then ( Fermat n > 1 or Fermat n < 1 ) by XXREAL_0:1; hence Fermat n > 1 by NAT_1:14; ::_thesis: verum end; Lm13: for n being Nat holds ((Fermat n) -' 1) mod 2 = 0 proof let n be Nat; ::_thesis: ((Fermat n) -' 1) mod 2 = 0 2 mod 2 = 0 by NAT_D:25; then ( (Fermat n) -' 1 = 2 |^ (2 |^ n) & 2 is even ) by NAT_2:21, NAT_D:34; then (Fermat n) -' 1 is even by Th21, PREPOWER:6; hence ((Fermat n) -' 1) mod 2 = 0 by NAT_2:21; ::_thesis: verum end; Lm14: for n being Nat holds (Fermat n) -' 1 > 0 proof let n be Nat; ::_thesis: (Fermat n) -' 1 > 0 Fermat n > 1 by Lm12; then (Fermat n) - 1 > 1 - 1 by XREAL_1:9; hence (Fermat n) -' 1 > 0 by XREAL_0:def_2; ::_thesis: verum end; Lm15: for n being Nat holds (Fermat n) mod (2 |^ (2 |^ n)) = 1 proof let n be Nat; ::_thesis: (Fermat n) mod (2 |^ (2 |^ n)) = 1 set 2N = 2 |^ (2 |^ n); (Fermat n) mod (2 |^ (2 |^ n)) = (((2 |^ (2 |^ n)) * 1) + 1) mod (2 |^ (2 |^ n)) .= 1 mod (2 |^ (2 |^ n)) by NAT_D:21 .= 1 by Lm2, NAT_D:14 ; hence (Fermat n) mod (2 |^ (2 |^ n)) = 1 ; ::_thesis: verum end; Lm16: for n being Nat holds Fermat n is odd proof let n be Nat; ::_thesis: Fermat n is odd ( (Fermat n) - 1 = (Fermat n) -' 1 & ((Fermat n) -' 1) mod 2 = 0 ) by Lm13, XREAL_0:def_2; hence Fermat n is odd by NAT_2:21; ::_thesis: verum 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 proof let p, n be Nat; ::_thesis: ( p is prime & p > 2 & p divides Fermat n implies ex k being Element of NAT st p = (k * (2 |^ (n + 1))) + 1 ) assume that A1: p is prime and A2: p > 2 and A3: p divides Fermat n ; ::_thesis: ex k being Element of NAT st p = (k * (2 |^ (n + 1))) + 1 A4: p > 1 by A1, INT_2:def_4; set t = (Fermat n) div p; set 2N = 2 |^ (2 |^ n); (p * ((Fermat n) div p)) - 0 = p * ((Fermat n) div p) ; then ( - 1, - 1 are_congruent_mod p & p * ((Fermat n) div p), 0 are_congruent_mod p ) by INT_1:11, INT_1:def_5; then A5: (p * ((Fermat n) div p)) + (- 1),0 + (- 1) are_congruent_mod p by INT_1:16; A6: p * ((Fermat n) div p) = (2 |^ (2 |^ n)) + 1 by A3, NAT_D:3; A7: (2 |^ (2 |^ n)) mod p <> 1 proof assume (2 |^ (2 |^ n)) mod p = 1 ; ::_thesis: contradiction then 2 |^ (2 |^ n),1 are_congruent_mod p by A4, Th39; then 1,2 |^ (2 |^ n) are_congruent_mod p by INT_1:14; then 1, - 1 are_congruent_mod p by A6, A5, INT_1:15; then p divides 1 - (- 1) by INT_2:15; hence contradiction by A2, NAT_D:7; ::_thesis: verum end; A8: 2,p are_relative_prime by A1, A2, INT_2:28, INT_2:30; then order (2,p) <> 0 by A4, Def2; then order (2,p) >= 1 by NAT_1:14; then A9: ( order (2,p) = 1 or order (2,p) > 1 ) by XXREAL_0:1; A10: 2 |^ (2 |^ n) > 1 by Th25, PREPOWER:6; then (2 |^ (2 |^ n)) * (2 |^ (2 |^ n)) > 1 * (2 |^ (2 |^ n)) by XREAL_1:68; then A11: (2 |^ (2 |^ n)) ^2 > 1 by A10, XXREAL_0:2; (2 |^ (2 |^ n)) ^2 ,(- 1) ^2 are_congruent_mod p by A6, A5, INT_1:18; then ((2 |^ (2 |^ n)) ^2) mod p = 1 by A4, A11, Lm11; then (2 |^ (2 |^ (n + 1))) mod p = 1 by Lm8; then A12: order (2,p) divides 2 |^ (n + 1) by A4, A8, Th47; (2 |^ (n + 1)) div 2 = (2 * (2 |^ n)) div 2 by NEWTON:6 .= 2 |^ n by NAT_D:18 ; then not order (2,p) divides (2 |^ (n + 1)) div 2 by A1, A2, A4, A7, Th48, INT_2:28, INT_2:30; then order (2,p) = 2 |^ (n + 1) by A12, A9, Th38, INT_2:28, NAT_D:6; then 2 |^ (n + 1) divides p -' 1 by A1, A2, Th49, INT_2:28, INT_2:30; then consider t2 being Nat such that A13: p -' 1 = (2 |^ (n + 1)) * t2 by NAT_D:def_3; reconsider t2 = t2 as Element of NAT by ORDINAL1:def_12; p - 1 > 1 - 1 by A4, XREAL_1:9; then p - 1 = (2 |^ (n + 1)) * t2 by A13, XREAL_0:def_2; then p = (t2 * (2 |^ (n + 1))) + 1 ; hence ex k being Element of NAT st p = (k * (2 |^ (n + 1))) + 1 ; ::_thesis: verum end; theorem Th57: :: PEPIN:57 for n being Nat st n <> 0 holds 3, Fermat n are_relative_prime proof let n be Nat; ::_thesis: ( n <> 0 implies 3, Fermat n are_relative_prime ) assume A1: n <> 0 ; ::_thesis: 3, Fermat n are_relative_prime (Fermat n) gcd 3 <> 3 proof assume (Fermat n) gcd 3 = 3 ; ::_thesis: contradiction then 3 divides Fermat n by NAT_D:def_5; then consider k being Element of NAT such that A2: 3 = (k * (2 |^ (n + 1))) + 1 by Th41, Th56; 1 = (k * (2 |^ (n + 1))) div 2 by A2, NAT_2:3; then 1 = k * (2 |^ n) by Lm5; then 2 |^ n = 1 by NAT_1:15; then 2 |^ n = 2 |^ 0 by NEWTON:4; hence contradiction by A1, Th30; ::_thesis: verum end; hence 3, Fermat n are_relative_prime by Th2, Th41; ::_thesis: verum end; begin 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 proof let n be Nat; ::_thesis: ( 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n implies Fermat n is prime ) percases ( n = 0 or n > 0 ) ; suppose n = 0 ; ::_thesis: ( 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n implies Fermat n is prime ) hence ( 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n implies Fermat n is prime ) by Th41, Th50; ::_thesis: verum end; supposeA1: n > 0 ; ::_thesis: ( 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n implies Fermat n is prime ) Fermat n > 2 by Th55; then consider p being Element of NAT such that A2: p is prime and A3: p divides Fermat n by INT_2:31; set d = order (3,p); consider i being Nat such that A4: Fermat n = p * i by A3, NAT_D:def_3; A5: p > 2 proof assume p <= 2 ; ::_thesis: contradiction then ( p = 2 or p < 1 + 1 ) by XXREAL_0:1; then A6: ( p = 2 or p <= 1 ) by NAT_1:13; A7: p <> 0 by A2, INT_2:def_4; Fermat n is odd by Lm16; then (Fermat n) mod p = 1 by A2, A6, INT_2:def_4, NAT_2:22; hence contradiction by A3, A7, Th6; ::_thesis: verum end; A8: (Fermat n) - 1 >= 0 ; assume A9: 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n ; ::_thesis: Fermat n is prime then A10: (3 |^ (((Fermat n) -' 1) div 2)) ^2 ,(- 1) ^2 are_congruent_mod Fermat n by INT_1:18; ((Fermat n) -' 1) mod 2 = 0 by Lm13; then A11: 3 |^ ((Fermat n) -' 1),(- 1) ^2 are_congruent_mod Fermat n by A10, Th27; set 2N = 2 |^ (2 |^ n); assume A12: not Fermat n is prime ; ::_thesis: contradiction reconsider i = i as Element of NAT by ORDINAL1:def_12; A13: 1 < p by A2, INT_2:def_4; A14: p <> 3 proof 1 gcd i = 1 by NEWTON:51; then A15: (3 * 1) gcd (3 * i) = 3 by EULER_1:5; assume p = 3 ; ::_thesis: contradiction then not 3, Fermat n are_relative_prime by A4, A15, INT_2:def_3; hence contradiction by A1, Th57; ::_thesis: verum end; then order (3,p) divides p -' 1 by A2, Th41, Th49, INT_2:30; then consider x being Nat such that A16: p -' 1 = (order (3,p)) * x by NAT_D:def_3; A17: 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod p by A9, A4, INT_1:20; A18: not order (3,p) divides ((Fermat n) -' 1) div 2 proof assume order (3,p) divides ((Fermat n) -' 1) div 2 ; ::_thesis: contradiction then (3 |^ (((Fermat n) -' 1) div 2)) mod p = 1 by A2, A14, A13, Th41, Th48, INT_2:30; then 3 |^ (((Fermat n) -' 1) div 2),1 are_congruent_mod p by A13, Th39; then 1, - 1 are_congruent_mod p by A17, Th40; then p divides 1 - (- 1) by INT_2:15; hence contradiction by A5, NAT_D:7; ::_thesis: verum end; then A19: not order (3,p) divides (2 |^ (2 |^ n)) div 2 by A8, XREAL_0:def_2; A20: 3,p are_relative_prime by A2, A14, Th41, INT_2:30; then A21: order (3,p) <> 0 by A13, Def2; A22: order (3,p) > 1 proof assume A23: order (3,p) <= 1 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( order (3,p) < 1 or order (3,p) = 1 ) by A23, XXREAL_0:1; suppose order (3,p) < 1 ; ::_thesis: contradiction hence contradiction by A21, NAT_1:14; ::_thesis: verum end; suppose order (3,p) = 1 ; ::_thesis: contradiction hence contradiction by A18, NAT_D:6; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; 3 |^ ((Fermat n) -' 1) > 1 by Lm14, Th25; then (3 |^ ((Fermat n) -' 1)) mod p = 1 by A4, A13, A11, Lm11, INT_1:20; then order (3,p) divides (Fermat n) -' 1 by A20, A13, Th47; then order (3,p) divides 2 |^ (2 |^ n) by A8, XREAL_0:def_2; then order (3,p) = 2 |^ (2 |^ n) by A19, A22, Th38, INT_2:28 .= (Fermat n) -' 1 by A8, XREAL_0:def_2 ; then A24: order (3,p) = 2 |^ (2 |^ n) by A8, XREAL_0:def_2; A25: (p * i) mod (2 |^ (2 |^ n)) = 1 by A4, Lm15; p - 1 > 1 - 1 by A13, XREAL_1:9; then A26: p - 1 = x * (order (3,p)) by A16, XREAL_0:def_2; then A27: p = (x * (2 |^ (2 |^ n))) + 1 by A24; then p mod (2 |^ (2 |^ n)) = 1 mod (2 |^ (2 |^ n)) by NAT_D:21 .= 1 by Lm2, NAT_D:24 ; then (1 * i) mod (2 |^ (2 |^ n)) = 1 by A25, EULER_2:8; then consider y being Nat such that A28: i = ((2 |^ (2 |^ n)) * y) + 1 and 1 < 2 |^ (2 |^ n) by NAT_D:def_2; A29: 2 |^ (2 |^ n) <> 0 by Lm2; A30: x >= 1 proof assume x < 1 ; ::_thesis: contradiction then p = (0 * (2 |^ (2 |^ n))) + 1 by A27, NAT_1:14; hence contradiction by A2, INT_2:def_4; ::_thesis: verum end; reconsider y = y as Element of NAT by ORDINAL1:def_12; Fermat n = ((x * (2 |^ (2 |^ n))) + 1) * ((y * (2 |^ (2 |^ n))) + 1) by A4, A24, A26, A28 .= ((2 |^ (2 |^ n)) * ((((x * y) * (2 |^ (2 |^ n))) + x) + y)) + 1 ; then A31: 1 = ((2 |^ (2 |^ n)) * ((((x * y) * (2 |^ (2 |^ n))) + x) + y)) div (2 |^ (2 |^ n)) by A29, Th44 .= (((x * y) * (2 |^ (2 |^ n))) + x) + y by A29, NAT_D:18 ; 2 |^ (2 |^ n) > 1 by Lm2; then p = (1 * (2 |^ (2 |^ n))) + 1 by A27, A30, A31, Lm1 .= Fermat n ; hence contradiction by A12, A2; ::_thesis: verum end; end; end; Lm17: 3 |^ 2 = 9 proof 3 |^ 2 = 3 |^ (1 + 1) .= (3 |^ 1) * (3 |^ 1) by NEWTON:8 .= 3 * (3 |^ 1) by NEWTON:5 .= 3 * 3 by NEWTON:5 ; hence 3 |^ 2 = 9 ; ::_thesis: verum end; Lm18: 3 |^ 4 = 81 proof 3 |^ 4 = 3 |^ (2 + 2) .= (3 |^ 2) * (3 |^ 2) by NEWTON:8 ; hence 3 |^ 4 = 81 by Lm17; ::_thesis: verum end; Lm19: 3 |^ 8 = 6561 proof 3 |^ 8 = 3 |^ (4 + 4) .= (3 |^ 4) * (3 |^ 4) by NEWTON:8 ; hence 3 |^ 8 = 6561 by Lm18; ::_thesis: verum end; Lm20: 3 |^ 16 = 6561 * 6561 proof 3 |^ 16 = 3 |^ (8 + 8) .= (3 |^ 8) * (3 |^ 8) by NEWTON:8 ; hence 3 |^ 16 = 6561 * 6561 by Lm19; ::_thesis: verum end; Lm21: for i being Nat holds Fermat 1 divides (3 |^ ((4 * i) + 2)) + 1 proof let i be Nat; ::_thesis: Fermat 1 divides (3 |^ ((4 * i) + 2)) + 1 defpred S1[ Nat] means Fermat 1 divides (3 |^ ((4 * $1) + 2)) + 1; A1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume Fermat 1 divides (3 |^ ((4 * n) + 2)) + 1 ; ::_thesis: S1[n + 1] then consider m being Nat such that A2: (3 |^ ((4 * n) + 2)) + 1 = (Fermat 1) * m by NAT_D:def_3; 3 |^ (4 * n) >= 3 |^ 0 by PREPOWER:93; then 3 |^ (4 * n) >= 1 by NEWTON:4; then (3 |^ (4 * n)) * (3 |^ 2) > 0 * (3 |^ 2) by Lm17, XREAL_1:68; then 3 |^ ((4 * n) + 2) > 0 by NEWTON:8; then (3 |^ ((4 * n) + 2)) + 1 > 0 + 1 by XREAL_1:6; then ((Fermat 1) * m) * 81 > 1 * 81 by A2, XREAL_1:68; then (((Fermat 1) * m) * 81) / (Fermat 1) > (1 * 81) / (Fermat 1) by XREAL_1:74; then ((m * (Fermat 1)) * 81) * ((Fermat 1) ") > (1 * 81) / (Fermat 1) by XCMPLX_0:def_9; then ((m * 81) * ((Fermat 1) ")) * (Fermat 1) > (1 * 81) / (Fermat 1) ; then ((m * 81) / (Fermat 1)) * (Fermat 1) > (1 * 81) / (Fermat 1) by XCMPLX_0:def_9; then m * 81 > 81 / 5 by Th51, XCMPLX_1:87; then m * 81 > 16 by XXREAL_0:2; then A3: (m * 81) + (- 16) > 16 + (- 16) by XREAL_1:6; (3 |^ ((4 * (n + 1)) + 2)) + 1 = (3 |^ (((4 * n) + 2) + 4)) + 1 .= ((((Fermat 1) * m) - 1) * (3 |^ 4)) + 1 by A2, NEWTON:8 .= (Fermat 1) * ((m * 81) - 16) by Lm18, Th51 .= (Fermat 1) * ((m * 81) -' 16) by A3, XREAL_0:def_2 ; hence S1[n + 1] by NAT_D:def_3; ::_thesis: verum end; (3 |^ ((4 * 0) + 2)) + 1 = 5 * 2 by Lm17; then A4: S1[ 0 ] by Th51, NAT_D:def_3; for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1); hence Fermat 1 divides (3 |^ ((4 * i) + 2)) + 1 ; ::_thesis: verum end; Lm22: for n being Nat st n = 1 holds 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n proof let n be Nat; ::_thesis: ( n = 1 implies 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n ) A1: 2 -' 1 = 2 - 1 by XREAL_0:def_2 .= 1 + 0 ; A2: 5 -' 1 = 5 - 1 by XREAL_0:def_2 .= 4 + 0 ; A3: 2 to_power 2 = 2 |^ (1 + 1) .= (2 |^ 1) * 2 by NEWTON:6 .= 2 * 2 by NEWTON:5 ; assume A4: n = 1 ; ::_thesis: 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n 2 to_power 1 = 2 |^ 1 .= 2 by NEWTON:5 ; then 4 div 2 = 2 to_power (2 -' 1) by A3, NAT_2:16 .= 2 |^ 1 by A1 .= 2 by NEWTON:5 ; then ((Fermat 1) -' 1) div 2 = (4 * 0) + 2 by A2, Th51; then Fermat 1 divides (3 |^ (((Fermat n) -' 1) div 2)) + 1 by A4, Lm21; then Fermat 1 divides (3 |^ (((Fermat n) -' 1) div 2)) - (- 1) ; hence 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n by A4, INT_2:15; ::_thesis: verum end; Lm23: for n being Nat holds Fermat 2 divides (3 |^ ((16 * n) + 8)) + 1 proof let n be Nat; ::_thesis: Fermat 2 divides (3 |^ ((16 * n) + 8)) + 1 defpred S1[ Nat] means Fermat 2 divides (3 |^ ((16 * $1) + 8)) + 1; A1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume Fermat 2 divides (3 |^ ((16 * n) + 8)) + 1 ; ::_thesis: S1[n + 1] then consider m being Nat such that A2: (3 |^ ((16 * n) + 8)) + 1 = (Fermat 2) * m by NAT_D:def_3; 3 |^ (16 * n) >= 3 |^ 0 by PREPOWER:93; then 3 |^ (16 * n) >= 1 by NEWTON:4; then (3 |^ (16 * n)) * (3 |^ 8) > 0 * (3 |^ 8) by Lm19, XREAL_1:68; then 3 |^ ((16 * n) + 8) > 0 by NEWTON:8; then (3 |^ ((16 * n) + 8)) + 1 > 0 + 1 by XREAL_1:6; then ((Fermat 2) * m) * 6561 > 1 * 6561 by A2, XREAL_1:68; then (((Fermat 2) * m) * 6561) * 6561 > 6561 * 6561 by XREAL_1:68; then (((Fermat 2) * m) * 6561) * 6561 > 6562 * 6560 by XXREAL_0:2; then ((((Fermat 2) * m) * 6561) * 6561) / (Fermat 2) > (6560 * 6562) / (Fermat 2) by XREAL_1:74; then (((m * 6561) * (Fermat 2)) * 6561) * ((Fermat 2) ") > (6560 * 6562) / (Fermat 2) by XCMPLX_0:def_9; then (((m * 6561) * 6561) * ((Fermat 2) ")) * (Fermat 2) > (6560 * 6562) / (Fermat 2) ; then (((m * 6561) * 6561) / (Fermat 2)) * (Fermat 2) > (6560 * 6562) / (Fermat 2) by XCMPLX_0:def_9; then (m * 6561) * 6561 > (6560 * 6562) / 17 by Th52, XCMPLX_1:87; then A3: ((m * 6561) * 6561) - (386 * 6560) > (386 * 6560) - (386 * 6560) by XREAL_1:9; (3 |^ ((16 * (n + 1)) + 8)) + 1 = (3 |^ (((16 * n) + 8) + 16)) + 1 .= ((((Fermat 2) * m) - 1) * (3 |^ 16)) + 1 by A2, NEWTON:8 .= (Fermat 2) * (((m * 6561) * 6561) - (386 * 6560)) by Lm20, Th52 .= (Fermat 2) * (((m * 6561) * 6561) -' (386 * 6560)) by A3, XREAL_0:def_2 ; hence S1[n + 1] by NAT_D:def_3; ::_thesis: verum end; (3 |^ ((16 * 0) + 8)) + 1 = 17 * 386 by Lm19; then A4: S1[ 0 ] by Th52, NAT_D:def_3; for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1); hence Fermat 2 divides (3 |^ ((16 * n) + 8)) + 1 ; ::_thesis: verum end; Lm24: (3 |^ 1) mod (Fermat 3) = 3 proof A1: 3 = (0 * 257) + 3 ; thus (3 |^ 1) mod (Fermat 3) = 3 mod (Fermat 3) by NEWTON:5 .= 3 by A1, Th53, NAT_D:def_2 ; ::_thesis: verum end; Lm25: (3 |^ 2) mod (Fermat 3) = 9 proof A1: 9 = (0 * 257) + 9 ; thus (3 |^ 2) mod (Fermat 3) = (3 |^ (1 + 1)) mod (Fermat 3) .= ((3 |^ 1) * (3 |^ 1)) mod (Fermat 3) by NEWTON:8 .= (((3 |^ 1) mod (Fermat 3)) * ((3 |^ 1) mod (Fermat 3))) mod (Fermat 3) by EULER_2:9 .= 9 by A1, Lm24, Th53, NAT_D:def_2 ; ::_thesis: verum end; Lm26: (3 |^ 4) mod (Fermat 3) = 81 proof A1: 81 = (0 * 257) + 81 ; thus (3 |^ 4) mod (Fermat 3) = (3 |^ (2 + 2)) mod (Fermat 3) .= ((3 |^ 2) * (3 |^ 2)) mod (Fermat 3) by NEWTON:8 .= (((3 |^ 2) mod (Fermat 3)) * ((3 |^ 2) mod (Fermat 3))) mod (Fermat 3) by EULER_2:9 .= 81 by A1, Lm25, Th53, NAT_D:def_2 ; ::_thesis: verum end; Lm27: (3 |^ 8) mod (Fermat 3) = 136 proof A1: 6561 = (25 * 257) + 136 ; thus (3 |^ 8) mod (Fermat 3) = (3 |^ (4 + 4)) mod (Fermat 3) .= ((3 |^ 4) * (3 |^ 4)) mod (Fermat 3) by NEWTON:8 .= (((3 |^ 4) mod (Fermat 3)) * ((3 |^ 4) mod (Fermat 3))) mod (Fermat 3) by EULER_2:9 .= 136 by A1, Lm26, Th53, NAT_D:def_2 ; ::_thesis: verum end; Lm28: (3 |^ 16) mod (Fermat 3) = 83 * 3 proof A1: 18496 = (71 * 257) + 249 ; thus (3 |^ 16) mod (Fermat 3) = (3 |^ (8 + 8)) mod (Fermat 3) .= ((3 |^ 8) * (3 |^ 8)) mod (Fermat 3) by NEWTON:8 .= (136 * 136) mod (Fermat 3) by Lm27, EULER_2:9 .= 83 * 3 by A1, Th53, NAT_D:def_2 ; ::_thesis: verum end; Lm29: (3 |^ 32) mod (Fermat 3) = 64 proof A1: ((83 * 3) * 83) * 3 = (241 * 257) + 64 ; (3 |^ 32) mod (Fermat 3) = (3 |^ (16 + 16)) mod (Fermat 3) .= ((3 |^ 16) * (3 |^ 16)) mod (Fermat 3) by NEWTON:8 .= ((83 * 3) * (83 * 3)) mod (Fermat 3) by Lm28, EULER_2:9 .= 64 by A1, Th53, NAT_D:def_2 ; hence (3 |^ 32) mod (Fermat 3) = 64 ; ::_thesis: verum end; Lm30: (3 |^ 64) mod (Fermat 3) = 241 proof A1: 4096 = (15 * 257) + 241 ; thus (3 |^ 64) mod (Fermat 3) = (3 |^ (32 + 32)) mod (Fermat 3) .= ((3 |^ 32) * (3 |^ 32)) mod (Fermat 3) by NEWTON:8 .= (64 * 64) mod (Fermat 3) by Lm29, EULER_2:9 .= 241 by A1, Th53, NAT_D:def_2 ; ::_thesis: verum end; Lm31: (3 |^ 128) mod (Fermat 3) = 256 proof A1: 241 * 241 = (225 * 257) + 256 ; thus (3 |^ 128) mod (Fermat 3) = (3 |^ (64 + 64)) mod (Fermat 3) .= ((3 |^ 64) * (3 |^ 64)) mod (Fermat 3) by NEWTON:8 .= (241 * 241) mod (Fermat 3) by Lm30, EULER_2:9 .= 256 by A1, Th53, NAT_D:def_2 ; ::_thesis: verum end; Lm32: (3 |^ 1) mod (Fermat 4) = 3 proof A1: 3 = (0 * ((256 * 256) + 1)) + 3 ; thus (3 |^ 1) mod (Fermat 4) = 3 mod (Fermat 4) by NEWTON:5 .= 3 by A1, Th54, NAT_D:def_2 ; ::_thesis: verum end; Lm33: (3 |^ 2) mod (Fermat 4) = 9 proof A1: 9 = (0 * ((256 * 256) + 1)) + 9 ; thus (3 |^ 2) mod (Fermat 4) = (3 |^ (1 + 1)) mod (Fermat 4) .= ((3 |^ 1) * (3 |^ 1)) mod (Fermat 4) by NEWTON:8 .= (3 * 3) mod (Fermat 4) by Lm32, EULER_2:9 .= 9 by A1, Th54, NAT_D:def_2 ; ::_thesis: verum end; Lm34: (3 |^ 4) mod (Fermat 4) = 81 proof A1: 81 = (0 * ((256 * 256) + 1)) + 81 ; thus (3 |^ 4) mod (Fermat 4) = (3 |^ (2 + 2)) mod (Fermat 4) .= ((3 |^ 2) * (3 |^ 2)) mod (Fermat 4) by NEWTON:8 .= (9 * 9) mod (Fermat 4) by Lm33, EULER_2:9 .= 81 by A1, Th54, NAT_D:def_2 ; ::_thesis: verum end; Lm35: (3 |^ 8) mod (Fermat 4) = 6561 proof A1: 6561 = (0 * ((256 * 256) + 1)) + 6561 ; thus (3 |^ 8) mod (Fermat 4) = (3 |^ (4 + 4)) mod (Fermat 4) .= ((3 |^ 4) * (3 |^ 4)) mod (Fermat 4) by NEWTON:8 .= (81 * 81) mod (Fermat 4) by Lm34, EULER_2:9 .= 6561 by A1, Th54, NAT_D:def_2 ; ::_thesis: verum end; Lm36: (3 |^ 16) mod (Fermat 4) = (164 * 332) + 1 proof A1: 6561 * 6561 = (656 * ((256 * 256) + 1)) + ((164 * 332) + 1) ; (3 |^ 16) mod (Fermat 4) = (3 |^ (8 + 8)) mod (Fermat 4) .= ((3 |^ 8) * (3 |^ 8)) mod (Fermat 4) by NEWTON:8 .= (6561 * 6561) mod (Fermat 4) by Lm35, EULER_2:9 .= (164 * 332) + 1 by A1, Th54, NAT_D:def_2 ; hence (3 |^ 16) mod (Fermat 4) = (164 * 332) + 1 ; ::_thesis: verum end; Lm37: (3 |^ 32) mod (Fermat 4) = 123 * 503 proof A1: ((164 * 332) + 1) * ((164 * 332) + 1) = ((263 * 172) * ((256 * 256) + 1)) + (123 * 503) ; (3 |^ 32) mod (Fermat 4) = (3 |^ (16 + 16)) mod (Fermat 4) .= ((3 |^ 16) * (3 |^ 16)) mod (Fermat 4) by NEWTON:8 .= (((164 * 332) + 1) * ((164 * 332) + 1)) mod (Fermat 4) by Lm36, EULER_2:9 .= 123 * 503 by A1, Th54, NAT_D:def_2 ; hence (3 |^ 32) mod (Fermat 4) = 123 * 503 ; ::_thesis: verum end; Lm38: (3 |^ 64) mod (Fermat 4) = (14 * 1367) + 1 proof A1: (123 * 503) * (123 * 503) = ((325 + (241 * 241)) * ((256 * 256) + 1)) + ((14 * 1367) + 1) ; (3 |^ 64) mod (Fermat 4) = (3 |^ (32 + 32)) mod (Fermat 4) .= ((3 |^ 32) * (3 |^ 32)) mod (Fermat 4) by NEWTON:8 .= ((123 * 503) * (123 * 503)) mod (Fermat 4) by Lm37, EULER_2:9 .= (14 * 1367) + 1 by A1, Th54, NAT_D:def_2 ; hence (3 |^ 64) mod (Fermat 4) = (14 * 1367) + 1 ; ::_thesis: verum end; Lm39: (3 |^ 128) mod (Fermat 4) = 52 * 289 proof A1: ((14 * 1367) + 1) * ((14 * 1367) + 1) = (5589 * ((256 * 256) + 1)) + (52 * 289) ; (3 |^ 128) mod (Fermat 4) = (3 |^ (64 + 64)) mod (Fermat 4) .= ((3 |^ 64) * (3 |^ 64)) mod (Fermat 4) by NEWTON:8 .= (((14 * 1367) + 1) * ((14 * 1367) + 1)) mod (Fermat 4) by Lm38, EULER_2:9 .= 52 * 289 by A1, Th54, NAT_D:def_2 ; hence (3 |^ 128) mod (Fermat 4) = 52 * 289 ; ::_thesis: verum end; Lm40: (3 |^ 256) mod (Fermat 4) = 282 proof A1: (52 * 289) * (52 * 289) = (3446 * ((256 * 256) + 1)) + 282 ; (3 |^ 256) mod (Fermat 4) = (3 |^ (128 + 128)) mod (Fermat 4) .= ((3 |^ 128) * (3 |^ 128)) mod (Fermat 4) by NEWTON:8 .= ((52 * 289) * (52 * 289)) mod (Fermat 4) by Lm39, EULER_2:9 .= 282 by A1, Th54, NAT_D:def_2 ; hence (3 |^ 256) mod (Fermat 4) = 282 ; ::_thesis: verum end; Lm41: (3 |^ (256 * 2)) mod (Fermat 4) = 71 * 197 proof A1: 282 * 282 = (1 * ((256 * 256) + 1)) + (71 * 197) ; (3 |^ 256) * (3 |^ 256) = 3 |^ (256 + 256) by NEWTON:8 .= 3 |^ 512 ; then (3 |^ (256 * 2)) mod (Fermat 4) = (282 * 282) mod (Fermat 4) by Lm40, EULER_2:9 .= 71 * 197 by A1, Th54, NAT_D:def_2 ; hence (3 |^ (256 * 2)) mod (Fermat 4) = 71 * 197 ; ::_thesis: verum end; Lm42: (3 |^ (256 * 4)) mod (Fermat 4) = 32 * 257 proof A1: (71 * 197) * (71 * 197) = (2985 * ((256 * 256) + 1)) + (32 * 257) ; (3 |^ (256 * 2)) * (3 |^ (256 * 2)) = 3 |^ ((256 * 2) + (256 * 2)) by NEWTON:8 .= 3 |^ 1024 ; then (3 |^ (256 * 4)) mod (Fermat 4) = ((71 * 197) * (71 * 197)) mod (Fermat 4) by Lm41, EULER_2:9 .= 32 * 257 by A1, Th54, NAT_D:def_2 ; hence (3 |^ (256 * 4)) mod (Fermat 4) = 32 * 257 ; ::_thesis: verum end; Lm43: (3 |^ (256 * 8)) mod (Fermat 4) = 81 * 809 proof A1: (32 * 257) * (32 * 257) = (1031 * ((256 * 256) + 1)) + (81 * 809) ; (3 |^ (256 * 4)) * (3 |^ (256 * 4)) = 3 |^ ((256 * 4) + (256 * 4)) by NEWTON:8 .= 3 |^ 2048 ; then (3 |^ (256 * 8)) mod (Fermat 4) = ((32 * 257) * (32 * 257)) mod ((256 * 256) + 1) by Lm42, Th54, EULER_2:9 .= 81 * 809 by A1, NAT_D:def_2 ; hence (3 |^ (256 * 8)) mod (Fermat 4) = 81 * 809 ; ::_thesis: verum end; Lm44: (3 |^ (256 * 16)) mod (Fermat 4) = 64 proof A1: (81 * 809) * (81 * 809) = (((256 * 255) + 241) * ((256 * 256) + 1)) + 64 ; (3 |^ (256 * 8)) * (3 |^ (256 * 8)) = 3 |^ ((256 * 8) + (256 * 8)) by NEWTON:8 .= 3 |^ 4096 ; then (3 |^ (256 * 16)) mod (Fermat 4) = ((81 * 809) * (81 * 809)) mod (Fermat 4) by Lm43, EULER_2:9 .= 64 by A1, Th54, NAT_D:def_2 ; hence (3 |^ (256 * 16)) mod (Fermat 4) = 64 ; ::_thesis: verum end; Lm45: (3 |^ (256 * 32)) mod (Fermat 4) = 256 * 16 proof A1: 64 * 64 = (0 * ((256 * 256) + 1)) + (256 * 16) ; (3 |^ (256 * 16)) * (3 |^ (256 * 16)) = 3 |^ ((256 * 16) + (256 * 16)) by NEWTON:8 .= 3 |^ 8192 ; then (3 |^ (256 * 32)) mod (Fermat 4) = (64 * 64) mod (Fermat 4) by Lm44, EULER_2:9 .= 256 * 16 by A1, Th54, NAT_D:def_2 ; hence (3 |^ (256 * 32)) mod (Fermat 4) = 256 * 16 ; ::_thesis: verum end; Lm46: (3 |^ (256 * 64)) mod (Fermat 4) = 673 * 97 proof A1: (256 * 16) * (256 * 16) = (255 * ((256 * 256) + 1)) + (673 * 97) ; (3 |^ (256 * 32)) * (3 |^ (256 * 32)) = 3 |^ ((256 * 32) + (256 * 32)) by NEWTON:8 .= 3 |^ (256 * (32 + 32)) ; then (3 |^ (256 * 64)) mod (Fermat 4) = ((256 * 16) * (256 * 16)) mod (Fermat 4) by Lm45, EULER_2:9 .= 673 * 97 by A1, Th54, NAT_D:def_2 ; hence (3 |^ (256 * 64)) mod (Fermat 4) = 673 * 97 ; ::_thesis: verum end; Lm47: (3 |^ (256 * 128)) mod (Fermat 4) = 256 * 256 proof A1: ((255 * 256) + 1) * ((255 * 256) + 1) = ((255 * 255) * ((256 * 256) + 1)) + (256 * 256) ; (3 |^ (256 * 64)) * (3 |^ (256 * 64)) = 3 |^ ((256 * 64) + (256 * 64)) by NEWTON:8 .= 3 |^ (256 * (64 + 64)) ; then (3 |^ (256 * 128)) mod (Fermat 4) = ((673 * 97) * (673 * 97)) mod (Fermat 4) by Lm46, EULER_2:9 .= 256 * 256 by A1, Th54, NAT_D:def_2 ; hence (3 |^ (256 * 128)) mod (Fermat 4) = 256 * 256 ; ::_thesis: verum end; Lm48: Fermat 3 divides (3 |^ ((32 * 0) + 128)) + 1 proof A1: 257 = (257 * 1) + 0 ; 1 = (257 * 0) + 1 ; then 1 mod (Fermat 3) = 1 by Th53, NAT_D:def_2; then ((3 |^ ((32 * 0) + 128)) + 1) mod (Fermat 3) = (256 + 1) mod (Fermat 3) by Lm31, EULER_2:6 .= 0 by A1, Th53, NAT_D:def_2 ; hence Fermat 3 divides (3 |^ ((32 * 0) + 128)) + 1 by Th7, NAT_D:6; ::_thesis: verum end; Lm49: Fermat 4 divides (3 |^ ((64 * 0) + (256 * 128))) + 1 proof (256 * 256) + 1 = (((256 * 256) + 1) * 1) + 0 ; then A1: ((256 * 256) + 1) mod (Fermat 4) = 0 by Th54, NAT_D:def_2; 1 = (((256 * 256) + 1) * 0) + 1 ; then 1 mod (Fermat 4) = 1 by Th54, NAT_D:def_2; then ((3 |^ ((64 * 0) + (256 * 128))) + 1) mod (Fermat 4) = 0 by A1, Lm47, EULER_2:6; hence Fermat 4 divides (3 |^ ((64 * 0) + (256 * 128))) + 1 by Th7, NAT_D:6; ::_thesis: verum end; theorem :: PEPIN:59 5 is prime proof 3 |^ (((Fermat 1) -' 1) div 2), - 1 are_congruent_mod Fermat 1 by Lm22; hence 5 is prime by Th51, Th58; ::_thesis: verum end; theorem :: PEPIN:60 17 is prime proof A1: 4 -' 1 = 4 - 1 by XREAL_0:def_2 .= 3 + 0 ; A2: 17 -' 1 = 17 - 1 by XREAL_0:def_2 .= 16 + 0 ; 2 to_power 1 = 2 |^ 1 .= 2 by NEWTON:5 ; then 16 div 2 = 2 to_power (4 -' 1) by NAT_2:16, POWER:62 .= 8 by A1, POWER:61 ; then ((Fermat 2) -' 1) div 2 = (16 * 0) + 8 by A2, Th52; then Fermat 2 divides (3 |^ (((Fermat 2) -' 1) div 2)) + 1 by Lm23; then Fermat 2 divides (3 |^ (((Fermat 2) -' 1) div 2)) - (- 1) ; then 3 |^ (((Fermat 2) -' 1) div 2), - 1 are_congruent_mod Fermat 2 by INT_2:15; hence 17 is prime by Th52, Th58; ::_thesis: verum end; theorem :: PEPIN:61 257 is prime proof A1: 2 to_power 1 = 2 |^ 1 .= 2 by NEWTON:5 ; A2: 8 -' 1 = 8 - 1 by XREAL_0:def_2 .= 7 + 0 ; A3: 257 -' 1 = 257 - 1 by XREAL_0:def_2 .= 256 + 0 ; 2 to_power 8 = 2 |^ (4 + 4) .= 16 * 16 by NEWTON:8, POWER:62 .= 256 ; then 256 div 2 = 2 to_power (8 -' 1) by A1, NAT_2:16 .= 2 |^ (4 + 3) by A2 .= 16 * 8 by NEWTON:8, POWER:61, POWER:62 .= 128 ; then Fermat 3 divides (3 |^ (((Fermat 3) -' 1) div 2)) - (- 1) by A3, Lm48, Th53; then 3 |^ (((Fermat 3) -' 1) div 2), - 1 are_congruent_mod Fermat 3 by INT_2:15; hence 257 is prime by Th53, Th58; ::_thesis: verum end; theorem :: PEPIN:62 (256 * 256) + 1 is prime proof A1: 2 to_power 1 = 2 |^ 1 .= 2 by NEWTON:5 ; A2: 16 -' 1 = 16 - 1 by XREAL_0:def_2 .= 15 + 0 ; A3: ((256 * 256) + 1) -' 1 = ((256 * 256) + 1) - 1 by XREAL_0:def_2 .= (256 * 256) + 0 ; 2 to_power 16 = 2 |^ (8 + 8) .= 256 * 256 by Lm7, NEWTON:8 ; then (256 * 256) div 2 = 2 to_power (16 -' 1) by A1, NAT_2:16 .= 2 |^ (8 + 7) by A2 .= 256 * (2 |^ (4 + 3)) by Lm7, NEWTON:8 .= 256 * (16 * 8) by NEWTON:8, POWER:61, POWER:62 .= 256 * 128 ; then Fermat 4 divides (3 |^ (((Fermat 4) -' 1) div 2)) - (- 1) by A3, Lm49, Th54; then 3 |^ (((Fermat 4) -' 1) div 2), - 1 are_congruent_mod Fermat 4 by INT_2:15; hence (256 * 256) + 1 is prime by Th54, Th58; ::_thesis: verum end; theorem Th63: :: PEPIN:63 for i, j being Nat st j > 0 & i mod j = 0 holds i div j = i / j proof let i, j be Nat; ::_thesis: ( j > 0 & i mod j = 0 implies i div j = i / j ) assume A1: j > 0 ; ::_thesis: ( not i mod j = 0 or i div j = i / j ) assume i mod j = 0 ; ::_thesis: i div j = i / j then consider t being Nat such that A2: i = (j * t) + 0 and A3: 0 < j by A1, NAT_D:def_2; thus i div j = t by A2, A3, NAT_D:def_1 .= i / j by A1, A2, XCMPLX_1:89 ; ::_thesis: verum end; theorem :: PEPIN:64 for i, n being Nat st n > 0 holds (i |^ n) div i = (i |^ n) / i proof let i, n be Nat; ::_thesis: ( n > 0 implies (i |^ n) div i = (i |^ n) / i ) assume A1: n > 0 ; ::_thesis: (i |^ n) div i = (i |^ n) / i percases ( i > 0 or i = 0 ) ; supposeA2: i > 0 ; ::_thesis: (i |^ n) div i = (i |^ n) / i (i |^ n) mod i = 0 by A1, Th36; hence (i |^ n) div i = (i |^ n) / i by A2, Th63; ::_thesis: verum end; supposeA3: i = 0 ; ::_thesis: (i |^ n) div i = (i |^ n) / i n >= 0 + 1 by A1, NAT_1:13; then i |^ n = 0 by A3, NEWTON:11; hence (i |^ n) div i = (i |^ n) / i by A3, NAT_D:def_1; ::_thesis: verum end; end; end; theorem Th65: :: PEPIN:65 for r being real number for n being Nat st 0 < n & 1 < r holds 1 < r |^ n proof let r be real number ; ::_thesis: for n being Nat st 0 < n & 1 < r holds 1 < r |^ n let n be Nat; ::_thesis: ( 0 < n & 1 < r implies 1 < r |^ n ) assume that A1: 0 < n and A2: r > 1 ; ::_thesis: 1 < r |^ n defpred S1[ Nat] means ( 0 < $1 implies 1 < r |^ $1 ); A3: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume that A4: S1[k] and 0 < k + 1 ; ::_thesis: 1 < r |^ (k + 1) percases ( k > 0 or k = 0 ) ; suppose k > 0 ; ::_thesis: 1 < r |^ (k + 1) then ( r |^ (k + 1) = (r |^ k) * r & 1 * r <= (r |^ k) * r ) by A2, A4, NEWTON:6, XREAL_1:64; hence 1 < r |^ (k + 1) by A2, XXREAL_0:2; ::_thesis: verum end; suppose k = 0 ; ::_thesis: 1 < r |^ (k + 1) hence 1 < r |^ (k + 1) by A2, NEWTON:5; ::_thesis: verum end; end; end; A5: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A5, A3); hence 1 < r |^ n by A1; ::_thesis: verum end; theorem :: PEPIN:66 for r being real number for m, n being Nat st r > 1 & m > n holds r |^ m > r |^ n proof let r be real number ; ::_thesis: for m, n being Nat st r > 1 & m > n holds r |^ m > r |^ n let m, n be Nat; ::_thesis: ( r > 1 & m > n implies r |^ m > r |^ n ) assume that A1: r > 1 and A2: m > n ; ::_thesis: r |^ m > r |^ n reconsider m = m, n = n as Element of NAT by ORDINAL1:def_12; (m -' n) + n = m by A2, XREAL_1:235; then A3: r |^ m = (r |^ (m -' n)) * (r |^ n) by NEWTON:8; m -' n <> 0 by A2, NAT_D:36; then r |^ (m -' n) > 1 by A1, Th65; hence r |^ m > r |^ n by A1, A3, NEWTON:83, XREAL_1:155; ::_thesis: verum end;