:: Subsets of Complex Numbers :: by Andrzej Trybulec :: :: Received November 7, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ORDINAL1, TARSKI, SUBSET_1, ARYTM_3, XBOOLE_0, CARD_1, ARYTM_2, ZFMISC_1, FUNCT_2, FUNCT_1, FUNCOP_1, RELAT_1, ORDINAL2, ORDINAL3, FINSET_1, NUMBERS; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, ORDINAL1, ORDINAL2, ORDINAL3, FINSET_1, ARYTM_3, ARYTM_2; constructors FUNCT_4, ORDINAL3, ARYTM_2, FINSET_1, XTUPLE_0; registrations XBOOLE_0, ORDINAL1, FUNCT_2, ARYTM_3, ARYTM_2, RELAT_1, ORDINAL2, ORDINAL3, CARD_1, XTUPLE_0; requirements BOOLE, SUBSET, NUMERALS; definitions TARSKI, ARYTM_3, XBOOLE_0; theorems XBOOLE_1, ARYTM_2, ZFMISC_1, ARYTM_3, XBOOLE_0, TARSKI, ORDINAL2, ORDINAL3, ENUMSET1, ORDINAL1, FUNCT_2, FUNCT_4, RELAT_1, FINSET_1, XTUPLE_0; schemes DOMAIN_1; 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: not contradiction}) \/ omega by XBOOLE_1:7; notation synonym NAT for omega; synonym 0 for {}; end; Lm2: 1 = succ 0; definition func REAL 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 func COMPLEX equals Funcs({0,1},REAL) \ { x where x is Element of Funcs({0,1 },REAL): x.1 = 0} \/ REAL; coherence; func RAT equals RAT+ \/ [:{0},RAT+:] \ {[0,0]}; coherence; func INT equals NAT \/ [:{0},NAT:] \ {[0,0]}; coherence; redefine func NAT -> Subset of REAL; coherence by Lm3,ARYTM_2:2,XBOOLE_1:1; 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 being 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 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 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 being set 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_relative_prime & j <> {}}; then consider i,j such that A7: f = [i,j] and i,j are_relative_prime 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,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,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,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,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_relative_prime & j <> {}} \ {[k,one]: not contradiction}; not ex x,y being set st {[0,x],[one,y]} in IR proof given x,y being set such that A19: {[0,x],[one,y]} in IR; 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; 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 redefine func 0 -> Element of NAT; coherence by ORDINAL1:def 11; end; theorem Th1: 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; A1: now assume (0,1) --> (0,1) in X; 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; 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 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 being 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 being 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 being 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 being ordinal number 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 by ARYTM_3:def 13; 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 ex k being 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; 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, ARYTM_3:def 3; then 2 divides 1 by A4,ARYTM_3:11; hence thesis by A5,ARYTM_3:8; 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 thesis by ARYTM_3:58; end; Lm14: for i being Element of RAT+ holds i + i = two *' i proof let i be Element of RAT+; 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; end; theorem Th2: RAT c< REAL proof 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} 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 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 09 = 0 as Element of RAT+ by Lm1; set DD = { A where A is 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 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 assume X in {{ s: s < t}: t <> 0}; then consider t0 being 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 being Element of RAT+ such that A18: two + es = t0 *' t0 or t0 *' t0 + es = two by ARYTM_3:92; A19: now assume 09 = es; then two + es = two by ARYTM_3:50; hence contradiction by A17,A18,ARYTM_3:def 13; end; 09 <=' es by ARYTM_3:64; then 09 < es by A19,ARYTM_3:68; then consider s such that A20: 09 < 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 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,78; set x = s *' s *' 2t9; consider t0x being 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,69; then A34: t0x <=' t0 by A32,ARYTM_3:def 13; 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,def 13 .= 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,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 + x *' x + s *' s = (t0x + x) *' t0 + x *' x by A29,A32 ,A33,ARYTM_3:51,def 13 .= t0x *' (t0x + x) + x *' t0 + x *' x by A32,A33,ARYTM_3:57 ,def 13 .= 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 by ARYTM_3:def 13; 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 2t9 = 0; hence contradiction by A31,ARYTM_3:48; end; end; then t0x <> t0 by A32,A33,ARYTM_3:84,def 13; 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,def 13; 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,ARYTM_3:def 13; 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 being 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 2t9 being Element of RAT+ such that A52: (two *' t0) *' 2t9 = one by A15,ARYTM_3:55,78; set x = s *' s *' 2t9; consider t0x being 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,69; then A55: t0x <=' t0 by A53,ARYTM_3:def 13; 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,def 13 .= 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,ARYTM_3:def 13; 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 ,def 13 .= t0x *' (t0x + x) + x *' t0 + x *' x by A53,A54,ARYTM_3:57 ,def 13 .= 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 by ARYTM_3:def 13; 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 2t9 = 0; hence contradiction by A52,ARYTM_3:48; end; end; then t0x <> t0 by A53,A54,ARYTM_3:84,def 13; 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,def 13; 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 .= n *^ n by ORDINAL2:39; then consider k being 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 .= 2 *^ (k *^ k)by ORDINAL3:50; then A64: ex p being natural Ordinal st d = 2 *^ p by Lm12; n, d are_relative_prime by ARYTM_3:34; hence contradiction by A63,A64,ARYTM_3:def 2; 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 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 3r9 being Element of RAT+ such that A71: (r + r + r) *' 3r9 = one by ARYTM_3:54,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 assume A74: eps = 0; per cases by A74,ARYTM_3:78; suppose rr = 09; then r *' r = two by A72,ARYTM_3:50; hence contradiction by A68; end; suppose 3r9 = 09; 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,def 13; hence t in X; 09 <=' eps by ARYTM_3:64; then 09 < eps by A73,ARYTM_3:68; then r + 09 < 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,80; a9 + half <> 0 by ARYTM_3:63; then t *' t < two *' r *' t by A70,A79,ARYTM_3:78,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,def 13; then t *' t < two by A81,ARYTM_3:69; hence t in X; 09 <> half & 09 <=' half by A10,ARYTM_3:48,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; 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_relative_prime & j <> {}} \ {[k,one]: not contradiction}; then X in {[i,j]: i,j are_relative_prime & j <> {}}; then ex i,j st X = [i,j] & i,j are_relative_prime & 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,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 being set 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,XBOOLE_0:def 8; end; theorem 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 Th4: INT c< RAT proof 1,2 are_relative_prime proof let c,d1,d2 be Ordinal such that A1: 1 = c *^ d1 and 2 = c *^ d2; thus thesis by A1,ORDINAL3:37; 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 thesis by Lm15,XBOOLE_0:def 8; end; theorem Th5: INT c< REAL by Th2,Th4,XBOOLE_1:56; theorem Th6: INT c< COMPLEX by Th1,Th5,XBOOLE_1:56; theorem 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,XBOOLE_0:def 8; end; theorem Th8: NAT c< RAT by Th4,Th7,XBOOLE_1:56; theorem Th9: NAT c< REAL by Th2,Th8,XBOOLE_1:56; theorem Th10: NAT c< COMPLEX by Th1,Th9,XBOOLE_1:56; begin :: to be canceled theorem REAL c= COMPLEX by Th1,XBOOLE_0:def 8; theorem RAT c= REAL by Th2,XBOOLE_0:def 8; theorem RAT c= COMPLEX by Th3,XBOOLE_0:def 8; theorem INT c= RAT by Th4,XBOOLE_0:def 8; theorem INT c= REAL by Th5,XBOOLE_0:def 8; theorem INT c= COMPLEX by Th6,XBOOLE_0:def 8; theorem NAT c= INT by Lm5; theorem Th18: NAT c= RAT by Th8,XBOOLE_0:def 8; theorem Th19: NAT c= REAL; theorem Th20: NAT c= COMPLEX by Th10,XBOOLE_0:def 8; theorem REAL <> COMPLEX by Th1; theorem RAT <> REAL by Th2; theorem RAT <> COMPLEX by Th1,Th2; theorem INT <> RAT by Th4; theorem INT <> REAL by Th2,Th4; theorem INT <> COMPLEX by Th1,Th2,Th4,XBOOLE_1:56; theorem NAT <> INT by Th7; theorem NAT <> RAT by Th4,Th7; theorem NAT <> REAL by Th2,Th4,Th7,XBOOLE_1:56; theorem NAT <> COMPLEX by Th1,Th2,Th8,XBOOLE_1:56; definition func ExtREAL equals REAL \/ { REAL, [0,REAL] }; coherence; end; registration cluster ExtREAL -> non empty; coherence; end; theorem Th31: REAL c= ExtREAL by XBOOLE_1:7; theorem 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 REAL c< ExtREAL by Th31,Th32,XBOOLE_0:def 8; 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;