xreal_0.miz



    begin

    definition

      let r be object;

      :: XREAL_0:def1

      attr r is real means

      : Def1: r in REAL ;

    end

    registration

      cluster -> real for Element of REAL ;

      coherence ;

    end

    registration

      cluster -infty -> non real;

      coherence

      proof

         { 0 , REAL } in { { 0 , REAL }, { 0 }} & REAL in { 0 , REAL } by TARSKI:def 2;

        hence thesis by XREGULAR: 7;

      end;

      cluster +infty -> non real;

      coherence

      proof

         not REAL in REAL ;

        hence thesis;

      end;

    end

    registration

      cluster natural -> real for object;

      coherence by NUMBERS: 19;

      cluster real -> complex for object;

      coherence ;

    end

    registration

      cluster real for object;

      existence

      proof

        take 0 ;

        thus 0 in REAL by NUMBERS: 19;

      end;

      cluster real for number;

      existence

      proof

        take 0 ;

        thus 0 in REAL by NUMBERS: 19;

      end;

      cluster real -> ext-real for object;

      coherence

      proof

        let n be object;

        assume n in REAL ;

        hence n in ExtREAL by XBOOLE_0:def 3;

      end;

    end

    definition

      mode Real is real Number;

    end

    

     Lm1: for x be Real, x1,x2 be Element of REAL st x = [*x1, x2*] holds x2 = 0 & x = x1

    proof

      let x be Real, x1,x2 be Element of REAL ;

      assume

       A1: x = [*x1, x2*];

      

       A2: x in REAL by Def1;

      now

        assume x2 <> 0 ;

        then x = (( 0 ,1) --> (x1,x2)) by A1, ARYTM_0:def 5;

        hence contradiction by A2, ARYTM_0: 8;

      end;

      hence thesis by A1, ARYTM_0:def 5;

    end;

    registration

      let x be Real;

      cluster ( - x) -> real;

      coherence

      proof

        (x + ( - x)) = 0 ;

        then

        consider x1,x2,y1,y2 be Element of REAL such that

         A1: x = [*x1, x2*] and

         A2: ( - x) = [*y1, y2*] and

         A3: 0 = [*( + (x1,y1)), ( + (x2,y2))*] by XCMPLX_0:def 4;

        ( + (x2,y2)) = 0 & x2 = 0 by A1, A3, Lm1;

        then y2 = 0 by ARYTM_0: 11;

        hence thesis by A2, ARYTM_0:def 5;

      end;

      cluster (x " ) -> real;

      coherence

      proof

        per cases ;

          suppose x = 0 ;

          hence thesis by XCMPLX_0:def 7;

        end;

          suppose

           A4: x <> 0 ;

          then (x * (x " )) = 1 by XCMPLX_0:def 7;

          then

          consider x1,x2,y1,y2 be Element of REAL such that

           A5: x = [*x1, x2*] and

           A6: (x " ) = [*y1, y2*] and

           A7: 1 = [*( + (( * (x1,y1)),( opp ( * (x2,y2))))), ( + (( * (x1,y2)),( * (x2,y1))))*] by XCMPLX_0:def 5;

          ( + (( * (x1,y2)),( * (x2,y1)))) = 0 & x2 = 0 by A5, A7, Lm1;

          then 0 = ( * (x1,y2)) by ARYTM_0: 11, ARYTM_0: 12;

          then x1 = 0 or y2 = 0 by ARYTM_0: 21;

          hence thesis by A4, A5, A6, Lm1, ARYTM_0:def 5;

        end;

      end;

      let y be Real;

      cluster (x + y) -> real;

      coherence

      proof

        consider x1,x2,y1,y2 be Element of REAL such that

         A8: x = [*x1, x2*] & y = [*y1, y2*] and

         A9: (x + y) = [*( + (x1,y1)), ( + (x2,y2))*] by XCMPLX_0:def 4;

        x2 = 0 & y2 = 0 by A8, Lm1;

        then ( + (x2,y2)) = 0 by ARYTM_0: 11;

        hence thesis by A9, ARYTM_0:def 5;

      end;

      cluster (x * y) -> real;

      coherence

      proof

        consider x1,x2,y1,y2 be Element of REAL such that

         A10: x = [*x1, x2*] and

         A11: y = [*y1, y2*] and

         A12: (x * y) = [*( + (( * (x1,y1)),( opp ( * (x2,y2))))), ( + (( * (x1,y2)),( * (x2,y1))))*] by XCMPLX_0:def 5;

        reconsider zz = 0 as Element of REAL by NUMBERS: 19;

        x2 = 0 by A10, Lm1;

        then

         A13: ( * (x2,y1)) = 0 by ARYTM_0: 12;

        

         A14: y2 = 0 by A11, Lm1;

        then ( * (( opp x2),y2)) = 0 by ARYTM_0: 12;

        then

         A15: ( opp ( * (x2,y2))) = 0 by ARYTM_0: 15;

        ( * (x1,y2)) = 0 by A14, ARYTM_0: 12;

        then ( + (( * (x1,y2)),( * (x2,y1)))) = 0 by A13, ARYTM_0: 11;

        

        then (x * y) = ( + (( * (x1,y1)),zz)) by A12, A15, ARYTM_0:def 5

        .= ( * (x1,y1)) by ARYTM_0: 11;

        hence thesis;

      end;

    end

    registration

      let x,y be Real;

      cluster (x - y) -> real;

      coherence ;

      cluster (x / y) -> real;

      coherence ;

    end

    begin

    reserve r,s,t for Real;

    

     Lm2: (r in REAL+ & s in REAL+ & ex x9,y9 be Element of REAL+ st r = x9 & s = y9 & x9 <=' y9) or (r in [: { 0 }, REAL+ :] & s in [: { 0 }, REAL+ :] & ex x9,y9 be Element of REAL+ st r = [ 0 , x9] & s = [ 0 , y9] & y9 <=' x9) or s in REAL+ & r in [: { 0 }, REAL+ :] implies r <= s

    proof

      assume

       A1: (r in REAL+ & s in REAL+ & ex x9,y9 be Element of REAL+ st r = x9 & s = y9 & x9 <=' y9) or (r in [: { 0 }, REAL+ :] & s in [: { 0 }, REAL+ :] & ex x9,y9 be Element of REAL+ st r = [ 0 , x9] & s = [ 0 , y9] & y9 <=' x9) or s in REAL+ & r in [: { 0 }, REAL+ :];

      per cases ;

        case r in REAL+ & s in REAL+ ;

        hence thesis by A1, ARYTM_0: 5, XBOOLE_0: 3;

      end;

        case r in [: { 0 }, REAL+ :] & s in [: { 0 }, REAL+ :];

        hence thesis by A1, ARYTM_0: 5, XBOOLE_0: 3;

      end;

        case not (r in REAL+ & s in REAL+ ) & not (r in [: { 0 }, REAL+ :] & s in [: { 0 }, REAL+ :]);

        hence thesis by A1;

      end;

    end;

    

     Lm3: {} in { {} } by TARSKI:def 1;

    

     Lm4: r <= s & s <= r implies r = s

    proof

      assume that

       A1: r <= s and

       A2: s <= r;

      

       A3: r in REAL & s in REAL by Def1;

      per cases by A3, NUMBERS:def 1, XBOOLE_0:def 3;

        suppose r in REAL+ & s in REAL+ ;

        then (ex r9,s9 be Element of REAL+ st r = r9 & s = s9 & r9 <=' s9) & ex s99,r99 be Element of REAL+ st s = s99 & r = r99 & s99 <=' r99 by A1, A2, XXREAL_0:def 5;

        hence thesis by ARYTM_1: 4;

      end;

        suppose

         A4: r in REAL+ & s in [: { 0 }, REAL+ :];

        then ( not (r in REAL+ & s in REAL+ )) & not (r in [: { 0 }, REAL+ :] & s in [: { 0 }, REAL+ :]) by ARYTM_0: 5, XBOOLE_0: 3;

        hence thesis by A1, A4, XXREAL_0:def 5;

      end;

        suppose

         A5: s in REAL+ & r in [: { 0 }, REAL+ :];

        then ( not (r in REAL+ & s in REAL+ )) & not (r in [: { 0 }, REAL+ :] & s in [: { 0 }, REAL+ :]) by ARYTM_0: 5, XBOOLE_0: 3;

        hence thesis by A2, A5, XXREAL_0:def 5;

      end;

        suppose that

         A6: r in [: { 0 }, REAL+ :] & s in [: { 0 }, REAL+ :];

        consider r9,s9 be Element of REAL+ such that

         A7: r = [ 0 , r9] & s = [ 0 , s9] and

         A8: s9 <=' r9 by A1, A6, XXREAL_0:def 5;

        consider s99,r99 be Element of REAL+ such that

         A9: s = [ 0 , s99] & r = [ 0 , r99] and

         A10: r99 <=' s99 by A2, A6, XXREAL_0:def 5;

        r9 = r99 & s9 = s99 by A7, A9, XTUPLE_0: 1;

        hence thesis by A8, A9, A10, ARYTM_1: 4;

      end;

    end;

    

     Lm5: r <= s implies (r + t) <= (s + t)

    proof

      reconsider x1 = r, y1 = s, z1 = t as Element of REAL by Def1;

      

       A1: for x9 be Element of REAL , r st x9 = r holds ( + (x9,z1)) = (r + t)

      proof

        let x9 be Element of REAL , r such that

         A2: x9 = r;

        consider x1,x2,y1,y2 be Element of REAL such that

         A3: r = [*x1, x2*] & t = [*y1, y2*] and

         A4: (r + t) = [*( + (x1,y1)), ( + (x2,y2))*] by XCMPLX_0:def 4;

        x2 = 0 & y2 = 0 by A3, Lm1;

        then

         A5: ( + (x2,y2)) = 0 by ARYTM_0: 11;

        r = x1 & t = y1 by A3, Lm1;

        hence thesis by A2, A4, A5, ARYTM_0:def 5;

      end;

      then

       A6: ( + (y1,z1)) = (s + t);

      

       A7: ( + (x1,z1)) = (r + t) by A1;

      assume

       A8: r <= s;

      per cases by A8, XXREAL_0:def 5;

        suppose that

         A9: r in REAL+ and

         A10: s in REAL+ and

         A11: t in REAL+ ;

        consider s9,t99 be Element of REAL+ such that

         A12: s = s9 & t = t99 and

         A13: ( + (y1,z1)) = (s9 + t99) by A10, A11, ARYTM_0:def 1;

        consider x9,t9 be Element of REAL+ such that

         A14: r = x9 & t = t9 and

         A15: ( + (x1,z1)) = (x9 + t9) by A9, A11, ARYTM_0:def 1;

        ex x99,s99 be Element of REAL+ st r = x99 & s = s99 & x99 <=' s99 by A8, A9, A10, XXREAL_0:def 5;

        then (x9 + t9) <=' (s9 + t99) by A14, A12, ARYTM_1: 7;

        hence thesis by A6, A7, A15, A13, Lm2;

      end;

        suppose that

         A16: r in [: { 0 }, REAL+ :] and

         A17: s in REAL+ and

         A18: t in REAL+ ;

        consider s9,t99 be Element of REAL+ such that s = s9 and

         A19: t = t99 and

         A20: ( + (y1,z1)) = (s9 + t99) by A17, A18, ARYTM_0:def 1;

        consider x9,t9 be Element of REAL+ such that r = [ 0 , x9] and

         A21: t = t9 and

         A22: ( + (x1,z1)) = (t9 - x9) by A16, A18, ARYTM_0:def 1;

        now

          per cases ;

            suppose

             A23: x9 <=' t9;

            (t9 -' x9) <=' t9 & t9 <=' (s9 + t99) by A21, A19, ARYTM_1: 11, ARYTM_2: 19;

            then

             A24: (t9 -' x9) <=' (s9 + t99) by ARYTM_1: 3;

            (t9 - x9) = (t9 -' x9) by A23, ARYTM_1:def 2;

            hence thesis by A6, A7, A22, A20, A24, Lm2;

          end;

            suppose not x9 <=' t9;

            then (t9 - x9) = [ 0 , (x9 -' t9)] by ARYTM_1:def 2;

            then (t9 - x9) in [: { 0 }, REAL+ :] by Lm3, ZFMISC_1: 87;

            then

             A25: not (r + t) in REAL+ by A7, A22, ARYTM_0: 5, XBOOLE_0: 3;

             not (s + t) in [: { 0 }, REAL+ :] by A6, A20, ARYTM_0: 5, XBOOLE_0: 3;

            hence thesis by A25, XXREAL_0:def 5;

          end;

        end;

        hence thesis;

      end;

        suppose that

         A26: r in [: { 0 }, REAL+ :] and

         A27: s in [: { 0 }, REAL+ :] and

         A28: t in REAL+ ;

        consider s9,t99 be Element of REAL+ such that

         A29: s = [ 0 , s9] and

         A30: t = t99 and

         A31: ( + (y1,z1)) = (t99 - s9) by A27, A28, ARYTM_0:def 1;

        consider x99,s99 be Element of REAL+ such that

         A32: r = [ 0 , x99] and

         A33: s = [ 0 , s99] and

         A34: s99 <=' x99 by A8, A26, A27, XXREAL_0:def 5;

        consider x9,t9 be Element of REAL+ such that

         A35: r = [ 0 , x9] and

         A36: t = t9 and

         A37: ( + (x1,z1)) = (t9 - x9) by A26, A28, ARYTM_0:def 1;

        

         A38: x9 = x99 by A32, A35, XTUPLE_0: 1;

        

         A39: s9 = s99 by A33, A29, XTUPLE_0: 1;

        now

          per cases ;

            suppose

             A40: x9 <=' t9;

            then s9 <=' t9 by A34, A38, A39, ARYTM_1: 3;

            then

             A41: (t9 - s9) = (t9 -' s9) by ARYTM_1:def 2;

            

             A42: (t9 - x9) = (t9 -' x9) by A40, ARYTM_1:def 2;

            (t9 -' x9) <=' (t99 -' s9) by A34, A36, A30, A38, A39, ARYTM_1: 16;

            hence thesis by A6, A7, A36, A37, A30, A31, A42, A41, Lm2;

          end;

            suppose not x9 <=' t9;

            then

             A43: ( + (x1,z1)) = [ 0 , (x9 -' t9)] by A37, ARYTM_1:def 2;

            then

             A44: ( + (x1,z1)) in [: { 0 }, REAL+ :] by Lm3, ZFMISC_1: 87;

            now

              per cases ;

                suppose s9 <=' t9;

                then (t9 - s9) = (t9 -' s9) by ARYTM_1:def 2;

                then

                 A45: not ( + (y1,z1)) in [: { 0 }, REAL+ :] by A36, A30, A31, ARYTM_0: 5, XBOOLE_0: 3;

                 not ( + (x1,z1)) in REAL+ by A44, ARYTM_0: 5, XBOOLE_0: 3;

                hence thesis by A6, A7, A45, XXREAL_0:def 5;

              end;

                suppose

                 A46: not s9 <=' t9;

                

                 A47: (s9 -' t9) <=' (x9 -' t9) by A34, A38, A39, ARYTM_1: 17;

                

                 A48: ( + (y1,z1)) = [ 0 , (s9 -' t9)] by A36, A30, A31, A46, ARYTM_1:def 2;

                then ( + (y1,z1)) in [: { 0 }, REAL+ :] by Lm3, ZFMISC_1: 87;

                hence thesis by A6, A7, A43, A44, A48, A47, Lm2;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

        suppose that

         A49: r in REAL+ and

         A50: s in REAL+ and

         A51: t in [: { 0 }, REAL+ :];

        consider s9,t99 be Element of REAL+ such that

         A52: s = s9 and

         A53: t = [ 0 , t99] and

         A54: ( + (y1,z1)) = (s9 - t99) by A50, A51, ARYTM_0:def 1;

        consider x9,t9 be Element of REAL+ such that

         A55: r = x9 and

         A56: t = [ 0 , t9] and

         A57: ( + (x1,z1)) = (x9 - t9) by A49, A51, ARYTM_0:def 1;

        

         A58: t9 = t99 by A56, A53, XTUPLE_0: 1;

        

         A59: ex x99,s99 be Element of REAL+ st r = x99 & s = s99 & x99 <=' s99 by A8, A49, A50, XXREAL_0:def 5;

        now

          per cases ;

            suppose

             A60: t9 <=' x9;

            then t9 <=' s9 by A59, A55, A52, ARYTM_1: 3;

            then

             A61: (s9 - t9) = (s9 -' t9) by ARYTM_1:def 2;

            

             A62: (x9 - t9) = (x9 -' t9) by A60, ARYTM_1:def 2;

            (x9 -' t9) <=' (s9 -' t99) by A59, A55, A52, A58, ARYTM_1: 17;

            hence thesis by A6, A7, A57, A54, A58, A62, A61, Lm2;

          end;

            suppose not t9 <=' x9;

            then

             A63: ( + (x1,z1)) = [ 0 , (t9 -' x9)] by A57, ARYTM_1:def 2;

            then

             A64: ( + (x1,z1)) in [: { 0 }, REAL+ :] by Lm3, ZFMISC_1: 87;

            now

              per cases ;

                suppose t9 <=' s9;

                then (s9 - t9) = (s9 -' t9) by ARYTM_1:def 2;

                then

                 A65: not ( + (y1,z1)) in [: { 0 }, REAL+ :] by A54, A58, ARYTM_0: 5, XBOOLE_0: 3;

                 not ( + (x1,z1)) in REAL+ by A64, ARYTM_0: 5, XBOOLE_0: 3;

                hence thesis by A6, A7, A65, XXREAL_0:def 5;

              end;

                suppose

                 A66: not t9 <=' s9;

                

                 A67: (t9 -' s9) <=' (t9 -' x9) by A59, A55, A52, ARYTM_1: 16;

                

                 A68: ( + (y1,z1)) = [ 0 , (t9 -' s9)] by A54, A58, A66, ARYTM_1:def 2;

                then ( + (y1,z1)) in [: { 0 }, REAL+ :] by Lm3, ZFMISC_1: 87;

                hence thesis by A6, A7, A63, A64, A68, A67, Lm2;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

        suppose that

         A69: r in [: { 0 }, REAL+ :] and

         A70: s in REAL+ and

         A71: t in [: { 0 }, REAL+ :];

        ( not r in REAL+ ) & not t in REAL+ by A69, A71, ARYTM_0: 5, XBOOLE_0: 3;

        then

        consider x9,t9 be Element of REAL+ such that r = [ 0 , x9] and

         A72: t = [ 0 , t9] and

         A73: ( + (x1,z1)) = [ 0 , (x9 + t9)] by ARYTM_0:def 1;

        

         A74: ( + (x1,z1)) in [: { 0 }, REAL+ :] by A73, Lm3, ZFMISC_1: 87;

        consider s9,t99 be Element of REAL+ such that s = s9 and

         A75: t = [ 0 , t99] and

         A76: ( + (y1,z1)) = (s9 - t99) by A70, A71, ARYTM_0:def 1;

        

         A77: t9 = t99 by A72, A75, XTUPLE_0: 1;

        now

          per cases ;

            suppose t9 <=' s9;

            then (s9 - t99) = (s9 -' t99) by A77, ARYTM_1:def 2;

            then

             A78: not ( + (y1,z1)) in [: { 0 }, REAL+ :] by A76, ARYTM_0: 5, XBOOLE_0: 3;

             not ( + (x1,z1)) in REAL+ by A74, ARYTM_0: 5, XBOOLE_0: 3;

            hence thesis by A6, A7, A78, XXREAL_0:def 5;

          end;

            suppose

             A79: not t9 <=' s9;

            (t9 -' s9) <=' t9 & t9 <=' (t9 + x9) by ARYTM_1: 11, ARYTM_2: 19;

            then

             A80: (t9 -' s9) <=' (t9 + x9) by ARYTM_1: 3;

            

             A81: ( + (y1,z1)) = [ 0 , (t9 -' s9)] by A76, A77, A79, ARYTM_1:def 2;

            then ( + (y1,z1)) in [: { 0 }, REAL+ :] by Lm3, ZFMISC_1: 87;

            hence thesis by A6, A7, A73, A74, A81, A80, Lm2;

          end;

        end;

        hence thesis;

      end;

        suppose that

         A82: r in [: { 0 }, REAL+ :] and

         A83: s in [: { 0 }, REAL+ :] and

         A84: t in [: { 0 }, REAL+ :];

        ( not s in REAL+ ) & not t in REAL+ by A83, A84, ARYTM_0: 5, XBOOLE_0: 3;

        then

        consider s9,t99 be Element of REAL+ such that

         A85: s = [ 0 , s9] and

         A86: t = [ 0 , t99] and

         A87: ( + (y1,z1)) = [ 0 , (s9 + t99)] by ARYTM_0:def 1;

        

         A88: ( + (y1,z1)) in [: { 0 }, REAL+ :] by A87, Lm3, ZFMISC_1: 87;

        ( not r in REAL+ ) & not t in REAL+ by A82, A84, ARYTM_0: 5, XBOOLE_0: 3;

        then

        consider x9,t9 be Element of REAL+ such that

         A89: r = [ 0 , x9] and

         A90: t = [ 0 , t9] and

         A91: ( + (x1,z1)) = [ 0 , (x9 + t9)] by ARYTM_0:def 1;

        

         A92: ( + (x1,z1)) in [: { 0 }, REAL+ :] by A91, Lm3, ZFMISC_1: 87;

        

         A93: t9 = t99 by A90, A86, XTUPLE_0: 1;

        consider x99,s99 be Element of REAL+ such that

         A94: r = [ 0 , x99] and

         A95: s = [ 0 , s99] and

         A96: s99 <=' x99 by A8, A82, A83, XXREAL_0:def 5;

        

         A97: s9 = s99 by A95, A85, XTUPLE_0: 1;

        x9 = x99 by A94, A89, XTUPLE_0: 1;

        then (s9 + t9) <=' (x9 + t99) by A96, A97, A93, ARYTM_1: 7;

        hence thesis by A6, A7, A91, A87, A93, A92, A88, Lm2;

      end;

    end;

    

     Lm6: r <= s & s <= t implies r <= t

    proof

      assume that

       A1: r <= s and

       A2: s <= t;

      

       A3: r in REAL & s in REAL by Def1;

      

       A4: t in REAL by Def1;

      per cases by A3, A4, NUMBERS:def 1, XBOOLE_0:def 3;

        suppose that

         A5: r in REAL+ and

         A6: s in REAL+ and

         A7: t in REAL+ ;

        consider s99,t9 be Element of REAL+ such that

         A8: s = s99 and

         A9: t = t9 and

         A10: s99 <=' t9 by A2, A6, A7, XXREAL_0:def 5;

        consider x9,s9 be Element of REAL+ such that

         A11: r = x9 and

         A12: s = s9 & x9 <=' s9 by A1, A5, A6, XXREAL_0:def 5;

        x9 <=' t9 by A12, A8, A10, ARYTM_1: 3;

        hence thesis by A11, A9, Lm2;

      end;

        suppose

         A13: r in REAL+ & s in [: { 0 }, REAL+ :];

        then ( not (r in REAL+ & s in REAL+ )) & not (r in [: { 0 }, REAL+ :] & s in [: { 0 }, REAL+ :]) by ARYTM_0: 5, XBOOLE_0: 3;

        hence thesis by A1, A13, XXREAL_0:def 5;

      end;

        suppose

         A14: s in REAL+ & t in [: { 0 }, REAL+ :];

        then ( not (t in REAL+ & s in REAL+ )) & not (t in [: { 0 }, REAL+ :] & s in [: { 0 }, REAL+ :]) by ARYTM_0: 5, XBOOLE_0: 3;

        hence thesis by A2, A14, XXREAL_0:def 5;

      end;

        suppose that

         A15: r in [: { 0 }, REAL+ :] and

         A16: t in REAL+ ;

        ( not (r in REAL+ & t in REAL+ )) & not (r in [: { 0 }, REAL+ :] & t in [: { 0 }, REAL+ :]) by A15, A16, ARYTM_0: 5, XBOOLE_0: 3;

        hence thesis by A16, XXREAL_0:def 5;

      end;

        suppose that

         A17: r in [: { 0 }, REAL+ :] and

         A18: s in [: { 0 }, REAL+ :] and

         A19: t in [: { 0 }, REAL+ :];

        consider s99,t9 be Element of REAL+ such that

         A20: s = [ 0 , s99] and

         A21: t = [ 0 , t9] and

         A22: t9 <=' s99 by A2, A18, A19, XXREAL_0:def 5;

        consider x9,s9 be Element of REAL+ such that

         A23: r = [ 0 , x9] and

         A24: s = [ 0 , s9] and

         A25: s9 <=' x9 by A1, A17, A18, XXREAL_0:def 5;

        s9 = s99 by A24, A20, XTUPLE_0: 1;

        then t9 <=' x9 by A25, A22, ARYTM_1: 3;

        hence thesis by A17, A19, A23, A21, Lm2;

      end;

    end;

    

     Lm7: not 0 in [: { 0 }, REAL+ :] by ARYTM_0: 5, ARYTM_2: 20, XBOOLE_0: 3;

    

     Lm8: 0 <= 1

    proof

      reconsider z = 0 , j = 1 as Element of REAL+ by ARYTM_2: 20;

      z <=' j by ARYTM_1: 6;

      hence thesis by Lm2;

    end;

    

     Lm14: r >= 0 & s > 0 implies (r + s) > 0

    proof

      assume r >= 0 ;

      then (r + s) >= ( 0 + s) by Lm5;

      hence thesis by Lm6;

    end;

    

     Lm15: r <= 0 & s < 0 implies (r + s) < 0

    proof

      assume r <= 0 ;

      then (r + s) <= ( 0 + s) by Lm5;

      hence thesis by Lm6;

    end;

    

     Lm16: r <= s & 0 <= t implies (r * t) <= (s * t)

    proof

      reconsider x1 = r, y1 = s, z1 = t as Element of REAL by Def1;

      assume that

       A1: r <= s and

       A2: 0 <= t;

       0 is Element of REAL+ by ARYTM_2: 20;

      then not 0 in [: { 0 }, REAL+ :] by ARYTM_0: 5, XBOOLE_0: 3;

      then

       A3: t in REAL+ by A2, XXREAL_0:def 5;

      for x9 be Element of REAL , r st x9 = r holds ( * (x9,z1)) = (r * t)

      proof

        let x9 be Element of REAL , r such that

         A4: x9 = r;

        consider x1,x2,y1,y2 be Element of REAL such that

         A5: r = [*x1, x2*] and

         A6: t = [*y1, y2*] and

         A7: (r * t) = [*( + (( * (x1,y1)),( opp ( * (x2,y2))))), ( + (( * (x1,y2)),( * (x2,y1))))*] by XCMPLX_0:def 5;

        x2 = 0 by A5, Lm1;

        then

         A8: ( * (x2,y1)) = 0 by ARYTM_0: 12;

        

         A9: y2 = 0 by A6, Lm1;

        then ( * (x1,y2)) = 0 by ARYTM_0: 12;

        then

         A10: ( + (( * (x1,y2)),( * (x2,y1)))) = 0 by A8, ARYTM_0: 11;

        r = x1 & t = y1 by A5, A6, Lm1;

        

        hence ( * (x9,z1)) = ( + (( * (x1,y1)),( * (( opp x2),y2)))) by A4, A9, ARYTM_0: 11, ARYTM_0: 12

        .= ( + (( * (x1,y1)),( opp ( * (x2,y2))))) by ARYTM_0: 15

        .= (r * t) by A7, A10, ARYTM_0:def 5;

      end;

      then

       A11: ( * (y1,z1)) = (s * t) & ( * (x1,z1)) = (r * t);

      assume

       A12: not thesis;

      then

       A13: t <> 0 ;

      per cases by A1, XXREAL_0:def 5;

        suppose that

         A14: r in REAL+ and

         A15: s in REAL+ ;

        consider s9,t99 be Element of REAL+ such that

         A16: s = s9 and

         A17: t = t99 & ( * (y1,z1)) = (s9 *' t99) by A3, A15, ARYTM_0:def 2;

        consider x9,t9 be Element of REAL+ such that

         A18: r = x9 and

         A19: t = t9 & ( * (x1,z1)) = (x9 *' t9) by A3, A14, ARYTM_0:def 2;

        ex x99,s99 be Element of REAL+ st r = x99 & s = s99 & x99 <=' s99 by A1, A14, A15, XXREAL_0:def 5;

        then (x9 *' t9) <=' (s9 *' t9) by A18, A16, ARYTM_1: 8;

        hence contradiction by A11, A12, A19, A17, Lm2;

      end;

        suppose that

         A20: r in [: { 0 }, REAL+ :] and

         A21: s in REAL+ ;

        ex x9,t9 be Element of REAL+ st r = [ 0 , x9] & t = t9 & ( * (x1,z1)) = [ 0 , (t9 *' x9)] by A3, A13, A20, ARYTM_0:def 2;

        then ( * (x1,z1)) in [: { 0 }, REAL+ :] by Lm3, ZFMISC_1: 87;

        then

         A22: not ( * (x1,z1)) in REAL+ by ARYTM_0: 5, XBOOLE_0: 3;

        ex s9,t99 be Element of REAL+ st s = s9 & t = t99 & ( * (y1,z1)) = (s9 *' t99) by A3, A21, ARYTM_0:def 2;

        then not ( * (y1,z1)) in [: { 0 }, REAL+ :] by ARYTM_0: 5, XBOOLE_0: 3;

        hence contradiction by A11, A12, A22, XXREAL_0:def 5;

      end;

        suppose that

         A23: r in [: { 0 }, REAL+ :] and

         A24: s in [: { 0 }, REAL+ :];

        consider s9,t99 be Element of REAL+ such that

         A25: s = [ 0 , s9] and

         A26: t = t99 and

         A27: ( * (y1,z1)) = [ 0 , (t99 *' s9)] by A3, A13, A24, ARYTM_0:def 2;

        

         A28: ( * (y1,z1)) in [: { 0 }, REAL+ :] by A27, Lm3, ZFMISC_1: 87;

        consider x99,s99 be Element of REAL+ such that

         A29: r = [ 0 , x99] and

         A30: s = [ 0 , s99] and

         A31: s99 <=' x99 by A1, A23, A24, XXREAL_0:def 5;

        

         A32: s9 = s99 by A30, A25, XTUPLE_0: 1;

        consider x9,t9 be Element of REAL+ such that

         A33: r = [ 0 , x9] and

         A34: t = t9 and

         A35: ( * (x1,z1)) = [ 0 , (t9 *' x9)] by A3, A13, A23, ARYTM_0:def 2;

        

         A36: ( * (x1,z1)) in [: { 0 }, REAL+ :] by A35, Lm3, ZFMISC_1: 87;

        x9 = x99 by A29, A33, XTUPLE_0: 1;

        then (s9 *' t9) <=' (x9 *' t9) by A31, A32, ARYTM_1: 8;

        hence contradiction by A11, A12, A34, A35, A26, A27, A36, A28, Lm2;

      end;

    end;

    

     Lm17: r > 0 & s > 0 implies (r * s) > 0

    proof

      assume

       A1: r > 0 & s > 0 ;

      then (r * s) >= ( 0 * s) by Lm16;

      hence thesis by A1, Lm4;

    end;

    

     Lm18: r > 0 & s < 0 implies (r * s) < 0

    proof

      assume

       A1: r > 0 & s < 0 ;

      then (r * s) <= (r * 0 ) by Lm16;

      hence thesis by A1, Lm4;

    end;

    

     Lm19: s <= t implies ( - t) <= ( - s)

    proof

      assume s <= t;

      then (s - t) <= (t - t) by Lm5;

      then ((s - t) - s) <= ( 0 - s) by Lm5;

      hence thesis;

    end;

    

     Lm20: r <= 0 & s >= 0 implies (r * s) <= 0

    proof

      assume

       A1: r <= 0 & s >= 0 ;

      per cases by A1, Lm4;

        suppose r = 0 or s = 0 ;

        hence thesis;

      end;

        suppose r < 0 & s > 0 ;

        hence thesis by Lm18;

      end;

    end;

    registration

      cluster positive for Real;

      existence

      proof

        take r = 1;

        thus 0 < r by Lm4, Lm8;

      end;

      cluster negative for Real;

      existence

      proof

        take r = ( - 1);

        (1 + ( - 1)) = 0 ;

        then

        consider x1,x2,y1,y2 be Element of REAL such that

         Lm9: 1 = [*x1, x2*] and

         Lm10: ( - 1) = [*y1, y2*] & 0 = [*( + (x1,y1)), ( + (x2,y2))*] by XCMPLX_0:def 4;

        

         Lm11: x1 = 1 by Lm1, Lm9;

        

         Lm12: y1 = ( - 1) & ( + (x1,y1)) = 0 by Lm1, Lm10;

        reconsider z = 0 as Element of REAL+ by ARYTM_2: 20;

        now

          assume ( - 1) in REAL+ ;

          then ex x9,y9 be Element of REAL+ st x1 = x9 & y1 = y9 & z = (x9 + y9) by Lm11, Lm12, ARYTM_0:def 1, ARYTM_2: 20;

          hence contradiction by Lm11, ARYTM_2: 5;

        end;

        hence 0 > r by Lm7, XXREAL_0:def 5;

      end;

      cluster zero for Real;

      existence

      proof

        take 0 ;

        thus thesis;

      end;

    end

    registration

      let r,s be non negative Real;

      cluster (r + s) -> non negative;

      coherence

      proof

        

         A1: s >= 0 by XXREAL_0:def 7;

        

         A2: r >= 0 by XXREAL_0:def 7;

        per cases by A2, Lm4;

          suppose r = 0 ;

          hence (r + s) >= 0 by XXREAL_0:def 7;

        end;

          suppose r > 0 ;

          hence (r + s) >= 0 by A1, Lm14;

        end;

      end;

    end

    registration

      let r,s be non positive Real;

      cluster (r + s) -> non positive;

      coherence

      proof

        

         A1: s <= 0 by XXREAL_0:def 6;

        

         A2: r <= 0 by XXREAL_0:def 6;

        per cases by A2, Lm4;

          suppose r = 0 ;

          hence (r + s) <= 0 by XXREAL_0:def 6;

        end;

          suppose r < 0 ;

          hence (r + s) <= 0 by A1, Lm15;

        end;

      end;

    end

    registration

      let r be positive Real;

      let s be non negative Real;

      cluster (r + s) -> positive;

      coherence

      proof

        r > 0 & s >= 0 by XXREAL_0:def 6;

        hence (r + s) > 0 by Lm14;

      end;

      cluster (s + r) -> positive;

      coherence ;

    end

    registration

      let r be negative Real;

      let s be non positive Real;

      cluster (r + s) -> negative;

      coherence

      proof

        r < 0 & s <= 0 by XXREAL_0:def 7;

        hence (r + s) < 0 by Lm15;

      end;

      cluster (s + r) -> negative;

      coherence ;

    end

    registration

      let r be non positive Real;

      cluster ( - r) -> non negative;

      coherence

      proof

        assume

         A1: ( - r) < 0 ;

        ( - ( - r)) <= 0 by XXREAL_0:def 6;

        then (( - r) + ( - ( - r))) < 0 by A1, Lm15;

        hence contradiction;

      end;

    end

    registration

      let r be non negative Real;

      cluster ( - r) -> non positive;

      coherence

      proof

        assume

         A1: ( - r) > 0 ;

        ( - ( - r)) >= 0 by XXREAL_0:def 7;

        then (( - r) + ( - ( - r))) > 0 by A1, Lm14;

        hence contradiction;

      end;

    end

    registration

      let r be non negative Real, s be non positive Real;

      cluster (r - s) -> non negative;

      coherence ;

      cluster (s - r) -> non positive;

      coherence ;

    end

    registration

      let r be positive Real;

      let s be non positive Real;

      cluster (r - s) -> positive;

      coherence ;

      cluster (s - r) -> negative;

      coherence ;

    end

    registration

      let r be negative Real;

      let s be non negative Real;

      cluster (r - s) -> negative;

      coherence ;

      cluster (s - r) -> positive;

      coherence ;

    end

    registration

      let r be non positive Real, s be non negative Real;

      cluster (r * s) -> non positive;

      coherence

      proof

        r <= 0 & s >= 0 by XXREAL_0:def 6;

        hence (r * s) <= 0 by Lm20;

      end;

      cluster (s * r) -> non positive;

      coherence ;

    end

    registration

      let r,s be non positive Real;

      cluster (r * s) -> non negative;

      coherence

      proof

        

         A1: r <= 0 & s <= 0 by XXREAL_0:def 6;

        per cases by A1, Lm4;

          suppose r = 0 or s = 0 ;

          hence (r * s) >= 0 ;

        end;

          suppose

           A2: ( - ( - r)) < ( - ( - 0 )) & s < 0 ;

          then 0 < ( - r) by Lm19;

          then (s * ( - r)) <= ( 0 * ( - r)) by A2, Lm16;

          then (s * ( - r)) < ( 0 * ( - r)) by A2, Lm4;

          then ( - ( - ( 0 * r))) < ( - ( - (s * r))) by Lm19;

          hence (r * s) >= 0 ;

        end;

      end;

    end

    registration

      let r,s be non negative Real;

      cluster (r * s) -> non negative;

      coherence

      proof

        

         A1: r >= 0 & s >= 0 by XXREAL_0:def 7;

        per cases by A1, Lm4;

          suppose r = 0 or s = 0 ;

          hence (r * s) >= 0 ;

        end;

          suppose r > 0 & s > 0 ;

          hence (r * s) >= 0 by Lm17;

        end;

      end;

    end

    registration

      let r be positive Real;

      cluster (r " ) -> positive;

      coherence

      proof

        assume

         A1: (r " ) <= 0 ;

        ((r " ) " ) > 0 by XXREAL_0:def 6;

        then ((r " ) * ((r " ) " )) = 1 & ((r " ) * ((r " ) " )) <= 0 by A1, Lm20, XCMPLX_0:def 7;

        hence contradiction by Lm4, Lm8;

      end;

    end

    registration

      let r be non positive Real;

      cluster (r " ) -> non positive;

      coherence

      proof

        

         A1: ((r " ) " ) <= 0 by XXREAL_0:def 6;

        assume

         A2: (r " ) > 0 ;

        per cases by A1, Lm4;

          suppose ((r " ) " ) = 0 ;

          hence contradiction by A2;

        end;

          suppose

           A3: ((r " ) " ) < 0 ;

          ((r " ) * ((r " ) " )) = 1 by A2, XCMPLX_0:def 7;

          hence contradiction by A2, A3, Lm8, Lm18;

        end;

      end;

    end

    registration

      let r be negative Real;

      cluster (r " ) -> negative;

      coherence ;

    end

    registration

      let r be non negative Real;

      cluster (r " ) -> non negative;

      coherence

      proof

        

         A1: ((r " ) " ) >= 0 by XXREAL_0:def 7;

        assume

         A2: (r " ) < 0 ;

        per cases by A1, Lm4;

          suppose ((r " ) " ) = 0 ;

          hence contradiction by A2;

        end;

          suppose

           A3: ((r " ) " ) > 0 ;

          ((r " ) * ((r " ) " )) = 1 by A2, XCMPLX_0:def 7;

          hence contradiction by A2, A3, Lm8, Lm18;

        end;

      end;

    end

    registration

      let r be non negative Real, s be non positive Real;

      cluster (r / s) -> non positive;

      coherence ;

      cluster (s / r) -> non positive;

      coherence ;

    end

    registration

      let r,s be non negative Real;

      cluster (r / s) -> non negative;

      coherence ;

    end

    registration

      let r,s be non positive Real;

      cluster (r / s) -> non negative;

      coherence ;

    end

    begin

    registration

      let r,s be Real;

      cluster ( min (r,s)) -> real;

      coherence by XXREAL_0: 15;

      cluster ( max (r,s)) -> real;

      coherence by XXREAL_0: 16;

    end

    definition

      let r,s be Real;

      :: XREAL_0:def2

      func r -' s -> set equals

      : Def2: (r - s) if (r - s) >= 0

      otherwise 0 ;

      correctness ;

    end

    registration

      let r,s be Real;

      cluster (r -' s) -> real;

      coherence

      proof

        (r -' s) = (r - s) or (r -' s) = 0 by Def2;

        hence thesis;

      end;

    end

    registration

      let r,s be Real;

      cluster (r -' s) -> non negative;

      coherence

      proof

        (r -' s) = (r - s) & (r - s) >= 0 or (r -' s) = 0 by Def2;

        hence thesis by XXREAL_0:def 7;

      end;

    end

    registration

      sethood of Real

      proof

        take REAL ;

        thus thesis by Def1;

      end;

    end

    registration

      let i be Real;

      reduce ( In (i, REAL )) to i;

      reducibility by Def1, SUBSET_1:def 8;

    end