numbers.miz



    begin

    

     Lm1: omega c= (({ [c, d] where c,d be Element of omega : (c,d) are_coprime & d <> {} } \ the set of all [k, 1] where k be Element of omega ) \/ omega ) by XBOOLE_1: 7;

    notation

      synonym NAT for omega ;

    end

    

     Lm2: 1 = ( succ 0 );

    definition

      :: NUMBERS:def1

      func REAL -> set equals (( REAL+ \/ [: { 0 }, REAL+ :]) \ { [ 0 , 0 ]});

      coherence ;

    end

    

     Lm3: REAL+ c= REAL

    proof

       REAL+ c= ( REAL+ \/ [: { 0 }, REAL+ :]) by XBOOLE_1: 7;

      hence thesis by ARYTM_2: 3, ZFMISC_1: 34;

    end;

    registration

      cluster REAL -> non empty;

      coherence by Lm3, XBOOLE_1: 3;

    end

    definition

      :: NUMBERS:def2

      func COMPLEX -> set equals ((( Funcs ( { 0 , 1}, REAL )) \ { x where x be Element of ( Funcs ( { 0 , 1}, REAL )) : (x . 1) = 0 }) \/ REAL );

      coherence ;

      :: NUMBERS:def3

      func RAT -> set equals (( RAT+ \/ [: { 0 }, RAT+ :]) \ { [ 0 , 0 ]});

      coherence ;

      :: NUMBERS:def4

      func INT -> set equals (( NAT \/ [: { 0 }, NAT :]) \ { [ 0 , 0 ]});

      coherence ;

    end

    

     Lm4: RAT+ c= RAT

    proof

       RAT+ c= ( RAT+ \/ [: { 0 }, RAT+ :]) by XBOOLE_1: 7;

      hence thesis by ARYTM_3: 61, ZFMISC_1: 34;

    end;

    

     Lm5: NAT c= INT

    proof

       NAT c= ( NAT \/ [: { 0 }, NAT :]) by XBOOLE_1: 7;

      hence thesis by ARYTM_3: 32, ZFMISC_1: 34;

    end;

    registration

      cluster COMPLEX -> non empty;

      coherence ;

      cluster RAT -> non empty;

      coherence by Lm4, XBOOLE_1: 3;

      cluster INT -> non empty;

      coherence by Lm5, XBOOLE_1: 3;

    end

    reserve i,j,k for Element of NAT ;

    reserve a,b for Element of REAL ;

    

     Lm6: for x,y,z be set st [x, y] = {z} holds z = {x} & x = y

    proof

      let x,y,z be set;

      assume

       A1: [x, y] = {z};

      then {x} in {z} by TARSKI:def 2;

      hence

       A2: z = {x} by TARSKI:def 1;

       {x, y} in {z} by A1, TARSKI:def 2;

      then {x, y} = z by TARSKI:def 1;

      hence thesis by A2, ZFMISC_1: 5;

    end;

    

     Lm7: not (( 0 , one ) --> (a,b)) in REAL

    proof

      set IR = { A where A be Subset of RAT+ : for r be Element of RAT+ st r in A holds (for s be Element of RAT+ st s <=' r holds s in A) & ex s be Element of RAT+ st s in A & r < s };

      set f = (( 0 , one ) --> (a,b));

       A1:

      now

        f = { [ 0 , a], [ one , b]} by FUNCT_4: 67;

        then

         A2: [ one , b] in f by TARSKI:def 2;

        assume f in [: { {} }, REAL+ :];

        then

        consider x,y be object such that

         A3: x in { {} } and y in REAL+ and

         A4: f = [x, y] by ZFMISC_1: 84;

        

         A5: x = 0 by A3, TARSKI:def 1;

        per cases by A4, A5, A2, TARSKI:def 2;

          suppose { { one , b}, { one }} = { 0 };

          then 0 in { { one , b}, { one }} by TARSKI:def 1;

          hence contradiction by TARSKI:def 2;

        end;

          suppose { { one , b}, { one }} = { 0 , y};

          then 0 in { { one , b}, { one }} by TARSKI:def 2;

          hence contradiction by TARSKI:def 2;

        end;

      end;

      

       A6: f = { [ 0 , a], [ one , b]} by FUNCT_4: 67;

      now

        assume f in { [i, j] : (i,j) are_coprime & j <> {} };

        then

        consider i, j such that

         A7: f = [i, j] and (i,j) are_coprime and j <> {} ;

        

         A8: {i} in f & {i, j} in f by A7, TARSKI:def 2;

         A9:

        now

          assume i = j;

          then {i} = {i, j} by ENUMSET1: 29;

          then

           A10: [i, j] = { {i}} by ENUMSET1: 29;

          then [ one , b] in { {i}} by A6, A7, TARSKI:def 2;

          then

           A11: [ one , b] = {i} by TARSKI:def 1;

           [ 0 , a] in { {i}} by A6, A7, A10, TARSKI:def 2;

          then [ 0 , a] = {i} by TARSKI:def 1;

          hence contradiction by A11, XTUPLE_0: 1;

        end;

        per cases by A6, A8, TARSKI:def 2;

          suppose {i, j} = [ 0 , a] & {i} = [ 0 , a];

          hence contradiction by A9, ZFMISC_1: 5;

        end;

          suppose that

           A12: {i, j} = [ 0 , a] and

           A13: {i} = [ one , b];

          i in { { 0 }, { 0 , a}} by A12, TARSKI:def 2;

          then i = { 0 , a} or i = { 0 } by TARSKI:def 2;

          then

           A14: 0 in i by TARSKI:def 1, TARSKI:def 2;

          i = { one } by A13, Lm6;

          hence contradiction by A14, TARSKI:def 1;

        end;

          suppose that

           A15: {i, j} = [ one , b] and

           A16: {i} = [ 0 , a];

          i in { { one }, { one , b}} by A15, TARSKI:def 2;

          then i = { one , b} or i = { one } by TARSKI:def 2;

          then

           A17: one in i by TARSKI:def 1, TARSKI:def 2;

          i = { 0 } by A16, Lm6;

          hence contradiction by A17, TARSKI:def 1;

        end;

          suppose {i, j} = [ one , b] & {i} = [ one , b];

          hence contradiction by A9, ZFMISC_1: 5;

        end;

      end;

      then

       A18: not f in ({ [i, j] : (i,j) are_coprime & j <> {} } \ the set of all [k, one ]);

       not ex x,y be set st { [ 0 , x], [ one , y]} in IR

      proof

        given x,y be set such that

         A19: { [ 0 , x], [ one , y]} in IR;

        consider A be Subset of RAT+ such that

         A20: { [ 0 , x], [ one , y]} = A and

         A21: for r be Element of RAT+ st r in A holds (for s be Element of RAT+ st s <=' r holds s in A) & ex s be Element of RAT+ st s in A & r < s by A19;

         [ 0 , x] in A & for r,s be Element of RAT+ st r in A & s <=' r holds s in A by A20, A21, TARSKI:def 2;

        then

        consider r1,r2,r3 be Element of RAT+ such that

         A22: r1 in A and

         A23: r2 in A and

         A24: r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 by ARYTM_3: 75;

        

         A25: r2 = [ 0 , x] or r2 = [ one , y] by A20, A23, TARSKI:def 2;

        r1 = [ 0 , x] or r1 = [ one , y] by A20, A22, TARSKI:def 2;

        hence contradiction by A20, A24, A25, TARSKI:def 2;

      end;

      then

       A26: not f in DEDEKIND_CUTS by A6, ARYTM_2:def 1;

      now

        assume f in omega ;

        then {} in f by ORDINAL3: 8;

        hence contradiction by A6, TARSKI:def 2;

      end;

      then not f in RAT+ by A18, XBOOLE_0:def 3;

      then not f in REAL+ by A26, ARYTM_2:def 2, XBOOLE_0:def 3;

      hence thesis by A1, XBOOLE_0:def 3;

    end;

    definition

      :: original: 0

      redefine

      func 0 -> Element of omega ;

      coherence by ORDINAL1:def 11;

    end

    theorem :: NUMBERS:1

    

     Th1: REAL c< COMPLEX

    proof

      set X = { x where x be Element of ( Funcs ( { 0 , one }, REAL )) : (x . one ) = 0 };

      thus REAL c= COMPLEX by XBOOLE_1: 7;

       A1:

      now

        assume (( 0 ,1) --> ( 0 ,1)) in X;

        then ex x be Element of ( Funcs ( { 0 , one }, REAL )) st x = (( 0 ,1) --> ( 0 ,1)) & (x . one ) = 0 ;

        hence contradiction by FUNCT_4: 63;

      end;

       REAL+ c= ( REAL+ \/ [: { {} }, REAL+ :]) by XBOOLE_1: 7;

      then

       A2: REAL+ c= REAL by ARYTM_2: 3, ZFMISC_1: 34;

      then

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

      

       A3: not (( 0 ,1) --> (z,j)) in REAL by Lm7;

      ( rng (( 0 ,1) --> ( 0 ,1))) c= { 0 , 1} & { 0 , 1} c= REAL by A2, ARYTM_2: 20, FUNCT_4: 62, ZFMISC_1: 32;

      then ( dom (( 0 ,1) --> ( 0 ,1))) = { 0 , 1} & ( rng (( 0 ,1) --> ( 0 ,1))) c= REAL by FUNCT_4: 62;

      then (( 0 ,1) --> ( 0 ,1)) in ( Funcs ( { 0 , one }, REAL )) by FUNCT_2:def 2;

      then (( 0 ,1) --> ( 0 ,1)) in (( Funcs ( { 0 , one }, REAL )) \ X) by A1, XBOOLE_0:def 5;

      hence thesis by A3, XBOOLE_0:def 3;

    end;

    

     Lm8: RAT c= REAL

    proof

       [: { 0 }, RAT+ :] c= [: { 0 }, REAL+ :] by ARYTM_2: 1, ZFMISC_1: 95;

      then ( RAT+ \/ [: { 0 }, RAT+ :]) c= ( REAL+ \/ [: { 0 }, REAL+ :]) by ARYTM_2: 1, XBOOLE_1: 13;

      hence thesis by XBOOLE_1: 33;

    end;

    reserve r,s,t for Element of RAT+ ;

    reserve i,j,k for Element of omega ;

    

     Lm9: for i,j be ordinal Element of RAT+ st i in j holds i < j

    proof

      let i,j be ordinal Element of RAT+ ;

      

       A1: j in omega by ARYTM_3: 31;

      i in omega by ARYTM_3: 31;

      then

      reconsider x = i, y = j as Element of REAL+ by A1, ARYTM_2: 2;

      assume

       A2: i in j;

      then x <=' y by A1, ARYTM_2: 18;

      then

       A3: ex x9,y9 be Element of RAT+ st x = x9 & y = y9 & x9 <=' y9 by ARYTM_2:def 5;

      i <> j by A2;

      hence thesis by A3, ARYTM_3: 66;

    end;

    

     Lm10: for i,j be ordinal Element of RAT+ st i c= j holds i <=' j

    proof

      let i,j be ordinal Element of RAT+ ;

      assume i c= j;

      then

      consider C be Ordinal such that

       A1: j = (i +^ C) by ORDINAL3: 27;

      C in omega by A1, ORDINAL3: 74;

      then

      reconsider C as Element of RAT+ by Lm1;

      j = (i + C) by A1, ARYTM_3: 58;

      hence thesis;

    end;

    

     Lm11: 2 = { 0 , 1}

    proof

      

      thus 2 = ( succ 1)

      .= (( succ 0 ) \/ {1})

      .= (( 0 \/ { 0 }) \/ {1})

      .= { 0 , 1} by ENUMSET1: 1;

    end;

    

     Lm12: for i,k be natural Ordinal st (i *^ i) = (2 *^ k) holds ex k be natural Ordinal st i = (2 *^ k)

    proof

      let i,k be natural Ordinal;

      assume

       A1: (i *^ i) = (2 *^ k);

      set id2 = (i div^ 2);

       {} in 2 by ORDINAL1: 14, Lm11;

      then

       A2: (i mod^ 2) in 2 by ARYTM_3: 6;

      per cases by A2, Lm11, TARSKI:def 2;

        suppose

         A3: (i mod^ 2) = 0 ;

        take k = id2;

        

        thus i = ((k *^ 2) +^ 0 ) by A3, ORDINAL3: 65

        .= (2 *^ k) by ORDINAL2: 27;

      end;

        suppose (i mod^ 2) = 1;

        then i = ((id2 *^ 2) +^ 1) by ORDINAL3: 65;

        

        then

         A4: (i *^ i) = (((id2 *^ 2) *^ ((id2 *^ 2) +^ 1)) +^ ( one *^ ((id2 *^ 2) +^ 1))) by ORDINAL3: 46

        .= (((id2 *^ 2) *^ ((id2 *^ 2) +^ 1)) +^ (( one *^ (id2 *^ 2)) +^ ( one *^ 1))) by ORDINAL3: 46

        .= (((id2 *^ 2) *^ ((id2 *^ 2) +^ 1)) +^ (( one *^ (id2 *^ 2)) +^ 1)) by ORDINAL2: 39

        .= ((((id2 *^ 2) *^ ((id2 *^ 2) +^ 1)) +^ ( one *^ (id2 *^ 2))) +^ 1) by ORDINAL3: 30

        .= (((id2 *^ 2) *^ (((id2 *^ 2) +^ 1) +^ one )) +^ 1) by ORDINAL3: 46

        .= (((id2 *^ (((id2 *^ 2) +^ 1) +^ one )) *^ 2) +^ 1) by ORDINAL3: 50;

        

         A5: 1 divides 2 by ARYTM_3: 9;

        2 divides ((id2 *^ (((id2 *^ 2) +^ 1) +^ one )) *^ 2) & 2 divides (i *^ i) by A1;

        then 2 divides 1 by A4, ARYTM_3: 11;

        hence thesis by A5, ARYTM_3: 8;

      end;

    end;

    

     Lm13: ( one + one ) = 2

    proof

      (1 +^ 1) = ( succ (1 +^ {} )) by Lm2, ORDINAL2: 28

      .= ( succ 1) by ORDINAL2: 27

      .= 2;

      hence thesis by ARYTM_3: 58;

    end;

    

     Lm14: for two,i be Element of RAT+ st two = 2 holds (i + i) = (two *' i)

    proof

      let two,i be Element of RAT+ such that

       A0: two = 2;

      

      thus (i + i) = (( one *' i) + i) by ARYTM_3: 53

      .= (( one *' i) + ( one *' i)) by ARYTM_3: 53

      .= (two *' i) by A0, Lm13, ARYTM_3: 57;

    end;

    theorem :: NUMBERS:2

    

     Th2: RAT c< REAL

    proof

      reconsider two = 2 as ordinal Element of RAT+ by Lm1;

      reconsider a9 = 1 as Element of RAT+ by Lm1;

      defpred P[ Element of RAT+ ] means ($1 *' $1) < two;

      set X = { s : P[s] };

      reconsider X as Subset of RAT+ from DOMAIN_1:sch 7;

      

       A1: (2 *^ 2) = (two *' two) & (1 *^ 2) = 2 by ARYTM_3: 59, ORDINAL2: 39;

      2 = ( succ 1)

      .= (1 \/ {1});

      then

       A2: a9 <=' two by Lm10, XBOOLE_1: 7;

      then

       A3: a9 < two by ARYTM_3: 68;

      

       A4: (a9 *' a9) = a9 by ARYTM_3: 53;

      then

       A5: 1 in X by A3;

      

       A6: for r, t st r in X & t <=' r holds t in X

      proof

        let r, t;

        assume r in X;

        then

         A7: ex s st r = s & (s *' s) < two;

        assume t <=' r;

        then (t *' t) <=' (t *' r) & (t *' r) <=' (r *' r) by ARYTM_3: 82;

        then (t *' t) <=' (r *' r) by ARYTM_3: 67;

        then (t *' t) < two by A7, ARYTM_3: 69;

        hence thesis;

      end;

      then

       A8: 0 in X by A5, ARYTM_3: 64;

      now

        assume X = [ 0 , 0 ];

        

        then X = { { 0 }, { 0 }} by ENUMSET1: 29

        .= { { 0 }} by ENUMSET1: 29;

        hence contradiction by A8, TARSKI:def 1;

      end;

      then

       A9: not X in { [ 0 , 0 ]} by TARSKI:def 1;

      reconsider O9 = 0 as Element of RAT+ by Lm1;

      set DD = { A where A be Subset of RAT+ : r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s };

      consider half be Element of RAT+ such that

       A10: a9 = (two *' half) by ARYTM_3: 55, Lm11;

      

       A11: one <=' two by Lm13;

      then

       A12: one < two by ARYTM_3: 68;

       A13:

      now

        assume X in { { s : s < t } : t <> 0 };

        then

        consider t0 be Element of RAT+ such that

         A14: X = { s : s < t0 } and

         A15: t0 <> 0 ;

        set n = ( numerator t0), d = ( denominator t0);

        now

          assume

           A16: (t0 *' t0) <> two;

          per cases by A16, ARYTM_3: 66;

            suppose (t0 *' t0) < two;

            then t0 in X;

            then ex s st s = t0 & s < t0 by A14;

            hence contradiction;

          end;

            suppose

             A17: two < (t0 *' t0);

            consider es be Element of RAT+ such that

             A18: (two + es) = (t0 *' t0) or ((t0 *' t0) + es) = two by ARYTM_3: 92;

             A19:

            now

              assume O9 = es;

              then (two + es) = two by ARYTM_3: 50;

              hence contradiction by A17, A18;

            end;

            O9 <=' es by ARYTM_3: 64;

            then O9 < es by A19, ARYTM_3: 68;

            then

            consider s such that

             A20: O9 < s and

             A21: s < es by ARYTM_3: 93;

            now

              per cases ;

                suppose

                 A22: s < one ;

                

                 A23: s <> 0 by A20;

                then (s *' s) < (s *' one ) by A22, ARYTM_3: 80;

                then

                 A24: (s *' s) < s by ARYTM_3: 53;

                 A25:

                now

                  assume

                   A26: t0 <=' one ;

                  then (t0 *' t0) <=' (t0 *' one ) by ARYTM_3: 82;

                  then (t0 *' t0) <=' t0 by ARYTM_3: 53;

                  then (t0 *' t0) <=' one by A26, ARYTM_3: 67;

                  hence contradiction by A11, A17, ARYTM_3: 69;

                end;

                then

                 A27: ( one *' one ) < ( one *' t0) by ARYTM_3: 80;

                ( one *' t0) < (two *' t0) by A12, A15, ARYTM_3: 80;

                then

                 A28: ( one *' one ) < (two *' t0) by A27, ARYTM_3: 70;

                consider t02s2 be Element of RAT+ such that

                 A29: ((s *' s) + t02s2) = (t0 *' t0) or ((t0 *' t0) + t02s2) = (s *' s) by ARYTM_3: 92;

                s < t0 by A22, A25, ARYTM_3: 70;

                then

                 A30: (s *' s) < t0 by A24, ARYTM_3: 70;

                consider T2t9 be Element of RAT+ such that

                 A31: ((two *' t0) *' T2t9) = one by A15, ARYTM_3: 55, ARYTM_3: 78;

                set x = ((s *' s) *' T2t9);

                consider t0x be Element of RAT+ such that

                 A32: (x + t0x) = t0 or (t0 + t0x) = x by ARYTM_3: 92;

                (x *' (two *' t0)) = ((s *' s) *' one ) by A31, ARYTM_3: 52;

                then x <=' (s *' s) or (two *' t0) <=' one by ARYTM_3: 83;

                then

                 A33: x < t0 by A28, A30, ARYTM_3: 53, ARYTM_3: 69;

                then

                 A34: t0x <=' t0 by A32;

                

                 A35: (((x *' t0x) + (x *' t0)) + (x *' x)) = (((x *' t0x) + (x *' x)) + (x *' t0)) by ARYTM_3: 51

                .= ((x *' t0) + (x *' t0)) by A32, A33, ARYTM_3: 57

                .= (((x *' t0) *' one ) + (x *' t0)) by ARYTM_3: 53

                .= (((x *' t0) *' one ) + ((x *' t0) *' one )) by ARYTM_3: 53

                .= ((t0 *' x) *' two) by Lm13, ARYTM_3: 57

                .= (x *' (t0 *' two)) by ARYTM_3: 52

                .= ((s *' s) *' one ) by A31, ARYTM_3: 52

                .= (s *' s) by ARYTM_3: 53;

                es <=' (t0 *' t0) by A17, A18;

                then s < (t0 *' t0) by A21, ARYTM_3: 69;

                then

                 A36: (s *' s) < (t0 *' t0) by A24, ARYTM_3: 70;

                

                then ((t02s2 + (x *' x)) + (s *' s)) = (((t0x + x) *' t0) + (x *' x)) by A29, A32, A33, ARYTM_3: 51

                .= (((t0x *' (t0x + x)) + (x *' t0)) + (x *' x)) by A32, A33, ARYTM_3: 57

                .= ((((t0x *' t0x) + (x *' t0x)) + (x *' t0)) + (x *' x)) by ARYTM_3: 57

                .= (((t0x *' t0x) + (x *' t0x)) + ((x *' t0) + (x *' x))) by ARYTM_3: 51

                .= ((t0x *' t0x) + ((x *' t0x) + ((x *' t0) + (x *' x)))) by ARYTM_3: 51

                .= ((t0x *' t0x) + (s *' s)) by A35, ARYTM_3: 51;

                then (t0x *' t0x) = (t02s2 + (x *' x)) by ARYTM_3: 62;

                then

                 A37: t02s2 <=' (t0x *' t0x);

                now

                  assume

                   A38: x = 0 ;

                  per cases by A38, ARYTM_3: 78;

                    suppose (s *' s) = 0 ;

                    hence contradiction by A23, ARYTM_3: 78;

                  end;

                    suppose T2t9 = 0 ;

                    hence contradiction by A31, ARYTM_3: 48;

                  end;

                end;

                then t0x <> t0 by A32, A33, ARYTM_3: 84;

                then t0x < t0 by A34, ARYTM_3: 68;

                then t0x in X by A14;

                then

                 A39: ex s st s = t0x & (s *' s) < two;

                (s *' s) < es by A21, A24, ARYTM_3: 70;

                then (two + (s *' s)) < (two + es) by ARYTM_3: 76;

                then two < t02s2 by A17, A18, A29, A36, ARYTM_3: 76;

                hence contradiction by A37, A39, ARYTM_3: 69;

              end;

                suppose

                 A40: one <=' s;

                (half *' two) = ( one *' one ) by A10, ARYTM_3: 53;

                then

                 A41: half <=' one by A12, ARYTM_3: 83;

                half <> one by A10, ARYTM_3: 53;

                then

                 A42: half < one by A41, ARYTM_3: 68;

                then half < s by A40, ARYTM_3: 69;

                then

                 A43: half < es by A21, ARYTM_3: 70;

                 one <=' two by Lm13;

                then one < two by ARYTM_3: 68;

                then

                 A44: ( one *' t0) < (two *' t0) by A15, ARYTM_3: 80;

                 A45:

                now

                  assume

                   A46: t0 <=' one ;

                  then (t0 *' t0) <=' (t0 *' one ) by ARYTM_3: 82;

                  then (t0 *' t0) <=' t0 by ARYTM_3: 53;

                  then (t0 *' t0) <=' one by A46, ARYTM_3: 67;

                  hence contradiction by A11, A17, ARYTM_3: 69;

                end;

                then ( one *' one ) < ( one *' t0) by ARYTM_3: 80;

                then

                 A47: ( one *' one ) < (two *' t0) by A44, ARYTM_3: 70;

                set s = half;

                consider t02s2 be Element of RAT+ such that

                 A48: ((s *' s) + t02s2) = (t0 *' t0) or ((t0 *' t0) + t02s2) = (s *' s) by ARYTM_3: 92;

                

                 A49: half <> 0 by A10, ARYTM_3: 48;

                then (half *' half) < (half *' one ) by A42, ARYTM_3: 80;

                then

                 A50: (half *' half) < half by ARYTM_3: 53;

                s < t0 by A42, A45, ARYTM_3: 70;

                then

                 A51: (s *' s) < t0 by A50, ARYTM_3: 70;

                consider T2t9 be Element of RAT+ such that

                 A52: ((two *' t0) *' T2t9) = one by A15, ARYTM_3: 55, ARYTM_3: 78;

                set x = ((s *' s) *' T2t9);

                consider t0x be Element of RAT+ such that

                 A53: (x + t0x) = t0 or (t0 + t0x) = x by ARYTM_3: 92;

                (x *' (two *' t0)) = ((s *' s) *' one ) by A52, ARYTM_3: 52;

                then x <=' (s *' s) or (two *' t0) <=' one by ARYTM_3: 83;

                then

                 A54: x < t0 by A47, A51, ARYTM_3: 53, ARYTM_3: 69;

                then

                 A55: t0x <=' t0 by A53;

                

                 A56: (((x *' t0x) + (x *' t0)) + (x *' x)) = (((x *' t0x) + (x *' x)) + (x *' t0)) by ARYTM_3: 51

                .= ((x *' t0) + (x *' t0)) by A53, A54, ARYTM_3: 57

                .= (((x *' t0) *' one ) + (x *' t0)) by ARYTM_3: 53

                .= (((x *' t0) *' one ) + ((x *' t0) *' one )) by ARYTM_3: 53

                .= ((t0 *' x) *' two) by Lm13, ARYTM_3: 57

                .= (x *' (t0 *' two)) by ARYTM_3: 52

                .= ((s *' s) *' one ) by A52, ARYTM_3: 52

                .= (s *' s) by ARYTM_3: 53;

                es <=' (t0 *' t0) by A17, A18;

                then s < (t0 *' t0) by A43, ARYTM_3: 69;

                then

                 A57: (s *' s) < (t0 *' t0) by A50, ARYTM_3: 70;

                

                then ((t02s2 + (x *' x)) + (s *' s)) = ((t0 *' t0) + (x *' x)) by A48, ARYTM_3: 51

                .= (((t0x *' (t0x + x)) + (x *' t0)) + (x *' x)) by A53, A54, ARYTM_3: 57

                .= ((((t0x *' t0x) + (x *' t0x)) + (x *' t0)) + (x *' x)) by ARYTM_3: 57

                .= (((t0x *' t0x) + (x *' t0x)) + ((x *' t0) + (x *' x))) by ARYTM_3: 51

                .= ((t0x *' t0x) + ((x *' t0x) + ((x *' t0) + (x *' x)))) by ARYTM_3: 51

                .= ((t0x *' t0x) + (s *' s)) by A56, ARYTM_3: 51;

                then (t0x *' t0x) = (t02s2 + (x *' x)) by ARYTM_3: 62;

                then

                 A58: t02s2 <=' (t0x *' t0x);

                now

                  assume

                   A59: x = 0 ;

                  per cases by A59, ARYTM_3: 78;

                    suppose (s *' s) = 0 ;

                    hence contradiction by A49, ARYTM_3: 78;

                  end;

                    suppose T2t9 = 0 ;

                    hence contradiction by A52, ARYTM_3: 48;

                  end;

                end;

                then t0x <> t0 by A53, A54, ARYTM_3: 84;

                then t0x < t0 by A55, ARYTM_3: 68;

                then t0x in X by A14;

                then

                 A60: ex s st s = t0x & (s *' s) < two;

                (s *' s) < es by A50, A43, ARYTM_3: 70;

                then (two + (s *' s)) < (two + es) by ARYTM_3: 76;

                then two < t02s2 by A17, A18, A48, A57, ARYTM_3: 76;

                hence contradiction by A58, A60, ARYTM_3: 69;

              end;

            end;

            hence contradiction;

          end;

        end;

        then

         A61: (two / 1) = ((n *^ n) / (d *^ d)) by ARYTM_3: 40;

        d <> 0 by ARYTM_3: 35;

        then (d *^ d) <> {} by ORDINAL3: 31;

        

        then

         A62: (two *^ (d *^ d)) = (1 *^ (n *^ n)) by A61, ARYTM_3: 45, Lm11

        .= (n *^ n) by ORDINAL2: 39;

        then

        consider k be natural Ordinal such that

         A63: n = (2 *^ k) by Lm12;

        (two *^ (d *^ d)) = (2 *^ (k *^ (2 *^ k))) by A62, A63, ORDINAL3: 50;

        

        then (d *^ d) = (k *^ (2 *^ k)) by ORDINAL3: 33, Lm11

        .= (2 *^ (k *^ k)) by ORDINAL3: 50;

        then

         A64: ex p be natural Ordinal st d = (2 *^ p) by Lm12;

        (n,d) are_coprime by ARYTM_3: 34;

        hence contradiction by A63, A64;

      end;

      2 = ( succ 1);

      then 1 in 2 by ORDINAL1: 6;

      then

       A65: (1 *^ 2) in (2 *^ 2) by ORDINAL3: 19;

      

       A66: O9 <=' a9 by ARYTM_3: 64;

      now

        let r;

        assume

         A67: r in X;

        then

         A68: ex s st r = s & (s *' s) < two;

        thus for t st t <=' r holds t in X by A6, A67;

        per cases ;

          suppose

           A69: r = 0 ;

          take a9;

          thus a9 in X by A4, A3;

          thus r < a9 by A66, A69, ARYTM_3: 68;

        end;

          suppose

           A70: r <> 0 ;

          then

          consider T3r9 be Element of RAT+ such that

           A71: (((r + r) + r) *' T3r9) = one by ARYTM_3: 54, ARYTM_3: 63;

          consider rr be Element of RAT+ such that

           A72: ((r *' r) + rr) = two or (two + rr) = (r *' r) by ARYTM_3: 92;

          set eps = (rr *' T3r9);

           A73:

          now

            assume

             A74: eps = 0 ;

            per cases by A74, ARYTM_3: 78;

              suppose rr = O9;

              then (r *' r) = two by A72, ARYTM_3: 50;

              hence contradiction by A68;

            end;

              suppose T3r9 = O9;

              hence contradiction by A71, ARYTM_3: 48;

            end;

          end;

          now

            per cases ;

              suppose eps < r;

              then (eps *' eps) < (r *' eps) by A73, ARYTM_3: 80;

              then

               A75: (((r *' eps) + (eps *' r)) + (eps *' eps)) < (((r *' eps) + (eps *' r)) + (r *' eps)) by ARYTM_3: 76;

              take t = (r + eps);

              

               A76: (t *' t) = ((r *' t) + (eps *' t)) by ARYTM_3: 57

              .= (((r *' r) + (r *' eps)) + (eps *' t)) by ARYTM_3: 57

              .= (((r *' r) + (r *' eps)) + ((eps *' r) + (eps *' eps))) by ARYTM_3: 57

              .= ((r *' r) + ((r *' eps) + ((eps *' r) + (eps *' eps)))) by ARYTM_3: 51

              .= ((r *' r) + (((r *' eps) + (eps *' r)) + (eps *' eps))) by ARYTM_3: 51;

              (((r *' eps) + (eps *' r)) + (r *' eps)) = ((eps *' (r + r)) + (r *' eps)) by ARYTM_3: 57

              .= (eps *' ((r + r) + r)) by ARYTM_3: 57

              .= (rr *' one ) by A71, ARYTM_3: 52

              .= rr by ARYTM_3: 53;

              then (t *' t) < two by A68, A72, A75, A76, ARYTM_3: 76;

              hence t in X;

              O9 <=' eps by ARYTM_3: 64;

              then O9 < eps by A73, ARYTM_3: 68;

              then (r + O9) < (r + eps) by ARYTM_3: 76;

              hence r < t by ARYTM_3: 50;

            end;

              suppose

               A77: r <=' eps;

              (eps *' ((r + r) + r)) = (rr *' one ) by A71, ARYTM_3: 52

              .= rr by ARYTM_3: 53;

              then

               A78: (r *' ((r + r) + r)) <=' rr by A77, ARYTM_3: 82;

              take t = ((a9 + half) *' r);

              a9 < (two *' one ) by A3, ARYTM_3: 53;

              then half < one by A10, ARYTM_3: 82;

              then ( one + half) < two by Lm13, ARYTM_3: 76;

              then

               A79: t < (two *' r) by A70, ARYTM_3: 80;

              then

               A80: ((two *' r) *' t) < ((two *' r) *' (two *' r)) by A70, ARYTM_3: 78, ARYTM_3: 80;

              (a9 + half) <> 0 by ARYTM_3: 63;

              then (t *' t) < ((two *' r) *' t) by A70, A79, ARYTM_3: 78, ARYTM_3: 80;

              then

               A81: (t *' t) < ((two *' r) *' (two *' r)) by A80, ARYTM_3: 70;

              ((r *' ((r + r) + r)) + (r *' r)) = (((r *' (r + r)) + (r *' r)) + (r *' r)) by ARYTM_3: 57

              .= ((r *' (r + r)) + ((r *' r) + (r *' r))) by ARYTM_3: 51

              .= ((r *' (two *' r)) + ((r *' r) + (r *' r))) by Lm14

              .= ((r *' (two *' r)) + (two *' (r *' r))) by Lm14

              .= ((two *' (r *' r)) + (two *' (r *' r))) by ARYTM_3: 52

              .= (two *' (two *' (r *' r))) by Lm14

              .= (two *' ((two *' r) *' r)) by ARYTM_3: 52

              .= ((two *' r) *' (two *' r)) by ARYTM_3: 52;

              then ((two *' r) *' (two *' r)) <=' two by A68, A72, A78, ARYTM_3: 76;

              then (t *' t) < two by A81, ARYTM_3: 69;

              hence t in X;

              O9 <> half & O9 <=' half by A10, ARYTM_3: 48, ARYTM_3: 64;

              then O9 < half by ARYTM_3: 68;

              then ( one + O9) < ( one + half) by ARYTM_3: 76;

              then one < ( one + half) by ARYTM_3: 50;

              then ( one *' r) < t by A70, ARYTM_3: 80;

              hence r < t by ARYTM_3: 53;

            end;

          end;

          hence ex t st t in X & r < t;

        end;

      end;

      then

       A82: X in DD;

      (a9 *' half) = half by ARYTM_3: 53;

      then

       A83: half in X by A10, A6, A2, A5, ARYTM_3: 82;

       A84:

      now

        assume

         A85: X in RAT ;

        per cases by A85, XBOOLE_0:def 3;

          suppose

           A86: X in RAT+ ;

          now

            per cases by A86, XBOOLE_0:def 3;

              suppose X in ({ [i, j] : (i,j) are_coprime & j <> {} } \ the set of all [k, one ]);

              then X in { [i, j] : (i,j) are_coprime & j <> {} };

              then ex i, j st X = [i, j] & (i,j) are_coprime & j <> {} ;

              hence contradiction by A8, TARSKI:def 2;

            end;

              suppose

               A87: X in omega ;

              2 c= X by A5, A8, Lm11, ZFMISC_1: 32;

              then

               A88: not X in 2 by ORDINAL1: 5;

              now

                per cases by A87, A88, ORDINAL1: 14;

                  suppose X = two;

                  then half = 0 or half = 1 by A83, Lm11, TARSKI:def 2;

                  hence contradiction by A10, ARYTM_3: 48, ARYTM_3: 53;

                end;

                  suppose two in X;

                  then ex s st s = two & (s *' s) < two;

                  hence contradiction by A1, A65, Lm9;

                end;

              end;

              hence contradiction;

            end;

          end;

          hence contradiction;

        end;

          suppose X in [: { 0 }, RAT+ :];

          then ex x,y be object st X = [x, y] by RELAT_1:def 1;

          hence contradiction by A8, TARSKI:def 2;

        end;

      end;

      now

        assume two in X;

        then ex s st two = s & (s *' s) < two;

        hence contradiction by A1, A65, Lm9;

      end;

      then X <> RAT+ ;

      then not X in { RAT+ } by TARSKI:def 1;

      then X in DEDEKIND_CUTS by A82, ARYTM_2:def 1, XBOOLE_0:def 5;

      then X in ( RAT+ \/ DEDEKIND_CUTS ) by XBOOLE_0:def 3;

      then X in REAL+ by A13, ARYTM_2:def 2, XBOOLE_0:def 5;

      then X in ( REAL+ \/ [: { 0 }, REAL+ :]) by XBOOLE_0:def 3;

      then X in REAL by A9, XBOOLE_0:def 5;

      hence thesis by A84, Lm8;

    end;

    theorem :: NUMBERS:3

    

     Th3: RAT c< COMPLEX by Th1, Th2, XBOOLE_1: 56;

    

     Lm15: INT c= RAT

    proof

       [: { 0 }, NAT :] c= [: { 0 }, RAT+ :] by Lm1, ZFMISC_1: 95;

      then ( NAT \/ [: { 0 }, NAT :]) c= ( RAT+ \/ [: { 0 }, RAT+ :]) by Lm1, XBOOLE_1: 13;

      hence thesis by XBOOLE_1: 33;

    end;

    theorem :: NUMBERS:4

    

     Th4: INT c< RAT

    proof

      (1,2) are_coprime by ORDINAL3: 37;

      then

       A1: [1, 2] in RAT+ by ARYTM_3: 33, Lm11;

       not 1 in { 0 } by TARSKI:def 1;

      then ( not [1, 2] in NAT ) & not [1, 2] in [: { 0 }, NAT :] by ARYTM_3: 32, ZFMISC_1: 87;

      then not [1, 2] in ( NAT \/ [: { 0 }, NAT :]) by XBOOLE_0:def 3;

      then INT <> RAT by A1, Lm4, XBOOLE_0:def 5;

      hence thesis by Lm15;

    end;

    theorem :: NUMBERS:5

    

     Th5: INT c< REAL by Th2, Th4, XBOOLE_1: 56;

    theorem :: NUMBERS:6

    

     Th6: INT c< COMPLEX by Th1, Th5, XBOOLE_1: 56;

    theorem :: NUMBERS:7

    

     Th7: NAT c< INT

    proof

       0 in { 0 } by TARSKI:def 1;

      then [ 0 , 1] in [: { 0 }, NAT :] by ZFMISC_1: 87;

      then

       A1: [ 0 , 1] in ( NAT \/ [: { 0 }, NAT :]) by XBOOLE_0:def 3;

      

       A2: not [ 0 , 1] in NAT by ARYTM_3: 32;

       [ 0 , 1] <> [ 0 , 0 ] by XTUPLE_0: 1;

      then not [ 0 , 1] in { [ 0 , 0 ]} by TARSKI:def 1;

      then [ 0 , 1] in INT by A1, XBOOLE_0:def 5;

      hence thesis by A2, Lm5;

    end;

    theorem :: NUMBERS:8

    

     Th8: NAT c< RAT by Th4, Th7, XBOOLE_1: 56;

    theorem :: NUMBERS:9

    

     Th9: NAT c< REAL by Th2, Th8, XBOOLE_1: 56;

    theorem :: NUMBERS:10

    

     Th10: NAT c< COMPLEX by Th1, Th9, XBOOLE_1: 56;

    begin

    theorem :: NUMBERS:11

     REAL c= COMPLEX by Th1;

    theorem :: NUMBERS:12

     RAT c= REAL by Th2;

    theorem :: NUMBERS:13

     RAT c= COMPLEX by Th3;

    theorem :: NUMBERS:14

     INT c= RAT by Th4;

    theorem :: NUMBERS:15

     INT c= REAL by Th5;

    theorem :: NUMBERS:16

     INT c= COMPLEX by Th6;

    theorem :: NUMBERS:17

     NAT c= INT by Lm5;

    theorem :: NUMBERS:18

    

     Th18: NAT c= RAT by Th8;

    theorem :: NUMBERS:19

    

     Th19: NAT c= REAL by Th9;

    theorem :: NUMBERS:20

    

     Th20: NAT c= COMPLEX by Th10;

    theorem :: NUMBERS:21

     REAL <> COMPLEX by Th1;

    theorem :: NUMBERS:22

     RAT <> REAL by Th2;

    theorem :: NUMBERS:23

     RAT <> COMPLEX by Th1, Th2;

    theorem :: NUMBERS:24

     INT <> RAT by Th4;

    theorem :: NUMBERS:25

     INT <> REAL by Th2, Th4;

    theorem :: NUMBERS:26

     INT <> COMPLEX by Th1, Th2, Th4, XBOOLE_1: 56;

    theorem :: NUMBERS:27

     NAT <> INT by Th7;

    theorem :: NUMBERS:28

     NAT <> RAT by Th4, Th7;

    theorem :: NUMBERS:29

     NAT <> REAL by Th2, Th4, Th7, XBOOLE_1: 56;

    theorem :: NUMBERS:30

     NAT <> COMPLEX by Th1, Th2, Th8, XBOOLE_1: 56;

    definition

      :: NUMBERS:def5

      func ExtREAL -> set equals ( REAL \/ { REAL , [ 0 , REAL ]});

      coherence ;

    end

    registration

      cluster ExtREAL -> non empty;

      coherence ;

    end

    theorem :: NUMBERS:31

    

     Th31: REAL c= ExtREAL by XBOOLE_1: 7;

    theorem :: NUMBERS:32

    

     Th32: REAL <> ExtREAL

    proof

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

      then REAL in ExtREAL by XBOOLE_0:def 3;

      hence thesis;

    end;

    theorem :: NUMBERS:33

     REAL c< ExtREAL by Th31, Th32;

    registration

      cluster INT -> infinite;

      coherence by Lm5, FINSET_1: 1;

      cluster RAT -> infinite;

      coherence by Th18, FINSET_1: 1;

      cluster REAL -> infinite;

      coherence by Th19, FINSET_1: 1;

      cluster COMPLEX -> infinite;

      coherence by Th20, FINSET_1: 1;

    end