:: Basic Properties of Real Numbers - Requirements
:: by Library Committee
::
:: Received February 27, 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 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;