Copyright (c) 1989 Association of Mizar Users
environ
vocabulary BOOLE, ARYTM, ARYTM_2, ARYTM_3, ORDINAL2, ARYTM_1, ORDINAL1,
COMPLEX1, OPPCAT_1, RELAT_1, FUNCOP_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, FUNCT_4,
ARYTM_2, ARYTM_1, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0;
constructors ARYTM_1, ARYTM_0, XREAL_0, XCMPLX_0, FUNCT_4, XBOOLE_0;
clusters XREAL_0, ARYTM_2, ARYTM_3, ORDINAL2, NUMBERS, XCMPLX_0, ZFMISC_1,
XBOOLE_0;
requirements SUBSET, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems XBOOLE_0, ARYTM_0, ZFMISC_1, TARSKI, ARYTM_1, ARYTM_2, SUBSET_1,
ORDINAL2, ORDINAL1, XBOOLE_1, XREAL_0, XCMPLX_0, NUMBERS;
begin
reserve x,y,z for real number,
k for natural number,
i for Element of NAT;
canceled 18;
theorem
ex y st x + y = 0
proof
take y = -x;
thus x + y = 0 by XCMPLX_0:def 6;
end;
theorem
x <> 0 implies ex y st x * y = 1
proof
assume
A1: x <> 0;
take y = x";
thus x * y = 1 by A1,XCMPLX_0:def 7;
end;
theorem Th21:
x <= y & y <= x implies x = y
proof assume that
A1: x <= y and
A2: y <= x;
x in REAL & y in REAL by XREAL_0:def 1;
then A3: x in REAL+ \/ [:{0},REAL+:] & y in REAL+ \/ [:{0},REAL+:]
by NUMBERS:def 1,XBOOLE_0:def 4;
per cases by A3,XBOOLE_0:def 2;
suppose that
A4: x in REAL+ and
A5: y in REAL+;
consider x',y' being Element of REAL+ such that
A6: x = x' and
A7: y = y' and
A8: x' <=' y' by A1,A4,A5,XREAL_0:def 2;
consider y'',x'' being Element of REAL+ such that
A9: y = y'' and
A10: x = x'' and
A11: y'' <=' x'' by A2,A4,A5,XREAL_0:def 2;
thus thesis by A6,A7,A8,A9,A10,A11,ARYTM_1:4;
suppose
A12: x in REAL+ & y in [:{0},REAL+:];
then not(x in REAL+ & y in REAL+) &
not(x in [:{0},REAL+:] & y in [:{0},REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
hence thesis by A1,A12,XREAL_0:def 2;
suppose
A13: y in REAL+ & x in [:{0},REAL+:];
then not(x in REAL+ & y in REAL+) &
not(x in [:{0},REAL+:] & y in [:{0},REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
hence thesis by A2,A13,XREAL_0:def 2;
suppose that
A14: x in [:{0},REAL+:] and
A15: y in [:{0},REAL+:];
consider x',y' being Element of REAL+ such that
A16: x = [0,x'] and
A17: y = [0,y'] and
A18: y' <=' x' by A1,A14,A15,XREAL_0:def 2;
consider y'',x'' being Element of REAL+ such that
A19: y = [0,y''] and
A20: x = [0,x''] and
A21: x'' <=' y'' by A2,A14,A15,XREAL_0:def 2;
x' = x'' & y' = y'' by A16,A17,A19,A20,ZFMISC_1:33;
hence thesis by A18,A19,A20,A21,ARYTM_1:4;
end;
theorem
x <= y & y <= z implies x <= z
proof assume that
A1: x <= y and
A2: y <= z;
x in REAL & y in REAL & z in REAL by XREAL_0:def 1;
then A3: x in REAL+ \/ [:{0},REAL+:] & y in REAL+ \/ [:{0},REAL+:]
& z in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4;
per cases by A3,XBOOLE_0:def 2;
suppose that
A4: x in REAL+ and
A5: y in REAL+ and
A6: z in REAL+;
consider x',y' being Element of REAL+ such that
A7: x = x' and
A8: y = y' and
A9: x' <=' y' by A1,A4,A5,XREAL_0:def 2;
consider y'',z' being Element of REAL+ such that
A10: y = y'' and
A11: z = z' and
A12: y'' <=' z' by A2,A5,A6,XREAL_0:def 2;
x' <=' z' by A8,A9,A10,A12,ARYTM_1:3;
hence thesis by A7,A11,XREAL_0:def 2;
suppose
A13: x in REAL+ & y in [:{0},REAL+:];
then not(x in REAL+ & y in REAL+) &
not(x in [:{0},REAL+:] & y in [:{0},REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
hence thesis by A1,A13,XREAL_0:def 2;
suppose
A14: y in REAL+ & z in [:{0},REAL+:];
then not(z in REAL+ & y in REAL+) &
not(z in [:{0},REAL+:] & y in [:{0},REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
hence thesis by A2,A14,XREAL_0:def 2;
suppose that
A15: x in [:{0},REAL+:] and
A16: z in REAL+;
not(x in REAL+ & z in REAL+) &
not(x in [:{0},REAL+:] & z in
[:{0},REAL+:]) by A15,A16,ARYTM_0:5,XBOOLE_0:3;
hence thesis by A16,XREAL_0:def 2;
suppose that
A17: x in [:{0},REAL+:] and
A18: y in [:{0},REAL+:] and
A19: z in [:{0},REAL+:];
consider x',y' being Element of REAL+ such that
A20: x = [0,x'] and
A21: y = [0,y'] and
A22: y' <=' x' by A1,A17,A18,XREAL_0:def 2;
consider y'',z' being Element of REAL+ such that
A23: y = [0,y''] and
A24: z = [0,z'] and
A25: z' <=' y'' by A2,A18,A19,XREAL_0:def 2;
y' = y'' by A21,A23,ZFMISC_1:33;
then z' <=' x' by A22,A25,ARYTM_1:3;
hence thesis by A17,A19,A20,A24,XREAL_0:def 2;
end;
Lm1: for x being real number, x1,x2 being Element of REAL st x = [*x1,x2*]
holds x2 = 0 & x = x1
proof let x be real number, x1,x2 being Element of REAL;
assume
A1: x = [*x1,x2*];
A2: x in REAL by XREAL_0:def 1;
hereby assume x2 <> 0;
then x = (0,one) --> (x1,x2) by A1,ARYTM_0:def 7;
hence contradiction by A2,ARYTM_0:10;
end;
hence x = x1 by A1,ARYTM_0:def 7;
end;
Lm2:
for x',y' being Element of REAL, x,y st x' = x & y' = y
holds +(x',y') = x + y
proof let x',y' be Element of REAL, x,y such that
A1: x' = x & y' = y;
consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [* x1,x2 *] and
A3: y = [*y1,y2*] and
A4: x+y = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
A5: x = x1 & y = y1 by A2,A3,Lm1;
x2 = 0 & y2 = 0 by A2,A3,Lm1;
then +(x2,y2) = 0 by ARYTM_0:13;
hence +(x',y') = x + y by A1,A4,A5,ARYTM_0:def 7;
end;
Lm3: {} in {{}} by TARSKI:def 1;
canceled;
theorem
x <= y implies x + z <= y + z
proof
assume
A1: x <= y;
reconsider x1=x, y1=y, z1=z as Element of REAL by XREAL_0:def 1;
A2: +(y1,z1) = y + z & +(x1,z1) = x + z by Lm2;
per cases by A1,XREAL_0:def 2;
suppose that
A3: x in REAL+ and
A4: y in REAL+ and
A5: z in REAL+;
consider x'',y'' being Element of REAL+ such that
A6: x = x'' and
A7: y = y'' and
A8: x'' <=' y'' by A1,A3,A4,XREAL_0:def 2;
consider x',z' being Element of REAL+ such that
A9: x = x' and
A10: z = z' and
A11: +(x1,z1) = x' + z' by A3,A5,ARYTM_0:def 2;
consider y',z'' being Element of REAL+ such that
A12: y = y' and
A13: z = z'' and
A14: +(y1,z1) = y' + z'' by A4,A5,ARYTM_0:def 2;
x' + z' <=' y' + z'' by A6,A7,A8,A9,A10,A12,A13,ARYTM_1:7;
hence x + z <= y + z by A2,A11,A14,XREAL_0:def 2;
suppose that
A15: x in [:{0},REAL+:] and
A16: y in REAL+ and
A17: z in REAL+;
consider x',z' being Element of REAL+ such that
x = [0,x'] and
A18: z = z' and
A19: +(x1,z1) = z' - x' by A15,A17,ARYTM_0:def 2;
consider y',z'' being Element of REAL+ such that
y = y' and
A20: z = z'' and
A21: +(y1,z1) = y' + z'' by A16,A17,ARYTM_0:def 2;
now per cases;
suppose x' <=' z';
then A22: z' - x' = z' -' x' by ARYTM_1:def 2;
A23: z' -' x' <=' z' by ARYTM_1:11;
z' <=' y' + z'' by A18,A20,ARYTM_2:20;
then z' -' x' <=' y' + z'' by A23,ARYTM_1:3;
hence x + z <= y + z by A2,A19,A21,A22,XREAL_0:def 2;
suppose
not x' <=' z';
then z' - x' = [0,x' -' z'] by ARYTM_1:def 2;
then z' - x' in [:{0},REAL+:] by Lm3,ZFMISC_1:106;
then not x + z in REAL+ & not y + z in [:{0},REAL+:]
by A2,A19,A21,ARYTM_0:5,XBOOLE_0:3;
hence x + z <= y + z by XREAL_0:def 2;
end;
hence thesis;
suppose that
A24: x in [:{0},REAL+:] and
A25: y in [:{0},REAL+:] and
A26: z in REAL+;
consider x'',y'' being Element of REAL+ such that
A27: x = [0,x''] and
A28: y = [0,y''] and
A29: y'' <=' x'' by A1,A24,A25,XREAL_0:def 2;
consider x',z' being Element of REAL+ such that
A30: x = [0,x'] and
A31: z = z' and
A32: +(x1,z1) = z' - x' by A24,A26,ARYTM_0:def 2;
consider y',z'' being Element of REAL+ such that
A33: y = [0,y'] and
A34: z = z'' and
A35: +(y1,z1) = z'' - y' by A25,A26,ARYTM_0:def 2;
A36: x' = x'' by A27,A30,ZFMISC_1:33;
A37: y' = y'' by A28,A33,ZFMISC_1:33;
now per cases;
suppose
A38: x' <=' z';
then A39: z' - x' = z' -' x' by ARYTM_1:def 2;
y' <=' z' by A29,A36,A37,A38,ARYTM_1:3;
then A40: z' - y' = z' -' y' by ARYTM_1:def 2;
z' -' x' <=' z'' -' y' by A29,A31,A34,A36,A37,ARYTM_1:16;
hence x + z <= y + z by A2,A31,A32,A34,A35,A39,A40,XREAL_0:def 2;
suppose not x' <=' z';
then A41: +(x1,z1) = [0,x' -' z'] by A32,ARYTM_1:def 2;
then A42: +(x1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:106;
now per cases;
suppose y' <=' z';
then z' - y' = z' -' y' by ARYTM_1:def 2;
then not +(x1,z1) in REAL+ & not +(y1,z1) in [:{0},REAL+:]
by A31,A34,A35,A42,ARYTM_0:5,XBOOLE_0:3;
hence x + z <= y + z by A2,XREAL_0:def 2;
suppose not y' <=' z';
then A43: +(y1,z1) = [0,y' -' z'] by A31,A34,A35,ARYTM_1:def 2;
then A44: +(y1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:106;
y' -' z' <=' x' -' z' by A29,A36,A37,ARYTM_1:17;
hence x + z <= y + z by A2,A41,A42,A43,A44,XREAL_0:def 2;
end;
hence thesis;
end;
hence thesis;
suppose that
A45: x in REAL+ and
A46: y in REAL+ and
A47: z in [:{0},REAL+:];
consider x'',y'' being Element of REAL+ such that
A48: x = x'' and
A49: y = y'' and
A50: x'' <=' y'' by A1,A45,A46,XREAL_0:def 2;
consider x',z' being Element of REAL+ such that
A51: x = x' and
A52: z = [0,z'] and
A53: +(x1,z1) = x' - z' by A45,A47,ARYTM_0:def 2;
consider y',z'' being Element of REAL+ such that
A54: y = y' and
A55: z = [0,z''] and
A56: +(y1,z1) = y' - z'' by A46,A47,ARYTM_0:def 2;
A57: z' = z'' by A52,A55,ZFMISC_1:33;
now per cases;
suppose
A58: z' <=' x';
then A59: x' - z' = x' -' z' by ARYTM_1:def 2;
z' <=' y' by A48,A49,A50,A51,A54,A58,ARYTM_1:3;
then A60: y' - z' = y' -' z' by ARYTM_1:def 2;
x' -' z' <=' y' -' z'' by A48,A49,A50,A51,A54,A57,ARYTM_1:17;
hence x + z <= y + z by A2,A53,A56,A57,A59,A60,XREAL_0:def 2;
suppose not z' <=' x';
then A61: +(x1,z1) = [0,z' -' x'] by A53,ARYTM_1:def 2;
then A62: +(x1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:106;
now per cases;
suppose z' <=' y';
then y' - z' = y' -' z' by ARYTM_1:def 2;
then not +(x1,z1) in REAL+ & not +(y1,z1) in [:{0},REAL+:]
by A56,A57,A62,ARYTM_0:5,XBOOLE_0:3;
hence x + z <= y + z by A2,XREAL_0:def 2;
suppose not z' <=' y';
then A63: +(y1,z1) = [0,z' -' y'] by A56,A57,ARYTM_1:def 2;
then A64: +(y1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:106;
z' -' y' <=' z' -' x' by A48,A49,A50,A51,A54,ARYTM_1:16;
hence x + z <= y + z by A2,A61,A62,A63,A64,XREAL_0:def 2;
end;
hence thesis;
end;
hence thesis;
suppose that
A65: x in [:{0},REAL+:] and
A66: y in REAL+ and
A67: z in [:{0},REAL+:];
not x in REAL+ & not z in REAL+ by A65,A67,ARYTM_0:5,XBOOLE_0:3;
then consider x',z' being Element of REAL+ such that
x = [0,x'] and
A68: z = [0,z'] and
A69: +(x1,z1) = [0,x' + z'] by ARYTM_0:def 2;
consider y',z'' being Element of REAL+ such that
y = y' and
A70: z = [0,z''] and
A71: +(y1,z1) = y' - z'' by A66,A67,ARYTM_0:def 2;
A72: z' = z'' by A68,A70,ZFMISC_1:33;
A73: +(x1,z1) in [:{0},REAL+:] by A69,Lm3,ZFMISC_1:106;
now per cases;
suppose z' <=' y';
then y' - z'' = y' -' z'' by A72,ARYTM_1:def 2;
then not +(x1,z1) in REAL+ & not +(y1,z1) in [:{0},REAL+:]
by A71,A73,ARYTM_0:5,XBOOLE_0:3;
hence x + z <= y + z by A2,XREAL_0:def 2;
suppose
not z' <=' y';
then A74: +(y1,z1) = [0,z' -' y'] by A71,A72,ARYTM_1:def 2;
then A75: +(y1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:106;
A76: z' -' y' <=' z' by ARYTM_1:11;
z' <=' z' + x' by ARYTM_2:20;
then z' -' y' <=' z' + x' by A76,ARYTM_1:3;
hence x + z <= y + z by A2,A69,A73,A74,A75,XREAL_0:def 2;
end;
hence thesis;
suppose that
A77: x in [:{0},REAL+:] and
A78: y in [:{0},REAL+:] and
A79: z in [:{0},REAL+:];
consider x'',y'' being Element of REAL+ such that
A80: x = [0,x''] and
A81: y = [0,y''] and
A82: y'' <=' x'' by A1,A77,A78,XREAL_0:def 2;
not x in REAL+ & not z in REAL+ by A77,A79,ARYTM_0:5,XBOOLE_0:3;
then consider x',z' being Element of REAL+ such that
A83: x = [0,x'] and
A84: z = [0,z'] and
A85: +(x1,z1) = [0,x' + z'] by ARYTM_0:def 2;
not y in REAL+ & not z in REAL+ by A78,A79,ARYTM_0:5,XBOOLE_0:3;
then consider y',z'' being Element of REAL+ such that
A86: y = [0,y'] and
A87: z = [0,z''] and
A88: +(y1,z1) = [0,y' + z''] by ARYTM_0:def 2;
A89: x' = x'' by A80,A83,ZFMISC_1:33;
A90: y' = y'' by A81,A86,ZFMISC_1:33;
A91: z' = z'' by A84,A87,ZFMISC_1:33;
then A92: y' + z' <=' x' + z'' by A82,A89,A90,ARYTM_1:7;
A93: +(x1,z1) in [:{0},REAL+:] by A85,Lm3,ZFMISC_1:106;
+(y1,z1) in [:{0},REAL+:] by A88,Lm3,ZFMISC_1:106;
hence x + z <= y + z by A2,A85,A88,A91,A92,A93,XREAL_0:def 2;
end;
reconsider o = 0 as Element of REAL+ by ARYTM_2:21;
Lm4:
for x',y' being Element of REAL, x,y st x' = x & y' = y
holds *(x',y') = x * y
proof let x',y' be Element of REAL, x,y such that
A1: x' = x & y' = y;
consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [* x1,x2 *] and
A3: y = [*y1,y2*] and
A4: x*y = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *]
by XCMPLX_0:def 5;
A5: x = x1 & y = y1 by A2,A3,Lm1;
A6: x2 = 0 & y2 = 0 by A2,A3,Lm1;
then *(x1,y2) = 0 & *(x2,y1) = 0 by ARYTM_0:14;
then A7: +(*(x1,y2),*(x2,y1)) = 0 by ARYTM_0:13;
thus *(x',y') = +(*(x1,y1),0) by A1,A5,ARYTM_0:13
.= +(*(x1,y1),*(opp x2,y2)) by A6,ARYTM_0:14
.= +(*(x1,y1),opp*(x2,y2)) by ARYTM_0:17
.= x * y by A4,A7,ARYTM_0:def 7;
end;
theorem
x <= y & 0 <= z implies x * z <= y * z
proof assume that
A1: x <= y and
A2: 0 <= z;
reconsider x1=x, y1=y, z1=z as Element of REAL by XREAL_0:def 1;
A3: *(y1,z1) = y * z & *(x1,z1) = x * z by Lm4;
not o in [:{0},REAL+:] by ARYTM_0:5,XBOOLE_0:3;
then A4: z in REAL+ by A2,XREAL_0:def 2;
assume
A5: not thesis;
then A6: z <> 0;
per cases by A1,XREAL_0:def 2;
suppose that
A7: x in REAL+ and
A8: y in REAL+;
consider x'',y'' being Element of REAL+ such that
A9: x = x'' and
A10: y = y'' and
A11: x'' <=' y'' by A1,A7,A8,XREAL_0:def 2;
consider x',z' being Element of REAL+ such that
A12: x = x' and
A13: z = z' and
A14: *(x1,z1) = x' *' z' by A4,A7,ARYTM_0:def 3;
consider y',z'' being Element of REAL+ such that
A15: y = y' and
A16: z = z'' and
A17: *(y1,z1) = y' *' z'' by A4,A8,ARYTM_0:def 3;
x' *' z' <=' y' *' z' by A9,A10,A11,A12,A15,ARYTM_1:8;
hence contradiction by A3,A5,A13,A14,A16,A17,XREAL_0:def 2;
suppose that
A18: x in [:{0},REAL+:] and
A19: y in REAL+;
consider x',z' being Element of REAL+ such that
x = [0,x'] and
z = z' and
A20: *(x1,z1) = [0,z' *' x'] by A4,A6,A18,ARYTM_0:def 3;
consider y',z'' being Element of REAL+ such that
y = y' and
z = z'' and
A21: *(y1,z1) = y' *' z'' by A4,A19,ARYTM_0:def 3;
*(x1,z1) in [:{0},REAL+:] by A20,Lm3,ZFMISC_1:106;
then not *(x1,z1) in REAL+ & not *(y1,z1) in [:{0},REAL+:]
by A21,ARYTM_0:5,XBOOLE_0:3;
hence contradiction by A3,A5,XREAL_0:def 2;
suppose that
A22: x in [:{0},REAL+:] and
A23: y in [:{0},REAL+:];
consider x'',y'' being Element of REAL+ such that
A24: x = [0,x''] and
A25: y = [0,y''] and
A26: y'' <=' x'' by A1,A22,A23,XREAL_0:def 2;
consider x',z' being Element of REAL+ such that
A27: x = [0,x'] and
A28: z = z' and
A29: *(x1,z1) = [0,z' *' x'] by A4,A6,A22,ARYTM_0:def 3;
consider y',z'' being Element of REAL+ such that
A30: y = [0,y'] and
A31: z = z'' and
A32: *(y1,z1) = [0,z'' *' y'] by A4,A6,A23,ARYTM_0:def 3;
A33: x' = x'' by A24,A27,ZFMISC_1:33;
A34: y' = y'' by A25,A30,ZFMISC_1:33;
A35: *(x1,z1) in [:{0},REAL+:] & *(y1,z1) in [:{0},REAL+:]
by A29,A32,Lm3,ZFMISC_1:106;
y' *' z' <=' x' *' z' by A26,A33,A34,ARYTM_1:8;
hence contradiction by A3,A5,A28,A29,A31,A32,A35,XREAL_0:def 2;
end;
reserve r,r1,r2 for Element of REAL+;
theorem
for X,Y being Subset of REAL st for x,y st x in X & y in Y holds x <= y
ex z st for x,y st x in X & y in Y holds x <= z & z <= y
proof let X,Y be Subset of REAL;
assume
A1: for x,y st x in X & y in Y holds x <= y;
per cases;
suppose
A2: X = 0 or Y = 0;
take 1;
thus thesis by A2;
suppose that
A3: X <> 0 and
A4: Y <> 0;
consider x1 being Element of REAL such that
A5: x1 in X by A3,SUBSET_1:10;
consider x2 being Element of REAL such that
A6: x2 in Y by A4,SUBSET_1:10;
A7: REAL c= REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_1:36;
then A8: X c= REAL+ \/ [:{0},REAL+:] by XBOOLE_1:1;
A9: Y c= REAL+ \/ [:{0},REAL+:] by A7,XBOOLE_1:1;
thus thesis
proof
per cases;
suppose that
A10: X misses REAL+ and
A11: Y misses [:{0},REAL+:];
A12: Y c= REAL+ by A9,A11,XBOOLE_1:73;
take z = 0;
let x,y such that
A13: x in X and
A14: y in Y;
not z in [:{0},REAL+:] & not x in REAL+
by A10,A13,ARYTM_0:5,ARYTM_2:21,XBOOLE_0:3;
hence x <= z by XREAL_0:def 2;
reconsider y' = y as Element of REAL+ by A12,A14;
o <=' y' by ARYTM_1:6;
hence z <= y by XREAL_0:def 2;
suppose
Y meets [:{0},REAL+:];
then consider e being set such that
A15: e in Y and
A16: e in [:{0},REAL+:] by XBOOLE_0:3;
consider u,y1 being set such that
A17: u in {0} and
A18: y1 in REAL+ and
A19: e = [u,y1] by A16,ZFMISC_1:103;
reconsider y1 as Element of REAL+ by A18;
e in REAL by A15;
then A20: [0,y1] in REAL by A17,A19,TARSKI:def 1;
then reconsider y0 = [0,y1] as real number by XREAL_0:def 1;
{r: [0,r] in Y} c= REAL+
proof let u be set;
assume u in {r: [0,r] in Y};
then ex r st u = r & [0,r] in Y;
hence thesis;
end;
then reconsider Y' = {r : [0,r] in Y} as Subset of REAL+;
A21: y0 in [:{0},REAL+:] by Lm3,ZFMISC_1:106;
A22: y0 in Y by A15,A17,A19,TARSKI:def 1;
then A23: y1 in Y';
A24: X c= [:{0},REAL+:]
proof let u be set;
assume
A25: u in X;
then reconsider x = u as real number by XREAL_0:def 1;
now assume
A26: x in REAL+;
A27: x <= y0 by A1,A22,A25;
not y0 in REAL+ & not x in
[:{0},REAL+:] by A21,A26,ARYTM_0:5,XBOOLE_0:3;
hence contradiction by A27,XREAL_0:def 2;
end;
hence u in [:{0},REAL+:] by A8,A25,XBOOLE_0:def 2;
end;
then consider e,x3 being set such that
A28: e in {0} and
A29: x3 in REAL+ and
A30: x1 = [e,x3] by A5,ZFMISC_1:103;
reconsider x3 as Element of REAL+ by A29;
A31: x1 = [0,x3] by A28,A30,TARSKI:def 1;
{r: [0,r] in X} c= REAL+
proof let u be set;
assume u in {r: [0,r] in X};
then ex r st u = r & [0,r] in X;
hence thesis;
end;
then reconsider X' = {r: [0,r] in X} as Subset of REAL+;
A32: x3 in X' by A5,A31;
for y',x' being Element of REAL+ st y' in Y' & x' in X' holds y' <=' x'
proof let y',x' be Element of REAL+;
assume y' in Y';
then consider r1 such that
A33: y' = r1 and
A34: [0,r1] in Y;
assume x' in X';
then consider r2 such that
A35: x' = r2 and
A36: [0,r2] in X;
reconsider x = [0,x'], y = [0,y'] as real number
by A33,A34,A35,A36,XREAL_0:def 1;
A37: x in [:{0},REAL+:] & y in [:{0},REAL+:] by Lm3,ZFMISC_1:106;
x <= y by A1,A33,A34,A35,A36;
then consider x'',y'' being Element of REAL+ such that
A38: x = [0,x''] and
A39: y = [0,y''] and
A40: y'' <=' x'' by A37,XREAL_0:def 2;
x' = x'' & y' = y'' by A38,A39,ZFMISC_1:33;
hence y' <=' x' by A40;
end;
then consider z' being Element of REAL+ such that
A41: for y',x' being Element of REAL+ st y' in Y' & x' in X'
holds y' <=' z' & z' <=' x' by A23,A32,ARYTM_2:9;
A42: y1 <> 0 by A20,ARYTM_0:3;
y1 <=' z' by A23,A32,A41;
then z' <> 0 by A42,ARYTM_1:5;
then [0,z'] in REAL by ARYTM_0:2;
then reconsider z = [0,z'] as real number by XREAL_0:def 1;
take z;
A43: z in [:{0},REAL+:] by Lm3,ZFMISC_1:106;
let x,y such that
A44: x in X and
A45: y in Y;
consider e,x' being set such that
A46: e in {0} and
A47: x' in REAL+ and
A48: x = [e,x'] by A24,A44,ZFMISC_1:103;
reconsider x' as Element of REAL+ by A47;
A49: x = [0,x'] by A46,A48,TARSKI:def 1;
then A50: x' in X' by A44;
now
per cases by A9,A45,XBOOLE_0:def 2;
suppose
A51: y in REAL+;
y1 <=' z' & z' <=' x' by A23,A41,A50;
hence x <= z by A24,A43,A44,A49,XREAL_0:def 2;
not z in REAL+ & not y in [:{0},REAL+:] by A43,A51,ARYTM_0:5,XBOOLE_0:3;
hence z <= y by XREAL_0:def 2;
suppose
A52: y in [:{0},REAL+:];
then consider e,y' being set such that
A53: e in {0} and
A54: y' in REAL+ and
A55: y = [e,y'] by ZFMISC_1:103;
reconsider y' as Element of REAL+ by A54;
A56: y = [0,y'] by A53,A55,TARSKI:def 1;
then y' in Y' by A45;
then y' <=' z' & z' <=' x' by A41,A50;
hence x <= z & z <= y by A24,A43,A44,A49,A52,A56,XREAL_0:def 2;
end;
hence thesis;
suppose
X meets REAL+;
then consider x1 being set such that
A57: x1 in X and
A58: x1 in REAL+ by XBOOLE_0:3;
reconsider x1 as Element of REAL+ by A58;
x1 in REAL+;
then reconsider x0 = x1 as real number by ARYTM_0:1,XREAL_0:def 1;
reconsider X' = X /\ REAL+ as Subset of REAL+ by XBOOLE_1:17;
A59: x0 in X' by A57,XBOOLE_0:def 3;
A60: Y c= REAL+
proof let u be set;
assume
A61: u in Y;
then reconsider y = u as real number by XREAL_0:def 1;
now assume
A62: y in [:{0},REAL+:];
A63: x0 <= y by A1,A57,A61;
not y in REAL+ & not x0 in [:{0},REAL+:] by A62,ARYTM_0:5,XBOOLE_0:3;
hence contradiction by A63,XREAL_0:def 2;
end;
hence u in REAL+ by A9,A61,XBOOLE_0:def 2;
end;
then reconsider Y' = Y as Subset of REAL+;
for x',y' being Element of REAL+ st x' in X' & y' in Y' holds x' <=' y'
proof let x',y' be Element of REAL+;
assume
A64: x' in X' & y' in Y';
x' in REAL+ & y' in REAL+;
then reconsider x = x', y = y' as real number by ARYTM_0:1,XREAL_0:def 1;
X' c= X by XBOOLE_1:17;
then x <= y by A1,A64;
then ex x',y' being Element of REAL+ st x = x' & y = y' & x' <=' y'
by XREAL_0:def 2;
hence x' <=' y';
end;
then consider z' being Element of REAL+ such that
A65: for x',y' being Element of REAL+ st x' in X' & y' in Y'
holds x' <=' z' & z' <=' y' by A6,A59,ARYTM_2:9;
z' in REAL+;
then reconsider z = z' as real number by ARYTM_0:1,XREAL_0:def 1;
take z;
let x,y such that
A66: x in X and
A67: y in Y;
reconsider y' = y as Element of REAL+ by A60,A67;
now
per cases by A8,A66,XBOOLE_0:def 2;
suppose
x in REAL+;
then reconsider x' = x as Element of REAL+;
x' in X' & y' in Y' by A66,A67,XBOOLE_0:def 3;
then x' <=' z' & z' <=' y' by A65;
hence x <= z & z <= y by XREAL_0:def 2;
suppose
x in [:{0},REAL+:];
then not x in REAL+ & not z in [:{0},REAL+:] by ARYTM_0:5,XBOOLE_0:3;
hence x <= z by XREAL_0:def 2;
x1 <=' z' & z' <=' y' by A59,A65,A67;
hence z <= y by XREAL_0:def 2;
end;
hence thesis;
end;
end;
canceled;
theorem
x in NAT & y in NAT implies x + y in NAT
proof
reconsider x1 = x, y1 = y as Element of REAL by XREAL_0:def 1;
A1: +(x1,y1) = x + y by Lm2;
assume
A2: x in NAT & y in NAT;
then ex x',y' being Element of REAL+ st
x1 = x' & y1 = y' & +(x1,y1) = x' + y' by ARYTM_0:def 2,ARYTM_2:2;
hence x + y in NAT by A1,A2,ARYTM_2:17;
end;
Lm5: one = succ 0 by ORDINAL2:def 4 .= 1;
theorem
for A being Subset of REAL
st 0 in A & for x st x in A holds x + 1 in A
holds NAT c= A
proof
let A be Subset of REAL such that
A1: 0 in A and
A2: for x st x in A holds x + 1 in A;
reconsider B = A /\ REAL+ as Subset of REAL+ by XBOOLE_1:17;
A3: 0 in B by A1,ARYTM_2:21,XBOOLE_0:def 3;
A4: B c= A by XBOOLE_1:17;
for x',y' being Element of REAL+ st x' in B & y' = 1 holds x' + y' in B
proof let x',y' be Element of REAL+ such that
A5: x' in B and
A6: y' = 1;
x' in REAL+;
then reconsider x = x' as Element of REAL by ARYTM_0:1;
reconsider xx = x as real number by XREAL_0:def 1;
consider x'',y'' being Element of REAL+ such that
A7: x = x'' and
A8: 1 = y'' and
A9: +(x,1) = x'' + y'' by Lm5,ARYTM_0:def 2,ARYTM_2:21;
xx+1 in A by A2,A4,A5;
then +(x,1) in A by Lm2;
hence x' + y' in B by A6,A7,A8,A9,XBOOLE_0:def 3;
end;
then NAT c= B by A3,Lm5,ARYTM_2:18;
hence NAT c= A by A4,XBOOLE_1:1;
end;
theorem
k = { i: i < k }
proof
thus k c= { i: i < k }
proof let e be set;
reconsider k' = k as Element of NAT by ORDINAL2:def 21;
A1: k' c= NAT by ORDINAL1:def 2;
assume
A2: e in k;
then reconsider j = e as Element of NAT by A1;
k' in NAT;
then reconsider x' = k' as Element of REAL+ by ARYTM_2:2;
e in NAT by A1,A2;
then reconsider y' = e as Element of REAL+ by ARYTM_2:2;
y' in x' by A2;
then A3: y' in NAT & y' <> x' & y' <=' x' by ARYTM_2:19;
then j <= k by XREAL_0:def 2;
then j < k by A3,Th21;
hence e in { i: i < k };
end;
let e be set;
assume e in { i: i < k };
then consider i be Element of NAT such that
A4: e = i and
A5: not k <= i;
A6: k in NAT & i in NAT by ORDINAL2:def 21;
then reconsider x' = e, y' = k as Element of REAL+ by A4,ARYTM_2:2;
not y' <=' x' by A4,A5,XREAL_0:def 2;
hence e in k by A4,A5,A6,ARYTM_2:19;
end;