pepin.miz



    begin

    reserve d,i,j,k,m,n,p,q,x,k1,k2 for Nat,

a,c,i1,i2,i3,i5 for Integer;

    

     Lm1: for n,x,y be Nat holds n > 1 & x >= 1 & 1 = ((((x * y) * n) + x) + y) implies x = 1 & y = 0

    proof

      let n,x,y be Nat;

      assume that

       A1: n > 1 and

       A2: x >= 1 and

       A3: 1 = ((((x * y) * n) + x) + y);

      now

        per cases by A2, XXREAL_0: 1;

          suppose

           A4: x > 1;

          now

            per cases ;

              suppose

               A5: 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 thesis by A3, A6, XREAL_1: 6;

            end;

              suppose y = 0 ;

              hence thesis by A3;

            end;

          end;

          hence thesis;

        end;

          suppose

           A7: x = 1;

          now

            per cases ;

              suppose

               A8: 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 thesis by A3, A9, XREAL_1: 6;

            end;

              suppose y = 0 ;

              hence thesis by A7;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    

     Lm2: (2 |^ (2 |^ n)) > 1

    proof

      defpred P[ Nat] means (2 |^ (2 |^ $1)) > 1;

      

       A1: for k holds P[k] implies P[(k + 1)]

      proof

        let k;

        assume

         A2: (2 |^ (2 |^ 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 thesis by NEWTON: 9;

      end;

      (2 |^ 0 ) = 1 by NEWTON: 4;

      then (2 |^ (2 |^ 0 )) = 2;

      then

       A3: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    

     Lm3: n <> 0 implies (n - 1) >= 0

    proof

      assume n <> 0 ;

      then n >= 1 by NAT_1: 14;

      then (n - 1) >= (1 - 1) by XREAL_1: 9;

      hence thesis;

    end;

    

     Lm4: n <> 0 implies ((n -' 1) + 1) = ((n + 1) -' 1)

    proof

      assume n <> 0 ;

      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 thesis by XREAL_0:def 2;

    end;

    theorem :: PEPIN:1

    for i be Nat holds (i,(i + 1)) are_coprime

    proof

      let k be Nat;

      (k gcd (k + 1)) = ((1 + (k * 1)) gcd k)

      .= (1 gcd k) by EULER_1: 8

      .= 1 by NEWTON: 51;

      hence thesis by INT_2:def 3;

    end;

    theorem :: PEPIN:2

    

     Th2: for p be Nat holds p is prime implies (m,p) are_coprime or (m gcd p) = p

    proof

      let p be Nat;

      

       A1: (m gcd p) divides p by NAT_D:def 5;

      assume p is prime;

      then (m gcd p) = 1 or (m gcd p) = p by A1, INT_2:def 4;

      hence thesis by INT_2:def 3;

    end;

    theorem :: PEPIN:3

    

     Th3: for k,m,n be Nat holds k divides (n * m) & (n,k) are_coprime implies k divides m

    proof

      let k,m,n be Nat;

      assume that

       A1: k divides (n * m) and

       A2: (n,k) are_coprime ;

      reconsider k, m, 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);

      hence thesis by A1, A3, NEWTON: 50;

    end;

    theorem :: PEPIN:4

    

     Th4: n divides m & k divides m & (n,k) are_coprime implies (n * k) divides m

    proof

      assume that

       A1: n divides m and

       A2: k divides m & (n,k) are_coprime ;

      consider t1 be Nat such that

       A3: m = (n * t1) by A1, NAT_D:def 3;

      k divides t1 by A2, A3, Th3;

      then

      consider t2 be Nat such that

       A4: t1 = (k * t2) by NAT_D:def 3;

      m = ((n * k) * t2) by A3, A4;

      hence thesis;

    end;

    registration

      let i be Integer;

      cluster (i ^2 ) -> natural;

      coherence

      proof

        (i ^2 ) in NAT by INT_1: 3, XREAL_1: 63;

        hence thesis;

      end;

    end

    theorem :: PEPIN:5

    c > 1 implies (1 mod c) = 1

    proof

      assume

       A1: 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 thesis;

    end;

    theorem :: PEPIN:6

    

     Th6: for i,n be Nat st i <> 0 holds i divides n iff (n mod i) = 0

    proof

      let i,n be Nat;

      assume

       A1: i <> 0 ;

      

       A2: (n mod i) = 0 implies i divides n

      proof

        assume (n mod i) = 0 ;

        then ex t be Nat st n = ((i * t) + 0 ) & 0 < i by A1, NAT_D:def 2;

        hence thesis;

      end;

      i divides n implies (n mod i) = 0

      proof

        assume i divides n;

        then ex t be Nat st n = (i * t) by NAT_D:def 3;

        hence thesis by NAT_D: 13;

      end;

      hence thesis by A2;

    end;

    theorem :: PEPIN:7

    

     Th7: for m,n be Nat holds m <> 0 & m divides (n mod m) implies m divides n

    proof

      let m,n be Nat;

      assume that

       A1: m <> 0 and

       A2: m divides (n mod m);

      consider x be 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 thesis;

    end;

    theorem :: PEPIN:8

    for m,n,k be Nat holds 0 < n & (m mod n) = k implies n divides (m - k)

    proof

      let m,n,k be Nat;

      assume

       A1: 0 < n & (m mod n) = k;

      take (m div n);

      m = ((n * (m div n)) + k) by A1, NAT_D: 2;

      hence thesis;

    end;

    theorem :: PEPIN:9

    (i * p) <> 0 & (k mod (i * p)) < p implies (k mod (i * p)) = (k mod p)

    proof

      assume that

       A1: (i * p) <> 0 and

       A2: (k mod (i * p)) < p;

      set T = (k mod (i * p));

      consider n be Nat such that

       A3: k = (((i * p) * n) + T) and T < (i * p) by A1, NAT_D:def 2;

      k = ((p * (i * n)) + T) by A3;

      

      then (k mod p) = (T mod p) by NAT_D: 21

      .= T by A2, NAT_D: 24;

      hence thesis;

    end;

    theorem :: PEPIN:10

    

     Th10: (((a * p) + 1) mod p) = (1 mod p)

    proof

      per cases ;

        suppose

         A1: p <> 0 ;

        reconsider 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 thesis by A1, INT_1:def 10;

      end;

        suppose p = 0 ;

        hence thesis;

      end;

    end;

    theorem :: PEPIN:11

    

     Th11: 1 < m & ((n * k) mod m) = (k mod m) & (k,m) are_coprime implies (n mod m) = 1

    proof

      assume that

       A1: 1 < m and

       A2: ((n * k) mod m) = (k mod m) and

       A3: (k,m) are_coprime ;

      consider t2 be Nat such that

       A4: k = ((m * t2) + (k mod m)) and (k mod m) < m by A1, NAT_D:def 2;

      consider t1 be 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));

      reconsider n, m as Integer;

      m divides (n - 1) by A3, A6, INT_2: 25;

      then

      consider tt be Integer such that

       A7: (n - 1) = (m * tt);

      n = ((m * tt) + 1) by A7;

      

      then (n mod m) = (1 qua Integer mod m) by EULER_1: 12

      .= 1 by A1, NAT_D: 14;

      hence thesis;

    end;

    theorem :: PEPIN:12

    

     Th12: ((p |^ k) mod m) = (((p mod m) |^ k) mod m)

    proof

      defpred P[ Nat] means ((p |^ $1) mod m) = (((p mod m) |^ $1) mod m);

      

       A1: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A2: P[n];

        ((p |^ (n + 1)) mod m) = (((p |^ n) * (p |^ 1)) mod m) by NEWTON: 8

        .= ((((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 thesis;

      end;

      ((p |^ 0 ) mod m) = (1 mod m) by NEWTON: 4;

      then

       A3: P[ 0 ] by NEWTON: 4;

      for n holds P[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    

     Lm5: ((k * (2 |^ (n + 1))) div 2) = (k * (2 |^ n))

    proof

      (k * (2 |^ (n + 1))) = (k * ((2 |^ n) * 2)) by NEWTON: 6

      .= ((k * (2 |^ n)) * 2);

      hence thesis by NAT_D: 18;

    end;

    

     Lm6: k <= n implies (m |^ k) divides (m |^ n)

    proof

      assume k <= n;

      then

      consider t be Nat such that

       A1: n = (k + t) by NAT_1: 10;

      (m |^ n) = ((m |^ k) * (m |^ t)) by A1, NEWTON: 8;

      hence thesis;

    end;

    

     Lm7: (2 |^ 8) = 256

    proof

      (2 |^ 8) = (2 |^ (4 + 4))

      .= (16 * 16) by NEWTON: 8, POWER: 62;

      hence thesis;

    end;

    theorem :: PEPIN:13

    i <> 0 implies ((i ^2 ) mod (i + 1)) = 1

    proof

      assume

       A1: i <> 0 ;

      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 thesis;

    end;

    theorem :: PEPIN:14

    (k ^2 ) < j & (i mod j) = k implies ((i ^2 ) mod j) = (k ^2 )

    proof

      assume that

       A1: (k ^2 ) < j and

       A2: (i mod j) = k;

      consider n be 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 thesis by A1, NAT_D: 24;

    end;

    theorem :: PEPIN:15

    p is prime & (i mod p) = ( - 1) implies ((i ^2 ) mod p) = 1

    proof

      assume that

       A1: p is prime and

       A2: (i 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 thesis;

    end;

    theorem :: PEPIN:16

    n is even implies (n + 1) is odd;

    theorem :: PEPIN:17

    for p be Nat holds p > 2 & p is prime implies p is odd

    proof

      let p be Nat;

      assume

       A1: p > 2 & p is prime;

      assume p is even;

      then (p mod 2) = 0 by NAT_2: 21;

      then ex k be Nat st p = ((2 * k) + 0 ) & 0 < 2 by NAT_D:def 2;

      then 2 divides p;

      hence contradiction by A1, INT_2:def 4;

    end;

    theorem :: PEPIN:18

    n > 0 implies (2 to_power n) is even

    proof

      assume n > 0 ;

      then ((2 to_power n) mod 2) = 0 by NAT_2: 17;

      hence thesis by NAT_2: 21;

    end;

    theorem :: PEPIN:19

    i is odd & j is odd implies (i * j) is odd;

    theorem :: PEPIN:20

    i is odd implies (i |^ k) is odd

    proof

      defpred P[ Nat] means (i |^ $1) is odd;

      assume

       A1: i is odd;

      

       A2: for n holds P[n] implies P[(n + 1)]

      proof

        let n;

        

         A3: (i |^ (n + 1)) = ((i |^ n) * i) by NEWTON: 6;

        assume (i |^ n) is odd;

        hence thesis by A1, A3;

      end;

      (i |^ 0 ) = 1 & (1 mod 2) = 1 by NAT_D: 24, NEWTON: 4;

      then

       A4: P[ 0 ] by NAT_2: 22;

      for n holds P[n] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: PEPIN:21

    

     Th21: k > 0 & i is even implies (i |^ k) is even

    proof

      assume that

       A1: k > 0 and

       A2: i is even;

      defpred P[ Nat] means $1 > 0 & i is even implies (i |^ $1) is even;

      

       A3: for n holds P[n] implies P[(n + 1)]

      proof

        let n;

        assume P[n];

         P[(n + 1)]

        proof

          now

            ((i |^ n) * i) is even by A2;

            hence thesis by NEWTON: 6;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      

       A4: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A4, A3);

      hence thesis by A1, A2;

    end;

    theorem :: PEPIN:22

    2 divides n iff n is even

    proof

      

       A1: n is even implies 2 divides n

      proof

        assume n is even;

        then (n mod 2) = 0 by NAT_2: 21;

        then ex k be Nat st n = ((2 * k) + 0 ) & 0 < 2 by NAT_D:def 2;

        hence thesis;

      end;

      thus thesis by A1;

    end;

    theorem :: PEPIN:23

    (m * n) is even implies m is even or n is even;

    theorem :: PEPIN:24

    

     Th24: (n |^ 2) = (n ^2 )

    proof

      (n |^ 2) = (n |^ (1 + 1))

      .= ((n |^ 1) * (n |^ 1)) by NEWTON: 8

      .= (n ^2 );

      hence thesis;

    end;

    theorem :: PEPIN:25

    

     Th25: m > 1 & n > 0 implies (m |^ n) > 1

    proof

      assume that

       A1: m > 1 and

       A2: n > 0 ;

      defpred P[ Nat] means $1 > 0 implies (m |^ $1) > 1;

      

       A3: for n holds P[n] implies P[(n + 1)]

      proof

        let n;

        

         A4: (m |^ (n + 1)) = ((m |^ n) * (m |^ 1)) by NEWTON: 8

        .= ((m |^ n) * m);

        assume

         A5: P[n];

         P[(n + 1)]

        proof

          now

            per cases ;

              suppose n = 0 ;

              hence thesis by A1;

            end;

              suppose n <> 0 ;

              then ((m |^ n) * m) > (1 * m) by A1, A5, XREAL_1: 68;

              hence thesis by A1, A4, XXREAL_0: 2;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      

       A6: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A6, A3);

      hence thesis by A2;

    end;

    

     Lm8: ((2 |^ (2 |^ n)) ^2 ) = (2 |^ (2 |^ (n + 1)))

    proof

      defpred P[ Nat] means ((2 |^ (2 |^ $1)) ^2 ) = (2 |^ (2 |^ ($1 + 1)));

      

       A1: (2 |^ (2 |^ ( 0 + 1))) = (2 to_power 2)

      .= (2 ^2 ) by POWER: 46;

      

       A2: for k st P[k] holds P[(k + 1)]

      proof

        let x;

        assume

         A3: ((2 |^ (2 |^ x)) ^2 ) = (2 |^ (2 |^ (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 thesis;

      end;

      (2 |^ 0 ) = 1 by NEWTON: 4;

      then

       A4: P[ 0 ] by A1;

      for k holds P[k] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: PEPIN:26

    

     Th26: n <> 0 & p <> 0 implies (n |^ p) = (n * (n |^ (p -' 1)))

    proof

      assume

       A1: n <> 0 & p <> 0 ;

      defpred P[ Nat] means n <> 0 & $1 <> 0 implies (n |^ $1) = (n * (n |^ ($1 -' 1)));

      

       A2: for m holds P[m] implies P[(m + 1)]

      proof

        let m;

        assume P[m];

        now

          per cases ;

            suppose

             A3: m = 0 ;

            (n * (n |^ (( 0 + 1) -' 1))) = (n * (n |^ 0 )) by XREAL_1: 232

            .= (n * 1) by NEWTON: 4;

            hence thesis by A3;

          end;

            suppose

             A4: m <> 0 ;

            (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 thesis;

          end;

        end;

        hence thesis;

      end;

      

       A5: P[ 0 ];

      for m holds P[m] from NAT_1:sch 2( A5, A2);

      hence thesis by A1;

    end;

    theorem :: PEPIN:27

    

     Th27: for n, m st (m mod 2) = 0 holds ((n |^ (m div 2)) ^2 ) = (n |^ m)

    proof

      let n, m;

      assume

       A1: (m mod 2) = 0 ;

      ((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 thesis;

    end;

    theorem :: PEPIN:28

    

     Th28: n <> 0 & 1 <= k implies ((n |^ k) div n) = (n |^ (k -' 1))

    proof

      assume that

       A1: n <> 0 and

       A2: 1 <= k;

      

       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 thesis by A1, NAT_D: 18;

    end;

    theorem :: PEPIN:29

    (2 |^ (n + 1)) = ((2 |^ n) + (2 |^ n))

    proof

      defpred P[ Nat] means (2 |^ ($1 + 1)) = ((2 |^ $1) + (2 |^ $1));

      

       A1: for m st P[m] holds P[(m + 1)]

      proof

        let m;

        assume

         A2: (2 |^ (m + 1)) = ((2 |^ m) + (2 |^ m));

        ((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 thesis;

      end;

      (2 |^ ( 0 + 1)) = (1 + 1)

      .= ((2 |^ 0 ) + 1) by NEWTON: 4

      .= ((2 |^ 0 ) + (2 |^ 0 )) by NEWTON: 4;

      then

       A3: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: PEPIN:30

    

     Th30: k > 1 & (k |^ n) = (k |^ m) implies n = m

    proof

      assume that

       A1: k > 1 and

       A2: (k |^ n) = (k |^ m);

      now

        per cases ;

          suppose n = m;

          hence thesis;

        end;

          suppose n <> m;

          then (k to_power m) <> (k to_power n) by A1, POWER: 50;

          hence thesis by A2;

        end;

      end;

      hence thesis;

    end;

    

     Lm9: k > n & x > 1 implies (x |^ k) > (x |^ n)

    proof

      assume that

       A1: k > n and

       A2: x > 1;

      consider m be 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;

      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 thesis by A6, A5, XREAL_1: 155;

    end;

    

     Lm10: (2 |^ m) divides (2 |^ n) implies m <= n

    proof

       not m <= n implies not (2 |^ m) divides (2 |^ n)

      proof

        assume

         A1: not m <= 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);

          hence contradiction by A2, NAT_D: 3;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: PEPIN:31

    m <= n iff (2 |^ m) divides (2 |^ n) by Lm6, Lm10;

    theorem :: PEPIN:32

    

     Th32: p is prime & i divides (p |^ n) implies i = 1 or ex k be Element of NAT st i = (p * k)

    proof

      defpred P[ Nat] means i divides (p |^ $1) implies i = 1 or (ex k be Element of NAT st i = (p * k));

      assume

       A1: p is prime;

      then

       A2: p <> 0 by INT_2:def 4;

      

       A3: for n holds P[n] implies P[(n + 1)]

      proof

        let n;

        assume

         A4: P[n];

        now

          assume i divides (p |^ (n + 1));

          then

          consider u1 be 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);

          now

            per cases by A1, A6, NEWTON: 80;

              suppose p divides i;

              then

              consider w1 be Nat such that

               A7: i = (p * w1) by NAT_D:def 3;

              w1 in NAT by ORDINAL1:def 12;

              hence thesis by A7;

            end;

              suppose p divides u1;

              then

              consider w2 be 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 thesis by A4, NAT_D:def 3;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      

       A9: P[ 0 ]

      proof

        now

          assume i divides (p |^ 0 );

          then i divides 1 by NEWTON: 4;

          then ex t be Nat st 1 = (i * t) by NAT_D:def 3;

          hence thesis by NAT_1: 15;

        end;

        hence thesis;

      end;

      for n holds P[n] from NAT_1:sch 2( A9, A3);

      hence thesis;

    end;

    theorem :: PEPIN:33

    

     Th33: for n st p is prime & n < (p |^ (k + 1)) holds n divides (p |^ (k + 1)) iff n divides (p |^ k)

    proof

      let n;

      assume that

       A1: p is prime and

       A2: n < (p |^ (k + 1));

      

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

        now

          per cases by A1, A5, Th32;

            suppose n = 1;

            hence thesis by NAT_D: 6;

          end;

            suppose ex i be Element of NAT st n = (p * i);

            then

            consider i be Element of NAT such that

             A6: n = (p * i);

            consider u be 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);

            u <> 1 by A2, A6, A9, NEWTON: 6;

            then

            consider j be 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 thesis;

          end;

        end;

        hence thesis;

      end;

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

      proof

        assume n divides (p |^ k);

        then n divides ((p |^ k) * p) by NAT_D: 9;

        hence thesis by NEWTON: 6;

      end;

      hence thesis by A4;

    end;

    theorem :: PEPIN:34

    

     Th34: for k holds p is prime & d divides (p |^ k) implies ex t be Element of NAT st d = (p |^ t) & t <= k

    proof

      let n;

      assume that

       A1: p is prime and

       A2: d divides (p |^ n);

      defpred P[ Nat] means d divides (p |^ $1) implies ex t be Element of NAT st d = (p |^ t) & t <= $1;

      

       A3: p > 0 by A1, INT_2:def 4;

      

       A4: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A5: P[n];

        now

          assume

           A6: d divides (p |^ (n + 1));

          (p |^ (n + 1)) > 0 by A3, PREPOWER: 6;

          then

           A7: d <= (p |^ (n + 1)) by A6, NAT_D: 7;

          now

            per cases by A7, XXREAL_0: 1;

              suppose d < (p |^ (n + 1));

              then ex t be Element of NAT st d = (p |^ t) & t <= n by A1, A5, A6, Th33;

              hence thesis by NAT_1: 12;

            end;

              suppose d = (p |^ (n + 1));

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      

       A8: P[ 0 ]

      proof

        assume

         A9: d divides (p |^ 0 );

        d = (p |^ 0 )

        proof

          ex t be Nat st (p |^ 0 ) = (d * t) by A9, NAT_D:def 3;

          then d = 1 by NAT_1: 15, NEWTON: 4;

          hence thesis by NEWTON: 4;

        end;

        hence thesis;

      end;

      for n holds P[n] from NAT_1:sch 2( A8, A4);

      hence thesis by A2;

    end;

    theorem :: PEPIN:35

    

     Th35: p > 1 & (i mod p) = 1 implies ((i |^ n) mod p) = 1

    proof

      assume that

       A1: p > 1 and

       A2: (i mod p) = 1;

      defpred P[ Nat] means ((i |^ $1) mod p) = 1;

      

       A3: for k holds P[k] implies P[(k + 1)]

      proof

        let k;

        assume

         A4: ((i |^ k) mod p) = 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 thesis;

      end;

      (1 mod p) = 1 by A1, NAT_D: 24;

      then

       A5: P[ 0 ] by NEWTON: 4;

      for n holds P[n] from NAT_1:sch 2( A5, A3);

      hence thesis;

    end;

    theorem :: PEPIN:36

    

     Th36: for m,n be Nat holds m > 0 implies ((n |^ m) mod n) = 0

    proof

      let m,n be Nat;

      assume

       A1: m > 0 ;

      defpred P[ Nat] means $1 > 0 implies ((n |^ $1) mod n) = 0 ;

      

       A2: for m be Nat holds P[m] implies P[(m + 1)]

      proof

        let m be Nat;

        assume P[m];

         P[(m + 1)]

        proof

          reconsider m, 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 thesis by NEWTON: 6;

        end;

        hence thesis;

      end;

      

       A3: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A3, A2);

      hence thesis by A1;

    end;

    theorem :: PEPIN:37

    

     Th37: for p be Nat holds p is prime & (n,p) are_coprime implies ((n |^ (p -' 1)) mod p) = 1

    proof

      let p be Nat;

      assume that

       A1: p is prime and

       A2: (n,p) are_coprime ;

      

       A3: p <> 0 by A1, INT_2:def 4;

      

       A4: n <> 0

      proof

        assume n = 0 ;

        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;

      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 thesis by A2, A6, A5, EULER_2: 12;

    end;

    theorem :: PEPIN:38

    

     Th38: p is prime & d > 1 & d divides (p |^ k) & not d divides ((p |^ k) div p) implies d = (p |^ k)

    proof

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

      

       A5: k <> 0

      proof

        assume k = 0 ;

        then (p |^ k) = 1 by NEWTON: 4;

        hence contradiction by A2, A3, NAT_D: 7;

      end;

      then k >= 1 by NAT_1: 14;

      then

       A6: (k - 1) >= (1 - 1) by XREAL_1: 9;

      consider t be 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;

        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;

      end;

      hence thesis by A7, A8, XXREAL_0: 1;

    end;

    definition

      let i be Integer;

      :: original: ^2

      redefine

      func i ^2 -> Element of NAT ;

      coherence by ORDINAL1:def 12;

    end

    theorem :: PEPIN:39

    

     Th39: for n st n > 1 holds (m mod n) = 1 iff (m,1) are_congruent_mod n

    proof

      let n;

      assume

       A1: n > 1;

      

       A2: (m,1) are_congruent_mod n implies (m mod n) = 1

      proof

        assume (m,1) are_congruent_mod n;

        then

        consider t be Integer such that

         A3: (n * t) = (m - 1);

        reconsider m, n as Integer;

        (m mod n) = (((n * t) + 1) mod n) by A3

        .= (1 mod n) by EULER_1: 12;

        hence thesis by A1, NAT_D: 14;

      end;

      (m mod n) = 1 implies (m,1) are_congruent_mod n

      proof

        assume (m mod n) = 1;

        then

        consider k be Nat such that

         A4: m = ((n * k) + 1) and 1 < n by NAT_D:def 2;

        (n * k) = (m - 1) by A4;

        hence thesis;

      end;

      hence thesis by A2;

    end;

    

     Lm11: n > 1 & m > 1 & (m,1) are_congruent_mod n implies (m mod n) = 1

    proof

      assume that

       A1: n > 1 and

       A2: m > 1 and

       A3: (m,1) are_congruent_mod n;

      consider d be Integer such that

       A4: (n * d) = (m - 1) by A3;

      (m - 1) > (1 - 1) by A2, XREAL_1: 9;

      then d > 0 by A4;

      then

      reconsider 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 thesis;

    end;

    theorem :: PEPIN:40

    

     Th40: (i1,i2) are_congruent_mod i5 & (i1,i3) are_congruent_mod i5 implies (i2,i3) are_congruent_mod i5

    proof

      assume that

       A1: (i1,i2) are_congruent_mod i5 and

       A2: (i1,i3) are_congruent_mod i5;

      (i2,i1) are_congruent_mod i5 by A1, INT_1: 14;

      then

      consider t1 be Integer such that

       A3: (i5 * t1) = (i2 - i1);

      (i3,i1) are_congruent_mod i5 by A2, INT_1: 14;

      then

      consider t2 be Integer such that

       A4: (i5 * t2) = (i3 - i1);

      (i2 - i3) = (i5 * (t1 - t2)) by A3, A4;

      hence thesis;

    end;

    theorem :: PEPIN:41

    

     Th41: 3 is prime

    proof

      for n be Nat holds n divides 3 implies n = 1 or n = 3

      proof

        let n be Nat;

        assume

         A1: n divides 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;

          hence contradiction by A1, A3, Th6;

        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;

        hence thesis by A4, A2, NAT_1: 14;

      end;

      hence thesis by INT_2:def 4;

    end;

    theorem :: PEPIN:42

    

     Th42: n <> 0 implies ( Euler n) <> 0

    proof

      assume

       A1: n <> 0 ;

      set X = { k where k be Element of NAT : (n,k) are_coprime & k >= 1 & k <= n };

      

       A2: X c= ( finSeg n)

      proof

        let x be object;

        assume x in X;

        then ex xx be Element of NAT st x = xx & (n,xx) are_coprime & xx >= 1 & xx <= n;

        hence thesis by FINSEQ_1: 1;

      end;

      assume ( Euler n) = 0 ;

      then

       A3: ( card X) = 0 by EULER_1:def 1;

      reconsider X as finite set by A2;

      ex k st k in X

      proof

        take 1;

        (n gcd 1) = 1 by NEWTON: 51;

        then

         A4: (n,1) are_coprime by INT_2:def 3;

        1 <= n by A1, NAT_1: 14;

        hence thesis by A4;

      end;

      hence contradiction by A3;

    end;

    theorem :: PEPIN:43

    n <> 0 implies ( - n) < n;

    theorem :: PEPIN:44

    

     Th44: n <> 0 implies (n div n) = 1

    proof

      assume n <> 0 ;

      then ((n * 1) div n) = 1 by NAT_D: 18;

      hence thesis;

    end;

    begin

    definition

      let k, m, n;

      :: PEPIN:def1

      func Crypto (m,n,k) -> Element of NAT equals ((m |^ k) mod n);

      coherence ;

    end

    theorem :: PEPIN:45

    p is prime & q is prime & p <> q & n = (p * q) & (k1,( Euler n)) are_coprime & ((k1 * k2) mod ( Euler n)) = 1 implies for m be Element of NAT st m < n holds ( Crypto (( Crypto (m,n,k1)),n,k2)) = m

    proof

      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_coprime and

       A6: ((k1 * k2) mod ( Euler n)) = 1;

      

       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 & q1 = 1) by A3;

      then

       A13: (p1 * q1) <> 1 by NAT_1: 15;

      

       A14: k1 <> 0

      proof

        assume k1 = 0 ;

        then (k1 gcd ( Euler n)) = ( Euler n) by NEWTON: 52;

        hence contradiction by A5, A9, A13, INT_2:def 3;

      end;

      

       A15: k2 <> 0 by A6, NAT_D: 26;

      

       A16: q > 0 by A2, INT_2:def 4;

      let m be Element of NAT ;

      assume

       A17: m < n;

      

       A18: p > 0 by A1, INT_2:def 4;

      now

        per cases ;

          suppose

           A19: m = 0 ;

          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 thesis by A19, NAT_D: 26;

        end;

          suppose

           A20: m = 1;

          then (m |^ k1) = 1;

          then ((m |^ k1) mod n) = 1 by A10, NAT_D: 14;

          then (( Crypto (m,n,k1)) |^ k2) = 1;

          hence thesis by A10, A20, NAT_D: 14;

        end;

          suppose

           A21: m <> 0 & m <> 1;

          

           A22: for t be Element of NAT holds ((m |^ (((t * p1) * q1) + 1)) mod n) = m

          proof

            let t be Element of NAT ;

            now

              (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

                  per cases ;

                    suppose (m gcd p) = 1;

                    then

                     A24: (m,p) are_coprime 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;

                    hence thesis by NAT_D: 9;

                  end;

                    suppose (m gcd p) <> 1;

                    then not (m,p) are_coprime by INT_2:def 3;

                    then (m gcd p) = p by A1, Th2;

                    then p divides m by NAT_D:def 5;

                    hence thesis by NAT_D: 9;

                  end;

                end;

                hence thesis;

              end;

              q divides (m * a)

              proof

                now

                  per cases ;

                    suppose (m gcd q) = 1;

                    then

                     A25: (m,q) are_coprime 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;

                    hence thesis by NAT_D: 9;

                  end;

                    suppose (m gcd q) <> 1;

                    then not (m,q) are_coprime by INT_2:def 3;

                    then (m gcd q) = q by A2, Th2;

                    then q divides m by NAT_D:def 5;

                    hence thesis by NAT_D: 9;

                  end;

                end;

                hence thesis;

              end;

              then (p * q) divides (m * a) by A1, A2, A3, A23, Th4, INT_2: 30;

              then

              consider k be 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 thesis by A17, NAT_D:def 2;

            end;

            hence thesis;

          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 thesis by Th12;

        end;

      end;

      hence thesis;

    end;

    begin

    definition

      let i, p;

      assume that

       A1: p > 1 and

       A2: (i,p) are_coprime ;

      :: PEPIN:def2

      func order (i,p) -> Element of NAT means

      : Def2: it > 0 & ((i |^ it ) mod p) = 1 & for k st k > 0 & ((i |^ k) mod p) = 1 holds 0 < it & it <= k;

      existence

      proof

        set A = { k where k be Element of NAT : k > 0 & ((i |^ k) mod p) = 1 };

        

         A3: A c= NAT

        proof

          let a be object;

          assume a in A;

          then ex k be Element of NAT st k = a & k > 0 & ((i |^ k) mod p) = 1;

          hence thesis;

        end;

        i <> 0

        proof

          assume i = 0 ;

          then (i gcd p) = p by NEWTON: 52;

          hence contradiction by A1, A2, INT_2:def 3;

        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 A by A4;

        then

        reconsider A as non empty Subset of NAT by A3;

        set a = the Element of A;

        defpred P[ set] means $1 in A;

        a is Element of NAT ;

        then

         A5: ex kk be Nat st P[kk];

        consider kk be Nat such that

         A6: P[kk] and

         A7: for n be Nat st P[n] holds kk <= n from NAT_1:sch 5( A5);

        take kk;

        

         A8: for k st k > 0 & ((i |^ k) mod p) = 1 holds kk <= k

        proof

          let k;

          assume

           A9: k > 0 & ((i |^ k) mod p) = 1;

          k in NAT by ORDINAL1:def 12;

          then k in A by A9;

          hence thesis by A7;

        end;

        ex k be Element of NAT st k = kk & k > 0 & ((i |^ k) mod p) = 1 by A6;

        hence thesis by A8;

      end;

      uniqueness

      proof

        let k1,k2 be Element of NAT ;

        assume k1 > 0 & ((i |^ k1) mod p) = 1 & (for k st k > 0 & ((i |^ k) mod p) = 1 holds 0 < k1 & k1 <= k) & k2 > 0 & (((i |^ k2) mod p) = 1 & for k st k > 0 & ((i |^ k) mod p) = 1 holds 0 < k2 & k2 <= k);

        then k1 <= k2 & k2 <= k1;

        hence thesis by XXREAL_0: 1;

      end;

    end

    theorem :: PEPIN:46

    p > 1 implies ( order (1,p)) = 1

    proof

      assume

       A1: p > 1;

      (p gcd 1) = 1 by NEWTON: 51;

      then

       A2: (1,p) are_coprime by INT_2:def 3;

      ((1 |^ 1) mod p) = 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;

      hence contradiction by A1, A2, A3, Def2;

    end;

    theorem :: PEPIN:47

    

     Th47: p > 1 & ((i |^ n) mod p) = 1 & (i,p) are_coprime implies ( order (i,p)) divides n

    proof

      assume that

       A1: p > 1 and

       A2: ((i |^ n) mod p) = 1 and

       A3: (i,p) are_coprime ;

      

       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 be Nat such that

         A6: n = ((( order (i,p)) * t) + I) and

         A7: I < ( order (i,p)) by A4, NAT_D:def 2;

        reconsider t as Element of NAT by ORDINAL1:def 12;

        (((i |^ (( order (i,p)) * t)) * (i |^ I)) mod p) = 1 by A2, A6, NEWTON: 8;

        then ((((i |^ ( order (i,p))) |^ t) * (i |^ I)) mod p) = 1 by NEWTON: 9;

        then (((((i |^ ( order (i,p))) |^ t) mod p) * (i |^ I)) mod p) = 1 by EULER_2: 8;

        then

         A8: ((1 * (i |^ I)) mod p) = 1 by A1, A5, Th35;

        assume (n mod ( order (i,p))) <> 0 ;

        hence contradiction by A1, A3, A7, A8, Def2;

      end;

      hence thesis by A4, Th6;

    end;

    theorem :: PEPIN:48

    

     Th48: p > 1 & (i,p) are_coprime & ( order (i,p)) divides n implies ((i |^ n) mod p) = 1

    proof

      assume that

       A1: p > 1 and

       A2: (i,p) are_coprime and

       A3: ( order (i,p)) divides n;

      consider t be Nat such that

       A4: n = (( order (i,p)) * t) by A3, NAT_D:def 3;

      reconsider 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 by A1, NAT_D: 24;

      hence thesis;

    end;

    theorem :: PEPIN:49

    

     Th49: p is prime & (i,p) are_coprime implies ( order (i,p)) divides (p -' 1)

    proof

      assume that

       A1: p is prime and

       A2: (i,p) are_coprime ;

      ((i |^ (p -' 1)) mod p) = 1 & p > 1 by A1, A2, Th37, INT_2:def 4;

      hence thesis by A2, Th47;

    end;

    begin

    definition

      let n be Nat;

      :: PEPIN:def3

      func Fermat (n) -> Element of NAT equals ((2 |^ (2 |^ n)) + 1);

      correctness ;

    end

    theorem :: PEPIN:50

    

     Th50: ( Fermat 0 ) = 3

    proof

      ( Fermat 0 ) = ((2 |^ 1) + 1) by NEWTON: 4

      .= (2 + 1);

      hence thesis;

    end;

    theorem :: PEPIN:51

    

     Th51: ( Fermat 1) = 5

    proof

      ( Fermat 1) = ((2 |^ (1 + 1)) + 1)

      .= (((2 |^ 1) * 2) + 1) by NEWTON: 6

      .= ((2 * 2) + 1);

      hence thesis;

    end;

    theorem :: PEPIN:52

    

     Th52: ( Fermat 2) = 17

    proof

      

      thus ( Fermat 2) = ((2 |^ (2 |^ (1 + 1))) + 1)

      .= ((2 |^ ((2 |^ 1) * 2)) + 1) by NEWTON: 6

      .= ((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

      .= 17;

    end;

    theorem :: PEPIN:53

    

     Th53: ( 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;

    end;

    theorem :: PEPIN:54

    

     Th54: ( 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;

    end;

    theorem :: PEPIN:55

    

     Th55: ( Fermat n) > 2

    proof

      set 2N = (2 |^ (2 |^ n));

      2N > 1 by Lm2;

      then (2N + 1) > (1 + 1) by XREAL_1: 6;

      hence thesis;

    end;

    

     Lm12: ( Fermat n) > 1

    proof

      ( Fermat n) <> 1 by Th55;

      then ( Fermat n) > 1 or ( Fermat n) < 1 by XXREAL_0: 1;

      hence thesis by NAT_1: 14;

    end;

    

     Lm13: ((( Fermat n) -' 1) mod 2) = 0

    proof

      (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 thesis by NAT_2: 21;

    end;

    

     Lm14: (( Fermat n) -' 1) > 0

    proof

      ( Fermat n) > 1 by Lm12;

      then (( Fermat n) - 1) > (1 - 1) by XREAL_1: 9;

      hence thesis by XREAL_0:def 2;

    end;

    

     Lm15: (( Fermat n) mod (2 |^ (2 |^ n))) = 1

    proof

      set 2N = (2 |^ (2 |^ n));

      (( Fermat n) mod 2N) = (((2N * 1) + 1) mod 2N)

      .= (1 mod 2N) by NAT_D: 21

      .= 1 by Lm2, NAT_D: 14;

      hence thesis;

    end;

    

     Lm16: ( Fermat n) is odd

    proof

      (( Fermat n) - 1) = (( Fermat n) -' 1) & ((( Fermat n) -' 1) mod 2) = 0 by Lm13, XREAL_0:def 2;

      hence thesis by NAT_2: 21;

    end;

    theorem :: PEPIN:56

    

     Th56: p is prime & p > 2 & p divides ( Fermat n) implies ex k be Element of NAT st p = ((k * (2 |^ (n + 1))) + 1)

    proof

      assume that

       A1: p is prime and

       A2: p > 2 and

       A3: p divides ( Fermat n);

      

       A4: p > 1 by A1, INT_2:def 4;

      set t = (( Fermat n) div p);

      set 2N = (2 |^ (2 |^ n));

      

       A5: (((p * t) + ( - 1)),( 0 + ( - 1))) are_congruent_mod p;

      

       A6: (p * t) = (2N + 1) by A3, NAT_D: 3;

      

       A7: (2N mod p) <> 1

      proof

        assume (2N mod p) = 1;

        then (2N,1) are_congruent_mod p by A4, Th39;

        then (1,2N) 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));

        hence contradiction by A2, NAT_D: 7;

      end;

      

       A8: (2,p) are_coprime 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: 2N > 1 by Th25, PREPOWER: 6;

      then (2N * 2N) > (1 * 2N) by XREAL_1: 68;

      then

       A11: (2N ^2 ) > 1 by A10, XXREAL_0: 2;

      ((2N ^2 ),(( - 1) ^2 )) are_congruent_mod p by A6, A5, INT_1: 18;

      then ((2N ^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 be Nat such that

       A13: (p -' 1) = ((2 |^ (n + 1)) * t2) by NAT_D:def 3;

      reconsider 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 thesis;

    end;

    theorem :: PEPIN:57

    

     Th57: n <> 0 implies (3,( Fermat n)) are_coprime

    proof

      assume

       A1: n <> 0 ;

      (( Fermat n) gcd 3) <> 3

      proof

        assume (( Fermat n) gcd 3) = 3;

        then 3 divides ( Fermat n) by NAT_D:def 5;

        then

        consider k be 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;

      end;

      hence thesis by Th2, Th41;

    end;

    begin

    ::$Notion-Name

    theorem :: PEPIN:58

    

     Th58: ((3 |^ ((( Fermat n) -' 1) div 2)),( - 1)) are_congruent_mod ( Fermat n) implies ( Fermat n) is prime

    proof

      per cases ;

        suppose n = 0 ;

        hence thesis by Th41, Th50;

      end;

        suppose

         A1: n > 0 ;

        ( Fermat n) > 2 by Th55;

        then

        consider p be 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 be Nat such that

         A4: ( Fermat n) = (p * i) by A3, NAT_D:def 3;

        

         A5: p > 2

        proof

          assume p <= 2;

          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;

        end;

        

         A8: (( Fermat n) - 1) >= 0 ;

        assume

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

        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;

        reconsider 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;

          then not (3,( Fermat n)) are_coprime by A4, A15, INT_2:def 3;

          hence contradiction by A1, Th57;

        end;

        then d divides (p -' 1) by A2, Th41, Th49, INT_2: 30;

        then

        consider x be Nat such that

         A16: (p -' 1) = (d * 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 d divides ((( Fermat n) -' 1) div 2)

        proof

          assume d divides ((( Fermat n) -' 1) div 2);

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

          hence contradiction by A5, NAT_D: 7;

        end;

        then

         A19: not d divides (2N div 2) by A8, XREAL_0:def 2;

        

         A20: (3,p) are_coprime by A2, A14, Th41, INT_2: 30;

        then

         A21: d <> 0 by A13, Def2;

        

         A22: d > 1

        proof

          assume

           A23: d <= 1;

          now

            per cases by A23, XXREAL_0: 1;

              suppose d < 1;

              hence thesis by A21, NAT_1: 14;

            end;

              suppose d = 1;

              hence thesis by A18, NAT_D: 6;

            end;

          end;

          hence thesis;

        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 d divides (( Fermat n) -' 1) by A20, A13, Th47;

        then d divides 2N by A8, XREAL_0:def 2;

        

        then d = 2N by A19, A22, Th38, INT_2: 28

        .= (( Fermat n) -' 1) by A8, XREAL_0:def 2;

        then

         A24: d = 2N by A8, XREAL_0:def 2;

        

         A25: ((p * i) mod 2N) = 1 by A4, Lm15;

        (p - 1) > (1 - 1) by A13, XREAL_1: 9;

        then

         A26: (p - 1) = (x * d) by A16, XREAL_0:def 2;

        then

         A27: p = ((x * 2N) + 1) by A24;

        

        then (p mod 2N) = (1 mod 2N) by NAT_D: 21

        .= 1 by Lm2, NAT_D: 24;

        then ((1 * i) mod 2N) = 1 by A25, EULER_2: 8;

        then

        consider y be Nat such that

         A28: i = ((2N * y) + 1) and 1 < 2N by NAT_D:def 2;

        

         A29: 2N <> 0 by Lm2;

        

         A30: x >= 1

        proof

          assume x < 1;

          then p = (( 0 * 2N) + 1) by A27, NAT_1: 14;

          hence contradiction by A2, INT_2:def 4;

        end;

        reconsider y as Element of NAT by ORDINAL1:def 12;

        ( Fermat n) = (((x * 2N) + 1) * ((y * 2N) + 1)) by A4, A24, A26, A28

        .= ((2N * ((((x * y) * 2N) + x) + y)) + 1);

        

        then

         A31: 1 = ((2N * ((((x * y) * 2N) + x) + y)) div 2N) by A29, Th44

        .= ((((x * y) * 2N) + x) + y) by A29, NAT_D: 18;

        2N > 1 by Lm2;

        

        then p = ((1 * 2N) + 1) by A27, A30, A31, Lm1

        .= ( Fermat n);

        hence contradiction by A12, A2;

      end;

    end;

    

     Lm17: (3 |^ 2) = 9

    proof

      (3 |^ 2) = (3 |^ (1 + 1))

      .= ((3 |^ 1) * (3 |^ 1)) by NEWTON: 8

      .= (3 * 3);

      hence thesis;

    end;

    

     Lm18: (3 |^ 4) = 81

    proof

      (3 |^ 4) = (3 |^ (2 + 2))

      .= ((3 |^ 2) * (3 |^ 2)) by NEWTON: 8;

      hence thesis by Lm17;

    end;

    

     Lm19: (3 |^ 8) = 6561

    proof

      (3 |^ 8) = (3 |^ (4 + 4))

      .= ((3 |^ 4) * (3 |^ 4)) by NEWTON: 8;

      hence thesis by Lm18;

    end;

    

     Lm20: (3 |^ 16) = (6561 * 6561)

    proof

      (3 |^ 16) = (3 |^ (8 + 8))

      .= ((3 |^ 8) * (3 |^ 8)) by NEWTON: 8;

      hence thesis by Lm19;

    end;

    

     Lm21: ( Fermat 1) divides ((3 |^ ((4 * i) + 2)) + 1)

    proof

      defpred P[ Nat] means ( Fermat 1) divides ((3 |^ ((4 * $1) + 2)) + 1);

      

       A1: for n holds P[n] implies P[(n + 1)]

      proof

        let n;

        assume ( Fermat 1) divides ((3 |^ ((4 * n) + 2)) + 1);

        then

        consider m be 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 thesis by NAT_D:def 3;

      end;

      ((3 |^ ((4 * 0 ) + 2)) + 1) = (5 * 2) by Lm17;

      then

       A4: P[ 0 ] by Th51, NAT_D:def 3;

      for n holds P[n] from NAT_1:sch 2( A4, A1);

      hence thesis;

    end;

    

     Lm22: (2 to_power 1) = 2;

    

     Lm23: n = 1 implies ((3 |^ ((( Fermat n) -' 1) div 2)),( - 1)) are_congruent_mod ( Fermat n)

    proof

      

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

      assume

       A4: n = 1;

      (4 div 2) = 2 by A1, A3, Lm22, NAT_2: 16;

      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 thesis by A4;

    end;

    

     Lm24: ( Fermat 2) divides ((3 |^ ((16 * n) + 8)) + 1)

    proof

      defpred P[ Nat] means ( Fermat 2) divides ((3 |^ ((16 * $1) + 8)) + 1);

      

       A1: for n holds P[n] implies P[(n + 1)]

      proof

        let n;

        assume ( Fermat 2) divides ((3 |^ ((16 * n) + 8)) + 1);

        then

        consider m be 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 thesis by NAT_D:def 3;

      end;

      ((3 |^ ((16 * 0 ) + 8)) + 1) = (17 * 386) by Lm19;

      then

       A4: P[ 0 ] by Th52, NAT_D:def 3;

      for n holds P[n] from NAT_1:sch 2( A4, A1);

      hence thesis;

    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

      .= 9 by A1, Th53, NAT_D:def 2;

    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;

    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;

    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;

    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 thesis;

    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;

    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;

    end;

    

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

      .= 9 by A1, Th54, NAT_D:def 2;

    end;

    

     Lm33: ((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 Lm32, EULER_2: 9

      .= 81 by A1, Th54, NAT_D:def 2;

    end;

    

     Lm34: ((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 Lm33, EULER_2: 9

      .= 6561 by A1, Th54, NAT_D:def 2;

    end;

    

     Lm35: ((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 Lm34, EULER_2: 9

      .= ((164 * 332) + 1) by A1, Th54, NAT_D:def 2;

      hence thesis;

    end;

    

     Lm36: ((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 Lm35, EULER_2: 9

      .= (123 * 503) by A1, Th54, NAT_D:def 2;

      hence thesis;

    end;

    

     Lm37: ((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 Lm36, EULER_2: 9

      .= ((14 * 1367) + 1) by A1, Th54, NAT_D:def 2;

      hence thesis;

    end;

    

     Lm38: ((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 Lm37, EULER_2: 9

      .= (52 * 289) by A1, Th54, NAT_D:def 2;

      hence thesis;

    end;

    

     Lm39: ((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 Lm38, EULER_2: 9

      .= 282 by A1, Th54, NAT_D:def 2;

      hence thesis;

    end;

    

     Lm40: ((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 Lm39, EULER_2: 9

      .= (71 * 197) by A1, Th54, NAT_D:def 2;

      hence thesis;

    end;

    

     Lm41: ((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 Lm40, EULER_2: 9

      .= (32 * 257) by A1, Th54, NAT_D:def 2;

      hence thesis;

    end;

    

     Lm42: ((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 Lm41, Th54, EULER_2: 9

      .= (81 * 809) by A1, NAT_D:def 2;

      hence thesis;

    end;

    

     Lm43: ((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 Lm42, EULER_2: 9

      .= 64 by A1, Th54, NAT_D:def 2;

      hence thesis;

    end;

    

     Lm44: ((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 Lm43, EULER_2: 9

      .= (256 * 16) by A1, Th54, NAT_D:def 2;

      hence thesis;

    end;

    

     Lm45: ((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 Lm44, EULER_2: 9

      .= (673 * 97) by A1, Th54, NAT_D:def 2;

      hence thesis;

    end;

    

     Lm46: ((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 Lm45, EULER_2: 9

      .= (256 * 256) by A1, Th54, NAT_D:def 2;

      hence thesis;

    end;

    

     Lm47: ( 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 thesis by Th7, NAT_D: 6;

    end;

    

     Lm48: ( 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, Lm46, EULER_2: 6;

      hence thesis by Th7, NAT_D: 6;

    end;

    theorem :: PEPIN:59

    5 is prime

    proof

      ((3 |^ ((( Fermat 1) -' 1) div 2)),( - 1)) are_congruent_mod ( Fermat 1) by Lm23;

      hence thesis by Th51, Th58;

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

      (16 div 2) = 8 by A1, POWER: 61, POWER: 62, NAT_2: 16, Lm22;

      then ((( Fermat 2) -' 1) div 2) = ((16 * 0 ) + 8) by A2, Th52;

      then ( Fermat 2) divides ((3 |^ ((( Fermat 2) -' 1) div 2)) + 1) by Lm24;

      then ( Fermat 2) divides ((3 |^ ((( Fermat 2) -' 1) div 2)) - ( - 1));

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

      hence thesis by Th52, Th58;

    end;

    theorem :: PEPIN:61

    257 is prime

    proof

      

       A1: (8 -' 1) = (8 - 1) by XREAL_0:def 2

      .= (7 + 0 );

      

       A2: (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 Lm22, NAT_2: 16

      .= (2 |^ (4 + 3)) by A1

      .= (16 * 8) by NEWTON: 8, POWER: 61, POWER: 62

      .= 128;

      then ( Fermat 3) divides ((3 |^ ((( Fermat 3) -' 1) div 2)) - ( - 1)) by A2, Lm47, Th53;

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

      hence thesis by Th53, Th58;

    end;

    theorem :: PEPIN:62

    ((256 * 256) + 1) is prime

    proof

      

       A1: (16 -' 1) = (16 - 1) by XREAL_0:def 2

      .= (15 + 0 );

      

       A2: (((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 Lm22, NAT_2: 16

      .= (2 |^ (8 + 7)) by A1

      .= (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 A2, Lm48, Th54;

      then ((3 |^ ((( Fermat 4) -' 1) div 2)),( - 1)) are_congruent_mod ( Fermat 4);

      hence thesis by Th54, Th58;

    end;

    theorem :: PEPIN:63

    

     Th63: for i,j be Integer holds j <> 0 & (i mod j) = 0 implies (i div j) = (i / j)

    proof

      let i,j be Integer such that

       A1: j <> 0 and

       A2: (i mod j) = 0 ;

      i = (((i div j) * j) + (i mod j)) by A1, INT_1: 59

      .= ((i div j) * j) by A2;

      hence thesis by A1, XCMPLX_1: 89;

    end;

    theorem :: PEPIN:64

    for i,n be Nat st n > 0 holds ((i |^ n) div i) = ((i |^ n) / i)

    proof

      let i,n be Nat;

      assume

       A1: n > 0 ;

      per cases ;

        suppose

         A2: i > 0 ;

        ((i |^ n) mod i) = 0 by A1, Th36;

        hence thesis by A2, Th63;

      end;

        suppose

         A3: i = 0 ;

        n >= ( 0 + 1) by A1, NAT_1: 13;

        then (i |^ n) = 0 by A3, NEWTON: 11;

        hence thesis by A3, NAT_D:def 1;

      end;

    end;

    reserve r for Real;

    theorem :: PEPIN:65

    

     Th65: for n be Nat holds 0 < n & 1 < r implies 1 < (r |^ n)

    proof

      let n be Nat;

      assume that

       A1: 0 < n and

       A2: r > 1;

      defpred P[ Nat] means 0 < $1 implies 1 < (r |^ $1);

      

       A3: for k be Nat holds P[k] implies P[(k + 1)]

      proof

        let k be Nat;

        assume that

         A4: P[k] and 0 < (k + 1);

        per cases ;

          suppose k > 0 ;

          then (r |^ (k + 1)) = ((r |^ k) * r) & (1 * r) <= ((r |^ k) * r) by A2, A4, NEWTON: 6, XREAL_1: 64;

          hence thesis by A2, XXREAL_0: 2;

        end;

          suppose k = 0 ;

          hence thesis by A2;

        end;

      end;

      

       A5: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A5, A3);

      hence thesis by A1;

    end;

    theorem :: PEPIN:66

    for m,n be Nat holds r > 1 & m > n implies (r |^ m) > (r |^ n)

    proof

      let m,n be Nat;

      assume that

       A1: r > 1 and

       A2: m > n;

      reconsider m, 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 thesis by A1, A3, NEWTON: 83, XREAL_1: 155;

    end;