square_1.miz



    begin

    reserve a,b,c,x,y,z for Real;

    scheme :: SQUARE_1:sch1

    RealContinuity { P,Q[ object] } :

ex z st for x, y st P[x] & Q[y] holds x <= z & z <= y

      provided

       A1: for x, y st P[x] & Q[y] holds x <= y;

      set Y = { z where z be Element of REAL : Q[z] };

      set X = { z where z be Element of REAL : P[z] };

      

       A2: X c= REAL

      proof

        let x be object;

        assume x in X;

        then ex z be Element of REAL st z = x & P[z];

        hence thesis;

      end;

      Y c= REAL

      proof

        let x be object;

        assume x in Y;

        then ex z be Element of REAL st z = x & Q[z];

        hence thesis;

      end;

      then

      reconsider X, Y as Subset of REAL by A2;

      for x,y be Real st x in X & y in Y holds x <= y

      proof

        let x,y be Real;

        assume that

         A3: x in X and

         A4: y in Y;

        

         A5: ex z be Element of REAL st z = y & Q[z] by A4;

        ex z be Element of REAL st z = x & P[z] by A3;

        hence thesis by A1, A5;

      end;

      then

      consider z be Real such that

       A6: for x,y be Real st x in X & y in Y holds x <= z & z <= y by AXIOMS: 1;

      take z;

      let x, y;

      assume that

       A7: P[x] and

       A8: Q[y];

      y is Element of REAL by XREAL_0:def 1;

      then

       A9: y in Y by A8;

      x is Element of REAL by XREAL_0:def 1;

      then x in X by A7;

      hence thesis by A6, A9;

    end;

    theorem :: SQUARE_1:1

    (( min (x,y)) + ( max (x,y))) = (x + y)

    proof

      per cases ;

        suppose

         A1: x <= y;

        then ( min (x,y)) = x by XXREAL_0:def 9;

        hence thesis by A1, XXREAL_0:def 10;

      end;

        suppose

         A2: x > y;

        then ( min (x,y)) = y by XXREAL_0:def 9;

        hence thesis by A2, XXREAL_0:def 10;

      end;

    end;

    theorem :: SQUARE_1:2

    for x,y be Real st 0 <= x & 0 <= y holds ( max (x,y)) <= (x + y)

    proof

      let x,y be Real;

      assume that

       A1: 0 <= x and

       A2: 0 <= y;

      now

        per cases by XXREAL_0: 16;

          suppose

           A3: ( max (x,y)) = x;

          (x + 0 ) <= (x + y) by A2, XREAL_1: 7;

          hence thesis by A3;

        end;

          suppose

           A4: ( max (x,y)) = y;

          (y + 0 ) <= (y + x) by A1, XREAL_1: 7;

          hence thesis by A4;

        end;

      end;

      hence thesis;

    end;

    definition

      let x be Complex;

      :: SQUARE_1:def1

      func x ^2 -> number equals (x * x);

      correctness ;

    end

    registration

      let x be Complex;

      cluster (x ^2 ) -> complex;

      coherence ;

    end

    registration

      let x be Real;

      cluster (x ^2 ) -> real;

      coherence ;

    end

    definition

      let x be Element of COMPLEX ;

      :: original: ^2

      redefine

      func x ^2 -> Element of COMPLEX ;

      coherence by XCMPLX_0:def 2;

    end

    theorem :: SQUARE_1:3

    for a be Complex holds (a ^2 ) = (( - a) ^2 );

    theorem :: SQUARE_1:4

    for a,b be Complex holds ((a + b) ^2 ) = (((a ^2 ) + ((2 * a) * b)) + (b ^2 ));

    theorem :: SQUARE_1:5

    for a,b be Complex holds ((a - b) ^2 ) = (((a ^2 ) - ((2 * a) * b)) + (b ^2 ));

    theorem :: SQUARE_1:6

    for a be Complex holds ((a + 1) ^2 ) = (((a ^2 ) + (2 * a)) + 1);

    theorem :: SQUARE_1:7

    for a be Complex holds ((a - 1) ^2 ) = (((a ^2 ) - (2 * a)) + 1);

    theorem :: SQUARE_1:8

    for a,b be Complex holds ((a - b) * (a + b)) = ((a ^2 ) - (b ^2 ));

    theorem :: SQUARE_1:9

    for a,b be Complex holds ((a * b) ^2 ) = ((a ^2 ) * (b ^2 ));

    theorem :: SQUARE_1:10

    

     Th10: for a,b be Complex st ((a ^2 ) - (b ^2 )) <> 0 holds (1 / (a + b)) = ((a - b) / ((a ^2 ) - (b ^2 )))

    proof

      let a,b be Complex;

      assume ((a ^2 ) - (b ^2 )) <> 0 ;

      then (a - b) <> 0 ;

      

      hence (1 / (a + b)) = ((1 * (a - b)) / ((a + b) * (a - b))) by XCMPLX_1: 91

      .= ((a - b) / ((a ^2 ) - (b ^2 )));

    end;

    theorem :: SQUARE_1:11

    

     Th11: for a,b be Complex st ((a ^2 ) - (b ^2 )) <> 0 holds (1 / (a - b)) = ((a + b) / ((a ^2 ) - (b ^2 )))

    proof

      let a,b be Complex;

      assume ((a ^2 ) - (b ^2 )) <> 0 ;

      then ((a + b) * (a - b)) <> 0 ;

      then (a + b) <> 0 ;

      

      hence (1 / (a - b)) = ((1 * (a + b)) / ((a - b) * (a + b))) by XCMPLX_1: 91

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

    end;

    theorem :: SQUARE_1:12

     0 <> a implies 0 < (a ^2 ) by XREAL_1: 63;

    theorem :: SQUARE_1:13

    

     Th13: 0 < a & a < 1 implies (a ^2 ) < a

    proof

      assume that

       A1: 0 < a and

       A2: a < 1;

      (a * a) < (a * 1) by A1, A2, XREAL_1: 68;

      hence thesis;

    end;

    theorem :: SQUARE_1:14

    

     Th14: 1 < a implies a < (a ^2 )

    proof

      assume 1 < a;

      then (a * 1) < (a * a) by XREAL_1: 68;

      hence thesis;

    end;

    

     Lm1: 0 < a implies ex x st 0 < x & (x ^2 ) < a

    proof

      assume

       A1: 0 < a;

      per cases ;

        suppose

         A2: 1 <= a;

        reconsider x = (2 " ) as Real;

        take x;

        thus 0 < x;

        thus thesis by A2, XXREAL_0: 2;

      end;

        suppose

         A3: a < 1;

        take x = a;

        thus 0 < x by A1;

        thus thesis by A1, A3, Th13;

      end;

    end;

    theorem :: SQUARE_1:15

    

     Th15: 0 <= x & x <= y implies (x ^2 ) <= (y ^2 )

    proof

      assume that

       A1: 0 <= x and

       A2: x <= y;

      

       A3: (x * y) <= (y * y) by A1, A2, XREAL_1: 64;

      (x * x) <= (x * y) by A1, A2, XREAL_1: 64;

      hence thesis by A3, XXREAL_0: 2;

    end;

    theorem :: SQUARE_1:16

    

     Th16: 0 <= x & x < y implies (x ^2 ) < (y ^2 )

    proof

      assume that

       A1: 0 <= x and

       A2: x < y;

      

       A3: (x * y) < (y * y) by A1, A2, XREAL_1: 68;

      (x * x) <= (x * y) by A1, A2, XREAL_1: 64;

      hence thesis by A3, XXREAL_0: 2;

    end;

    

     Lm2: 0 <= x & 0 <= y & (x ^2 ) = (y ^2 ) implies x = y

    proof

      assume that

       A1: 0 <= x and

       A2: 0 <= y;

      assume

       A3: (x ^2 ) = (y ^2 );

      then

       A4: y <= x by A1, Th16;

      x <= y by A2, A3, Th16;

      hence thesis by A4, XXREAL_0: 1;

    end;

    definition

      let a be Real;

      assume

       A1: 0 <= a;

      :: SQUARE_1:def2

      func sqrt a -> Real means

      : Def2: 0 <= it & (it ^2 ) = a;

      existence

      proof

        defpred Y[ Real] means 0 <= $1 & a <= ($1 ^2 );

        defpred X[ Real] means $1 <= 0 or ($1 ^2 ) <= a;

        a <= (a + 1) by XREAL_1: 29;

        then

         A2: ( 0 + a) <= (((a ^2 ) + a) + (a + 1)) by A1, XREAL_1: 7;

         A3:

        now

          let x, y such that

           A4: X[x] and

           A5: Y[y];

          per cases ;

            suppose x <= 0 ;

            hence x <= y by A5;

          end;

            suppose not x <= 0 ;

            then (x ^2 ) <= (y ^2 ) by A4, A5, XXREAL_0: 2;

            hence x <= y by A5, Th16;

          end;

        end;

        consider z such that

         A6: for x, y st X[x] & Y[y] holds x <= z & z <= y from RealContinuity( A3);

        take z;

        

         A7: ((a + 1) ^2 ) = (((a ^2 ) + a) + (a + 1));

        hence 0 <= z by A1, A2, A6;

        assume

         A8: (z ^2 ) <> a;

        now

          per cases by A8, XXREAL_0: 1;

            suppose

             A9: z <= 0 ;

            then z = 0 by A1, A7, A2, A6;

            then ex c st 0 < c & (c ^2 ) < a by A1, A8, Lm1;

            hence contradiction by A1, A7, A2, A6, A9;

          end;

            suppose

             A10: (z ^2 ) < a & not z <= 0 ;

            set b = (a - (z ^2 ));

            

             A11: 0 < b by A10, XREAL_1: 50;

            then

            consider c such that

             A12: 0 < c and

             A13: (c ^2 ) < (b / 2) by Lm1;

            set eps = ( min (c,(b / (4 * z))));

            

             A14: 0 < eps by A10, A11, A12, XXREAL_0: 15;

            then

             A15: z < (z + eps) by XREAL_1: 29;

            (eps * (2 * z)) <= ((b / (2 * (2 * z))) * (2 * z)) by A10, XREAL_1: 64, XXREAL_0: 17;

            then (eps * (2 * z)) <= (((b / 2) / (2 * z)) * (2 * z)) by XCMPLX_1: 78;

            then

             A16: ((2 * z) * eps) <= (b / 2) by A10, XCMPLX_1: 87;

            (eps ^2 ) <= (c ^2 ) by A14, Th15, XXREAL_0: 17;

            then (eps ^2 ) <= (b / 2) by A13, XXREAL_0: 2;

            then

             A17: (((2 * z) * eps) + (eps ^2 )) <= ((b / 2) + (b / 2)) by A16, XREAL_1: 7;

            

             A18: ((z + eps) ^2 ) = ((z ^2 ) + (((2 * z) * eps) + (eps ^2 )));

            a = ((z ^2 ) + b);

            then ((z + eps) ^2 ) <= a by A18, A17, XREAL_1: 6;

            hence contradiction by A1, A7, A2, A6, A15;

          end;

            suppose

             A19: a < (z ^2 ) & not z <= 0 ;

            set b = ((z ^2 ) - a);

            set eps = ( min ((b / (2 * z)),z));

            

             A20: ((z - eps) ^2 ) = ((z ^2 ) - (((2 * z) * eps) - (eps ^2 )));

             0 < b by A19, XREAL_1: 50;

            then 0 < eps by A19, XXREAL_0: 15;

            then

             A21: (z - eps) < z by XREAL_1: 44;

             0 <= (eps ^2 ) by XREAL_1: 63;

            then

             A22: (((2 * z) * eps) - (eps ^2 )) <= (((2 * z) * eps) - 0 ) by XREAL_1: 13;

            (eps * (2 * z)) <= ((b / (2 * z)) * (2 * z)) by A19, XREAL_1: 64, XXREAL_0: 17;

            then ((2 * z) * eps) <= b by A19, XCMPLX_1: 87;

            then

             A23: (((2 * z) * eps) - (eps ^2 )) <= b by A22, XXREAL_0: 2;

            

             A24: 0 <= (z - eps) by XREAL_1: 48, XXREAL_0: 17;

            a = ((z ^2 ) - b);

            then a <= ((z - eps) ^2 ) by A20, A23, XREAL_1: 13;

            hence contradiction by A6, A24, A21;

          end;

        end;

        hence contradiction;

      end;

      uniqueness by Lm2;

    end

    theorem :: SQUARE_1:17

    

     Th17: ( sqrt 0 ) = 0

    proof

      ( sqrt ( 0 ^2 )) = 0 by Def2;

      hence thesis;

    end;

    theorem :: SQUARE_1:18

    

     Th18: ( sqrt 1) = 1

    proof

      ( sqrt (1 ^2 )) = 1 by Def2;

      hence thesis;

    end;

    

     Lm3: 0 <= x & x < y implies ( sqrt x) < ( sqrt y)

    proof

      assume that

       A1: 0 <= x and

       A2: x < y;

      

       A3: (( sqrt y) ^2 ) = y by A1, A2, Def2;

      

       A4: (( sqrt x) ^2 ) = x by A1, Def2;

       0 <= ( sqrt y) by A1, A2, Def2;

      hence thesis by A2, A4, A3, Th15;

    end;

    theorem :: SQUARE_1:19

    1 < ( sqrt 2) by Lm3, Th18;

    

     Lm4: (2 ^2 ) = (2 * 2);

    theorem :: SQUARE_1:20

    

     Th20: ( sqrt 4) = 2 by Def2, Lm4;

    theorem :: SQUARE_1:21

    ( sqrt 2) < 2 by Lm3, Th20;

    theorem :: SQUARE_1:22

     0 <= a implies ( sqrt (a ^2 )) = a by Def2;

    theorem :: SQUARE_1:23

    a <= 0 implies ( sqrt (a ^2 )) = ( - a)

    proof

      

       A1: (a ^2 ) = (( - a) ^2 );

      assume a <= 0 ;

      hence thesis by A1, Def2;

    end;

    theorem :: SQUARE_1:24

    

     Th24: 0 <= a & ( sqrt a) = 0 implies a = 0

    proof

       0 <= a & ( sqrt a) = 0 implies a = ( 0 ^2 ) by Def2;

      hence thesis;

    end;

    theorem :: SQUARE_1:25

    

     Th25: 0 < a implies 0 < ( sqrt a)

    proof

      assume

       A1: 0 < a;

      then ( sqrt a) <> ( 0 ^2 ) by Def2;

      hence thesis by A1, Def2;

    end;

    theorem :: SQUARE_1:26

    

     Th26: 0 <= x & x <= y implies ( sqrt x) <= ( sqrt y)

    proof

      per cases ;

        suppose x = y;

        hence thesis;

      end;

        suppose

         A1: x <> y;

        assume

         A2: 0 <= x;

        assume x <= y;

        then x < y by A1, XXREAL_0: 1;

        hence thesis by A2, Lm3;

      end;

    end;

    theorem :: SQUARE_1:27

     0 <= x & x < y implies ( sqrt x) < ( sqrt y) by Lm3;

    theorem :: SQUARE_1:28

    

     Th28: 0 <= x & 0 <= y & ( sqrt x) = ( sqrt y) implies x = y

    proof

      assume that

       A1: 0 <= x and

       A2: 0 <= y and

       A3: ( sqrt x) = ( sqrt y);

      assume x <> y;

      then x < y or y < x by XXREAL_0: 1;

      hence contradiction by A1, A2, A3, Lm3;

    end;

    theorem :: SQUARE_1:29

    

     Th29: 0 <= a & 0 <= b implies ( sqrt (a * b)) = (( sqrt a) * ( sqrt b))

    proof

      assume that

       A1: 0 <= a and

       A2: 0 <= b;

      

       A3: 0 <= ( sqrt a) by A1, Def2;

      

       A4: 0 <= ( sqrt b) by A2, Def2;

      (( sqrt (a * b)) ^2 ) = (a * b) by A1, A2, Def2

      .= ((( sqrt a) ^2 ) * b) by A1, Def2

      .= ((( sqrt a) ^2 ) * (( sqrt b) ^2 )) by A2, Def2

      .= ((( sqrt a) * ( sqrt b)) ^2 );

      

      hence ( sqrt (a * b)) = ( sqrt ((( sqrt a) * ( sqrt b)) ^2 )) by A1, A2, Def2

      .= (( sqrt a) * ( sqrt b)) by A3, A4, Def2;

    end;

    theorem :: SQUARE_1:30

    

     Th30: 0 <= a & 0 <= b implies ( sqrt (a / b)) = (( sqrt a) / ( sqrt b))

    proof

      assume that

       A1: 0 <= a and

       A2: 0 <= b;

      

       A3: (( sqrt b) ^2 ) = b by A2, Def2;

      (( sqrt a) ^2 ) = a by A1, Def2;

      then

       A4: ((( sqrt a) / ( sqrt b)) ^2 ) = (a / b) by A3, XCMPLX_1: 76;

      

       A5: 0 <= ( sqrt b) by A2, Def2;

       0 <= ( sqrt a) by A1, Def2;

      hence thesis by A5, A4, Def2;

    end;

    theorem :: SQUARE_1:31

    for a,b be Real st 0 <= a & 0 <= b holds ( sqrt (a + b)) = 0 iff a = 0 & b = 0 by Th17, Th24;

    theorem :: SQUARE_1:32

     0 < a implies ( sqrt (1 / a)) = (1 / ( sqrt a)) by Th18, Th30;

    theorem :: SQUARE_1:33

     0 < a implies (( sqrt a) / a) = (1 / ( sqrt a))

    proof

      assume

       A1: 0 < a;

      then ( sqrt a) <> ( 0 ^2 ) by Def2;

      

      hence (( sqrt a) / a) = ((( sqrt a) ^2 ) / (a * ( sqrt a))) by XCMPLX_1: 91

      .= ((1 * a) / (( sqrt a) * a)) by A1, Def2

      .= (1 / ( sqrt a)) by A1, XCMPLX_1: 91;

    end;

    theorem :: SQUARE_1:34

     0 < a implies (a / ( sqrt a)) = ( sqrt a)

    proof

      assume

       A1: 0 < a;

      then ( sqrt a) <> ( 0 ^2 ) by Def2;

      

      hence (a / ( sqrt a)) = ((a * ( sqrt a)) / (( sqrt a) ^2 )) by XCMPLX_1: 91

      .= ((( sqrt a) * a) / (1 * a)) by A1, Def2

      .= (( sqrt a) / 1) by A1, XCMPLX_1: 91

      .= ( sqrt a);

    end;

    theorem :: SQUARE_1:35

     0 <= a & 0 <= b implies ((( sqrt a) - ( sqrt b)) * (( sqrt a) + ( sqrt b))) = (a - b)

    proof

      assume that

       A1: 0 <= a and

       A2: 0 <= b;

      

      thus ((( sqrt a) - ( sqrt b)) * (( sqrt a) + ( sqrt b))) = ((( sqrt a) ^2 ) - (( sqrt b) ^2 ))

      .= (a - (( sqrt b) ^2 )) by A1, Def2

      .= (a - b) by A2, Def2;

    end;

    

     Lm5: 0 <= a & 0 <= b & a <> b implies ((( sqrt a) ^2 ) - (( sqrt b) ^2 )) <> 0

    proof

      assume that

       A1: 0 <= a and

       A2: 0 <= b and

       A3: a <> b;

      

       A4: 0 <= ( sqrt a) by A1, Def2;

      

       A5: 0 <= ( sqrt b) by A2, Def2;

      ( sqrt a) <> ( sqrt b) by A1, A2, A3, Th28;

      hence thesis by A4, A5, Lm2;

    end;

    theorem :: SQUARE_1:36

     0 <= a & 0 <= b & a <> b implies (1 / (( sqrt a) + ( sqrt b))) = ((( sqrt a) - ( sqrt b)) / (a - b))

    proof

      assume that

       A1: 0 <= a and

       A2: 0 <= b and

       A3: a <> b;

      

      thus (1 / (( sqrt a) + ( sqrt b))) = ((( sqrt a) - ( sqrt b)) / ((( sqrt a) ^2 ) - (( sqrt b) ^2 ))) by A1, A2, A3, Lm5, Th10

      .= ((( sqrt a) - ( sqrt b)) / (a - (( sqrt b) ^2 ))) by A1, Def2

      .= ((( sqrt a) - ( sqrt b)) / (a - b)) by A2, Def2;

    end;

    theorem :: SQUARE_1:37

     0 <= b & b < a implies (1 / (( sqrt a) + ( sqrt b))) = ((( sqrt a) - ( sqrt b)) / (a - b))

    proof

      assume that

       A1: 0 <= b and

       A2: b < a;

      

      thus (1 / (( sqrt a) + ( sqrt b))) = ((( sqrt a) - ( sqrt b)) / ((( sqrt a) ^2 ) - (( sqrt b) ^2 ))) by A1, A2, Lm5, Th10

      .= ((( sqrt a) - ( sqrt b)) / (a - (( sqrt b) ^2 ))) by A1, A2, Def2

      .= ((( sqrt a) - ( sqrt b)) / (a - b)) by A1, Def2;

    end;

    theorem :: SQUARE_1:38

     0 <= a & 0 <= b implies (1 / (( sqrt a) - ( sqrt b))) = ((( sqrt a) + ( sqrt b)) / (a - b))

    proof

      assume that

       A1: 0 <= a and

       A2: 0 <= b;

      per cases ;

        suppose a <> b;

        

        hence (1 / (( sqrt a) - ( sqrt b))) = ((( sqrt a) + ( sqrt b)) / ((( sqrt a) ^2 ) - (( sqrt b) ^2 ))) by A1, A2, Lm5, Th11

        .= ((( sqrt a) + ( sqrt b)) / (a - (( sqrt b) ^2 ))) by A1, Def2

        .= ((( sqrt a) + ( sqrt b)) / (a - b)) by A2, Def2;

      end;

        suppose

         A3: a = b;

        then (1 / (( sqrt a) - ( sqrt b))) = 0 ;

        hence thesis by A3;

      end;

    end;

    theorem :: SQUARE_1:39

     0 <= b & b < a implies (1 / (( sqrt a) - ( sqrt b))) = ((( sqrt a) + ( sqrt b)) / (a - b))

    proof

      assume that

       A1: 0 <= b and

       A2: b < a;

      

      thus (1 / (( sqrt a) - ( sqrt b))) = ((( sqrt a) + ( sqrt b)) / ((( sqrt a) ^2 ) - (( sqrt b) ^2 ))) by A1, A2, Lm5, Th11

      .= ((( sqrt a) + ( sqrt b)) / (a - (( sqrt b) ^2 ))) by A1, A2, Def2

      .= ((( sqrt a) + ( sqrt b)) / (a - b)) by A1, Def2;

    end;

    theorem :: SQUARE_1:40

    for x,y be Complex st (x ^2 ) = (y ^2 ) holds x = y or x = ( - y)

    proof

      let x,y be Complex;

      assume (x ^2 ) = (y ^2 );

      then ((x - y) * (x + y)) = 0 ;

      then (x - y) = 0 or (x + y) = 0 ;

      hence thesis;

    end;

    theorem :: SQUARE_1:41

    for x be Complex st (x ^2 ) = 1 holds x = 1 or x = ( - 1)

    proof

      let x be Complex;

      assume (x ^2 ) = 1;

      then ((x - 1) * (x + 1)) = 0 ;

      then (x - 1) = 0 or (x + 1) = 0 ;

      hence thesis;

    end;

    theorem :: SQUARE_1:42

     0 <= x & x <= 1 implies (x ^2 ) <= x

    proof

      assume that

       A1: 0 <= x and

       A2: x <= 1;

      per cases by A1;

        suppose 0 = x;

        hence thesis;

      end;

        suppose

         A3: 0 < x;

        per cases by A2, XXREAL_0: 1;

          suppose x = 1;

          hence thesis;

        end;

          suppose x < 1;

          hence thesis by A3, Th13;

        end;

      end;

    end;

    theorem :: SQUARE_1:43

    ((x ^2 ) - 1) <= 0 implies ( - 1) <= x & x <= 1

    proof

      assume ((x ^2 ) - 1) <= 0 ;

      then ((x - 1) * (x + 1)) <= 0 ;

      hence thesis by XREAL_1: 93;

    end;

    begin

    theorem :: SQUARE_1:44

    

     Th44: a <= 0 & x < a implies (x ^2 ) > (a ^2 )

    proof

      assume that

       A1: a <= 0 and

       A2: x < a;

      ( - x) > ( - a) by A2, XREAL_1: 24;

      then (( - x) ^2 ) > (( - a) ^2 ) by A1, Th16;

      hence thesis;

    end;

    theorem :: SQUARE_1:45

    ( - 1) >= a implies ( - a) <= (a ^2 )

    proof

      assume ( - 1) >= a;

      then ( - ( - 1)) <= ( - a) by XREAL_1: 24;

      then ( - a) <= (( - a) ^2 ) by XREAL_1: 151;

      hence thesis;

    end;

    theorem :: SQUARE_1:46

    ( - 1) > a implies ( - a) < (a ^2 )

    proof

      assume ( - 1) > a;

      then ( - ( - 1)) < ( - a) by XREAL_1: 24;

      then ( - a) < (( - a) ^2 ) by Th14;

      hence thesis;

    end;

    theorem :: SQUARE_1:47

    (b ^2 ) <= (a ^2 ) & a >= 0 implies ( - a) <= b & b <= a

    proof

      assume that

       A1: (b ^2 ) <= (a ^2 ) and

       A2: a >= 0 ;

      now

        assume

         A3: ( - a) > b or b > a;

        now

          per cases by A3;

            case ( - a) > b;

            then ( - ( - a)) < ( - b) by XREAL_1: 24;

            then (a ^2 ) < (( - b) ^2 ) by A2, Th16;

            hence contradiction by A1;

          end;

            case b > a;

            hence contradiction by A1, A2, Th16;

          end;

        end;

        hence contradiction;

      end;

      hence thesis;

    end;

    theorem :: SQUARE_1:48

    (b ^2 ) < (a ^2 ) & a >= 0 implies ( - a) < b & b < a

    proof

      assume that

       A1: (b ^2 ) < (a ^2 ) and

       A2: a >= 0 ;

      now

        assume

         A3: ( - a) >= b or b >= a;

        now

          per cases by A3;

            case ( - a) >= b;

            then ( - ( - a)) <= ( - b) by XREAL_1: 24;

            then (a ^2 ) <= (( - b) ^2 ) by A2, Th15;

            hence contradiction by A1;

          end;

            case b >= a;

            hence contradiction by A1, A2, Th15;

          end;

        end;

        hence contradiction;

      end;

      hence thesis;

    end;

    theorem :: SQUARE_1:49

    

     Th49: ( - a) <= b & b <= a implies (b ^2 ) <= (a ^2 )

    proof

      assume that

       A1: ( - a) <= b and

       A2: b <= a;

      per cases ;

        suppose b >= 0 ;

        hence thesis by A2, Th15;

      end;

        suppose

         A3: b < 0 ;

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

        then (( - b) ^2 ) <= (a ^2 ) by A3, Th15;

        hence thesis;

      end;

    end;

    theorem :: SQUARE_1:50

    ( - a) < b & b < a implies (b ^2 ) < (a ^2 )

    proof

      assume that

       A1: ( - a) < b and

       A2: b < a;

      per cases ;

        suppose b >= 0 ;

        hence thesis by A2, Th16;

      end;

        suppose

         A3: b < 0 ;

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

        then (( - b) ^2 ) < (a ^2 ) by A3, Th16;

        hence thesis;

      end;

    end;

    theorem :: SQUARE_1:51

    (a ^2 ) <= 1 implies ( - 1) <= a & a <= 1

    proof

      assume (a ^2 ) <= 1;

      then ((a ^2 ) - (1 ^2 )) <= ((1 ^2 ) - (1 ^2 )) by XREAL_1: 9;

      then ((a - 1) * (a + 1)) <= 0 ;

      hence thesis by XREAL_1: 93;

    end;

    theorem :: SQUARE_1:52

    (a ^2 ) < 1 implies ( - 1) < a & a < 1

    proof

      assume (a ^2 ) < 1;

      then ((a ^2 ) - (1 ^2 )) < ((1 ^2 ) - (1 ^2 )) by XREAL_1: 9;

      then ((a - 1) * (a + 1)) < 0 ;

      hence thesis by XREAL_1: 94;

    end;

    theorem :: SQUARE_1:53

    

     Th53: ( - 1) <= a & a <= 1 & ( - 1) <= b & b <= 1 implies ((a ^2 ) * (b ^2 )) <= 1

    proof

      assume that

       A1: ( - 1) <= a and

       A2: a <= 1 and

       A3: ( - 1) <= b and

       A4: b <= 1;

      

       A5: 0 <= (b ^2 ) by XREAL_1: 63;

      (a ^2 ) <= (1 ^2 ) by A1, A2, Th49;

      then

       A6: ((a ^2 ) * (b ^2 )) <= (1 * (b ^2 )) by A5, XREAL_1: 64;

      (b ^2 ) <= (1 ^2 ) by A3, A4, Th49;

      hence thesis by A6, XXREAL_0: 2;

    end;

    theorem :: SQUARE_1:54

    

     Th54: a >= 0 & b >= 0 implies (a * ( sqrt b)) = ( sqrt ((a ^2 ) * b))

    proof

      assume that

       A1: a >= 0 and

       A2: b >= 0 ;

      ( sqrt (a ^2 )) = a by A1, Def2;

      hence thesis by A1, A2, Th29;

    end;

    

     Lm6: ( - 1) <= a & a <= 1 & ( - 1) <= b & b <= 1 implies ((1 + (a ^2 )) * (b ^2 )) <= (1 + (b ^2 ))

    proof

      assume that

       A1: ( - 1) <= a and

       A2: a <= 1 and

       A3: ( - 1) <= b and

       A4: b <= 1;

      ((a ^2 ) * (b ^2 )) <= 1 by A1, A2, A3, A4, Th53;

      then ((1 * (b ^2 )) + ((a ^2 ) * (b ^2 ))) <= (1 + (b ^2 )) by XREAL_1: 7;

      hence thesis;

    end;

    theorem :: SQUARE_1:55

    

     Th55: ( - 1) <= a & a <= 1 & ( - 1) <= b & b <= 1 implies (( - b) * ( sqrt (1 + (a ^2 )))) <= ( sqrt (1 + (b ^2 ))) & ( - ( sqrt (1 + (b ^2 )))) <= (b * ( sqrt (1 + (a ^2 ))))

    proof

      assume that

       A1: ( - 1) <= a and

       A2: a <= 1 and

       A3: ( - 1) <= b and

       A4: b <= 1;

      

       A5: (a ^2 ) >= 0 by XREAL_1: 63;

      then

       A6: (1 + (a ^2 )) >= (1 + 0 ) by XREAL_1: 7;

      (b ^2 ) >= 0 by XREAL_1: 63;

      then

       A7: ( sqrt (1 + (b ^2 ))) >= 0 by Def2;

      

       A8: ( sqrt (1 + (a ^2 ))) >= 0 by A5, Def2;

       A9:

      now

        per cases ;

          suppose b >= 0 ;

          hence (( - b) * ( sqrt (1 + (a ^2 )))) <= ( sqrt (1 + (b ^2 ))) by A8, A7;

        end;

          suppose

           A10: b < 0 ;

          

           A11: (( - b) ^2 ) >= 0 by XREAL_1: 63;

          (( - b) * ( sqrt (1 + (a ^2 )))) = ( sqrt ((( - b) ^2 ) * (1 + (a ^2 )))) by A5, A10, Th54;

          hence (( - b) * ( sqrt (1 + (a ^2 )))) <= ( sqrt (1 + (b ^2 ))) by A1, A2, A3, A4, A6, A11, Lm6, Th26;

        end;

      end;

      then ( - (( - b) * ( sqrt (1 + (a ^2 ))))) >= ( - ( sqrt (1 + (b ^2 )))) by XREAL_1: 24;

      hence thesis by A9;

    end;

    theorem :: SQUARE_1:56

    ( - 1) <= a & a <= 1 & ( - 1) <= b & b <= 1 implies (b * ( sqrt (1 + (a ^2 )))) <= ( sqrt (1 + (b ^2 )))

    proof

      assume that

       A1: ( - 1) <= a and

       A2: a <= 1 and

       A3: ( - 1) <= b and

       A4: b <= 1;

      

       A5: ( - 1) <= ( - b) by A4, XREAL_1: 24;

      ( - ( - 1)) >= ( - b) by A3, XREAL_1: 24;

      then (( - ( - b)) * ( sqrt (1 + (a ^2 )))) <= ( sqrt (1 + (( - b) ^2 ))) by A1, A2, A5, Th55;

      hence thesis;

    end;

    

     Lm7: b <= 0 & a <= b implies (a * ( sqrt (1 + (b ^2 )))) <= (b * ( sqrt (1 + (a ^2 ))))

    proof

      assume that

       A1: b <= 0 and

       A2: a <= b;

      

       A3: (( - a) * ( sqrt (1 + (b ^2 )))) = ( sqrt ((( - a) ^2 ) * (1 + (b ^2 )))) by A1, A2, Th54;

      a < b or a = b by A2, XXREAL_0: 1;

      then (b ^2 ) < (a ^2 ) or a = b by A1, Th44;

      then

       A4: (((b ^2 ) * 1) + ((b ^2 ) * (a ^2 ))) <= (((a ^2 ) * 1) + ((a ^2 ) * (b ^2 ))) by XREAL_1: 7;

      

       A5: (b ^2 ) >= 0 by XREAL_1: 63;

      

       A6: (a ^2 ) >= 0 by XREAL_1: 63;

      then (( - b) * ( sqrt (1 + (a ^2 )))) = ( sqrt ((( - b) ^2 ) * (1 + (a ^2 )))) by A1, Th54;

      then ( - (a * ( sqrt (1 + (b ^2 ))))) >= ( - (b * ( sqrt (1 + (a ^2 ))))) by A6, A3, A4, A5, Th26;

      hence thesis by XREAL_1: 24;

    end;

    

     Lm8: for a,b be Real st a <= 0 & a <= b holds (a * ( sqrt (1 + (b ^2 )))) <= (b * ( sqrt (1 + (a ^2 ))))

    proof

      let a,b be Real;

      assume that

       A1: a <= 0 and

       A2: a <= b;

      now

        per cases ;

          case b <= 0 ;

          hence thesis by A2, Lm7;

        end;

          case

           A3: b > 0 ;

          (b ^2 ) >= 0 by XREAL_1: 63;

          then ( sqrt (1 + (b ^2 ))) > 0 by Th25;

          then

           A4: (a * ( sqrt (1 + (b ^2 )))) <= 0 by A1;

          (a ^2 ) >= 0 by XREAL_1: 63;

          then ( sqrt (1 + (a ^2 ))) > 0 by Th25;

          hence thesis by A3, A4;

        end;

      end;

      hence thesis;

    end;

    

     Lm9: for a,b be Real st a >= 0 & a >= b holds (a * ( sqrt (1 + (b ^2 )))) >= (b * ( sqrt (1 + (a ^2 ))))

    proof

      let a,b be Real;

      assume that

       A1: a >= 0 and

       A2: a >= b;

      ( - a) <= ( - b) by A2, XREAL_1: 24;

      then (( - a) * ( sqrt (1 + (( - b) ^2 )))) <= (( - b) * ( sqrt (1 + (( - a) ^2 )))) by A1, Lm8;

      then ( - (a * ( sqrt (1 + (b ^2 ))))) <= ( - (b * ( sqrt (1 + (a ^2 )))));

      hence thesis by XREAL_1: 24;

    end;

    theorem :: SQUARE_1:57

    a >= b implies (a * ( sqrt (1 + (b ^2 )))) >= (b * ( sqrt (1 + (a ^2 ))))

    proof

      assume

       A1: a >= b;

      per cases ;

        suppose a >= 0 ;

        hence thesis by A1, Lm9;

      end;

        suppose a < 0 ;

        hence thesis by A1, Lm7;

      end;

    end;

    theorem :: SQUARE_1:58

    a >= 0 implies ( sqrt (a + (b ^2 ))) >= b

    proof

      assume

       A1: a >= 0 ;

      per cases ;

        suppose b < 0 ;

        hence thesis by A1, Def2;

      end;

        suppose

         A2: b >= 0 ;

        

         A3: (b ^2 ) >= 0 by XREAL_1: 63;

        (a + (b ^2 )) >= ( 0 + (b ^2 )) by A1, XREAL_1: 6;

        then ( sqrt (a + (b ^2 ))) >= ( sqrt (b ^2 )) by A3, Th26;

        hence ( sqrt (a + (b ^2 ))) >= b by A2, Def2;

      end;

    end;

    theorem :: SQUARE_1:59

     0 <= a & 0 <= b implies ( sqrt (a + b)) <= (( sqrt a) + ( sqrt b))

    proof

      assume that

       A1: 0 <= a and

       A2: 0 <= b;

      

       A3: 0 <= ( sqrt a) by A1, Def2;

       0 <= ( sqrt (a * b)) by A1, A2, Def2;

      then 0 <= (( sqrt a) * ( sqrt b)) by A1, A2, Th29;

      then 0 <= (2 * (( sqrt a) * ( sqrt b)));

      then (a + 0 ) <= (a + ((2 * ( sqrt a)) * ( sqrt b))) by XREAL_1: 6;

      then

       A4: (a + b) <= ((a + ((2 * ( sqrt a)) * ( sqrt b))) + b) by XREAL_1: 6;

      

       A5: 0 <= ( sqrt b) by A2, Def2;

      ( sqrt ((a + ((2 * ( sqrt a)) * ( sqrt b))) + b)) = ( sqrt (((( sqrt a) ^2 ) + ((2 * ( sqrt a)) * ( sqrt b))) + b)) by A1, Def2

      .= ( sqrt (((( sqrt a) ^2 ) + ((2 * ( sqrt a)) * ( sqrt b))) + (( sqrt b) ^2 ))) by A2, Def2

      .= ( sqrt ((( sqrt a) + ( sqrt b)) ^2 ))

      .= (( sqrt a) + ( sqrt b)) by A3, A5, Def2;

      hence thesis by A1, A2, A4, Th26;

    end;