xxreal_3.miz



    begin

    reserve x,y,z,w for ExtReal,

r for Real;

    definition

      let x, y;

      :: original: <=

      redefine

      :: XXREAL_3:def1

      pred x <= y means

      : Def1: ex p,q be Element of REAL st p = x & q = y & p <= q if x in REAL & y in REAL

      otherwise x = -infty or y = +infty ;

      consistency ;

      compatibility

      proof

        thus x in REAL & y in REAL implies (x <= y iff ex p,q be Element of REAL st p = x & q = y & p <= q);

        thus not (x in REAL & y in REAL ) implies (x <= y iff x = -infty or y = +infty )

        proof

          assume

           A1: not (x in REAL & y in REAL );

          per cases by A1;

            suppose

             A2: not x in REAL ;

            thus x <= y implies x = -infty or y = +infty

            proof

              assume

               A3: x <= y;

              assume x <> -infty ;

              then x = +infty by A2, XXREAL_0: 14;

              hence thesis by A3, XXREAL_0: 4;

            end;

            thus thesis by XXREAL_0: 3, XXREAL_0: 5;

          end;

            suppose

             A4: not y in REAL ;

            thus x <= y implies x = -infty or y = +infty

            proof

              assume

               A5: x <= y;

              assume

               A6: x <> -infty ;

              assume y <> +infty ;

              then y = -infty by A4, XXREAL_0: 14;

              hence thesis by A5, A6, XXREAL_0: 6;

            end;

            thus thesis by XXREAL_0: 3, XXREAL_0: 5;

          end;

        end;

      end;

    end

    registration

      cluster non real positive for ExtReal;

      existence

      proof

        take +infty ;

        thus thesis;

      end;

      cluster non real negative for ExtReal;

      existence

      proof

        take -infty ;

        thus thesis;

      end;

    end

    theorem :: XXREAL_3:1

    

     Th1: for x be non real positive ExtReal holds x = +infty

    proof

      let x be non real positive ExtReal;

       not x in REAL ;

      hence thesis by XXREAL_0: 14;

    end;

    theorem :: XXREAL_3:2

    

     Th2: for x be non real negative ExtReal holds x = -infty

    proof

      let x be non real negative ExtReal;

       not x in REAL ;

      hence thesis by XXREAL_0: 14;

    end;

    registration

      cluster non real non negative -> positive for ExtReal;

      coherence ;

      cluster non real non positive -> negative for ExtReal;

      coherence ;

    end

    theorem :: XXREAL_3:3

    

     Th3: x < z implies ex y be Real st x < y & y < z

    proof

      assume

       A1: x < z;

      per cases by XXREAL_0: 14;

        suppose x in REAL & z in REAL ;

        hence thesis by A1, XREAL_1: 5;

      end;

        suppose x = +infty or z = -infty ;

        hence thesis by A1, XXREAL_0: 4, XXREAL_0: 6;

      end;

        suppose

         A2: z = +infty ;

        per cases by A1, A2, XXREAL_0: 14;

          suppose x = -infty ;

          hence thesis by A2;

        end;

          suppose x in REAL ;

          then

          reconsider x1 = x as Real;

          take (x1 + 1);

          

           A3: (x1 + 1) in REAL by XREAL_0:def 1;

          (x1 + 0 ) < (x1 + 1) by XREAL_1: 8;

          hence thesis by A2, A3, XXREAL_0: 9;

        end;

      end;

        suppose

         A4: x = -infty ;

        per cases by A1, A4, XXREAL_0: 14;

          suppose z = +infty ;

          hence thesis by A4;

        end;

          suppose z in REAL ;

          then

          reconsider z1 = z as Real;

          take (z1 - 1);

          

           A5: (z1 - 1) in REAL by XREAL_0:def 1;

          (z1 - 1) < (z1 - 0 ) by XREAL_1: 10;

          hence thesis by A4, A5, XXREAL_0: 12;

        end;

      end;

    end;

    begin

    definition

      let x,y be ExtReal;

      :: XXREAL_3:def2

      func x + y -> ExtReal means

      : Def2: ex a,b be Complex st x = a & y = b & it = (a + b) if x is real & y is real,

it = +infty if x = +infty & y <> -infty or y = +infty & x <> -infty ,

it = -infty if x = -infty & y <> +infty or y = -infty & x <> +infty

      otherwise it = 0 ;

      existence

      proof

        thus x is real & y is real implies ex c be ExtReal, a,b be Complex st x = a & y = b & c = (a + b)

        proof

          assume x is real & y is real;

          then

          reconsider a = x, b = y as Real;

          take (a + b), a, b;

          thus thesis;

        end;

        thus thesis;

      end;

      uniqueness ;

      consistency ;

      commutativity ;

    end

    definition

      let x be ExtReal;

      :: XXREAL_3:def3

      func - x -> ExtReal means

      : Def3: ex a be Complex st x = a & it = ( - a) if x is real,

it = -infty if x = +infty

      otherwise it = +infty ;

      existence

      proof

        thus x is real implies ex c be ExtReal, a be Complex st x = a & c = ( - a)

        proof

          assume x is real;

          then

          reconsider a = x as Real;

          take ( - a), a;

          thus thesis;

        end;

        thus thesis;

      end;

      uniqueness ;

      consistency ;

      involutiveness

      proof

        let y,x be ExtReal such that

         A1: x is real implies ex a be Complex st x = a & y = ( - a) and

         A2: x = +infty implies y = -infty and

         A3: not x is real & x <> +infty implies y = +infty ;

        thus y is real implies ex a be Complex st y = a & x = ( - a)

        proof

          assume y is real;

          then

          consider a be Complex such that

           A4: x = a & y = ( - a) by A1, A2, A3;

          take ( - a);

          thus thesis by A4;

        end;

        x in REAL implies x is real;

        hence y = +infty implies x = -infty by A1, A2, XXREAL_0: 14;

        thus thesis by A1, A3;

      end;

    end

    definition

      let x,y be ExtReal;

      :: XXREAL_3:def4

      func x - y -> ExtReal equals (x + ( - y));

      coherence ;

    end

    registration

      let x,y be Real, a,b be Complex;

      identify a + b with x + y when x = a, y = b;

      compatibility by Def2;

    end

    registration

      let x be Real, a be Complex;

      identify - a with - x when x = a;

      compatibility by Def3;

    end

    registration

      let r be Real;

      cluster ( - r) -> real;

      coherence ;

    end

    registration

      let r,s be Real;

      cluster (r + s) -> real;

      coherence ;

      cluster (r - s) -> real;

      coherence ;

    end

    registration

      let x be Real, y be non real ExtReal;

      cluster (x + y) -> non real;

      coherence

      proof

         not y in REAL ;

        then

         A1: y = -infty or y = +infty by XXREAL_0: 14;

        let z be object;

        assume z = (x + y);

        hence thesis by A1, Def2;

      end;

    end

    registration

      let x,y be non real positive ExtReal;

      cluster (x + y) -> non real;

      coherence

      proof

        x = +infty by Th1;

        hence thesis by Def2;

      end;

    end

    registration

      let x,y be non real negative ExtReal;

      cluster (x + y) -> non real;

      coherence

      proof

        x = -infty by Th2;

        hence thesis by Def2;

      end;

    end

    registration

      let x be non real negative ExtReal, y be non real positive ExtReal;

      cluster (x + y) -> zero;

      coherence

      proof

        x = -infty & y = +infty by Th1, Th2;

        hence thesis by Def2;

      end;

    end

    registration

      let x,y be Real, a,b be Complex;

      identify a - b with x - y when x = a, y = b;

      compatibility ;

    end

    theorem :: XXREAL_3:4

    

     Th4: (x + 0 ) = x

    proof

      per cases by XXREAL_0: 14;

        suppose x in REAL ;

        then

        reconsider r = x as Real;

        (r + 0 ) = r;

        hence thesis;

      end;

        suppose x = -infty or x = +infty ;

        hence thesis by Def2;

      end;

    end;

    theorem :: XXREAL_3:5

    

     Th5: ( - -infty ) = +infty by Def3;

    theorem :: XXREAL_3:6

    

     Th6: ( - +infty ) = -infty by Def3;

    

     Lm1: ( +infty + +infty ) = +infty by Def2;

    

     Lm2: ( -infty + -infty ) = -infty by Def2;

    theorem :: XXREAL_3:7

    

     Th7: (x + ( - x)) = 0

    proof

      per cases by XXREAL_0: 14;

        suppose x = -infty ;

        hence thesis by Th5;

      end;

        suppose x in REAL ;

        then

        reconsider x as Real;

        reconsider y = ( - x) as Real;

        (x + y) = 0 ;

        hence thesis;

      end;

        suppose x = +infty ;

        hence thesis by Th6;

      end;

    end;

    theorem :: XXREAL_3:8

    (x + y) = 0 implies x = ( - y)

    proof

      assume

       A1: (x + y) = 0 ;

      per cases by XXREAL_0: 14;

        suppose x in REAL ;

        then

        reconsider x as Real;

        (x + y) is real by A1;

        then

        reconsider y as Real;

        (x + y) = 0 by A1;

        then x = ( - y);

        hence thesis;

      end;

        suppose

         A2: x = -infty ;

        then y = +infty by A1, Def2;

        hence thesis by A2, Def3;

      end;

        suppose

         A3: x = +infty ;

        then y = -infty by A1, Def2;

        hence thesis by A3, Def3;

      end;

    end;

    

     Lm3: for x holds ( - x) in REAL iff x in REAL

    proof

      let x;

      hereby

        assume ( - x) in REAL ;

        then

        reconsider a = ( - x) as Real;

        ( - a) in REAL by XREAL_0:def 1;

        hence x in REAL ;

      end;

      assume x in REAL ;

      then

      reconsider a = x as Real;

      ( - a) is real;

      hence thesis by XREAL_0:def 1;

    end;

    

     Lm4: ( - ( +infty + -infty )) = (( - -infty ) - +infty )

    proof

      

      thus ( - ( +infty + -infty )) = ( +infty - +infty ) by Def3

      .= (( - -infty ) - +infty ) by Def3;

    end;

    

     Lm5: ( - +infty ) = -infty by Def3;

    

     Lm6: x in REAL implies ( - (x + +infty )) = (( - +infty ) + ( - x))

    proof

      assume

       A1: x in REAL ;

      then (x + +infty ) = +infty by Def2;

      hence thesis by A1, Def2, Th6;

    end;

    

     Lm7: x in REAL implies ( - (x + -infty )) = (( - -infty ) + ( - x))

    proof

      assume

       A1: x in REAL ;

      then (x + -infty ) = -infty by Def2;

      hence thesis by A1, Def2, Th5;

    end;

    theorem :: XXREAL_3:9

    

     Th9: ( - (x + y)) = (( - x) + ( - y))

    proof

      per cases by XXREAL_0: 14;

        suppose

         A1: x = +infty & y = +infty ;

        

        hence ( - (x + y)) = ( - +infty ) by Def2

        .= (( - x) + ( - y)) by A1, Def2, Lm5;

      end;

        suppose x = +infty & y = -infty ;

        hence thesis by Lm4;

      end;

        suppose x = +infty & y in REAL ;

        hence thesis by Lm6;

      end;

        suppose x = -infty & y = +infty ;

        hence thesis by Lm4;

      end;

        suppose

         A2: x = -infty & y = -infty ;

        

        hence ( - (x + y)) = ( - -infty ) by Def2

        .= (( - x) + ( - y)) by A2, Def2, Th5;

      end;

        suppose x = -infty & y in REAL ;

        hence thesis by Lm7;

      end;

        suppose x in REAL & y = +infty ;

        hence thesis by Lm6;

      end;

        suppose x in REAL & y = -infty ;

        hence thesis by Lm7;

      end;

        suppose x in REAL & y in REAL ;

        then

        reconsider a = x, b = y as Real;

        ( - (x + y)) = ( - (a + b))

        .= (( - a) + ( - b));

        hence thesis;

      end;

    end;

    reserve f,g for ExtReal;

    theorem :: XXREAL_3:10

    

     Th10: ( - f) = ( - g) implies f = g

    proof

      assume

       A1: ( - f) = ( - g);

      per cases by XXREAL_0: 14;

        suppose

         A2: f in REAL ;

        now

          assume not g in REAL ;

          then g = +infty or g = -infty by XXREAL_0: 14;

          hence contradiction by A1, A2, Def3;

        end;

        then

         A3: ex a be Complex st g = a & ( - g) = ( - a) by Def3;

        ex a be Complex st f = a & ( - f) = ( - a) by A2, Def3;

        hence thesis by A1, A3;

      end;

        suppose f = +infty ;

        hence thesis by A1, Th5;

      end;

        suppose f = -infty ;

        then ( - ( - g)) = -infty by A1;

        hence thesis by A1;

      end;

    end;

    

     Lm8: (x + y) = +infty implies x = +infty or y = +infty

    proof

      assume

       A1: (x + y) = +infty ;

      assume ( not x = +infty ) & not y = +infty ;

      then x in REAL & y in REAL or x in REAL & y = -infty or x = -infty & y in REAL or x = -infty & y = -infty by XXREAL_0: 14;

      hence thesis by A1, Def2;

    end;

    

     Lm9: (x + y) = -infty implies (x = -infty or y = -infty )

    proof

      assume

       A1: (x + y) = -infty ;

      assume ( not x = -infty ) & not y = -infty ;

      then x in REAL & y in REAL or x in REAL & y = +infty or x = +infty & y in REAL or x = +infty & y = +infty by XXREAL_0: 14;

      hence thesis by A1, Def2;

    end;

    theorem :: XXREAL_3:11

    

     Th11: (r + f) = (r + g) implies f = g

    proof

      assume

       A1: (r + f) = (r + g);

      per cases by XXREAL_0: 14;

        suppose

         A2: f in REAL ;

        now

          assume not g in REAL ;

          then g = +infty or g = -infty by XXREAL_0: 14;

          hence contradiction by A1, A2;

        end;

        then

         A3: ex c,d be Complex st r = c & g = d & (r + g) = (c + d) by Def2;

        ex a,b be Complex st r = a & f = b & (r + f) = (a + b) by A2, Def2;

        hence thesis by A1, A3;

      end;

        suppose

         A4: f = +infty ;

        then (r + f) = +infty by Def2;

        hence thesis by A1, A4, Lm8;

      end;

        suppose

         A5: f = -infty ;

        then (r + f) = -infty by Def2;

        hence thesis by A1, A5, Lm9;

      end;

    end;

    theorem :: XXREAL_3:12

    (r - f) = (r - g) implies f = g

    proof

      assume (r - f) = (r - g);

      then ( - f) = ( - g) by Th11;

      hence thesis by Th10;

    end;

    theorem :: XXREAL_3:13

    

     Th13: x <> +infty implies ( +infty - x) = +infty & (x - +infty ) = -infty

    proof

      assume

       A1: x <> +infty ;

      then ( - x) <> -infty by Th5;

      hence ( +infty - x) = +infty by Def2;

      ( - +infty ) = -infty by Def3;

      hence thesis by A1, Def2;

    end;

    theorem :: XXREAL_3:14

    

     Th14: x <> -infty implies ( -infty - x) = -infty & (x - -infty ) = +infty

    proof

      assume

       A1: x <> -infty ;

      now

        assume ( - x) = +infty ;

        then ( - ( - x)) = -infty by Def3;

        hence contradiction by A1;

      end;

      hence ( -infty - x) = -infty by Def2;

      thus thesis by A1, Def2, Th5;

    end;

    theorem :: XXREAL_3:15

    

     Th15: (x - 0 ) = x

    proof

      per cases by XXREAL_0: 14;

        suppose x in REAL ;

        then

        reconsider a = x as Real;

        (x - 0 ) = (a - 0 )

        .= x;

        hence thesis;

      end;

        suppose x = -infty ;

        hence thesis by Th14;

      end;

        suppose x = +infty ;

        hence thesis by Th13;

      end;

    end;

    theorem :: XXREAL_3:16

    (x + y) = +infty implies x = +infty or y = +infty by Lm8;

    theorem :: XXREAL_3:17

    (x + y) = -infty implies (x = -infty or y = -infty ) by Lm9;

    theorem :: XXREAL_3:18

    

     Th18: (x - y) = +infty implies (x = +infty or y = -infty )

    proof

      assume

       A1: (x - y) = +infty ;

      assume ( not x = +infty ) & not y = -infty ;

      then x in REAL & y in REAL or x in REAL & y = +infty or x = -infty & y in REAL or x = -infty & y = +infty by XXREAL_0: 14;

      hence thesis by A1, Th13, Th14;

    end;

    theorem :: XXREAL_3:19

    

     Th19: (x - y) = -infty implies (x = -infty or y = +infty )

    proof

      assume

       A1: (x - y) = -infty ;

      assume ( not x = -infty ) & not y = +infty ;

      then x in REAL & y in REAL or x in REAL & y = -infty or x = +infty & y in REAL or x = +infty & y = -infty by XXREAL_0: 14;

      hence thesis by A1, Th13, Th14;

    end;

    theorem :: XXREAL_3:20

    

     Th20: not (x = +infty & y = -infty or x = -infty & y = +infty ) & (x + y) in REAL implies x in REAL & y in REAL

    proof

      assume

       A1: ( not (x = +infty & y = -infty or x = -infty & y = +infty )) & (x + y) in REAL ;

      

       A2: x in REAL or x = -infty or x = +infty by XXREAL_0: 14;

      

       A3: y in REAL or y = -infty or y = +infty by XXREAL_0: 14;

      assume not (x in REAL & y in REAL );

      hence thesis by A1, A2, A3;

    end;

    theorem :: XXREAL_3:21

    

     Th21: not (x = +infty & y = +infty or x = -infty & y = -infty ) & (x - y) in REAL implies x in REAL & y in REAL

    proof

      assume

       A1: ( not (x = +infty & y = +infty or x = -infty & y = -infty )) & (x - y) in REAL ;

      

       A2: x in REAL or x = -infty or x = +infty by XXREAL_0: 14;

      

       A3: y in REAL or y = -infty or y = +infty by XXREAL_0: 14;

      assume not (x in REAL & y in REAL );

      hence thesis by A1, A2, A3, Th13, Th14;

    end;

    theorem :: XXREAL_3:22

    

     Th22: x is real implies ((y - x) + x) = y & ((y + x) - x) = y

    proof

      assume

       A1: x is real;

      per cases by A1, XXREAL_0: 14;

        suppose x in REAL & y in REAL ;

        then

        reconsider a = x, b = y as Real;

        

         A2: ((y + x) - x) = ((b + a) - a)

        .= y;

        ((y - x) + x) = ((b - a) + a)

        .= y;

        hence thesis by A2;

      end;

        suppose

         A3: x in REAL & y = -infty ;

        then (y - x) = -infty by Def2;

        hence thesis by A3, Def2;

      end;

        suppose

         A4: x in REAL & y = +infty ;

        then (y - x) = +infty by Def2;

        hence thesis by A4, Def2;

      end;

    end;

    theorem :: XXREAL_3:23

    

     Th23: (x = +infty iff ( - x) = -infty ) & (x = -infty iff ( - x) = +infty )

    proof

      ( - x) = +infty implies x = -infty

      proof

        assume ( - x) = +infty ;

        then ( - ( - x)) = -infty by Def3;

        hence thesis;

      end;

      hence thesis by Th5;

    end;

    theorem :: XXREAL_3:24

    z is real implies x = ((x + z) - z)

    proof

      assume

       A1: z is real;

      per cases by XXREAL_0: 14;

        suppose

         A2: x = +infty ;

        then (x + z) = +infty by A1, Def2;

        hence thesis by A1, A2, Th13;

      end;

        suppose

         A3: x = -infty ;

        then (x + z) = -infty by A1, Def2;

        hence thesis by A1, A3, Th14;

      end;

        suppose x is Element of REAL ;

        then

        reconsider a = x, c = z as Real by A1;

        ((x + z) - z) = ((a + c) - c);

        hence thesis;

      end;

    end;

    

     Lm10: ( - +infty ) = -infty by Def3;

    

     Lm11: x in REAL implies ( - (x + -infty )) = (( - -infty ) + ( - x))

    proof

      

       A1: ( - -infty ) = +infty by Th23;

      assume

       A2: x in REAL ;

      then (x + -infty ) = -infty by Def2;

      hence thesis by A2, A1, Def2;

    end;

    theorem :: XXREAL_3:25

    

     Th25: ( - (x + y)) = (( - y) - x)

    proof

      per cases by XXREAL_0: 14;

        suppose

         A1: x = +infty & y = +infty ;

        

        hence ( - (x + y)) = ( - +infty ) by Def2

        .= (( - y) - x) by A1, Def2, Lm10;

      end;

        suppose x = +infty & y = -infty ;

        hence thesis by Lm4;

      end;

        suppose x = +infty & y in REAL ;

        hence thesis by Lm6;

      end;

        suppose x = -infty & y = +infty ;

        hence thesis by Lm4;

      end;

        suppose

         A2: x = -infty & y = -infty ;

        

        hence ( - (x + y)) = ( - -infty ) by Def2

        .= (( - y) - x) by A2, Def2, Th5;

      end;

        suppose x = -infty & y in REAL ;

        hence thesis by Lm11;

      end;

        suppose x in REAL & y = +infty ;

        hence thesis by Lm6;

      end;

        suppose x in REAL & y = -infty ;

        hence thesis by Lm11;

      end;

        suppose x in REAL & y in REAL ;

        then

        reconsider a = x, b = y as Real;

        ( - (x + y)) = ( - (a + b))

        .= (( - a) + ( - b));

        hence thesis;

      end;

    end;

    theorem :: XXREAL_3:26

    ( - (x - y)) = (( - x) + y) & ( - (x - y)) = (y - x)

    proof

      ( - (x - y)) = (( - ( - y)) - x) by Th25;

      hence thesis;

    end;

    theorem :: XXREAL_3:27

    

     Th27: ( - (( - x) + y)) = (x - y) & ( - (( - x) + y)) = (x + ( - y))

    proof

      ( - (( - x) + y)) = (( - ( - x)) - y) by Th25

      .= (x - y);

      hence thesis;

    end;

    theorem :: XXREAL_3:28

     0 <= y & y < +infty implies z = ((z + y) - y)

    proof

      assume 0 <= y & y < +infty ;

      then y in REAL by XXREAL_0: 14;

      hence thesis by Th22;

    end;

    theorem :: XXREAL_3:29

    

     Th29: not (x = +infty & y = -infty ) & not (x = -infty & y = +infty ) & not (y = +infty & z = -infty or y = -infty & z = +infty ) & not (x = +infty & z = -infty or x = -infty & z = +infty ) implies ((x + y) + z) = (x + (y + z))

    proof

      assume

       A1: ( not (x = +infty & y = -infty or x = -infty & y = +infty )) & not (y = +infty & z = -infty or y = -infty & z = +infty ) & not (x = +infty & z = -infty or x = -infty & z = +infty );

      per cases by A1, XXREAL_0: 14;

        suppose x in REAL & y in REAL & z in REAL ;

        then

        reconsider A = x, B = y, C = z as Real;

        ((A + B) + C) = ((x + y) + z) & (A + (B + C)) = (x + (y + z));

        hence thesis;

      end;

        suppose

         A2: x in REAL & y = +infty & z in REAL ;

        then (x + y) = +infty & (y + z) = +infty by Def2;

        hence thesis by A2;

      end;

        suppose

         A3: x in REAL & y = -infty & z in REAL ;

        then (x + y) = -infty & (y + z) = -infty by Def2;

        hence thesis by A3;

      end;

        suppose

         A4: x = -infty & y in REAL & z in REAL ;

        then (x + y) = -infty by Def2;

        then ((x + y) + z) = -infty by A4, Def2;

        hence thesis by A4, Def2;

      end;

        suppose

         A5: x = +infty & y in REAL & z in REAL ;

        then (x + y) = +infty by Def2;

        then ((x + y) + z) = +infty by A5, Def2;

        hence thesis by A5, Def2;

      end;

        suppose

         A6: x in REAL & y in REAL & z = +infty ;

        then (y + z) = +infty by Def2;

        then (x + (y + z)) = +infty by A6, Def2;

        hence thesis by A6, Def2;

      end;

        suppose

         A7: x in REAL & y in REAL & z = -infty ;

        then (y + z) = -infty by Def2;

        then (x + (y + z)) = -infty by A7, Def2;

        hence thesis by A7, Def2;

      end;

        suppose

         A8: x = +infty & y = +infty & z in REAL ;

        then (x + y) = +infty by Def2;

        then

         A9: ((x + y) + z) = +infty by A8, Def2;

        (y + z) <> -infty by A8, Def2;

        hence thesis by A8, A9, Def2;

      end;

        suppose

         A10: x in REAL & y = -infty & z = -infty ;

        then

         A11: (x + y) = -infty by Def2;

        then ((x + y) + z) = -infty by A10, Def2;

        hence thesis by A10, A11;

      end;

        suppose

         A12: x = -infty & y = -infty & z in REAL ;

        then

         A13: (x + y) = -infty by Def2;

        then ((x + y) + z) = -infty by A12, Def2;

        hence thesis by A12, A13;

      end;

        suppose x = -infty & y in REAL & z = -infty or x = -infty & y = -infty & z = -infty or x = +infty & y in REAL & z = +infty or x = +infty & y = +infty & z = +infty ;

        hence thesis;

      end;

        suppose

         A14: x in REAL & y = +infty & z = +infty ;

        then (x + y) = +infty & (y + z) = +infty by Def2;

        hence thesis by A14;

      end;

    end;

    theorem :: XXREAL_3:30

    

     Th30: not (x = +infty & y = -infty ) & not (x = -infty & y = +infty ) & not (y = +infty & z = +infty ) & not (y = -infty & z = -infty ) & not (x = +infty & z = +infty ) & not (x = -infty & z = -infty ) implies ((x + y) - z) = (x + (y - z))

    proof

      assume that

       A1: ( not (x = +infty & y = -infty )) & not (x = -infty & y = +infty ) and

       A2: ( not (y = +infty & z = +infty )) & not (y = -infty & z = -infty ) and

       A3: ( not (x = +infty & z = +infty )) & not (x = -infty & z = -infty );

      

       A4: ( not (x = +infty & ( - z) = -infty )) & not (x = -infty & ( - z) = +infty ) by A3, Th23;

      ( not (y = +infty & ( - z) = -infty )) & not (y = -infty & ( - z) = +infty ) by A2, Th23;

      hence thesis by A1, A4, Th29;

    end;

    theorem :: XXREAL_3:31

     not (x = +infty & y = +infty ) & not (x = -infty & y = -infty ) & not (y = +infty & z = -infty ) & not (y = -infty & z = +infty ) & not (x = +infty & z = +infty ) & not (x = -infty & z = -infty ) implies ((x - y) - z) = (x - (y + z))

    proof

      assume that

       A1: not (x = +infty & y = +infty ) and

       A2: not (x = -infty & y = -infty ) and

       A3: not (y = +infty & z = -infty ) and

       A4: not (y = -infty & z = +infty ) and

       A5: not (x = +infty & z = +infty ) and

       A6: not (x = -infty & z = -infty );

      per cases ;

        suppose

         A7: x = +infty ;

        then (x - y) = +infty by A1, Th13;

        then

         A8: ((x - y) - z) = +infty by A5, A7, Th13;

        (y + z) <> +infty by A1, A5, A7, Lm8;

        hence thesis by A7, A8, Th13;

      end;

        suppose

         A9: x = -infty ;

        then (x - y) = -infty by A2, Th14;

        then

         A10: ((x - y) - z) = -infty by A6, A9, Th14;

        (y + z) <> -infty by A2, A6, A9, Lm9;

        hence thesis by A9, A10, Th14;

      end;

        suppose

         A11: x <> +infty & x <> -infty ;

        then x in REAL by XXREAL_0: 14;

        then

        reconsider a = x as Real;

        per cases ;

          suppose

           A12: y = +infty ;

          then (x - y) = -infty & (y + z) = +infty by A3, A11, Def2, Th13;

          hence thesis by A3, A12, Th14;

        end;

          suppose

           A13: y = -infty ;

          then (x - y) = +infty & (y + z) = -infty by A4, A11, Def2, Th14;

          hence thesis by A4, A13, Th13;

        end;

          suppose y <> +infty & y <> -infty ;

          then y in REAL by XXREAL_0: 14;

          then

          reconsider b = y as Real;

          

           A14: (x - y) = (a - b);

          per cases ;

            suppose z = +infty ;

            then ((x - y) - z) = -infty & (y + z) = +infty by A14, Def2, Th13;

            hence thesis by A11, Th13;

          end;

            suppose z = -infty ;

            then ((x - y) - z) = +infty & (y + z) = -infty by A14, Def2, Th14;

            hence thesis by A11, Th14;

          end;

            suppose z <> +infty & z <> -infty ;

            then z in REAL by XXREAL_0: 14;

            then

            reconsider c = z as Real;

            ((x - y) - z) = ((a - b) - c) & (x - (y + z)) = (a - (b + c));

            hence thesis;

          end;

        end;

      end;

    end;

    theorem :: XXREAL_3:32

    

     Th32: not (x = +infty & y = +infty ) & not (x = -infty & y = -infty ) & not (y = +infty & z = +infty ) & not (y = -infty & z = -infty ) & not (x = +infty & z = -infty ) & not (x = -infty & z = +infty ) implies ((x - y) + z) = (x - (y - z))

    proof

      assume that

       A1: not (x = +infty & y = +infty ) and

       A2: not (x = -infty & y = -infty ) and

       A3: not (y = +infty & z = +infty ) and

       A4: not (y = -infty & z = -infty ) and

       A5: not (x = +infty & z = -infty ) and

       A6: not (x = -infty & z = +infty );

      per cases ;

        suppose

         A7: x = +infty ;

        then (x - y) = +infty by A1, Th13;

        then

         A8: ((x - y) + z) = +infty by A5, A7, Def2;

        (y - z) <> +infty by A1, A5, A7, Th18;

        hence thesis by A7, A8, Th13;

      end;

        suppose

         A9: x = -infty ;

        then (x - y) = -infty by A2, Th14;

        then

         A10: ((x - y) + z) = -infty by A6, A9, Def2;

        (y - z) <> -infty by A2, A6, A9, Th19;

        hence thesis by A9, A10, Th14;

      end;

        suppose

         A11: x <> +infty & x <> -infty ;

        then x in REAL by XXREAL_0: 14;

        then

        reconsider a = x as Real;

        per cases ;

          suppose

           A12: y = +infty ;

          then (x - y) = -infty & (y - z) = +infty by A3, A11, Th13;

          hence thesis by A3, A12, Def2;

        end;

          suppose

           A13: y = -infty ;

          then (x - y) = +infty & (y - z) = -infty by A4, A11, Th14;

          hence thesis by A4, A13, Def2;

        end;

          suppose y <> +infty & y <> -infty ;

          then y in REAL by XXREAL_0: 14;

          then

          reconsider b = y as Real;

          

           A14: (x - y) = (a - b);

          per cases ;

            suppose z = +infty ;

            then ((x - y) + z) = +infty & (y - z) = -infty by A14, Def2, Th13;

            hence thesis by A11, Th14;

          end;

            suppose z = -infty ;

            then ((x - y) + z) = -infty & (y - z) = +infty by A14, Def2, Th14;

            hence thesis by A11, Th13;

          end;

            suppose z <> +infty & z <> -infty ;

            then z in REAL by XXREAL_0: 14;

            then

            reconsider c = z as Real;

            ((x - y) + z) = ((a - b) + c) & (x - (y - z)) = (a - (b - c));

            hence thesis;

          end;

        end;

      end;

    end;

    theorem :: XXREAL_3:33

    

     Th33: z is real implies ((z + x) - (z + y)) = (x - y)

    proof

      assume

       A1: z is real;

      per cases by A1, XXREAL_0: 14;

        suppose

         A2: x = -infty ;

        per cases by XXREAL_0: 14;

          suppose

           A3: y = -infty ;

          ((z + -infty ) - (z + -infty )) = ( -infty - (z + -infty )) by A1, Def2

          .= ( -infty - -infty ) by A1, Def2;

          hence thesis by A2, A3;

        end;

          suppose

           A4: y = +infty ;

          ((z + -infty ) - (z + +infty )) = ( -infty - (z + +infty )) by A1, Def2

          .= ( -infty - +infty ) by A1, Def2;

          hence thesis by A2, A4;

        end;

          suppose

           A5: y in REAL ;

          then

          consider a,b be Complex such that

           A6: z = a & y = b and (z + y) = (a + b) by A1, Def2;

          reconsider a, b as Real by A1, A5, A6;

          

           A7: (a + b) in REAL by XREAL_0:def 1;

          ((z + -infty ) - (z + y)) = ( -infty - (z + y)) by A1, Def2

          .= -infty by A6, A7, Def2

          .= ( -infty - y) by A5, Def2;

          hence thesis by A2;

        end;

      end;

        suppose

         A8: y = +infty ;

        per cases by XXREAL_0: 14;

          suppose

           A9: x = -infty ;

          ((z + -infty ) - (z + +infty )) = ((z + -infty ) - +infty ) by A1, Def2

          .= ( -infty - +infty ) by A1, Def2;

          hence thesis by A8, A9;

        end;

          suppose

           A10: x = +infty ;

          ((z + +infty ) - (z + +infty )) = ((z + +infty ) - +infty ) by A1, Def2

          .= ( +infty - +infty ) by A1, Def2;

          hence thesis by A8, A10;

        end;

          suppose

           A11: x in REAL ;

          then

          consider a,b be Complex such that

           A12: z = a & x = b and (z + x) = (a + b) by A1, Def2;

          reconsider a, b as Real by A1, A11, A12;

          

           A13: (a + b) in REAL by XREAL_0:def 1;

          

           A14: ( - +infty ) = -infty by Def3;

          ((z + x) - (z + +infty )) = ((z + x) - +infty ) by A1, Def2

          .= ((z + x) + -infty ) by Def3

          .= -infty by A12, A13, Def2

          .= (x + ( - +infty )) by A11, A14, Def2;

          hence thesis by A8;

        end;

      end;

        suppose x in REAL & y in REAL & z in REAL ;

        then

        reconsider a = x, b = y, c = z as Real;

        ((z + x) - (z + y)) = ((a + c) - (c + b))

        .= (a - b)

        .= (x - y);

        hence thesis;

      end;

        suppose

         A15: x = +infty & y in REAL & z in REAL ;

        then

        reconsider c = z, b = y as Real;

        

         A16: (z + y) = (c + b);

        (z + x) = +infty & (x - y) = +infty by A15, Def2;

        hence thesis by A16, Th13;

      end;

        suppose

         A17: x in REAL & y = -infty & z in REAL ;

        then

        reconsider c = z, a = x as Real;

        (z + x) = (c + a) & (z + y) = -infty by A17, Def2;

        

        then ((z + x) - (z + y)) = +infty by Th14

        .= (x - y) by A17, Th14;

        hence thesis;

      end;

        suppose

         A18: x = +infty & y = -infty & z in REAL ;

        then (z + y) = -infty & not (z + x) = -infty by Def2;

        

        then ((z + x) - (z + y)) = +infty by Th14

        .= (x - y) by A18, Th14;

        hence thesis;

      end;

    end;

    theorem :: XXREAL_3:34

    y is real implies ((z - y) + (y - x)) = (z - x)

    proof

      assume

       A1: y is real;

      

      thus ((z - y) + (y - x)) = ((z - y) - (x - y)) by Th27

      .= (z - x) by A1, Th33;

    end;

    begin

    

     Lm12: x <= y implies (x + z) <= (y + z)

    proof

      assume

       A1: x <= y;

      per cases by XXREAL_0: 14;

        suppose

         A2: x in REAL & y in REAL ;

        per cases by XXREAL_0: 14;

          suppose

           A3: z = -infty ;

           -infty <= (y + z) by XXREAL_0: 5;

          hence thesis by A2, A3, Def2;

        end;

          suppose z in REAL ;

          then

          reconsider x, y, z as Real by A2;

          (x + z) <= (y + z) by A1, XREAL_1: 6;

          hence thesis;

        end;

          suppose

           A4: z = +infty ;

          (x + z) <= +infty by XXREAL_0: 3;

          hence thesis by A2, A4, Def2;

        end;

      end;

        suppose

         A5: x in REAL & y = +infty ;

        per cases by XXREAL_0: 14;

          suppose

           A6: z = -infty ;

           -infty <= (y + z) by XXREAL_0: 5;

          hence thesis by A5, A6, Def2;

        end;

          suppose

           A7: z in REAL ;

          (x + z) <= +infty by XXREAL_0: 3;

          hence thesis by A5, A7, Def2;

        end;

          suppose z = +infty ;

          hence thesis by A5, Lm1, XXREAL_0: 3;

        end;

      end;

        suppose

         A8: x = -infty & y in REAL ;

        per cases by XXREAL_0: 14;

          suppose z = -infty ;

          hence thesis by A8, Lm2, XXREAL_0: 5;

        end;

          suppose

           A9: z in REAL ;

           -infty <= (y + z) by XXREAL_0: 5;

          hence thesis by A8, A9, Def2;

        end;

          suppose

           A10: z = +infty ;

          (x + z) <= +infty by XXREAL_0: 3;

          hence thesis by A8, A10, Def2;

        end;

      end;

        suppose

         A11: x = -infty & y = +infty ;

        per cases by XXREAL_0: 14;

          suppose z = -infty ;

          hence thesis by A11, Lm2;

        end;

          suppose

           A12: z in REAL ;

           -infty <= (y + z) by XXREAL_0: 5;

          hence thesis by A11, A12, Def2;

        end;

          suppose z = +infty ;

          hence thesis by A11, Lm1;

        end;

      end;

        suppose x = +infty ;

        hence thesis by A1, XXREAL_0: 4;

      end;

        suppose y = -infty ;

        hence thesis by A1, XXREAL_0: 6;

      end;

    end;

    

     Lm13: x >= 0 & y > 0 implies (x + y) > 0

    proof

      assume x >= 0 ;

      then (x + y) >= ( 0 + y) by Lm12;

      hence thesis by Th4;

    end;

    

     Lm14: x <= 0 & y < 0 implies (x + y) < 0

    proof

      assume x <= 0 ;

      then (x + y) <= ( 0 + y) by Lm12;

      hence thesis by Th4;

    end;

    registration

      let x,y be non negative ExtReal;

      cluster (x + y) -> non negative;

      coherence

      proof

        per cases ;

          suppose x = 0 ;

          hence (x + y) >= 0 by Th4;

        end;

          suppose x > 0 ;

          hence (x + y) >= 0 by Lm13;

        end;

      end;

    end

    registration

      let x,y be non positive ExtReal;

      cluster (x + y) -> non positive;

      coherence

      proof

        per cases ;

          suppose x = 0 ;

          hence (x + y) <= 0 by Th4;

        end;

          suppose x < 0 ;

          hence (x + y) <= 0 by Lm14;

        end;

      end;

    end

    registration

      let x be positive ExtReal;

      let y be non negative ExtReal;

      cluster (x + y) -> positive;

      coherence by Lm13;

      cluster (y + x) -> positive;

      coherence ;

    end

    registration

      let x be negative ExtReal;

      let y be non positive ExtReal;

      cluster (x + y) -> negative;

      coherence by Lm14;

      cluster (y + x) -> negative;

      coherence ;

    end

    registration

      let x be non positive ExtReal;

      cluster ( - x) -> non negative;

      coherence

      proof

        assume ( - x) < 0 ;

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

        hence contradiction by Th7;

      end;

    end

    registration

      let x be non negative ExtReal;

      cluster ( - x) -> non positive;

      coherence

      proof

        assume ( - x) > 0 ;

        then (( - x) - ( - x)) > 0 ;

        hence contradiction by Th7;

      end;

    end

    registration

      let x be positive ExtReal;

      cluster ( - x) -> negative;

      coherence

      proof

        assume ( - x) >= 0 ;

        then (( - x) - ( - x)) > 0 ;

        hence contradiction by Th7;

      end;

    end

    registration

      let x be negative ExtReal;

      cluster ( - x) -> positive;

      coherence

      proof

        assume ( - x) <= 0 ;

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

        hence contradiction by Th7;

      end;

    end

    registration

      let x be non negative ExtReal, y be non positive ExtReal;

      cluster (x - y) -> non negative;

      coherence ;

      cluster (y - x) -> non positive;

      coherence ;

    end

    registration

      let x be positive ExtReal;

      let y be non positive ExtReal;

      cluster (x - y) -> positive;

      coherence ;

      cluster (y - x) -> negative;

      coherence ;

    end

    registration

      let x be negative ExtReal;

      let y be non negative ExtReal;

      cluster (x - y) -> negative;

      coherence ;

      cluster (y - x) -> positive;

      coherence ;

    end

    

     Lm15: for x, y st x <= y holds ( - y) <= ( - x)

    proof

      let x, y;

      assume

       A1: x <= y;

      per cases ;

        case that

         A2: ( - y) in REAL and

         A3: ( - x) in REAL ;

        x in REAL by A3, Lm3;

        then

        consider a be Complex such that

         A4: x = a and

         A5: ( - x) = ( - a) by Def3;

        y in REAL by A2, Lm3;

        then

        consider b be Complex such that

         A6: y = b and

         A7: ( - y) = ( - b) by Def3;

        x in REAL & y in REAL by A2, A3, Lm3;

        then

        reconsider a, b as Real by A6, A4;

        reconsider mb = ( - b), ma = ( - a) as Element of REAL by XREAL_0:def 1;

        take mb, ma;

        thus mb = ( - y) & ma = ( - x) by A7, A5;

        thus thesis by A1, A6, A4, XREAL_1: 24;

      end;

        case not (( - y) in REAL & ( - x) in REAL );

        then not (y in REAL & x in REAL ) by Lm3;

        then x = -infty or y = +infty by A1, Def1;

        hence thesis by Def3;

      end;

    end;

    theorem :: XXREAL_3:35

    x <= y implies (x + z) <= (y + z) by Lm12;

    theorem :: XXREAL_3:36

    

     Th36: x <= y & z <= w implies (x + z) <= (y + w)

    proof

      assume that

       A1: x <= y and

       A2: z <= w;

      per cases ;

        suppose

         A3: x = +infty & z = -infty ;

        

         A4: w <> -infty implies ( +infty + w) = +infty by Def2;

        y = +infty by A1, A3, XXREAL_0: 4;

        hence thesis by A3, A4;

      end;

        suppose

         A5: x = -infty & z = +infty ;

        

         A6: y <> -infty implies ( +infty + y) = +infty by Def2;

        w = +infty by A2, A5, XXREAL_0: 4;

        hence thesis by A5, A6;

      end;

        suppose

         A7: y = +infty & w = -infty ;

        

         A8: x <> +infty implies ( -infty + x) = -infty by Def2;

        z = -infty by A2, A7, XXREAL_0: 6;

        hence thesis by A7, A8;

      end;

        suppose

         A9: y = -infty & w = +infty ;

        

         A10: z <> +infty implies ( -infty + z) = -infty by Def2;

        x = -infty by A1, A9, XXREAL_0: 6;

        hence thesis by A9, A10;

      end;

        suppose

         A11: not (x = +infty & z = -infty or x = -infty & z = +infty ) & not (y = +infty & w = -infty or y = -infty & w = +infty );

        reconsider a = (x + z), b = (y + w) as Element of ExtREAL by XXREAL_0:def 1;

        

         A12: not (a = +infty & b = -infty )

        proof

          assume that

           A13: a = +infty and

           A14: b = -infty ;

          x = +infty or z = +infty by A13, Lm8;

          hence thesis by A1, A2, A11, A14, Lm9, XXREAL_0: 4;

        end;

        

         A15: a in REAL & b in REAL implies a <= b

        proof

          assume

           A16: a in REAL & b in REAL ;

          then

           A17: z in REAL & w in REAL by A11, Th20;

          x in REAL & y in REAL by A11, A16, Th20;

          then

          consider Ox,Oy,Os,Ot be Real such that

           A18: Ox = x & Oy = y & Os = z & Ot = w and

           A19: Ox <= Oy & Os <= Ot by A1, A2, A17;

          (Ox + Os) <= (Os + Oy) & (Os + Oy) <= (Ot + Oy) by A19, XREAL_1: 6;

          hence thesis by A18, XXREAL_0: 2;

        end;

        

         A20: a = +infty & b in REAL implies a <= b

        proof

          assume that

           A21: a = +infty and b in REAL ;

          x = +infty or z = +infty by A21, Lm8;

          then y = +infty or w = +infty by A1, A2, XXREAL_0: 4;

          then b = +infty by A11, Def2;

          hence thesis by XXREAL_0: 4;

        end;

        

         A22: a in REAL & b = -infty implies a <= b

        proof

          assume that a in REAL and

           A23: b = -infty ;

          y = -infty or w = -infty by A23, Lm9;

          then x = -infty or z = -infty by A1, A2, XXREAL_0: 6;

          then a = -infty by A11, Def2;

          hence thesis by XXREAL_0: 5;

        end;

        a in REAL & b in REAL or a in REAL & b = +infty or a in REAL & b = -infty or a = +infty & b in REAL or a = +infty & b = +infty or a = +infty & b = -infty or a = -infty & b in REAL or a = -infty & b = +infty or a = -infty & b = -infty by XXREAL_0: 14;

        hence thesis by A15, A22, A20, A12, XXREAL_0: 4, XXREAL_0: 5;

      end;

    end;

    theorem :: XXREAL_3:37

    

     Th37: x <= y & z <= w implies (x - w) <= (y - z)

    proof

      assume that

       A1: x <= y and

       A2: z <= w;

      ( - w) <= ( - z) by A2, Lm15;

      hence thesis by A1, Th36;

    end;

    theorem :: XXREAL_3:38

    

     Th38: x <= y iff ( - y) <= ( - x)

    proof

      thus x <= y implies ( - y) <= ( - x) by Lm15;

      ( - y) <= ( - x) implies ( - ( - x)) <= ( - ( - y)) by Lm15;

      hence thesis;

    end;

    theorem :: XXREAL_3:39

    

     Th39: 0 <= z implies x <= (x + z)

    proof

      assume 0 <= z;

      then (x + 0 ) <= (x + z) by Th36;

      hence thesis by Th4;

    end;

    theorem :: XXREAL_3:40

    x <= y implies (y - x) >= 0

    proof

      assume x <= y;

      then ( - y) <= ( - x) by Lm15;

      then (( - y) + y) <= (y + ( - x)) by Th36;

      hence thesis by Th7;

    end;

    theorem :: XXREAL_3:41

    (z = -infty & y = +infty implies x <= 0 ) & (z = +infty & y = -infty implies x <= 0 ) implies ((x - y) <= z implies x <= (z + y))

    proof

      assume that

       A1: z = -infty & y = +infty implies x <= 0 and

       A2: z = +infty & y = -infty implies x <= 0 and

       A3: (x - y) <= z;

      per cases by XXREAL_0: 14;

        suppose

         A4: z = -infty ;

        per cases by A3, A4, Th19, XXREAL_0: 6;

          suppose x = -infty ;

          hence thesis by XXREAL_0: 5;

        end;

          suppose y = +infty ;

          hence thesis by A1, A4;

        end;

      end;

        suppose

         A5: z = +infty ;

        per cases ;

          suppose y = -infty ;

          hence thesis by A2, A5;

        end;

          suppose y <> -infty ;

          then (z + y) = +infty by A5, Def2;

          hence thesis by XXREAL_0: 3;

        end;

      end;

        suppose

         A6: z in REAL ;

        per cases by A3, A6, XXREAL_0: 13;

          suppose

           A7: (x - y) in REAL ;

          per cases by A7, Th21;

            suppose y = +infty ;

            then (z + y) = +infty by A6, Def2;

            hence thesis by XXREAL_0: 3;

          end;

            suppose x = -infty ;

            hence thesis by XXREAL_0: 5;

          end;

            suppose x in REAL & y in REAL ;

            then

            reconsider a = x, b = y, c = z as Element of REAL by A6;

            (a - b) <= c by A3;

            then a <= (b + c) by XREAL_1: 20;

            hence thesis;

          end;

        end;

          suppose

           A8: (x - y) = -infty ;

          per cases by A8, Th19;

            suppose x = -infty ;

            hence thesis by XXREAL_0: 5;

          end;

            suppose y = +infty ;

            then (z + y) = +infty by A6, Def2;

            hence thesis by XXREAL_0: 3;

          end;

        end;

      end;

    end;

    theorem :: XXREAL_3:42

    (x = +infty & y = +infty implies 0 <= z) & (x = -infty & y = -infty implies 0 <= z) implies (x <= (z + y) implies (x - y) <= z)

    proof

      assume that

       A1: x = +infty & y = +infty implies 0 <= z and

       A2: x = -infty & y = -infty implies 0 <= z and

       A3: x <= (z + y);

      per cases by XXREAL_0: 14;

        suppose

         A4: x = +infty ;

        per cases by A3, A4, Lm8, XXREAL_0: 4;

          suppose z = +infty ;

          hence thesis by XXREAL_0: 3;

        end;

          suppose y = +infty ;

          hence thesis by A1, A4, Th7;

        end;

      end;

        suppose

         A5: x = -infty ;

        per cases ;

          suppose y = -infty ;

          hence thesis by A2, A5, Th7;

        end;

          suppose ( - ( - y)) <> -infty ;

          then ( - y) <> +infty by Def3;

          then (x - y) = -infty by A5, Def2;

          hence thesis by XXREAL_0: 5;

        end;

      end;

        suppose

         A6: x in REAL ;

        per cases by A3, A6, XXREAL_0: 10;

          suppose

           A7: (z + y) in REAL ;

          per cases by A7, Th20;

            suppose y = +infty ;

            then (x - y) = -infty by A6, Def2, Th5;

            hence thesis by XXREAL_0: 5;

          end;

            suppose z = +infty ;

            hence thesis by XXREAL_0: 3;

          end;

            suppose z in REAL & y in REAL ;

            then

            reconsider a = x, b = y, c = z as Element of REAL by A6;

            a <= (b + c) by A3;

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

            hence thesis;

          end;

        end;

          suppose

           A8: (z + y) = +infty ;

          per cases by A8, Lm8;

            suppose z = +infty ;

            hence thesis by XXREAL_0: 3;

          end;

            suppose y = +infty ;

            then (x - y) = -infty by A6, Def2, Th5;

            hence thesis by XXREAL_0: 5;

          end;

        end;

      end;

    end;

    theorem :: XXREAL_3:43

    

     Th43: z in REAL & x < y implies (x + z) < (y + z) & (x - z) < (y - z)

    proof

      assume that

       A1: z in REAL and

       A2: x < y;

      

       A3: (x + z) <> (y + z)

      proof

        assume (x + z) = (y + z);

        

        then x = ((y + z) - z) by A1, Th22

        .= y by A1, Th22;

        hence thesis by A2;

      end;

      

       A4: (x - z) <> (y - z)

      proof

        assume (x - z) = (y - z);

        

        then x = ((y - z) + z) by A1, Th22

        .= y by A1, Th22;

        hence thesis by A2;

      end;

      (x + z) <= (y + z) & (x - z) <= (y - z) by A2, Th36;

      hence thesis by A3, A4, XXREAL_0: 1;

    end;

    theorem :: XXREAL_3:44

     0 <= x & 0 <= y & 0 <= z implies ((x + y) + z) = (x + (y + z))

    proof

      assume that

       A1: 0 <= x and

       A2: 0 <= y and

       A3: 0 <= z;

      per cases by A1, A2, A3, XXREAL_0: 14;

        suppose x in REAL & y in REAL & z in REAL ;

        then

        consider a,b,c,d,e be Real such that

         A4: x = a & y = b & z = c and (x + y) = d and (y + z) = e;

        ((x + y) + z) = ((a + b) + c) by A4

        .= (a + (b + c))

        .= (x + (y + z)) by A4;

        hence thesis;

      end;

        suppose

         A5: x = +infty ;

        

        then ((x + y) + z) = ( +infty + z) by A2, Def2

        .= +infty by A3, Def2

        .= ( +infty + (y + z)) by A2, A3, Def2;

        hence thesis by A5;

      end;

        suppose

         A6: y = +infty ;

        

        then ((x + y) + z) = ( +infty + z) by A1, Def2

        .= +infty by A3, Def2

        .= (x + +infty ) by A1, Def2

        .= (x + ( +infty + z)) by A3, Def2;

        hence thesis by A6;

      end;

        suppose

         A7: z = +infty ;

        

        then ((x + y) + z) = +infty by A1, A2, Def2

        .= (x + +infty ) by A1, Def2

        .= (x + (y + +infty )) by A2, Def2;

        hence thesis by A7;

      end;

    end;

    theorem :: XXREAL_3:45

    

     Th45: x is real implies ((y + x) <= z iff y <= (z - x))

    proof

      assume

       A1: x is real;

      

       A2: ((z - x) + x) = z

      proof

        per cases by XXREAL_0: 14;

          suppose z in REAL ;

          then

          reconsider a = x, b = z as Real by A1;

          

          thus ((z - x) + x) = ((b - a) + a)

          .= z;

        end;

          suppose

           A3: z = -infty ;

          

          hence ((z - x) + x) = ( -infty + x) by A1, Th14

          .= z by A1, A3, Def2;

        end;

          suppose

           A4: z = +infty ;

          

          hence ((z - x) + x) = ( +infty + x) by A1, Th13

          .= z by A1, A4, Def2;

        end;

      end;

      hereby

        

         A5: ((y + x) - x) = y

        proof

          per cases by XXREAL_0: 14;

            suppose y in REAL ;

            then

            reconsider a = x, b = y as Element of REAL by A1, XXREAL_0: 14;

            ((y + x) - x) = ((b + a) - a)

            .= y;

            hence thesis;

          end;

            suppose

             A6: y = -infty or y = +infty ;

            per cases by A6;

              suppose

               A7: y = -infty ;

              

              hence ((y + x) - x) = ( -infty - x) by A1, Def2

              .= y by A1, A7, Th14;

            end;

              suppose

               A8: y = +infty ;

              

              hence ((y + x) - x) = ( +infty - x) by A1, Def2

              .= y by A1, A8, Th13;

            end;

          end;

        end;

        assume (y + x) <= z;

        hence y <= (z - x) by A5, Th37;

      end;

      assume y <= (z - x);

      hence thesis by A2, Th36;

    end;

    theorem :: XXREAL_3:46

    

     Th46: 0 < x & x < y implies 0 < (y - x)

    proof

      assume that

       A1: 0 < x and

       A2: x < y;

      

       A3: x in REAL by A1, A2, XXREAL_0: 48;

      

       A4: 0 <> (y - x)

      proof

        assume 0 = (y - x);

        

        then x = ((y - x) + x) by Th4

        .= y by A3, Th22;

        hence thesis by A2;

      end;

      ( 0 + x) < y by A2, Th4;

      hence thesis by A3, A4, Th45;

    end;

    

     Lm16: 0 in REAL by XREAL_0:def 1;

    theorem :: XXREAL_3:47

     0 <= x & 0 <= z & (z + x) < y implies z < (y - x)

    proof

      assume that

       A1: 0 <= x and

       A2: 0 <= z and

       A3: (z + x) < y;

      x in REAL

      proof

        

         A4: x <> +infty

        proof

          assume x = +infty ;

          then +infty < y by A2, A3, Def2;

          hence thesis by XXREAL_0: 4;

        end;

        assume not x in REAL ;

        hence thesis by A1, A4, XXREAL_0: 10, Lm16;

      end;

      then z <= (y - x) & z <> (y - x) by A3, Th22, Th45;

      hence thesis by XXREAL_0: 1;

    end;

    theorem :: XXREAL_3:48

     0 <= x & 0 <= z & (z + x) < y implies z <= y

    proof

      assume that

       A1: 0 <= x and

       A2: 0 <= z and

       A3: (z + x) < y;

      x in REAL

      proof

        

         A4: x <> +infty

        proof

          assume x = +infty ;

          then +infty < y by A2, A3, Def2;

          hence thesis by XXREAL_0: 4;

        end;

        assume not x in REAL ;

        hence thesis by A1, A4, XXREAL_0: 10, Lm16;

      end;

      then

       A5: ((z + x) - x) = z by Th22;

      (y - 0 ) = y by Th15;

      hence thesis by A1, A3, A5, Th37;

    end;

    theorem :: XXREAL_3:49

    

     Th49: 0 <= x & x < z implies ex y be Real st 0 < y & (x + y) < z

    proof

      assume that

       A1: 0 <= x and

       A2: x < z;

      per cases by A1;

        suppose

         A3: 0 < x;

        then 0 < (z - x) by A2, Th46;

        then

        consider y be Real such that

         A4: 0 < y and

         A5: y < (z - x) by Th3;

        take y;

        

         A6: (x + y) <= (x + (z - x)) by A5, Th36;

        

         A7: x in REAL by A2, A3, XXREAL_0: 48;

        then

         A8: (x + (z - x)) = z by Th22;

        (x + y) <> z by A7, A5, Th22;

        hence thesis by A4, A6, A8, XXREAL_0: 1;

      end;

        suppose

         A9: 0 = x;

        consider y be Real such that

         A10: 0 < y & y < z by A1, A2, Th3;

        take y;

        thus thesis by A9, A10, Th4;

      end;

    end;

    theorem :: XXREAL_3:50

     0 < x implies ex y be Real st 0 < y & (y + y) < x

    proof

      assume 0 < x;

      then

      consider x1 be Real such that

       A1: 0 < x1 and

       A2: x1 < x by Th3;

      consider x2 be Real such that

       A3: 0 < x2 and

       A4: (x1 + x2) < x by A1, A2, Th49;

      take y = ( min (x1,x2));

      per cases ;

        suppose

         A5: x1 <= x2;

        hence 0 < y by A1, XXREAL_0:def 9;

        y = x1 by A5, XXREAL_0:def 9;

        then (y + y) <= (x1 + x2) by A5, Th36;

        hence thesis by A4, XXREAL_0: 2;

      end;

        suppose

         A6: x2 <= x1;

        hence 0 < y by A3, XXREAL_0:def 9;

        y = x2 by A6, XXREAL_0:def 9;

        then (y + y) <= (x1 + x2) by A6, Th36;

        hence thesis by A4, XXREAL_0: 2;

      end;

    end;

    theorem :: XXREAL_3:51

    

     Th51: x < y & x < +infty & -infty < y implies 0 < (y - x)

    proof

      assume that

       A1: x < y and

       A2: x < +infty and

       A3: -infty < y;

      per cases ;

        suppose y = +infty ;

        hence thesis by A2, Th13;

      end;

        suppose

         A4: y <> +infty ;

        per cases ;

          suppose x = -infty ;

          hence thesis by A3, Th14;

        end;

          suppose

           A5: x <> -infty ;

          

           A6: y in REAL by A3, A4, XXREAL_0: 14;

          x in REAL by A2, A5, XXREAL_0: 14;

          then

          reconsider a = x, b = y as Real by A6;

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

          hence thesis;

        end;

      end;

    end;

    theorem :: XXREAL_3:52

     not (x = +infty & y = -infty or x = -infty & y = +infty ) & (x + y) < z implies x <> +infty & y <> +infty & z <> -infty & x < (z - y)

    proof

      assume that

       A1: not (x = +infty & y = -infty or x = -infty & y = +infty ) and

       A2: (x + y) < z;

      per cases ;

        suppose

         A3: z = +infty ;

        then x <> +infty by A1, A2, Def2;

        then

         A4: x < +infty by XXREAL_0: 4;

        y <> +infty by A1, A2, A3, Def2;

        hence thesis by A3, A4, Th13;

      end;

        suppose

         A5: z <> +infty ;

        

         A6: -infty <= (x + y) by XXREAL_0: 5;

        then z in REAL by A2, A5, XXREAL_0: 14;

        then

        reconsider c = z as Real;

        

         A7: (x + y) < +infty by A2, XXREAL_0: 2, XXREAL_0: 4;

        then

         A8: x <> +infty by A1, Def2;

        

         A9: y <> +infty by A1, A7, Def2;

        per cases ;

          suppose

           A10: y = -infty ;

          then x < +infty by A1, XXREAL_0: 4;

          hence thesis by A2, A6, A10, Th14;

        end;

          suppose y <> -infty ;

          then y in REAL by A9, XXREAL_0: 14;

          then

          reconsider b = y as Real;

          per cases ;

            suppose

             A11: x = -infty ;

            hence x <> +infty ;

            

             A12: (z - y) = (c - b);

            hence y <> +infty ;

            thus z <> -infty by A12;

            (c - b) in REAL by XREAL_0:def 1;

            hence thesis by A11, XXREAL_0: 12;

          end;

            suppose x <> -infty ;

            then x in REAL by A8, XXREAL_0: 14;

            then

            reconsider a = x as Real;

            (x + y) = (a + b);

            then a < (c - b) by A2, XREAL_1: 20;

            hence thesis;

          end;

        end;

      end;

    end;

    theorem :: XXREAL_3:53

     not (z = +infty & y = +infty or z = -infty & y = -infty ) & x < (z - y) implies x <> +infty & y <> +infty & z <> -infty & (x + y) < z

    proof

      assume that

       A1: not (z = +infty & y = +infty or z = -infty & y = -infty ) and

       A2: x < (z - y);

      per cases ;

        suppose

         A3: x = -infty ;

        

         A4: -infty <= z by XXREAL_0: 5;

        z <> -infty by A1, A2, A3, Th14;

        then

         A5: -infty < z by A4, XXREAL_0: 1;

        y <> +infty by A1, A2, A3, Th13;

        hence thesis by A3, A5, Def2;

      end;

        suppose

         A6: x <> -infty ;

        

         A7: (z - y) <= +infty by XXREAL_0: 4;

        then x in REAL by A2, A6, XXREAL_0: 14;

        then

        reconsider a = x as Real;

        

         A8: -infty <= x by XXREAL_0: 5;

        then

         A9: z <> -infty by A1, A2, Th14;

        

         A10: y <> +infty by A1, A2, A8, Th13;

        per cases ;

          suppose

           A11: y = -infty ;

           -infty <= z by XXREAL_0: 5;

          then -infty < z by A1, A11, XXREAL_0: 1;

          hence thesis by A2, A7, A11, Def2;

        end;

          suppose y <> -infty ;

          then y in REAL by A10, XXREAL_0: 14;

          then

          reconsider b = y as Real;

          per cases ;

            suppose

             A12: z = +infty ;

            (a + b) in REAL by XREAL_0:def 1;

            hence thesis by A12, XXREAL_0: 9;

          end;

            suppose z <> +infty ;

            then z in REAL by A9, XXREAL_0: 14;

            then

            reconsider c = z as Real;

            (z - y) = (c - b);

            then (a + b) < c by A2, XREAL_1: 20;

            hence thesis;

          end;

        end;

      end;

    end;

    theorem :: XXREAL_3:54

     not (x = +infty & y = +infty or x = -infty & y = -infty ) & (x - y) < z implies x <> +infty & y <> -infty & z <> -infty & x < (z + y)

    proof

      assume that

       A1: not (x = +infty & y = +infty or x = -infty & y = -infty ) and

       A2: (x - y) < z;

      per cases ;

        suppose

         A3: z = +infty ;

        then x <> +infty by A1, A2, Th13;

        then

         A4: x < +infty by XXREAL_0: 4;

        y <> -infty by A1, A2, A3, Th14;

        hence thesis by A3, A4, Def2;

      end;

        suppose

         A5: z <> +infty ;

        

         A6: -infty <= (x - y) by XXREAL_0: 5;

        then z in REAL by A2, A5, XXREAL_0: 14;

        then

        reconsider c = z as Real;

        

         A7: (x - y) < +infty by A2, XXREAL_0: 2, XXREAL_0: 4;

        then

         A8: x <> +infty by A1, Th13;

        

         A9: y <> -infty by A1, A7, Th14;

        per cases ;

          suppose

           A10: y = +infty ;

          then x < +infty by A1, XXREAL_0: 4;

          hence thesis by A2, A6, A10, Def2;

        end;

          suppose y <> +infty ;

          then y in REAL by A9, XXREAL_0: 14;

          then

          reconsider b = y as Real;

          per cases ;

            suppose

             A11: x = -infty ;

            (c + b) in REAL by XREAL_0:def 1;

            hence thesis by A11, XXREAL_0: 12;

          end;

            suppose x <> -infty ;

            then x in REAL by A8, XXREAL_0: 14;

            then

            reconsider a = x as Real;

            (x - y) = (a - b);

            then a < (c + b) by A2, XREAL_1: 19;

            hence thesis;

          end;

        end;

      end;

    end;

    theorem :: XXREAL_3:55

     not (z = +infty & y = -infty or z = -infty & y = +infty ) & x < (z + y) implies x <> +infty & y <> -infty & z <> -infty & (x - y) < z

    proof

      assume that

       A1: not (z = +infty & y = -infty or z = -infty & y = +infty ) and

       A2: x < (z + y);

      per cases ;

        suppose

         A3: x = -infty ;

        

         A4: -infty <= z by XXREAL_0: 5;

        z <> -infty by A1, A2, A3, Def2;

        then

         A5: -infty < z by A4, XXREAL_0: 1;

        y <> -infty by A1, A2, A3, Def2;

        hence thesis by A3, A5, Th14;

      end;

        suppose

         A6: x <> -infty ;

        

         A7: (z + y) <= +infty by XXREAL_0: 4;

        then x in REAL by A2, A6, XXREAL_0: 14;

        then

        reconsider a = x as Real;

        

         A8: -infty <= x by XXREAL_0: 5;

        then

         A9: z <> -infty by A1, A2, Def2;

        

         A10: y <> -infty by A1, A2, A8, Def2;

        per cases ;

          suppose

           A11: y = +infty ;

           -infty <= z by XXREAL_0: 5;

          then -infty < z by A1, A11, XXREAL_0: 1;

          hence thesis by A2, A7, A11, Th13;

        end;

          suppose y <> +infty ;

          then y in REAL by A10, XXREAL_0: 14;

          then

          reconsider b = y as Real;

          per cases ;

            suppose

             A12: z = +infty ;

            (a - b) in REAL by XREAL_0:def 1;

            hence thesis by A12, XXREAL_0: 9;

          end;

            suppose z <> +infty ;

            then z in REAL by A9, XXREAL_0: 14;

            then

            reconsider c = z as Real;

            (z + y) = (c + b);

            then (a - b) < c by A2, XREAL_1: 19;

            hence thesis;

          end;

        end;

      end;

    end;

    theorem :: XXREAL_3:56

     not (x = +infty & y = -infty or x = -infty & y = +infty or y = +infty & z = +infty or y = -infty & z = -infty ) & (x + y) <= z implies y <> +infty & x <= (z - y)

    proof

      assume that

       A1: not (x = +infty & y = -infty or x = -infty & y = +infty or y = +infty & z = +infty or y = -infty & z = -infty ) and

       A2: (x + y) <= z;

      thus y <> +infty

      proof

        assume

         A3: y = +infty ;

        then (x + y) = +infty by A1, Def2;

        hence contradiction by A1, A2, A3, XXREAL_0: 4;

      end;

      per cases ;

        suppose z = +infty ;

        then (z - y) = +infty by A1, Th13;

        hence thesis by XXREAL_0: 4;

      end;

        suppose

         A4: z <> +infty ;

        then

         A5: (x + y) < +infty by A2, XXREAL_0: 2, XXREAL_0: 4;

        then

         A6: x <> +infty by A1, Def2;

        

         A7: y <> +infty by A1, A5, Def2;

        per cases ;

          suppose x = -infty ;

          hence thesis by XXREAL_0: 5;

        end;

          suppose x <> -infty ;

          then x in REAL by A6, XXREAL_0: 14;

          then

          reconsider a = x as Real;

          per cases ;

            suppose y = -infty ;

            then (z - y) = +infty by A1, Th14;

            hence thesis by XXREAL_0: 4;

          end;

            suppose y <> -infty ;

            then y in REAL by A7, XXREAL_0: 14;

            then

            reconsider b = y as Real;

            (a + b) in REAL by XREAL_0:def 1;

            then z <> -infty by A2, XXREAL_0: 12;

            then z in REAL by A4, XXREAL_0: 14;

            then

            reconsider c = z as Real;

            (x + y) = (a + b);

            then a <= (c - b) by A2, XREAL_1: 19;

            hence thesis;

          end;

        end;

      end;

    end;

    theorem :: XXREAL_3:57

     not (x = +infty & y = -infty ) & not (x = -infty & y = +infty ) & not (y = +infty & z = +infty ) & x <= (z - y) implies y <> +infty & (x + y) <= z

    proof

      assume that

       A1: not (x = +infty & y = -infty ) and

       A2: not (x = -infty & y = +infty ) and

       A3: not (y = +infty & z = +infty ) and

       A4: x <= (z - y);

      thus

       A5: y <> +infty

      proof

        assume

         A6: y = +infty ;

        then (z - y) = -infty by A3, Th13;

        hence contradiction by A2, A4, A6, XXREAL_0: 6;

      end;

      per cases by A5;

        suppose y = -infty ;

        then (x + y) = -infty by A1, Def2;

        hence thesis by XXREAL_0: 5;

      end;

        suppose

         A7: y <> +infty & y <> -infty ;

        ( - -infty ) = +infty by Def3;

        then

         A8: ( - y) <> -infty by A7;

        ( - +infty ) = -infty by Def3;

        then ( - y) <> +infty by A7;

        

        then ((z - y) + y) = (z + (( - y) + y)) by A7, A8, Th29

        .= (z + 0 ) by Th7

        .= z by Th4;

        hence thesis by A4, Th36;

      end;

    end;

    theorem :: XXREAL_3:58

     not (x = +infty & y = +infty or x = -infty & y = -infty or y = +infty & z = -infty or y = -infty & z = +infty ) & (x - y) <= z implies y <> -infty

    proof

      assume that

       A1: not (x = +infty & y = +infty or x = -infty & y = -infty or y = +infty & z = -infty or y = -infty & z = +infty ) and

       A2: (x - y) <= z;

      assume

       A3: y = -infty ;

      then (x - y) = +infty by A1, Th14;

      hence contradiction by A1, A2, A3, XXREAL_0: 4;

    end;

    theorem :: XXREAL_3:59

     not (x = -infty & y = -infty ) & not (y = -infty & z = +infty ) & x <= (z + y) implies y <> -infty

    proof

      assume that

       A1: not (x = -infty & y = -infty ) and

       A2: not (y = -infty & z = +infty ) and

       A3: x <= (z + y);

      assume

       A4: y = -infty ;

      then (z + y) = -infty by A2, Def2;

      hence contradiction by A1, A3, A4, XXREAL_0: 6;

    end;

    theorem :: XXREAL_3:60

    (x <= ( - y) implies y <= ( - x)) & (( - x) <= y implies ( - y) <= x)

    proof

      x <= ( - y) implies ( - ( - y)) <= ( - x) by Th38;

      hence x <= ( - y) implies y <= ( - x);

      ( - x) <= y implies ( - y) <= ( - ( - x)) by Th38;

      hence thesis;

    end;

    theorem :: XXREAL_3:61

    (for e be Real st 0 < e holds x < (y + e)) implies x <= y

    proof

      assume

       A1: for e be Real st 0 < e holds x < (y + e);

      per cases ;

        suppose

         A2: y = +infty or y = -infty ;

        per cases by A2;

          suppose y = +infty ;

          hence thesis by XXREAL_0: 4;

        end;

          suppose

           A3: y = -infty ;

          x < (y + 1) by A1;

          hence thesis by A3, Def2;

        end;

      end;

        suppose

         A4: y <> +infty & y <> -infty ;

        per cases ;

          suppose

           A5: x = +infty ;

          x < (y + 1) by A1;

          hence thesis by A5, XXREAL_0: 4;

        end;

          suppose

           A6: x <> +infty ;

          now

            assume

             A7: x <> -infty ;

            then x in REAL by A6, XXREAL_0: 14;

            then

            reconsider x1 = x as Real;

             -infty <= x by XXREAL_0: 5;

            then

             A8: -infty < x by A7, XXREAL_0: 1;

            y in REAL by A4, XXREAL_0: 14;

            then

            reconsider y1 = y as Real;

            assume

             A9: not x <= y;

            y < +infty by A4, XXREAL_0: 4;

            then 0 < (x - y) by A9, A8, Th51;

            then x < (y + (x1 - y1)) by A1;

            then x < ((y + x) - y) by Th30;

            then x < (x + (y - y)) by A4, Th30;

            then x < (x + 0 ) by Th7;

            hence contradiction by Th4;

          end;

          hence thesis by XXREAL_0: 5;

        end;

      end;

    end;

    reserve t for ExtReal;

    theorem :: XXREAL_3:62

    t <> -infty & t <> +infty & x < y implies (x + t) < (y + t)

    proof

      assume that

       A1: t <> -infty & t <> +infty and

       A2: x < y;

      

       A3: (t - t) = 0 by Th7;

       A4:

      now

        assume (x + t) = (y + t);

        then (x + (t - t)) = ((y + t) - t) by A1, Th30;

        then (x + 0 ) = (y + (t - t)) by A1, A3, Th30;

        then x = (y + 0 ) by A3, Th4;

        hence contradiction by A2, Th4;

      end;

      (x + t) <= (y + t) by A2, Th36;

      hence thesis by A4, XXREAL_0: 1;

    end;

    theorem :: XXREAL_3:63

    t <> -infty & t <> +infty & x < y implies (x - t) < (y - t)

    proof

      assume that

       A1: t <> -infty & t <> +infty and

       A2: x < y;

      

       A3: (t - t) = 0 by Th7;

       A4:

      now

        assume (x - t) = (y - t);

        then (x - (t - t)) = ((y - t) + t) by A1, Th32;

        then (x - 0 ) = (y - (t - t)) by A1, A3, Th32;

        then x = (y + 0 ) by A3, Th4;

        hence contradiction by A2, Th4;

      end;

      (x - t) <= (y - t) by A2, Th37;

      hence thesis by A4, XXREAL_0: 1;

    end;

    theorem :: XXREAL_3:64

    x < y & w < z implies (x + w) < (y + z)

    proof

      assume that

       A1: x < y and

       A2: w < z;

       -infty <= w by XXREAL_0: 5;

      per cases by XXREAL_0: 1;

        suppose

         A3: w = -infty ;

        

         A4: y <> -infty & z <> -infty by A1, A2, XXREAL_0: 5;

        x <> +infty by A1, XXREAL_0: 3;

        then (x + w) = -infty by A3, Def2;

        hence thesis by A4, Lm9, XXREAL_0: 6;

      end;

        suppose

         A5: -infty < w;

        per cases ;

          suppose

           A6: y = +infty ;

          

           A7: z <= +infty by XXREAL_0: 4;

          (y + z) = +infty by A5, A2, A6, Def2;

          hence thesis by A1, A2, A6, A7, Lm8, XXREAL_0: 4;

        end;

          suppose

           A8: y <> +infty ;

           -infty <= x by XXREAL_0: 5;

          then y in REAL by A1, A8, XXREAL_0: 14;

          then

           A9: (y + w) < (y + z) by A2, Th43;

          z <= +infty by XXREAL_0: 4;

          then w in REAL by A5, A2, XXREAL_0: 14;

          then (x + w) < (y + w) by A1, Th43;

          hence thesis by A9, XXREAL_0: 2;

        end;

      end;

    end;

    theorem :: XXREAL_3:65

     0 <= x & (z + x) <= y implies z <= y

    proof

      assume 0 <= x;

      then z <= (z + x) by Th39;

      hence thesis by XXREAL_0: 2;

    end;

    begin

    definition

      let x,y be ExtReal;

      :: XXREAL_3:def5

      func x * y -> ExtReal means

      : Def5: ex a,b be Complex st x = a & y = b & it = (a * b) if x is real & y is real,

it = +infty if ( not x is real or not y is real) & (x is positive & y is positive or x is negative & y is negative),

it = -infty if ( not x is real or not y is real) & (x is positive & y is negative or x is negative & y is positive)

      otherwise it = 0 ;

      existence

      proof

        thus x is real & y is real implies ex c be ExtReal, a,b be Complex st x = a & y = b & c = (a * b)

        proof

          assume x is real & y is real;

          then

          reconsider a = x, b = y as Real;

          take (a * b), a, b;

          thus thesis;

        end;

        thus thesis;

      end;

      uniqueness ;

      consistency ;

      commutativity ;

    end

    registration

      let x,y be Real, a,b be Complex;

      identify a * b with x * y when x = a, y = b;

      compatibility by Def5;

    end

    definition

      let x be ExtReal;

      :: XXREAL_3:def6

      func x " -> ExtReal means

      : Def6: ex a be Complex st x = a & it = (a " ) if x is real

      otherwise it = 0 ;

      existence

      proof

        thus x is real implies ex c be ExtReal, a be Complex st x = a & c = (a " )

        proof

          assume x is real;

          then

          reconsider a = x as Real;

          take (a " ), a;

          thus thesis;

        end;

        thus thesis;

      end;

      uniqueness ;

      consistency ;

    end

    registration

      let x be Real, a be Complex;

      identify a " with x " when x = a;

      compatibility by Def6;

    end

    definition

      let x,y be ExtReal;

      :: XXREAL_3:def7

      func x / y -> ExtReal equals (x * (y " ));

      coherence ;

    end

    registration

      let x,y be Real, a,b be Complex;

      identify a / b with x / y when x = a, y = b;

      compatibility

      proof

        reconsider y1 = (y " ) as Real;

        assume x = a & y = b;

        

        hence (a / b) = (x * y1)

        .= (x / y);

      end;

    end

    

     Lm17: (x * 0 ) = 0

    proof

      per cases by XXREAL_0: 14;

        suppose x in REAL ;

        then ex a,b be Complex st x = a & 0 = b & (x * 0 ) = (a * b) by Def5;

        hence thesis;

      end;

        suppose x = +infty ;

        hence thesis by Def5;

      end;

        suppose x = -infty ;

        hence thesis by Def5;

      end;

    end;

    registration

      let x be positive ExtReal, y be negative ExtReal;

      cluster (x * y) -> negative;

      coherence

      proof

        per cases ;

          suppose x in REAL & y in REAL ;

          then

          reconsider x, y as Real;

          (x * y) < 0 ;

          hence thesis;

        end;

          suppose not x in REAL or not y in REAL ;

          then not x is real or not y is real by XREAL_0:def 1;

          hence thesis by Def5;

        end;

      end;

    end

    registration

      let x,y be negative ExtReal;

      cluster (x * y) -> positive;

      coherence

      proof

        per cases ;

          suppose x in REAL & y in REAL ;

          then

          reconsider x, y as Real;

          (x * y) > 0 ;

          hence thesis;

        end;

          suppose not x in REAL or not y in REAL ;

          then not x is real or not y is real by XREAL_0:def 1;

          hence thesis by Def5;

        end;

      end;

    end

    registration

      let x,y be positive ExtReal;

      cluster (x * y) -> positive;

      coherence

      proof

        per cases ;

          suppose x in REAL & y in REAL ;

          then

          reconsider x, y as Real;

          (x * y) > 0 ;

          hence thesis;

        end;

          suppose not x in REAL or not y in REAL ;

          then not x is real or not y is real by XREAL_0:def 1;

          hence thesis by Def5;

        end;

      end;

    end

    registration

      let x be non positive ExtReal, y be non negative ExtReal;

      cluster (x * y) -> non positive;

      coherence

      proof

        per cases ;

          suppose x = 0 or y = 0 ;

          hence (x * y) <= 0 by Lm17;

        end;

          suppose x < 0 & y > 0 ;

          hence (x * y) <= 0 ;

        end;

      end;

    end

    registration

      let x,y be non positive ExtReal;

      cluster (x * y) -> non negative;

      coherence

      proof

        per cases ;

          suppose x = 0 or y = 0 ;

          hence (x * y) >= 0 by Lm17;

        end;

          suppose x < 0 & y < 0 ;

          hence (x * y) >= 0 ;

        end;

      end;

    end

    registration

      let x,y be non negative ExtReal;

      cluster (x * y) -> non negative;

      coherence

      proof

        per cases ;

          suppose x = 0 or y = 0 ;

          hence (x * y) >= 0 by Lm17;

        end;

          suppose x > 0 & y > 0 ;

          hence (x * y) >= 0 ;

        end;

      end;

    end

    registration

      let x be non positive ExtReal;

      cluster (x " ) -> non positive;

      coherence

      proof

        per cases ;

          suppose x is real;

          then

          reconsider x as Real;

          (x " ) is non positive;

          hence thesis;

        end;

          suppose not x is real;

          hence thesis by Def6;

        end;

      end;

    end

    registration

      let x be non negative ExtReal;

      cluster (x " ) -> non negative;

      coherence

      proof

        per cases ;

          suppose x is real;

          then

          reconsider x as Real;

          (x " ) is non negative;

          hence thesis;

        end;

          suppose not x is real;

          hence thesis by Def6;

        end;

      end;

    end

    registration

      let x be non negative ExtReal, y be non positive ExtReal;

      cluster (x / y) -> non positive;

      coherence ;

      cluster (y / x) -> non positive;

      coherence ;

    end

    registration

      let x,y be non negative ExtReal;

      cluster (x / y) -> non negative;

      coherence ;

    end

    registration

      let x,y be non positive ExtReal;

      cluster (x / y) -> non negative;

      coherence ;

    end

    

     Lm18: not x is real & (x * y) = 0 implies y = 0

    proof

      assume that

       A1: not x is real and

       A2: (x * y) = 0 ;

       not (x is positive & y is positive or x is negative & y is negative) by A2;

      hence thesis by A1, A2;

    end;

    registration

      let x,y be non zero ExtReal;

      cluster (x * y) -> non zero;

      coherence

      proof

        per cases ;

          suppose x is real & y is real;

          then

          reconsider r = x, s = y as Real;

          assume (x * y) is zero;

          then (r * s) = 0 ;

          hence contradiction;

        end;

          suppose not x is real or not y is real;

          then (x * y) <> 0 by Lm18;

          hence thesis;

        end;

      end;

    end

    registration

      let x be zero ExtReal, y be ExtReal;

      cluster (x * y) -> zero;

      coherence by Lm17;

    end

    

     Lm19: x = 0 implies (x * (y * z)) = ((x * y) * z)

    proof

      assume

       A1: x = 0 ;

      

      hence (x * (y * z)) = 0

      .= ((x * y) * z) by A1;

    end;

    

     Lm20: y = 0 implies (x * (y * z)) = ((x * y) * z)

    proof

      assume

       A1: y = 0 ;

      

      hence (x * (y * z)) = 0

      .= ((x * y) * z) by A1;

    end;

    

     Lm21: not y is real implies (x * (y * z)) = ((x * y) * z)

    proof

      assume not y is real;

      then

       A1: not y in REAL ;

      assume

       A2: not thesis;

      then

       A3: x <> 0 & z <> 0 by Lm19;

      per cases by A1, XXREAL_0: 14;

        suppose

         A4: y = -infty ;

        per cases by A3;

          suppose

           A5: x is positive & z is positive;

          

          then (x * ( -infty * z)) = (x * -infty ) by Def5

          .= -infty by A5, Def5

          .= ( -infty * z) by A5, Def5

          .= ((x * -infty ) * z) by A5, Def5;

          hence thesis by A2, A4;

        end;

          suppose

           A6: x is positive & z is negative;

          

          then (x * ( -infty * z)) = (x * +infty ) by Def5

          .= +infty by A6, Def5

          .= ( -infty * z) by A6, Def5

          .= ((x * -infty ) * z) by A6, Def5;

          hence thesis by A2, A4;

        end;

          suppose

           A7: x is negative & z is positive;

          

          then (x * ( -infty * z)) = (x * -infty ) by Def5

          .= +infty by A7, Def5

          .= ( +infty * z) by A7, Def5

          .= ((x * -infty ) * z) by A7, Def5;

          hence thesis by A2, A4;

        end;

          suppose

           A8: x is negative & z is negative;

          

          then (x * ( -infty * z)) = (x * +infty ) by Def5

          .= -infty by A8, Def5

          .= ( +infty * z) by A8, Def5

          .= ((x * -infty ) * z) by A8, Def5;

          hence thesis by A2, A4;

        end;

      end;

        suppose

         A9: y = +infty ;

        per cases by A3;

          suppose

           A10: x is positive & z is positive;

          

          then (x * ( +infty * z)) = (x * +infty ) by Def5

          .= +infty by A10, Def5

          .= ( +infty * z) by A10, Def5

          .= ((x * +infty ) * z) by A10, Def5;

          hence thesis by A2, A9;

        end;

          suppose

           A11: x is positive & z is negative;

          

          then (x * ( +infty * z)) = (x * -infty ) by Def5

          .= -infty by A11, Def5

          .= ( +infty * z) by A11, Def5

          .= ((x * +infty ) * z) by A11, Def5;

          hence thesis by A2, A9;

        end;

          suppose

           A12: x is negative & z is positive;

          

          then (x * ( +infty * z)) = (x * +infty ) by Def5

          .= -infty by A12, Def5

          .= ( -infty * z) by A12, Def5

          .= ((x * +infty ) * z) by A12, Def5;

          hence thesis by A2, A9;

        end;

          suppose

           A13: x is negative & z is negative;

          

          then (x * ( +infty * z)) = (x * -infty ) by Def5

          .= +infty by A13, Def5

          .= ( -infty * z) by A13, Def5

          .= ((x * +infty ) * z) by A13, Def5;

          hence thesis by A2, A9;

        end;

      end;

    end;

    

     Lm22: not x is real implies (x * (y * z)) = ((x * y) * z)

    proof

      assume not x is real;

      then

       A1: not x in REAL ;

      assume

       A2: not thesis;

      then

       A3: y <> 0 & z <> 0 by Lm19, Lm20;

      per cases by A1, XXREAL_0: 14;

        suppose

         A4: x = -infty ;

        per cases by A3;

          suppose

           A5: y is positive & z is positive;

          

          then ( -infty * (y * z)) = -infty by Def5

          .= ( -infty * z) by A5, Def5

          .= (( -infty * y) * z) by A5, Def5;

          hence thesis by A2, A4;

        end;

          suppose

           A6: y is positive & z is negative;

          

          then ( -infty * (y * z)) = +infty by Def5

          .= ( -infty * z) by A6, Def5

          .= (( -infty * y) * z) by A6, Def5;

          hence thesis by A2, A4;

        end;

          suppose

           A7: y is negative & z is positive;

          

          then ( -infty * (y * z)) = +infty by Def5

          .= ( +infty * z) by A7, Def5

          .= (( -infty * y) * z) by A7, Def5;

          hence thesis by A2, A4;

        end;

          suppose

           A8: y is negative & z is negative;

          

          then ( -infty * (y * z)) = -infty by Def5

          .= ( +infty * z) by A8, Def5

          .= (( -infty * y) * z) by A8, Def5;

          hence thesis by A2, A4;

        end;

      end;

        suppose

         A9: x = +infty ;

        per cases by A3;

          suppose

           A10: y is positive & z is positive;

          

          then ( +infty * (y * z)) = +infty by Def5

          .= ( +infty * z) by A10, Def5

          .= (( +infty * y) * z) by A10, Def5;

          hence thesis by A2, A9;

        end;

          suppose

           A11: y is positive & z is negative;

          

          then ( +infty * (y * z)) = -infty by Def5

          .= ( +infty * z) by A11, Def5

          .= (( +infty * y) * z) by A11, Def5;

          hence thesis by A2, A9;

        end;

          suppose

           A12: y is negative & z is positive;

          

          then ( +infty * (y * z)) = -infty by Def5

          .= ( -infty * z) by A12, Def5

          .= (( +infty * y) * z) by A12, Def5;

          hence thesis by A2, A9;

        end;

          suppose

           A13: y is negative & z is negative;

          

          then ( +infty * (y * z)) = +infty by Def5

          .= ( -infty * z) by A13, Def5

          .= (( +infty * y) * z) by A13, Def5;

          hence thesis by A2, A9;

        end;

      end;

    end;

    theorem :: XXREAL_3:66

    

     Th66: (x * (y * z)) = ((x * y) * z)

    proof

      per cases ;

        suppose x is real & y is real & z is real;

        then

        reconsider r = x, s = y, t = z as Real;

        reconsider rs = (r * s), sx = (s * t) as Real;

        

        thus (x * (y * z)) = (r * sx)

        .= (rs * t)

        .= ((x * y) * z);

      end;

        suppose not x is real or not z is real;

        hence thesis by Lm22;

      end;

        suppose not y is real;

        hence thesis by Lm21;

      end;

    end;

    registration

      let r be Real;

      cluster (r " ) -> real;

      coherence ;

    end

    registration

      let r,s be Real;

      cluster (r * s) -> real;

      coherence ;

      cluster (r / s) -> real;

      coherence ;

    end

    registration

      cluster ( -infty " ) -> zero;

      coherence by Def6;

      cluster ( +infty " ) -> zero;

      coherence by Def6;

    end

    theorem :: XXREAL_3:67

    ((f * g) " ) = ((f " ) * (g " ))

    proof

      per cases by XXREAL_0: 14;

        suppose f in REAL & g in REAL ;

        then

        reconsider f1 = f, g1 = g as Real;

        

         A1: (ex a be Complex st f1 = a & (f " ) = (a " )) & ex b be Complex st g1 = b & (g " ) = (b " ) by Def6;

        then ex a,b be Complex st (f " ) = a & (g " ) = b & ((f " ) * (g " )) = (a * b) by Def5;

        then ((f " ) * (g " )) = ((f1 * g1) " ) by A1, XCMPLX_1: 204;

        hence thesis;

      end;

        suppose

         A2: f = +infty ;

        g is positive or g is negative or g = 0 ;

        then ((f * g) " ) = ( +infty " ) or ((f * g) " ) = ( -infty " ) or ((f * g) " ) = ( 0 " ) by A2, Def5;

        hence thesis by A2;

      end;

        suppose

         A3: f = -infty ;

        g is positive or g is negative or g = 0 ;

        then ((f * g) " ) = ( +infty " ) or ((f * g) " ) = ( -infty " ) or ((f * g) " ) = ( 0 " ) by A3, Def5;

        hence thesis by A3;

      end;

        suppose

         A4: g = +infty ;

        f is positive or f is negative or f = 0 ;

        then ((f * g) " ) = ( +infty " ) or ((f * g) " ) = ( -infty " ) or ((f * g) " ) = ( 0 " ) by A4, Def5;

        hence thesis by A4;

      end;

        suppose

         A5: g = -infty ;

        f is positive or f is negative or f = 0 ;

        then ((f * g) " ) = ( +infty " ) or ((f * g) " ) = ( -infty " ) or ((f * g) " ) = ( 0 " ) by A5, Def5;

        hence thesis by A5;

      end;

    end;

    theorem :: XXREAL_3:68

    r <> 0 & (r * f) = (r * g) implies f = g

    proof

      assume that

       A1: r <> 0 and

       A2: (r * f) = (r * g);

      

       A3: r is positive or r is negative by A1;

      per cases by XXREAL_0: 14;

        suppose

         A4: f in REAL ;

        now

          assume not g in REAL ;

          then g = +infty or g = -infty by XXREAL_0: 14;

          hence contradiction by A2, A3, A4, Def5;

        end;

        then

         A5: ex c,d be Complex st r = c & g = d & (r * g) = (c * d) by Def5;

        ex a,b be Complex st r = a & f = b & (r * f) = (a * b) by A4, Def5;

        hence thesis by A1, A2, A5, XCMPLX_1: 5;

      end;

        suppose

         A6: f = +infty ;

        assume f <> g;

        then g in REAL or g = -infty by A6, XXREAL_0: 14;

        hence thesis by A2, A3, A6, Def5;

      end;

        suppose

         A7: f = -infty ;

        assume f <> g;

        then g in REAL or g = +infty by A7, XXREAL_0: 14;

        hence thesis by A2, A3, A7, Def5;

      end;

    end;

    theorem :: XXREAL_3:69

    

     Th69: x <> +infty & x <> -infty & (x * y) = +infty implies y = +infty or y = -infty

    proof

      assume that

       A1: x <> +infty & x <> -infty and

       A2: (x * y) = +infty ;

      assume y <> +infty & y <> -infty ;

      then

       A3: y in REAL by XXREAL_0: 14;

      x in REAL by A1, XXREAL_0: 14;

      then

      reconsider a = x, b = y as Real by A3;

      (x * y) = (a * b);

      hence contradiction by A2;

    end;

    theorem :: XXREAL_3:70

    

     Th70: x <> +infty & x <> -infty & (x * y) = -infty implies y = +infty or y = -infty

    proof

      assume that

       A1: x <> +infty & x <> -infty and

       A2: (x * y) = -infty ;

      assume y <> +infty & y <> -infty ;

      then

       A3: y in REAL by XXREAL_0: 14;

      x in REAL by A1, XXREAL_0: 14;

      then

      reconsider a = x, b = y as Real by A3;

      (x * y) = (a * b);

      hence contradiction by A2;

    end;

    

     Lm23: (x * y) in REAL implies x in REAL & y in REAL or (x * y) = 0

    proof

      assume

       A1: (x * y) in REAL ;

      assume not x in REAL or not y in REAL ;

      then

       A2: not x is real or not y is real by XREAL_0:def 1;

      assume

       A3: (x * y) <> 0 ;

      per cases by A3;

        suppose x is positive & y is positive or x is negative & y is negative;

        hence contradiction by A1, A2, Def5;

      end;

        suppose x is positive & y is negative or x is negative & y is positive;

        hence contradiction by A1, A2, Def5;

      end;

    end;

    theorem :: XXREAL_3:71

    

     Th71: x <= y & 0 <= z implies (x * z) <= (y * z)

    proof

      assume that

       A1: x <= y and

       A2: 0 <= z;

      per cases by A2;

        suppose z = 0 ;

        hence thesis;

      end;

        suppose

         A3: z > 0 ;

        per cases ;

          suppose

           A4: x = 0 ;

          then (z * y) >= 0 by A1, A2;

          hence thesis by A4;

        end;

          suppose

           A5: x <> 0 ;

          per cases ;

            case that

             A6: (x * z) in REAL & (y * z) in REAL ;

            (y * z) = 0 implies y = 0 by A3;

            then

            reconsider x, y, z as Element of REAL by A3, A5, A6, Lm23;

            reconsider p = (x * z), q = (y * z) as Element of REAL by XREAL_0:def 1;

            take p, q;

            thus thesis by A1, A2, XREAL_1: 64;

          end;

            case

             A7: not (x * z) in REAL or not (y * z) in REAL ;

            per cases by A7;

              suppose

               A8: not (x * z) in REAL ;

              per cases by A8, XXREAL_0: 14;

                suppose (x * z) = -infty ;

                hence thesis;

              end;

                suppose (x * z) = +infty ;

                then

                 A9: x <> -infty by A3;

                

                 A10: not x in REAL or not y in REAL or not z in REAL by A8, XREAL_0:def 1;

                per cases by A9, A10, XXREAL_0: 14;

                  suppose y = +infty ;

                  hence thesis by A3, Def5;

                end;

                  suppose x = +infty ;

                  then y = +infty by A1, XXREAL_0: 4;

                  hence thesis by A3, Def5;

                end;

                  suppose y = -infty ;

                  then x = -infty by A1, XXREAL_0: 6;

                  hence thesis by A3, Def5;

                end;

                  suppose that

                   A11: not z in REAL and x in REAL & y in REAL ;

                  

                   A12: z = +infty by A3, A11, XXREAL_0: 14;

                  per cases by A5;

                    suppose x < 0 ;

                    hence thesis by A12, Def5;

                  end;

                    suppose 0 < x;

                    then 0 < y by A1;

                    hence thesis by A12, Def5;

                  end;

                end;

              end;

            end;

              suppose not (y * z) in REAL ;

              then

               A13: not x in REAL or not y in REAL or not z in REAL by XREAL_0:def 1;

              per cases by A13, XXREAL_0: 14;

                suppose x = -infty ;

                hence thesis by A3, Def5;

              end;

                suppose y = +infty ;

                hence thesis by A3, Def5;

              end;

                suppose x = +infty ;

                then y = +infty by A1, XXREAL_0: 4;

                hence thesis by A3, Def5;

              end;

                suppose y = -infty ;

                then x = -infty by A1, XXREAL_0: 6;

                hence thesis by A3, Def5;

              end;

                suppose that

                 A14: not z in REAL and x in REAL & y in REAL ;

                

                 A15: z = +infty by A3, A14, XXREAL_0: 14;

                per cases by A5;

                  suppose x < 0 ;

                  hence thesis by A15, Def5;

                end;

                  suppose 0 < x;

                  then 0 < y by A1;

                  hence thesis by A15, Def5;

                end;

              end;

            end;

          end;

        end;

      end;

    end;

    theorem :: XXREAL_3:72

    

     Th72: x < y & 0 < z & z <> +infty implies (x * z) < (y * z)

    proof

      assume that

       A1: x < y and

       A2: 0 < z and

       A3: z <> +infty ;

       A4:

      now

        

         A5: x <> +infty & y <> -infty by A1, XXREAL_0: 3, XXREAL_0: 5;

        assume

         A6: (x * z) = (y * z);

        per cases by A5, XXREAL_0: 14;

          suppose

           A7: x in REAL & y in REAL ;

          z in REAL by A2, A3, XXREAL_0: 14;

          then

          reconsider x, y, z as Real by A7;

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

          hence contradiction by A6;

        end;

          suppose

           A8: y = +infty ;

          then (y * z) = +infty by A2, Def5;

          then x = +infty or x = -infty by A2, A3, A6, Th69;

          hence contradiction by A1, A2, A6, A8;

        end;

          suppose

           A9: x = -infty ;

          then (x * z) = -infty by A2, Def5;

          then y = +infty or y = -infty by A2, A3, A6, Th70;

          hence contradiction by A1, A2, A6, A9;

        end;

      end;

      (x * z) <= (y * z) by A1, A2, Th71;

      hence thesis by A4, XXREAL_0: 1;

    end;

    theorem :: XXREAL_3:73

    (x * y) in REAL implies x in REAL & y in REAL or (x * y) = 0 by Lm23;

    theorem :: XXREAL_3:74

    ( +infty " ) = 0 ;

    theorem :: XXREAL_3:75

    ( -infty " ) = 0 ;

    theorem :: XXREAL_3:76

    (x / +infty ) = 0 ;

    theorem :: XXREAL_3:77

    (x / -infty ) = 0 ;

    theorem :: XXREAL_3:78

    

     Th78: x <> -infty & x <> +infty & x <> 0 implies (x / x) = 1

    proof

      assume x <> -infty & x <> +infty ;

      then x in REAL by XXREAL_0: 14;

      then

      reconsider a = x as Real;

      assume x <> 0 ;

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

      hence thesis;

    end;

    theorem :: XXREAL_3:79

    x <= y & 0 < z implies (x / z) <= (y / z) by Th71;

    theorem :: XXREAL_3:80

    x < y & 0 < z & z <> +infty implies (x / z) < (y / z)

    proof

      assume that

       A1: x < y and

       A2: 0 < z and

       A3: z <> +infty ;

      per cases by A3, XXREAL_0: 14;

        suppose z = -infty ;

        hence thesis by A2;

      end;

        suppose z in REAL ;

        then

        reconsider z as Real;

        (z " ) > 0 by A2;

        hence thesis by A1, Th72;

      end;

    end;

    theorem :: XXREAL_3:81

    

     Th81: (1 * x) = x

    proof

      per cases by XXREAL_0: 14;

        suppose x in REAL ;

        then

        reconsider x, y = 1 as Real;

        (y * x) = x;

        hence thesis;

      end;

        suppose x = -infty or x = +infty ;

        hence thesis by Def5;

      end;

    end;

    theorem :: XXREAL_3:82

    

     Th82: (y " ) = 0 implies y = +infty or y = -infty or y = 0

    proof

      assume

       A1: (y " ) = 0 ;

      assume y <> +infty & y <> -infty ;

      then y in REAL by XXREAL_0: 14;

      then

      reconsider y as Real;

      ((y " ) " ) = 0 by A1;

      hence thesis;

    end;

    theorem :: XXREAL_3:83

    

     Th83: 0 < y & y <> +infty implies ( +infty / y) = +infty

    proof

      assume that

       A1: 0 < y and

       A2: y <> +infty ;

      (y " ) <> 0 by A1, A2, Th82;

      hence thesis by A1, Def5;

    end;

    theorem :: XXREAL_3:84

    

     Th84: y < 0 & -infty <> y implies ( -infty / y) = +infty

    proof

      assume that

       A1: y < 0 and

       A2: -infty <> y;

      (y " ) <> 0 by A1, A2, Th82;

      hence thesis by A1, Def5;

    end;

    theorem :: XXREAL_3:85

    

     Th85: y < 0 & -infty <> y implies ( +infty / y) = -infty

    proof

      assume that

       A1: y < 0 and

       A2: -infty <> y;

      (y " ) <> 0 by A1, A2, Th82;

      hence thesis by A1, Def5;

    end;

    theorem :: XXREAL_3:86

    

     Th86: 0 < y & y <> +infty implies ( -infty / y) = -infty

    proof

      assume that

       A1: 0 < y and

       A2: y <> +infty ;

      (y " ) <> 0 by A1, A2, Th82;

      hence thesis by A1, Def5;

    end;

    theorem :: XXREAL_3:87

    x <> +infty & x <> -infty & x <> 0 implies (x * (1 / x)) = 1 & ((1 / x) * x) = 1

    proof

      assume that

       A1: x <> +infty & x <> -infty and

       A2: x <> 0 ;

      x in REAL by A1, XXREAL_0: 14;

      then

      reconsider a = x as Real;

      (x * (1 / x)) = (a * (1 / a))

      .= 1 by A2, XCMPLX_1: 106;

      hence thesis;

    end;

    theorem :: XXREAL_3:88

     -infty <> y & y <> +infty & y <> 0 implies ((x * y) / y) = x & (x * (y / y)) = x

    proof

      assume that

       A1: -infty <> y and

       A2: y <> +infty and

       A3: y <> 0 ;

      reconsider b = y as Element of REAL by A1, A2, XXREAL_0: 14;

      

       A4: ((x * y) / y) = x

      proof

        per cases ;

          suppose

           A5: x = +infty ;

          per cases by A3;

            suppose

             A6: 0 < y;

            then (x * y) = +infty by A5, Def5;

            hence thesis by A2, A5, A6, Th83;

          end;

            suppose

             A7: y < 0 ;

            then (x * y) = -infty by A5, Def5;

            hence thesis by A1, A5, A7, Th84;

          end;

        end;

          suppose

           A8: x = -infty ;

          per cases by A3;

            suppose

             A9: 0 < y;

            then (x * y) = -infty by A8, Def5;

            hence thesis by A2, A8, A9, Th86;

          end;

            suppose

             A10: y < 0 ;

            then (x * y) = +infty by A8, Def5;

            hence thesis by A1, A8, A10, Th85;

          end;

        end;

          suppose x <> +infty & x <> -infty ;

          then x in REAL by XXREAL_0: 14;

          then

          reconsider a = x as Real;

          ((x * y) / y) = ((a * b) / b)

          .= a by A3, XCMPLX_1: 89;

          hence thesis;

        end;

      end;

      (y / y) = 1 by A1, A2, A3, Th78;

      hence thesis by A4, Th81;

    end;

    theorem :: XXREAL_3:89

    ( +infty * y) <> 1 & ( -infty * y) <> 1

    proof

      y = 0 or 0 < y or y < 0 ;

      hence thesis by Def5;

    end;

    theorem :: XXREAL_3:90

    (x * y) <> +infty & (x * y) <> -infty implies x in REAL or y in REAL

    proof

      assume that

       A1: (x * y) <> +infty and

       A2: (x * y) <> -infty ;

      assume

       A3: ( not x in REAL ) & not y in REAL ;

      per cases by A3, XXREAL_0: 14;

        suppose x = +infty & y = +infty ;

        hence contradiction by A1, Def5;

      end;

        suppose x = +infty & y = -infty ;

        hence contradiction by A2, Def5;

      end;

        suppose x = -infty & y = +infty ;

        hence contradiction by A2, Def5;

      end;

        suppose x = -infty & y = -infty ;

        hence contradiction by A1, Def5;

      end;

    end;

    begin

    theorem :: XXREAL_3:91

    

     Th91: (( - 1) * x) = ( - x)

    proof

      per cases by XXREAL_0: 14;

        suppose x in REAL ;

        then

        reconsider x, y = ( - 1) as Real;

        (y * x) = ( - x);

        hence thesis;

      end;

        suppose

         A1: x = -infty ;

        

        hence (( - 1) * x) = +infty by Def5

        .= ( - x) by A1, Def3;

      end;

        suppose

         A2: x = +infty ;

        

        hence (( - 1) * x) = -infty by Def5

        .= ( - x) by A2, Def3;

      end;

    end;

    theorem :: XXREAL_3:92

    

     Th92: ( - (x * y)) = (( - x) * y)

    proof

      

      thus ( - (x * y)) = (( - 1) * (x * y)) by Th91

      .= ((( - 1) * x) * y) by Th66

      .= (( - x) * y) by Th91;

    end;

    theorem :: XXREAL_3:93

    

     Th93: y = ( - z) implies (x * (y + z)) = ((x * y) + (x * z))

    proof

      assume

       A1: y = ( - z);

      

      hence (x * (y + z)) = (x * 0 ) by Th7

      .= ((x * y) - (x * y)) by Th7

      .= ((x * y) + (x * ( - y))) by Th92

      .= ((x * y) + (x * z)) by A1;

    end;

    theorem :: XXREAL_3:94

    

     Th94: (2 * x) = (x + x)

    proof

      per cases by XXREAL_0: 14;

        suppose x in REAL ;

        then

        reconsider x as Real;

        (2 * x) = (x + x);

        hence thesis;

      end;

        suppose

         A1: x = -infty ;

        

        hence (2 * x) = -infty by Def5

        .= (x + x) by A1, Def2;

      end;

        suppose

         A2: x = +infty ;

        

        hence (2 * x) = +infty by Def5

        .= (x + x) by A2, Def2;

      end;

    end;

    

     Lm24: (x * (y + y)) = ((x * y) + (x * y))

    proof

      

      thus (x * (y + y)) = (x * (2 * y)) by Th94

      .= (2 * (x * y)) by Th66

      .= ((x * y) + (x * y)) by Th94;

    end;

    

     Lm25: (x * ( 0 + z)) = ((x * 0 ) + (x * z))

    proof

      

      thus (x * ( 0 + z)) = (x * z) by Th4

      .= ((x * 0 ) + (x * z)) by Th4;

    end;

    

     Lm26: ( 0 * (y + z)) = (( 0 * y) + ( 0 * z));

    

     Lm27: x is real & y is real implies (x * (y + z)) = ((x * y) + (x * z))

    proof

      assume that

       A1: x is real and

       A2: y is real;

      reconsider r = x, s = y as Real by A1, A2;

      

       A3: (x * y) = (r * s);

      per cases by XXREAL_0: 14;

        suppose z in REAL ;

        then

        reconsider t = z as Real;

        reconsider u = (s + t), v = (r * s), w = (r * t) as Real;

        (r * u) = (v + w);

        hence thesis;

      end;

        suppose

         A4: z = -infty ;

        then

         A5: (y + z) = -infty by A2, Def2;

        per cases ;

          suppose x is zero;

          then x = 0 ;

          hence thesis by Lm26;

        end;

          suppose

           A6: x is positive;

          

          hence (x * (y + z)) = -infty by A5, Def5

          .= ((x * y) + -infty ) by A3, Def2

          .= ((x * y) + (x * z)) by A4, A6, Def5;

        end;

          suppose

           A7: x is negative;

          

          hence (x * (y + z)) = +infty by A5, Def5

          .= ((x * y) + +infty ) by A3, Def2

          .= ((x * y) + (x * z)) by A4, A7, Def5;

        end;

      end;

        suppose

         A8: z = +infty ;

        then

         A9: (y + z) = +infty by A2, Def2;

        per cases ;

          suppose x is zero;

          then x = 0 ;

          hence thesis by Lm26;

        end;

          suppose

           A10: x is positive;

          

          hence (x * (y + z)) = +infty by A9, Def5

          .= ((x * y) + +infty ) by A3, Def2

          .= ((x * y) + (x * z)) by A8, A10, Def5;

        end;

          suppose

           A11: x is negative;

          

          hence (x * (y + z)) = -infty by A9, Def5

          .= ((x * y) + -infty ) by A3, Def2

          .= ((x * y) + (x * z)) by A8, A11, Def5;

        end;

      end;

    end;

    

     Lm28: x is real & not y is real implies (x * (y + z)) = ((x * y) + (x * z))

    proof

      assume that

       A1: x is real and

       A2: not y is real;

      per cases ;

        suppose z is real;

        hence thesis by A1, Lm27;

      end;

        suppose not z is real;

        then

         A3: not z in REAL ;

        

         A4: not y in REAL by A2;

        per cases by A4, A3, XXREAL_0: 14;

          suppose y = -infty & z = -infty ;

          hence thesis by Lm24;

        end;

          suppose y = -infty & z = +infty ;

          hence thesis by Th5, Th93;

        end;

          suppose y = +infty & z = -infty ;

          hence thesis by Th6, Th93;

        end;

          suppose y = +infty & z = +infty ;

          hence thesis by Lm24;

        end;

      end;

    end;

    theorem :: XXREAL_3:95

    

     Th95: x is real implies (x * (y + z)) = ((x * y) + (x * z))

    proof

      assume

       A1: x is real;

      per cases ;

        suppose y is real & z is real;

        hence thesis by A1, Lm27;

      end;

        suppose not y is real or not z is real;

        hence thesis by A1, Lm28;

      end;

    end;

    theorem :: XXREAL_3:96

    

     Th96: y >= 0 & z >= 0 implies (x * (y + z)) = ((x * y) + (x * z))

    proof

      assume

       A1: y >= 0 & z >= 0 ;

      per cases by A1;

        suppose y = 0 or z = 0 ;

        hence thesis by Lm25;

      end;

        suppose

         A2: y > 0 & z > 0 ;

        per cases ;

          suppose x is real;

          hence thesis by Th95;

        end;

          suppose not x is real;

          then

           A3: not x in REAL ;

          per cases by A3, XXREAL_0: 14;

            suppose

             A4: x = -infty ;

            

            hence (x * (y + z)) = -infty by A2, Def5

            .= ( -infty + (x * z)) by A2, A4, Def2

            .= ((x * y) + (x * z)) by A2, A4, Def5;

          end;

            suppose

             A5: x = +infty ;

            

            hence (x * (y + z)) = +infty by A2, Def5

            .= ( +infty + (x * z)) by A2, A5, Def2

            .= ((x * y) + (x * z)) by A2, A5, Def5;

          end;

        end;

      end;

    end;

    theorem :: XXREAL_3:97

    y <= 0 & z <= 0 implies (x * (y + z)) = ((x * y) + (x * z))

    proof

      assume

       A1: y <= 0 & z <= 0 ;

      

      thus (x * (y + z)) = ( - ( - (x * (y + z))))

      .= ( - (x * ( - (y + z)))) by Th92

      .= ( - (x * (( - y) + ( - z)))) by Th9

      .= ( - ((x * ( - y)) + (x * ( - z)))) by A1, Th96

      .= ( - (( - (x * y)) + (x * ( - z)))) by Th92

      .= ( - (( - (x * y)) + ( - (x * z)))) by Th92

      .= ( - ( - ((x * y) + (x * z)))) by Th9

      .= ((x * y) + (x * z));

    end;

    theorem :: XXREAL_3:98

    (x * ( 0 + z)) = ((x * 0 ) + (x * z)) by Lm25;

    theorem :: XXREAL_3:99

    (( - f) " ) = ( - (f " ))

    proof

      per cases by XXREAL_0: 14;

        suppose

         A1: f in REAL ;

        then

        reconsider g = f as Real;

        

         A2: ( - f) = ( - g);

        consider a be Complex such that

         A3: f = a and

         A4: (f " ) = (a " ) by A1, Def6;

        

         A5: (( - a) " ) = ( - (a " )) by XCMPLX_1: 222;

        ex m be Complex st ( - f) = m & ( - (f " )) = (m " )

        proof

          take ( - a);

          thus ( - f) = ( - a) by A3, A2;

          thus thesis by A4, A5, A2, Def3;

        end;

        hence thesis by A2, Def6;

      end;

        suppose

         A6: f = +infty ;

        

        hence (( - f) " ) = ( -infty " ) by Def3

        .= ( - (f " )) by A6;

      end;

        suppose

         A7: f = -infty ;

        

        hence (( - f) " ) = ( +infty " ) by Def3

        .= ( - (f " )) by A7;

      end;

    end;

    theorem :: XXREAL_3:100

    x is real implies (x * (y - z)) = ((x * y) - (x * z))

    proof

      assume x is real;

      

      then (x * (y - z)) = ((x * y) + (x * ( - z))) by Th95

      .= ((x * y) + ( - (x * z))) by Th92;

      hence thesis;

    end;

    theorem :: XXREAL_3:101

    

     Th101: x <= y & z <= 0 implies (y * z) <= (x * z)

    proof

      assume x <= y & z <= 0 ;

      then

       A1: (x * ( - z)) <= (y * ( - z)) by Th71;

      ( - (x * z)) = (x * ( - z)) & ( - (y * z)) = (y * ( - z)) by Th92;

      hence thesis by A1, Th38;

    end;

    theorem :: XXREAL_3:102

    

     Th102: x < y & z < 0 & z <> -infty implies (y * z) < (x * z)

    proof

      assume x < y & z < 0 & z <> -infty ;

      then

       A1: (x * ( - z)) < (y * ( - z)) by Th5, Th10, Th72;

      ( - (x * z)) = (x * ( - z)) & ( - (y * z)) = (y * ( - z)) by Th92;

      hence thesis by A1, Th38;

    end;

    theorem :: XXREAL_3:103

    x <= y & z < 0 implies (y / z) <= (x / z) by Th101;

    theorem :: XXREAL_3:104

    x < y & z < 0 & z <> -infty implies (y / z) < (x / z)

    proof

      assume that

       A1: x < y and

       A2: 0 > z and

       A3: z <> -infty ;

      per cases by A3, XXREAL_0: 14;

        suppose z = +infty ;

        hence thesis by A2;

      end;

        suppose z in REAL ;

        then

        reconsider z as Real;

        (z " ) < 0 by A2;

        hence thesis by A1, Th102;

      end;

    end;

    theorem :: XXREAL_3:105

    ((x / 2) + (x / 2)) = x

    proof

      ((x / 2) + (x / 2)) = ((x + x) / 2) by Th95

      .= ((2 * x) / 2) by Th94

      .= (x * (2 / 2)) by Th66

      .= x by Th81;

      hence thesis;

    end;

    registration

      let x,y be Nat;

      cluster (x + y) -> natural;

      coherence ;

      cluster (x * y) -> natural;

      coherence ;

    end

    registration

      cluster ( - 1) -> dim-like;

      coherence ;

      let n be dim-like number;

      cluster (n + 1) -> natural;

      coherence ;

    end