:: Basic Properties of Real Numbers - Requirements :: by Library Committee :: :: Received February 27, 2003 :: Copyright (c) 2003-2018 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 XXREAL_0, NUMBERS, ARYTM_2, SUBSET_1, ARYTM_3, ZFMISC_1, CARD_1, XCMPLX_0, REAL_1; notations TARSKI, ZFMISC_1, SUBSET_1, ARYTM_2, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0; constructors ARYTM_2, NUMBERS, XXREAL_0, XREAL_0; registrations ARYTM_2, XREAL_0, ORDINAL1; requirements SUBSET, BOOLE; equalities ORDINAL1; theorems XBOOLE_0, ARYTM_0, ARYTM_1, XREAL_0, NUMBERS, XXREAL_0, XTUPLE_0; 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; Lm1: x <= y & y <= x implies x = y proof assume that A1: x <= y and A2: y <= x; A3: x in REAL & y in REAL by XREAL_0:def 1; per cases by A3,NUMBERS:def 1,XBOOLE_0:def 3; suppose x in REAL+ & y in REAL+; then (ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & x9 <=' y9 )& ex y99, x99 being Element of REAL+ st y = y99 & x = x99 & y99 <=' x99 by A1,A2, XXREAL_0:def 5; hence thesis by ARYTM_1:4; end; suppose A4: 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,A4,XXREAL_0:def 5; end; suppose A5: 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,A5,XXREAL_0:def 5; end; suppose that A6: x in [:{0},REAL+:] & y in [:{0},REAL+:]; consider x9,y9 being Element of REAL+ such that A7: x = [0,x9] & y = [0,y9] and A8: y9 <=' x9 by A1,A6,XXREAL_0:def 5; consider y99,x99 being Element of REAL+ such that A9: y = [0,y99] & x = [0,x99] and A10: x99 <=' y99 by A2,A6,XXREAL_0:def 5; x9 = x99 & y9 = y99 by A7,A9,XTUPLE_0:1; hence thesis by A8,A9,A10,ARYTM_1:4; end; end; Lm2: x <= y & y <= z implies x <= z proof assume that A1: x <= y and A2: y <= z; A3: x in REAL & y in REAL by XREAL_0:def 1; A4: z in REAL by XREAL_0:def 1; per cases by A3,A4,NUMBERS:def 1,XBOOLE_0:def 3; suppose that A5: x in REAL+ and A6: y in REAL+ and A7: z in REAL+; consider y99,z9 being Element of REAL+ such that A8: y = y99 and A9: z = z9 and A10: y99 <=' z9 by A2,A6,A7,XXREAL_0:def 5; consider x9,y9 being Element of REAL+ such that A11: x = x9 and A12: y = y9 & x9 <=' y9 by A1,A5,A6,XXREAL_0:def 5; x9 <=' z9 by A12,A8,A10,ARYTM_1:3; hence thesis by A11,A9,XXREAL_0:def 5; end; 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,XXREAL_0:def 5; end; 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,XXREAL_0:def 5; end; 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,XXREAL_0:def 5; end; suppose that A17: x in [:{0},REAL+:] and A18: y in [:{0},REAL+:] and A19: z in [:{0},REAL+:]; consider y99,z9 being Element of REAL+ such that A20: y = [0,y99] and A21: z = [0,z9] and A22: z9 <=' y99 by A2,A18,A19,XXREAL_0:def 5; consider x9,y9 being Element of REAL+ such that A23: x = [0,x9] and A24: y = [0,y9] and A25: y9 <=' x9 by A1,A17,A18,XXREAL_0:def 5; y9 = y99 by A24,A20,XTUPLE_0:1; then z9 <=' x9 by A25,A22,ARYTM_1:3; hence thesis by A17,A19,A23,A21,XXREAL_0:def 5; end; end; theorem x <= y & x is positive implies y is positive proof assume that A1: x <= y and A2: x is positive; x > 0 by A2,XXREAL_0:def 6; then y > 0 by A1,Lm2; hence thesis by XXREAL_0:def 6; end; theorem x <= y & y is negative implies x is negative proof assume that A1: x <= y and A2: y is negative; y < 0 by A2,XXREAL_0:def 7; then x < 0 by A1,Lm2; hence thesis by XXREAL_0:def 7; end; theorem x <= y & x is non negative implies y is non negative proof assume that A1: x <= y and A2: x is non negative and A3: y is negative; y < 0 by A3,XXREAL_0:def 7; then x < 0 by A1,Lm2; hence thesis by A2,XXREAL_0:def 7; end; theorem x <= y & y is non positive implies x is non positive proof assume that A1: x <= y and A2: y is non positive and A3: x is positive; x > 0 by A3,XXREAL_0:def 6; then y > 0 by A1,Lm2; hence thesis by A2,XXREAL_0:def 6; end; theorem x <= y & y is non zero & x is non negative implies y is positive proof assume that A1: x <= y and A2: y is non zero and A3: x is non negative and A4: y is non positive; y <= 0 by A4,XXREAL_0:def 6; then A5: y < 0 by A2,Lm1; x >= 0 by A3,XXREAL_0:def 7; hence thesis by A1,A5,Lm2; end; theorem x <= y & x is non zero & y is non positive implies x is negative proof assume that A1: x <= y and A2: x is non zero and A3: y is non positive and A4: x is non negative; x >= 0 by A4,XXREAL_0:def 7; then A5: x > 0 by A2,Lm1; y <= 0 by A3,XXREAL_0:def 6; hence thesis by A1,A5,Lm2; end; theorem not x <= y & x is non positive implies y is negative proof assume that A1: x > y and A2: x is non positive & y is non negative; x <= 0 & y >= 0 by A2,XXREAL_0:def 6,def 7; hence thesis by A1,Lm2; end; theorem not x <= y & y is non negative implies x is positive proof assume that A1: x > y and A2: y is non negative & x is non positive; x <= 0 & y >= 0 by A2,XXREAL_0:def 6,def 7; hence thesis by A1,Lm2; end; ::theorem :: numeral(X) & X <> 0 implies X is positive;