### The Mizar article:

### Strong Arithmetic of Real Numbers

**by****Andrzej Trybulec**

- Received January 1, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: AXIOMS
- [ MML identifier index ]

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;

Back to top