nat_6.miz



    begin

    registration

      let n be positive natural number;

      cluster (n - 1) -> natural;

      coherence

      proof

        (n + 1) > ( 0 + 1) by XREAL_1: 6;

        then n >= 1 by NAT_1: 13;

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

        then (n - 1) in NAT by INT_1: 3;

        hence thesis;

      end;

    end

    registration

      let n be non trivial natural number;

      cluster (n - 1) -> positive;

      coherence

      proof

        (n - 1) >= (2 - 1) by NAT_2: 29, XREAL_1: 9;

        hence thesis;

      end;

    end

    registration

      let n be natural number;

      reduce (1 |^ n) to 1;

      reducibility ;

    end

    

     Lm1: for n be even natural number holds (( - 1) |^ n) = 1

    proof

      let n be even natural number;

      defpred P[ Nat] means $1 is even implies (( - 1) |^ $1) = 1;

       A1:

      now

        let k be Nat;

        assume

         A2: for n be Nat st n < k holds P[n];

        per cases ;

          suppose k is odd;

          hence P[k];

        end;

          suppose

           A3: k is even;

          now

            per cases ;

              case k = 0 ;

              hence P[k] by NEWTON: 4;

            end;

              case

               A4: k > 0 ;

               0 is even & ( 0 + 1) = 1;

              then (k - 2) in NAT by A3, A4, NAT_1: 23, INT_1: 5;

              then

              reconsider k2 = (k - 2) as Nat;

              

               A5: (k2 + 2) = k;

              then

               A6: k2 is even by A3;

              (( - 1) |^ k) = (( - 1) |^ (k2 + 2))

              .= ((( - 1) |^ k2) * (( - 1) |^ 2)) by NEWTON: 8

              .= (1 * (( - 1) |^ (1 + 1))) by A2, A6, A5, NAT_1: 16

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

              .= (( - 1) * ( - 1));

              hence P[k];

            end;

          end;

          hence P[k];

        end;

      end;

      for k be Nat holds P[k] from NAT_1:sch 4( A1);

      hence thesis;

    end;

    registration

      let n be even natural number;

      reduce (( - 1) |^ n) to 1;

      reducibility by Lm1;

    end

    

     Lm2: for n be odd natural number holds (( - 1) |^ n) = ( - 1)

    proof

      let n be odd natural number;

      defpred P[ Nat] means $1 is odd implies (( - 1) |^ $1) = ( - 1);

       A1:

      now

        let k be Nat;

        assume

         A2: for n be Nat st n < k holds P[n];

        per cases ;

          suppose k is even;

          hence P[k];

        end;

          suppose

           A3: k is odd;

          now

            per cases by NAT_1: 23;

              case k = 0 ;

              hence P[k];

            end;

              case k = 1;

              hence P[k];

            end;

              case k >= 2;

              then (k - 2) in NAT by INT_1: 5;

              then

              reconsider k2 = (k - 2) as Nat;

              

               A4: (k2 + 2) = k;

              then

               A5: k2 is odd by A3;

              (( - 1) |^ k) = (( - 1) |^ (k2 + 2))

              .= ((( - 1) |^ k2) * (( - 1) |^ 2)) by NEWTON: 8

              .= (( - 1) * (( - 1) |^ (1 + 1))) by A2, A5, A4, NAT_1: 16

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

              .= ((( - 1) * ( - 1)) * ( - 1));

              hence P[k];

            end;

          end;

          hence P[k];

        end;

      end;

      for k be Nat holds P[k] from NAT_1:sch 4( A1);

      hence thesis;

    end;

    registration

      let n be odd natural number;

      reduce (( - 1) |^ n) to ( - 1);

      reducibility by Lm2;

    end

    theorem :: NAT_6:1

    

     Th1: for a be positive natural number, n,m be natural number st n >= m holds (a |^ n) >= (a |^ m)

    proof

      let a be positive natural number;

      let n,m be natural number;

      assume n >= m;

      then (a |^ m) divides (a |^ n) by NEWTON: 89;

      hence thesis by INT_2: 27;

    end;

    theorem :: NAT_6:2

    

     Th2: for a be non trivial natural number, n,m be natural number st n > m holds (a |^ n) > (a |^ m)

    proof

      let a be non trivial natural number;

      let n,m be natural number;

      assume

       A1: n > m;

      then

      consider k be Nat such that

       A2: n = (m + k) by NAT_1: 10;

      k <> 0 by A1, A2;

      then (k + 1) > ( 0 + 1) by XREAL_1: 6;

      then k >= 1 by NAT_1: 13;

      then (a |^ k) >= (a |^ 1) by Th1;

      then

       A3: (a |^ k) >= a;

      a >= 2 by NAT_2: 29;

      then (a |^ k) >= (1 + 1) by A3, XXREAL_0: 2;

      then (a |^ k) > 1 by NAT_1: 13;

      then (1 * (a |^ m)) < ((a |^ k) * (a |^ m)) by XREAL_1: 68;

      hence thesis by A2, NEWTON: 8;

    end;

    theorem :: NAT_6:3

    

     Th3: for n be non zero natural number holds ex k be natural number, l be odd natural number st n = (l * (2 |^ k))

    proof

      let n be non zero natural number;

      per cases ;

        suppose n is odd;

        then

        reconsider l = n as odd natural number;

        take k = 0 , l;

        

        thus (l * (2 |^ k)) = (l * 1) by NEWTON: 4

        .= n;

      end;

        suppose

         A1: n is even;

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

         A2:

        now

          let m be Nat;

          

           A3: (2 |^ m) > m by NEWTON: 86;

          assume P[m];

          then (2 |^ m) <= n by INT_2: 27;

          hence m <= n by A3, XXREAL_0: 2;

        end;

        (2 |^ 1) = 2;

        then

         A3: ex m be Nat st P[m] by A1;

        consider k be Nat such that

         A4: P[k] & for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A2, A3);

        consider l be Integer such that

         A5: n = ((2 |^ k) * l) by A4, INT_1:def 3;

        l >= 0 by A5;

        then

         A6: l in NAT by INT_1: 3;

        now

          assume l is even;

          then

          consider u be Integer such that

           A7: l = (2 * u) by INT_1:def 3;

          n = (((2 |^ k) * 2) * u) by A5, A7

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

          then (2 |^ (k + 1)) divides n;

          hence contradiction by A4, NAT_1: 16;

        end;

        then

        reconsider l as odd natural number by A6;

        take k, l;

        thus thesis by A5;

      end;

    end;

    theorem :: NAT_6:4

    

     Th4: for n be even natural number holds (n div 2) = (n / 2)

    proof

      let n be even natural number;

      consider k be Nat such that

       A1: n = (2 * k) by ABIAN:def 2;

      thus thesis by A1, INT_1: 25;

    end;

    theorem :: NAT_6:5

    for n be odd natural number holds (n div 2) = ((n - 1) / 2)

    proof

      let n be odd natural number;

      consider k be Integer such that

       A1: n = ((2 * k) + 1) by ABIAN: 1;

      

       A2: ((n - 1) / 2) = k by A1;

      ((n - 1) + 1) = n;

      then (n - 1) <= n by INT_1: 6;

      then

       A3: k <= (n / 2) by A2, XREAL_1: 72;

      ((n / 2) - (1 / 2)) > ((n / 2) - 1) by XREAL_1: 10;

      hence thesis by A1, A3, INT_1:def 6;

    end;

    registration

      let n be even integer number;

      cluster (n / 2) -> integer;

      coherence

      proof

        consider k be Integer such that

         A1: n = (2 * k) by ABIAN:def 1, INT_1:def 3;

        thus thesis by A1;

      end;

    end

    registration

      let n be even natural number;

      cluster (n / 2) -> natural;

      coherence

      proof

        consider k be Integer such that

         A1: n = (2 * k) by ABIAN:def 1, INT_1:def 3;

        k >= 0 by A1;

        then k in NAT by INT_1: 3;

        then

        reconsider k as natural number;

        (n / 2) = k by A1;

        hence thesis;

      end;

    end

    begin

    registration

      cluster prime -> non trivial for natural number;

      coherence ;

    end

    

     Lm3: for a be natural number, b be integer number st a divides b holds (a gcd b) = a

    proof

      let a be natural number, b be integer number;

      assume

       A1: a divides b;

      for m be Integer st m divides a & m divides b holds m divides a;

      hence thesis by A1, INT_2:def 2;

    end;

    theorem :: NAT_6:6

    

     Th6: for p be prime natural number, a be integer number holds (a gcd p) <> 1 iff p divides a

    proof

      let p be prime natural number, a be integer number;

      hereby

        assume (a gcd p) <> 1;

        then (a gcd p) = p by INT_2: 21, INT_2:def 4;

        hence p divides a by INT_2: 21;

      end;

      assume

       A1: p divides a;

      p divides (a gcd p) by A1, INT_2: 22;

      hence (a gcd p) <> 1 by INT_2: 27, INT_2:def 4;

    end;

    theorem :: NAT_6:7

    

     Th7: for i,j be integer number, p be prime natural number st p divides (i * j) holds p divides i or p divides j

    proof

      let i,j be integer number, p be prime natural number;

      assume

       A1: p divides (i * j);

      assume not (p divides i);

      then (i gcd p) = 1 by Th6;

      hence thesis by A1, INT_2: 25, INT_2:def 3;

    end;

    theorem :: NAT_6:8

    

     Th8: for x,p be prime natural number, k be non zero natural number holds x divides (p |^ k) iff x = p

    proof

      let x,p be prime natural number;

      let k be non zero natural number;

       A1:

      now

        assume

         A2: x divides (p |^ k);

        defpred P[ Nat] means x divides (p |^ $1) implies x = p;

        

         A3: P[1]

        proof

          assume x divides (p |^ 1);

          then x divides p;

          then x = 1 or x = p by INT_2:def 4;

          hence x = p by NAT_2:def 1;

        end;

         A4:

        now

          let k be non zero Nat;

          assume

           A5: P[k];

          now

            assume

             A6: x divides (p |^ (k + 1));

            

             A7: (p |^ (k + 1)) = (p * (p |^ k)) by NEWTON: 6;

            per cases by INT_2: 30;

              suppose (x,p) are_coprime ;

              hence x = p by A5, A6, A7, INT_2: 25;

            end;

              suppose x = p;

              hence x = p;

            end;

          end;

          hence P[(k + 1)];

        end;

        

         A8: for k be non zero Nat holds P[k] from NAT_1:sch 10( A3, A4);

        thus x = p by A8, A2;

      end;

      now

        assume

         A9: x = p;

        reconsider k1 = (k - 1) as natural number;

        (p * (p |^ k1)) = (p |^ (k1 + 1)) by NEWTON: 6;

        hence x divides (p |^ k) by A9;

      end;

      hence thesis by A1;

    end;

    theorem :: NAT_6:9

    

     Th9: for x,y,n be integer number holds (x,y) are_congruent_mod n iff ex k be Integer st x = ((k * n) + y)

    proof

      let x,y,n be integer number;

      now

        assume (x,y) are_congruent_mod n;

        then

        consider k be integer Number such that

         A1: (n * k) = (x - y);

        x = ((n * k) + y) by A1;

        hence ex k be Integer st x = ((k * n) + y);

      end;

      hence thesis;

    end;

    theorem :: NAT_6:10

    

     Th10: for i be integer number, j be non zero integer number holds (i,(i mod j)) are_congruent_mod j

    proof

      let i be integer number;

      let j be non zero integer number;

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

      hence (i,(i mod j)) are_congruent_mod j;

    end;

    theorem :: NAT_6:11

    for x,y be integer number, n be positive integer number holds (x,y) are_congruent_mod n iff (x mod n) = (y mod n)

    proof

      let x,y be integer number, n be positive integer number;

       A1:

      now

        assume (x,y) are_congruent_mod n;

        then

        consider k be Integer such that

         A2: x = ((k * n) + y) by Th9;

        thus (x mod n) = (y mod n) by A2, EULER_1: 12;

      end;

      now

        assume

         A3: (x mod n) = (y mod n);

        

         A4: (x,(x mod n)) are_congruent_mod n by Th10;

        ((y mod n),y) are_congruent_mod n by Th10, INT_1: 14;

        hence (x,y) are_congruent_mod n by A3, A4, INT_1: 15;

      end;

      hence thesis by A1;

    end;

    theorem :: NAT_6:12

    

     Th12: for i,j be integer number, n be natural number st n < j & (i,n) are_congruent_mod j holds (i mod j) = n

    proof

      let i,j be integer number, n be natural number;

      assume

       A1: n < j & (i,n) are_congruent_mod j;

      then

      consider x be Integer such that

       A2: (j * x) = (i - n);

      

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

      

       A4: j in NAT by A1, INT_1: 3;

      per cases ;

        suppose n = 0 ;

        hence (i mod j) = n by A4, A1, INT_1: 62;

      end;

        suppose

         A5: n <> 0 ;

        

         A6: (i / j) = (((j * x) + n) * (j " )) by A2, XCMPLX_0:def 9

        .= ((x * (j * (j " ))) + (n * (j " )))

        .= ((x * 1) + (n * (j " ))) by A1, XCMPLX_0:def 7;

        then

         A7: x <= (i / j) by A5, A1, XREAL_1: 29;

        

         A8: ((i / j) - 1) = (x + ((n * (j " )) - 1)) by A6;

        

         A9: (n / j) < (j / j) by A1, XREAL_1: 74;

        (j / j) = (j * (j " )) by XCMPLX_0:def 9

        .= 1 by A1, XCMPLX_0:def 7;

        then (n * (j " )) < 1 by A9, XCMPLX_0:def 9;

        then ((n * (j " )) - 1) < (1 - 1) by XREAL_1: 9;

        then ((i / j) - 1) < x by A8, XREAL_1: 30;

        then (i div j) = x by A7, INT_1:def 6;

        hence (i mod j) = n by A2, A3;

      end;

    end;

    theorem :: NAT_6:13

    

     Th13: for n be non zero natural number, x be integer number holds (x, 0 ) are_congruent_mod n or ... or (x,(n - 1)) are_congruent_mod n

    proof

      let n be non zero natural number, x be integer number;

      (x mod n) in NAT by INT_1: 3, INT_1: 57;

      then

      reconsider j = (x mod n) as Nat;

      ((x mod n) + 1) <= n by INT_1: 7, INT_1: 58;

      then

       A1: (((x mod n) + 1) - 1) <= (n - 1) by XREAL_1: 9;

      take j;

      thus thesis by Th10, A1;

    end;

    theorem :: NAT_6:14

    

     Th14: for n be non zero natural number, x be integer number, k,l be natural number st k < n & l < n & (x,k) are_congruent_mod n & (x,l) are_congruent_mod n holds k = l

    proof

      let n be non zero natural number, x be integer number, k,l be natural number;

      assume

       A1: k < n & l < n & (x,k) are_congruent_mod n & (x,l) are_congruent_mod n;

      

      hence k = (x mod n) by Th12

      .= l by A1, Th12;

    end;

    theorem :: NAT_6:15

    

     Th15: for x be integer number holds ((x |^ 2), 0 ) are_congruent_mod 3 or ((x |^ 2),1) are_congruent_mod 3

    proof

      let x be integer number;

      (x, 0 ) are_congruent_mod 3 or ... or (x,(3 - 1)) are_congruent_mod 3 by Th13;

      then

       A1: (x, 0 ) are_congruent_mod 3 or ... or (x,2) are_congruent_mod 3;

      per cases by A1;

        suppose (x, 0 ) are_congruent_mod 3;

        then ((x * x),( 0 * 0 )) are_congruent_mod 3 by INT_1: 18;

        hence thesis by NEWTON: 81;

      end;

        suppose (x,1) are_congruent_mod 3;

        then ((x * x),(1 * 1)) are_congruent_mod 3 by INT_1: 18;

        hence thesis by NEWTON: 81;

      end;

        suppose (x,2) are_congruent_mod 3;

        then ((x * x),(2 * 2)) are_congruent_mod 3 by INT_1: 18;

        then (4,(x * x)) are_congruent_mod 3 by INT_1: 14;

        then ((4 - 3),(x * x)) are_congruent_mod 3 by INT_1: 22;

        then ((x * x),(4 - 3)) are_congruent_mod 3 by INT_1: 14;

        hence thesis by NEWTON: 81;

      end;

    end;

    theorem :: NAT_6:16

    

     Th16: for p be prime natural number, x,y be Element of ( Z/Z* p), i,j be integer number st x = i & y = j holds (x * y) = ((i * j) mod p)

    proof

      let p be prime natural number, x,y be Element of ( Z/Z* p), i,j be integer number;

      assume

       A1: x = i & y = j;

      

       A2: ( INT.Ring p) = doubleLoopStr (# ( Segm p), ( addint p), ( multint p), ( In (1,( Segm p))), ( In ( 0 ,( Segm p))) #) by INT_3:def 12;

      

       A3: ( Z/Z* p) = multMagma (# ( Segm0 p), ( multint0 p) #) by INT_7:def 4;

      then x in ( Segm0 p);

      then x in (( Segm p) \ { 0 }) by INT_2:def 4, INT_7:def 2;

      then

      reconsider xx = x as Element of ( Segm p) by XBOOLE_0:def 5;

      y in ( Segm0 p) by A3;

      then y in (( Segm p) \ { 0 }) by INT_2:def 4, INT_7:def 2;

      then

      reconsider yy = y as Element of ( Segm p) by XBOOLE_0:def 5;

      reconsider x1 = xx, y1 = yy as Element of ( INT.Ring p) by A2;

      

       A4: (x * y) = (x1 * y1) by INT_7: 20;

      (x1 * y1) = (( multint p) . (xx,yy)) by A2, ALGSTR_0:def 18;

      hence thesis by A4, A1, INT_3:def 10;

    end;

    theorem :: NAT_6:17

    

     Th17: for p be prime natural number, x be Element of ( Z/Z* p), i be integer number, n be natural number st x = i holds (x |^ n) = ((i |^ n) mod p)

    proof

      let p be prime natural number, x be Element of ( Z/Z* p), i be integer number, n be natural number;

      assume

       A1: x = i;

      

       A2: ( Z/Z* p) = multMagma (# ( Segm0 p), ( multint0 p) #) by INT_7:def 4;

      ( Segm0 p) = (( Segm p) \ { 0 }) by INT_2:def 4, INT_7:def 2;

      then

       A3: i in ( Segm p) by A2, A1, XBOOLE_0:def 5;

      reconsider i as Element of NAT by A1, A2, INT_1: 3;

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

      

       A4: (x |^ 0 ) = ( 1_ ( Z/Z* p)) by GROUP_1: 25;

      1 < p by INT_2:def 4;

      then

       A5: (1 div p) <= (1 - 1) by INT_1: 56, INT_1: 52;

      

       A6: (1 div p) = 0 by A5;

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

      then ((i |^ 0 ) mod p) = (1 - ((1 div p) * p)) by INT_1:def 10;

      then

       A7: P[ 0 ] by A4, A6, INT_7: 21;

       A8:

      now

        let k be Nat;

        assume

         A9: P[k];

        (x |^ (k + 1)) = ((x |^ k) * x) by GROUP_1: 34

        .= ((((i |^ k) mod p) * i) mod p) by A1, A9, Th16

        .= ((((i |^ k) mod p) * (i mod p)) mod p) by A3, NAT_D: 24, NAT_1: 44

        .= (((i |^ k) * i) mod p) by NAT_D: 67

        .= ((i |^ (k + 1)) mod p) by NEWTON: 6;

        hence P[(k + 1)];

      end;

      

       A10: for k be Nat holds P[k] from NAT_1:sch 2( A7, A8);

      thus thesis by A10;

    end;

    theorem :: NAT_6:18

    

     Th18: for p be prime natural number, x be integer number holds ((x |^ 2),1) are_congruent_mod p iff ((x,1) are_congruent_mod p or (x,( - 1)) are_congruent_mod p)

    proof

      let p be prime natural number, x be integer number;

       A1:

      now

        assume ((x |^ 2),1) are_congruent_mod p;

        then p divides ((x ^2 ) - (1 ^2 )) by NEWTON: 81;

        then

         A2: p divides ((x + 1) * (x - 1));

        now

          per cases by A2, Th7;

            case p divides (x + 1);

            then

            consider l be Integer such that

             A3: (p * l) = (x + 1);

            thus (x,( - 1)) are_congruent_mod p by A3;

          end;

            case p divides (x - 1);

            then

            consider l be Integer such that

             A4: (p * l) = (x - 1);

            thus (x,1) are_congruent_mod p by A4;

          end;

        end;

        hence (x,1) are_congruent_mod p or (x,( - 1)) are_congruent_mod p;

      end;

      now

        assume

         A5: (x,1) are_congruent_mod p or (x,( - 1)) are_congruent_mod p;

        now

          per cases by A5;

            case (x,1) are_congruent_mod p;

            then ((x * x),(1 * 1)) are_congruent_mod p by INT_1: 18;

            hence ((x |^ 2),1) are_congruent_mod p by NEWTON: 81;

          end;

            case (x,( - 1)) are_congruent_mod p;

            then ((x * x),(( - 1) * ( - 1))) are_congruent_mod p by INT_1: 18;

            hence ((x |^ 2),1) are_congruent_mod p by NEWTON: 81;

          end;

        end;

        hence ((x |^ 2),1) are_congruent_mod p;

      end;

      hence thesis by A1;

    end;

    theorem :: NAT_6:19

    

     Th19: for n be natural number holds (( - 1),1) are_congruent_mod n iff (n = 2 or n = 1)

    proof

      let n be natural number;

      hereby

        assume (( - 1),1) are_congruent_mod n;

        then

        consider k be Integer such that

         A1: (n * k) = ( - 2);

        k < 0 & n <> 0 by A1;

        then

         A2: k <= ( - 1) by INT_1: 8;

        now

          assume

           A3: n <> 2;

          now

            assume n <> 1;

            then not (n = 0 or ... or n = 2) by A1, A3;

            then not (n <= 2);

            then n >= (2 + 1) by NAT_1: 13;

            then n >= 3 & k < 0 by A1;

            then

             A4: (n * k) <= (3 * k) by XREAL_1: 65;

            (3 * k) <= (3 * ( - 1)) by A2, XREAL_1: 64;

            hence contradiction by A1, A4, XXREAL_0: 2;

          end;

          hence n = 1;

        end;

        hence n = 2 or n = 1;

      end;

      assume

       A5: n = 2 or n = 1;

      per cases by A5;

        suppose n = 2;

        then (n * ( - 1)) = ( - 2);

        hence (( - 1),1) are_congruent_mod n;

      end;

        suppose n = 1;

        hence (( - 1),1) are_congruent_mod n by INT_1: 13;

      end;

    end;

    theorem :: NAT_6:20

    

     Th20: for i be integer Number holds (( - 1),1) are_congruent_mod i iff (i = 2 or i = 1 or i = ( - 2) or i = ( - 1))

    proof

      let n be integer Number;

      hereby

        assume

         A1: (( - 1),1) are_congruent_mod n;

        then

        consider k be Integer such that

         A2: (n * k) = ( - 2);

        now

          per cases ;

            case n >= 0 ;

            then n in NAT by INT_1: 3;

            then

            reconsider m = n as natural number;

            m = 1 or m = 2 by A1, Th19;

            hence n = 2 or n = 1 or n = ( - 2) or n = ( - 1);

          end;

            case

             A3: n < 0 ;

            then

             A4: k > 0 by A2;

            then

             A5: k >= ( 0 + 1) by INT_1: 7;

            now

              assume

               A6: n <> ( - 2);

              now

                assume

                 A7: n <> ( - 1);

                n <= ( - 1) by A3, INT_1: 8;

                then n < ( - 1) by A7, XXREAL_0: 1;

                then (n + 1) <= ( - 1) by INT_1: 7;

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

                then n < ( - 2) by A6, XXREAL_0: 1;

                then (n + 1) <= ( - 2) by INT_1: 7;

                then ((n + 1) - 1) <= (( - 2) - 1) by XREAL_1: 9;

                then

                 A8: (n * k) <= (( - 3) * k) by A4, XREAL_1: 64;

                (( - 3) * k) <= (( - 3) * 1) by A5, XREAL_1: 65;

                hence contradiction by A2, A8, XXREAL_0: 2;

              end;

              hence n = ( - 1);

            end;

            hence n = 2 or n = 1 or n = ( - 2) or n = ( - 1);

          end;

        end;

        hence n = 2 or n = 1 or n = ( - 2) or n = ( - 1);

      end;

      assume

       A9: n = 2 or n = 1 or n = ( - 2) or n = ( - 1);

      per cases by A9;

        suppose n = 2;

        then (n * ( - 1)) = ( - 2);

        hence (( - 1),1) are_congruent_mod n;

      end;

        suppose n = 1;

        hence (( - 1),1) are_congruent_mod n by INT_1: 13;

      end;

        suppose n = ( - 2);

        hence (( - 1),1) are_congruent_mod n;

      end;

        suppose n = ( - 1);

        then (n * ( - 1)) = 1;

        hence (( - 1),1) are_congruent_mod n by INT_1: 20, INT_1: 13;

      end;

    end;

    begin

    definition

      let n,x be natural number;

      :: NAT_6:def1

      attr x is n _greater means

      : Def1: x > n;

    end

    notation

      let n,x be natural number;

      antonym x is n _smaller for x is n _or_greater;

      antonym x is n _or_smaller for x is n _greater;

    end

    registration

      let n be natural number;

      cluster n _greater odd for natural number;

      existence

      proof

        per cases ;

          suppose n is even;

          then

          consider k be Nat such that

           A1: n = (2 * k);

          take (n + 1);

          (n + 1) > (n + 0 ) by XREAL_1: 6;

          hence (n + 1) is n _greater;

          thus (n + 1) is odd by A1;

        end;

          suppose n is odd;

          then

          consider k be Integer such that

           A2: n = ((2 * k) + 1) by ABIAN: 1;

          take (n + 2);

          (n + 1) > (n + 0 ) by XREAL_1: 6;

          hence (n + 2) is n _greater by XREAL_1: 6;

          thus (n + 2) is odd by A2;

        end;

      end;

      cluster n _greater even for natural number;

      existence

      proof

        per cases ;

          suppose n is odd;

          then

          consider k be Integer such that

           A3: n = ((2 * k) + 1) by ABIAN: 1;

          take (n + 1);

          (n + 1) > (n + 0 ) by XREAL_1: 6;

          hence (n + 1) is n _greater;

          thus (n + 1) is even by A3;

        end;

          suppose n is even;

          then

          consider k be Nat such that

           A4: n = (2 * k);

          take (n + 2);

          (n + 1) > (n + 0 ) by XREAL_1: 6;

          hence (n + 2) is n _greater by XREAL_1: 6;

          thus (n + 2) is even by A4;

        end;

      end;

    end

    registration

      let n be natural number;

      cluster n _greater -> n _or_greater for natural number;

      coherence ;

    end

    registration

      let n be natural number;

      cluster (n + 1) _or_greater -> n _or_greater for natural number;

      coherence

      proof

        let x be natural number;

        assume

         A1: x is (n + 1) _or_greater;

        (n + 1) >= (n + 0 ) by XREAL_1: 6;

        hence x is n _or_greater by A1, XXREAL_0: 2;

      end;

      cluster (n + 1) _greater -> n _greater for natural number;

      coherence

      proof

        let x be natural number;

        assume

         A2: x is (n + 1) _greater;

        (n + 1) > (n + 0 ) by XREAL_1: 6;

        hence x is n _greater by A2, XXREAL_0: 2;

      end;

      cluster n _greater -> (n + 1) _or_greater for natural number;

      coherence by NAT_1: 13;

    end

    registration

      let m be non trivial natural number;

      cluster m _or_greater -> non trivial for natural number;

      coherence

      proof

        let n be natural number;

        assume

         A1: n is m _or_greater;

        m >= 2 by NAT_2: 29;

        hence thesis by A1, XXREAL_0: 2;

      end;

    end

    registration

      let a be positive natural number;

      let m be natural number;

      let n be m _or_greater natural number;

      cluster (a |^ n) -> (a |^ m) _or_greater;

      coherence by Th1, EC_PF_2:def 1;

    end

    registration

      let a be non trivial natural number;

      let m be natural number;

      let n be m _greater natural number;

      cluster (a |^ n) -> (a |^ m) _greater;

      coherence by Def1, Th2;

    end

    registration

      cluster 2 _or_greater -> non trivial for natural number;

      coherence ;

      cluster non trivial -> 2 _or_greater for natural number;

      coherence

      proof

        let n be natural number;

        assume

         A1: n is non trivial;

        n <= 1 implies n = 0 or ... or n = 1;

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

        hence thesis;

      end;

      cluster non trivial odd -> 2 _greater for natural number;

      coherence

      proof

        let n be natural number;

        assume

         A2: n is non trivial odd;

        n <= 2 implies n = 0 or ... or n = 2;

        hence thesis by A2;

      end;

    end

    registration

      let n be 2 _greater natural number;

      cluster (n - 1) -> non trivial;

      coherence

      proof

        (n - 1) > (2 - 1) by Def1, XREAL_1: 9;

        hence thesis by NAT_2:def 1;

      end;

    end

    registration

      let n be 2 _or_greater natural number;

      cluster (n - 2) -> natural;

      coherence

      proof

        (n - 2) >= (2 - 2) by EC_PF_2:def 1, XREAL_1: 9;

        then (n - 2) in NAT by INT_1: 3;

        hence thesis;

      end;

    end

    registration

      let m be non zero natural number;

      let n be m _or_greater natural number;

      cluster (n - 1) -> natural;

      coherence

      proof

        n >= m by EC_PF_2:def 1;

        then

        reconsider nn = (n - 1) as Element of NAT by INT_1: 3;

        (n - 1) >= (m - 1) by EC_PF_2:def 1, XREAL_1: 9;

        then (n - 1) in NAT by INT_1: 3;

        hence thesis;

      end;

    end

    registration

      cluster 2 _greater -> odd for prime natural number;

      coherence by INT_2:def 4;

    end

    registration

      let n be natural number;

      cluster n _greater prime for natural number;

      existence

      proof

        now

          assume

           A1: not (ex p be natural number st p is n _greater prime);

           A2:

          now

            let p be prime natural number;

             not (p is n _greater) by A1;

            hence p < (n + 1) by NAT_1: 13;

          end;

           A3:

          now

            let p be set;

            assume

             A4: p in SetPrimes ;

            then

            reconsider p1 = p as Element of NAT ;

            

             A5: p1 is prime by A4, NEWTON:def 6;

            then p1 < (n + 1) by A2;

            hence p in ( SetPrimenumber (n + 1)) by A5, NEWTON:def 7;

          end;

          now

            let p be set;

            assume

             A6: p in ( SetPrimenumber (n + 1));

            reconsider n1 = (n + 1) as Nat;

            ( SetPrimenumber n1) c= SetPrimes by NEWTON: 68;

            hence p in SetPrimes by A6;

          end;

          then SetPrimes = ( SetPrimenumber (n + 1)) by A3;

          hence contradiction;

        end;

        hence thesis;

      end;

    end

    begin

    definition

      let n be natural number;

      :: NAT_6:def2

      mode Divisor of n -> natural number means

      : Def2: it divides n;

      existence ;

    end

    registration

      let n be non trivial natural number;

      cluster non trivial for Divisor of n;

      existence

      proof

        reconsider m = n as Divisor of n by Def2;

        take m;

        thus thesis;

      end;

    end

    registration

      let n be non zero natural number;

      cluster -> non zero for Divisor of n;

      coherence

      proof

        let x be Divisor of n;

        consider k be Integer such that

         A1: (x * k) = n by Def2, INT_1:def 3;

        thus thesis by A1;

      end;

    end

    registration

      let n be positive natural number;

      cluster -> positive for Divisor of n;

      coherence ;

    end

    registration

      let n be non zero natural number;

      cluster -> n _or_smaller for Divisor of n;

      coherence

      proof

        let x be Divisor of n;

        consider k be Integer such that

         A1: (x * k) = n by Def2, INT_1:def 3;

        k >= 0 by A1;

        then

        reconsider k as Element of NAT by INT_1: 3;

        k <> 0 by A1;

        hence thesis by A1, NAT_1: 24;

      end;

    end

    registration

      let n be non trivial natural number;

      cluster prime for Divisor of n;

      existence

      proof

        consider p be Element of NAT such that

         A1: p is prime & p divides n by NAT_2: 29, INT_2: 31;

        reconsider p as natural number;

        take p;

        thus thesis by A1, Def2;

      end;

    end

    registration

      let n be natural number;

      let q be Divisor of n;

      cluster (n / q) -> natural;

      coherence

      proof

        per cases ;

          suppose n = 0 ;

          hence thesis;

        end;

          suppose

           A1: n <> 0 ;

          consider k be Integer such that

           A2: (q * k) = n by Def2, INT_1:def 3;

           0 <= k by A2, A1;

          then

           A3: k in NAT by INT_1: 3;

          (n / q) = ((q * k) * (q " )) by A2, XCMPLX_0:def 9

          .= (k * (q * (q " )))

          .= (k * 1) by A1, XCMPLX_0:def 7;

          hence thesis by A3;

        end;

      end;

    end

    registration

      let n be natural number;

      let s be Divisor of n;

      let q be Divisor of s;

      cluster (n / q) -> natural;

      coherence

      proof

        per cases ;

          suppose n = 0 ;

          hence thesis;

        end;

          suppose

           A1: n <> 0 ;

          consider k be Integer such that

           A2: (s * k) = n by Def2, INT_1:def 3;

          consider l be Integer such that

           A3: (q * l) = s by Def2, INT_1:def 3;

           0 <= k by A2, A1;

          then

           A4: k in NAT by INT_1: 3;

           0 <= l by A3, A1;

          then

           A5: l in NAT by INT_1: 3;

          (n / q) = (((q * l) * k) * (q " )) by A3, A2, XCMPLX_0:def 9

          .= ((l * k) * (q * (q " )))

          .= ((l * k) * 1) by A1, XCMPLX_0:def 7;

          hence thesis by A4, A5;

        end;

      end;

    end

    ::$Notion-Name

    theorem :: NAT_6:21

    

     Th21: for n be 2 _greater natural number, s be non trivial Divisor of (n - 1) st s > ( sqrt n) & ex a be natural number st ((a |^ (n - 1)),1) are_congruent_mod n & for q be prime Divisor of s holds (((a |^ ((n - 1) / q)) - 1) gcd n) = 1 holds n is prime

    proof

      let n be 2 _greater natural number;

      let s be non trivial Divisor of (n - 1);

      assume

       A1: s > ( sqrt n) & ex a be natural number st ((a |^ (n - 1)),1) are_congruent_mod n & for q be prime Divisor of s holds (((a |^ ((n - 1) / q)) - 1) gcd n) = 1;

      reconsider m = n as Element of NAT by ORDINAL1:def 12;

      reconsider f = s as Element of NAT by ORDINAL1:def 12;

      m > (1 + 1) by Def1;

      then

       A2: m >= 1 by NAT_1: 13;

      consider c be Integer such that

       A3: (m - 1) = (f * c) by Def2, INT_1:def 3;

      

       A4: ( sqrt n) >= 0 by SQUARE_1:def 2;

       A5:

      now

        assume s <= c;

        then c >= ( sqrt n) by A1, XXREAL_0: 2;

        then (s * c) >= (( sqrt n) ^2 ) by A4, A1, XREAL_1: 66;

        then (s * c) >= n by SQUARE_1:def 2;

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

        then ( - 1) >= 0 ;

        hence contradiction;

      end;

      c > 0 by A3;

      then

      reconsider c as Element of NAT by INT_1: 3;

      

       A6: (m - 1) = (f * c) & f > c & c > 0 by A3, A5;

      now

        let p be Element of NAT ;

        assume

         A7: p divides f & p is prime;

        reconsider q = p as natural number;

        reconsider q as Divisor of s by A7, Def2;

        reconsider q as prime Divisor of s by A7;

        consider b be natural number such that

         A8: ((b |^ (n - 1)),1) are_congruent_mod n & for q be prime Divisor of s holds (((b |^ ((n - 1) / q)) - 1) gcd n) = 1 by A1;

        reconsider a = b as Element of NAT by ORDINAL1:def 12;

        consider k1 be Integer such that

         A9: (q * k1) = s by Def2, INT_1:def 3;

        consider k2 be Integer such that

         A10: (s * k2) = (n - 1) by Def2, INT_1:def 3;

        consider l1 be Integer such that

         A11: (p * l1) = f by A7;

        

         A12: k2 = c by A3, A10, XCMPLX_1: 5;

        

         A13: ((m - 1) / p) = (((p * l1) * c) * (p " )) by A3, A11, XCMPLX_0:def 9

        .= ((l1 * c) * (p * (p " )))

        .= ((l1 * c) * 1) by A7, XCMPLX_0:def 7;

        

         A14: (n - 1) >= (2 - 1) by Def1, XREAL_1: 9;

        now

          assume a = 0 ;

          then (a |^ (n - 1)) = 0 by A14, NEWTON: 11;

          then n = 1 or n = ( - 1) by A8, INT_2: 13;

          hence contradiction by Def1;

        end;

        then ((a |^ ((m -' 1) div p)) + 1) > ( 0 + 1) by XREAL_1: 6;

        then

         A15: (a |^ ((m -' 1) div p)) >= 1 by NAT_1: 13;

        ((n - 1) / q) = (((q * k1) * k2) * (q " )) by A9, A10, XCMPLX_0:def 9

        .= ((k1 * k2) * (q * (q " )))

        .= ((k1 * k2) * 1) by XCMPLX_0:def 7

        .= ((m - 1) / p) by A9, A11, A12, A13, XCMPLX_1: 5

        .= [/((m - 1) / p)\] by A13, INT_1: 30

        .= [\((m - 1) / p)/] by A13, INT_1: 34

        .= ((m -' 1) div p) by A2, XREAL_1: 233;

        then ((a |^ ((m -' 1) div p)) -' 1) = ((b |^ ((n - 1) / q)) - 1) by A15, XREAL_1: 233;

        then

         A16: (((a |^ ((m -' 1) div p)) -' 1) gcd m) = 1 by A8;

        consider x be Integer such that

         A17: (n * x) = ((a |^ (n - 1)) - 1) by A8;

        

         A18: ((a |^ (n - 1)) / n) = (((n * x) + 1) * (n " )) by A17, XCMPLX_0:def 9

        .= ((((n " ) * n) * x) + (1 * (n " )))

        .= ((1 * x) + (n " )) by XCMPLX_0:def 7;

        

         A19: x <= ((a |^ (n - 1)) / n) by A18, XREAL_1: 29;

        

         A20: (((a |^ (n - 1)) / n) - 1) = (x + ((n " ) - 1)) by A18;

        2 < n by Def1;

        then (2 - 1) < (n - 0 ) by XREAL_1: 15;

        then (n " ) < (1 " ) by XREAL_1: 88;

        then ((n " ) - 1) < 0 by XREAL_1: 49;

        then (((a |^ (n - 1)) / n) - 1) < x by A20, XREAL_1: 30;

        then ((a |^ (n - 1)) div n) = x by A19, INT_1:def 6;

        

        then

         A21: ((a |^ (n - 1)) mod n) = ((a |^ (n - 1)) - (n * x)) by INT_1:def 10

        .= 1 by A17;

        ((a |^ (m -' 1)) mod m) = 1 by A21, A2, XREAL_1: 233;

        hence ex a be Element of NAT st ((a |^ (m -' 1)) mod m) = 1 & (((a |^ ((m -' 1) div p)) -' 1) gcd m) = 1 by A16;

      end;

      hence thesis by A6, NAT_4: 24;

    end;

    begin

    notation

      let a be integer number, p be natural number;

      antonym a is_quadratic_non_residue_mod p for a is_quadratic_residue_mod p;

    end

    theorem :: NAT_6:22

    

     Th22: for p be positive natural number, a be integer number holds a is_quadratic_residue_mod p iff ex x be integer number st ((x |^ 2),a) are_congruent_mod p

    proof

      let p be positive natural number, a be integer number;

      thus a is_quadratic_residue_mod p implies ex x be integer number st ((x |^ 2),a) are_congruent_mod p

      proof

        assume a is_quadratic_residue_mod p;

        then

        consider x be Integer such that

         A1: (((x ^2 ) - a) mod p) = 0 by INT_5:def 2;

        

         A2: ((x ^2 ) - a) = (((((x ^2 ) - a) div p) * p) + 0 ) by A1, INT_1: 59;

        reconsider xx = x as integer number by TARSKI: 1;

        take xx;

        (xx ^2 ) = (xx |^ 2) by NEWTON: 81;

        hence thesis by A2;

      end;

      assume ex x be integer number st ((x |^ 2),a) are_congruent_mod p;

      then

      consider x be integer number such that

       A3: ((x |^ 2),a) are_congruent_mod p;

      (x ^2 ) = ((x |^ 1) * x)

      .= (x |^ (1 + 1)) by NEWTON: 6;

      then (((x ^2 ) - a) mod p) = 0 by A3, INT_1: 62;

      hence a is_quadratic_residue_mod p by INT_5:def 2;

    end;

    theorem :: NAT_6:23

    

     Th23: 2 is_quadratic_non_residue_mod 3

    proof

      now

        assume ex x be integer number st ((x |^ 2),2) are_congruent_mod 3;

        then

        consider x be integer number such that

         A1: ((x |^ 2),2) are_congruent_mod 3;

        now

          per cases by Th15;

            case ((x |^ 2), 0 ) are_congruent_mod 3;

            hence contradiction by A1, Th14;

          end;

            case ((x |^ 2),1) are_congruent_mod 3;

            hence contradiction by A1, Th14;

          end;

        end;

        hence contradiction;

      end;

      hence thesis by Th22;

    end;

    ::$Notion-Name

    definition

      let p be natural number;

      let a be integer number;

      :: NAT_6:def3

      func LegendreSymbol (a,p) -> integer Number equals

      : Def3: 1 if (a gcd p) = 1 & a is_quadratic_residue_mod p & p <> 1,

0 if p divides a,

( - 1) if (a gcd p) = 1 & a is_quadratic_non_residue_mod p & p <> 1;

      coherence ;

      consistency by Lm3;

    end

    definition

      let p be prime natural number;

      let a be integer number;

      :: original: LegendreSymbol

      redefine

      :: NAT_6:def4

      func LegendreSymbol (a,p) equals

      : Def4: 1 if (a gcd p) = 1 & a is_quadratic_residue_mod p,

0 if p divides a,

( - 1) if (a gcd p) = 1 & a is_quadratic_non_residue_mod p;

      consistency

      proof

        

         A1: (a gcd p) = 1 & a is_quadratic_residue_mod p & p divides a implies for z be integer number holds z = 1 iff z = 0

        proof

          assume

           A2: (a gcd p) = 1 & a is_quadratic_residue_mod p & p divides a;

          then (a gcd p) = p by Lm3;

          hence thesis by A2, INT_2:def 4;

        end;

        (a gcd p) = 1 & a is_quadratic_non_residue_mod p & p divides a implies for z be integer number holds z = ( - 1) iff z = 0

        proof

          assume

           A3: (a gcd p) = 1 & a is_quadratic_non_residue_mod p & p divides a;

          then (a gcd p) = p by Lm3;

          hence thesis by A3, INT_2:def 4;

        end;

        hence thesis by A1;

      end;

      compatibility

      proof

        p <> 1 by INT_2:def 4;

        hence thesis by Def3;

      end;

    end

    notation

      let p be natural number;

      let a be integer number;

      synonym Leg (a,p) for LegendreSymbol (a,p);

    end

    theorem :: NAT_6:24

    

     Th24: for p be prime natural number, a be integer number holds ( Leg (a,p)) = 1 or ( Leg (a,p)) = 0 or ( Leg (a,p)) = ( - 1)

    proof

      let p be prime natural number;

      let a be integer number;

      assume

       A1: ( Leg (a,p)) <> 1 & ( Leg (a,p)) <> 0 ;

      (a gcd p) = 1

      proof

        (a gcd p) = 1 or (a gcd p) = p by INT_2:def 4, INT_2: 21;

        hence thesis by A1, Def4, INT_2: 21;

      end;

      hence ( Leg (a,p)) = ( - 1) by A1, Def4;

    end;

    theorem :: NAT_6:25

    

     Th25: for p be prime natural number, a be integer number holds (( Leg (a,p)) = 1 iff (a gcd p) = 1 & a is_quadratic_residue_mod p) & (( Leg (a,p)) = 0 iff p divides a) & (( Leg (a,p)) = ( - 1) iff (a gcd p) = 1 & a is_quadratic_non_residue_mod p)

    proof

      let p be prime natural number, a be integer number;

       A1:

      now

        assume

         A2: ( Leg (a,p)) = 0 ;

        now

          assume not p divides a;

          then (a gcd p) = 1 by Th6;

          hence contradiction by A2, Def4;

        end;

        hence p divides a;

      end;

      now

        assume

         A3: ( Leg (a,p)) = 1;

        then (a gcd p) = 1 by Th6, Def4;

        hence (a gcd p) = 1 & a is_quadratic_residue_mod p by A3, Def4;

      end;

      hence ( Leg (a,p)) = 1 iff (a gcd p) = 1 & a is_quadratic_residue_mod p by Def4;

      now

        assume

         A4: ( Leg (a,p)) = ( - 1);

        then (a gcd p) = 1 by Th6, Def4;

        hence (a gcd p) = 1 & a is_quadratic_non_residue_mod p by A4, Def4;

      end;

      hence thesis by A1, Def4;

    end;

    theorem :: NAT_6:26

    for p be natural number holds ( Leg (p,p)) = 0 by Def3;

    theorem :: NAT_6:27

    for a be integer number holds ( Leg (a,2)) = (a mod 2)

    proof

      let a be integer number;

      per cases ;

        suppose

         A1: a is even;

        then (a mod 2) = 0 by INT_1: 62;

        hence thesis by A1, Def3;

      end;

        suppose

         A2: a is odd;

        reconsider amod2 = (a mod 2) as Element of NAT by INT_1: 3, INT_1: 57;

        

         A3: amod2 = 0 or amod2 = 1 by NAT_1: 23, INT_1: 58;

        (a - 1) = ((((a div 2) * 2) + 1) - 1) by A3, A2, INT_1: 62, INT_1: 59;

        then

         A4: (1,a) are_congruent_mod 2 by INT_1:def 5, INT_1: 14;

        (a gcd 2) <= 2 by INT_2: 27, INT_2: 21;

        then

         A5: (a gcd 2) = 0 or ... or (a gcd 2) = 2;

        (1 |^ (1 + 1)) = 1;

        hence thesis by A4, INT_2: 5, A5, INT_2: 21, A3, A2, INT_1: 62, Def3, Th22;

      end;

    end;

    

     Lm4: for a be integer number, p be prime natural number holds ( Lege (a,p)) = ( Leg (a,p))

    proof

      let a be integer number, p be prime natural number;

      per cases by Th24;

        suppose

         A1: ( Leg (a,p)) = 1;

        then not (p divides a) by Th25;

        then (a mod p) <> 0 by INT_1: 62;

        hence thesis by A1, INT_5:def 3, Th25;

      end;

        suppose

         A2: ( Leg (a,p)) = 0 ;

        then

         A3: p divides a by Th25;

        p divides ( - a) by A2, Th25, INT_2: 10;

        then

         A4: ((( 0 ^2 ) - a) mod p) = 0 by INT_1: 62;

        (a mod p) = 0 by A3, INT_1: 62;

        hence thesis by A2, A4, INT_5:def 3, INT_5:def 2;

      end;

        suppose ( Leg (a,p)) = ( - 1);

        hence thesis by Th25, INT_5:def 3;

      end;

    end;

    theorem :: NAT_6:28

    

     Th28: for p be 2 _greater prime natural number, a,b be integer number st (a gcd p) = 1 & (b gcd p) = 1 & (a,b) are_congruent_mod p holds ( Leg (a,p)) = ( Leg (b,p))

    proof

      let p be 2 _greater prime natural number, a,b be integer number;

      assume

       A1: (a gcd p) = 1 & (b gcd p) = 1 & (a,b) are_congruent_mod p;

      

      thus ( Leg (a,p)) = ( Lege (a,p)) by Lm4

      .= ( Lege (b,p)) by Def1, A1, INT_5: 29

      .= ( Leg (b,p)) by Lm4;

    end;

    theorem :: NAT_6:29

    for p be 2 _greater prime natural number, a,b be integer number st (a gcd p) = 1 & (b gcd p) = 1 holds ( Leg ((a * b),p)) = (( Leg (a,p)) * ( Leg (b,p)))

    proof

      let p be 2 _greater prime natural number, a,b be integer number;

      assume

       A1: (a gcd p) = 1 & (b gcd p) = 1;

      

      thus ( Leg ((a * b),p)) = ( Lege ((a * b),p)) by Lm4

      .= (( Lege (a,p)) * ( Lege (b,p))) by A1, Def1, INT_5: 30

      .= (( Leg (a,p)) * ( Lege (b,p))) by Lm4

      .= (( Leg (a,p)) * ( Leg (b,p))) by Lm4;

    end;

    theorem :: NAT_6:30

    

     Th30: for p,q be 2 _greater prime natural number st p <> q holds (( Leg (p,q)) * ( Leg (q,p))) = (( - 1) |^ (((p - 1) / 2) * ((q - 1) / 2)))

    proof

      let p,q be 2 _greater prime natural number;

      assume

       A1: p <> q;

      

       A2: p > 2 & q > 2 by Def1;

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

      then (p -' 1) = (p - 1) by NAT_D: 39;

      then

       A3: ((p -' 1) div 2) = ((p - 1) / 2) by Th4;

      (q - 1) > (2 - 1) by Def1, XREAL_1: 9;

      then (q -' 1) = (q - 1) by NAT_D: 39;

      then

       A4: (( - 1) |^ (((p -' 1) div 2) * ((q -' 1) div 2))) = (( - 1) |^ (((p - 1) / 2) * ((q - 1) / 2))) by A3, Th4;

      

      thus (( Leg (p,q)) * ( Leg (q,p))) = (( Leg (p,q)) * ( Lege (q,p))) by Lm4

      .= (( Lege (p,q)) * ( Lege (q,p))) by Lm4

      .= (( - 1) |^ (((p - 1) / 2) * ((q - 1) / 2))) by A1, A2, A4, INT_5: 49;

    end;

    ::$Notion-Name

    theorem :: NAT_6:31

    

     Th31: for p be 2 _greater prime natural number, a be integer number st (a gcd p) = 1 holds ((a |^ ((p - 1) / 2)),( LegendreSymbol (a,p))) are_congruent_mod p

    proof

      let p be 2 _greater prime natural number, a be integer number;

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

      then

       A1: (p -' 1) = (p - 1) by NAT_D: 39;

      assume (a gcd p) = 1;

      then (( Lege (a,p)),(a |^ ((p -' 1) div 2))) are_congruent_mod p by Def1, INT_5: 28;

      then

       A2: (( Lege (a,p)),(a |^ ((p - 1) / 2))) are_congruent_mod p by A1, Th4;

      ( Leg (a,p)) = ( Lege (a,p)) by Lm4;

      hence thesis by A2, INT_1: 14;

    end;

    begin

    ::$Notion-Name

    definition

      let p be natural number;

      :: NAT_6:def5

      attr p is Proth means

      : Def5: ex k be odd natural number, n be positive natural number st (2 |^ n) > k & p = ((k * (2 |^ n)) + 1);

    end

    

     Lm5: 1 is odd

    proof

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

      hence thesis;

    end;

    

     Lm6: 3 is Proth

    proof

      reconsider e = 1 as odd natural number by Lm5;

      take e, 1;

      thus thesis;

    end;

    

     Lm7: 9 is Proth

    proof

      

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

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

      .= (2 * 2);

      

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

      .= (4 * 2) by A1, NEWTON: 6;

      reconsider e = 1 as odd natural number by Lm5;

      take e, 3;

      thus thesis by A2;

    end;

    registration

      cluster Proth prime for natural number;

      existence by Lm6, PEPIN: 41;

      cluster Proth non prime for natural number;

      existence

      proof

        (3 * 3) = 9;

        then 3 divides 9;

        then 9 is non prime;

        hence thesis by Lm7;

      end;

    end

    registration

      cluster Proth -> non trivial odd for natural number;

      coherence

      proof

        let p be natural number;

        assume

         A1: p is Proth;

        then

        consider k be odd natural number, n be positive natural number such that

         A2: (2 |^ n) > k & p = ((k * (2 |^ n)) + 1);

        thus p is non trivial by A1, NAT_2:def 1;

        reconsider n1 = (n - 1) as Element of NAT by INT_1: 3;

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

        .= (2 |^ n);

        hence thesis by A2;

      end;

    end

    theorem :: NAT_6:32

    3 is Proth by Lm6;

    theorem :: NAT_6:33

    5 is Proth

    proof

      

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

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

      .= (2 * 2);

      reconsider e = 1 as odd natural number by Lm5;

      take e, 2;

      thus thesis by A1;

    end;

    theorem :: NAT_6:34

    9 is Proth by Lm7;

    theorem :: NAT_6:35

    13 is Proth

    proof

      

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

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

      .= (2 * 2);

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

      then

      reconsider e = 3 as odd natural number;

      take e, 2;

      thus thesis by A1;

    end;

    theorem :: NAT_6:36

    17 is Proth

    proof

      

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

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

      .= (2 * 2);

      

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

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

      .= 8 by A1;

      

       A3: (2 |^ 4) = (2 |^ (3 + 1))

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

      .= 16 by A2;

      reconsider e = 1 as odd natural number by Lm5;

      take e, 4;

      thus thesis by A3;

    end;

    theorem :: NAT_6:37

    

     Th37: 641 is Proth

    proof

      

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

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

      .= (2 * 2);

      then (2 |^ (2 + 2)) = (4 * 4) by NEWTON: 8;

      then

       A2: (2 |^ (4 + 2)) = (16 * 4) by A1, NEWTON: 8;

      

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

      .= (64 * 2) by A2;

      

       A4: 5 = ((2 * 2) + 1);

      641 = ((5 * (2 |^ 7)) + 1) by A3;

      hence thesis by A3, A4;

    end;

    theorem :: NAT_6:38

    11777 is Proth

    proof

      

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

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

      .= (2 * 2);

      

       A2: (2 |^ (2 + 2)) = (4 * 4) by A1, NEWTON: 8;

      

       A3: (2 |^ (4 + 4)) = (16 * 16) by A2, NEWTON: 8;

      

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

      .= (256 * 2) by A3;

      

       A5: 23 = ((2 * 11) + 1);

      11777 = ((23 * (2 |^ 9)) + 1) by A4;

      hence thesis by A4, A5;

    end;

    theorem :: NAT_6:39

    13313 is Proth

    proof

      

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

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

      .= (2 * 2);

      then (2 |^ (2 + 2)) = (4 * 4) by NEWTON: 8;

      then (2 |^ (4 + 4)) = (16 * 16) by NEWTON: 8;

      then

       A2: (2 |^ (8 + 2)) = (256 * 4) by A1, NEWTON: 8;

      

       A3: 13 = ((2 * 6) + 1);

      13313 = ((13 * (2 |^ 10)) + 1) by A2;

      hence thesis by A2, A3;

    end;

    ::$Notion-Name

    theorem :: NAT_6:40

    

     Th40: for n be Proth natural number holds n is prime iff ex a be natural number st ((a |^ ((n - 1) / 2)),( - 1)) are_congruent_mod n

    proof

      let n be Proth natural number;

      consider k be odd natural number, l be positive natural number such that

       A1: (2 |^ l) > k & n = ((k * (2 |^ l)) + 1) by Def5;

      set s = (2 |^ l);

      

       A2: (l + 1) >= (1 + 1) by NAT_1: 14, XREAL_1: 6;

      (2 |^ l) >= (l + 1) by NEWTON: 85;

      then (2 |^ l) <> 0 & (2 |^ l) <> 1 by A2, XXREAL_0: 2;

      then

      reconsider s as non trivial natural number by NAT_2:def 1;

      reconsider s as non trivial Divisor of (n - 1) by A1, INT_1:def 3, Def2;

       A3:

      now

        assume ex a be natural number st ((a |^ ((n - 1) / 2)),( - 1)) are_congruent_mod n;

        then

        consider a be natural number such that

         A4: ((a |^ ((n - 1) / 2)),( - 1)) are_congruent_mod n;

        

         A5: ((a |^ ((n - 1) / 2)) * (a |^ ((n - 1) / 2))) = (a |^ (((n - 1) / 2) + ((n - 1) / 2))) by NEWTON: 8

        .= (a |^ (n - 1));

        

         A6: (( - 1) * ( - 1)) = 1;

        

         A7: l >= 1 by NAT_1: 14;

        (((2 |^ l) - 1) + 1) > k by A1;

        then

         A8: k <= ((2 |^ l) - 1) by NAT_1: 13;

        then (k * (2 |^ l)) <= (((2 |^ l) - 1) * (2 |^ l)) by XREAL_1: 64;

        then

         A9: n <= ((((2 |^ l) - 1) * (2 |^ l)) + 1) by A1, XREAL_1: 6;

        ((((2 |^ l) - 1) * (2 |^ l)) + 1) = ((((2 |^ l) * (2 |^ l)) - (2 |^ l)) + 1)

        .= (((2 |^ (l + l)) - (2 |^ l)) + 1) by NEWTON: 8;

        then

         A10: n < ((((2 |^ (l + l)) - (2 |^ l)) + 1) + 1) by A9, NAT_1: 13;

        

         A11: s > ( sqrt n)

        proof

          per cases ;

            suppose l >= 2;

            then

             A12: (2 |^ l) >= (2 |^ 2) by Th1;

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

            .= (2 * 2);

            then (2 |^ l) > 2 by A12, XXREAL_0: 2;

            then (2 - (2 |^ l)) < ((2 |^ l) - (2 |^ l)) by XREAL_1: 9;

            then ((2 |^ (l + l)) + (( - (2 |^ l)) + 2)) < ((2 |^ (l + l)) + 0 ) by XREAL_1: 6;

            then

             A13: n < (2 |^ (2 * l)) by A10, XXREAL_0: 2;

            ((2 |^ l) ^2 ) = (2 |^ (l + l)) by NEWTON: 8;

            then ( sqrt (2 |^ (2 * l))) = (2 |^ l) by SQUARE_1:def 2;

            hence thesis by A13, SQUARE_1: 27;

          end;

            suppose l < 2;

            then l < (1 + 1);

            then

             A14: l <= 1 by NAT_1: 13;

            then

             A15: l = 1 by A7, XXREAL_0: 1;

            then

             A16: s = ( sqrt 4) by SQUARE_1: 20;

            

             A17: n = ((k * (2 |^ 1)) + 1) by A14, A1, A7, XXREAL_0: 1

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

            

             A18: k <= (2 - 1) by A8, A15;

            k >= 1 by NAT_1: 14;

            then k = 1 by A18, XXREAL_0: 1;

            hence thesis by A17, A16, SQUARE_1: 27;

          end;

        end;

        now

          let q be prime Divisor of s;

          

           A19: ((a |^ ((n - 1) / q)),( - 1)) are_congruent_mod n by A4, Th8, INT_2: 28, Def2;

          (1 * ((a |^ ((n - 1) / q)) - 1)) = ((a |^ ((n - 1) / q)) - 1);

          then

           A20: 1 divides ((a |^ ((n - 1) / q)) - 1);

          (1 * n) = n;

          then

           A21: 1 divides n;

          now

            let m be Integer;

            assume

             A22: m divides ((a |^ ((n - 1) / q)) - 1) & m divides n;

            then

             A23: ((a |^ ((n - 1) / q)),1) are_congruent_mod m;

            consider j be Integer such that

             A24: (m * j) = n by A22;

            ((a |^ ((n - 1) / q)),( - 1)) are_congruent_mod m by A19, A24, INT_1: 20;

            then (((a |^ ((n - 1) / q)) - (a |^ ((n - 1) / q))),(( - 1) - 1)) are_congruent_mod m by A23, INT_1: 17;

            then (( 0 + 1),(( - 2) + 1)) are_congruent_mod m;

            then

             A25: m = 2 or m = 1 or m = ( - 2) or m = ( - 1) by Th20, INT_1: 14;

             A26:

            now

              assume ( - 2) divides n;

              then

              consider g be Integer such that

               A27: n = (( - 2) * g);

              n = (2 * ( - g)) by A27;

              hence contradiction;

            end;

            (1 * 1) = 1 & (( - 1) * ( - 1)) = 1;

            hence m divides 1 by A26, A22, A25;

          end;

          hence (((a |^ ((n - 1) / q)) - 1) gcd n) = 1 by A20, A21, INT_2:def 2;

        end;

        hence n is prime by A4, A5, INT_1: 18, A6, A11, Th21;

      end;

      now

        assume n is prime;

        then

        reconsider m = n as prime Proth natural number;

        ( Z/Z* m) is cyclic by INT_7: 31;

        then

        consider g be Element of ( Z/Z* m) such that

         A28: ( ord g) = ( card ( Z/Z* m)) by GR_CY_1: 19;

        

         A29: ( ord g) = (m - 1) by A28, INT_7: 23;

        ( Z/Z* m) = multMagma (# ( Segm0 m), ( multint0 m) #) by INT_7:def 4;

        then

        reconsider g1 = g as natural number;

        

         A30: not (g is being_of_order_0) by A28, GROUP_1:def 11;

        

         A31: ((g1 |^ (m - 1)) mod m) = (g |^ (m - 1)) by Th17

        .= ( 1_ ( Z/Z* m)) by A29, A30, GROUP_1:def 11

        .= 1 by INT_7: 21;

        

         A32: ((g1 |^ (m - 1)),1) are_congruent_mod m by Th10, A31;

        

         A33: ((g1 |^ ((m - 1) / 2)) |^ (1 + 1)) = (((g1 |^ ((m - 1) / 2)) |^ 1) * (g1 |^ ((m - 1) / 2))) by NEWTON: 6

        .= ((g1 |^ ((m - 1) / 2)) * (g1 |^ ((m - 1) / 2)))

        .= (g1 |^ (((m - 1) / 2) + ((m - 1) / 2))) by NEWTON: 8

        .= (g1 |^ (m - 1));

        now

          assume

           A34: ((g1 |^ ((m - 1) / 2)),1) are_congruent_mod n;

          

           A35: ( 1_ ( Z/Z* m)) = 1 by INT_7: 21

          .= ((g1 |^ ((m - 1) / 2)) mod m) by A34, INT_2:def 4, Th12

          .= (g |^ ((m - 1) / 2)) by Th17;

          

           A36: (m - 1) <> 0 ;

          ((m - 1) * 2) >= ((m - 1) * 1) & 0 < 2 by XREAL_1: 64;

          then

           A37: ((m - 1) / 2) <= (m - 1) by XREAL_1: 79;

          (m - 1) <= ((m - 1) / 2) by A29, A30, A35, GROUP_1:def 11;

          then (m - 1) = ((m - 1) / 2) by A37, XXREAL_0: 1;

          hence contradiction by A36;

        end;

        hence ex a be natural number st ((a |^ ((n - 1) / 2)),( - 1)) are_congruent_mod n by A33, A32, Th18;

      end;

      hence thesis by A3;

    end;

    theorem :: NAT_6:41

    

     Th41: for l be 2 _or_greater natural number, k be positive natural number st not (3 divides k) & k <= ((2 |^ l) - 1) holds ((k * (2 |^ l)) + 1) is prime iff ((3 |^ (k * (2 |^ (l - 1)))),( - 1)) are_congruent_mod ((k * (2 |^ l)) + 1)

    proof

      let l be 2 _or_greater natural number, k be positive natural number;

      assume

       A1: not 3 divides k & k <= ((2 |^ l) - 1);

      set s = (2 |^ l), a = 3, n = ((k * (2 |^ l)) + 1);

      k >= 1 by NAT_1: 14;

      then (k * (2 |^ l)) >= (1 * (2 |^ l)) by XREAL_1: 66;

      then

       A2: n >= ((2 |^ l) + 1) by XREAL_1: 7;

      

       A3: ((2 |^ l) / 2) = ((2 |^ ((l - 1) + 1)) * (2 " ))

      .= (((2 |^ (l - 1)) * 2) * (2 " )) by NEWTON: 6

      .= ((2 |^ (l - 1)) * 1);

      

       A4: (2 * (k * (2 |^ (l - 1)))) = (k * (2 * (2 |^ (l - 1))))

      .= (k * (2 |^ ((l - 1) + 1))) by NEWTON: 6;

      

       A5: l >= 1 by NAT_1: 14;

      

       A6: (l + 1) >= (1 + 1) by NAT_1: 14, XREAL_1: 6;

      

       A7: (2 |^ l) >= (l + 1) by NEWTON: 85;

      then (2 |^ l) >= (1 + 1) by A6, XXREAL_0: 2;

      then ((2 |^ l) + 1) >= (2 + 1) by XREAL_1: 7;

      then n >= (2 + 1) by A2, XXREAL_0: 2;

      then n > 2 by NAT_1: 13;

      then

      reconsider n as 2 _greater odd natural number by A4, Def1;

      (2 * (k * (2 |^ (l - 1)))) = (k * (2 * (2 |^ (l - 1))))

      .= (k * (2 |^ ((l - 1) + 1))) by NEWTON: 6;

      then

      reconsider k2 = ((k * (2 |^ l)) / 2) as natural number;

      

       A8: (3 |^ ((n - 1) / 2)) = (3 |^ (k * (2 |^ (l - 1)))) by A3;

       A9:

      now

        assume

         A10: ((3 |^ (k * (2 |^ (l - 1)))),( - 1)) are_congruent_mod ((k * (2 |^ l)) + 1);

        reconsider s as Divisor of (n - 1) by INT_2: 2, Def2;

        s <> 0 & s <> 1 by A7, A6, XXREAL_0: 2;

        then

        reconsider s as non trivial Divisor of (n - 1) by NAT_2:def 1;

        

         A11: (((3 |^ (k * (2 |^ (l - 1)))) * (3 |^ (k * (2 |^ (l - 1))))),(( - 1) * ( - 1))) are_congruent_mod n by A10, INT_1: 18;

        

         A12: ((3 |^ (k * (2 |^ (l - 1)))) * (3 |^ (k * (2 |^ (l - 1))))) = (3 |^ ((k * (2 |^ (l - 1))) + (k * (2 |^ (l - 1))))) by NEWTON: 8

        .= (3 |^ (k * ((2 |^ (l - 1)) * 2)))

        .= (3 |^ (k * (2 |^ ((l - 1) + 1)))) by NEWTON: 6

        .= (3 |^ (k * (2 |^ l)));

        

         A13: (k * (2 |^ l)) <= (((2 |^ l) - 1) * (2 |^ l)) by A1, XREAL_1: 64;

        

         A14: ((((2 |^ l) - 1) * (2 |^ l)) + 1) = ((((2 |^ l) * (2 |^ l)) - (2 |^ l)) + 1)

        .= (((2 |^ (l + l)) - (2 |^ l)) + 1) by NEWTON: 8;

        then n <= (((2 |^ (l + l)) - (2 |^ l)) + 1) by A13, XREAL_1: 6;

        then

         A15: n < ((((2 |^ (l + l)) - (2 |^ l)) + 1) + 1) by A14, NAT_1: 13;

        

         A16: s > ( sqrt n)

        proof

          per cases ;

            suppose l >= 2;

            then

             A17: (2 |^ l) >= (2 |^ 2) by Th1;

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

            .= (2 * 2);

            then (2 |^ l) > 2 by A17, XXREAL_0: 2;

            then (2 - (2 |^ l)) < ((2 |^ l) - (2 |^ l)) by XREAL_1: 9;

            then ((2 |^ (l + l)) + (( - (2 |^ l)) + 2)) < ((2 |^ (l + l)) + 0 ) by XREAL_1: 6;

            then

             A18: n < (2 |^ (2 * l)) by A15, XXREAL_0: 2;

            ((2 |^ l) ^2 ) = (2 |^ (l + l)) by NEWTON: 8;

            then ( sqrt (2 |^ (2 * l))) = (2 |^ l) by SQUARE_1:def 2;

            hence thesis by A18, SQUARE_1: 27;

          end;

            suppose l < 2;

            then l < (1 + 1);

            then l <= 1 by NAT_1: 13;

            then

             A19: l = 1 by A5, XXREAL_0: 1;

            then

             A20: n = ((k * 2) + 1);

            

             A21: k <= (2 - 1) by A1, A19;

            k >= 1 by NAT_1: 14;

            then k = 1 by A21, XXREAL_0: 1;

            hence thesis by A20, SQUARE_1: 27, SQUARE_1: 20;

          end;

        end;

        now

          let q be prime Divisor of s;

          

           A22: ((a |^ ((n - 1) / q)),( - 1)) are_congruent_mod n by A8, A10, Th8, INT_2: 28, Def2;

          (1 * ((a |^ ((n - 1) / q)) - 1)) = ((a |^ ((n - 1) / q)) - 1);

          then

           A23: 1 divides ((a |^ ((n - 1) / q)) - 1);

          (1 * n) = n;

          then

           A24: 1 divides n;

          now

            let m be Integer;

            assume

             A25: m divides ((a |^ ((n - 1) / q)) - 1) & m divides n;

            then

             A26: ((a |^ ((n - 1) / q)),1) are_congruent_mod m;

            consider j be Integer such that

             A27: (m * j) = n by A25;

            ((a |^ ((n - 1) / q)),( - 1)) are_congruent_mod m by A22, A27, INT_1: 20;

            then (((a |^ ((n - 1) / q)) - (a |^ ((n - 1) / q))),(( - 1) - 1)) are_congruent_mod m by A26, INT_1: 17;

            then (( 0 + 1),(( - 2) + 1)) are_congruent_mod m;

            then m = 2 or m = 1 or m = ( - 2) or m = ( - 1) by Th20, INT_1: 14;

            hence m divides 1 by A25, INT_2: 10, ABIAN:def 1;

          end;

          hence (((a |^ ((n - 1) / q)) - 1) gcd n) = 1 by A23, A24, INT_2:def 2;

        end;

        hence ((k * (2 |^ l)) + 1) is prime by A12, A11, A16, Th21;

      end;

      now

        assume n is prime;

        then

        reconsider n as 2 _greater prime natural number;

        reconsider two = 2 as prime natural number by INT_2: 28;

        reconsider three = 3 as 2 _greater prime natural number by Def1, PEPIN: 41;

        

         A28: ((2 |^ l) + 1) >= ((2 |^ 2) + 1) by XREAL_1: 6, EC_PF_2:def 1;

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

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

        .= (2 * 2);

        then

         A29: 3 <> n by A28, A2, XXREAL_0: 2;

        

         A30: not ((n, 0 ) are_congruent_mod 3) by A29, INT_2:def 4;

         A31:

        now

          assume

           A32: (n,1) are_congruent_mod 3;

           not (three divides (2 |^ l)) by Th8, INT_2: 28;

          then (3 gcd (2 |^ l)) = 1 by Th6;

          hence contradiction by A1, INT_2: 25, A32, INT_2:def 3;

        end;

        (n, 0 ) are_congruent_mod 3 or ... or (n,(3 - 1)) are_congruent_mod 3 by Th13;

        then

         A33: (n, 0 ) are_congruent_mod 3 or ... or (n,2) are_congruent_mod 3;

        

         A34: (2,(2 + 1)) are_coprime by PEPIN: 1;

         not (three divides n) by A29, INT_2:def 4;

        then

         A35: (n gcd 3) = 1 by Th6;

        

         A36: (((3 - 1) / 2) * ((n - 1) / 2)) = (1 * ((n - 1) / 2));

        ((n - 1) / 2) = ((k * (2 |^ ((l - 1) + 1))) / 2)

        .= ((k * ((2 |^ (l - 1)) * 2)) / 2) by NEWTON: 6

        .= (k * (2 |^ ((l - 2) + 1)))

        .= (k * ((2 |^ (l - 2)) * 2)) by NEWTON: 6

        .= ((2 * k) * (2 |^ (l - 2)));

        then

         A37: (( - 1) |^ ((n - 1) / 2)) = 1;

        (( Leg (three,n)) * ( Leg (n,three))) = 1 by A36, A37, A29, Th30;

        then ( Leg (three,n)) = 1 & ( Leg (n,three)) = 1 or ( Leg (three,n)) = ( - 1) & ( Leg (n,three)) = ( - 1) by INT_1: 9;

        

        then ( Leg (3,n)) = ( Leg (two,three)) by A35, A33, A30, A31, A34, Th28

        .= ( - 1) by Th23, A34, Def4;

        hence ((3 |^ (k * (2 |^ (l - 1)))),( - 1)) are_congruent_mod ((k * (2 |^ l)) + 1) by A8, A35, Th31;

      end;

      hence thesis by A9;

    end;

    theorem :: NAT_6:42

    641 is prime

    proof

      641 = ((2 * 320) + 1);

      then

      reconsider n = 641 as odd natural number;

      

       A1: (256 + 64) = 320;

      

       A2: (3 * 3) = ((3 |^ 1) * 3)

      .= ((3 |^ 1) * (3 |^ 1))

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

      

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

      

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

      6561 = ((10 * 641) + 151);

      then ((3 |^ 8),151) are_congruent_mod 641 by A4, A3, A2;

      then (((3 |^ 8) * (3 |^ 8)),(151 * 151)) are_congruent_mod 641 by INT_1: 18;

      then

       A5: ((3 |^ (8 + 8)),22801) are_congruent_mod 641 by NEWTON: 8;

      22801 = ((35 * 641) + 366);

      then (22801,366) are_congruent_mod 641;

      then ((3 |^ 16),366) are_congruent_mod 641 by A5, INT_1: 15;

      then

       A6: (((3 |^ 16) * (3 |^ 16)),(366 * 366)) are_congruent_mod 641 by INT_1: 18;

      

       A7: (183,183) are_congruent_mod 641 by INT_1: 11;

      (732,91) are_congruent_mod 641;

      then ((732 * 183),(91 * 183)) are_congruent_mod 641 by A7, INT_1: 18;

      then (((3 |^ 16) * (3 |^ 16)),(91 * 183)) are_congruent_mod 641 by A6, INT_1: 15;

      then

       A8: ((3 |^ (16 + 16)),(91 * 183)) are_congruent_mod 641 by NEWTON: 8;

      16653 = ((26 * 641) + ( - 13));

      then (16653,( - 13)) are_congruent_mod 641;

      then ((3 |^ 32),( - 13)) are_congruent_mod 641 by A8, INT_1: 15;

      then (((3 |^ 32) * (3 |^ 32)),(( - 13) * ( - 13))) are_congruent_mod 641 by INT_1: 18;

      then

       A9: ((3 |^ (32 + 32)),169) are_congruent_mod 641 by NEWTON: 8;

      then

       A10: (((3 |^ 64) * (3 |^ 64)),(169 * 169)) are_congruent_mod 641 by INT_1: 18;

      28561 = ((44 * 641) + 357);

      then (28561,357) are_congruent_mod 641;

      then (((3 |^ 64) * (3 |^ 64)),357) are_congruent_mod 641 by A10, INT_1: 15;

      then ((3 |^ (64 + 64)),357) are_congruent_mod 641 by NEWTON: 8;

      then

       A11: (((3 |^ 128) * (3 |^ 128)),(357 * 357)) are_congruent_mod 641 by INT_1: 18;

      

       A12: (119,119) are_congruent_mod 641 by INT_1: 11;

      (1071,430) are_congruent_mod 641;

      then ((1071 * 119),(430 * 119)) are_congruent_mod 641 by A12, INT_1: 18;

      then (((3 |^ 128) * (3 |^ 128)),(430 * 119)) are_congruent_mod 641 by A11, INT_1: 15;

      then

       A13: ((3 |^ (128 + 128)),(3010 * 17)) are_congruent_mod 641 by NEWTON: 8;

      

       A14: (17,17) are_congruent_mod 641 by INT_1: 11;

      3010 = ((4 * 641) + 446);

      then (3010,446) are_congruent_mod 641;

      then ((3010 * 17),(446 * 17)) are_congruent_mod 641 by A14, INT_1: 18;

      then

       A15: ((3 |^ (128 + 128)),(446 * 17)) are_congruent_mod 641 by A13, INT_1: 15;

      7582 = ((12 * 641) + ( - 110));

      then (7582,( - 110)) are_congruent_mod 641;

      then ((3 |^ 256),( - 110)) are_congruent_mod 641 by A15, INT_1: 15;

      then (((3 |^ 256) * (3 |^ 64)),(( - 110) * 169)) are_congruent_mod 641 by A9, INT_1: 18;

      then

       A16: ((3 |^ 320),( - 18590)) are_congruent_mod 641 by A1, NEWTON: 8;

      

       A17: ( - 18590) = ((( - 30) * 641) + 640);

      

       A18: (640,( - 1)) are_congruent_mod 641;

      (( - 18590),640) are_congruent_mod 641 by A17;

      then (( - 18590),( - 1)) are_congruent_mod 641 by A18, INT_1: 15;

      then ex a be natural number st ((a |^ ((n - 1) / 2)),( - 1)) are_congruent_mod n by A16, INT_1: 15;

      hence thesis by Th40, Th37;

    end;

    begin

    registration

      let l be natural number;

      cluster ( Fermat l) -> Proth;

      coherence

      proof

        reconsider p = ( Fermat l) as natural number;

        set k = 1, n = (2 |^ l);

        

         A3: (2 |^ n) > n by NEWTON: 86;

        (n + 1) > ( 0 + 1) by XREAL_1: 6;

        then n >= 1 by NAT_1: 13;

        then

         A1: (2 |^ n) > k by A3, XXREAL_0: 2;

        

         A2: ((2 * 0 ) + 1) = 1;

        p = ((k * (2 |^ n)) + 1) by PEPIN:def 3;

        hence thesis by A1, A2;

      end;

    end

    ::$Notion-Name

    theorem :: NAT_6:43

    for l be non zero natural number holds ( Fermat l) is prime iff ((3 |^ ((( Fermat l) - 1) / 2)),( - 1)) are_congruent_mod ( Fermat l)

    proof

      let l be non zero natural number;

      set k = 1;

      

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

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

      .= (2 * 2);

      (l + 1) >= ( 0 + 1) by XREAL_1: 6;

      then l >= 1 by NAT_1: 13;

      then (2 |^ l) >= (2 |^ 1) by Th1;

      then (2 |^ l) >= 2;

      then

      reconsider l1 = (2 |^ l) as 2 _or_greater natural number by EC_PF_2:def 1;

      

       A2: not (3 divides k) by INT_2: 27;

      ((2 |^ l1) - 1) >= (4 - 1) by A1, XREAL_1: 9, EC_PF_2:def 1;

      then

       A3: 1 <= ((2 |^ l1) - 1) by XXREAL_0: 2;

      

       A4: ((k * (2 |^ l1)) + 1) = ( Fermat l) by PEPIN:def 3;

      ((( Fermat l) - 1) / 2) = ((((2 |^ (2 |^ l)) + 1) - 1) / 2) by PEPIN:def 3

      .= ((2 |^ ((l1 - 1) + 1)) / 2)

      .= (((2 |^ (l1 - 1)) * 2) / 2) by NEWTON: 6

      .= (k * (2 |^ (l1 - 1)));

      hence thesis by A2, A3, A4, Th41;

    end;

    theorem :: NAT_6:44

    ( Fermat 5) is non prime

    proof

      

       A1: ((2 |^ 7) * (2 |^ 7)) = (2 |^ (7 + 7)) by NEWTON: 8;

      

       A2: (5 * 5) = ((5 |^ 1) * 5)

      .= ((5 |^ 1) * (5 |^ 1))

      .= (5 |^ (1 + 1)) by NEWTON: 8;

      

       A3: ((5 |^ 2) * (5 |^ 2)) = (5 |^ (2 + 2)) by NEWTON: 8;

      

       A4: ((2 |^ 14) * (2 |^ 14)) = (2 |^ (14 + 14)) by NEWTON: 8;

      

       A5: ((2 |^ 4) * (2 |^ 28)) = (2 |^ (4 + 28)) by NEWTON: 8;

      

       A6: (2 |^ 2) = (2 |^ (1 + 1))

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

      .= (2 * 2);

      

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

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

      .= 8 by A6;

      

       A8: (2 |^ 4) = (2 |^ (3 + 1))

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

      .= 16 by A7;

      

       A9: (2 |^ (3 + 4)) = (8 * 16) by A8, A7, NEWTON: 8;

      ((5 * (2 |^ 7)),( - 1)) are_congruent_mod 641 by A9;

      then (((5 * (2 |^ 7)) * (5 * (2 |^ 7))),(( - 1) * ( - 1))) are_congruent_mod 641 by INT_1: 18;

      then

       A10: ((((5 |^ 2) * (2 |^ 14)) * ((5 |^ 2) * (2 |^ 14))),(1 * 1)) are_congruent_mod 641 by A1, A2, INT_1: 18;

      ((((5 |^ 4) + (2 |^ 4)) - (2 |^ 4)),( 0 - (2 |^ 4))) are_congruent_mod 641 by A2, A3, A8;

      then

       A11: (( - (2 |^ 4)),(5 |^ 4)) are_congruent_mod 641 by INT_1: 14;

      ((2 |^ 28),(2 |^ 28)) are_congruent_mod 641 by INT_1: 11;

      then ((( - (2 |^ 4)) * (2 |^ 28)),((5 |^ 4) * (2 |^ 28))) are_congruent_mod 641 by A11, INT_1: 18;

      then

       A12: (( - (2 |^ 32)),1) are_congruent_mod 641 by A3, A4, A5, A10, INT_1: 15;

      (( - 1),( - 1)) are_congruent_mod 641 by INT_1: 11;

      then

       A13: ((( - 1) * ( - (2 |^ 32))),(( - 1) * 1)) are_congruent_mod 641 by A12, INT_1: 18;

      

       A14: ((5 * (2 |^ 7)) + 1) = 641 by A9;

      (2 |^ (4 + 1)) = (16 * 2) by A8, NEWTON: 6;

      then

       A15: ( Fermat 5) = ((2 |^ 32) + 1) by PEPIN:def 3;

      (5 * (2 |^ 7)) < ((2 |^ 3) * (2 |^ 7)) by A7, XREAL_1: 68;

      then

       A16: (5 * (2 |^ 7)) < (2 |^ (3 + 7)) by NEWTON: 8;

      2 is non trivial;

      then (2 |^ 10) < (2 |^ 32) by Th2;

      then (5 * (2 |^ 7)) < (2 |^ 32) by A16, XXREAL_0: 2;

      then 641 < ((2 |^ 32) + 1) by A14, XREAL_1: 6;

      hence thesis by A15, A13;

    end;

    begin

    ::$Notion-Name

    definition

      let n be natural number;

      :: NAT_6:def6

      func CullenNumber n -> natural number equals ((n * (2 |^ n)) + 1);

      coherence ;

    end

    registration

      let n be non zero natural number;

      cluster ( CullenNumber n) -> Proth;

      coherence

      proof

        consider k be natural number, l be odd natural number such that

         A1: n = (l * (2 |^ k)) by Th3;

        

         A2: ((n * (2 |^ n)) + 1) = ((l * ((2 |^ k) * (2 |^ n))) + 1) by A1

        .= ((l * (2 |^ (k + n))) + 1) by NEWTON: 8;

        ((2 |^ k) + 1) > ( 0 + 1) by XREAL_1: 6;

        then (2 |^ k) >= 1 by NAT_1: 13;

        then

         A3: ((2 |^ k) * l) >= (1 * l) by XREAL_1: 64;

        

         A4: (2 |^ (k + n)) > (k + n) by NEWTON: 86;

        (k + n) >= n by NAT_1: 11;

        then (k + n) >= l by A1, A3, XXREAL_0: 2;

        then (2 |^ (k + n)) > l by A4, XXREAL_0: 2;

        hence thesis by A2;

      end;

    end