Copyright (c) 2003 Association of Mizar Users
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;