newton03.miz



    begin

    reserve a,b,c,d,x,j,k,l,m,n,o,xi,xj for Nat,

p,q,t,z,u,v for Integer,

a1,b1,c1,d1 for Complex;

    theorem :: NEWTON03:1

    ((a1 |^ (n + k)) + (b1 |^ (n + k))) = (((a1 |^ n) * ((a1 |^ k) + (b1 |^ k))) + ((b1 |^ k) * ((b1 |^ n) - (a1 |^ n))))

    proof

      (a1 |^ (n + k)) = ((a1 |^ n) * (a1 |^ k)) & (b1 |^ (n + k)) = ((b1 |^ n) * (b1 |^ k)) by NEWTON: 8;

      hence thesis;

    end;

    theorem :: NEWTON03:2

    

     RI2: ((a1 |^ (n + k)) - (b1 |^ (n + k))) = (((a1 |^ n) * ((a1 |^ k) - (b1 |^ k))) + ((b1 |^ k) * ((a1 |^ n) - (b1 |^ n))))

    proof

      (a1 |^ (n + k)) = ((a1 |^ n) * (a1 |^ k)) & (b1 |^ (n + k)) = ((b1 |^ n) * (b1 |^ k)) by NEWTON: 8;

      hence thesis;

    end;

    theorem :: NEWTON03:3

    

     RI3: ((a1 |^ (m + 2)) + (b1 |^ (m + 2))) = (((a1 + b1) * ((a1 |^ (m + 1)) + (b1 |^ (m + 1)))) - ((a1 * b1) * ((a1 |^ m) + (b1 |^ m))))

    proof

      (a1 |^ ((m + 1) + 1)) = (a1 * (a1 |^ (m + 1))) & (b1 |^ ((m + 1) + 1)) = (b1 * (b1 |^ (m + 1))) & (a1 |^ (m + 1)) = (a1 * (a1 |^ m)) & (b1 |^ (m + 1)) = (b1 * (b1 |^ m)) by NEWTON: 6;

      hence thesis;

    end;

    definition

      let a be Nat;

      :: original: trivial

      redefine

      :: NEWTON03:def1

      attr a is trivial means

      : Def0: a <= 1;

      compatibility

      proof

        a <= 1 implies a = 1 or a < 1 by XXREAL_0: 1;

        hence thesis by NAT_2:def 1, NAT_1: 14;

      end;

    end

    definition

      let a be Complex;

      :: original: ^2

      redefine

      :: NEWTON03:def2

      func a ^2 -> set equals (a |^ 2);

      correctness by NEWTON: 81;

    end

    definition

      let a,b be Integer;

      :: original: gcd

      redefine

      :: NEWTON03:def3

      func a gcd b -> Nat equals ( |.a.| gcd |.b.|);

      correctness by INT_2: 34;

      :: original: lcm

      redefine

      :: NEWTON03:def4

      func a lcm b -> Nat equals

      : Def2: ( |.a.| lcm |.b.|);

      correctness by INT_2: 33;

    end

    registration

      let a,b be positive Real;

      cluster ( max (a,b)) -> positive;

      coherence by XXREAL_0:def 10;

      cluster ( min (a,b)) -> positive;

      coherence by XXREAL_0:def 9;

    end

    registration

      let a be non zero Integer, b be Integer;

      cluster (a gcd b) -> non zero;

      coherence by INT_2: 5;

    end

    registration

      let a be non zero Complex, n be Nat;

      cluster (a |^ n) -> non zero;

      coherence by PREPOWER: 5;

    end

    registration

      let a be non trivial Nat, n be non zero Nat;

      cluster (a |^ n) -> non trivial;

      coherence

      proof

        reconsider m = (n - 1) as Nat;

        (a |^ (m + 1)) = (a * (a |^ m)) & a > 1 by NEWTON: 6, Def0;

        then (a |^ (m + 1)) > (1 * (a |^ m)) & (a |^ m) >= 1 by XREAL_1: 68, NAT_1: 14;

        hence thesis by XXREAL_0: 2;

      end;

    end

    registration

      let a be Integer;

      cluster |.a.| -> natural;

      coherence ;

    end

    registration

      let a be even Integer;

      cluster |.a.| -> even;

      coherence

      proof

        2 divides a iff |.2.| divides |.a.| by INT_2: 16;

        hence thesis by ABIAN:def 1;

      end;

    end

    registration

      let a be Nat;

      reduce (a lcm a) to a;

      reducibility by NAT_D: 31;

      reduce (a gcd a) to a;

      reducibility by NAT_D: 32;

    end

    registration

      let a be non zero Integer, b be Integer;

      cluster (a gcd b) -> positive;

      coherence ;

    end

    registration

      let a,b be Integer;

      reduce (a gcd (a gcd b)) to (a gcd b);

      correctness

      proof

        (a gcd (a gcd b)) = ((a gcd a) gcd b) by INT_6: 18

        .= (( |.a.| gcd |.a.|) gcd b) by INT_2: 34;

        hence thesis by INT_6: 14;

      end;

      reduce (a lcm (a lcm b)) to (a lcm b);

      correctness

      proof

        (a lcm (a lcm b)) = ( |.a.| lcm |.(a lcm b).|) by INT_2: 33

        .= ( |.a.| lcm ( |.a.| lcm |.b.|)) by INT_2: 33

        .= (( |.a.| lcm |.a.|) lcm |.b.|) by NEWTON: 43

        .= (a lcm b) by INT_2: 33;

        hence thesis;

      end;

    end

    registration

      let a be Integer;

      reduce (a gcd 1) to 1;

      reducibility

      proof

        

         A1: a = |.a.| or ( - a) = |.a.| by ABSVALUE:def 1;

        ( |.a.| gcd 1) = 1 by NEWTON: 51;

        hence thesis by A1, NEWTON02: 1;

      end;

      reduce ((a + 1) gcd a) to 1;

      reducibility

      proof

        (((1 * a) + 1) gcd a) = (1 gcd a) by NEWTON02: 5;

        hence thesis;

      end;

    end

    theorem :: NEWTON03:4

    

     NEWTON027: for t,z be Integer holds ((t |^ n) gcd (z |^ n)) = ((t gcd z) |^ n)

    proof

      let t,z be Integer;

      

       A1: ((t |^ n) gcd (z |^ n)) = ( |.(t |^ n).| gcd |.(z |^ n).|) & (t gcd z) = ( |.t.| gcd |.z.|) by INT_2: 34;

       |.(t |^ n).| = ( |.t.| |^ n) & |.(z |^ n).| = ( |.z.| |^ n) by TAYLOR_2: 1;

      hence thesis by A1, NEWTON02: 7;

    end;

    registration

      let a be Integer, n be Nat;

      reduce (((a + 1) |^ n) gcd (a |^ n)) to 1;

      reducibility

      proof

        (1 |^ n) = ((a gcd (a + 1)) |^ n);

        hence thesis by NEWTON027;

      end;

    end

    registration

      let a1, b1;

      reduce ((a1 |^ 0 ) - (b1 |^ 0 )) to 0 ;

      reducibility

      proof

        ((1 * (a1 |^ 0 )) - (1 * (b1 |^ 0 ))) = 0 ;

        hence thesis;

      end;

    end

    registration

      let a be non negative Real, n be Nat;

      cluster (a |^ n) -> non negative;

      coherence

      proof

        (a |^ n) >= ( 0 |^ n) by NEWTON02: 41;

        hence thesis;

      end;

    end

    registration

      cluster non trivial for odd Nat;

      existence

      proof

        3 is non trivial & ((2 * 1) + 1) is odd;

        hence thesis;

      end;

      cluster non trivial for even Nat;

      existence

      proof

        2 is non trivial & (2 * 1) is even;

        hence thesis;

      end;

    end

    registration

      let a be positive Real, n be Nat;

      cluster (a |^ n) -> positive;

      coherence ;

    end

    registration

      let a be Integer;

      cluster (a * a) -> square;

      coherence

      proof

        reconsider b = |.a.| as Nat;

        b = a or b = ( - a) by COMPLEX1: 71;

        then (b * b) = (a * a) or (b * b) = (( - a) * ( - a));

        then (a * a) = (b ^2 ) by SQUARE_1:def 1;

        hence thesis;

      end;

      cluster (a / a) -> square;

      coherence

      proof

        per cases ;

          suppose a is zero;

          then (a / a) = ( 0 ^2 );

          hence thesis;

        end;

          suppose a is non zero;

          then (a / a) = (1 ^2 ) by XCMPLX_1: 60;

          hence thesis;

        end;

      end;

    end

    registration

      cluster non square for Element of NAT ;

      existence

      proof

         not 3 is square by PEPIN: 41;

        hence thesis;

      end;

    end

    registration

      cluster prime -> non square for Element of NAT ;

      coherence ;

    end

    registration

      cluster even for prime Nat;

      correctness

      proof

        2 is even & 2 is prime by INT_2: 28;

        hence thesis;

      end;

      cluster odd for prime Nat;

      correctness

      proof

        ((2 * 1) + 1) is odd & 3 is prime by PEPIN: 41;

        hence thesis;

      end;

    end

    registration

      cluster prime -> non square for Integer;

      coherence

      proof

        let p be Integer;

        assume p is prime;

        then

        reconsider p as non square Element of NAT by ORDINAL1:def 12;

        p is non square;

        hence thesis;

      end;

    end

    registration

      let a be square Element of NAT ;

      cluster ( sqrt a) -> natural;

      coherence

      proof

        reconsider a as Nat;

        consider m be Nat such that

         A0: (m ^2 ) = a by PYTHTRIP:def 3;

        thus thesis by A0, SQUARE_1:def 2;

      end;

    end

    registration

      let a be Integer;

      cluster (a |^ 2) -> square;

      coherence

      proof

        (a |^ 2) = (a ^2 )

        .= ( |.a.| ^2 ) by COMPLEX1: 75;

        hence thesis;

      end;

      cluster (a * a) -> square;

      coherence ;

    end

    registration

      cluster non square for Integer;

      existence by INT_2: 28;

    end

    registration

      cluster zero -> trivial for Nat;

      correctness ;

    end

    registration

      cluster square for Nat;

      existence

      proof

        ( 0 * 0 ) = ( 0 ^2 );

        hence thesis;

      end;

    end

    registration

      cluster non zero for Element of NAT ;

      existence by INT_2: 28;

      cluster non trivial for square Element of NAT ;

      existence

      proof

        

         A1: (2 ^2 ) = (2 * 2) by SQUARE_1:def 1;

        4 is non trivial Element of NAT by NAT_2:def 1;

        hence thesis by A1;

      end;

    end

    registration

      cluster trivial -> square for Nat;

      coherence

      proof

        (1 * 1) = (1 ^2 ) & ( 0 * 0 ) = ( 0 ^2 );

        hence thesis by NAT_2:def 1;

      end;

    end

    registration

      cluster non square -> non zero for Integer;

      coherence ;

    end

    theorem :: NEWTON03:5

    

     NAT31: for a,b,c,d be Integer holds a divides b & c divides d implies (a * c) divides (b * d)

    proof

      let a,b,c,d be Integer;

      assume a divides b & c divides d;

      then |.a.| divides |.b.| & |.c.| divides |.d.| by INT_2: 16;

      then

       A2: ( |.a.| * |.c.|) divides ( |.b.| * |.d.|) by NAT_3: 1;

       |.(a * c).| = ( |.a.| * |.c.|) & |.(b * d).| = ( |.b.| * |.d.|) by COMPLEX1: 65;

      hence thesis by A2, INT_2: 16;

    end;

    theorem :: NEWTON03:6

    

     LCM1: for a,b be Integer holds a divides b iff (a lcm b) = |.b.|

    proof

      let a,b be Integer;

      thus a divides b implies (a lcm b) = |.b.|

      proof

        assume a divides b;

        then |.b.| = ( |.a.| lcm |.b.|) by INT_2: 16, NEWTON: 44;

        hence thesis by Def2;

      end;

      assume (a lcm b) = |.b.|;

      then ( |.a.| lcm |.b.|) = |.b.| by Def2;

      hence thesis by NEWTON: 44, INT_2: 16;

    end;

    registration

      let a be Integer;

      reduce (a lcm 0 ) to 0 ;

      reducibility by INT_2: 4;

    end

    registration

      let a be Nat;

      reduce (a lcm 1) to a;

      reducibility by NEWTON: 46;

    end

    registration

      let a, b;

      reduce ((a * b) lcm a) to (a * b);

      reducibility

      proof

        a divides (a * b);

        then (a lcm (a * b)) = |.(a * b).| by LCM1;

        hence thesis;

      end;

      reduce ((a gcd b) lcm b) to b;

      reducibility by NEWTON: 53;

      reduce (a gcd (a lcm b)) to a;

      reducibility by NEWTON: 54;

    end

    theorem :: NEWTON03:7

    

     NATD29: for a,b be Integer holds |.(a * b).| = ((a gcd b) * (a lcm b))

    proof

      let a,b be Integer;

       |.(a * b).| = ( |.a.| * |.b.|) by COMPLEX1: 65

      .= (( |.a.| gcd |.b.|) * ( |.a.| lcm |.b.|)) by NAT_D: 29

      .= ((a gcd b) * ( |.a.| lcm |.b.|)) by INT_2: 34

      .= ((a gcd b) * (a lcm b)) by INT_2: 33;

      hence thesis;

    end;

    theorem :: NEWTON03:8

    

     LmLCM: for a,b be Integer holds ((a |^ n) lcm (b |^ n)) = ((a lcm b) |^ n)

    proof

      let a,b be Integer;

      

       A2: ((a |^ n) gcd (b |^ n)) = ((a gcd b) |^ n) by NEWTON027;

      

       A3: |.((a |^ n) * (b |^ n)).| = (((a |^ n) gcd (b |^ n)) * ((a |^ n) lcm (b |^ n))) & |.(a * b).| = ((a gcd b) * (a lcm b)) by NATD29;

      

      then

       A4: (((a |^ n) gcd (b |^ n)) * ((a |^ n) lcm (b |^ n))) = |.((a * b) |^ n).| by NEWTON: 7

      .= (((a gcd b) * (a lcm b)) |^ n) by A3, TAYLOR_2: 1

      .= (((a gcd b) |^ n) * ((a lcm b) |^ n)) by NEWTON: 7

      .= (((a |^ n) gcd (b |^ n)) * ((a lcm b) |^ n)) by NEWTON027;

      per cases ;

        suppose (a gcd b) = 0 ;

        then a = 0 & b = 0 ;

        hence thesis;

      end;

        suppose (a gcd b) <> 0 ;

        hence thesis by A2, A4, XCMPLX_1: 5;

      end;

    end;

    registration

      let a be square Element of NAT , b be square Element of NAT ;

      cluster (a gcd b) -> square;

      coherence

      proof

        reconsider t = ( sqrt a) as Element of NAT by ORDINAL1:def 12;

        reconsider q = ( sqrt b) as Element of NAT by ORDINAL1:def 12;

        

         A1: (t ^2 ) = a & (q ^2 ) = b by SQUARE_1:def 2;

        ((t ^2 ) gcd (q ^2 )) = ((t gcd q) ^2 ) by NEWTON02: 7;

        hence thesis by A1;

      end;

      cluster (a lcm b) -> square;

      coherence

      proof

        reconsider t = ( sqrt a), q = ( sqrt b) as Element of NAT by ORDINAL1:def 12;

        

         A1: (t ^2 ) = a & (q ^2 ) = b by SQUARE_1:def 2;

        ((t ^2 ) lcm (q ^2 )) = ((t lcm q) ^2 ) by LmLCM;

        hence thesis by A1;

      end;

    end

    registration

      let a,b be square Integer;

      cluster (a gcd b) -> square;

      coherence

      proof

        consider x be Nat such that

         A1: a = (x ^2 ) by PYTHTRIP:def 3;

        consider y be Nat such that

         A2: b = (y ^2 ) by PYTHTRIP:def 3;

        (a gcd b) = ((x gcd y) ^2 ) by A1, A2, NEWTON02: 7;

        hence thesis;

      end;

      cluster (a lcm b) -> square;

      coherence

      proof

        consider x be Nat such that

         A1: a = (x ^2 ) by PYTHTRIP:def 3;

        consider y be Nat such that

         A2: b = (y ^2 ) by PYTHTRIP:def 3;

        (a lcm b) = ((x lcm y) ^2 ) by A1, A2, LmLCM;

        hence thesis;

      end;

    end

    theorem :: NEWTON03:9

    

     ODD: for t be Integer holds t is odd iff (t gcd 2) = 1

    proof

      let t be Integer;

      thus t is odd implies (t gcd 2) = 1

      proof

        assume t is odd;

        then

        consider z be Integer such that

         A1: t = ((2 * z) + 1) by ABIAN: 1;

        (t gcd 2) = (1 gcd (1 + (1 * 1))) by A1, NEWTON02: 5

        .= 1;

        hence thesis;

      end;

      (t gcd 2) <> |.2.| implies not 2 divides t by NEWTON02: 3;

      hence thesis;

    end;

    definition

      let t be Integer;

      :: original: odd

      redefine

      :: NEWTON03:def5

      attr t is odd means

      : Def3: (t gcd 2) = 1;

      compatibility by ODD;

    end

    registration

      let a be odd Integer;

      cluster |.a.| -> odd;

      coherence

      proof

        1 = (a gcd 2) by Def3;

        hence thesis by INT_6: 14;

      end;

      cluster ( - a) -> odd;

      coherence

      proof

        1 = ( |.a.| gcd 2) by Def3

        .= ( |.( - a).| gcd 2) by COMPLEX1: 52;

        hence thesis by INT_6: 14;

      end;

    end

    registration

      let a,b be even Integer;

      cluster (a gcd b) -> even;

      coherence by NEWTON02: 9;

    end

    registration

      let a be Integer;

      let b be odd Integer;

      cluster (a gcd b) -> odd;

      coherence by NEWTON02: 9;

    end

    registration

      let a be Nat;

      reduce |.( - a).| to a;

      reducibility

      proof

         |.( - a).| = ( - ( - a)) by ABSVALUE: 30;

        hence thesis;

      end;

    end

    registration

      let t,z be even Integer;

      cluster (t + z) -> even;

      correctness ;

      cluster (t - z) -> even;

      correctness ;

      cluster (t * z) -> even;

      correctness ;

    end

    registration

      let t,z be odd Integer;

      cluster (t + z) -> even;

      coherence ;

      cluster (t - z) -> even;

      coherence ;

      cluster (t * z) -> odd;

      coherence ;

    end

    registration

      let t be odd Integer, z be even Integer;

      cluster (t + z) -> odd;

      coherence ;

      cluster (t - z) -> odd;

      coherence ;

      cluster (t * z) -> even;

      coherence ;

    end

    theorem :: NEWTON03:10

    

     PT1: for a be non zero square Integer, b be Integer holds (a * b) is square implies b is square

    proof

      let a be non zero square Integer, b be Integer;

      assume

       A1: (a * b) is square;

      consider x be Nat such that

       A2: a = (x ^2 ) by PYTHTRIP:def 3;

      consider y be Nat such that

       A3: (a * b) = (y ^2 ) by A1, PYTHTRIP:def 3;

      (x ^2 ) divides (y ^2 ) by A2, A3;

      then |.x.| divides |.y.| by PYTHTRIP: 6;

      then

      consider k be Integer such that

       A4: y = (k * x);

      

       A5: (k * k) = (k ^2 ) & (x * x) = (x ^2 ) & (y * y) = (y ^2 ) by SQUARE_1:def 1;

      (a * b) = (a * (k ^2 )) by A2, A3, A4, A5;

      

      then b = (k ^2 ) by XCMPLX_1: 5

      .= ( |.k.| ^2 ) by COMPLEX1: 75;

      hence thesis;

    end;

    registration

      let a be square Element of NAT , n be Nat;

      cluster (a |^ n) -> square;

      coherence

      proof

        consider k be Nat such that

         A1: (k ^2 ) = a by PYTHTRIP:def 3;

        (a |^ n) = (k |^ (2 * n)) by A1, NEWTON: 9

        .= ((k |^ n) ^2 ) by NEWTON: 9;

        hence thesis;

      end;

    end

    registration

      let a be square Integer, n be Nat;

      cluster (a |^ n) -> square;

      coherence

      proof

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

        (a |^ n) is square;

        hence thesis;

      end;

    end

    registration

      let a be non zero square Integer, b be non square Integer;

      cluster (a * b) -> non square;

      coherence by PT1;

    end

    registration

      let a be Element of NAT ;

      let b be even Nat;

      cluster (a |^ b) -> square;

      coherence

      proof

        reconsider x = (b / 2) as Nat;

        reconsider k = (a |^ x) as Element of NAT by ORDINAL1:def 12;

        (a |^ (2 * x)) = ((a |^ x) |^ 2) by NEWTON: 9;

        hence thesis;

      end;

    end

    registration

      let a be non square Element of NAT ;

      let b be odd Nat;

      cluster (a |^ b) -> non square;

      coherence

      proof

        reconsider x = ((b - 1) / 2) as Nat;

        reconsider k = (a |^ (2 * x)) as square Nat;

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

        hence thesis;

      end;

    end

    

     LmNAT: for a,n be Nat, x be non negative Real holds (a |^ n) < (x |^ n) < ((a + 1) |^ n) implies not x is Nat

    proof

      let a,n be Nat, x be non negative Real;

      assume (a |^ n) < (x |^ n) < ((a + 1) |^ n);

      then a < x < (a + 1) by NEWTON02: 41;

      hence thesis by NAT_1: 13;

    end;

    registration

      let a be non zero square Integer;

      cluster (a + 1) -> non square;

      coherence

      proof

        consider b be Nat such that

         A1: a = (b ^2 ) by PYTHTRIP:def 3;

        a = (b * b) by A1, SQUARE_1:def 1;

        then b > 0 ;

        then

         A2: (((b * b) + 1) + (2 * b)) > (((b * b) + 1) + 0 ) by XREAL_1: 6;

        

         A3: (b * b) = (b ^2 ) & ((b + 1) * (b + 1)) = ((b + 1) ^2 ) by SQUARE_1:def 1;

        ((b * b) + 1) > ((b * b) + 0 ) by XREAL_1: 6;

        then not ex k be Nat st ((b ^2 ) + 1) = (k ^2 ) by A2, A3, LmNAT;

        hence thesis by A1, PYTHTRIP:def 3;

      end;

    end

    registration

      let a be non zero square Element of NAT ;

      cluster (a + 1) -> non square;

      coherence ;

    end

    registration

      let a be non zero square object, b be non square Element of NAT ;

      cluster (a * b) -> non square;

      coherence ;

    end

    registration

      let a be non zero square Integer;

      let n,m be Nat;

      cluster ((a |^ n) + (a |^ m)) -> non square;

      coherence

      proof

        per cases ;

          suppose n >= m;

          then

          consider x be Nat such that

           A1: n = (m + x) by NAT_1: 10;

          reconsider l = (a |^ x) as non zero square Integer;

          ((a |^ (m + x)) + (a |^ m)) = (((a |^ m) * (a |^ x)) + (a |^ m)) by NEWTON: 8

          .= ((l + 1) * (a |^ m));

          hence thesis by A1;

        end;

          suppose m > n;

          then

          consider x be Nat such that

           A1: m = (n + x) by NAT_1: 10;

          reconsider l = (a |^ x) as non zero square Integer;

          ((a |^ (n + x)) + (a |^ n)) = (((a |^ n) * (a |^ x)) + (a |^ n)) by NEWTON: 8

          .= ((l + 1) * (a |^ n));

          hence thesis by A1;

        end;

      end;

    end

    registration

      let a be non zero square Element of NAT ;

      let n,m be Nat;

      cluster ((a |^ n) + (a |^ m)) -> non square;

      coherence ;

    end

    registration

      let a be non zero square Integer;

      let p be prime Nat;

      cluster (p * a) -> non square;

      coherence ;

    end

    registration

      let a be non trivial Element of NAT ;

      cluster (a - 1) -> non zero;

      coherence ;

    end

    registration

      let q be square Integer;

      cluster |.q.| -> square;

      coherence ;

    end

    registration

      let x be non zero Integer;

      cluster |.x.| -> non zero;

      coherence by COMPLEX1: 47;

    end

    registration

      let a be non trivial square Element of NAT ;

      cluster (a - 1) -> non square;

      coherence

      proof

        assume not thesis;

        then

        reconsider k = (a - 1) as square Element of NAT by ORDINAL1:def 12;

        (k + 1) is non square;

        hence contradiction;

      end;

    end

    

     LmN30: for a,b be non square Element of NAT holds (a,b) are_coprime implies (a * b) is non square

    proof

      let a,b be non square Element of NAT ;

      assume

       A1: (a,b) are_coprime ;

      assume not thesis;

      then

      consider k be Nat such that

       A2: (a * b) = (k ^2 ) by PYTHTRIP:def 3;

      ex k st (k |^ 2) = a by A1, A2, NEWTON02: 30;

      hence contradiction;

    end;

    

     COMPLEX175: for a be Integer holds ( |.a.| |^ 2) = (a |^ 2)

    proof

      let a be Integer;

      

      thus ( |.a.| |^ 2) = ( |.a.| ^2 )

      .= (a ^2 ) by COMPLEX1: 75

      .= (a |^ 2);

    end;

    registration

      let a be non trivial Element of NAT ;

      cluster (a * (a - 1)) -> non square;

      coherence

      proof

        per cases ;

          suppose a is square;

          hence thesis;

        end;

          suppose a is non square;

          then

          reconsider a as non square Element of NAT ;

          per cases ;

            suppose (a - 1) is square;

            hence thesis;

          end;

            suppose (a - 1) is non square;

            then

            reconsider k = (a - 1) as non square Element of NAT by ORDINAL1:def 12;

            ((a - 1),((a - 1) + 1)) are_coprime ;

            then (a * k) is non square by LmN30;

            hence thesis;

          end;

        end;

      end;

    end

    registration

      let a,b be Integer, n,m be Nat;

      cluster ((((a |^ n) + (b |^ n)) * ((a |^ m) - (b |^ m))) + (((a |^ m) + (b |^ m)) * ((a |^ n) - (b |^ n)))) -> even;

      coherence

      proof

        ((((((a |^ n) + (b |^ n)) * ((a |^ m) - (b |^ m))) + (((a |^ m) + (b |^ m)) * ((a |^ n) - (b |^ n)))) / 2) * 2) = (((a |^ (n + m)) - (b |^ (n + m))) * 2) by NEWTON01: 5;

        hence thesis;

      end;

      cluster ((((a |^ n) + (b |^ n)) * ((a |^ m) + (b |^ m))) + (((a |^ m) - (b |^ m)) * ((a |^ n) - (b |^ n)))) -> even;

      coherence

      proof

        ((((((a |^ n) + (b |^ n)) * ((a |^ m) + (b |^ m))) + (((a |^ m) - (b |^ m)) * ((a |^ n) - (b |^ n)))) / 2) * 2) = (((a |^ (n + m)) + (b |^ (n + m))) * 2) by NEWTON01: 8;

        hence thesis;

      end;

    end

    registration

      let a be even Integer;

      cluster (a / 2) -> integer;

      coherence

      proof

        2 divides a by ABIAN:def 1;

        then

        consider k be Integer such that

         A1: a = (2 * k);

        thus thesis by A1;

      end;

    end

    registration

      let a,b be non zero Nat;

      cluster (a + b) -> non trivial;

      coherence

      proof

        b >= 1 by NAT_1: 14;

        then (a + b) > ( 0 + 1) by XREAL_1: 8;

        hence thesis;

      end;

    end

    registration

      let b be non zero Nat, a,c be non trivial Nat;

      reduce (c |-count (c |^ (a |-count b))) to (a |-count b);

      reducibility by Def0, NAT_3: 25;

    end

    registration

      let a,b be non zero Integer;

      cluster (a / (a gcd b)) -> integer;

      coherence

      proof

        (a gcd b) divides a by INT_2:def 2;

        then

        consider k be Integer such that

         A1: a = ((a gcd b) * k);

        thus thesis by A1, XCMPLX_1: 89;

      end;

      cluster ((a lcm b) / b) -> integer;

      coherence

      proof

        b divides (a lcm b) by INT_2:def 1;

        then

        consider k be Integer such that

         A1: (a lcm b) = (b * k);

        thus thesis by A1, XCMPLX_1: 89;

      end;

      cluster ((a lcm b) / (a gcd b)) -> integer;

      coherence

      proof

        

         A1: (a gcd b) divides a by INT_2:def 2;

        a divides (a lcm b) by INT_2:def 1;

        then (a gcd b) divides (a lcm b) by A1, INT_2: 9;

        then

        consider k be Integer such that

         A2: (a lcm b) = ((a gcd b) * k);

        thus thesis by A2, XCMPLX_1: 89;

      end;

    end

    registration

      let a be even Integer;

      reduce (a gcd 2) to 2;

      reducibility

      proof

        2 divides a by ABIAN:def 1;

        then

        consider k be Integer such that

         A1: a = (2 * k);

        (k,1) are_coprime ;

        then ((2 * k) gcd (2 * 1)) = |.2.| by INT_2: 24;

        hence thesis by A1;

      end;

    end

    registration

      cluster non zero for even Nat;

      existence

      proof

        2 is even & 2 is non zero;

        hence thesis;

      end;

    end

    registration

      let a be even Integer, n be non zero Nat;

      cluster (a * n) -> even;

      coherence ;

      cluster (a |^ n) -> even;

      coherence ;

    end

    registration

      let a be Integer, n be zero Nat;

      cluster (a * n) -> even;

      coherence ;

      cluster (a |^ n) -> odd;

      coherence

      proof

        (1 * (a |^ n)) is odd;

        hence thesis;

      end;

    end

    registration

      let a be Element of NAT ;

      reduce |.a.| to a;

      reducibility ;

    end

    registration

      let a be non negative Real;

      let n be non zero Nat;

      reduce (n -root (a |^ n)) to a;

      reducibility

      proof

        n >= 1 & a >= 0 by NAT_1: 14;

        hence thesis by POWER: 4;

      end;

      reduce ((n -root a) |^ n) to a;

      reducibility

      proof

        n >= 1 & a >= 0 by NAT_1: 14;

        hence thesis by POWER: 4;

      end;

    end

    theorem :: NEWTON03:11

    

     INT29: not a divides b implies not (a * c) divides b

    proof

      a divides (a * c);

      hence thesis by INT_2: 9;

    end;

    theorem :: NEWTON03:12

    

     POW1: for a,b be non negative Real, n be positive Nat holds (a |^ n) = (b |^ n) iff a = b

    proof

      let a,b be non negative Real, n be positive Nat;

      (a > b implies (a |^ n) > (b |^ n)) & (a < b implies (a |^ n) < (b |^ n)) by NEWTON02: 40;

      hence thesis by XXREAL_0: 1;

    end;

    registration

      let a be Real, n be even Nat;

      cluster (a |^ n) -> non negative;

      coherence

      proof

        per cases ;

          suppose a >= 0 ;

          hence thesis;

        end;

          suppose a < 0 ;

          hence thesis;

        end;

      end;

    end

    registration

      let a be negative Real, n be odd Nat;

      cluster (a |^ n) -> negative;

      coherence

      proof

        (( - a) |^ n) is positive;

        then ( - (a |^ n)) is positive by POWER: 2;

        hence thesis;

      end;

    end

    theorem :: NEWTON03:13

    

     POW2: for a,b be Real, n be odd Nat holds (a |^ n) = (b |^ n) iff a = b

    proof

      let a,b be Real, n be odd Nat;

      per cases ;

        suppose

         A1: a >= 0 ;

        per cases ;

          suppose b >= 0 ;

          hence thesis by A1, POW1;

        end;

          suppose b < 0 ;

          hence thesis by A1;

        end;

      end;

        suppose

         A2: a < 0 ;

        per cases ;

          suppose b < 0 ;

          then

          reconsider k = ( - b) as positive Real;

          reconsider l = ( - a) as positive Real by A2;

          

           B1: (( - a) |^ n) = ( - (a |^ n)) & (( - b) |^ n) = ( - (b |^ n)) by POWER: 2;

          (k |^ n) = (l |^ n) iff k = l by POW1;

          hence thesis by B1;

        end;

          suppose b >= 0 ;

          hence thesis by A2;

        end;

      end;

    end;

    theorem :: NEWTON03:14

    for a, b st (a,b) are_coprime holds for n be non zero Nat holds (a * b) = (c |^ n) iff ((n -root a) in NAT & (n -root b) in NAT & c = ((n -root a) * (n -root b)))

    proof

      let a, b such that

       A1: (a,b) are_coprime ;

      let n be non zero Nat;

      thus (a * b) = (c |^ n) implies ((n -root a) in NAT & (n -root b) in NAT & c = ((n -root a) * (n -root b)))

      proof

        assume

         B1: (a * b) = (c |^ n);

        then

        consider k such that

         B2: a = (k |^ n) by A1, NEWTON02: 30;

        consider l such that

         B3: b = (l |^ n) by A1, B1, NEWTON02: 30;

        ((n -root c) |^ n) = (n -root (a * b)) by B1

        .= ((n -root a) * (n -root b)) by POWER: 11, NAT_1: 14

        .= (((n -root k) |^ n) * ((n -root l) |^ n)) by B2, B3;

        hence thesis by ORDINAL1:def 12, B2, B3;

      end;

      assume (n -root a) in NAT & (n -root b) in NAT & c = ((n -root a) * (n -root b));

      then (c |^ n) = (((n -root a) |^ n) * ((n -root b) |^ n)) by NEWTON: 7;

      hence thesis;

    end;

    theorem :: NEWTON03:15

    

     POWD: for n be non zero Nat, a be Integer, b be Integer holds (b |^ n) divides (a |^ n) iff b divides a

    proof

      let n be non zero Nat, a be Integer, b be Integer;

      thus (b |^ n) divides (a |^ n) implies b divides a

      proof

        assume

         A1: (b |^ n) divides (a |^ n);

        ( |.b.| |^ n) = |.(b |^ n).| by TAYLOR_2: 1

        .= ((b |^ n) gcd (a |^ n)) by A1, NEWTON02: 3

        .= ((b gcd a) |^ n) by NEWTON027;

        hence thesis by NEWTON02: 3, WSIERP_1: 3;

      end;

      thus thesis by NEWTON02: 15;

    end;

    theorem :: NEWTON03:16

    

     NEWTON89: for a be Integer, m,n be Nat st m >= n holds (a |^ n) divides (a |^ m)

    proof

      let a be Integer, m,n be Nat;

      

       A1: |.(a |^ n).| = ( |.a.| |^ n) & |.(a |^ m).| = ( |.a.| |^ m) by TAYLOR_2: 1;

      assume m >= n;

      hence thesis by INT_2: 16, A1, NEWTON: 89;

    end;

    

     LmX: for a,b be Integer holds (a |^ m) divides b & not (a |^ n) divides b implies n > m

    proof

      let a,b be Integer;

      assume

       A1: (a |^ m) divides b & not (a |^ n) divides b;

      assume not thesis;

      then (a |^ n) divides (a |^ m) by NEWTON89;

      hence contradiction by A1, INT_2: 9;

    end;

    theorem :: NEWTON03:17

    

     LmY: for a,b be Integer holds a divides b & (b |^ m) divides c implies (a |^ m) divides c

    proof

      let a,b be Integer;

      assume

       A1: a divides b & (b |^ m) divides c;

      then (a gcd b) = |.a.| by NEWTON02: 3;

      

      then ((a |^ m) gcd (b |^ m)) = ( |.a.| |^ m) by NEWTON027

      .= |.(a |^ m).| by TAYLOR_2: 1;

      then (a |^ m) divides (b |^ m) by NEWTON02: 3;

      hence thesis by A1, INT_2: 9;

    end;

    theorem :: NEWTON03:18

    for a,p be Integer holds (p |^ ((2 * n) + k)) divides (a |^ 2) implies (p |^ n) divides a

    proof

      let a,p be Integer;

      assume

       A1: (p |^ ((2 * n) + k)) divides (a |^ 2);

      (p |^ (2 * n)) divides (p |^ ((2 * n) + k)) by NAT_1: 11, NEWTON89;

      then (p |^ (2 * n)) divides (a |^ 2) by A1, INT_2: 9;

      then

       A2: ((p |^ n) |^ 2) divides (a |^ 2) by NEWTON: 9;

      ( |.(p |^ n).| |^ 2) = |.((p |^ n) |^ 2).| by TAYLOR_2: 1

      .= (((p |^ n) |^ 2) gcd (a |^ 2)) by A2, NEWTON02: 3

      .= (((p |^ n) gcd a) |^ 2) by NEWTON027;

      hence thesis by POW1, NEWTON02: 3;

    end;

    theorem :: NEWTON03:19

    for a,b be odd square Element of NAT holds 8 divides (a - b)

    proof

      let a,b be odd square Element of NAT ;

      consider c such that

       A1: a = (c ^2 ) by PYTHTRIP:def 3;

      consider d such that

       A2: b = (d ^2 ) by PYTHTRIP:def 3;

      c is odd & d is odd & a = (c |^ 2) & b = (d |^ 2) by A1, A2;

      hence thesis by NEWTON02: 63;

    end;

    theorem :: NEWTON03:20

    for a,b be odd Nat holds 4 divides (a - b) implies not 4 divides ((a |^ n) + (b |^ n))

    proof

      let a,b be odd Nat;

      assume

       A1: 4 divides (a - b);

      per cases ;

        suppose n is odd;

        hence thesis by A1, NEWTON02: 69;

      end;

        suppose n is even;

        then 4 divides ((a |^ n) - (b |^ n)) by NEWTON02: 65;

        hence thesis by NEWTON02: 58;

      end;

    end;

    theorem :: NEWTON03:21

    for a,b be odd Nat holds (4 divides ((a |^ n) + (b |^ n))) implies not 4 divides ((a |^ (2 * n)) + (b |^ (2 * n)))

    proof

      let a,b be odd Nat;

      

       A0: ((a |^ n) |^ 2) = (a |^ (2 * n)) & ((b |^ n) |^ 2) = (b |^ (2 * n)) by NEWTON: 9;

      assume 4 divides ((a |^ n) + (b |^ n));

      then 4 divides (((a |^ n) + (b |^ n)) * ((a |^ n) - (b |^ n))) by INT_2: 2;

      then 4 divides ((a |^ (2 * n)) - (b |^ (2 * n))) by A0, NEWTON01: 1;

      hence thesis by NEWTON02: 58;

    end;

    theorem :: NEWTON03:22

    for a,b be odd Nat holds (4 divides ((a |^ n) - (b |^ n))) implies not 4 divides ((a |^ (2 * n)) + (b |^ (2 * n)))

    proof

      let a,b be odd Nat;

      

       A0: ((a |^ n) |^ 2) = (a |^ (2 * n)) & ((b |^ n) |^ 2) = (b |^ (2 * n)) by NEWTON: 9;

      assume 4 divides ((a |^ n) - (b |^ n));

      then 4 divides (((a |^ n) + (b |^ n)) * ((a |^ n) - (b |^ n))) by INT_2: 2;

      then 4 divides (((a |^ n) |^ 2) - ((b |^ n) |^ 2)) by NEWTON01: 1;

      hence thesis by NEWTON02: 58, A0;

    end;

    theorem :: NEWTON03:23

    

     Even: for a,b be odd Nat holds (2 |^ m) divides ((a |^ n) - (b |^ n)) implies (2 |^ (m + 1)) divides ((a |^ (2 * n)) - (b |^ (2 * n)))

    proof

      let a,b be odd Nat;

      

       A0: (a |^ (2 * n)) = ((a |^ n) |^ 2) & (b |^ (2 * n)) = ((b |^ n) |^ 2) by NEWTON: 9;

      assume

       A1: (2 |^ m) divides ((a |^ n) - (b |^ n));

      

       A2: 2 divides ((a |^ n) + (b |^ n)) by ABIAN:def 1;

      ((a |^ (2 * n)) - (b |^ (2 * n))) = (((a |^ n) - (b |^ n)) * ((a |^ n) + (b |^ n))) by A0, NEWTON01: 1;

      then (2 * (2 |^ m)) divides ((a |^ (2 * n)) - (b |^ (2 * n))) by A1, A2, NEWTON02: 2;

      hence thesis by NEWTON: 6;

    end;

    theorem :: NEWTON03:24

    

     N3: ((a1 |^ 3) - (b1 |^ 3)) = ((a1 - b1) * (((a1 |^ 2) + (b1 |^ 2)) + (a1 * b1)))

    proof

      ((a1 |^ (2 + 1)) - (b1 |^ (2 + 1))) = (((a1 |^ 2) * ((a1 |^ 1) - (b1 |^ 1))) + ((b1 |^ 1) * ((a1 |^ 2) - (b1 |^ 2)))) by RI2

      .= (((a1 |^ 2) * (a1 - b1)) + (b1 * ((a1 + b1) * (a1 - b1)))) by NEWTON01: 1

      .= ((a1 - b1) * (((a1 |^ 2) + (b1 * b1)) + (a1 * b1)));

      hence thesis by NEWTON: 81;

    end;

    theorem :: NEWTON03:25

    for n be odd Nat holds 3 divides ((a |^ n) + (b |^ n)) iff 3 divides (a + b)

    proof

      let n be odd Nat;

      consider k such that

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

      3 divides ((a |^ n) + (b |^ n)) implies 3 divides (a + b)

      proof

        assume

         A1: 3 divides ((a |^ n) + (b |^ n));

        3 divides ((a |^ n) - a) & 3 divides ((b |^ n) - b) by A0, NEWTON02: 173;

        then 3 divides (((a |^ n) - a) + ((b |^ n) - b)) by WSIERP_1: 4;

        then 3 divides (((a |^ n) + (b |^ n)) + ( - (a + b)));

        then 3 divides ( - (a + b)) by A1, INT_2: 1;

        hence thesis by INT_2: 10;

      end;

      hence thesis by A0, NEWTON02: 196, PEPIN: 41;

    end;

    theorem :: NEWTON03:26

    

     D3: for c be Integer holds c divides (a - b) implies c divides ((a |^ n) - (b |^ n))

    proof

      let c be Integer;

      assume

       A1: c divides (a - b);

      (a - b) divides ((a |^ n) - (b |^ n)) by NEWTON01: 33;

      hence thesis by A1, INT_2: 9;

    end;

    theorem :: NEWTON03:27

    for n be odd Nat holds 3 divides ((a |^ n) - (b |^ n)) iff 3 divides (a - b)

    proof

      let n be odd Nat;

      consider k such that

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

      3 divides ((a |^ n) - (b |^ n)) implies 3 divides (a - b)

      proof

        assume

         A1: 3 divides ((a |^ n) - (b |^ n));

        3 divides ((a |^ n) - a) & 3 divides ( - ((b |^ n) - b)) by A0, NEWTON02: 173, INT_2: 10;

        then 3 divides (((a |^ n) - a) + ( - ((b |^ n) - b))) by WSIERP_1: 4;

        then 3 divides (((a |^ n) - (b |^ n)) + ( - (a - b)));

        then 3 divides ( - (a - b)) by A1, INT_2: 1;

        hence thesis by INT_2: 10;

      end;

      hence thesis by D3;

    end;

    theorem :: NEWTON03:28

    for n be Nat holds ((a |^ n),((a - b) |^ n)) are_congruent_mod b

    proof

      b divides ((((a - b) + b) |^ n) - ((a - b) |^ n)) by NEWTON02: 10;

      hence thesis;

    end;

    theorem :: NEWTON03:29

    for a be non trivial Nat holds ex n be prime Nat st n divides a

    proof

      let a be non trivial Nat;

      per cases ;

        suppose a is prime;

        hence thesis;

      end;

        suppose not (a is prime);

        then ex n be Element of NAT st n > 1 & (n * n) <= a & n is prime & n divides a by NAT_4: 14, Def0;

        hence thesis;

      end;

    end;

    theorem :: NEWTON03:30

    

     PSQ: for p be prime Nat holds p divides ((p + (k + 1)) * (p - (k + 1))) implies (k + 1) >= p

    proof

      let p be prime Nat;

      p divides (p * p);

      then

       A1: p divides (p |^ 2) by NEWTON: 81;

      

       A2: (p |^ 2) = (((p |^ 2) - ((k + 1) |^ 2)) + ((k + 1) |^ 2));

      assume p divides ((p + (k + 1)) * (p - (k + 1)));

      then p divides ((p |^ 2) - ((k + 1) |^ 2)) by NEWTON01: 1;

      then p divides ((k + 1) |^ 2) by A1, A2, INT_2: 1;

      hence thesis by NAT_D: 7, NAT_3: 5;

    end;

    theorem :: NEWTON03:31

    for p be prime Nat, k be non zero Nat st k < p holds not p divides ((p |^ 2) - (k |^ 2))

    proof

      let p be prime Nat, k be non zero Nat;

      reconsider a = (k - 1) as Nat;

      p divides ((p - (a + 1)) * (p + (a + 1))) implies (a + 1) >= p by PSQ;

      hence thesis by NEWTON01: 1;

    end;

    theorem :: NEWTON03:32

    

     SUD: for a,b be Integer, p be odd prime Nat st not p divides b holds p divides (a - b) implies not p divides (a + b)

    proof

      let a,b be Integer, p be odd prime Nat such that

       A1: not p divides b;

      (p gcd 2) = 1 by Def3;

      then not p divides 2 by INT_2: 28, PEPIN: 2, PYTHTRIP:def 2;

      then

       A2: not p divides (2 * b) by A1, INT_5: 7;

      assume p divides (a - b);

      then not p divides ((a - b) + (2 * b)) by A2, INT_2: 1;

      hence thesis;

    end;

    

     LmSQ: for p be prime Nat, k be square Nat holds p divides k implies (p ^2 ) divides k

    proof

      let p be prime Nat, k be square Nat;

      consider a be Nat such that

       A1: (a ^2 ) = k by PYTHTRIP:def 3;

      assume p divides k;

      hence thesis by A1, NAT_3: 5, NEWTON02: 15;

    end;

    theorem :: NEWTON03:33

    for a be non zero square Element of NAT , p be prime Nat st p divides a holds not (a + p) is square

    proof

      let a be non zero square Element of NAT ;

      let p be prime Nat;

      assume

       B0: p divides a;

      then

      consider k such that

       B1: a = (p * k) by NAT_D:def 3;

      

       B3: not p is trivial;

      (p ^2 ) divides a by B0, LmSQ;

      then (p * p) divides (p * k) by B1, SQUARE_1:def 1;

      then p divides k by INT_4: 7;

      then

      consider n such that

       B4: k = (p * n) by NAT_D:def 3;

       not p divides (1 * (k + 1)) by B3, INT_2: 13, B4, NEWTON02: 77;

      then not (p * p) divides (p * (k + 1)) by INT_4: 7;

      then not (p ^2 ) divides (p * (k + 1)) by SQUARE_1:def 1;

      hence thesis by B1, LmSQ, INT_1:def 3;

    end;

    theorem :: NEWTON03:34

    for a be non zero square Element of NAT , p be prime Nat holds (a + p) is square implies p = ((2 * ( sqrt a)) + 1)

    proof

      let a be non zero square Element of NAT ;

      let p be prime Nat;

      assume (a + p) is square;

      then

      consider m such that

       B2: (a + p) = (m ^2 ) by PYTHTRIP:def 3;

      consider n such that

       B3: a = (n ^2 ) by PYTHTRIP:def 3;

      

       B4: p = ((m ^2 ) - (n ^2 )) by B2, B3

      .= ((m - n) * (m + n)) by NEWTON01: 1;

      (m - n) > 0 by B4;

      then

      reconsider l = (m - n) as Element of NAT by INT_1: 3;

      (m - n) divides p & (m + n) divides p by B4;

      then

       B5: ((m + n) = p or (m + n) = 1) & (l = p or l = 1) by INT_2:def 4;

      n >= ( - n) & not p is trivial;

      then (n + m) >= (( - n) + m) & p > 1 by XREAL_1: 6;

      then p = ((2 * n) + 1) by B4, B5;

      hence thesis by B3, SQUARE_1:def 2;

    end;

    

     NAT517: for a,b be Nat st (a,b) are_coprime holds (c gcd (a * b)) = ((c gcd a) * (c gcd b))

    proof

      let a,b be Nat such that

       A1: (a,b) are_coprime ;

      per cases ;

        suppose a = 0 ;

        hence thesis by A1;

      end;

        suppose b = 0 ;

        hence thesis by A1;

      end;

        suppose a <> 0 & b <> 0 ;

        hence thesis by A1, NAT_5: 17;

      end;

    end;

    theorem :: NEWTON03:35

    for a,b,c be Integer st (a,b) are_coprime holds (c gcd (a * b)) = ((c gcd a) * (c gcd b))

    proof

      let a,b,c be Integer such that

       A1: (a,b) are_coprime ;

      reconsider k = |.a.|, l = |.b.|, m = |.c.| as Nat;

      

       A2: (k,l) are_coprime by A1, INT_2: 34;

      ( |.a.| * |.b.|) = |.(a * b).| by COMPLEX1: 65;

      then (c gcd (a * b)) = (m gcd (k * l)) & (c gcd a) = (m gcd k) & (c gcd b) = (m gcd l) by INT_2: 34;

      hence thesis by A2, NAT517;

    end;

    theorem :: NEWTON03:36

    for p be prime Nat holds a divides (p |^ n) implies ex k st a = (p |^ k)

    proof

      let p be prime Nat;

      assume a divides (p |^ n);

      then ex k be Nat st a = (p |^ k) & k <= n by GROUPP_1: 2;

      hence thesis;

    end;

    theorem :: NEWTON03:37

    for a,b be non zero Nat, p be prime Nat st (a + b) = p holds (a,b) are_coprime

    proof

      let a,b be non zero Nat, p be prime Nat;

      

       A1: (a + b) > (a + 0 ) by XREAL_1: 6;

      assume

       A2: (a + b) = p;

      then (a,p) are_coprime by A1, NAT_D: 7, NAT_6: 6;

      hence thesis by A2, NEWTON02: 45;

    end;

    theorem :: NEWTON03:38

    for a,b be non zero Nat, p be prime Nat holds ((a |^ n) + (b |^ n)) = (p |^ n) implies (a,b) are_coprime

    proof

      let a,b be non zero Nat, p be prime Nat;

      

       A1: ((a |^ n) + (b |^ n)) > ((a |^ n) + 0 ) by XREAL_1: 6;

      assume

       A2: ((a |^ n) + (b |^ n)) = (p |^ n);

      then

      reconsider n as non zero Nat;

      (a |^ n) < (p |^ n) by A1, A2;

      then a < p by NEWTON02: 40;

      then (a,p) are_coprime by NAT_D: 7, NAT_6: 6;

      then ((a |^ n),(p |^ n)) are_coprime by WSIERP_1: 11;

      then ((a |^ n),(b |^ n)) are_coprime by A2, NEWTON02: 45;

      then (a,(b |^ n)) are_coprime by NEWTON02: 73;

      hence thesis by NEWTON02: 73;

    end;

    theorem :: NEWTON03:39

    for a,b be non zero Nat st c >= (a + b) holds ((c |^ (k + 1)) * (a + b)) > ((a |^ (k + 2)) + (b |^ (k + 2)))

    proof

      let a,b be non zero Nat;

      

       A1: ((a |^ 1) + (b |^ 1)) <= ((a + b) |^ 1) implies ((a |^ ((k + 1) + 1)) + (b |^ ((k + 1) + 1))) < ((a + b) |^ ((k + 1) + 1)) by NEWTON01: 18;

      assume c >= (a + b);

      then (c |^ (k + 1)) >= ((a + b) |^ (k + 1)) by NEWTON02: 40;

      then ((c |^ (k + 1)) * (a + b)) >= (((a + b) |^ (k + 1)) * (a + b)) by XREAL_1: 64;

      then ((c |^ (k + 1)) * (a + b)) >= ((a + b) |^ ((k + 1) + 1)) by NEWTON: 6;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: NEWTON03:40

    for a,c be Nat, b be non zero Nat holds (a * b) < c < (a * (b + 1)) implies not a divides c & not c divides a

    proof

      let a,c be Nat, b be non zero Nat;

      assume

       A1: (a * b) < c < (a * (b + 1));

      then

      reconsider c as non zero Nat;

      reconsider a as non zero Nat by A1;

      assume not thesis;

      per cases ;

        suppose a divides c;

        then

        consider k be Nat such that

         B1: c = (a * k) by NAT_D:def 3;

        b < k by A1, B1, XREAL_1: 64;

        then (b + 1) <= k by NAT_1: 13;

        hence contradiction by A1, B1, XREAL_1: 64;

      end;

        suppose

         B1: c divides a;

        (a * b) >= (a * 1) by XREAL_1: 64, NAT_1: 14;

        then c > a by A1, XXREAL_0: 2;

        hence thesis by B1, NAT_D: 7;

      end;

    end;

    theorem :: NEWTON03:41

    

     MinMax: for a,b be Real holds (a + b) = (( min (a,b)) + ( max (a,b)))

    proof

      let a,b be Real;

      per cases ;

        suppose a >= b;

        then a = ( max (a,b)) & b = ( min (a,b)) by XXREAL_0:def 9, XXREAL_0:def 10;

        hence thesis;

      end;

        suppose a < b;

        then a = ( min (a,b)) & b = ( max (a,b)) by XXREAL_0:def 9, XXREAL_0:def 10;

        hence thesis;

      end;

    end;

    theorem :: NEWTON03:42

    

     MM1: for a,b be non negative Real holds ( max ((a |^ n),(b |^ n))) = (( max (a,b)) |^ n) & ( min ((a |^ n),(b |^ n))) = (( min (a,b)) |^ n)

    proof

      let a,b be non negative Real;

      per cases ;

        suppose a >= b;

        then (a |^ n) = ( max ((a |^ n),(b |^ n))) & (b |^ n) = ( min ((a |^ n),(b |^ n))) & a = ( max (a,b)) & b = ( min (a,b)) by NEWTON02: 41, XXREAL_0:def 9, XXREAL_0:def 10;

        hence thesis;

      end;

        suppose a < b;

        then (b |^ n) = ( max ((a |^ n),(b |^ n))) & (a |^ n) = ( min ((a |^ n),(b |^ n))) & b = ( max (a,b)) & a = ( min (a,b)) by NEWTON02: 41, XXREAL_0:def 9, XXREAL_0:def 10;

        hence thesis;

      end;

    end;

    theorem :: NEWTON03:43

    for p be prime Nat holds (a * b) = (p |^ n) implies ex k,l be Nat st a = (p |^ k) & b = (p |^ l) & (k + l) = n

    proof

      let p be prime Nat;

      assume

       A1: (a * b) = (p |^ n);

      then a divides (p |^ n);

      then

      consider k be Nat such that

       A2: a = (p |^ k) & k <= n by GROUPP_1: 2;

      b divides (p |^ n) by A1;

      then

      consider l be Nat such that

       A3: b = (p |^ l) & l <= n by GROUPP_1: 2;

      (p |^ n) = (p |^ (k + l)) by NEWTON: 8, A1, A2, A3;

      then n = (k + l) by PEPIN: 30, Def0;

      hence thesis by A2, A3;

    end;

    theorem :: NEWTON03:44

    

     NTC: for a,b be non trivial Nat holds (a,b) are_coprime implies not a divides b & not b divides a

    proof

      let a,b be non trivial Nat;

      assume (a,b) are_coprime ;

      then 1 = (a gcd (b mod a)) & 1 = (b gcd (a mod b)) by NAT_D: 28;

      then

       A3: not (b mod a) = 0 & not (a mod b) = 0 by Def0;

      a = (((a div b) * b) + (a mod b)) & b = (((b div a) * a) + (b mod a)) by NAT_D: 2;

      then not a = ((a div b) * b) & not b = ((b div a) * a) by A3;

      hence thesis by NAT_D: 3;

    end;

    theorem :: NEWTON03:45

    for a be non trivial Nat, p be prime Nat st p > a holds not p divides a & not a divides p

    proof

      let a be non trivial Nat, p be prime Nat;

      assume p > a;

      then (a,p) are_coprime by NAT_6: 6, NAT_D: 7;

      hence thesis by NTC;

    end;

    theorem :: NEWTON03:46

    

     GCDP: for p be prime Nat holds (a gcd p) = 1 or (a gcd p) = p

    proof

      let p be prime Nat;

      per cases by NAT_6: 6;

        suppose p divides a;

        hence thesis by NEWTON: 49;

      end;

        suppose (a gcd p) = 1;

        hence thesis;

      end;

    end;

    theorem :: NEWTON03:47

    for a be non trivial Nat, p be prime Nat holds a divides (p |^ n) implies p divides a

    proof

      let a be non trivial Nat, p be prime Nat;

      assume a divides (p |^ n);

      then

       A1: (a gcd (p |^ n)) = |.a.| by NEWTON02: 3;

      per cases by GCDP;

        suppose (a gcd p) = 1;

        then (a gcd (p |^ n)) = 1 by WSIERP_1: 12;

        hence thesis by A1, Def0;

      end;

        suppose (a gcd p) = p;

        hence thesis by INT_2:def 2;

      end;

    end;

    theorem :: NEWTON03:48

    

     SC1: for a,b be odd Nat, m be even Nat holds (2 |-count ((a |^ m) + (b |^ m))) = 1

    proof

      let a,b be odd Nat, m be even Nat;

      

       A1: 4 = (2 * 2)

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

      4 divides ((a |^ m) - (b |^ m)) by NEWTON02: 65;

      then

       A2: not (2 |^ (1 + 1)) divides ((a |^ m) + (b |^ m)) by A1, NEWTON02: 58;

      ((a |^ m) + (b |^ m)) is even;

      then (2 |^ 1) divides ((a |^ m) + (b |^ m));

      hence thesis by A2, NAT_3:def 7;

    end;

    

     LmC1: for a be non zero Nat, p be non trivial Nat holds ((p |^ (p |-count a)) divides a & not (p * (p |^ (p |-count a))) divides a)

    proof

      let a be non zero Nat, p be non trivial Nat;

      a <> 0 & p <> 1 by NAT_2:def 1;

      then (p |^ (p |-count a)) divides a & not (p |^ ((p |-count a) + 1)) divides a by NAT_3:def 7;

      hence thesis by NEWTON: 6;

    end;

    theorem :: NEWTON03:49

    for a be non zero Nat holds ex k be odd Nat st a = ((2 |^ (2 |-count a)) * k)

    proof

      let a be non zero Nat;

      

       A1: 2 is non trivial;

      then

      consider k such that

       A2: a = ((2 |^ (2 |-count a)) * k) by LmC1, NAT_D:def 3;

       not (2 * (2 |^ (2 |-count a))) divides ((2 |^ (2 |-count a)) * k) by A1, A2, LmC1;

      then k is odd by NEWTON02: 2;

      hence thesis by A2;

    end;

    theorem :: NEWTON03:50

    for b be non zero Nat holds a > b implies ex p be prime Nat st (p |-count a) > (p |-count b)

    proof

      let b be non zero Nat;

      assume

       A1: a > b;

      then

      reconsider a as non zero Nat;

      (for p be prime Nat holds (p |-count a) <= (p |-count b)) implies a <= b

      proof

        assume for p be prime Nat holds (p |-count a) <= (p |-count b);

        then for p be Element of NAT st p is prime holds (p |-count a) <= (p |-count b);

        then

        consider c be Element of NAT such that

         B1: b = (a * c) by NAT_4: 20;

        c is non zero by B1;

        then (a * c) >= (a * 1) by NAT_1: 14, XREAL_1: 64;

        hence thesis by B1;

      end;

      hence thesis by A1;

    end;

    theorem :: NEWTON03:51

    

     NAT330: for a,b,c be Nat st a <> 1 & b <> 0 & c <> 0 & b > (a |-count c) holds not (a |^ b) divides c

    proof

      let a,b,c be Nat;

      assume a <> 1 & b <> 0 & c <> 0 ;

      then

       A2: (a |^ (a |-count c)) divides c & not (a |^ ((a |-count c) + 1)) divides c by NAT_3:def 7;

      assume b > (a |-count c);

      then b >= ((a |-count c) + 1) by NAT_1: 13;

      then

      consider k be Nat such that

       A3: b = (((a |-count c) + 1) + k) by NAT_1: 10;

      (a |^ b) = ((a |^ ((a |-count c) + 1)) * (a |^ k)) by A3, NEWTON: 8;

      hence thesis by A2, INT29;

    end;

    theorem :: NEWTON03:52

    

     CountD: for b be non zero Integer, a be Integer st |.a.| <> 1 holds (a |^ ( |.a.| |-count |.b.|)) divides b & not (a |^ (( |.a.| |-count |.b.|) + 1)) divides b

    proof

      let b be non zero Integer, a be Integer such that

       A0: |.a.| <> 1;

      reconsider k = |.a.|, l = |.b.| as Nat;

      

       A1: ( |.a.| |^ (k |-count l)) = |.(a |^ (k |-count l)).| & ( |.a.| |^ ((k |-count l) + 1)) = |.(a |^ ((k |-count l) + 1)).| by TAYLOR_2: 1;

      (k |^ (k |-count l)) divides l & not (k |^ ((k |-count l) + 1)) divides l by A0, NAT_3:def 7;

      hence thesis by A1, INT_2: 16;

    end;

    theorem :: NEWTON03:53

    

     CountD1: for b be non zero Integer, a be Integer st |.a.| <> 1 holds (a |^ n) divides b & not (a |^ (n + 1)) divides b implies n = ( |.a.| |-count |.b.|)

    proof

      let b be non zero Integer, a be Integer such that

       A0: |.a.| <> 1;

      reconsider k = |.a.|, l = |.b.| as Nat;

      

       A1: |.(a |^ n).| = ( |.a.| |^ n) & |.(a |^ (n + 1)).| = ( |.a.| |^ (n + 1)) by TAYLOR_2: 1;

      assume (a |^ n) divides b & not (a |^ (n + 1)) divides b;

      then ( |.a.| |^ n) divides |.b.| & not ( |.a.| |^ (n + 1)) divides |.b.| by A1, INT_2: 16;

      hence thesis by A0, NAT_3:def 7;

    end;

    theorem :: NEWTON03:54

    

     CD: for b be non zero Nat, a be non trivial Nat holds a divides b iff (a |-count (a gcd b)) = 1

    proof

      let b be non zero Nat, a be non trivial Nat;

      reconsider c = (a gcd b) as non zero Nat;

      

       A1: a > 1 by Def0;

      

       A2: c divides b by INT_2:def 2;

      thus a divides b implies (a |-count (a gcd b)) = 1

      proof

        assume a divides b;

        then (a gcd b) = |.a.| by NEWTON02: 3;

        hence thesis by NAT_3: 22, Def0;

      end;

      assume (a |-count (a gcd b)) = 1;

      then (a |^ 1) divides c by A1, NAT_3:def 7;

      hence thesis by A2, INT_2: 9;

    end;

    theorem :: NEWTON03:55

    for b,n be non zero Nat, a be non trivial Nat holds (a |-count (a gcd b)) = 1 iff ((a |^ n) |-count ((a gcd b) |^ n)) = 1

    proof

      let b,n be non zero Nat, a be non trivial Nat;

      a divides b iff (a |^ n) divides (b |^ n) by POWD;

      then (a |-count (a gcd b)) = 1 iff ((a |^ n) |-count ((a |^ n) gcd (b |^ n))) = 1 by CD;

      hence thesis by NEWTON027;

    end;

    theorem :: NEWTON03:56

    for b be non zero Nat, a be non trivial Nat holds (a |-count (a gcd b)) = 0 iff not (a |-count (a gcd b)) = 1

    proof

      let b be non zero Nat, a be non trivial Nat;

      reconsider c = (a gcd b) as non zero Nat;

      a > 1 by Def0;

      then

       L1: (a |-count (a gcd b)) = 0 iff not a divides (a gcd b) by NAT_3: 27;

      (a gcd b) divides b by INT_2:def 2;

      hence thesis by CD, INT_2: 9, L1;

    end;

    definition

      let a,b be Integer;

      :: NEWTON03:def6

      func a |-count b -> Nat equals ( |.a.| |-count |.b.|);

      coherence ;

    end

    definition

      let a be Integer;

      let b be non zero Integer;

      :: original: |-count

      redefine

      :: NEWTON03:def7

      func a |-count b means

      : Def6: (a |^ it ) divides b & not (a |^ (it + 1)) divides b;

      compatibility by A0, CountD, CountD1;

    end

    theorem :: NEWTON03:57

    

     NAT328: for p be prime Nat, a,b be non zero Integer holds (p |-count (a * b)) = ((p |-count a) + (p |-count b))

    proof

      let p be prime Nat, a,b be non zero Integer;

      reconsider k = |.a.|, l = |.b.| as non zero Nat;

      (p |-count (a * b)) = ( |.p.| |-count ( |.a.| * |.b.|)) by COMPLEX1: 65

      .= (( |.p.| |-count k) + ( |.p.| |-count l)) by NAT_3: 28;

      hence thesis;

    end;

    theorem :: NEWTON03:58

    

     Count0: for a be non trivial Nat, b be non zero Nat holds (a |^ (a |-count b)) <= b

    proof

      let a be non trivial Nat, b be non zero Nat;

      a <> 1 by Def0;

      then (a |^ (a |-count b)) divides b by NAT_3:def 7;

      hence thesis by NAT_D: 7;

    end;

    theorem :: NEWTON03:59

    

     Count1: for a be non trivial Nat, b be non zero Integer holds (a |^ n) divides b iff n <= (a |-count b)

    proof

      let a be non trivial Nat, b be non zero Integer;

      

       L0: a <> 1 by Def0;

      

       L1: (a |^ n) divides b implies n <= (a |-count b)

      proof

        assume

         A1: (a |^ n) divides b;

        (a |^ n) divides b & not (a |^ ((a |-count b) + 1)) divides b implies not (a |^ ((a |-count b) + 1)) divides (a |^ n) by INT_2: 9;

        then ((a |-count b) + 1) > n by L0, A1, Def6, NEWTON: 89;

        hence thesis by NAT_1: 13;

      end;

       not (a |^ n) divides b implies (a |-count b) < n

      proof

        assume

         A1: not (a |^ n) divides b;

         not (a |^ n) divides b & (a |^ (a |-count b)) divides b implies not (a |^ n) divides (a |^ (a |-count b)) by INT_2: 9;

        hence thesis by L0, A1, Def6, NEWTON: 89;

      end;

      hence thesis by L1;

    end;

    theorem :: NEWTON03:60

    

     Count2: for a be non trivial Nat, b be non zero Integer, n be non zero Nat holds (n * (a |-count b)) <= (a |-count (b |^ n)) < (n * ((a |-count b) + 1))

    proof

      let a be non trivial Nat, b be non zero Integer, n be non zero Nat;

      reconsider k = (a |-count b) as Nat;

      

       A0: ((a |^ k) |^ n) = (a |^ (k * n)) & ((a |^ (k + 1)) |^ n) = (a |^ ((k + 1) * n)) by NEWTON: 9;

      a <> 1 by NAT_2:def 1;

      then

       A1: (a |^ k) divides b & not (a |^ (k + 1)) divides b by Def6;

      ((a |^ k) gcd b) = |.(a |^ k).| & ((a |^ (k + 1)) gcd b) <> |.(a |^ (k + 1)).| by A1, NEWTON02: 3;

      then (((a |^ k) gcd b) |^ n) = ((a |^ k) |^ n) & (((a |^ (k + 1)) gcd b) |^ n) <> ((a |^ (k + 1)) |^ n) by WSIERP_1: 3;

      then (((a |^ k) |^ n) gcd (b |^ n)) = |.((a |^ k) |^ n).| & (((a |^ (k + 1)) |^ n) gcd (b |^ n)) <> |.((a |^ (k + 1)) |^ n).| by NEWTON027;

      hence thesis by Count1, A0, NEWTON02: 3;

    end;

    theorem :: NEWTON03:61

    for a be non trivial Nat, b,n be non zero Nat holds b < a implies (a |-count (b |^ n)) < n

    proof

      let a be non trivial Nat, b,n be non zero Nat;

      assume

       A1: b < a;

      b >= ( 0 + 1) by NAT_1: 13;

      then

       A2: (a |-count b) = 0 by A1, NAT_3: 23;

      (a |-count (b |^ n)) < (n * ((a |-count b) + 1)) by Count2;

      hence thesis by A2;

    end;

    theorem :: NEWTON03:62

    

     Count4: for a be non trivial Nat, b be non zero Nat holds b < (a |^ n) implies (a |-count b) < n

    proof

      let a be non trivial Nat, b be non zero Nat;

      assume b < (a |^ n);

      then (1 * (a |^ 0 )) divides b & not (a |^ ( 0 + n)) divides b by INT_2: 12, NAT_D: 7;

      hence thesis by Count1;

    end;

    theorem :: NEWTON03:63

    for a,b be non zero Nat, n be non trivial Nat holds ((a + b) |-count ((a |^ n) + (b |^ n))) < n

    proof

      let a,b be non zero Nat, n be non trivial Nat;

      reconsider m = (n - 1) as non zero Nat;

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

      then ((a + b) |^ (1 + m)) > ((a |^ (1 + m)) + (b |^ (1 + m))) by NEWTON01: 18;

      hence thesis by Count4;

    end;

    theorem :: NEWTON03:64

    for a,b be non zero Nat holds (a gcd b) = 1 iff (for c be non trivial Nat holds ((c |-count a) * (c |-count b)) = 0 )

    proof

      let a,b be non zero Nat;

      thus (a gcd b) = 1 implies (for c be non trivial Nat holds ((c |-count a) * (c |-count b)) = 0 )

      proof

        assume (a gcd b) = 1;

        then

         B1: (a,b) are_coprime ;

        for c be non trivial Nat holds ((c |-count a) * (c |-count b)) = 0

        proof

          let c be non trivial Nat;

          

           C1: c <> 1 by Def0;

          per cases ;

            suppose not c divides a;

            then (c |-count a) = 0 by C1, NAT_3: 27;

            hence thesis;

          end;

            suppose c divides a;

            then not c divides b by C1, B1, PYTHTRIP:def 1;

            then (c |-count b) = 0 by C1, NAT_3: 27;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      (for c be prime Nat holds ((c |-count a) * (c |-count b)) = 0 ) implies (a gcd b) = 1

      proof

        assume

         B1: for c be prime Nat holds ((c |-count a) * (c |-count b)) = 0 ;

        for c be prime Nat holds ( not c divides a) or ( not c divides b)

        proof

          let c be prime Nat;

          

           C1: c <> 1 by INT_2:def 4;

          ((c |-count a) * (c |-count b)) = 0 by B1;

          then ((c |-count a) = 0 or (c |-count b) = 0 );

          hence thesis by C1, NAT_3: 27;

        end;

        then (a,b) are_coprime by PYTHTRIP:def 2;

        hence thesis;

      end;

      hence thesis;

    end;

    

     ABS1: for a,b be Integer holds |.a.| <> |.b.| implies (a - b) <> 0 & (a + b) <> 0

    proof

      let a,b be Integer;

      assume

       A0: |.a.| <> |.b.|;

      per cases by ABSVALUE: 1;

        suppose

         A1: |.a.| = a;

        per cases by ABSVALUE: 1;

          suppose

           A2: |.b.| = b;

          a <> b & (a <> 0 or b <> 0 ) by A0;

          hence thesis by A1, A2;

        end;

          suppose |.b.| = ( - b);

          hence thesis by A0;

        end;

      end;

        suppose |.a.| = ( - a);

        hence thesis by A0;

      end;

    end;

    theorem :: NEWTON03:65

    for m be non zero even Nat, a,b be odd Nat st a <> b holds (2 |-count ((a |^ (2 * m)) - (b |^ (2 * m)))) >= ((2 |-count ((a |^ m) - (b |^ m))) + 1)

    proof

      let m be non zero even Nat, a,b be odd Nat such that

       A0: a <> b;

      reconsider c = ((a |^ (2 * m)) - (b |^ (2 * m))) as non zero Integer by A0, POW1;

      reconsider d = ((a |^ m) - (b |^ m)) as non zero Integer by A0, POW1;

      

       A1: 2 is non trivial;

      (2 |^ (2 |-count d)) divides d & not (2 |^ ((2 |-count d) + 1)) divides d by Def6;

      then (2 |^ ((2 |-count d) + 1)) divides c by Even;

      hence thesis by A1, Count1;

    end;

    theorem :: NEWTON03:66

    for m be non zero even Nat, a,b be odd Nat st a <> b holds (2 |-count ((a |^ (2 * m)) - (b |^ (2 * m)))) = ((2 |-count ((a |^ m) - (b |^ m))) + 1)

    proof

      let m be non zero even Nat, a,b be odd Nat such that

       A0: a <> b;

      reconsider c = ((a |^ m) + (b |^ m)) as non zero Nat;

      reconsider d = ((a |^ m) - (b |^ m)) as non zero Integer by A0, POW1;

      (a |^ (2 * m)) = ((a |^ m) |^ 2) & (b |^ (2 * m)) = ((b |^ m) |^ 2) by NEWTON: 9;

      then ((a |^ (2 * m)) - (b |^ (2 * m))) = (((a |^ m) - (b |^ m)) * ((a |^ m) + (b |^ m))) by NEWTON01: 1;

      

      then (2 |-count ((a |^ (2 * m)) - (b |^ (2 * m)))) = ((2 |-count c) + (2 |-count d)) by NAT328, INT_2: 28

      .= ((2 |-count ((a |^ m) - (b |^ m))) + 1) by SC1;

      hence thesis;

    end;

    theorem :: NEWTON03:67

    for p be prime Nat, a,b be Integer st |.a.| <> |.b.| holds (p |-count ((a |^ 2) - (b |^ 2))) = ((p |-count (a - b)) + (p |-count (a + b)))

    proof

      let p be prime Nat, a,b be Integer such that

       A1: |.a.| <> |.b.|;

      (a - b) <> 0 & (a + b) <> 0 by A1, ABS1;

      then

      reconsider t = |.(a - b).|, u = |.(a + b).| as non zero Nat;

      (p |-count ((a |^ 2) - (b |^ 2))) = (p |-count |.((a + b) * (a - b)).|) by NEWTON01: 1

      .= (p |-count (t * u)) by COMPLEX1: 65

      .= ((p |-count |.(a - b).|) + (p |-count |.(a + b).|)) by NAT_3: 28;

      hence thesis;

    end;

    theorem :: NEWTON03:68

    for p be prime Nat, a,b be Integer st |.a.| <> |.b.| holds (p |-count ((a |^ 3) - (b |^ 3))) = ((p |-count (a - b)) + (p |-count (((a |^ 2) + (a * b)) + (b |^ 2))))

    proof

      let p be prime Nat, a,b be Integer such that

       A1: |.a.| <> |.b.|;

      (a - b) <> 0 & (a + b) <> 0 by A1, ABS1;

      then

      reconsider t = |.(a - b).| as non zero Nat;

      

       A3: ( |.a.| |^ 2) = (a |^ 2) & ( |.b.| |^ 2) = (b |^ 2) by COMPLEX175;

      ((2 * |.a.|) * |.b.|) < (( |.a.| |^ 2) + ( |.b.| |^ 2)) by A1, NEWTON02: 55;

      then (2 * ( |.a.| * |.b.|)) < ((a |^ 2) + (b |^ 2)) by A3;

      then

       A4: (2 * |.(a * b).|) < ((a |^ 2) + (b |^ 2)) by COMPLEX1: 65;

      (2 * |.(a * b).|) >= (1 * |.(a * b).|) by XREAL_1: 64;

      then

       A5: ((a |^ 2) + (b |^ 2)) > |.(a * b).| by A4, XXREAL_0: 2;

       |.( - (a * b)).| >= ( - (a * b)) by ABSVALUE: 4;

      then |.(a * b).| >= ( - (a * b)) by COMPLEX1: 52;

      then ((a |^ 2) + (b |^ 2)) > ( - (a * b)) by A5, XXREAL_0: 2;

      then (((a |^ 2) + (b |^ 2)) + (a * b)) > (( - (a * b)) + (a * b)) by XREAL_1: 6;

      then

      reconsider u = |.(((a |^ 2) + (a * b)) + (b |^ 2)).| as non zero Nat;

      (p |-count ((a |^ 3) - (b |^ 3))) = (p |-count |.((((a |^ 2) + (b |^ 2)) + (a * b)) * (a - b)).|) by N3

      .= (p |-count (t * u)) by COMPLEX1: 65

      .= ((p |-count t) + (p |-count u)) by NAT_3: 28;

      hence thesis;

    end;

    theorem :: NEWTON03:69

    

     GL: for a,b be non zero Nat holds (a / (a gcd b)) = ((a lcm b) / b)

    proof

      let a,b be non zero Nat;

      (a / (a gcd b)) = ((a * b) / (b * (a gcd b))) by XCMPLX_1: 91

      .= (((a gcd b) * (a lcm b)) / (b * (a gcd b))) by NAT_D: 29

      .= ((a lcm b) / b) by XCMPLX_1: 91;

      hence thesis;

    end;

    theorem :: NEWTON03:70

    

     LCM2: for b be non zero Nat holds (a lcm ((a * n) + b)) = ((((a * n) / b) + 1) * (a lcm b))

    proof

      let b be non zero Nat;

      per cases ;

        suppose a is zero;

        hence thesis;

      end;

        suppose a is non zero;

        then

        reconsider a, b as non zero Nat;

        

         B2: (a * ((a * n) + b)) = ((a lcm ((a * n) + b)) * (a gcd ((a * n) + b))) by NAT_D: 29

        .= ((a lcm ((a * n) + b)) * (a gcd b)) by NEWTON02: 5;

        (((a * a) * n) + (a * b)) = ((a gcd b) * ((((a * a) * n) / (a gcd b)) + ((a * b) / (a gcd b)))) by XCMPLX_1: 114;

        

        then (a lcm ((a * n) + b)) = ((((a * a) * n) / (a gcd b)) + ((a * b) / (a gcd b))) by B2, XCMPLX_1: 5

        .= ((((a * n) * a) / (a gcd b)) + (((a lcm b) * (a gcd b)) / (a gcd b))) by NAT_D: 29

        .= ((((a * n) * a) / (a gcd b)) + (a lcm b)) by XCMPLX_1: 89

        .= (((a * n) * (a / (a gcd b))) + (a lcm b)) by XCMPLX_1: 74

        .= (((a * n) * ((a lcm b) / b)) + (a lcm b)) by GL

        .= ((((a * n) / b) * (a lcm b)) + (1 * (a lcm b))) by XCMPLX_1: 75;

        hence thesis;

      end;

    end;

    theorem :: NEWTON03:71

    for b be non zero Nat holds (a lcm (((n * a) + 1) * b)) = (((n * a) + 1) * (a lcm b))

    proof

      let b be non zero Nat;

      (a lcm ((a * (n * b)) + b)) = (((((a * n) * b) / b) + 1) * (a lcm b)) by LCM2;

      hence thesis by XCMPLX_1: 89;

    end;

    theorem :: NEWTON03:72

    for a be non trivial Nat, n,b be non zero Nat holds (a |-count b) >= (n * ((a |^ n) |-count b))

    proof

      let a be non trivial Nat, n,b be non zero Nat;

      

       A1: a <> 1 & b <> 0 by Def0;

      reconsider k = (a |^ n) as non trivial Nat;

      k <> 1 & b <> 0 by Def0;

      then (k |^ (k |-count b)) divides b & not (k |^ ((k |-count b) + 1)) divides b by NAT_3:def 7;

      then (a |^ (n * ((a |^ n) |-count b))) divides b by NEWTON: 9;

      hence thesis by A1, NAT330;

    end;

    theorem :: NEWTON03:73

    

     NEWTON0258: for a,b be odd Integer holds 4 divides (a - b) iff not 4 divides (a + b)

    proof

      let a,b be odd Integer;

      reconsider t = |.a.| as odd Nat;

      reconsider u = |.b.| as odd Nat;

      

       A0: 4 divides (t - u) iff not 4 divides (t + u) by NEWTON02: 58;

      4 divides (u - t) iff not 4 divides (u + t) by NEWTON02: 58;

      then

       A0a: 4 divides (u - t) iff not 4 divides ( - (u + t)) by INT_2: 10;

      per cases by ABSVALUE: 1;

        suppose

         A1: |.a.| = a;

        then

        reconsider a as Nat;

        per cases by ABSVALUE: 1;

          suppose |.b.| = b;

          hence thesis by NEWTON02: 58, A1;

        end;

          suppose |.b.| = ( - b);

          hence thesis by A0, A1;

        end;

      end;

        suppose

         A1: |.a.| = ( - a);

        per cases by ABSVALUE: 1;

          suppose |.b.| = b;

          hence thesis by A0a, A1;

        end;

          suppose |.b.| = ( - b);

          hence thesis by A0a, A1;

        end;

      end;

    end;

    theorem :: NEWTON03:74

    for a,b be odd Integer holds (2 |-count ((a |^ 2) + (b |^ 2))) = 1

    proof

      let a,b be odd Integer;

      reconsider t = (a |^ 2), u = (b |^ 2) as odd Nat;

      

       A2: (2 * 2) = (2 |^ 2) by NEWTON: 81;

      2 divides (a - b) & 2 divides (a + b) by ABIAN:def 1;

      then (2 * 2) divides ((a - b) * (a + b)) by NAT31;

      then 4 divides ((a |^ 2) - (b |^ 2)) by NEWTON01: 1;

      then (2 |^ 1) divides ((a |^ 2) + (b |^ 2)) & not (2 |^ (1 + 1)) divides ((a |^ 2) + (b |^ 2)) by ABIAN:def 1, A2, NEWTON0258;

      hence thesis by NAT_3:def 7;

    end;

    theorem :: NEWTON03:75

    for p be prime Nat, a,b be Nat st a <> b holds (p |-count (a + b)) >= (p |-count (a gcd b))

    proof

      let p be prime Nat, a,b be Nat such that

       A1: a <> b;

      

       A1a: a <> 0 or b <> 0 by A1;

      then

      consider k,l be Integer such that

       A2: a = ((a gcd b) * k) & b = ((a gcd b) * l) & (k,l) are_coprime by INT_2: 23;

      k >= 0 & l >= 0 by A1a, A2;

      then k in NAT & l in NAT by INT_1: 3;

      then

      reconsider k, l as Nat;

      

       A4: k is non zero or l is non zero by A2;

      (p |-count (a + b)) = (p |-count ((k + l) * (a gcd b))) by A2

      .= ((p |-count (k + l)) + (p |-count (a gcd b))) by A1a, A4, NAT_3: 28;

      hence thesis by NAT_1: 12;

    end;

    theorem :: NEWTON03:76

    

     DX: for a be non zero Integer, b be non trivial Nat, c be Integer holds a = ((b |^ (b |-count a)) * c) implies not b divides c

    proof

      let a be non zero Integer, b be non trivial Nat, c be Integer;

      

       A0: b > 1 by Def0;

      assume

       A1: a = ((b |^ (b |-count a)) * c);

      assume not thesis;

      then

      consider d be Integer such that

       A2: c = (b * d);

      a = (((b |^ (b |-count a)) * b) * d) by A1, A2;

      then (b * (b |^ (b |-count a))) divides a;

      then (b |^ ((b |-count a) + 1)) divides a by NEWTON: 6;

      hence contradiction by Def6, A0;

    end;

    registration

      let a be non zero Integer, b be non trivial Nat;

      cluster (a / (b |^ (b |-count a))) -> integer;

      coherence

      proof

        b > 1 by Def0;

        then (b |^ (b |-count a)) divides a by Def6;

        then

        consider c be Integer such that

         A1: a = ((b |^ (b |-count a)) * c);

        thus thesis by A1, XCMPLX_1: 89;

      end;

    end

    registration

      let a be non zero Integer;

      cluster (a / (2 |^ (2 |-count a))) -> integer;

      coherence

      proof

        2 is non trivial Nat by Def0;

        hence thesis;

      end;

      cluster (a / (2 |^ (2 |-count a))) -> odd;

      coherence

      proof

        

         A1: 2 is non trivial Nat by Def0;

        a = ((2 |^ (2 |-count a)) * (a / (2 |^ (2 |-count a)))) by XCMPLX_1: 87;

        hence thesis by A1, DX;

      end;

    end

    theorem :: NEWTON03:77

    

     NAT327: for a be non zero Integer, b be non trivial Nat holds (b |-count a) = 0 iff not b divides a

    proof

      let a be non zero Integer, b be non trivial Nat;

      reconsider c = |.a.| as non zero Nat;

      b > 1 by Def0;

      then not b divides |.a.| iff (b |-count |.a.|) = 0 by NAT_3: 27;

      hence thesis by INT_2: 16;

    end;

    registration

      let a be odd Integer;

      cluster (2 |-count a) -> zero;

      coherence

      proof

        2 is non trivial & a <> 0 & not 2 divides a;

        hence thesis by NAT327;

      end;

      reduce (a / (2 |^ (2 |-count a))) to a;

      reducibility

      proof

        (1 * (2 |^ (2 |-count a))) = 1;

        hence thesis;

      end;

    end

    theorem :: NEWTON03:78

    

     NAT332: for a be prime Nat, b be non zero Integer, c be Nat holds (a |-count (b |^ c)) = (c * (a |-count b))

    proof

      let a be prime Nat, b be non zero Integer, c be Nat;

      (a |-count (b |^ c)) = (a |-count ( |.b.| |^ c)) by TAYLOR_2: 1

      .= (c * (a |-count |.b.|)) by NAT_3: 32;

      hence thesis;

    end;

    theorem :: NEWTON03:79

    for a,b be non zero Nat, n be odd Nat holds (((a |^ (n + 2)) + (b |^ (n + 2))) / (a + b)) = (((a |^ (n + 1)) + (b |^ (n + 1))) - ((a * b) * (((a |^ n) + (b |^ n)) / (a + b))))

    proof

      let a,b be non zero Nat, n be odd Nat;

      reconsider m = ((n - 1) / 2) as Nat;

      ((a |^ (((2 * m) + 1) + 2)) + (b |^ (((2 * m) + 1) + 2))) = (((a + b) * ((a |^ (((2 * m) + 1) + 1)) + (b |^ (((2 * m) + 1) + 1)))) - ((a * b) * ((a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1))))) by RI3;

      

      then (((a |^ (((2 * m) + 1) + 2)) + (b |^ (((2 * m) + 1) + 2))) / (a + b)) = ((((a + b) * ((a |^ (((2 * m) + 1) + 1)) + (b |^ (((2 * m) + 1) + 1)))) / (a + b)) - (((a * b) * ((a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1)))) / (a + b))) by XCMPLX_1: 120

      .= (((a |^ (((2 * m) + 1) + 1)) + (b |^ (((2 * m) + 1) + 1))) - (((a * b) * ((a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1)))) / (a + b))) by XCMPLX_1: 89

      .= (((a |^ (((2 * m) + 1) + 1)) + (b |^ (((2 * m) + 1) + 1))) - ((a * b) * (((a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1))) / (a + b)))) by XCMPLX_1: 74;

      hence thesis;

    end;

    theorem :: NEWTON03:80

    

     Odd: for a,b be odd Integer, n be Nat holds (2 |-count ((a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1)))) = (2 |-count (a - b))

    proof

      let a,b be odd Integer, n be Nat;

      per cases ;

        suppose a = b;

        hence thesis;

      end;

        suppose

         A0: a <> b;

        then

        reconsider c = (a - b) as non zero Integer;

        defpred P[ Nat] means (2 |-count ((a |^ ((2 * $1) + 1)) - (b |^ ((2 * $1) + 1)))) = (2 |-count (a - b));

        

         A1: P[ 0 ];

        

         A2: P[k] implies P[(k + 1)]

        proof

          assume

           B0: P[k];

          reconsider d = ((a |^ ((2 * k) + 1)) - (b |^ ((2 * k) + 1))) as non zero Integer by A0, POW2;

          

           B1: (2 |^ (2 |-count c)) divides c & (2 |^ (2 |-count d)) divides d by Def6;

          reconsider x = (d / (2 |^ (2 |-count d))) as odd Integer;

          consider y be Integer such that

           B3: c = ((2 |^ (2 |-count c)) * y) by B1;

          

           B5: ((a |^ (((2 * k) + 1) + 2)) - (b |^ (((2 * k) + 1) + 2))) = (((a |^ ((2 * k) + 1)) * ((a |^ 2) - (b |^ 2))) + ((b |^ 2) * ((a |^ ((2 * k) + 1)) - (b |^ ((2 * k) + 1))))) by RI2

          .= (((a |^ ((2 * k) + 1)) * ((a |^ 2) - (b |^ 2))) + ((b |^ 2) * ((2 |^ (2 |-count (a - b))) * x))) by B0, XCMPLX_1: 87

          .= (((a |^ ((2 * k) + 1)) * ((a + b) * ((2 |^ (2 |-count (a - b))) * y))) + (((b |^ 2) * (2 |^ (2 |-count (a - b)))) * x)) by B3, NEWTON01: 1

          .= (((((a |^ ((2 * k) + 1)) * (a + b)) * y) + ((b |^ 2) * x)) * (2 |^ (2 |-count (a - b))));

          

           B6: 2 is non trivial;

          (2 |-count ((a |^ (((2 * k) + 1) + 2)) - (b |^ (((2 * k) + 1) + 2)))) = ((2 |-count ((((a |^ ((2 * k) + 1)) * (a + b)) * y) + ((b |^ 2) * x))) + (2 |-count (2 |^ (2 |-count (a - b))))) by B5, NAT328, INT_2: 28

          .= (2 |-count c) by B6;

          hence thesis;

        end;

        for x holds P[x] from NAT_1:sch 2( A1, A2);

        hence thesis;

      end;

    end;

    theorem :: NEWTON03:81

    for a,b be odd Integer, m be odd Nat holds (2 |-count ((a |^ m) + (b |^ m))) = (2 |-count (a + b))

    proof

      let a,b be odd Integer, m be odd Nat;

      reconsider c = ( - b) as odd Integer;

      reconsider n = ((m - 1) / 2) as Nat;

      (2 |-count ((a |^ m) + (( - c) |^ m))) = (2 |-count ((a |^ ((2 * n) + 1)) + ( - (c |^ ((2 * n) + 1))))) by POWER: 2

      .= (2 |-count ((a |^ ((2 * n) + 1)) - (c |^ ((2 * n) + 1))))

      .= (2 |-count (a - ( - b))) by Odd;

      hence thesis;

    end;

    theorem :: NEWTON03:82

    for a,b be odd Nat st a <> b holds 1 = ( min ((2 |-count (a - b)),(2 |-count (a + b))))

    proof

      let a,b be odd Nat such that

       A0: a <> b;

      reconsider k = |.(a - b).| as even Nat;

      reconsider l = (a + b) as even Nat;

      

       A1: (2 |^ 2) = (2 * 2) by NEWTON: 81;

      

       A2: (2 |^ 1) divides |.(a - b).| & (2 |^ 1) divides (a + b) by ABIAN:def 1;

      

       A3: (a - b) <> (b - b) by A0;

      then

       A4: (2 |-count |.(a - b).|) <> 0 & (2 |-count (a + b)) <> 0 by A2, NAT_3: 27;

      per cases ;

        suppose not 4 divides (a - b);

        then not |.(2 |^ (1 + 1)).| divides |.(a - b).| by A1, INT_2: 16;

        then 1 = (2 |-count |.(a - b).|) by A2, A3, NAT_3:def 7;

        hence thesis by A4, NAT_1: 14, XXREAL_0:def 9;

      end;

        suppose 4 divides (a - b);

        then not (2 |^ (1 + 1)) divides (a + b) by A1, NEWTON02: 58;

        then (2 |-count (a + b)) = 1 by A2, NAT_3:def 7;

        hence thesis by A4, NAT_1: 14, XXREAL_0:def 9;

      end;

    end;

    theorem :: NEWTON03:83

    

     DL: for a be non trivial Nat, b,c be non zero Integer holds (a |-count b) > (a |-count c) implies (a |^ (a |-count c)) divides b & not (a |^ (a |-count b)) divides c

    proof

      let a be non trivial Nat, b,c be non zero Integer;

      

       A1: a > 1 by Def0;

      reconsider n = (a |-count b), m = (a |-count c) as Nat;

      assume

       A2: (a |-count b) > (a |-count c);

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

      then

      consider k such that

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

       not (a |^ (m + 1)) divides c & (a |^ (m + 1)) divides ((a |^ (m + 1)) * (a |^ k)) by A1, Def6;

      then not ((a |^ (m + 1)) * (a |^ k)) divides c by INT_2: 9;

      then not (a |^ n) divides c & (a |^ n) divides b & (a |^ m) divides (a |^ n) by NEWTON: 8, A3, A1, Def6, A2, NEWTON: 89;

      hence thesis by INT_2: 9;

    end;

    theorem :: NEWTON03:84

    for a be non trivial Nat, b,c be non zero Integer holds (a |^ (a |-count b)) divides c & (a |^ (a |-count c)) divides b implies (a |-count b) = (a |-count c)

    proof

      let a be non trivial Nat, b,c be non zero Integer;

      assume (a |^ (a |-count b)) divides c & (a |^ (a |-count c)) divides b;

      then (a |-count b) >= (a |-count c) & (a |-count b) <= (a |-count c) by DL;

      hence thesis by XXREAL_0: 1;

    end;

    theorem :: NEWTON03:85

    

     PP: for a,b be Integer, m,n be Nat holds (a |^ n) divides b & not (a |^ m) divides b implies m > n

    proof

      let a,b be Integer, m,n be Nat;

      assume (a |^ n) divides b & not (a |^ m) divides b;

      then not (a |^ m) divides (a |^ n) by INT_2: 9;

      hence thesis by NEWTON89;

    end;

    theorem :: NEWTON03:86

    

     DN: for a be non trivial Nat, b,c be non zero Integer holds (a |-count b) = (a |-count c) & (a |^ n) divides b implies (a |^ n) divides c

    proof

      let a be non trivial Nat, b,c be non zero Integer;

      

       A0: a > 1 by Def0;

      assume

       A1: (a |-count b) = (a |-count c) & (a |^ n) divides b;

       not (a |^ ((a |-count b) + 1)) divides b by A0, Def6;

      then ((a |-count b) + 1) > n by A1, PP;

      then (a |-count b) >= n by NAT_1: 13;

      then

       A3: (a |^ n) divides (a |^ (a |-count b)) by NEWTON: 89;

      (a |^ (a |-count c)) divides c by A0, Def6;

      hence thesis by A1, A3, INT_2: 9;

    end;

    theorem :: NEWTON03:87

    

     DIC: for a be non trivial Nat, b,c be non zero Integer holds (a |-count b) = (a |-count c) iff (for n be Nat holds (a |^ n) divides b iff (a |^ n) divides c)

    proof

      let a be non trivial Nat, b,c be non zero Integer;

      

       A1: a > 1 by Def0;

      (a |-count b) <> (a |-count c) implies (ex n be Nat st ((a |^ n) divides b & not (a |^ n) divides c) or ((a |^ n) divides c & not (a |^ n) divides b))

      proof

        reconsider n = (a |-count b), m = (a |-count c) as Nat;

        assume (a |-count b) <> (a |-count c);

        per cases by XXREAL_0: 1;

          suppose n > m;

          then (a |^ n) divides b & not (a |^ n) divides c by DL, A1, Def6;

          hence thesis;

        end;

          suppose n < m;

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

          then (a |^ (n + 1)) divides (a |^ m) & (a |^ m) divides c by NEWTON: 89, Def6, A1;

          then (a |^ (n + 1)) divides c & not (a |^ (n + 1)) divides b by INT_2: 9, A1, Def6;

          hence thesis;

        end;

      end;

      hence thesis by DN;

    end;

    theorem :: NEWTON03:88

    for a,b be odd Integer st |.a.| <> |.b.| holds (2 |-count ((a - b) |^ 2)) <> (2 |-count ((a + b) |^ 2)) & (2 |-count ((a - b) |^ 2)) <> ((2 |-count (a |^ 2)) - (b |^ 2))

    proof

      let a,b be odd Integer such that

       A1: |.a.| <> |.b.|;

      

       A1a: (a - b) <> (a - a) by A1;

      reconsider c = (a - b) as non zero Integer by A1;

      reconsider d = (a + b) as non zero Integer by A1, ABS1;

      

       A2: (2 |-count ((a - b) |^ 2)) = (2 |-count (c |^ 2))

      .= (2 * (2 |-count (a - b))) by NAT332, INT_2: 28;

      

       A3: (2 |-count ((a + b) |^ 2)) = (2 |-count (d |^ 2))

      .= (2 * (2 |-count (a + b))) by NAT332, INT_2: 28;

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

      then

       A6: not ((2 |^ 2) divides (a - b) iff (2 |^ 2) divides (a + b)) by NEWTON0258;

      (a + b) <> 0 & 2 is non trivial by A1, ABS1;

      hence thesis by A2, A3, A6, A1a, DIC;

    end;

    theorem :: NEWTON03:89

    

     MOB16: for b be non trivial Nat, a be non zero Integer holds (b |-count a) <> 0 iff b divides a

    proof

      let b be non trivial Nat, a be non zero Integer;

      (b |-count |.a.|) <> 0 iff b divides |.a.|

      proof

        b <> 1 & a <> 0 by NAT_2:def 1;

        hence thesis by NAT_3: 27;

      end;

      hence thesis by INT_2: 16;

    end;

    theorem :: NEWTON03:90

    for b be non trivial Nat, a be non zero Nat holds (b |-count a) = 0 iff (a mod b) <> 0

    proof

      let b be non trivial Nat, a be non zero Nat;

      per cases ;

        suppose

         A1: (b |-count a) <> 0 ;

        then b divides a by MOB16;

        hence thesis by A1, PEPIN: 6;

      end;

        suppose

         A1: (b |-count a) = 0 ;

        then not b divides a by MOB16;

        hence thesis by A1, PEPIN: 6;

      end;

    end;

    theorem :: NEWTON03:91

    for p be prime Nat, a be non trivial Nat holds (a |-count p) <= 1

    proof

      let p be prime Nat, a be non trivial Nat;

      a > 1 by Def0;

      then (a |-count p) = 0 or a = p by NAT_3: 24;

      hence thesis by Def0, NAT_3: 22;

    end;

    theorem :: NEWTON03:92

    

     Count7: for a,b be non trivial Nat, c be non zero Nat holds (a |^ ((a |-count b) * (b |-count c))) <= c

    proof

      let a,b be non trivial Nat, c be non zero Nat;

      

       A1: (a |^ ((a |-count b) * (b |-count c))) = ((a |^ (a |-count b)) |^ (b |-count c)) by NEWTON: 9;

      

       A2: ((a |^ (a |-count b)) |^ (b |-count c)) <= (b |^ (b |-count c)) by Count0, NEWTON02: 41;

      (b |^ (b |-count c)) <= c by Count0;

      hence thesis by A1, A2, XXREAL_0: 2;

    end;

    theorem :: NEWTON03:93

    for p be prime Nat, a be non trivial Nat, b be non zero Nat holds (a |-count (p |^ b)) <= b

    proof

      let p be prime Nat, a be non trivial Nat, b be non zero Nat;

      

       A1: a > 1 by Def0;

      per cases ;

        suppose p = a;

        hence thesis by Def0, NAT_3: 25;

      end;

        suppose p <> a;

        then (a |-count p) = 0 by A1, NAT_3: 24;

        then not (a |^ ( 0 + b)) divides (p |^ b) by MOB16, WSIERP_1: 26;

        hence thesis by Count1;

      end;

    end;

    theorem :: NEWTON03:94

    for p be prime Nat, a be non trivial Nat holds ((p |-count a) * (a |-count (p |^ n))) <= n

    proof

      let p be prime Nat, a be non trivial Nat;

      

       A1: p > 1 by NAT_4: 14;

      (p |^ ((p |-count a) * (a |-count (p |^ n)))) <= (p |^ n) by Count7;

      hence thesis by A1, PEPIN: 66;

    end;

    theorem :: NEWTON03:95

    for a,b be non trivial Nat, c be non zero Nat holds ((a |-count b) * (b |-count c)) <= (a |-count c)

    proof

      let a,b be non trivial Nat, c be non zero Nat;

      a <> 1 & b <> 1 by Def0;

      then

       A2: (a |^ (a |-count b)) divides b & (b |^ (b |-count c)) divides c & (a |^ (a |-count c)) divides c & not (a |^ ((a |-count c) + 1)) divides c by NAT_3:def 7;

      then ((a |^ (a |-count b)) |^ (b |-count c)) divides c by LmY;

      then (a |^ ((a |-count b) * (b |-count c))) divides c by NEWTON: 9;

      then ((a |-count b) * (b |-count c)) < ((a |-count c) + 1) by A2, LmX;

      hence thesis by NAT_1: 13;

    end;

    theorem :: NEWTON03:96

    for a be non zero Nat, b be odd Nat holds (2 |-count (a * b)) = (2 |-count a)

    proof

      let a be non zero Nat, b be odd Nat;

      (2 |-count (a * b)) = ((2 |-count a) + (2 |-count b)) by INT_2: 28, NAT_3: 28

      .= ((2 |-count a) + 0 );

      hence thesis;

    end;

    theorem :: NEWTON03:97

    for a be non trivial Nat holds ((a |^ (n + 1)) + (a |^ n)) < (a |^ (n + 2))

    proof

      let a be non trivial Nat;

      

       A0: not (a = 0 or a = 1) by NAT_2:def 1;

      then

       A0a: a >= 2 by NAT_1: 23;

      

       A1: (a |^ ((n + 1) + 1)) = (a * (a |^ (n + 1))) by NEWTON: 6;

      

       A2: (a * (a |^ (n + 1))) >= (2 * (a |^ (n + 1))) by A0, NAT_1: 23, XREAL_1: 64;

      a > 1 by A0a, XXREAL_0: 2;

      then (a * (a |^ n)) > (1 * (a |^ n)) by XREAL_1: 68;

      then (a |^ (n + 1)) > (a |^ n) by NEWTON: 6;

      then ((a |^ (n + 1)) + (a |^ (n + 1))) > ((a |^ (n + 1)) + (a |^ n)) by XREAL_1: 6;

      hence thesis by A1, A2, XXREAL_0: 2;

    end;

    theorem :: NEWTON03:98

    

     LmNT: for a be non trivial Nat holds (((a + 1) |^ n) + ((a + 1) |^ n)) < ((a + 1) |^ (n + 1))

    proof

      let a be non trivial Nat;

      a <> 0 & a <> 1 by NAT_2:def 1;

      then (a + 1) > 2 by NAT_1: 13, NAT_1: 23;

      then ((a + 1) * ((a + 1) |^ n)) > (2 * ((a + 1) |^ n)) by XREAL_1: 68;

      hence thesis by NEWTON: 6;

    end;

    theorem :: NEWTON03:99

    for a be non trivial odd Nat holds ((a |^ n) + (a |^ n)) < (a |^ (n + 1))

    proof

      let a be non trivial odd Nat;

      (a - 1) <> 1 & (a - 1) <> 0 ;

      then

      reconsider b = (a - 1) as non trivial Nat by NAT_2:def 1;

      (((b + 1) |^ n) + ((b + 1) |^ n)) < ((b + 1) |^ (n + 1)) by LmNT;

      hence thesis;

    end;

    theorem :: NEWTON03:100

    for p be non trivial Nat holds not a divides b implies ((p |^ a) |^ c) <> (p |^ b)

    proof

      let p be non trivial Nat;

      assume

       A1: not a divides b;

      

       A2: (p |^ (a * c)) = (p |^ b) iff ((p |^ a) |^ c) = (p |^ b) by NEWTON: 9;

      p > 1 by Def0;

      hence thesis by A1, A2, PEPIN: 30;

    end;

    

     LmC10: for a be Integer, b be non zero Integer, n be non zero Nat holds a = (b |^ n) implies (for p be prime Nat holds n divides (p |-count a))

    proof

      let a be Integer, b be non zero Integer, n be non zero Nat;

      assume

       A1: a = (b |^ n);

      for p be prime Nat holds n divides (p |-count a)

      proof

        let p be prime Nat;

        (p |-count (b |^ n)) = (n * (p |-count b)) by NAT332;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: NEWTON03:101

    for a,b be non zero Integer, n be non zero Nat holds (ex p be prime Nat st not n divides (p |-count a)) implies a <> (b |^ n) by LmC10;

    theorem :: NEWTON03:102

    for a,b be non zero Integer, n be non zero Nat holds a = (b |^ n) implies (for p be prime Nat holds n divides (p |-count a)) by LmC10;

    theorem :: NEWTON03:103

    for a,b be positive Real, n be non trivial Nat holds ((a + b) |^ n) > ((a |^ n) + (b |^ n))

    proof

      let a,b be positive Real, n be non trivial Nat;

      reconsider m = (n - 1) as non zero Nat;

      reconsider c = ( max (a,b)), d = ( min (a,b)) as positive Real;

      

       A1: (c * (c |^ m)) = (c |^ (m + 1)) & (d * (d |^ m)) = (d |^ (m + 1)) & ((c + d) * ((c + d) |^ m)) = ((c + d) |^ (m + 1)) by NEWTON: 6;

      

       A2: (c |^ n) = ( max ((a |^ n),(b |^ n))) & (d |^ n) = ( min ((a |^ n),(b |^ n))) by MM1;

      (c + d) > (c + 0 ) & (c + d) > ( 0 + d) by XREAL_1: 6;

      then ((c + d) |^ m) > (c |^ m) & ((c + d) |^ m) > (d |^ m) by NEWTON02: 40;

      then (c * ((c + d) |^ m)) > (c * (c |^ m)) & (d * ((c + d) |^ m)) > (d * (d |^ m)) by XREAL_1: 68;

      then (c * ((c + d) |^ m)) > (c |^ (m + 1)) & (d * ((c + d) |^ m)) > (d |^ (m + 1)) by NEWTON: 6;

      then

       A3: ((c * ((c + d) |^ m)) + (d * ((c + d) |^ m))) > ((c |^ (m + 1)) + (d |^ (m + 1))) by XREAL_1: 8;

      ((a + b) |^ (m + 1)) = ((c * ((c + d) |^ m)) + (d * ((c + d) |^ m))) by A1, MinMax;

      hence thesis by A2, A3, MinMax;

    end;

    theorem :: NEWTON03:104

    for a,b be non zero Integer, p be odd prime Nat st |.a.| <> |.b.| & not p divides b holds (p |-count ((a |^ 2) - (b |^ 2))) = ( max ((p |-count (a - b)),(p |-count (a + b))))

    proof

      let a,b be non zero Integer, p be odd prime Nat such that

       A1: |.a.| <> |.b.| & not p divides b;

      

       A2: p is non trivial & (a - b) <> 0 & (a + b) <> 0 by A1, ABS1;

      p divides (a - b) implies not p divides (a + b) by A1, SUD;

      then

       A3: (p |-count (a - b)) <> 0 implies (p |-count (a + b)) = 0 by A2, NAT327;

      (p |-count ((a |^ 2) - (b |^ 2))) = (p |-count ((a - b) * (a + b))) by NEWTON01: 1

      .= ((p |-count (a - b)) + (p |-count (a + b))) by A2, NAT328;

      hence thesis by A3, XXREAL_0:def 10;

    end;

    theorem :: NEWTON03:105

    for a be non trivial Nat, b be non zero Integer holds (a |-count ((a |^ n) * b)) = (n + (a |-count b))

    proof

      let a be non trivial Nat, b be non zero Integer;

      

       A0: ((a |^ n) * (a |^ (a |-count b))) = (a |^ ((a |-count b) + n)) & ((a |^ n) * (a |^ ((a |-count b) + 1))) = (a |^ (((a |-count b) + 1) + n)) by NEWTON: 8;

      

       A1: a <> 1 by Def0;

      then (a |^ (a |-count b)) divides b & not (a |^ ((a |-count b) + 1)) divides b by Def6;

      then (a |^ ((a |-count b) + n)) divides ((a |^ n) * b) & not (a |^ (((a |-count b) + n) + 1)) divides ((a |^ n) * b) by INT_4: 7, A0;

      hence thesis by A1, Def6;

    end;