axioms.miz



    begin

    reserve r,s for Real;

    

     Lm1: (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;

    reserve x,y,z for Real;

    

     Lm2: 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 XREAL_0:def 1;

      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;

    

     Lm3: for x9,y9 be Element of REAL , x, y st x9 = x & y9 = y holds ( + (x9,y9)) = (x + y)

    proof

      let x9,y9 be Element of REAL , x, y such that

       A1: x9 = x & y9 = y;

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

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

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

      x2 = 0 & y2 = 0 by A2, Lm2;

      then

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

      x = x1 & y = y1 by A2, Lm2;

      hence thesis by A1, A3, A4, ARYTM_0:def 5;

    end;

    

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

    reserve r,r1,r2 for Element of REAL+ ;

    theorem :: AXIOMS:1

    for X,Y be Subset of REAL st for x, y st x in X & y in Y holds x <= y holds ex z st for x, y st x in X & y in Y holds x <= z & z <= y

    proof

      let X,Y be Subset of REAL ;

      assume

       A1: for x, y st x in X & y in Y holds x <= y;

      per cases ;

        suppose

         A2: X = 0 or Y = 0 ;

        take 1;

        thus thesis by A2;

      end;

        suppose that

         A3: X <> 0 and

         A4: Y <> 0 ;

        consider x1 be Element of REAL such that

         A5: x1 in X by A3, SUBSET_1: 4;

        

         A6: X c= ( REAL+ \/ [: { 0 }, REAL+ :]) by NUMBERS:def 1, XBOOLE_1: 1;

        

         A7: Y c= ( REAL+ \/ [: { 0 }, REAL+ :]) by NUMBERS:def 1, XBOOLE_1: 1;

        

         A8: ex x2 be Element of REAL st x2 in Y by A4, SUBSET_1: 4;

        thus thesis

        proof

          per cases ;

            suppose that

             A9: X misses REAL+ and

             A10: Y misses [: { 0 }, REAL+ :];

            take z = 0 ;

            let x, y such that

             A11: x in X and

             A12: y in Y;

            ( not z in [: { 0 }, REAL+ :]) & not x in REAL+ by A9, A11, ARYTM_0: 5, ARYTM_2: 20, XBOOLE_0: 3;

            hence x <= z by XXREAL_0:def 5;

            Y c= REAL+ by A7, A10, XBOOLE_1: 73;

            then

            reconsider y9 = y, o = 0 as Element of REAL+ by A12, ARYTM_2: 20;

            o <=' y9 by ARYTM_1: 6;

            hence thesis by Lm1;

          end;

            suppose

             A13: Y meets [: { 0 }, REAL+ :];

            { r : [ 0 , r] in X } c= REAL+

            proof

              let u be object;

              assume u in { r : [ 0 , r] in X };

              then ex r st u = r & [ 0 , r] in X;

              hence thesis;

            end;

            then

            reconsider X9 = { r : [ 0 , r] in X } as Subset of REAL+ ;

            { r : [ 0 , r] in Y } c= REAL+

            proof

              let u be object;

              assume u in { r : [ 0 , r] in Y };

              then ex r st u = r & [ 0 , r] in Y;

              hence thesis;

            end;

            then

            reconsider Y9 = { r : [ 0 , r] in Y } as Subset of REAL+ ;

            consider e be object such that

             A14: e in Y and

             A15: e in [: { 0 }, REAL+ :] by A13, XBOOLE_0: 3;

            consider u,y1 be object such that

             A16: u in { 0 } and

             A17: y1 in REAL+ and

             A18: e = [u, y1] by A15, ZFMISC_1: 84;

            reconsider y1 as Element of REAL+ by A17;

            e in REAL by A14;

            then

             A19: [ 0 , y1] in REAL by A16, A18, TARSKI:def 1;

            then

            reconsider y0 = [ 0 , y1] as Real;

            

             A20: y0 in Y by A14, A16, A18, TARSKI:def 1;

            then

             A21: y1 in Y9;

            

             A22: y0 in [: { 0 }, REAL+ :] by Lm4, ZFMISC_1: 87;

            

             A23: X c= [: { 0 }, REAL+ :]

            proof

              let u be object;

              assume

               A24: u in X;

              then

              reconsider x = u as Real;

              now

                assume x in REAL+ ;

                then

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

                x <= y0 & not y0 in REAL+ by A1, A22, A20, A24, ARYTM_0: 5, XBOOLE_0: 3;

                hence contradiction by A25, XXREAL_0:def 5;

              end;

              hence thesis by A6, A24, XBOOLE_0:def 3;

            end;

            then

            consider e,x3 be object such that

             A26: e in { 0 } and

             A27: x3 in REAL+ and

             A28: x1 = [e, x3] by A5, ZFMISC_1: 84;

            reconsider x3 as Element of REAL+ by A27;

            x1 = [ 0 , x3] by A26, A28, TARSKI:def 1;

            then

             A29: x3 in X9 by A5;

            for y9,x9 be Element of REAL+ st y9 in Y9 & x9 in X9 holds y9 <=' x9

            proof

              let y9,x9 be Element of REAL+ ;

              assume y9 in Y9;

              then

               A30: ex r1 st y9 = r1 & [ 0 , r1] in Y;

              assume x9 in X9;

              then

               A31: ex r2 st x9 = r2 & [ 0 , r2] in X;

              then

              reconsider x = [ 0 , x9], y = [ 0 , y9] as Real by A30;

              

               A32: x in [: { 0 }, REAL+ :] & y in [: { 0 }, REAL+ :] by Lm4, ZFMISC_1: 87;

              x <= y by A1, A30, A31;

              then

              consider x99,y99 be Element of REAL+ such that

               A33: x = [ 0 , x99] and

               A34: y = [ 0 , y99] & y99 <=' x99 by A32, XXREAL_0:def 5;

              x9 = x99 by A33, XTUPLE_0: 1;

              hence thesis by A34, XTUPLE_0: 1;

            end;

            then

            consider z9 be Element of REAL+ such that

             A35: for y9,x9 be Element of REAL+ st y9 in Y9 & x9 in X9 holds y9 <=' z9 & z9 <=' x9 by A29, ARYTM_2: 8;

            

             A36: y1 <> 0 by A19, ARYTM_0: 3;

            y1 <=' z9 by A21, A29, A35;

            then [ 0 , z9] in REAL by A36, ARYTM_0: 2, ARYTM_1: 5;

            then

            reconsider z = [ 0 , z9] as Real;

            take z;

            let x, y such that

             A37: x in X and

             A38: y in Y;

            consider e,x9 be object such that

             A39: e in { 0 } and

             A40: x9 in REAL+ and

             A41: x = [e, x9] by A23, A37, ZFMISC_1: 84;

            reconsider x9 as Element of REAL+ by A40;

            

             A42: z in [: { 0 }, REAL+ :] by Lm4, ZFMISC_1: 87;

            

             A43: x = [ 0 , x9] by A39, A41, TARSKI:def 1;

            then

             A44: x9 in X9 by A37;

            per cases by A7, A38, XBOOLE_0:def 3;

              suppose

               A45: y in REAL+ ;

              z9 <=' x9 by A21, A35, A44;

              hence x <= z by A23, A42, A37, A43, Lm1;

              

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

               not z in REAL+ by A42, ARYTM_0: 5, XBOOLE_0: 3;

              hence z <= y by A46, XXREAL_0:def 5;

            end;

              suppose

               A47: y in [: { 0 }, REAL+ :];

              then

              consider e,y9 be object such that

               A48: e in { 0 } and

               A49: y9 in REAL+ and

               A50: y = [e, y9] by ZFMISC_1: 84;

              reconsider y9 as Element of REAL+ by A49;

              

               A51: y = [ 0 , y9] by A48, A50, TARSKI:def 1;

              then y9 in Y9 by A38;

              then y9 <=' z9 & z9 <=' x9 by A35, A44;

              hence thesis by A23, A42, A37, A43, A47, A51, Lm1;

            end;

          end;

            suppose

             A52: X meets REAL+ ;

            reconsider X9 = (X /\ REAL+ ) as Subset of REAL+ by XBOOLE_1: 17;

            consider x1 be object such that

             A53: x1 in X and

             A54: x1 in REAL+ by A52, XBOOLE_0: 3;

            reconsider x1 as Element of REAL+ by A54;

            x1 in REAL+ ;

            then

            reconsider x0 = x1 as Real by ARYTM_0: 1;

            

             A55: Y c= REAL+

            proof

              let u be object;

              assume

               A56: u in Y;

              then

              reconsider y = u as Real;

              now

                assume y in [: { 0 }, REAL+ :];

                then

                 A57: not y in REAL+ by ARYTM_0: 5, XBOOLE_0: 3;

                x0 <= y & not x0 in [: { 0 }, REAL+ :] by A1, A53, A56, ARYTM_0: 5, XBOOLE_0: 3;

                hence contradiction by A57, XXREAL_0:def 5;

              end;

              hence thesis by A7, A56, XBOOLE_0:def 3;

            end;

            then

            reconsider Y9 = Y as Subset of REAL+ ;

            for x9,y9 be Element of REAL+ st x9 in X9 & y9 in Y9 holds x9 <=' y9

            proof

              let x9,y9 be Element of REAL+ ;

              

               A58: X9 c= X by XBOOLE_1: 17;

              x9 in REAL+ & y9 in REAL+ ;

              then

              reconsider x = x9, y = y9 as Real by ARYTM_0: 1;

              assume x9 in X9 & y9 in Y9;

              then x <= y by A1, A58;

              then ex x9,y9 be Element of REAL+ st x = x9 & y = y9 & x9 <=' y9 by XXREAL_0:def 5;

              hence thesis;

            end;

            then

            consider z9 be Element of REAL+ such that

             A59: for x9,y9 be Element of REAL+ st x9 in X9 & y9 in Y9 holds x9 <=' z9 & z9 <=' y9 by A8, ARYTM_2: 8;

            z9 in REAL+ ;

            then

            reconsider z = z9 as Real by ARYTM_0: 1;

            take z;

            let x, y such that

             A60: x in X and

             A61: y in Y;

            reconsider y9 = y as Element of REAL+ by A55, A61;

            

             A62: x0 in X9 by A53, XBOOLE_0:def 4;

            per cases by A6, A60, XBOOLE_0:def 3;

              suppose x in REAL+ ;

              then

              reconsider x9 = x as Element of REAL+ ;

              x9 in X9 by A60, XBOOLE_0:def 4;

              then x9 <=' z9 & z9 <=' y9 by A59, A61;

              hence thesis by Lm1;

            end;

              suppose

               A63: x in [: { 0 }, REAL+ :];

              

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

               not x in REAL+ by A63, ARYTM_0: 5, XBOOLE_0: 3;

              hence x <= z by A64, XXREAL_0:def 5;

              z9 <=' y9 by A62, A59, A61;

              hence z <= y by Lm1;

            end;

          end;

        end;

      end;

    end;

    theorem :: AXIOMS:2

    x in NAT & y in NAT implies (x + y) in NAT

    proof

      reconsider x1 = x, y1 = y as Element of REAL by XREAL_0:def 1;

      

       A1: ( + (x1,y1)) = (x + y) by Lm3;

      assume

       A2: x in NAT & y in NAT ;

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

      hence thesis by A1, A2, ARYTM_2: 16;

    end;

    theorem :: AXIOMS:3

    for A be Subset of REAL st 0 in A & for x st x in A holds (x + 1) in A holds NAT c= A

    proof

      let A be Subset of REAL such that

       A1: 0 in A and

       A2: for x st x in A holds (x + 1) in A;

      reconsider B = (A /\ REAL+ ) as Subset of REAL+ by XBOOLE_1: 17;

      

       A3: B c= A by XBOOLE_1: 17;

      

       A4: for x9,y9 be Element of REAL+ st x9 in B & y9 = 1 holds (x9 + y9) in B

      proof

        let x9,y9 be Element of REAL+ such that

         A5: x9 in B and

         A6: y9 = 1;

        reconsider x = x9 as Element of REAL by ARYTM_0: 1;

        reconsider y = 1 as Element of REAL by NUMBERS: 19;

        reconsider xx = x as Real;

        (xx + 1) in A by A2, A3, A5;

        then (ex x99,y99 be Element of REAL+ st x = x99 & 1 = y99 & ( + (x,y)) = (x99 + y99)) & ( + (x,y)) in A by Lm3, ARYTM_0:def 1, ARYTM_2: 20;

        hence thesis by A6, XBOOLE_0:def 4;

      end;

       0 in B by A1, ARYTM_2: 20, XBOOLE_0:def 4;

      then NAT c= B by A4, ARYTM_2: 17;

      hence thesis by A3;

    end;

    theorem :: AXIOMS:4

    for k be natural Number holds k = { i where i be Nat : i < k }

    proof

      let k be natural Number;

      

       A1: k in NAT by ORDINAL1:def 12;

      set Y = { i where i be Nat : i < k };

      reconsider K = k as Element of NAT by ORDINAL1:def 12;

      for e be object holds e in K iff e in Y

      proof

        let e be object;

        thus e in K implies e in Y

        proof

          assume

           A2: e in K;

          

           A3: K c= NAT by ORDINAL1:def 2;

          then

          reconsider j = e as Element of NAT by A2;

          e in NAT by A3, A2;

          then

          reconsider y9 = e as Element of REAL+ by ARYTM_2: 2;

          reconsider x9 = K as Element of REAL+ by ARYTM_2: 2;

          y9 <=' x9 by A2, ARYTM_2: 18;

          then

           A4: j <= k by Lm1;

          reconsider yy9 = y9 as set;

           not yy9 in yy9;

          then y9 <> x9 by A2;

          then j < k by A4, XXREAL_0: 1;

          hence thesis;

        end;

        assume e in Y;

        then

        consider i be Nat such that

         A5: e = i and

         A6: not k <= i;

        

         A7: i in NAT by ORDINAL1:def 12;

        then

        reconsider x9 = e, y9 = k as Element of REAL+ by A5, A1, ARYTM_2: 2;

         not y9 <=' x9 by A5, A6, Lm1;

        hence thesis by A5, A6, A7, ARYTM_2: 18;

      end;

      hence thesis by TARSKI: 2;

    end;