newton01.miz



    begin

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

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

a1,b1,c1,d1 for Complex;

    registration

      let u,v be even Integer;

      cluster (u - v) -> even;

      coherence

      proof

        ((u + 1) - (v + 1)) is even;

        hence thesis;

      end;

    end

    registration

      let u be odd Integer;

      let k;

      cluster (u |^ k) -> odd;

      coherence

      proof

        

         A1: 2 divides u iff |.2.| divides |.u.| by INT_2: 16;

        

         A2: |.u.| is odd implies ( |.u.| |^ k) is odd by PEPIN: 20;

         |.(u |^ k).| = ( |.u.| |^ k) by TAYLOR_2: 1;

        hence thesis by A1, A2, INT_2: 16;

      end;

    end

    registration

      let k be positive Nat;

      let u be even Integer;

      cluster (u |^ k) -> even;

      coherence

      proof

        

         A0: 2 = |.2.|;

        

         A2: k > 0 & |.u.| is even implies ( |.u.| |^ k) is even by PEPIN: 21;

         |.(u |^ k).| = ( |.u.| |^ k) by TAYLOR_2: 1;

        hence thesis by A2, A0, ABIAN:def 1, INT_2: 16;

      end;

    end

    

     Lm10: ((a1 + b1) |^ 2) = (((a1 |^ 2) + ((2 * a1) * b1)) + (b1 |^ 2))

    proof

      ((a1 + b1) |^ 2) = ((a1 + b1) ^2 ) & (a1 |^ 2) = (a1 ^2 ) & (b1 |^ 2) = (b1 ^2 ) by NEWTON: 81;

      hence thesis by SQUARE_1: 4;

    end;

    theorem :: NEWTON01:1

    

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

    proof

      (a1 |^ 2) = (a1 ^2 ) & (b1 |^ 2) = (b1 ^2 ) by NEWTON: 81;

      hence thesis by SQUARE_1: 8;

    end;

    theorem :: NEWTON01:2

    

     Th2: ((((2 * a1) + 1) |^ 2) + (((2 * (a1 |^ 2)) + (2 * a1)) |^ 2)) = ((((2 * (a1 |^ 2)) + (2 * a1)) + 1) |^ 2)

    proof

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

      .= (((((((2 * (a1 |^ 2)) * (2 * (a1 |^ 2))) + ((2 * a1) * (2 * a1))) + 1) + ((2 * (2 * a1)) * (2 * (a1 |^ 2)))) + (2 * (2 * (a1 |^ 2)))) + (2 * (2 * a1)))

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

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

      .= (((((2 * (a1 |^ 2)) |^ 2) + ((2 * (2 * (a1 |^ 2))) * (2 * a1))) + ((2 * a1) |^ 2)) + ((((2 * 2) * (a1 |^ 2)) + ((2 * (2 * a1)) * 1)) + (1 |^ 2)))

      .= ((((2 * (a1 |^ 2)) + (2 * a1)) |^ 2) + ((((2 * 2) * (a1 |^ 2)) + ((2 * (2 * a1)) * 1)) + (1 |^ 2))) by Lm10

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

      .= ((((2 * (a1 |^ 2)) + (2 * a1)) |^ 2) + ((((2 * a1) |^ 2) + ((2 * (2 * a1)) * 1)) + (1 |^ 2))) by NEWTON: 7;

      hence thesis by Lm10;

    end;

    theorem :: NEWTON01:3

    (((a1 |^ 2) + (a1 * b1)) + (b1 |^ 2)) = (((3 * ((a1 + b1) |^ 2)) + ((a1 - b1) |^ 2)) / 4)

    proof

      

       A1: ((a1 + b1) |^ 2) = ((a1 + b1) * (a1 + b1)) by NEWTON: 81

      .= (((a1 * a1) + ((2 * a1) * b1)) + (b1 * b1))

      .= (((a1 |^ 2) + ((2 * a1) * b1)) + (b1 * b1)) by NEWTON: 81

      .= (((a1 |^ 2) + ((2 * a1) * b1)) + (b1 |^ 2)) by NEWTON: 81;

      ((a1 - b1) |^ 2) = ((a1 - b1) * (a1 - b1)) by NEWTON: 81

      .= (((a1 * a1) - ((2 * a1) * b1)) + (b1 * b1))

      .= (((a1 |^ 2) - ((2 * a1) * b1)) + (b1 * b1)) by NEWTON: 81

      .= (((a1 |^ 2) - ((2 * a1) * b1)) + (b1 |^ 2)) by NEWTON: 81;

      hence thesis by A1;

    end;

    theorem :: NEWTON01:4

    a is odd implies ex b st ((a |^ 2) + (b |^ 2)) = ((b + 1) |^ 2)

    proof

      assume a is odd;

      then

      consider k be Nat such that

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

      ((((2 * k) + 1) |^ 2) + (((2 * (k |^ 2)) + (2 * k)) |^ 2)) = ((((2 * (k |^ 2)) + (2 * k)) + 1) |^ 2) by Th2;

      hence thesis by A2;

    end;

    theorem :: NEWTON01:5

    

     Th5: (((((a1 |^ m) + (b1 |^ m)) * ((a1 |^ n) - (b1 |^ n))) + (((a1 |^ n) + (b1 |^ n)) * ((a1 |^ m) - (b1 |^ m)))) / 2) = ((a1 |^ (m + n)) - (b1 |^ (m + n)))

    proof

      (((((a1 |^ m) + (b1 |^ m)) * ((a1 |^ n) - (b1 |^ n))) + (((a1 |^ n) + (b1 |^ n)) * ((a1 |^ m) - (b1 |^ m)))) / 2) = ((((((a1 |^ m) * (a1 |^ n)) - ((b1 |^ m) * (b1 |^ n))) + ((a1 |^ n) * (a1 |^ m))) - ((b1 |^ n) * (b1 |^ m))) / 2)

      .= (((((a1 |^ (m + n)) - ((b1 |^ m) * (b1 |^ n))) + ((a1 |^ n) * (a1 |^ m))) - ((b1 |^ n) * (b1 |^ m))) / 2) by NEWTON: 8

      .= (((((a1 |^ (m + n)) - (b1 |^ (m + n))) + ((a1 |^ n) * (a1 |^ m))) - ((b1 |^ n) * (b1 |^ m))) / 2) by NEWTON: 8

      .= (((((a1 |^ (m + n)) - (b1 |^ (m + n))) + (a1 |^ (m + n))) - ((b1 |^ n) * (b1 |^ m))) / 2) by NEWTON: 8

      .= (((((a1 |^ (m + n)) - (b1 |^ (m + n))) + (a1 |^ (n + m))) - (b1 |^ (n + m))) / 2) by NEWTON: 8

      .= ((a1 |^ (m + n)) - (b1 |^ (m + n)));

      hence thesis;

    end;

    

     Lm0: ((a |^ 0 ) + (b |^ 0 )) > (c |^ 0 )

    proof

      (a |^ 0 ) = 1 & (b |^ 0 ) = 1 & (c |^ 0 ) = 1 by NEWTON: 4;

      hence thesis;

    end;

    theorem :: NEWTON01:6

    

     Th6: ((a |^ m) + (b |^ m)) <= (c |^ m) implies a <= c

    proof

      assume

       A0: ((a |^ m) + (b |^ m)) <= (c |^ m);

      m = 0 implies ((a |^ m) + (b |^ m)) > (c |^ m) by Lm0;

      then

       A2e: ( 0 + 1) <= m by A0, NAT_1: 13;

      ((a |^ m) + (b |^ m)) <= ((c |^ m) + (b |^ m)) by A0, NAT_1: 12;

      then (((a |^ m) + (b |^ m)) - (b |^ m)) <= (((c |^ m) + (b |^ m)) - (b |^ m)) by XREAL_1: 9;

      hence thesis by A2e, PREPOWER: 10;

    end;

    theorem :: NEWTON01:7

    ((a1 + b1) |^ (n + 1)) = (((a1 |^ (n + 1)) + (b1 |^ (n + 1))) + ((a1 * b1) * c1)) implies ((a1 + b1) |^ (n + 2)) = (((a1 |^ (n + 2)) + (b1 |^ (n + 2))) + ((a1 * b1) * (((a1 |^ n) + (b1 |^ n)) + (c1 * (a1 + b1)))))

    proof

      assume ((a1 + b1) |^ (n + 1)) = (((a1 |^ (n + 1)) + (b1 |^ (n + 1))) + ((a1 * b1) * c1));

      

      then ((a1 + b1) |^ ((n + 1) + 1)) = ((a1 + b1) * (((a1 |^ (n + 1)) + (b1 |^ (n + 1))) + ((a1 * b1) * c1))) by NEWTON: 6

      .= (((((a1 * (a1 |^ (n + 1))) + (b1 * (a1 |^ (n + 1)))) + (a1 * (b1 |^ (n + 1)))) + (b1 * (b1 |^ (n + 1)))) + ((((a1 + b1) * a1) * b1) * c1))

      .= (((((a1 |^ ((n + 1) + 1)) + (b1 * (a1 |^ (n + 1)))) + (a1 * (b1 |^ (n + 1)))) + (b1 * (b1 |^ (n + 1)))) + ((a1 * b1) * (c1 * (a1 + b1)))) by NEWTON: 6

      .= (((((a1 |^ (n + 2)) + (b1 * (a1 * (a1 |^ n)))) + (a1 * (b1 |^ (n + 1)))) + (b1 * (b1 |^ (n + 1)))) + (((a1 * b1) * c1) * (a1 + b1))) by NEWTON: 6

      .= (((((a1 |^ (n + 2)) + ((b1 * a1) * (a1 |^ n))) + (a1 * (b1 * (b1 |^ n)))) + (b1 * (b1 |^ (n + 1)))) + (((a1 * b1) * c1) * (a1 + b1))) by NEWTON: 6

      .= (((((a1 |^ (n + 2)) + ((b1 * a1) * (a1 |^ n))) + ((a1 * b1) * (b1 |^ n))) + (b1 |^ ((n + 1) + 1))) + ((a1 * b1) * ((c1 * a1) + (c1 * b1)))) by NEWTON: 6

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

      hence thesis;

    end;

    theorem :: NEWTON01:8

    

     Th8: (((((a1 |^ m) + (b1 |^ m)) * ((a1 |^ n) + (b1 |^ n))) + (((a1 |^ n) - (b1 |^ n)) * ((a1 |^ m) - (b1 |^ m)))) / 2) = ((a1 |^ (m + n)) + (b1 |^ (m + n)))

    proof

      

      thus (((((a1 |^ m) + (b1 |^ m)) * ((a1 |^ n) + (b1 |^ n))) + (((a1 |^ n) - (b1 |^ n)) * ((a1 |^ m) - (b1 |^ m)))) / 2) = ((((((a1 |^ m) * (a1 |^ n)) + ((b1 |^ m) * (b1 |^ n))) + ((a1 |^ n) * (a1 |^ m))) + ((b1 |^ n) * (b1 |^ m))) / 2)

      .= (((((a1 |^ (m + n)) + ((b1 |^ m) * (b1 |^ n))) + ((a1 |^ n) * (a1 |^ m))) + ((b1 |^ n) * (b1 |^ m))) / 2) by NEWTON: 8

      .= (((((a1 |^ (m + n)) + (b1 |^ (m + n))) + ((a1 |^ n) * (a1 |^ m))) + ((b1 |^ n) * (b1 |^ m))) / 2) by NEWTON: 8

      .= (((((a1 |^ (m + n)) + (b1 |^ (m + n))) + (a1 |^ (m + n))) + ((b1 |^ n) * (b1 |^ m))) / 2) by NEWTON: 8

      .= (((((a1 |^ (m + n)) + (b1 |^ (m + n))) + (a1 |^ (n + m))) + (b1 |^ (n + m))) / 2) by NEWTON: 8

      .= ((a1 |^ (m + n)) + (b1 |^ (m + n)));

    end;

    

     Lm3a: a <= b implies (a |^ n) <= (b |^ n)

    proof

      per cases by NAT_1: 14;

        suppose

         A1: n = 0 ;

        (a |^ 0 ) = 1 & (b |^ 0 ) = 1 by NEWTON: 4;

        hence thesis by A1;

      end;

        suppose

         A1: 1 <= n;

        assume a <= b;

        per cases by XXREAL_0: 1;

          suppose a < b;

          hence thesis by A1, PREPOWER: 10;

        end;

          suppose a = b;

          hence thesis;

        end;

      end;

    end;

    

     Lm4a: (a |^ n) > (b |^ n) implies (a |^ (n + 1)) > (b |^ (n + 1))

    proof

      assume

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

      

       A2: (a |^ (n + 1)) = (a * (a |^ n)) & (b |^ (n + 1)) = (b * (b |^ n)) by NEWTON: 6;

      

       A3: a > b by A1, Lm3a;

      then

       A4: (a * (a |^ n)) > (a * (b |^ n)) by A1, XREAL_1: 68;

      ((b |^ n) * a) >= ((b |^ n) * b) by A3, XREAL_1: 66;

      hence thesis by A2, A4, XXREAL_0: 2;

    end;

    

     Lm5c: b > 0 implies a < (a + (b |^ m))

    proof

      assume b > 0 ;

      then (b |^ m) > 0 by PREPOWER: 6;

      hence thesis by NAT_1: 16;

    end;

    

     Lm5d: ((a + x) |^ m) >= ((a |^ m) + (b |^ m)) & a > 0 & b > 0 implies x > 0

    proof

      assume ((a + x) |^ m) >= ((a |^ m) + (b |^ m)) & a > 0 & b > 0 ;

      then x <> 0 by Lm5c;

      hence thesis;

    end;

    theorem :: NEWTON01:9

    

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

    proof

      

      thus ((a1 |^ (m + 1)) + (b1 |^ (m + 1))) = (((((a1 |^ m) + (b1 |^ m)) * (a1 + b1)) + (((a1 |^ 1) - (b1 |^ 1)) * ((a1 |^ m) - (b1 |^ m)))) / 2) by Th8

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

    end;

    theorem :: NEWTON01:10

    

     Th10: ((a - b) * ((a |^ m) - (b |^ m))) >= 0

    proof

      

       A0: (a |^ 0 ) = 1 & (b |^ 0 ) = 1 by NEWTON: 4;

      per cases ;

        suppose

         A1: ((a |^ m) - (b |^ m)) >= 0 ;

        then (((a |^ m) - (b |^ m)) + (b |^ m)) >= ( 0 + (b |^ m)) by XREAL_1: 7;

        then a >= b or m < 1 by PREPOWER: 10;

        then (a - b) >= (b - b) or m = 0 by XREAL_1: 9, NAT_1: 14;

        hence thesis by A0, A1;

      end;

        suppose

         A2: ((a |^ m) - (b |^ m)) < 0 ;

        then (((a |^ m) - (b |^ m)) + (b |^ m)) < ( 0 + (b |^ m)) by XREAL_1: 8;

        then (a - b) < (b - b) by Lm3a, XREAL_1: 9;

        hence thesis by A2;

      end;

    end;

    theorem :: NEWTON01:11

    ((a |^ (m + 1)) + (b |^ (m + 1))) >= ((((a |^ m) + (b |^ m)) * (a + b)) / 2)

    proof

      

       A1: ((a |^ (m + 1)) + (b |^ (m + 1))) = (((((a |^ m) + (b |^ m)) * (a + b)) + ((a - b) * ((a |^ m) - (b |^ m)))) / 2) by Th9

      .= (((((a |^ m) + (b |^ m)) * (a + b)) / 2) + (((a - b) * ((a |^ m) - (b |^ m))) / 2));

      ((((a |^ m) + (b |^ m)) * (a + b)) + ((a - b) * ((a |^ m) - (b |^ m)))) >= (((a |^ m) + (b |^ m)) * (a + b)) by Th10, XREAL_1: 31;

      then (((((a |^ m) + (b |^ m)) * (a + b)) + ((a - b) * ((a |^ m) - (b |^ m)))) / 2) >= ((((a |^ m) + (b |^ m)) * (a + b)) / 2) by XREAL_1: 72;

      hence thesis by A1;

    end;

    theorem :: NEWTON01:12

    ((a |^ m) + (b |^ m)) <= (c |^ m) implies ex x st ((a |^ m) + (b |^ m)) <= ((a + x) |^ m)

    proof

      assume

       A1: ((a |^ m) + (b |^ m)) <= (c |^ m);

      then ex x st c = (a + x) by Th6, NAT_1: 10;

      hence thesis by A1;

    end;

    theorem :: NEWTON01:13

    

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

    proof

      

      thus ((a1 |^ (m + 1)) - (b1 |^ (m + 1))) = (((((a1 |^ m) + (b1 |^ m)) * (a1 - b1)) + (((a1 |^ 1) + (b1 |^ 1)) * ((a1 |^ m) - (b1 |^ m)))) / 2) by Th5

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

    end;

    

     Lm16: ((a1 |^ m) - (b1 |^ m)) = ((a1 - b1) * t) implies ((a1 |^ (m + 1)) - (b1 |^ (m + 1))) = (((a1 - b1) * (((t * (a1 + b1)) + (a1 |^ m)) + (b1 |^ m))) / 2)

    proof

      assume ((a1 |^ m) - (b1 |^ m)) = ((a1 - b1) * t);

      then ((a1 |^ (m + 1)) - (b1 |^ (m + 1))) = (((((a1 |^ m) + (b1 |^ m)) * (a1 - b1)) + ((a1 + b1) * ((a1 - b1) * t))) / 2) by Th13;

      hence thesis;

    end;

    

     Lm17: ((a1 |^ (m + 1)) - (b1 |^ (m + 1))) = (((a1 - b1) * (((t * (a1 + b1)) + (a1 |^ m)) + (b1 |^ m))) / 2) & (a1 + b1) <> 0 implies ((a1 |^ m) - (b1 |^ m)) = ((a1 - b1) * t)

    proof

      assume

       A1: ((a1 |^ (m + 1)) - (b1 |^ (m + 1))) = (((a1 - b1) * (((t * (a1 + b1)) + (a1 |^ m)) + (b1 |^ m))) / 2) & (a1 + b1) <> 0 ;

      then (((((a1 |^ m) + (b1 |^ m)) * (a1 - b1)) + ((a1 + b1) * ((a1 |^ m) - (b1 |^ m)))) / 2) = (((a1 - b1) * (((t * (a1 + b1)) + (a1 |^ m)) + (b1 |^ m))) / 2) by Th13;

      then ((a1 + b1) * ((a1 |^ m) - (b1 |^ m))) = (((a1 - b1) * t) * (a1 + b1));

      hence thesis by A1, XCMPLX_1: 5;

    end;

    theorem :: NEWTON01:14

    

     Th14: ((a |^ (m + 1)) - (b |^ (m + 1))) = (((a - b) * (((t * (a + b)) + (a |^ m)) + (b |^ m))) / 2) iff ((a |^ m) - (b |^ m)) = ((a - b) * t)

    proof

      (a + b) = 0 implies ((a |^ m) - (b |^ m)) = ((a - b) * t)

      proof

        assume (a + b) = 0 ;

        then a = 0 & b = 0 ;

        hence thesis;

      end;

      hence thesis by Lm16, Lm17;

    end;

    theorem :: NEWTON01:15

    (((((c1 |^ n) / 2) + (c1 / 2)) |^ 2) - ((((c1 |^ n) / 2) - (c1 / 2)) |^ 2)) = (c1 |^ (n + 1))

    proof

      set k = (((c1 |^ n) / 2) + (c1 / 2));

      set l = (((c1 |^ n) / 2) - (c1 / 2));

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

      .= ((k * k) - (l * l)) by NEWTON: 81

      .= (c1 * (c1 |^ n))

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

      hence thesis;

    end;

    

     Lm18d: n > 0 & (u - v) is odd implies (u + v) is odd & ((u |^ n) - (v |^ n)) is odd & ((u |^ n) + (v |^ n)) is odd

    proof

      (u is odd or u is even) & (v is odd or v is even);

      hence thesis;

    end;

    

     Lm18e: (u - v) is even implies (u + v) is even & ((u |^ n) - (v |^ n)) is even & ((u |^ n) + (v |^ n)) is even

    proof

      assume

       A1: (u - v) is even;

      per cases ;

        suppose

         A2: u is even & v is even;

        then ((u |^ n) is even & (v |^ n) is even) or n = 0 ;

        then

         A3a: ((u |^ n) is even & (v |^ n) is even) or ((u |^ n) = 1 & (v |^ n) = 1) by NEWTON: 4;

        then (((u |^ n) - (v |^ n)) is even) or (((u |^ n) - (v |^ n)) = 0 );

        hence thesis by A2, A3a;

      end;

        suppose u is odd & v is odd;

        hence thesis;

      end;

        suppose u is odd & v is even;

        hence thesis by A1;

      end;

        suppose u is even & v is odd;

        hence thesis by A1;

      end;

    end;

    theorem :: NEWTON01:16

    ((a |^ 3) - (b |^ 3)) = (((a - b) * ((((a + b) * (a + b)) + (a |^ 2)) + (b |^ 2))) / 2)

    proof

      

       A1: ((a |^ 2) - (b |^ 2)) = ((a - b) * (a + b)) by Th1;

      ((a |^ 3) - (b |^ 3)) = ((a |^ (2 + 1)) - (b |^ (2 + 1)))

      .= (((a - b) * ((((a + b) * (a + b)) + (a |^ 2)) + (b |^ 2))) / 2) by A1, Th14;

      hence thesis;

    end;

    theorem :: NEWTON01:17

    

     Th17: (c |^ m) >= ((a |^ m) + (b |^ m)) & a > 0 & b > 0 implies (c |^ (m + 1)) > ((a |^ (m + 1)) + (b |^ (m + 1)))

    proof

      assume

       A0: (c |^ m) >= ((a |^ m) + (b |^ m)) & a > 0 & b > 0 ;

      consider x be Nat such that

       A0b: c = (a + x) by A0, Th6, NAT_1: 10;

      

       A1: ((a + x) |^ m) >= ((a |^ m) + (b |^ m)) & a > 0 & x > 0 by A0, A0b, Lm5d;

      

       A2a: (a |^ m) > 0 by A0, PREPOWER: 6;

      then

       A3: ((a + x) |^ m) > (b |^ m) by A0, A0b, XREAL_1: 39;

      

       A4: (a + x) > b by A3, Lm3a;

      

       A5: (((a + x) |^ m) * (a + x)) >= (((a |^ m) + (b |^ m)) * (a + x)) by A0, A0b, XREAL_1: 66;

      

       A7: (b |^ m) > 0 by A0, PREPOWER: 6;

      

       A8: ((a |^ m) * (a + x)) > ((a |^ m) * a) by A1, NAT_1: 16, A2a, XREAL_1: 68;

      ((b |^ m) * (a + x)) > ((b |^ m) * b) by A4, A7, XREAL_1: 68;

      then (((a |^ m) * (a + x)) + ((b |^ m) * (a + x))) > (((a |^ m) * a) + ((b |^ m) * b)) by A8, XREAL_1: 8;

      then

       A12: (((a + x) |^ m) * (a + x)) > (((a |^ m) * a) + ((b |^ m) * b)) by A5, XXREAL_0: 2;

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

      hence thesis by A0b, A12, NEWTON: 6;

    end;

    theorem :: NEWTON01:18

    

     Th18: (c |^ m) >= ((a |^ m) + (b |^ m)) & a > 0 & b > 0 & k > 0 implies (c |^ (k + m)) > ((a |^ (k + m)) + (b |^ (k + m)))

    proof

      assume

       A0: (c |^ m) >= ((a |^ m) + (b |^ m)) & a > 0 & b > 0 & k > 0 ;

      then

      consider l such that

       A0b: k = (1 + l) by NAT_1: 10, NAT_1: 14;

      defpred P[ Nat] means (c |^ (($1 + m) + 1)) > ((a |^ (($1 + m) + 1)) + (b |^ (($1 + m) + 1))) & a > 0 & b > 0 ;

      

       A1: P[ 0 ] by A0, Th17;

      

       A2: P[x] implies P[(x + 1)] by Th17;

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

      then (c |^ ((l + m) + 1)) > ((a |^ ((l + m) + 1)) + (b |^ ((l + m) + 1)));

      hence thesis by A0b;

    end;

    theorem :: NEWTON01:19

    (c |^ m) >= ((a |^ m) + (b |^ m)) implies (c |^ (k + m)) >= ((a |^ (k + m)) + (b |^ (k + m)))

    proof

      assume

       A0: (c |^ m) >= ((a |^ m) + (b |^ m));

      then

       A0a: m <> 0 by Lm0;

      

       A0c: k = 0 implies thesis by A0;

      per cases ;

        suppose a = 0 or b = 0 ;

        then

         A1: ((a |^ m) = 0 or (b |^ m) = 0 ) & ((a |^ (k + m)) = 0 or (b |^ (k + m)) = 0 ) by A0a, NAT_1: 14, NEWTON: 11;

        then c >= a & c >= b by A0, A0a, NAT_1: 14, PREPOWER: 10;

        hence thesis by A1, Lm3a;

      end;

        suppose a > 0 & b > 0 ;

        hence thesis by A0, A0c, Th18;

      end;

    end;

    

     Lm28: (c |^ m) > ((a |^ m) + (b |^ m)) & a > 0 implies (c |^ (m + 1)) > ((a |^ (m + 1)) + (b |^ (m + 1)))

    proof

      assume

       A1: (c |^ m) > ((a |^ m) + (b |^ m)) & a > 0 ;

      then

       A2: m <> 0 by Lm0;

      per cases ;

        suppose b = 0 ;

        then (b |^ m) = 0 & (b |^ (m + 1)) = 0 by A2, NEWTON: 84;

        hence thesis by A1, Lm4a;

      end;

        suppose b <> 0 ;

        hence thesis by A1, Th18;

      end;

    end;

    

     Lm29: (c |^ m) > ((a |^ m) + (b |^ m)) implies (c |^ (m + 1)) > ((a |^ (m + 1)) + (b |^ (m + 1)))

    proof

      assume

       A1: (c |^ m) > ((a |^ m) + (b |^ m));

      then

       A2: m <> 0 by Lm0;

      per cases ;

        suppose b = 0 ;

        then (b |^ m) = 0 & (b |^ (m + 1)) = 0 by A2, NEWTON: 84;

        hence thesis by A1, Lm4a;

      end;

        suppose b <> 0 ;

        hence thesis by A1, Lm28;

      end;

    end;

    theorem :: NEWTON01:20

    (c |^ n) > ((a |^ n) + (b |^ n)) implies (c |^ (k + n)) > ((a |^ (k + n)) + (b |^ (k + n)))

    proof

      assume

       AX: (c |^ n) > ((a |^ n) + (b |^ n));

      then n <> 0 by Lm0;

      then

      consider m such that

       AY: n = (1 + m) by NAT_1: 10, NAT_1: 14;

      defpred P[ Nat] means (c |^ (($1 + m) + 1)) > ((a |^ (($1 + m) + 1)) + (b |^ (($1 + m) + 1)));

      

       A1: P[ 0 ] by AX, AY;

      

       A2: P[x] implies P[(x + 1)] by Lm29;

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

      then (c |^ ((k + m) + 1)) > ((a |^ ((k + m) + 1)) + (b |^ ((k + m) + 1)));

      hence thesis by AY;

    end;

    theorem :: NEWTON01:21

    

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

    proof

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

      .= (((((a1 |^ ((m + 1) + 1)) + ((b1 |^ (m + 1)) * a1)) - ((a1 |^ (m + 1)) * b1)) - ((b1 |^ (m + 1)) * b1)) + ((a1 * b1) * ((a1 |^ m) - (b1 |^ m)))) by NEWTON: 6

      .= (((((a1 |^ (m + 2)) + ((b1 |^ (m + 1)) * a1)) - ((a1 |^ (m + 1)) * b1)) - (b1 |^ ((m + 1) + 1))) + ((a1 * b1) * ((a1 |^ m) - (b1 |^ m)))) by NEWTON: 6

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

      .= ((((((a1 |^ (m + 2)) + ((b1 |^ (m + 1)) * a1)) - ((a1 |^ (m + 1)) * b1)) - (b1 |^ (m + 2))) + (b1 * (a1 |^ (m + 1)))) - (a1 * (b1 * (b1 |^ m)))) by NEWTON: 6

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

      hence thesis;

    end;

    theorem :: NEWTON01:22

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

    proof

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

      .= (((((a1 |^ ((m + 1) + 1)) - ((b1 |^ (m + 1)) * a1)) - ((a1 |^ (m + 1)) * b1)) + ((b1 |^ (m + 1)) * b1)) + ((a1 * b1) * ((a1 |^ m) + (b1 |^ m)))) by NEWTON: 6

      .= (((((a1 |^ (m + 2)) - ((b1 |^ (m + 1)) * a1)) - ((a1 |^ (m + 1)) * b1)) + (b1 |^ ((m + 1) + 1))) + ((a1 * b1) * ((a1 |^ m) + (b1 |^ m)))) by NEWTON: 6

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

      .= ((((((a1 |^ (m + 2)) - ((b1 |^ (m + 1)) * a1)) - ((a1 |^ (m + 1)) * b1)) + (b1 |^ (m + 2))) + (b1 * (a1 |^ (m + 1)))) + (a1 * (b1 * (b1 |^ m)))) by NEWTON: 6

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

      hence thesis;

    end;

    theorem :: NEWTON01:23

    ((a |^ ((2 * m) + 2)) - (b |^ ((2 * m) + 2))) = ((((a |^ 2) - (b |^ 2)) * (((c * ((a |^ 2) + (b |^ 2))) + (a |^ (2 * m))) + (b |^ (2 * m)))) / 2) iff ((a |^ (2 * m)) - (b |^ (2 * m))) = (((a |^ 2) - (b |^ 2)) * c)

    proof

      set k = (a |^ 2);

      set l = (b |^ 2);

      

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

      

       A2: (a |^ ((2 * m) + 2)) = (a |^ (2 * (m + 1)))

      .= ((a |^ 2) |^ (m + 1)) by NEWTON: 9;

      (b |^ ((2 * m) + 2)) = (b |^ (2 * (m + 1)))

      .= ((b |^ 2) |^ (m + 1)) by NEWTON: 9;

      hence thesis by A1, A2, Th14;

    end;

    theorem :: NEWTON01:24

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

    proof

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

      .= ((((a1 * ((a1 |^ ((2 * m) + 2)) + (b1 |^ ((2 * m) + 2)))) + (b1 * ((a1 |^ ((2 * m) + 2)) + (b1 |^ ((2 * m) + 2))))) - (b1 * (a1 * (a1 |^ ((2 * m) + 1))))) - (a1 * (b1 |^ (((2 * m) + 1) + 1)))) by NEWTON: 6

      .= ((((a1 * ((a1 |^ ((2 * m) + 2)) + (b1 |^ ((2 * m) + 2)))) + (b1 * ((a1 |^ ((2 * m) + 2)) + (b1 |^ ((2 * m) + 2))))) - (b1 * (a1 |^ (((2 * m) + 1) + 1)))) - (a1 * (b1 |^ ((2 * m) + 2)))) by NEWTON: 6

      .= ((a1 * (a1 |^ ((2 * m) + 2))) + (b1 * (b1 |^ ((2 * m) + 2))))

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

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

      hence thesis;

    end;

    theorem :: NEWTON01:25

    ((a1 |^ m) - (b1 |^ m)) = ((a1 - b1) * k) implies ((a1 |^ (m + 2)) - (b1 |^ (m + 2))) = ((((a1 |^ (m + 1)) + (b1 |^ (m + 1))) + ((a1 * b1) * k)) * (a1 - b1))

    proof

      assume ((a1 |^ m) - (b1 |^ m)) = ((a1 - b1) * k);

      

      hence ((a1 |^ (m + 2)) - (b1 |^ (m + 2))) = ((((a1 |^ (m + 1)) + (b1 |^ (m + 1))) * (a1 - b1)) + ((a1 * b1) * ((a1 - b1) * k))) by Th21

      .= ((((a1 |^ (m + 1)) + (b1 |^ (m + 1))) + ((a1 * b1) * k)) * (a1 - b1));

    end;

    theorem :: NEWTON01:26

    ((a1 |^ (m + 2)) - (b1 |^ (m + 2))) = ((((a1 |^ (m + 1)) + (b1 |^ (m + 1))) + ((a1 * b1) * k)) * (a1 - b1)) & (a1 * b1) <> 0 implies ((a1 |^ m) - (b1 |^ m)) = ((a1 - b1) * k)

    proof

      assume

       A1: ((a1 |^ (m + 2)) - (b1 |^ (m + 2))) = ((((a1 |^ (m + 1)) + (b1 |^ (m + 1))) + ((a1 * b1) * k)) * (a1 - b1)) & (a1 * b1) <> 0 ;

      then

       A5: (((k * (a1 - b1)) * (a1 * b1)) / (a1 * b1)) = (k * (a1 - b1)) by XCMPLX_1: 89;

      ((((a1 |^ (m + 1)) + (b1 |^ (m + 1))) * (a1 - b1)) + ((a1 * b1) * ((a1 |^ m) - (b1 |^ m)))) = ((((a1 |^ (m + 1)) + (b1 |^ (m + 1))) * (a1 - b1)) + (((a1 * b1) * k) * (a1 - b1))) by A1, Th21;

      hence thesis by A1, XCMPLX_1: 89, A5;

    end;

    

     Lm56a: n > 1 & b > 0 & a > b implies (((a |^ n) + (b |^ n)) * (a - b)) < ((a |^ (n + 1)) - (b |^ (n + 1)))

    proof

      assume

       A1: n > 1 & b > 0 & a > b;

      

       A2: (a |^ (n + 1)) = (a * (a |^ n)) & (b |^ (n + 1)) = (b * (b |^ n)) & (a |^ (m + 1)) = (a * (a |^ m)) & (b |^ (m + 1)) = (b * (b |^ m)) by NEWTON: 6;

      consider m such that

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

      

       A3a: m >= 1 by A3, A1, NAT_1: 13;

      (a |^ m) > (b |^ m) by A1, A3a, PREPOWER: 10;

      then

       A3c: ((a |^ m) - (b |^ m)) > ((b |^ m) - (b |^ m)) by XREAL_1: 9;

      (((a |^ n) + (b |^ n)) * (a - b)) = ((((a |^ (n + 1)) - (b |^ (n + 1))) + (a * (b |^ n))) - (b * (a |^ n))) by A2

      .= ((((a |^ (n + 1)) - (b |^ (n + 1))) + (a * (b |^ (m + 1)))) - (b * (a * (a |^ m)))) by NEWTON: 6, A3

      .= ((((a |^ (n + 1)) - (b |^ (n + 1))) + (a * (b * (b |^ m)))) - (b * (a * (a |^ m)))) by NEWTON: 6

      .= (((a |^ (n + 1)) - (b |^ (n + 1))) - ((a * b) * ((a |^ m) - (b |^ m))));

      hence thesis by A1, A3c, XREAL_1: 44;

    end;

    

     Lm57: n > 0 & a > b implies (((a |^ n) - (b |^ n)) * (a + b)) >= ((a |^ (n + 1)) - (b |^ (n + 1)))

    proof

      assume

       A1: n > 0 & a > b;

      

       A2: 0 <= ((a |^ m) - (b |^ m)) by A1, Lm3a, XREAL_1: 48;

      

       A2b: (a |^ (n + 1)) = (a * (a |^ n)) & (b |^ (n + 1)) = (b * (b |^ n)) & (a |^ (m + 1)) = (a * (a |^ m)) & (b |^ (m + 1)) = (b * (b |^ m)) by NEWTON: 6;

      consider m such that

       A3: n = (1 + m) by A1, NAT_1: 14, NAT_1: 10;

      

       A4: (((a |^ n) - (b |^ n)) * (a + b)) = ((((a |^ (n + 1)) - (b |^ (n + 1))) - (a * (b |^ n))) + (b * (a |^ n))) by A2b

      .= ((((a |^ (n + 1)) - (b |^ (n + 1))) - (a * (b |^ (m + 1)))) + (b * (a * (a |^ m)))) by NEWTON: 6, A3

      .= ((((a |^ (n + 1)) - (b |^ (n + 1))) - (a * (b * (b |^ m)))) + (b * (a * (a |^ m)))) by NEWTON: 6

      .= (((a |^ (n + 1)) - (b |^ (n + 1))) + ((a * b) * ((a |^ m) - (b |^ m))));

      ((a |^ m) - (b |^ m)) in NAT by A2, INT_1: 3;

      hence thesis by A4, XREAL_1: 40;

    end;

    

     Lm57d: b > 0 & a > b & (((a |^ n) - (b |^ n)) * (a + b)) = (((a |^ n) + (b |^ n)) * (a - b)) implies n = 1

    proof

      assume

       A0: b > 0 & a > b & (((a |^ n) - (b |^ n)) * (a + b)) = (((a |^ n) + (b |^ n)) * (a - b));

      

       A1: (a |^ 0 ) = 1 & (b |^ 0 ) = 1 by NEWTON: 4;

      per cases ;

        suppose n = 0 ;

        then ( 0 * (a + b)) = (2 * (a - b)) by A0, A1;

        hence thesis by A0;

      end;

        suppose

         A20: n > 0 ;

        then

         A20a: n >= 1 by NAT_1: 14;

        ((a |^ (n + 1)) - (b |^ (n + 1))) <= (((a |^ n) + (b |^ n)) * (a - b)) by A0, A20, Lm57;

        then n <= 1 by A0, Lm56a;

        hence thesis by A20a, XXREAL_0: 1;

      end;

    end;

    theorem :: NEWTON01:27

    b > 0 & a > b implies ((((a |^ n) - (b |^ n)) * (a + b)) = (((a |^ n) + (b |^ n)) * (a - b)) iff n = 1) by Lm57d;

    theorem :: NEWTON01:28

    n > 1 & b > 0 & a > b implies (((a |^ n) - (b |^ n)) * (a + b)) > ((a |^ (n + 1)) - (b |^ (n + 1)))

    proof

      assume

       A1: n > 1 & b > 0 & a > b;

      

       A2: (a |^ (n + 1)) = (a * (a |^ n)) & (b |^ (n + 1)) = (b * (b |^ n)) & (a |^ (m + 1)) = (a * (a |^ m)) & (b |^ (m + 1)) = (b * (b |^ m)) by NEWTON: 6;

      consider m such that

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

      

       A3a: m >= 1 by A3, A1, NAT_1: 13;

      

       A3b: (a |^ m) > (b |^ m) by A1, A3a, PREPOWER: 10;

      

       A3c: ((a |^ m) - (b |^ m)) > ((b |^ m) - (b |^ m)) by A3b, XREAL_1: 9;

      (((a |^ n) - (b |^ n)) * (a + b)) = ((((a |^ (n + 1)) - (b |^ (n + 1))) - (a * (b |^ n))) + (b * (a |^ n))) by A2

      .= ((((a |^ (n + 1)) - (b |^ (n + 1))) - (a * (b |^ (m + 1)))) + (b * (a * (a |^ m)))) by NEWTON: 6, A3

      .= ((((a |^ (n + 1)) - (b |^ (n + 1))) - (a * (b * (b |^ m)))) + (b * (a * (a |^ m)))) by NEWTON: 6

      .= (((a |^ (n + 1)) - (b |^ (n + 1))) + ((a * b) * ((a |^ m) - (b |^ m))));

      hence thesis by A1, A3c, XREAL_1: 39;

    end;

    theorem :: NEWTON01:29

    n > 0 & a > b implies (((a |^ n) + (b |^ n)) * (a - b)) <= ((a |^ (n + 1)) - (b |^ (n + 1)))

    proof

      assume

       A1: n > 0 & a > b;

      then

       A2: 0 <= ((a |^ m) - (b |^ m)) by Lm3a, XREAL_1: 48;

      

       A2b: (a |^ (n + 1)) = (a * (a |^ n)) & (b |^ (n + 1)) = (b * (b |^ n)) & (a |^ (m + 1)) = (a * (a |^ m)) & (b |^ (m + 1)) = (b * (b |^ m)) by NEWTON: 6;

      consider m such that

       A3: n = (1 + m) by A1, NAT_1: 14, NAT_1: 10;

      

       A4: (((a |^ n) + (b |^ n)) * (a - b)) = ((((a |^ (n + 1)) - (b |^ (n + 1))) + (a * (b |^ n))) - (b * (a |^ n))) by A2b

      .= ((((a |^ (n + 1)) - (b |^ (n + 1))) + (a * (b |^ (m + 1)))) - (b * (a * (a |^ m)))) by NEWTON: 6, A3

      .= ((((a |^ (n + 1)) - (b |^ (n + 1))) + (a * (b * (b |^ m)))) - (b * (a * (a |^ m)))) by NEWTON: 6

      .= (((a |^ (n + 1)) - (b |^ (n + 1))) - ((a * b) * ((a |^ m) - (b |^ m))));

      ((a |^ m) - (b |^ m)) in NAT by A2, INT_1: 3;

      hence thesis by A4, XREAL_1: 43;

    end;

    

     Lm18b: (a - b) divides ((a |^ 0 ) - (b |^ 0 ))

    proof

      ((a |^ 0 ) - (b |^ 0 )) = (1 - (b |^ 0 )) by NEWTON: 4

      .= (1 - 1) by NEWTON: 4;

      hence thesis by INT_2: 12;

    end;

    

     Lm18f: n > 0 & (a - b) divides ((a |^ n) - (b |^ n)) implies (a - b) divides ((a |^ (n + 1)) - (b |^ (n + 1)))

    proof

      assume

       A1: n > 0 & (a - b) divides ((a |^ n) - (b |^ n));

      consider q be Integer such that

       A3: ((a |^ n) - (b |^ n)) = ((a - b) * q) by A1;

      per cases ;

        suppose (a - b) is even;

        then

         A5: (a + b) is even & ((a |^ n) + (b |^ n)) is even & ((a |^ n) - (b |^ n)) is even by Lm18e;

        then

        consider l be Integer such that

         A6: (a + b) = (2 * l);

        consider k be Integer such that

         A7: ((a |^ n) + (b |^ n)) = (2 * k) by A5;

        ((a |^ (n + 1)) - (b |^ (n + 1))) = ((((2 * k) * (a - b)) + ((2 * l) * ((a |^ n) - (b |^ n)))) / 2) by Th13, A6, A7

        .= ((k * (a - b)) + (l * ((a |^ n) - (b |^ n))))

        .= ((k * (a - b)) + (l * ((a - b) * q))) by A3

        .= ((a - b) * (k + (l * q)));

        hence thesis;

      end;

        suppose

         A12: (a - b) is odd;

        then

         A13: (a + b) is odd & ((a |^ n) + (b |^ n)) is odd & ((a |^ n) - (b |^ n)) is odd & ((a |^ (n + 1)) - (b |^ (n + 1))) is odd by A1, Lm18d;

        q is odd by A3, A1, A12, Lm18d;

        then

        consider m be Integer such that

         A18: (2 * m) = (((a |^ n) + (b |^ n)) + ((a + b) * q)) by A13, ABIAN: 11;

        ((a |^ (n + 1)) - (b |^ (n + 1))) = (((((a |^ n) + (b |^ n)) * (a - b)) + ((a + b) * ((a - b) * q))) / 2) by Th13, A3

        .= (((a - b) * (((a |^ n) + (b |^ n)) + ((a + b) * q))) / 2)

        .= (((a - b) * (2 * m)) / 2) by A18

        .= ((a - b) * m);

        hence thesis;

      end;

    end;

    

     Lm46: m > 0 implies (2 * a) divides ((a |^ m) + (a |^ m))

    proof

      assume m > 0 ;

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

      then (2 * a) divides (2 * (a |^ m)) by NAT_3: 1;

      hence thesis;

    end;

    theorem :: NEWTON01:30

    

     Th29: (p + q) divides ((p * u) + (q * v)) implies (p + q) divides ((p * (u + z)) + (q * (v + z)))

    proof

      assume (p + q) divides ((p * u) + (q * v));

      then

      consider t be Integer such that

       A2: ((p + q) * t) = ((p * u) + (q * v));

      ((p * (u + z)) + (q * (v + z))) = ((p + q) * (t + z)) by A2;

      hence thesis;

    end;

    theorem :: NEWTON01:31

    (p + q) divides ((p * ((t * (p + q)) + z)) + (q * z))

    proof

      

       A1: z = (((q * t) * 0 ) + z);

      ((p * (t * (p + q))) + (q * (t * 0 ))) = (((p * t) * (p + q)) + ((q * t) * 0 ));

      hence thesis by A1, INT_1:def 3, Th29;

    end;

    theorem :: NEWTON01:32

    

     Th31: (p + q) divides (u - v) implies (p + q) divides ((p * (u + t)) + (q * (v + t)))

    proof

      set z = (u - v);

      assume (p + q) divides (u - v);

      then (p + q) divides ((p * z) + (q * 0 )) by INT_2: 2;

      then (p + q) divides ((p * (z + (v + t))) + (q * ( 0 + (v + t)))) by Th29;

      hence thesis;

    end;

    theorem :: NEWTON01:33

    

     Th32: (a - b) divides ((a |^ n) - (b |^ n))

    proof

      defpred P[ Nat] means (a - b) divides ((a |^ $1) - (b |^ $1));

      

       A1: P[ 0 ] by Lm18b;

      

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

      proof

        x = 0 or x > 0 ;

        hence thesis by Lm18f;

      end;

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

      hence thesis;

    end;

    theorem :: NEWTON01:34

    

     Th33: ((a |^ 2) - (b |^ 2)) divides ((a |^ (2 * m)) - (b |^ (2 * m)))

    proof

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

      hence thesis by Th32;

    end;

    theorem :: NEWTON01:35

    

     Th34: (a + b) divides ((a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1)))

    proof

      

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

      set n = (m + 1);

      consider t be Integer such that

       A4: ((a |^ (2 * m)) - (b |^ (2 * m))) = (((a |^ 2) - (b |^ 2)) * t) by Th33, INT_1:def 3;

      consider z be Integer such that

       A4a: ((a |^ (2 * n)) - (b |^ (2 * n))) = (((a |^ 2) - (b |^ 2)) * z) by Th33, INT_1:def 3;

      

       A5: ((a - b) * ((a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1)))) = (((a |^ ((2 * m) + 2)) - (b |^ ((2 * m) + 2))) - ((a * b) * ((a |^ (2 * m)) - (b |^ (2 * m))))) by A2

      .= (((a |^ (2 * n)) - (b |^ (2 * n))) - ((a * b) * (((a |^ 2) - (b |^ 2)) * t))) by A4

      .= (((a |^ 2) - (b |^ 2)) * (z - ((a * b) * t))) by A4a

      .= (((a - b) * (a + b)) * (z - ((a * b) * t))) by Th1

      .= ((a - b) * ((a + b) * (z - ((a * b) * t))));

      

       X: (2 * a) = (a + a);

      ((a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1))) = ((a + b) * (z - ((a * b) * t))) or (a - b) = 0 by A5, XCMPLX_1: 5;

      hence thesis by Lm46, X;

    end;

    

     Lm44: (a + b) divides ((a |^ 2) - (b |^ 2))

    proof

      ((a |^ 2) - (b |^ 2)) = ((a + b) * (a - b)) by Th1;

      hence thesis;

    end;

    theorem :: NEWTON01:36

    (a + b) divides ((a |^ (2 * m)) - (b |^ (2 * m)))

    proof

      

       A1: (a + b) divides ((a |^ 2) - (b |^ 2)) by Lm44;

      ((a |^ 2) - (b |^ 2)) divides ((a |^ (2 * m)) - (b |^ (2 * m))) by Th33;

      hence thesis by A1, INT_2: 9;

    end;

    theorem :: NEWTON01:37

    (a + b) divides ((a |^ n) - (b |^ n)) implies (a + b) divides ((a |^ (n + 1)) + (b |^ (n + 1)))

    proof

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

      then (a + b) divides ((a * ((a |^ n) + 0 )) + (b * ((b |^ n) + 0 ))) by Th31;

      then (a + b) divides ((a |^ (n + 1)) + (b * (b |^ n))) by NEWTON: 6;

      hence thesis by NEWTON: 6;

    end;

    theorem :: NEWTON01:38

    (a + b) divides ((a |^ n) + (b |^ n)) or (a + b) divides ((a |^ n) - (b |^ n))

    proof

      per cases ;

        suppose n is odd;

        then ex k be Nat st n = ((2 * k) + 1) by ABIAN: 9;

        hence thesis by Th34;

      end;

        suppose n is even;

        then

        consider m be Nat such that

         A2: n = (2 * m);

        

         A3: (a + b) divides ((a |^ 2) - (b |^ 2)) by Lm44;

        ((a |^ 2) - (b |^ 2)) divides ((a |^ (2 * m)) - (b |^ (2 * m))) by Th33;

        hence thesis by A2, A3, INT_2: 9;

      end;

    end;

    theorem :: NEWTON01:39

    a >= b & ((c |^ n) - (b |^ n)) = (a |^ n) implies ((c - b) gcd (a |^ n)) = (c - b) & ((c - a) gcd (b |^ n)) = (c - a)

    proof

      assume

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

      

       A1a: (c |^ n) = ((b |^ n) + (a |^ n)) by A1;

      then

       A1c: (c - b) >= (a - b) by Th6, XREAL_1: 9;

      (a - b) >= (b - b) by A1, XREAL_1: 9;

      then

       A1f: (c - b) in NAT by A1c, INT_1: 3;

      (c - a) >= (a - a) by A1a, Th6, XREAL_1: 9;

      then

       A1i: (c - a) in NAT by INT_1: 3;

      (c - a) divides ((c |^ n) - (a |^ n)) by Th32;

      hence thesis by A1, A1i, A1f, Th32, NEWTON: 49;

    end;

    theorem :: NEWTON01:40

    (a,b) are_coprime & (a + b) divides ((a * c) + (b * d)) implies (a + b) divides (c - d)

    proof

      assume

       A1: (a,b) are_coprime & (a + b) divides ((a * c) + (b * d));

      set u = (a * c);

      set v = ( - (b * d));

      

       A1a: (a + b) divides (u - v) by A1;

      

       A2: (a + b) divides ((a * (u + 0 )) + (b * (v + 0 ))) by A1a, Th31;

      consider t such that

       A4: (((a * a) * c) - ((b * b) * d)) = ((a + b) * t) by A2;

      

       A6: ((a * b) * (c - d)) = ((((a * c) - (b * d)) - t) * (a + b)) by A4;

      (a,(a + b)) are_coprime & (b,(a + b)) are_coprime by A1, EULER_1: 7;

      then ((a * b),(a + b)) are_coprime by WSIERP_1: 6;

      hence thesis by A6, INT_1:def 3, WSIERP_1: 29;

    end;

    theorem :: NEWTON01:41

    

     Th40: ((a * b),(c * d)) are_coprime implies (a,c) are_coprime

    proof

      assume

       A1: ((a * b),(c * d)) are_coprime ;

      

       A3: (a gcd c) divides (a * b) by INT_2: 2, INT_2: 21;

      (a gcd c) divides (c * d) by INT_2: 2, INT_2: 21;

      hence (a,c) are_coprime by A1, A3, WSIERP_1: 15, INT_2: 22;

    end;

    

     Lm53: ((a |^ (k + 1)),(b |^ (m + 1))) are_coprime implies (a,b) are_coprime

    proof

      (a |^ (k + 1)) = (a * (a |^ k)) & (b |^ (m + 1)) = (b * (b |^ m)) by NEWTON: 6;

      hence thesis by Th40;

    end;

    

     Lm58: a > 0 & b > 0 & ((a |^ n) + (b |^ n)) = (c |^ n) implies ex j, k, l st ((j |^ n) + (k |^ n)) = (l |^ n) & (j,k) are_coprime & a = ((a gcd b) * j) & b = ((a gcd b) * k) & c = ((a gcd b) * l)

    proof

      set x = (a gcd b);

      assume

       A1: a > 0 & b > 0 & ((a |^ n) + (b |^ n)) = (c |^ n);

      then

       A1b: n <> 0 by Lm0;

      x <> 0 by A1, INT_2: 5;

      then

       A1d: (x |^ n) > 0 by PREPOWER: 6;

      consider j,k be Integer such that

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

      j > 0 & k > 0 by A1, A2;

      then

       A2b: j in NAT & k in NAT by INT_1: 3;

      

       A3: (a |^ n) = ((x |^ n) * (j |^ n)) by A2, NEWTON: 7;

      

       A4: (b |^ n) = ((x |^ n) * (k |^ n)) by A2, NEWTON: 7;

      then (c |^ n) = ((x |^ n) * ((j |^ n) + (k |^ n))) by A1, A3;

      then x divides c by A1b, INT_1:def 3, WSIERP_1: 26;

      then

      consider l such that

       A8: c = (x * l) by NAT_D:def 3;

      (((j |^ n) + (k |^ n)) * (x |^ n)) = ((l |^ n) * (x |^ n)) by A1, A3, A4, A8, NEWTON: 7;

      then ((j |^ n) + (k |^ n)) = (l |^ n) by A1d, XCMPLX_1: 5;

      hence thesis by A2, A2b, A8;

    end;

    

     Lm59: ((j |^ (m + 1)) + (k |^ (m + 1))) = (l |^ (m + 1)) & (j,k) are_coprime implies (j,l) are_coprime

    proof

      set n = (m + 1);

      assume

       A1: ((j |^ n) + (k |^ n)) = (l |^ n) & (j,k) are_coprime ;

      then ((j |^ n) gcd (k |^ n)) = 1 by WSIERP_1: 11, INT_2:def 3;

      then ((l |^ n),(j |^ n)) are_coprime by A1, EULER_1: 7;

      hence thesis by Lm53;

    end;

    theorem :: NEWTON01:42

    

     Th41: a > 0 & b > 0 & ((a |^ n) + (b |^ n)) = (c |^ n) implies ex j, k, l st ((j |^ n) + (k |^ n)) = (l |^ n) & (j,k) are_coprime & (j,l) are_coprime & (k,l) are_coprime & a = ((a gcd b) * j) & b = ((a gcd b) * k) & c = ((a gcd b) * l)

    proof

      assume

       A1: a > 0 & b > 0 & ((a |^ n) + (b |^ n)) = (c |^ n);

      then n <> 0 by Lm0;

      then

      consider m such that

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

      consider j, k, l such that

       A4: ((j |^ (m + 1)) + (k |^ (m + 1))) = (l |^ (m + 1)) & (j,k) are_coprime & a = ((a gcd b) * j) & b = ((a gcd b) * k) & c = ((a gcd b) * l) by A1, A3, Lm58;

      (j,l) are_coprime & (k,l) are_coprime by A4, Lm59;

      hence thesis by A3, A4;

    end;

    

     Lm60: a = 1 implies ((a |^ (n + 2)) + (a |^ (n + 2))) <> (b |^ (n + 2))

    proof

      assume

       A1: a = 1;

      

       A5: (2 + 0 ) <= (2 + n) by XREAL_1: 6;

      assume

       A2: not thesis;

      (2 + n) < (2 |^ (2 + n)) by NEWTON: 86;

      then (b |^ (2 + n)) > (1 |^ (2 + n)) & (b |^ (2 + n)) < (2 |^ (2 + n)) by A1, A5, A2, XXREAL_0: 2;

      then b > 1 & b < (1 + 1) by Lm3a;

      hence contradiction by NAT_1: 13;

    end;

    theorem :: NEWTON01:43

    a > 0 implies ((a |^ (n + 2)) + (a |^ (n + 2))) <> (b |^ (n + 2))

    proof

      assume

       A1: a > 0 ;

      assume not thesis;

      then

      consider j, k, l such that

       A3: ((j |^ (n + 2)) + (k |^ (n + 2))) = (l |^ (n + 2)) & (j,k) are_coprime & (j,l) are_coprime & (k,l) are_coprime & a = ((a gcd a) * j) & a = ((a gcd a) * k) & b = ((a gcd a) * l) by A1, Th41;

      (k * a) = (1 * a) & (j * a) = (1 * a) by NAT_D: 32, A3;

      then k = 1 & j = 1 by A1, XCMPLX_1: 5;

      hence contradiction by A3, Lm60;

    end;

    

     Lm61: (a1 + (b1 |^ 2)) = (c1 |^ 2) implies ((a1 + ((b1 + d1) |^ 2)) - ((c1 + d1) |^ 2)) = ((2 * d1) * (b1 - c1))

    proof

      assume

       A1: (a1 + (b1 |^ 2)) = (c1 |^ 2);

      ((a1 + ((b1 + d1) |^ 2)) - ((c1 + d1) |^ 2)) = ((a1 + (((b1 |^ 2) + ((2 * b1) * d1)) + (d1 |^ 2))) - ((c1 + d1) |^ 2)) by Lm10

      .= ((((a1 + (b1 |^ 2)) + ((2 * b1) * d1)) + (d1 |^ 2)) - (((c1 |^ 2) + ((2 * c1) * d1)) + (d1 |^ 2))) by Lm10

      .= (((2 * b1) * d1) - ((2 * c1) * d1)) by A1;

      hence thesis;

    end;

    theorem :: NEWTON01:44

    x > 0 & b < c & (a + (b |^ 2)) = (c |^ 2) implies (a + ((b + x) |^ 2)) < ((c + x) |^ 2)

    proof

      assume

       A1: x > 0 & b < c & (a + (b |^ 2)) = (c |^ 2);

      then

       A1a: (b - c) < (c - c) by XREAL_1: 9;

      ((a + ((b + x) |^ 2)) - ((c + x) |^ 2)) = ((2 * x) * (b - c)) by A1, Lm61;

      then (((a + ((b + x) |^ 2)) - ((c + x) |^ 2)) + ((c + x) |^ 2)) < ( 0 + ((c + x) |^ 2)) by A1, A1a, XREAL_1: 6;

      hence thesis;

    end;

    theorem :: NEWTON01:45

    

     Th44: q < 0 & b < c & ((a |^ 2) + (b |^ 2)) = (c |^ 2) implies ((a |^ 2) + ((b + q) |^ 2)) > ((c + q) |^ 2)

    proof

      assume

       A1: q < 0 & b < c & ((a |^ 2) + (b |^ 2)) = (c |^ 2);

      then

       A1a: (b - c) < (c - c) by XREAL_1: 9;

      (((a |^ 2) + ((b + q) |^ 2)) - ((c + q) |^ 2)) = ((2 * q) * (b - c)) by A1, Lm61;

      then ((((a |^ 2) + ((b + q) |^ 2)) - ((c + q) |^ 2)) + ((c + q) |^ 2)) > ( 0 + ((c + q) |^ 2)) by A1, A1a, XREAL_1: 6;

      hence thesis;

    end;

    theorem :: NEWTON01:46

    x > 0 & ((a |^ 2) + (b |^ 2)) = ((b + 1) |^ 2) implies ((a |^ 2) + ((b - x) |^ 2)) > (((b + 1) - x) |^ 2)

    proof

      

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

      assume

       A1: x > 0 & ((a |^ 2) + (b |^ 2)) = ((b + 1) |^ 2);

      consider q such that

       A2: q = ( - x);

      ((a |^ 2) + ((b + q) |^ 2)) > (((b + 1) + q) |^ 2) by A0, A1, A2, Th44;

      hence thesis by A2;

    end;

    theorem :: NEWTON01:47

    

     Th46: a >= 1 & (((a + 1) |^ 2) + (((a + 1) + x) |^ 2)) <= ((((a + 1) + x) + 1) |^ 2) implies ((a |^ 2) + ((a + x) |^ 2)) < (((a + x) + 1) |^ 2)

    proof

      

       A2: (((a + x) + 1) |^ 2) = ((((((a |^ 2) + (x |^ 2)) + (1 |^ 2)) + ((2 * a) * x)) + ((2 * a) * 1)) + ((2 * x) * 1)) by SERIES_4: 1

      .= ((((((a |^ 2) + (x |^ 2)) + ((2 * a) * x)) + (2 * x)) + (2 * a)) + 1);

      

       A3: (((a + x) + 2) |^ 2) = ((((((a |^ 2) + (x |^ 2)) + (2 |^ 2)) + ((2 * a) * x)) + ((2 * a) * 2)) + ((2 * x) * 2)) by SERIES_4: 1

      .= ((((((((2 * a) * 2) + (2 * x)) + (2 * x)) + (2 |^ 2)) + (a |^ 2)) + ((2 * a) * x)) + (x |^ 2));

      

       A4: ((a + x) |^ 2) = (((a |^ 2) + ((2 * a) * x)) + (x |^ 2)) by Lm10;

      assume

       A5: a >= 1 & (((a + 1) |^ 2) + (((a + 1) + x) |^ 2)) <= ((((a + 1) + x) + 1) |^ 2);

      then

       A5a: ((((a + 1) |^ 2) + (((a + x) + 1) |^ 2)) - (((a + x) + 2) |^ 2)) <= ((((a + x) + 2) |^ 2) - (((a + x) + 2) |^ 2)) by XREAL_1: 9;

      ( - ((((a + 1) |^ 2) + (((a + x) + 1) |^ 2)) - (((a + x) + 2) |^ 2))) = ((((a + x) + 2) |^ 2) - (((a + 1) |^ 2) + (((a + x) + 1) |^ 2)))

      .= ((((((((a |^ 2) + (x |^ 2)) + (2 |^ 2)) + ((2 * a) * x)) + ((2 * 2) * a)) + (2 * x)) + (2 * x)) - ((((a |^ 2) + (2 * a)) + 1) + ((((((a |^ 2) + (x |^ 2)) + (1 |^ 2)) + ((2 * a) * x)) + ((2 * a) * 1)) + ((2 * x) * 1)))) by Lm10, A2, A3

      .= (((((2 |^ 2) + (2 * x)) - 1) - (a |^ 2)) - (1 * 1))

      .= (((((2 * 2) + (2 * x)) - 1) - (a |^ 2)) - 1) by WSIERP_1: 1;

      then

       A6: (((a |^ 2) + ((a + x) |^ 2)) + 0 ) <= (((a |^ 2) + ((a + x) |^ 2)) + (((4 + (2 * x)) - (a |^ 2)) - 2)) by A5a, XREAL_1: 6;

      

       A7: (a + 1) > ( 0 + 1) & (a + 1) >= (1 + 1) by A5, XREAL_1: 6;

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

      then ((2 * a) + 1) > (1 + 1) by A7, XXREAL_0: 2;

      then (((((a |^ 2) + (x |^ 2)) + ((2 * a) * x)) + (2 * x)) + ((2 * a) + 1)) > (((((a |^ 2) + (x |^ 2)) + ((2 * a) * x)) + (2 * x)) + 2) by XREAL_1: 6;

      hence thesis by A2, A4, A6, XXREAL_0: 2;

    end;

    theorem :: NEWTON01:48

    

     Th47: a >= 1 & ((a |^ 2) + ((a + x) |^ 2)) >= (((a + x) + 1) |^ 2) implies ((((a + l) + 1) |^ 2) + ((((a + l) + 1) + x) |^ 2)) > (((((a + l) + 1) + x) + 1) |^ 2)

    proof

      assume

       A1: a >= 1 & ((a |^ 2) + ((a + x) |^ 2)) >= (((a + x) + 1) |^ 2);

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

      

       A2: P[ 0 ] by A1, Th46;

      

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

      proof

        assume

         A4: P[k];

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

        hence thesis by A4, Th46;

      end;

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

      hence thesis;

    end;

    

     Lm120: ((a |^ 2) + (a |^ 2)) > ((a + 1) |^ 2) implies a >= 3

    proof

      

       L1: ((a - 1) |^ 2) = ((a + ( - 1)) |^ 2)

      .= (((a |^ 2) + ((2 * a) * ( - 1))) + (( - 1) |^ 2)) by Lm10

      .= (((a |^ 2) + ((2 * a) * ( - 1))) + (( - 1) * ( - 1))) by NEWTON: 81;

      assume

       A1: ((a |^ 2) + (a |^ 2)) > ((a + 1) |^ 2);

      then (a |^ 2) > 0 ;

      then (a |^ 2) > ( 0 |^ 2) by NEWTON: 11;

      then (a - 1) >= (1 - 1) by NAT_1: 14, XREAL_1: 9;

      then

       A2: (a - 1) in NAT by INT_1: 3;

      ((a + 1) |^ 2) = (((a |^ 2) + ((2 * a) * 1)) + (1 |^ 2)) by Lm10

      .= (((a |^ 2) + (2 * a)) + 1);

      then (((a |^ 2) + (a |^ 2)) - (((a |^ 2) + (2 * a)) - 1)) > ((((a |^ 2) + (2 * a)) + 1) - (((a |^ 2) + (2 * a)) - 1)) by A1, XREAL_1: 9;

      then ((a - 1) |^ 2) > (1 |^ 2) by L1, XXREAL_0: 2;

      then ((a - 1) + 1) > (1 + 1) by A2, Lm3a, XREAL_1: 6;

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

      hence thesis;

    end;

    theorem :: NEWTON01:49

    a >= 3 iff ((a |^ 2) + (a |^ 2)) > ((a + 1) |^ 2)

    proof

      a >= 3 implies ((a |^ 2) + (a |^ 2)) > ((a + 1) |^ 2)

      proof

        assume a >= 3;

        then

        consider b such that

         A2: a = (3 + b) by NAT_1: 10;

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

        

         A3: P[ 0 ]

        proof

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

          hence thesis;

        end;

        

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

        proof

          assume P[k];

          then (1 + (2 + k)) >= (1 + 0 ) & (((3 + k) |^ 2) + (((3 + k) + 0 ) |^ 2)) > ((((3 + k) + 0 ) + 1) |^ 2) by XREAL_1: 6;

          then ((((3 + k) + 1) |^ 2) + ((((3 + k) + 0 ) + 1) |^ 2)) > (((((3 + k) + 1) + 0 ) + 1) |^ 2) by Th47;

          hence thesis;

        end;

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

        hence thesis by A2;

      end;

      hence thesis by Lm120;

    end;

    theorem :: NEWTON01:50

    ((2 |^ (3 + m)) + (2 |^ (3 + m))) < (3 |^ (3 + m))

    proof

      

       A4: ((2 |^ (2 + 1)) + (2 |^ (2 + 1))) = (2 * (2 |^ (2 + 1)))

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

      .= (2 * ((2 * 2) * 2)) by NEWTON: 81;

      

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

      .= ((3 * 3) * 3) by NEWTON: 81;

      

       A6: (2 |^ (3 + m)) = ((2 |^ 3) * (2 |^ m)) & (3 |^ (3 + m)) = ((3 |^ 3) * (3 |^ m)) by NEWTON: 8;

      (2 |^ m) <= (3 |^ m) by Lm3a;

      then

       A7: (((2 |^ 3) + (2 |^ 3)) * (2 |^ m)) <= (((2 |^ 3) + (2 |^ 3)) * (3 |^ m)) by XREAL_1: 64;

      (3 |^ m) > 0 by PREPOWER: 6;

      then (((2 |^ 3) + (2 |^ 3)) * (3 |^ m)) < ((3 |^ 3) * (3 |^ m)) by A4, A5, XREAL_1: 68;

      hence thesis by XXREAL_0: 2, A6, A7;

    end;