:: NUMBERS semantic presentation
begin
Lm1: omega c= ( { [c,d] where c, d is Element of omega : ( c,d are_relative_prime & d <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega
by XBOOLE_1:7;
notation
synonym NAT for omega ;
synonym 0 for {} ;
end;
Lm2: 1 = succ 0
;
definition
func REAL -> set equals :: NUMBERS:def 1
(REAL+ \/ [:{0},REAL+:]) \ {[0,0]};
coherence
(REAL+ \/ [:{0},REAL+:]) \ {[0,0]} is set ;
end;
:: deftheorem defines REAL NUMBERS:def_1_:_
REAL = (REAL+ \/ [:{0},REAL+:]) \ {[0,0]};
Lm3: REAL+ c= REAL
proof
REAL+ c= REAL+ \/ [:{0},REAL+:] by XBOOLE_1:7;
hence REAL+ c= REAL by ARYTM_2:3, ZFMISC_1:34; ::_thesis: verum
end;
registration
cluster REAL -> non empty ;
coherence
not REAL is empty by Lm3, XBOOLE_1:3;
end;
definition
func COMPLEX -> set equals :: NUMBERS:def 2
((Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ) \/ REAL;
coherence
((Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ) \/ REAL is set ;
func RAT -> set equals :: NUMBERS:def 3
(RAT+ \/ [:{0},RAT+:]) \ {[0,0]};
coherence
(RAT+ \/ [:{0},RAT+:]) \ {[0,0]} is set ;
func INT -> set equals :: NUMBERS:def 4
(NAT \/ [:{0},NAT:]) \ {[0,0]};
coherence
(NAT \/ [:{0},NAT:]) \ {[0,0]} is set ;
:: original: NAT
redefine func NAT -> Subset of REAL;
coherence
NAT is Subset of REAL by Lm3, ARYTM_2:2, XBOOLE_1:1;
end;
:: deftheorem defines COMPLEX NUMBERS:def_2_:_
COMPLEX = ((Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ) \/ REAL;
:: deftheorem defines RAT NUMBERS:def_3_:_
RAT = (RAT+ \/ [:{0},RAT+:]) \ {[0,0]};
:: deftheorem defines INT NUMBERS:def_4_:_
INT = (NAT \/ [:{0},NAT:]) \ {[0,0]};
Lm4: RAT+ c= RAT
proof
RAT+ c= RAT+ \/ [:{0},RAT+:] by XBOOLE_1:7;
hence RAT+ c= RAT by ARYTM_3:61, ZFMISC_1:34; ::_thesis: verum
end;
Lm5: NAT c= INT
proof
NAT c= NAT \/ [:{0},NAT:] by XBOOLE_1:7;
hence NAT c= INT by ARYTM_3:32, ZFMISC_1:34; ::_thesis: verum
end;
registration
cluster COMPLEX -> non empty ;
coherence
not COMPLEX is empty ;
cluster RAT -> non empty ;
coherence
not RAT is empty by Lm4, XBOOLE_1:3;
cluster INT -> non empty ;
coherence
not INT is empty by Lm5, XBOOLE_1:3;
end;
Lm6: for x, y, z being set st [x,y] = {z} holds
( z = {x} & x = y )
proof
let x, y, z be set ; ::_thesis: ( [x,y] = {z} implies ( z = {x} & x = y ) )
assume A1: [x,y] = {z} ; ::_thesis: ( z = {x} & x = y )
then {x} in {z} by TARSKI:def_2;
hence A2: z = {x} by TARSKI:def_1; ::_thesis: x = y
{x,y} in {z} by A1, TARSKI:def_2;
then {x,y} = z by TARSKI:def_1;
hence x = y by A2, ZFMISC_1:5; ::_thesis: verum
end;
Lm7: for a, b being Element of REAL holds not (0,one) --> (a,b) in REAL
proof
let a, b be Element of REAL ; ::_thesis: not (0,one) --> (a,b) in REAL
set IR = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
set f = (0,one) --> (a,b);
A1: now__::_thesis:_not_(0,one)_-->_(a,b)_in_[:{{}},REAL+:]
(0,one) --> (a,b) = {[0,a],[one,b]} by FUNCT_4:67;
then A2: [one,b] in (0,one) --> (a,b) by TARSKI:def_2;
assume (0,one) --> (a,b) in [:{{}},REAL+:] ; ::_thesis: contradiction
then consider x, y being set such that
A3: x in {{}} and
y in REAL+ and
A4: (0,one) --> (a,b) = [x,y] by ZFMISC_1:84;
A5: x = 0 by A3, TARSKI:def_1;
percases ( {{one,b},{one}} = {0} or {{one,b},{one}} = {0,y} ) by A4, A5, A2, TARSKI:def_2;
suppose {{one,b},{one}} = {0} ; ::_thesis: contradiction
then 0 in {{one,b},{one}} by TARSKI:def_1;
hence contradiction by TARSKI:def_2; ::_thesis: verum
end;
suppose {{one,b},{one}} = {0,y} ; ::_thesis: contradiction
then 0 in {{one,b},{one}} by TARSKI:def_2;
hence contradiction by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
A6: (0,one) --> (a,b) = {[0,a],[one,b]} by FUNCT_4:67;
now__::_thesis:_not_(0,one)_-->_(a,b)_in__{__[i,j]_where_i,_j_is_Element_of_NAT_:_(_i,j_are_relative_prime_&_j_<>_{}_)__}_
assume (0,one) --> (a,b) in { [i,j] where i, j is Element of NAT : ( i,j are_relative_prime & j <> {} ) } ; ::_thesis: contradiction
then consider i, j being Element of NAT such that
A7: (0,one) --> (a,b) = [i,j] and
i,j are_relative_prime and
j <> {} ;
A8: ( {i} in (0,one) --> (a,b) & {i,j} in (0,one) --> (a,b) ) by A7, TARSKI:def_2;
A9: now__::_thesis:_not_i_=_j
assume i = j ; ::_thesis: contradiction
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; ::_thesis: verum
end;
percases ( ( {i,j} = [0,a] & {i} = [0,a] ) or ( {i,j} = [0,a] & {i} = [one,b] ) or ( {i,j} = [one,b] & {i} = [0,a] ) or ( {i,j} = [one,b] & {i} = [one,b] ) ) by A6, A8, TARSKI:def_2;
suppose ( {i,j} = [0,a] & {i} = [0,a] ) ; ::_thesis: contradiction
hence contradiction by A9, ZFMISC_1:5; ::_thesis: verum
end;
supposethat A12: {i,j} = [0,a] and
A13: {i} = [one,b] ; ::_thesis: contradiction
i in [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; ::_thesis: verum
end;
supposethat A15: {i,j} = [one,b] and
A16: {i} = [0,a] ; ::_thesis: contradiction
i in [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; ::_thesis: verum
end;
suppose ( {i,j} = [one,b] & {i} = [one,b] ) ; ::_thesis: contradiction
hence contradiction by A9, ZFMISC_1:5; ::_thesis: verum
end;
end;
end;
then A18: not (0,one) --> (a,b) in { [i,j] where i, j is Element of NAT : ( i,j are_relative_prime & j <> {} ) } \ { [k,one] where k is Element of NAT : verum } ;
for x, y being set holds not {[0,x],[one,y]} in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
proof
given x, y being set such that A19: {[0,x],[one,y]} in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ; ::_thesis: contradiction
consider A being Subset of RAT+ such that
A20: {[0,x],[one,y]} = A and
A21: for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) by A19;
( [0,x] in A & ( for r, s being Element of RAT+ st r in A & s <=' r holds
s in A ) ) by A20, A21, TARSKI:def_2;
then consider r1, r2, r3 being 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; ::_thesis: verum
end;
then A26: not (0,one) --> (a,b) in DEDEKIND_CUTS by A6, ARYTM_2:def_1;
now__::_thesis:_not_(0,one)_-->_(a,b)_in_omega
assume (0,one) --> (a,b) in omega ; ::_thesis: contradiction
then {} in (0,one) --> (a,b) by ORDINAL3:8;
hence contradiction by A6, TARSKI:def_2; ::_thesis: verum
end;
then not (0,one) --> (a,b) in RAT+ by A18, XBOOLE_0:def_3;
then not (0,one) --> (a,b) in REAL+ by A26, ARYTM_2:def_2, XBOOLE_0:def_3;
hence not (0,one) --> (a,b) in REAL by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
definition
:: original: 0
redefine func 0 -> Element of NAT ;
coherence
0 is Element of NAT by ORDINAL1:def_11;
end;
theorem Th1: :: NUMBERS:1
REAL c< COMPLEX
proof
set X = { x where x is Element of Funcs ({0,one},REAL) : x . one = 0 } ;
thus REAL c= COMPLEX by XBOOLE_1:7; :: according to XBOOLE_0:def_8 ::_thesis: not REAL = COMPLEX
A1: now__::_thesis:_not_(0,1)_-->_(0,1)_in__{__x_where_x_is_Element_of_Funcs_({0,one},REAL)_:_x_._one_=_0__}_
assume (0,1) --> (0,1) in { x where x is Element of Funcs ({0,one},REAL) : x . one = 0 } ; ::_thesis: contradiction
then ex x being Element of Funcs ({0,one},REAL) st
( x = (0,1) --> (0,1) & x . one = 0 ) ;
hence contradiction by FUNCT_4:63; ::_thesis: verum
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, XBOOLE_1:1;
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 where x is Element of Funcs ({0,one},REAL) : x . one = 0 } by A1, XBOOLE_0:def_5;
hence not REAL = COMPLEX by A3, XBOOLE_0:def_3; ::_thesis: verum
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 RAT c= REAL by XBOOLE_1:33; ::_thesis: verum
end;
Lm9: for i, j being ordinal Element of RAT+ st i in j holds
i < j
proof
let i, j be ordinal Element of RAT+ ; ::_thesis: ( i in j implies i < j )
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 ; ::_thesis: i < j
then x <=' y by A1, ARYTM_2:18;
then A3: ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x9 <=' y9 ) by ARYTM_2:def_5;
i <> j by A2;
hence i < j by A3, ARYTM_3:66; ::_thesis: verum
end;
Lm10: for i, j being ordinal Element of RAT+ st i c= j holds
i <=' j
proof
let i, j be ordinal Element of RAT+ ; ::_thesis: ( i c= j implies i <=' j )
assume i c= j ; ::_thesis: i <=' j
then consider C being ordinal number such that
A1: j = i +^ C by ORDINAL3:27;
C in omega by A1, ORDINAL3:74;
then reconsider C = C as Element of RAT+ by Lm1;
j = i + C by A1, ARYTM_3:58;
hence i <=' j by ARYTM_3:def_13; ::_thesis: verum
end;
Lm11: 2 = succ 1
.= (succ 0) \/ {1} by ORDINAL1:def_1
.= (0 \/ {0}) \/ {1} by ORDINAL1:def_1
.= {0,1} by ENUMSET1:1 ;
Lm12: for i, k being natural Ordinal st i *^ i = 2 *^ k holds
ex k being natural Ordinal st i = 2 *^ k
proof
let i, k be natural Ordinal; ::_thesis: ( i *^ i = 2 *^ k implies ex k being natural Ordinal st i = 2 *^ k )
assume A1: i *^ i = 2 *^ k ; ::_thesis: ex k being natural Ordinal st i = 2 *^ k
set id2 = i div^ 2;
{} in 2 by ORDINAL1:14;
then A2: i mod^ 2 in 2 by ARYTM_3:6;
percases ( i mod^ 2 = 0 or i mod^ 2 = 1 ) by A2, Lm11, TARSKI:def_2;
supposeA3: i mod^ 2 = 0 ; ::_thesis: ex k being natural Ordinal st i = 2 *^ k
take k = i div^ 2; ::_thesis: i = 2 *^ k
thus i = (k *^ 2) +^ 0 by A3, ORDINAL3:65
.= 2 *^ k by ORDINAL2:27 ; ::_thesis: verum
end;
suppose i mod^ 2 = 1 ; ::_thesis: ex k being natural Ordinal st i = 2 *^ k
then i = ((i div^ 2) *^ 2) +^ 1 by ORDINAL3:65;
then A4: i *^ i = (((i div^ 2) *^ 2) *^ (((i div^ 2) *^ 2) +^ 1)) +^ (one *^ (((i div^ 2) *^ 2) +^ 1)) by ORDINAL3:46
.= (((i div^ 2) *^ 2) *^ (((i div^ 2) *^ 2) +^ 1)) +^ ((one *^ ((i div^ 2) *^ 2)) +^ (one *^ 1)) by ORDINAL3:46
.= (((i div^ 2) *^ 2) *^ (((i div^ 2) *^ 2) +^ 1)) +^ ((one *^ ((i div^ 2) *^ 2)) +^ 1) by ORDINAL2:39
.= ((((i div^ 2) *^ 2) *^ (((i div^ 2) *^ 2) +^ 1)) +^ (one *^ ((i div^ 2) *^ 2))) +^ 1 by ORDINAL3:30
.= (((i div^ 2) *^ 2) *^ ((((i div^ 2) *^ 2) +^ 1) +^ one)) +^ 1 by ORDINAL3:46
.= (((i div^ 2) *^ ((((i div^ 2) *^ 2) +^ 1) +^ one)) *^ 2) +^ 1 by ORDINAL3:50 ;
A5: 1 divides 2 by ARYTM_3:9;
( 2 divides ((i div^ 2) *^ ((((i div^ 2) *^ 2) +^ 1) +^ one)) *^ 2 & 2 divides i *^ i ) by A1, ARYTM_3:def_3;
then 2 divides 1 by A4, ARYTM_3:11;
hence ex k being natural Ordinal st i = 2 *^ k by A5, ARYTM_3:8; ::_thesis: verum
end;
end;
end;
1 in omega
;
then reconsider a9 = 1 as Element of RAT+ by Lm1;
2 in omega
;
then reconsider two = 2 as ordinal Element of RAT+ by Lm1;
Lm13: one + one = two
proof
1 +^ 1 = succ (1 +^ {}) by Lm2, ORDINAL2:28
.= succ 1 by ORDINAL2:27
.= two ;
hence one + one = two by ARYTM_3:58; ::_thesis: verum
end;
Lm14: for i being Element of RAT+ holds i + i = two *' i
proof
let i be Element of RAT+ ; ::_thesis: i + i = two *' i
thus i + i = (one *' i) + i by ARYTM_3:53
.= (one *' i) + (one *' i) by ARYTM_3:53
.= two *' i by Lm13, ARYTM_3:57 ; ::_thesis: verum
end;
theorem Th2: :: NUMBERS:2
RAT c< REAL
proof
defpred S1[ Element of RAT+ ] means $1 *' $1 < two;
set X = { s where s is Element of RAT+ : S1[s] } ;
reconsider X = { s where s is Element of RAT+ : S1[s] } 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} by ORDINAL1:def_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 being Element of RAT+ st r in X & t <=' r holds
t in X
proof
let r, t be Element of RAT+ ; ::_thesis: ( r in X & t <=' r implies t in X )
assume r in X ; ::_thesis: ( not t <=' r or t in X )
then A7: ex s being Element of RAT+ st
( r = s & s *' s < two ) ;
assume t <=' r ; ::_thesis: t in X
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 t in X ; ::_thesis: verum
end;
then A8: 0 in X by A5, ARYTM_3:64;
now__::_thesis:_not_X_=_[0,0]
assume X = [0,0] ; ::_thesis: contradiction
then X = {{0},{0}} by ENUMSET1:29
.= {{0}} by ENUMSET1:29 ;
hence contradiction by A8, TARSKI:def_1; ::_thesis: verum
end;
then A9: not X in {[0,0]} by TARSKI:def_1;
reconsider 09 = 0 as Element of RAT+ by Lm1;
set DD = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
consider half being Element of RAT+ such that
A10: a9 = two *' half by ARYTM_3:55;
A11: one <=' two by Lm13, ARYTM_3:def_13;
then A12: one < two by ARYTM_3:68;
A13: now__::_thesis:_not_X_in__{___{__s_where_s_is_Element_of_RAT+_:_s_<_t__}__where_t_is_Element_of_RAT+_:_t_<>_0__}_
assume X in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> 0 } ; ::_thesis: contradiction
then consider t0 being Element of RAT+ such that
A14: X = { s where s is Element of RAT+ : s < t0 } and
A15: t0 <> 0 ;
set n = numerator t0;
set d = denominator t0;
now__::_thesis:_not_t0_*'_t0_<>_two
assume A16: t0 *' t0 <> two ; ::_thesis: contradiction
percases ( t0 *' t0 < two or two < t0 *' t0 ) by A16, ARYTM_3:66;
suppose t0 *' t0 < two ; ::_thesis: contradiction
then t0 in X ;
then ex s being Element of RAT+ st
( s = t0 & s < t0 ) by A14;
hence contradiction ; ::_thesis: verum
end;
supposeA17: two < t0 *' t0 ; ::_thesis: contradiction
consider es being Element of RAT+ such that
A18: ( two + es = t0 *' t0 or (t0 *' t0) + es = two ) by ARYTM_3:92;
A19: now__::_thesis:_not_09_=_es
assume 09 = es ; ::_thesis: contradiction
then two + es = two by ARYTM_3:50;
hence contradiction by A17, A18, ARYTM_3:def_13; ::_thesis: verum
end;
09 <=' es by ARYTM_3:64;
then 09 < es by A19, ARYTM_3:68;
then consider s being Element of RAT+ such that
A20: 09 < s and
A21: s < es by ARYTM_3:93;
now__::_thesis:_contradiction
percases ( s < one or one <=' s ) ;
supposeA22: s < one ; ::_thesis: contradiction
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__::_thesis:_not_t0_<='_one
assume A26: t0 <=' one ; ::_thesis: contradiction
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; ::_thesis: verum
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 being 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 2t9 being Element of RAT+ such that
A31: (two *' t0) *' 2t9 = one by A15, ARYTM_3:55, ARYTM_3:78;
set x = (s *' s) *' 2t9;
consider t0x being Element of RAT+ such that
A32: ( ((s *' s) *' 2t9) + t0x = t0 or t0 + t0x = (s *' s) *' 2t9 ) by ARYTM_3:92;
((s *' s) *' 2t9) *' (two *' t0) = (s *' s) *' one by A31, ARYTM_3:52;
then ( (s *' s) *' 2t9 <=' s *' s or two *' t0 <=' one ) by ARYTM_3:83;
then A33: (s *' s) *' 2t9 < t0 by A28, A30, ARYTM_3:53, ARYTM_3:69;
then A34: t0x <=' t0 by A32, ARYTM_3:def_13;
A35: ((((s *' s) *' 2t9) *' t0x) + (((s *' s) *' 2t9) *' t0)) + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9)) = ((((s *' s) *' 2t9) *' t0x) + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9))) + (((s *' s) *' 2t9) *' t0) by ARYTM_3:51
.= (((s *' s) *' 2t9) *' t0) + (((s *' s) *' 2t9) *' t0) by A32, A33, ARYTM_3:57, ARYTM_3:def_13
.= ((((s *' s) *' 2t9) *' t0) *' one) + (((s *' s) *' 2t9) *' t0) by ARYTM_3:53
.= ((((s *' s) *' 2t9) *' t0) *' one) + ((((s *' s) *' 2t9) *' t0) *' one) by ARYTM_3:53
.= (t0 *' ((s *' s) *' 2t9)) *' two by Lm13, ARYTM_3:57
.= ((s *' s) *' 2t9) *' (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, ARYTM_3:def_13;
then s < t0 *' t0 by A21, ARYTM_3:69;
then A36: s *' s < t0 *' t0 by A24, ARYTM_3:70;
then (t02s2 + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9))) + (s *' s) = ((t0x + ((s *' s) *' 2t9)) *' t0) + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9)) by A29, A32, A33, ARYTM_3:51, ARYTM_3:def_13
.= ((t0x *' (t0x + ((s *' s) *' 2t9))) + (((s *' s) *' 2t9) *' t0)) + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9)) by A32, A33, ARYTM_3:57, ARYTM_3:def_13
.= (((t0x *' t0x) + (((s *' s) *' 2t9) *' t0x)) + (((s *' s) *' 2t9) *' t0)) + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9)) by ARYTM_3:57
.= ((t0x *' t0x) + (((s *' s) *' 2t9) *' t0x)) + ((((s *' s) *' 2t9) *' t0) + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9))) by ARYTM_3:51
.= (t0x *' t0x) + ((((s *' s) *' 2t9) *' t0x) + ((((s *' s) *' 2t9) *' t0) + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9)))) by ARYTM_3:51
.= (t0x *' t0x) + (s *' s) by A35, ARYTM_3:51 ;
then t0x *' t0x = t02s2 + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9)) by ARYTM_3:62;
then A37: t02s2 <=' t0x *' t0x by ARYTM_3:def_13;
now__::_thesis:_not_(s_*'_s)_*'_2t9_=_0
assume A38: (s *' s) *' 2t9 = 0 ; ::_thesis: contradiction
percases ( s *' s = 0 or 2t9 = 0 ) by A38, ARYTM_3:78;
suppose s *' s = 0 ; ::_thesis: contradiction
hence contradiction by A23, ARYTM_3:78; ::_thesis: verum
end;
suppose 2t9 = 0 ; ::_thesis: contradiction
hence contradiction by A31, ARYTM_3:48; ::_thesis: verum
end;
end;
end;
then t0x <> t0 by A32, A33, ARYTM_3:84, ARYTM_3:def_13;
then t0x < t0 by A34, ARYTM_3:68;
then t0x in X by A14;
then A39: ex s being Element of RAT+ 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, ARYTM_3:def_13;
hence contradiction by A37, A39, ARYTM_3:69; ::_thesis: verum
end;
supposeA40: one <=' s ; ::_thesis: contradiction
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, ARYTM_3:def_13;
then one < two by ARYTM_3:68;
then A44: one *' t0 < two *' t0 by A15, ARYTM_3:80;
A45: now__::_thesis:_not_t0_<='_one
assume A46: t0 <=' one ; ::_thesis: contradiction
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; ::_thesis: verum
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 being Element of RAT+ such that
A48: ( (half *' half) + t02s2 = t0 *' t0 or (t0 *' t0) + t02s2 = half *' half ) 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;
half < t0 by A42, A45, ARYTM_3:70;
then A51: half *' half < t0 by A50, ARYTM_3:70;
consider 2t9 being Element of RAT+ such that
A52: (two *' t0) *' 2t9 = one by A15, ARYTM_3:55, ARYTM_3:78;
set x = (half *' half) *' 2t9;
consider t0x being Element of RAT+ such that
A53: ( ((half *' half) *' 2t9) + t0x = t0 or t0 + t0x = (half *' half) *' 2t9 ) by ARYTM_3:92;
((half *' half) *' 2t9) *' (two *' t0) = (half *' half) *' one by A52, ARYTM_3:52;
then ( (half *' half) *' 2t9 <=' half *' half or two *' t0 <=' one ) by ARYTM_3:83;
then A54: (half *' half) *' 2t9 < t0 by A47, A51, ARYTM_3:53, ARYTM_3:69;
then A55: t0x <=' t0 by A53, ARYTM_3:def_13;
A56: ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' t0)) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) = ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' t0) by ARYTM_3:51
.= (((half *' half) *' 2t9) *' t0) + (((half *' half) *' 2t9) *' t0) by A53, A54, ARYTM_3:57, ARYTM_3:def_13
.= ((((half *' half) *' 2t9) *' t0) *' one) + (((half *' half) *' 2t9) *' t0) by ARYTM_3:53
.= ((((half *' half) *' 2t9) *' t0) *' one) + ((((half *' half) *' 2t9) *' t0) *' one) by ARYTM_3:53
.= (t0 *' ((half *' half) *' 2t9)) *' two by Lm13, ARYTM_3:57
.= ((half *' half) *' 2t9) *' (t0 *' two) by ARYTM_3:52
.= (half *' half) *' one by A52, ARYTM_3:52
.= half *' half by ARYTM_3:53 ;
es <=' t0 *' t0 by A17, A18, ARYTM_3:def_13;
then half < t0 *' t0 by A43, ARYTM_3:69;
then A57: half *' half < t0 *' t0 by A50, ARYTM_3:70;
then (t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) + (half *' half) = (t0 *' t0) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) by A48, ARYTM_3:51, ARYTM_3:def_13
.= ((t0x *' (t0x + ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' t0)) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) by A53, A54, ARYTM_3:57, ARYTM_3:def_13
.= (((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + (((half *' half) *' 2t9) *' t0)) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) by ARYTM_3:57
.= ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + ((((half *' half) *' 2t9) *' t0) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) by ARYTM_3:51
.= (t0x *' t0x) + ((((half *' half) *' 2t9) *' t0x) + ((((half *' half) *' 2t9) *' t0) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) by ARYTM_3:51
.= (t0x *' t0x) + (half *' half) by A56, ARYTM_3:51 ;
then t0x *' t0x = t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) by ARYTM_3:62;
then A58: t02s2 <=' t0x *' t0x by ARYTM_3:def_13;
now__::_thesis:_not_(half_*'_half)_*'_2t9_=_0
assume A59: (half *' half) *' 2t9 = 0 ; ::_thesis: contradiction
percases ( half *' half = 0 or 2t9 = 0 ) by A59, ARYTM_3:78;
suppose half *' half = 0 ; ::_thesis: contradiction
hence contradiction by A49, ARYTM_3:78; ::_thesis: verum
end;
suppose 2t9 = 0 ; ::_thesis: contradiction
hence contradiction by A52, ARYTM_3:48; ::_thesis: verum
end;
end;
end;
then t0x <> t0 by A53, A54, ARYTM_3:84, ARYTM_3:def_13;
then t0x < t0 by A55, ARYTM_3:68;
then t0x in X by A14;
then A60: ex s being Element of RAT+ st
( s = t0x & s *' s < two ) ;
half *' half < es by A50, A43, ARYTM_3:70;
then two + (half *' half) < two + es by ARYTM_3:76;
then two < t02s2 by A17, A18, A48, A57, ARYTM_3:76, ARYTM_3:def_13;
hence contradiction by A58, A60, ARYTM_3:69; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
end;
then A61: two / 1 = ((numerator t0) *^ (numerator t0)) / ((denominator t0) *^ (denominator t0)) by ARYTM_3:40;
denominator t0 <> 0 by ARYTM_3:35;
then (denominator t0) *^ (denominator t0) <> {} by ORDINAL3:31;
then A62: two *^ ((denominator t0) *^ (denominator t0)) = 1 *^ ((numerator t0) *^ (numerator t0)) by A61, ARYTM_3:45
.= (numerator t0) *^ (numerator t0) by ORDINAL2:39 ;
then consider k being natural Ordinal such that
A63: numerator t0 = 2 *^ k by Lm12;
two *^ ((denominator t0) *^ (denominator t0)) = 2 *^ (k *^ (2 *^ k)) by A62, A63, ORDINAL3:50;
then (denominator t0) *^ (denominator t0) = k *^ (2 *^ k) by ORDINAL3:33
.= 2 *^ (k *^ k) by ORDINAL3:50 ;
then A64: ex p being natural Ordinal st denominator t0 = 2 *^ p by Lm12;
numerator t0, denominator t0 are_relative_prime by ARYTM_3:34;
hence contradiction by A63, A64, ARYTM_3:def_2; ::_thesis: verum
end;
2 = succ 1 ;
then 1 in 2 by ORDINAL1:6;
then A65: 1 *^ 2 in 2 *^ 2 by ORDINAL3:19;
A66: 09 <=' a9 by ARYTM_3:64;
now__::_thesis:_for_r_being_Element_of_RAT+_st_r_in_X_holds_
(_(_for_t_being_Element_of_RAT+_st_t_<='_r_holds_
t_in_X_)_&_ex_a9_being_Element_of_RAT+_st_
(_a9_in_X_&_r_<_a9_)_)
let r be Element of RAT+ ; ::_thesis: ( r in X implies ( ( for t being Element of RAT+ st t <=' r holds
t in X ) & ex a9 being Element of RAT+ st
( b2 in X & a9 < b2 ) ) )
assume A67: r in X ; ::_thesis: ( ( for t being Element of RAT+ st t <=' r holds
t in X ) & ex a9 being Element of RAT+ st
( b2 in X & a9 < b2 ) )
then A68: ex s being Element of RAT+ st
( r = s & s *' s < two ) ;
thus for t being Element of RAT+ st t <=' r holds
t in X by A6, A67; ::_thesis: ex a9 being Element of RAT+ st
( b2 in X & a9 < b2 )
percases ( r = 0 or r <> 0 ) ;
supposeA69: r = 0 ; ::_thesis: ex a9 being Element of RAT+ st
( b2 in X & a9 < b2 )
take a9 = a9; ::_thesis: ( a9 in X & r < a9 )
thus a9 in X by A4, A3; ::_thesis: r < a9
thus r < a9 by A66, A69, ARYTM_3:68; ::_thesis: verum
end;
supposeA70: r <> 0 ; ::_thesis: ex t being Element of RAT+ st
( b2 in X & t < b2 )
then consider 3r9 being Element of RAT+ such that
A71: ((r + r) + r) *' 3r9 = one by ARYTM_3:54, ARYTM_3:63;
consider rr being Element of RAT+ such that
A72: ( (r *' r) + rr = two or two + rr = r *' r ) by ARYTM_3:92;
set eps = rr *' 3r9;
A73: now__::_thesis:_not_rr_*'_3r9_=_0
assume A74: rr *' 3r9 = 0 ; ::_thesis: contradiction
percases ( rr = 09 or 3r9 = 09 ) by A74, ARYTM_3:78;
suppose rr = 09 ; ::_thesis: contradiction
then r *' r = two by A72, ARYTM_3:50;
hence contradiction by A68; ::_thesis: verum
end;
suppose 3r9 = 09 ; ::_thesis: contradiction
hence contradiction by A71, ARYTM_3:48; ::_thesis: verum
end;
end;
end;
now__::_thesis:_ex_t_being_Element_of_RAT+_st_
(_t_in_X_&_r_<_t_)
percases ( rr *' 3r9 < r or r <=' rr *' 3r9 ) ;
suppose rr *' 3r9 < r ; ::_thesis: ex t being Element of RAT+ st
( t in X & r < t )
then (rr *' 3r9) *' (rr *' 3r9) < r *' (rr *' 3r9) by A73, ARYTM_3:80;
then A75: ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9)) < ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + (r *' (rr *' 3r9)) by ARYTM_3:76;
take t = r + (rr *' 3r9); ::_thesis: ( t in X & r < t )
A76: t *' t = (r *' t) + ((rr *' 3r9) *' t) by ARYTM_3:57
.= ((r *' r) + (r *' (rr *' 3r9))) + ((rr *' 3r9) *' t) by ARYTM_3:57
.= ((r *' r) + (r *' (rr *' 3r9))) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))) by ARYTM_3:57
.= (r *' r) + ((r *' (rr *' 3r9)) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) by ARYTM_3:51
.= (r *' r) + (((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9))) by ARYTM_3:51 ;
((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + (r *' (rr *' 3r9)) = ((rr *' 3r9) *' (r + r)) + (r *' (rr *' 3r9)) by ARYTM_3:57
.= (rr *' 3r9) *' ((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, ARYTM_3:def_13;
hence t in X ; ::_thesis: r < t
09 <=' rr *' 3r9 by ARYTM_3:64;
then 09 < rr *' 3r9 by A73, ARYTM_3:68;
then r + 09 < r + (rr *' 3r9) by ARYTM_3:76;
hence r < t by ARYTM_3:50; ::_thesis: verum
end;
supposeA77: r <=' rr *' 3r9 ; ::_thesis: ex t being Element of RAT+ st
( t in X & r < t )
(rr *' 3r9) *' ((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; ::_thesis: ( t in X & r < t )
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, ARYTM_3:def_13;
then t *' t < two by A81, ARYTM_3:69;
hence t in X ; ::_thesis: r < t
( 09 <> half & 09 <=' half ) by A10, ARYTM_3:48, ARYTM_3:64;
then 09 < half by ARYTM_3:68;
then one + 09 < 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; ::_thesis: verum
end;
end;
end;
hence ex t being Element of RAT+ st
( t in X & r < t ) ; ::_thesis: verum
end;
end;
end;
then A82: X in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
a9 *' half = half by ARYTM_3:53;
then A83: half in X by A10, A6, A2, A5, ARYTM_3:82;
A84: now__::_thesis:_not_X_in_RAT
assume A85: X in RAT ; ::_thesis: contradiction
percases ( X in RAT+ or X in [:{0},RAT+:] ) by A85, XBOOLE_0:def_3;
supposeA86: X in RAT+ ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( X in { [i,j] where i, j is Element of omega : ( i,j are_relative_prime & j <> {} ) } \ { [k,one] where k is Element of omega : verum } or X in omega ) by A86, XBOOLE_0:def_3;
suppose X in { [i,j] where i, j is Element of omega : ( i,j are_relative_prime & j <> {} ) } \ { [k,one] where k is Element of omega : verum } ; ::_thesis: contradiction
then X in { [i,j] where i, j is Element of omega : ( i,j are_relative_prime & j <> {} ) } ;
then ex i, j being Element of omega st
( X = [i,j] & i,j are_relative_prime & j <> {} ) ;
hence contradiction by A8, TARSKI:def_2; ::_thesis: verum
end;
supposeA87: X in omega ; ::_thesis: contradiction
2 c= X by A5, A8, Lm11, ZFMISC_1:32;
then A88: not X in 2 by ORDINAL1:5;
now__::_thesis:_contradiction
percases ( X = two or two in X ) by A87, A88, ORDINAL1:14;
suppose X = two ; ::_thesis: contradiction
then ( half = 0 or half = 1 ) by A83, Lm11, TARSKI:def_2;
hence contradiction by A10, ARYTM_3:48, ARYTM_3:53; ::_thesis: verum
end;
suppose two in X ; ::_thesis: contradiction
then ex s being Element of RAT+ st
( s = two & s *' s < two ) ;
hence contradiction by A1, A65, Lm9; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
suppose X in [:{0},RAT+:] ; ::_thesis: contradiction
then ex x, y being set st X = [x,y] by RELAT_1:def_1;
hence contradiction by A8, TARSKI:def_2; ::_thesis: verum
end;
end;
end;
now__::_thesis:_not_two_in_X
assume two in X ; ::_thesis: contradiction
then ex s being Element of RAT+ st
( two = s & s *' s < two ) ;
hence contradiction by A1, A65, Lm9; ::_thesis: verum
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 RAT c< REAL by A84, Lm8, XBOOLE_0:def_8; ::_thesis: verum
end;
theorem Th3: :: NUMBERS:3
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 INT c= RAT by XBOOLE_1:33; ::_thesis: verum
end;
theorem Th4: :: NUMBERS:4
INT c< RAT
proof
1,2 are_relative_prime
proof
let c, d1, d2 be Ordinal; :: according to ARYTM_3:def_2 ::_thesis: ( not 1 = c *^ d1 or not 2 = c *^ d2 or c = 1 )
assume that
A1: 1 = c *^ d1 and
2 = c *^ d2 ; ::_thesis: c = 1
thus c = 1 by A1, ORDINAL3:37; ::_thesis: verum
end;
then A2: [1,2] in RAT+ by ARYTM_3:33;
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 A2, Lm4, XBOOLE_0:def_5;
hence INT c< RAT by Lm15, XBOOLE_0:def_8; ::_thesis: verum
end;
theorem Th5: :: NUMBERS:5
INT c< REAL by Th2, Th4, XBOOLE_1:56;
theorem Th6: :: NUMBERS:6
INT c< COMPLEX by Th1, Th5, XBOOLE_1:56;
theorem Th7: :: NUMBERS:7
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 NAT c< INT by A2, Lm5, XBOOLE_0:def_8; ::_thesis: verum
end;
theorem Th8: :: NUMBERS:8
NAT c< RAT by Th4, Th7, XBOOLE_1:56;
theorem Th9: :: NUMBERS:9
NAT c< REAL by Th2, Th8, XBOOLE_1:56;
theorem Th10: :: NUMBERS:10
NAT c< COMPLEX by Th1, Th9, XBOOLE_1:56;
begin
theorem :: NUMBERS:11
REAL c= COMPLEX by Th1, XBOOLE_0:def_8;
theorem :: NUMBERS:12
RAT c= REAL by Th2, XBOOLE_0:def_8;
theorem :: NUMBERS:13
RAT c= COMPLEX by Th3, XBOOLE_0:def_8;
theorem :: NUMBERS:14
INT c= RAT by Th4, XBOOLE_0:def_8;
theorem :: NUMBERS:15
INT c= REAL by Th5, XBOOLE_0:def_8;
theorem :: NUMBERS:16
INT c= COMPLEX by Th6, XBOOLE_0:def_8;
theorem :: NUMBERS:17
NAT c= INT by Lm5;
theorem Th18: :: NUMBERS:18
NAT c= RAT by Th8, XBOOLE_0:def_8;
theorem Th19: :: NUMBERS:19
NAT c= REAL ;
theorem Th20: :: NUMBERS:20
NAT c= COMPLEX by Th10, XBOOLE_0:def_8;
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
func ExtREAL -> set equals :: NUMBERS:def 5
REAL \/ {REAL,[0,REAL]};
coherence
REAL \/ {REAL,[0,REAL]} is set ;
end;
:: deftheorem defines ExtREAL NUMBERS:def_5_:_
ExtREAL = REAL \/ {REAL,[0,REAL]};
registration
cluster ExtREAL -> non empty ;
coherence
not ExtREAL is empty ;
end;
theorem Th31: :: NUMBERS:31
REAL c= ExtREAL by XBOOLE_1:7;
theorem Th32: :: NUMBERS:32
REAL <> ExtREAL
proof
REAL in {REAL,[0,REAL]} by TARSKI:def_2;
then REAL in ExtREAL by XBOOLE_0:def_3;
hence REAL <> ExtREAL ; ::_thesis: verum
end;
theorem :: NUMBERS:33
REAL c< ExtREAL by Th31, Th32, XBOOLE_0:def_8;
registration
cluster INT -> infinite ;
coherence
not INT is finite by Lm5, FINSET_1:1;
cluster RAT -> infinite ;
coherence
not RAT is finite by Th18, FINSET_1:1;
cluster REAL -> infinite ;
coherence
not REAL is finite by Th19, FINSET_1:1;
cluster COMPLEX -> infinite ;
coherence
not COMPLEX is finite by Th20, FINSET_1:1;
end;