### The Mizar article:

### Basic Properties of Real Numbers --- Requirements

**by****Library Committee**

- Received February 27, 2003
Copyright (c) 2003 Association of Mizar Users

- MML identifier: REAL
- [ MML identifier index ]

environ vocabulary XREAL_0, ARYTM, ARYTM_3, ASYMPT_0, ZF_LANG, ARYTM_2, BOOLE; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ARYTM_2, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0; constructors ARYTM_0, XREAL_0, ARYTM_2, XCMPLX_0, XBOOLE_0; clusters XREAL_0, ARYTM_2, NUMBERS, XCMPLX_0, ARYTM_3, ZFMISC_1, XBOOLE_0; requirements NUMERALS, SUBSET, BOOLE; theorems XBOOLE_0, ZFMISC_1, ARYTM_0, ARYTM_1, XREAL_0, NUMBERS; begin :: This file contains statements which are obvious for Mizar checker if :: "requirements REAL" is included in the environment description of an article. :: They are published for testing purposes only. :: Users should use appropriate requirements instead of referencing :: to these theorems. :: Note that the checker needs also "requirements BOOLE" to accept :: the statements with attribute 'zero'. reserve x, y, z for real number; Lm1: 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; Lm2: 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; theorem x <= y & x is positive implies y is positive proof assume A1: x <= y & x is positive; then x > 0 by XREAL_0:def 3; then y > 0 by A1,Lm2; hence thesis by XREAL_0:def 3; end; theorem x <= y & y is negative implies x is negative proof assume A1: x <= y & y is negative; then y < 0 by XREAL_0:def 4; then x < 0 by A1,Lm2; hence thesis by XREAL_0:def 4; end; theorem x <= y & x is non negative implies y is non negative proof assume A1: x <= y & x is non negative & y is negative; then y < 0 by XREAL_0:def 4; then x < 0 by A1,Lm2; hence thesis by A1,XREAL_0:def 4; end; theorem x <= y & y is non positive implies x is non positive proof assume A1: x <= y & y is non positive & x is positive; then x > 0 by XREAL_0:def 3; then y > 0 by A1,Lm2; hence thesis by A1,XREAL_0:def 3; end; theorem x <= y & y is non zero & x is non negative implies y is positive proof assume A1: x <= y & y is non zero & x is non negative & y is non positive; then x >= 0 & y <= 0 by XREAL_0:def 3,def 4; then x >= 0 & y < 0 by A1,Lm1; hence thesis by A1,Lm2; end; theorem x <= y & x is non zero & y is non positive implies x is negative proof assume A1: x <= y & x is non zero & y is non positive & x is non negative; then x >= 0 & y <= 0 by XREAL_0:def 3,def 4; then x > 0 & y <= 0 by A1,Lm1; hence thesis by A1,Lm2; end; theorem not x <= y & x is non positive implies y is negative proof assume A1: x > y & x is non positive & y is non negative; then x <= 0 & y >= 0 by XREAL_0:def 3,def 4; hence thesis by A1,Lm2; end; theorem not x <= y & y is non negative implies x is positive proof assume A1: x > y & y is non negative & x is non positive; then x <= 0 & y >= 0 by XREAL_0:def 3,def 4; hence thesis by A1,Lm2; end;

Back to top