:: Subsets of Complex Numbers
:: by Andrzej Trybulec
::
:: Received November 7, 2003
:: Copyright (c) 2003-2026 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;
requirements BOOLE, SUBSET, NUMERALS;
definitions XBOOLE_0;
equalities TARSKI, ARYTM_3, ORDINAL1;
expansions 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_coprime &
d <> {}} \ the set of all [k,1] where k is Element of omega) \/ omega by
XBOOLE_1:7;
notation
synonym NAT for omega;
end;
Lm2: 1 = succ 0;
definition
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
func COMPLEX -> set equals
Funcs({0,1},REAL) \ { x where x is Element of Funcs({0,1
},REAL): x.1 = 0} \/ REAL;
coherence;
func RAT -> set equals
RAT+ \/ [:{0},RAT+:] \ {[0,0]};
coherence;
func INT -> set 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 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 {i} = [one,b];
then i = {one} by Lm6;
hence contradiction;
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 2;
i = {0} by A16,Lm6;
hence contradiction by A17,TARSKI:def 1;
end;
end;
then
A18: not f in {[i,j]: i,j are_coprime & j <> {}} \ the set of all
[k,one];
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 omega; :: redefines 0 (ORDINAL1, definition)
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;
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 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 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,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 being 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 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 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,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 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 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 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 T2t9 being Element of RAT+ such that
A31: (two *' t0) *' T2t9 = one by A15,ARYTM_3:55,78;
set x = s *' s *' T2t9;
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;
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 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 T2t9 being Element of RAT+ such that
A52: (two *' t0) *' T2t9 = one by A15,ARYTM_3:55,78;
set x = s *' s *' T2t9;
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;
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 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,Lm11
.= 2 *^ (k *^ k)by ORDINAL3:50;
then
A64: ex p being 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 being Element of RAT+ such that
A71: (r + r + r) *' T3r9 = 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 *' 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,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;
then t *' t < two by A81,ARYTM_3:69;
hence t in X;
O9 <> half & O9 <=' half by A10,ARYTM_3:48,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,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 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 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_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 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;
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;
theorem
RAT c= REAL by Th2;
theorem
RAT c= COMPLEX by Th3;
theorem
INT c= RAT by Th4;
theorem
INT c= REAL by Th5;
theorem
INT c= COMPLEX by Th6;
theorem
NAT c= INT by Lm5;
theorem Th18:
NAT c= RAT by Th8;
theorem Th19:
NAT c= REAL by Th9;
theorem Th20:
NAT c= COMPLEX by Th10;
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 -> set 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;
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;