absvalue.miz



    begin

    reserve x,y,z,r,s,t for Real;

    definition

      let x be Real;

      :: original: |.

      redefine

      :: ABSVALUE:def1

      func |.x.| equals

      : Def1: x if 0 <= x

      otherwise ( - x);

      correctness by COMPLEX1: 43, COMPLEX1: 70;

    end

    registration

      let x be non negative Real;

      reduce |.x.| to x;

      reducibility by Def1;

    end

    theorem :: ABSVALUE:1

     |.x.| = x or |.x.| = ( - x) by Def1;

    theorem :: ABSVALUE:2

    x = 0 iff |.x.| = 0 by COMPLEX1: 47;

    theorem :: ABSVALUE:3

     |.x.| = ( - x) & x <> 0 implies x < 0 by Def1;

    theorem :: ABSVALUE:4

    ( - |.x.|) <= x & x <= |.x.|

    proof

      per cases ;

        suppose

         A1: x < 0 ;

        then |.x.| = ( - x) by Def1;

        hence thesis by A1;

      end;

        suppose

         A2: 0 <= x;

        then ( - x) <= ( - 0 );

        hence thesis by A2, Def1;

      end;

    end;

    theorem :: ABSVALUE:5

    ( - y) <= x & x <= y iff |.x.| <= y

    proof

      hereby

        assume that

         A1: ( - y) <= x and

         A2: x <= y;

        ( - x) <= ( - ( - y)) by A1, XREAL_1: 24;

        hence |.x.| <= y by A2, Def1;

      end;

      assume

       A3: |.x.| <= y;

      then

       A4: 0 <= y by COMPLEX1: 46;

      per cases ;

        suppose 0 < x;

        hence thesis by A3, A4, Def1;

      end;

        suppose

         A5: x < 0 ;

        then ( - x) <= y by A3, Def1;

        then ( - y) <= ( - ( - x)) by XREAL_1: 24;

        hence thesis by A5;

      end;

        suppose x = ( - 0 );

        hence thesis by A3;

      end;

    end;

    theorem :: ABSVALUE:6

    x <> 0 implies ( |.x.| * |.(1 / x).|) = 1

    proof

      assume x <> 0 ;

      then ( |.x.| * |.(1 / x).|) = |.(x * (1 / x)).| & |.(x * (1 / x)).| = |.1.| by COMPLEX1: 65, XCMPLX_1: 106;

      hence thesis;

    end;

    theorem :: ABSVALUE:7

     |.(1 / x).| = (1 / |.x.|) by COMPLEX1: 80;

    theorem :: ABSVALUE:8

     0 <= (x * y) implies ( sqrt (x * y)) = (( sqrt |.x.|) * ( sqrt |.y.|))

    proof

      assume 0 <= (x * y);

      then |.(x * y).| = (x * y) by Def1;

      then

       A1: ( |.x.| * |.y.|) = (x * y) by COMPLEX1: 65;

       0 <= |.x.| & 0 <= |.y.| by COMPLEX1: 46;

      hence thesis by A1, SQUARE_1: 29;

    end;

    theorem :: ABSVALUE:9

     |.x.| <= z & |.y.| <= t implies |.(x + y).| <= (z + t)

    proof

      assume |.x.| <= z & |.y.| <= t;

      then |.(x + y).| <= ( |.x.| + |.y.|) & ( |.x.| + |.y.|) <= (z + t) by COMPLEX1: 56, XREAL_1: 7;

      hence thesis by XXREAL_0: 2;

    end;

    theorem :: ABSVALUE:10

     0 < (x / y) implies ( sqrt (x / y)) = (( sqrt |.x.|) / ( sqrt |.y.|))

    proof

      assume 0 < (x / y);

      then (x / y) = |.(x / y).| by Def1;

      then

       A1: (x / y) = ( |.x.| / |.y.|) by COMPLEX1: 67;

       0 <= |.x.| & 0 <= |.y.| by COMPLEX1: 46;

      hence thesis by A1, SQUARE_1: 30;

    end;

    theorem :: ABSVALUE:11

     0 <= (x * y) implies |.(x + y).| = ( |.x.| + |.y.|)

    proof

      assume

       A1: 0 <= (x * y);

      per cases by A1;

        suppose (x * y) = 0 ;

        then x = 0 or y = 0 by XCMPLX_1: 6;

        hence thesis;

      end;

        suppose

         A5: 0 < (x * y);

        then

         A6: x <> 0 & y <> 0 ;

        per cases by A5, A6;

          suppose that

           A7: 0 < x & 0 < y;

           |.x.| = x & |.y.| = y by A7, Def1;

          hence thesis by A7, Def1;

        end;

          suppose that

           A8: x < 0 and

           A9: y < 0 ;

           |.x.| = ( - x) by A8, Def1;

          

          then ( |.x.| + |.y.|) = ((( - 1) * x) + ( - (1 * y))) by A9, Def1

          .= ( - (x + y));

          hence thesis by A8, A9, Def1;

        end;

      end;

    end;

    theorem :: ABSVALUE:12

     |.(x + y).| = ( |.x.| + |.y.|) implies 0 <= (x * y)

    proof

      

       A1: (x * y) < 0 implies x < 0 & 0 < y or 0 < x & y < 0

      proof

        assume

         A2: (x * y) < 0 ;

        then x <> 0 & y <> 0 ;

        hence thesis by A2;

      end;

      

       A3: x < 0 & 0 < y & (x + y) < 0 implies |.(x + y).| <> ( |.x.| + |.y.|)

      proof

        assume that

         A4: x < 0 and

         A5: 0 < y and

         A6: (x + y) < 0 ;

        (( - (1 * x)) + ( - y)) < (( - x) + y) by A5, XREAL_1: 6;

        then

         A7: ( - (1 * (x + y))) < (( - x) + y);

         |.x.| = ( - x) & |.y.| = y by A4, A5, Def1;

        hence thesis by A6, A7, Def1;

      end;

      

       A8: 0 < x & y < 0 & (x + y) < 0 implies |.(x + y).| <> ( |.x.| + |.y.|)

      proof

        assume that

         A9: 0 < x and

         A10: y < 0 and

         A11: (x + y) < 0 ;

        (( - (1 * x)) + ( - y)) < (x + ( - y)) by A9, XREAL_1: 6;

        then

         A12: ( - (1 * (x + y))) < (x + ( - y));

         |.x.| = x & |.y.| = ( - y) by A9, A10, Def1;

        hence thesis by A11, A12, Def1;

      end;

      

       A13: 0 < x & y < 0 & 0 <= (x + y) implies |.(x + y).| <> ( |.x.| + |.y.|)

      proof

        assume that

         A14: 0 < x and

         A15: y < 0 and

         A16: 0 <= (x + y);

        

         A17: |.y.| = ( - y) by A15, Def1;

        (x + y) < (x + ( - y)) & |.x.| = x by A14, A15, Def1, XREAL_1: 6;

        hence thesis by A16, A17, Def1;

      end;

      

       A18: x < 0 & 0 < y & 0 <= (x + y) implies |.(x + y).| <> ( |.x.| + |.y.|)

      proof

        assume that

         A19: x < 0 and

         A20: 0 < y and

         A21: 0 <= (x + y);

        

         A22: |.y.| = y by A20, Def1;

        (x + y) < (( - x) + y) & |.x.| = ( - x) by A19, Def1, XREAL_1: 6;

        hence thesis by A21, A22, Def1;

      end;

      assume |.(x + y).| = ( |.x.| + |.y.|) & 0 > (x * y);

      hence contradiction by A1, A3, A18, A8, A13;

    end;

    theorem :: ABSVALUE:13

    ( |.(x + y).| / (1 + |.(x + y).|)) <= (( |.x.| / (1 + |.x.|)) + ( |.y.| / (1 + |.y.|)))

    proof

      

       A1: s <= t & 0 < (1 + s) & 0 < (1 + t) implies (s / (1 + s)) <= (t / (1 + t))

      proof

        assume that

         A2: s <= t and

         A3: 0 < (1 + s) and

         A4: 0 < (1 + t);

        ((s * 1) + (s * t)) <= (t + (s * t)) by A2, XREAL_1: 6;

        then ((s * (1 + t)) * ((1 + s) " )) <= ((t * (1 + s)) * ((1 + s) " )) by A3, XREAL_1: 64;

        then ((s * (1 + t)) * ((1 + s) " )) <= (t * ((1 + s) * ((1 + s) " )));

        then ((s * (1 + t)) * ((1 + s) " )) <= (t * 1) by A3, XCMPLX_0:def 7;

        then (((s * ((1 + s) " )) * (1 + t)) * ((1 + t) " )) <= (t * ((1 + t) " )) by A4, XREAL_1: 64;

        then ((s * ((1 + s) " )) * ((1 + t) * ((1 + t) " ))) <= (t * ((1 + t) " ));

        then ((s * ((1 + s) " )) * 1) <= (t * ((1 + t) " )) by A4, XCMPLX_0:def 7;

        then (s / (1 + s)) <= (t * ((1 + t) " )) by XCMPLX_0:def 9;

        hence thesis by XCMPLX_0:def 9;

      end;

      set a = |.x.|, b = |.y.|, c = |.(x + y).|;

      

       A5: 0 <= a by COMPLEX1: 46;

      

       A6: 0 <= b by COMPLEX1: 46;

      

       A7: ( 0 + 0 ) < (1 + a) by COMPLEX1: 46, XREAL_1: 8;

      

       A8: 0 < (1 + a) & 0 < ((1 + a) + b) implies (a / ((1 + a) + b)) <= (a / (1 + a))

      proof

        assume that

         A9: 0 < (1 + a) and

         A10: 0 < ((1 + a) + b);

        ( 0 + a) <= ((a * b) + a) by A5, A6, XREAL_1: 6;

        then ((a * 1) + (a * a)) <= ((a * (1 + b)) + (a * a)) by XREAL_1: 6;

        then ((a * (1 + a)) * ((1 + a) " )) <= ((a * ((1 + a) + b)) * ((1 + a) " )) by A9, XREAL_1: 64;

        then (a * ((1 + a) * ((1 + a) " ))) <= ((a * ((1 + a) + b)) * ((1 + a) " ));

        then (a * 1) <= ((a * ((1 + a) + b)) * ((1 + a) " )) by A7, XCMPLX_0:def 7;

        then (a * (((1 + a) + b) " )) <= (((a * ((1 + a) " )) * ((1 + a) + b)) * (((1 + a) + b) " )) by A10, XREAL_1: 64;

        then (a * (((1 + a) + b) " )) <= ((a * ((1 + a) " )) * (((1 + a) + b) * (((1 + a) + b) " )));

        then (a * (((1 + a) + b) " )) <= ((a * ((1 + a) " )) * 1) by A5, A6, XCMPLX_0:def 7;

        then (a / ((1 + a) + b)) <= (a * ((1 + a) " )) by XCMPLX_0:def 9;

        hence thesis by XCMPLX_0:def 9;

      end;

      

       A11: ( 0 + 0 ) < (1 + b) by COMPLEX1: 46, XREAL_1: 8;

      

       A12: 0 < (1 + b) & 0 < ((1 + a) + b) implies (b / ((1 + a) + b)) <= (b / (1 + b))

      proof

        assume that

         A13: 0 < (1 + b) and

         A14: 0 < ((1 + a) + b);

        ( 0 + b) <= ((a * b) + b) by A5, A6, XREAL_1: 6;

        then ((b * 1) + (b * b)) <= (((1 + a) * b) + (b * b)) by XREAL_1: 6;

        then ((b * (1 + b)) * ((1 + b) " )) <= ((b * ((1 + a) + b)) * ((1 + b) " )) by A13, XREAL_1: 64;

        then (b * ((1 + b) * ((1 + b) " ))) <= ((b * ((1 + a) + b)) * ((1 + b) " ));

        then (b * 1) <= ((b * ((1 + a) + b)) * ((1 + b) " )) by A11, XCMPLX_0:def 7;

        then (b * (((1 + a) + b) " )) <= (((b * ((1 + b) " )) * ((1 + a) + b)) * (((1 + a) + b) " )) by A14, XREAL_1: 64;

        then (b * (((1 + a) + b) " )) <= ((b * ((1 + b) " )) * (((1 + a) + b) * (((1 + a) + b) " )));

        then (b * (((1 + a) + b) " )) <= ((b * ((1 + b) " )) * 1) by A5, A6, XCMPLX_0:def 7;

        then (b / ((1 + a) + b)) <= (b * ((1 + b) " )) by XCMPLX_0:def 9;

        hence thesis by XCMPLX_0:def 9;

      end;

      ( 0 + 0 ) < (1 + c) by COMPLEX1: 46, XREAL_1: 8;

      then

       A15: (c / (1 + c)) <= ((a + b) / (1 + (a + b))) by A5, A6, A1, COMPLEX1: 56;

      ((a + b) / ((1 + a) + b)) = ((a / ((1 + a) + b)) + (b / ((1 + a) + b))) by XCMPLX_1: 62;

      then ((a + b) / ((1 + a) + b)) <= ((a / (1 + a)) + (b / (1 + b))) by A6, A7, A8, A12, XREAL_1: 7;

      hence thesis by A15, XXREAL_0: 2;

    end;

    definition

      let x;

      :: ABSVALUE:def2

      func sgn x -> Real equals

      : Def2: 1 if 0 < x,

( - 1) if x < 0

      otherwise 0 ;

      coherence ;

      consistency ;

      projectivity ;

    end

    registration

      let x;

      cluster ( sgn x) -> integer;

      coherence

      proof

        x = 0 or x > 0 or x < 0 ;

        hence thesis by Def2;

      end;

    end

    theorem :: ABSVALUE:14

    ( sgn x) = 1 implies 0 < x

    proof

      assume that

       A1: ( sgn x) = 1 and

       A2: 0 >= x;

      x < 0 or x = 0 by A2;

      hence contradiction by A1, Def2;

    end;

    theorem :: ABSVALUE:15

    ( sgn x) = ( - 1) implies x < 0

    proof

      assume that

       A1: ( sgn x) = ( - 1) and

       A2: x >= 0 ;

       0 < x or x = 0 by A2;

      hence contradiction by A1, Def2;

    end;

    theorem :: ABSVALUE:16

    

     Th16: ( sgn x) = 0 implies x = 0

    proof

      assume that

       A1: ( sgn x) = 0 and

       A2: x <> 0 ;

       0 < x or x < 0 by A2;

      hence contradiction by A1, Def2;

    end;

    theorem :: ABSVALUE:17

    x = ( |.x.| * ( sgn x))

    proof

      

       A1: 0 < x implies x = ( |.x.| * ( sgn x))

      proof

        assume

         A2: 0 < x;

        then |.x.| = x by Def1;

        then ( |.x.| * ( sgn x)) = (x * 1) by A2, Def2;

        hence thesis;

      end;

      

       A3: x < 0 implies x = ( |.x.| * ( sgn x))

      proof

        assume

         A4: x < 0 ;

        then |.x.| = ( - x) by Def1;

        

        then ( |.x.| * ( sgn x)) = (( - x) * ( - 1)) by A4, Def2

        .= x;

        hence thesis;

      end;

      x = 0 implies x = ( |.x.| * ( sgn x));

      hence thesis by A1, A3;

    end;

    theorem :: ABSVALUE:18

    

     Th18: ( sgn (x * y)) = (( sgn x) * ( sgn y))

    proof

      

       A1: 0 < x & 0 < y implies ( sgn (x * y)) = (( sgn x) * ( sgn y))

      proof

        assume that

         A2: 0 < x and

         A3: 0 < y;

        

         A4: ( sgn y) = 1 by A3, Def2;

        ( 0 * y) < (x * y) & ( sgn x) = 1 by A2, A3, Def2, XREAL_1: 68;

        hence thesis by A4, Def2;

      end;

      

       A5: 0 < x & y < 0 implies ( sgn (x * y)) = (( sgn x) * ( sgn y))

      proof

        assume that

         A6: 0 < x and

         A7: y < 0 ;

        ( sgn y) = ( - 1) by A7, Def2;

        

        then

         A8: (( sgn x) * ( sgn y)) = (1 * ( - 1)) by A6, Def2

        .= ( - 1);

        (x * y) < ( 0 * y) by A6, A7, XREAL_1: 69;

        hence thesis by A8, Def2;

      end;

      

       A9: x < 0 & y < 0 implies ( sgn (x * y)) = (( sgn x) * ( sgn y))

      proof

        assume that

         A10: x < 0 and

         A11: y < 0 ;

        ( sgn y) = ( - 1) by A11, Def2;

        

        then

         A12: (( sgn x) * ( sgn y)) = (( - 1) * ( - 1)) by A10, Def2

        .= 1;

        (x * 0 ) < (x * y) by A10, A11, XREAL_1: 69;

        hence thesis by A12, Def2;

      end;

      

       A13: x < 0 & 0 < y implies ( sgn (x * y)) = (( sgn x) * ( sgn y))

      proof

        assume that

         A14: x < 0 and

         A15: 0 < y;

        ( sgn y) = 1 by A15, Def2;

        then

         A16: (( sgn x) * ( sgn y)) = ( - 1) by A14, Def2;

        (x * y) < ( 0 * y) by A14, A15, XREAL_1: 68;

        hence thesis by A16, Def2;

      end;

      x = 0 or y = 0 implies ( sgn (x * y)) = (( sgn x) * ( sgn y))

      proof

        assume

         A17: x = 0 or y = 0 ;

        then ( sgn x) = 0 or ( sgn y) = 0 by Def2;

        hence thesis by A17;

      end;

      hence thesis by A1, A5, A13, A9;

    end;

    ::$Canceled

    theorem :: ABSVALUE:20

    ( sgn (x + y)) <= ((( sgn x) + ( sgn y)) + 1)

    proof

      

       A1: y = 0 implies ( sgn (x + y)) <= ((( sgn x) + ( sgn y)) + 1)

      proof

        assume

         A2: y = 0 ;

        

        then ((( sgn x) + ( sgn y)) + 1) = ((( sgn x) + 0 ) + 1) by Def2

        .= (( sgn x) + 1);

        hence thesis by A2, XREAL_1: 29;

      end;

      

       A3: 0 < x & 0 < y implies ( sgn (x + y)) <= ((( sgn x) + ( sgn y)) + 1)

      proof

        ( sgn x) < (( sgn x) + 1) by XREAL_1: 29;

        then

         A4: (( sgn x) + 0 ) < ((( sgn x) + 1) + 1) by XREAL_1: 8;

        assume

         A5: 0 < x & 0 < y;

        then ( sgn x) = 1 & ( sgn y) = 1 by Def2;

        hence thesis by A5, A4, Def2;

      end;

      

       A6: x < 0 & 0 < y implies ( sgn (x + y)) <= ((( sgn x) + ( sgn y)) + 1)

      proof

        assume that

         A7: x < 0 and

         A8: 0 < y;

        ( sgn x) = ( - 1) by A7, Def2;

        then

         A9: ((( sgn x) + ( sgn y)) + 1) = 1 by A8, Def2;

        (x + y) < 0 or (x + y) = 0 or 0 < (x + y);

        hence thesis by A9, Def2;

      end;

      

       A10: 0 < x & y < 0 implies ( sgn (x + y)) <= ((( sgn x) + ( sgn y)) + 1)

      proof

        assume that

         A11: 0 < x and

         A12: y < 0 ;

        ( sgn x) = 1 by A11, Def2;

        

        then

         A13: ((( sgn x) + ( sgn y)) + 1) = ((1 + ( - 1)) + 1) by A12, Def2

        .= 1;

        (x + y) < 0 or (x + y) = 0 or 0 < (x + y);

        hence thesis by A13, Def2;

      end;

      

       A14: x < 0 & y < 0 implies ( sgn (x + y)) <= ((( sgn x) + ( sgn y)) + 1)

      proof

        assume that

         A15: x < 0 and

         A16: y < 0 ;

        ( sgn y) = ( - 1) by A16, Def2;

        then ((( sgn x) + ( sgn y)) + 1) = ( - 1) by A15, Def2;

        hence thesis by A15, A16, Def2;

      end;

      x = 0 implies ( sgn (x + y)) <= ((( sgn x) + ( sgn y)) + 1)

      proof

        assume

         A17: x = 0 ;

        

        then ((( sgn x) + ( sgn y)) + 1) = (( 0 + ( sgn y)) + 1) by Def2

        .= (( sgn y) + 1);

        hence thesis by A17, XREAL_1: 29;

      end;

      hence thesis by A3, A10, A6, A14, A1;

    end;

    theorem :: ABSVALUE:21

    

     Th20: x <> 0 implies (( sgn x) * ( sgn (1 / x))) = 1

    proof

      assume x <> 0 ;

      then ( sgn (x * (1 / x))) = ( sgn 1) by XCMPLX_1: 106;

      then ( sgn (x * (1 / x))) = 1 by Def2;

      hence thesis by Th18;

    end;

    theorem :: ABSVALUE:22

    

     Th21: (1 / ( sgn x)) = ( sgn (1 / x))

    proof

      per cases ;

        suppose

         A1: x = 0 ;

        

        hence (1 / ( sgn x)) = (1 / 0 ) by Def2

        .= ( sgn (1 / x)) by A1, Def2;

      end;

        suppose

         A2: x <> 0 ;

        then ((( sgn x) * ( sgn (1 / x))) * (1 / ( sgn x))) = (1 * (1 / ( sgn x))) by Th20;

        then (( sgn (1 / x)) * (( sgn x) * (1 / ( sgn x)))) = (1 / ( sgn x));

        then (( sgn (1 / x)) * 1) = (1 / ( sgn x)) by A2, Th16, XCMPLX_1: 106;

        hence thesis;

      end;

    end;

    theorem :: ABSVALUE:23

    ((( sgn x) + ( sgn y)) - 1) <= ( sgn (x + y))

    proof

      

       A1: x = 0 or y = 0 implies ((( sgn x) + ( sgn y)) - 1) <= ( sgn (x + y))

      proof

        

         A2: y = 0 implies ((( sgn x) + ( sgn y)) - 1) <= ( sgn (x + y))

        proof

          

           A3: (( sgn x) - 1) < ((( sgn x) + ( - 1)) + 1) by XREAL_1: 29;

          assume

           A4: y = 0 ;

          

          then ((( sgn x) + ( sgn y)) - 1) = ((( sgn x) + 0 ) - 1) by Def2

          .= (( sgn x) - 1);

          hence thesis by A4, A3;

        end;

        

         A5: x = 0 implies ((( sgn x) + ( sgn y)) - 1) <= ( sgn (x + y))

        proof

          

           A6: (( sgn y) - 1) < ((( sgn y) + ( - 1)) + 1) by XREAL_1: 29;

          assume

           A7: x = 0 ;

          

          then ((( sgn x) + ( sgn y)) - 1) = (( 0 + ( sgn y)) - 1) by Def2

          .= (( sgn y) - 1);

          hence thesis by A7, A6;

        end;

        assume x = 0 or y = 0 ;

        hence thesis by A5, A2;

      end;

      

       A8: x < 0 & y < 0 implies ((( sgn x) + ( sgn y)) - 1) <= ( sgn (x + y))

      proof

        assume that

         A9: x < 0 and

         A10: y < 0 ;

        ( sgn x) = ( - 1) by A9, Def2;

        then

         A11: ( sgn x) = ( sgn (x + y)) by A9, A10, Def2;

        

         A12: ((( sgn (x + y)) + ( - 1)) - 1) < (((( sgn (x + y)) + ( - 1)) - 1) + 1) & (( sgn (x + y)) + ( - 1)) < ((( sgn (x + y)) + ( - 1)) + 1) by XREAL_1: 29;

        ( sgn y) = ( - 1) by A10, Def2;

        hence thesis by A11, A12, XXREAL_0: 2;

      end;

      

       A13: 0 < x & y < 0 implies ((( sgn x) + ( sgn y)) - 1) <= ( sgn (x + y))

      proof

        assume that

         A14: 0 < x and

         A15: y < 0 ;

        ( sgn x) = 1 by A14, Def2;

        

        then

         A16: (( sgn x) + ( sgn y)) = (1 + ( - 1)) by A15, Def2

        .= 0 ;

        (x + y) < 0 or (x + y) = 0 or 0 < (x + y);

        hence thesis by A16, Def2;

      end;

      

       A17: x < 0 & 0 < y implies ((( sgn x) + ( sgn y)) - 1) <= ( sgn (x + y))

      proof

        assume that

         A18: x < 0 and

         A19: 0 < y;

        ( sgn x) = ( - 1) by A18, Def2;

        

        then

         A20: (( sgn x) + ( sgn y)) = (( - 1) + 1) by A19, Def2

        .= 0 ;

        (x + y) < 0 or (x + y) = 0 or 0 < (x + y);

        hence thesis by A20, Def2;

      end;

       0 < x & 0 < y implies ((( sgn x) + ( sgn y)) - 1) <= ( sgn (x + y))

      proof

        assume that

         A21: 0 < x and

         A22: 0 < y;

        ( sgn y) = 1 by A22, Def2;

        then ((( sgn x) + ( sgn y)) - 1) = 1 by A21, Def2;

        hence thesis by A21, A22, Def2;

      end;

      hence thesis by A8, A17, A13, A1;

    end;

    theorem :: ABSVALUE:24

    ( sgn x) = ( sgn (1 / x))

    proof

      

       A1: 0 < x implies ( sgn x) = ( sgn (1 / x))

      proof

        assume

         A2: 0 < x;

        ( sgn (1 / x)) = (1 / ( sgn x)) by Th21;

        

        then ( sgn (1 / x)) = (1 / 1) by A2, Def2

        .= 1;

        hence thesis by A2, Def2;

      end;

      x < 0 implies ( sgn x) = ( sgn (1 / x))

      proof

        assume

         A3: x < 0 ;

        then ( sgn x) = ( - 1) by Def2;

        then ( sgn (1 / x)) = (1 / ( - 1)) by Th21;

        hence thesis by A3, Def2;

      end;

      hence thesis by A1;

    end;

    theorem :: ABSVALUE:25

    ( sgn (x / y)) = (( sgn x) / ( sgn y))

    proof

      per cases ;

        suppose

         A1: y = 0 ;

        

        hence ( sgn (x / y)) = ( sgn (x * ( 0 " ))) by XCMPLX_0:def 9

        .= (( sgn x) * ( 0 " )) by Def2

        .= (( sgn x) / 0 ) by XCMPLX_0:def 9

        .= (( sgn x) / ( sgn y)) by A1, Def2;

      end;

        suppose

         A2: y <> 0 ;

        (x / y) = ((x / y) * 1)

        .= ((x / y) * (y * (1 / y))) by A2, XCMPLX_1: 106

        .= (((x / y) * y) * (1 / y))

        .= (x * (1 / y)) by A2, XCMPLX_1: 87;

        

        then ( sgn (x / y)) = (( sgn x) * ( sgn (1 / y))) by Th18

        .= ((( sgn x) / 1) * (1 / ( sgn y))) by Th21

        .= ((( sgn x) * 1) / (1 * ( sgn y))) by XCMPLX_1: 76

        .= (( sgn x) / (1 * ( sgn y)));

        hence thesis;

      end;

    end;

    theorem :: ABSVALUE:26

     0 <= (r + |.r.|)

    proof

      

       A1: 0 <= |.r.| by COMPLEX1: 46;

      ( |.r.| + |.r.|) = (r + |.r.|) or ( |.r.| + r) = (( - r) + r) by Def1;

      hence thesis by A1;

    end;

    theorem :: ABSVALUE:27

     0 <= (( - r) + |.r.|)

    proof

      ( - r) >= ( - |.r.|) by XREAL_1: 24, COMPLEX1: 76;

      then (( - r) + |.r.|) >= (( - |.r.|) + |.r.|) by XREAL_1: 7;

      hence thesis;

    end;

    theorem :: ABSVALUE:28

     |.r.| = |.s.| implies r = s or r = ( - s)

    proof

      assume

       A1: |.r.| = |.s.|;

      assume

       A2: r <> s;

      per cases by Def1;

        suppose |.r.| = r & |.s.| = s;

        hence thesis by A1, A2;

      end;

        suppose |.r.| = r & |.s.| = ( - s);

        hence thesis by A1;

      end;

        suppose |.r.| = ( - r) & |.s.| = s;

        hence thesis by A1;

      end;

        suppose |.r.| = ( - r) & |.s.| = ( - s);

        hence thesis by A1, A2;

      end;

    end;

    theorem :: ABSVALUE:29

    for m be Nat holds m = |.m.|;

    theorem :: ABSVALUE:30

    r <= 0 implies |.r.| = ( - r)

    proof

      assume r <= 0 ;

      then r < 0 or r = 0 ;

      hence thesis by Def1;

    end;