:: Introduction to Arithmetic of Real Numbers
:: by Library Committee
::
:: Received February 11, 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 ORDINAL1, NUMBERS, XXREAL_0, CARD_1, XCMPLX_0, SUBSET_1, ARYTM_0,
FUNCOP_1, ARYTM_1, ARYTM_3, RELAT_1, ARYTM_2, ZFMISC_1, XBOOLE_0,
XREAL_0, FUNCT_7, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_4, ORDINAL1, ARYTM_2,
ARYTM_1, NUMBERS, ARYTM_0, XCMPLX_0, XXREAL_0;
constructors FUNCT_4, ARYTM_1, ARYTM_0, XCMPLX_0, XXREAL_0;
registrations ARYTM_2, NUMBERS, XCMPLX_0, XXREAL_0, ORDINAL1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions XXREAL_0;
equalities TARSKI, XCMPLX_0, XXREAL_0, ARYTM_3, ORDINAL1;
expansions TARSKI, ORDINAL1;
theorems XBOOLE_0, ARYTM_1, ZFMISC_1, TARSKI, ARYTM_2, ARYTM_0, XCMPLX_0,
NUMBERS, XXREAL_0, XTUPLE_0, XREGULAR, SUBSET_1;
begin
definition
let r be object;
attr r is real means
:Def1:
r in REAL;
end;
registration
cluster -> real for Element of REAL;
coherence;
end;
registration
cluster -infty -> non real;
coherence
proof
{0,REAL} in {{0,REAL},{0}} & REAL in {0,REAL} by TARSKI:def 2;
hence thesis by XREGULAR:7;
end;
cluster +infty -> non real;
coherence
proof
not REAL in REAL;
hence thesis;
end;
end;
registration
cluster natural -> real for object;
coherence by NUMBERS:19;
cluster real -> complex for object;
coherence;
end;
registration
cluster real for object;
existence
proof
take 0;
thus 0 in REAL by NUMBERS:19;
end;
cluster real for number;
existence
proof
take 0;
thus 0 in REAL by NUMBERS:19;
end;
cluster real -> ext-real for object;
coherence
proof
let n be object;
assume n in REAL;
hence n in ExtREAL by XBOOLE_0:def 3;
end;
end;
definition
mode Real is real Number;
end;
Lm1: for x being Real, x1,x2 being Element of REAL st x = [*x1,x2*]
holds x2 = 0 & x = x1
proof
let x be Real, x1,x2 being Element of REAL;
assume
A1: x = [*x1,x2*];
A2: x in REAL by Def1;
thus now
assume x2 <> 0;
then x = (0,1) --> (x1,x2) by A1,ARYTM_0:def 5;
hence contradiction by A2,ARYTM_0:8;
end;
hence thesis by A1,ARYTM_0:def 5;
end;
registration
let x be Real;
cluster -x -> real;
coherence
proof
x + -x = 0;
then consider x1,x2,y1,y2 being Element of REAL such that
A1: x = [*x1,x2*] and
A2: -x = [*y1,y2*] and
A3: 0 = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
+(x2,y2) = 0 & x2 = 0 by A1,A3,Lm1;
then y2 = 0 by ARYTM_0:11;
hence thesis by A2,ARYTM_0:def 5;
end;
cluster x" -> real;
coherence
proof
per cases;
suppose x = 0;
hence thesis by XCMPLX_0:def 7;
end;
suppose
A4: x <> 0;
then x * x" = 1 by XCMPLX_0:def 7;
then consider x1,x2,y1,y2 being Element of REAL such that
A5: x = [*x1,x2*] and
A6: x" = [*y1,y2*] and
A7: 1 = [*+(*(x1,y1),opp*(x2,y2)),+(*(x1,y2),*(x2,y1))*] by XCMPLX_0:def 5;
+(*(x1,y2),*(x2,y1)) = 0 & x2 = 0 by A5,A7,Lm1;
then 0 = *(x1,y2) by ARYTM_0:11,12;
then x1 = 0 or y2 = 0 by ARYTM_0:21;
hence thesis by A4,A5,A6,Lm1,ARYTM_0:def 5;
end;
end;
let y be Real;
cluster x + y -> real;
coherence
proof
consider x1,x2,y1,y2 being Element of REAL such that
A8: x = [*x1,x2*] & y = [*y1,y2*] and
A9: x+y = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
x2 = 0 & y2 = 0 by A8,Lm1;
then +(x2,y2) = 0 by ARYTM_0:11;
hence thesis by A9,ARYTM_0:def 5;
end;
cluster x * y -> real;
coherence
proof
consider x1,x2,y1,y2 being Element of REAL such that
A10: x = [*x1,x2*] and
A11: y = [*y1,y2*] and
A12: x*y = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by
XCMPLX_0:def 5;
reconsider zz=0 as Element of REAL by NUMBERS:19;
x2 = 0 by A10,Lm1;
then
A13: *(x2,y1) = 0 by ARYTM_0:12;
A14: y2 = 0 by A11,Lm1;
then *(opp x2,y2) = 0 by ARYTM_0:12;
then
A15: opp*(x2,y2) = 0 by ARYTM_0:15;
*(x1,y2) = 0 by A14,ARYTM_0:12;
then +(*(x1,y2),*(x2,y1)) = 0 by A13,ARYTM_0:11;
then x * y = +(*(x1,y1),zz) by A12,A15,ARYTM_0:def 5
.= *(x1,y1) by ARYTM_0:11;
hence thesis;
end;
end;
registration
let x,y be Real;
cluster x-y -> real;
coherence;
cluster x/y -> real;
coherence;
end;
begin
reserve r,s,t for Real;
Lm2: (r in REAL+ & s in REAL+ & ex x9,y9 being Element of REAL+ st r = x9 & s
= y9 & x9 <=' y9) or (r in [:{0},REAL+:] & s in [:{0},REAL+:] & ex x9,y9 being
Element of REAL+ st r = [0,x9] & s = [0,y9] & y9 <=' x9) or s in REAL+ & r in
[:{0},REAL+:] implies r <= s
proof
assume
A1: (r in REAL+ & s in REAL+ & ex x9,y9 being Element of REAL+ st r = x9
& s = y9 & x9 <=' y9) or (r in [:{0},REAL+:] & s in [:{0},REAL+:] & ex x9,y9
being Element of REAL+ st r = [0,x9] & s = [0,y9] & y9 <=' x9) or s in REAL+ &
r in [:{0},REAL+:];
per cases;
case r in REAL+ & s in REAL+;
hence thesis by A1,ARYTM_0:5,XBOOLE_0:3;
end;
case r in [:{0},REAL+:] & s in [:{0},REAL+:];
hence thesis by A1,ARYTM_0:5,XBOOLE_0:3;
end;
case not(r in REAL+ & s in REAL+) & not (r in [:{0},REAL+:] &
s in [:{0},REAL+:]);
hence thesis by A1;
end;
end;
Lm3: {} in {{}} by TARSKI:def 1;
Lm4: r <= s & s <= r implies r = s
proof
assume that
A1: r <= s and
A2: s <= r;
A3: r in REAL & s in REAL by Def1;
per cases by A3,NUMBERS:def 1,XBOOLE_0:def 3;
suppose r in REAL+ & s in REAL+;
then
(ex r9,s9 being Element of REAL+ st r = r9 & s = s9 & r9 <=' s9 )& ex
s99, r99 being Element of REAL+ st s = s99 & r = r99 & s99 <=' r99 by A1,A2,
XXREAL_0:def 5;
hence thesis by ARYTM_1:4;
end;
suppose
A4: r in REAL+ & s in [:{0},REAL+:];
then
( not(r in REAL+ & s in REAL+))& not(r in [:{0},REAL+:] & s in [:{0},
REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
hence thesis by A1,A4,XXREAL_0:def 5;
end;
suppose
A5: s in REAL+ & r in [:{0},REAL+:];
then
( not(r in REAL+ & s in REAL+))& not(r in [:{0},REAL+:] & s in [:{0},
REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
hence thesis by A2,A5,XXREAL_0:def 5;
end;
suppose that
A6: r in [:{0},REAL+:] & s in [:{0},REAL+:];
consider r9,s9 being Element of REAL+ such that
A7: r = [0,r9] & s = [0,s9] and
A8: s9 <=' r9 by A1,A6,XXREAL_0:def 5;
consider s99,r99 being Element of REAL+ such that
A9: s = [0,s99] & r = [0,r99] and
A10: r99 <=' s99 by A2,A6,XXREAL_0:def 5;
r9 = r99 & s9 = s99 by A7,A9,XTUPLE_0:1;
hence thesis by A8,A9,A10,ARYTM_1:4;
end;
end;
Lm5: r <= s implies r + t <= s + t
proof
reconsider x1=r, y1=s, z1=t as Element of REAL by Def1;
A1: for x9 being Element of REAL, r st x9 = r holds +(x9,z1) = r + t
proof
let x9 be Element of REAL, r such that
A2: x9 = r;
consider x1,x2,y1,y2 being Element of REAL such that
A3: r = [* x1,x2 *] & t = [*y1,y2*] and
A4: r+t = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
x2 = 0 & y2 = 0 by A3,Lm1;
then
A5: +(x2,y2) = 0 by ARYTM_0:11;
r = x1 & t = y1 by A3,Lm1;
hence thesis by A2,A4,A5,ARYTM_0:def 5;
end;
then
A6: +(y1,z1) = s + t;
A7: +(x1,z1) = r + t by A1;
assume
A8: r <= s;
per cases by A8,XXREAL_0:def 5;
suppose that
A9: r in REAL+ and
A10: s in REAL+ and
A11: t in REAL+;
consider s9,t99 being Element of REAL+ such that
A12: s = s9 & t = t99 and
A13: +(y1,z1) = s9 + t99 by A10,A11,ARYTM_0:def 1;
consider x9,t9 being Element of REAL+ such that
A14: r = x9 & t = t9 and
A15: +(x1,z1) = x9 + t9 by A9,A11,ARYTM_0:def 1;
ex x99,s99 being Element of REAL+ st r = x99 & s = s99 & x99 <=' s99
by A8,A9,A10,XXREAL_0:def 5;
then x9 + t9 <=' s9 + t99 by A14,A12,ARYTM_1:7;
hence thesis by A6,A7,A15,A13,Lm2;
end;
suppose that
A16: r in [:{0},REAL+:] and
A17: s in REAL+ and
A18: t in REAL+;
consider s9,t99 being Element of REAL+ such that
s = s9 and
A19: t = t99 and
A20: +(y1,z1) = s9 + t99 by A17,A18,ARYTM_0:def 1;
consider x9,t9 being Element of REAL+ such that
r = [0,x9] and
A21: t = t9 and
A22: +(x1,z1) = t9 - x9 by A16,A18,ARYTM_0:def 1;
now
per cases;
suppose
A23: x9 <=' t9;
t9 -' x9 <=' t9 & t9 <=' s9 + t99 by A21,A19,ARYTM_1:11,ARYTM_2:19;
then
A24: t9 -' x9 <=' s9 + t99 by ARYTM_1:3;
t9 - x9 = t9 -' x9 by A23,ARYTM_1:def 2;
hence thesis by A6,A7,A22,A20,A24,Lm2;
end;
suppose
not x9 <=' t9;
then t9 - x9 = [0,x9 -' t9] by ARYTM_1:def 2;
then t9 - x9 in [:{0},REAL+:] by Lm3,ZFMISC_1:87;
then
A25: not r + t in REAL+ by A7,A22,ARYTM_0:5,XBOOLE_0:3;
not s + t in [:{0},REAL+:] by A6,A20,ARYTM_0:5,XBOOLE_0:3;
hence thesis by A25,XXREAL_0:def 5;
end;
end;
hence thesis;
end;
suppose that
A26: r in [:{0},REAL+:] and
A27: s in [:{0},REAL+:] and
A28: t in REAL+;
consider s9,t99 being Element of REAL+ such that
A29: s = [0,s9] and
A30: t = t99 and
A31: +(y1,z1) = t99 - s9 by A27,A28,ARYTM_0:def 1;
consider x99,s99 being Element of REAL+ such that
A32: r = [0,x99] and
A33: s = [0,s99] and
A34: s99 <=' x99 by A8,A26,A27,XXREAL_0:def 5;
consider x9,t9 being Element of REAL+ such that
A35: r = [0,x9] and
A36: t = t9 and
A37: +(x1,z1) = t9 - x9 by A26,A28,ARYTM_0:def 1;
A38: x9 = x99 by A32,A35,XTUPLE_0:1;
A39: s9 = s99 by A33,A29,XTUPLE_0:1;
now
per cases;
suppose
A40: x9 <=' t9;
then s9 <=' t9 by A34,A38,A39,ARYTM_1:3;
then
A41: t9 - s9 = t9 -' s9 by ARYTM_1:def 2;
A42: t9 - x9 = t9 -' x9 by A40,ARYTM_1:def 2;
t9 -' x9 <=' t99 -' s9 by A34,A36,A30,A38,A39,ARYTM_1:16;
hence thesis by A6,A7,A36,A37,A30,A31,A42,A41,Lm2;
end;
suppose
not x9 <=' t9;
then
A43: +(x1,z1) = [0,x9 -' t9] by A37,ARYTM_1:def 2;
then
A44: +(x1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:87;
now
per cases;
suppose
s9 <=' t9;
then t9 - s9 = t9 -' s9 by ARYTM_1:def 2;
then
A45: not +(y1,z1) in [:{0},REAL+:] by A36,A30,A31,ARYTM_0:5,XBOOLE_0:3;
not +(x1,z1) in REAL+ by A44,ARYTM_0:5,XBOOLE_0:3;
hence thesis by A6,A7,A45,XXREAL_0:def 5;
end;
suppose
A46: not s9 <=' t9;
A47: s9 -' t9 <=' x9 -' t9 by A34,A38,A39,ARYTM_1:17;
A48: +(y1,z1) = [0,s9 -' t9] by A36,A30,A31,A46,ARYTM_1:def 2;
then +(y1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:87;
hence thesis by A6,A7,A43,A44,A48,A47,Lm2;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose that
A49: r in REAL+ and
A50: s in REAL+ and
A51: t in [:{0},REAL+:];
consider s9,t99 being Element of REAL+ such that
A52: s = s9 and
A53: t = [0,t99] and
A54: +(y1,z1) = s9 - t99 by A50,A51,ARYTM_0:def 1;
consider x9,t9 being Element of REAL+ such that
A55: r = x9 and
A56: t = [0,t9] and
A57: +(x1,z1) = x9 - t9 by A49,A51,ARYTM_0:def 1;
A58: t9 = t99 by A56,A53,XTUPLE_0:1;
A59: ex x99,s99 being Element of REAL+ st r = x99 & s = s99 & x99 <=' s99
by A8,A49,A50,XXREAL_0:def 5;
now
per cases;
suppose
A60: t9 <=' x9;
then t9 <=' s9 by A59,A55,A52,ARYTM_1:3;
then
A61: s9 - t9 = s9 -' t9 by ARYTM_1:def 2;
A62: x9 - t9 = x9 -' t9 by A60,ARYTM_1:def 2;
x9 -' t9 <=' s9 -' t99 by A59,A55,A52,A58,ARYTM_1:17;
hence thesis by A6,A7,A57,A54,A58,A62,A61,Lm2;
end;
suppose
not t9 <=' x9;
then
A63: +(x1,z1) = [0,t9 -' x9] by A57,ARYTM_1:def 2;
then
A64: +(x1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:87;
now
per cases;
suppose
t9 <=' s9;
then s9 - t9 = s9 -' t9 by ARYTM_1:def 2;
then
A65: not +(y1,z1) in [:{0},REAL+:] by A54,A58,ARYTM_0:5,XBOOLE_0:3;
not +(x1,z1) in REAL+ by A64,ARYTM_0:5,XBOOLE_0:3;
hence thesis by A6,A7,A65,XXREAL_0:def 5;
end;
suppose
A66: not t9 <=' s9;
A67: t9 -' s9 <=' t9 -' x9 by A59,A55,A52,ARYTM_1:16;
A68: +(y1,z1) = [0,t9 -' s9] by A54,A58,A66,ARYTM_1:def 2;
then +(y1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:87;
hence thesis by A6,A7,A63,A64,A68,A67,Lm2;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose that
A69: r in [:{0},REAL+:] and
A70: s in REAL+ and
A71: t in [:{0},REAL+:];
( not r in REAL+)& not t in REAL+ by A69,A71,ARYTM_0:5,XBOOLE_0:3;
then consider x9,t9 being Element of REAL+ such that
r = [0,x9] and
A72: t = [0,t9] and
A73: +(x1,z1) = [0,x9 + t9] by ARYTM_0:def 1;
A74: +(x1,z1) in [:{0},REAL+:] by A73,Lm3,ZFMISC_1:87;
consider s9,t99 being Element of REAL+ such that
s = s9 and
A75: t = [0,t99] and
A76: +(y1,z1) = s9 - t99 by A70,A71,ARYTM_0:def 1;
A77: t9 = t99 by A72,A75,XTUPLE_0:1;
now
per cases;
suppose
t9 <=' s9;
then s9 - t99 = s9 -' t99 by A77,ARYTM_1:def 2;
then
A78: not +(y1,z1) in [:{0},REAL+:] by A76,ARYTM_0:5,XBOOLE_0:3;
not +(x1,z1) in REAL+ by A74,ARYTM_0:5,XBOOLE_0:3;
hence thesis by A6,A7,A78,XXREAL_0:def 5;
end;
suppose
A79: not t9 <=' s9;
t9 -' s9 <=' t9 & t9 <=' t9 + x9 by ARYTM_1:11,ARYTM_2:19;
then
A80: t9 -' s9 <=' t9 + x9 by ARYTM_1:3;
A81: +(y1,z1) = [0,t9 -' s9] by A76,A77,A79,ARYTM_1:def 2;
then +(y1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:87;
hence thesis by A6,A7,A73,A74,A81,A80,Lm2;
end;
end;
hence thesis;
end;
suppose that
A82: r in [:{0},REAL+:] and
A83: s in [:{0},REAL+:] and
A84: t in [:{0},REAL+:];
( not s in REAL+)& not t in REAL+ by A83,A84,ARYTM_0:5,XBOOLE_0:3;
then consider s9,t99 being Element of REAL+ such that
A85: s = [0,s9] and
A86: t = [0,t99] and
A87: +(y1,z1) = [0,s9 + t99] by ARYTM_0:def 1;
A88: +(y1,z1) in [:{0},REAL+:] by A87,Lm3,ZFMISC_1:87;
( not r in REAL+)& not t in REAL+ by A82,A84,ARYTM_0:5,XBOOLE_0:3;
then consider x9,t9 being Element of REAL+ such that
A89: r = [0,x9] and
A90: t = [0,t9] and
A91: +(x1,z1) = [0,x9 + t9] by ARYTM_0:def 1;
A92: +(x1,z1) in [:{0},REAL+:] by A91,Lm3,ZFMISC_1:87;
A93: t9 = t99 by A90,A86,XTUPLE_0:1;
consider x99,s99 being Element of REAL+ such that
A94: r = [0,x99] and
A95: s = [0,s99] and
A96: s99 <=' x99 by A8,A82,A83,XXREAL_0:def 5;
A97: s9 = s99 by A95,A85,XTUPLE_0:1;
x9 = x99 by A94,A89,XTUPLE_0:1;
then s9 + t9 <=' x9 + t99 by A96,A97,A93,ARYTM_1:7;
hence thesis by A6,A7,A91,A87,A93,A92,A88,Lm2;
end;
end;
Lm6: r <= s & s <= t implies r <= t
proof
assume that
A1: r <= s and
A2: s <= t;
A3: r in REAL & s in REAL by Def1;
A4: t in REAL by Def1;
per cases by A3,A4,NUMBERS:def 1,XBOOLE_0:def 3;
suppose that
A5: r in REAL+ and
A6: s in REAL+ and
A7: t in REAL+;
consider s99,t9 being Element of REAL+ such that
A8: s = s99 and
A9: t = t9 and
A10: s99 <=' t9 by A2,A6,A7,XXREAL_0:def 5;
consider x9,s9 being Element of REAL+ such that
A11: r = x9 and
A12: s = s9 & x9 <=' s9 by A1,A5,A6,XXREAL_0:def 5;
x9 <=' t9 by A12,A8,A10,ARYTM_1:3;
hence thesis by A11,A9,Lm2;
end;
suppose
A13: r in REAL+ & s in [:{0},REAL+:];
then
( not(r in REAL+ & s in REAL+))& not(r in [:{0},REAL+:] & s in [:{0},
REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
hence thesis by A1,A13,XXREAL_0:def 5;
end;
suppose
A14: s in REAL+ & t in [:{0},REAL+:];
then
( not(t in REAL+ & s in REAL+))& not(t in [:{0},REAL+:] & s in [:{0},
REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
hence thesis by A2,A14,XXREAL_0:def 5;
end;
suppose that
A15: r in [:{0},REAL+:] and
A16: t in REAL+;
( not(r in REAL+ & t in REAL+))& not(r in [:{0},REAL+:] & t in [:{0},
REAL+:]) by A15,A16,ARYTM_0:5,XBOOLE_0:3;
hence thesis by A16,XXREAL_0:def 5;
end;
suppose that
A17: r in [:{0},REAL+:] and
A18: s in [:{0},REAL+:] and
A19: t in [:{0},REAL+:];
consider s99,t9 being Element of REAL+ such that
A20: s = [0,s99] and
A21: t = [0,t9] and
A22: t9 <=' s99 by A2,A18,A19,XXREAL_0:def 5;
consider x9,s9 being Element of REAL+ such that
A23: r = [0,x9] and
A24: s = [0,s9] and
A25: s9 <=' x9 by A1,A17,A18,XXREAL_0:def 5;
s9 = s99 by A24,A20,XTUPLE_0:1;
then t9 <=' x9 by A25,A22,ARYTM_1:3;
hence thesis by A17,A19,A23,A21,Lm2;
end;
end;
Lm7: not 0 in [:{0},REAL+:] by ARYTM_0:5,ARYTM_2:20,XBOOLE_0:3;
Lm8: 0 <= 1
proof
reconsider z=0, j = 1 as Element of REAL+ by ARYTM_2:20;
z <=' j by ARYTM_1:6;
hence thesis by Lm2;
end;
Lm14: r >= 0 & s > 0 implies r + s > 0
proof
assume r >= 0;
then r + s >= 0 + s by Lm5;
hence thesis by Lm6;
end;
Lm15: r <= 0 & s < 0 implies r + s < 0
proof
assume r <= 0;
then r + s <= 0 + s by Lm5;
hence thesis by Lm6;
end;
Lm16: r <= s & 0 <= t implies r * t <= s * t
proof
reconsider x1=r, y1=s, z1=t as Element of REAL by Def1;
assume that
A1: r <= s and
A2: 0 <= t;
0 is Element of REAL+ by ARYTM_2:20;
then not 0 in [:{0},REAL+:] by ARYTM_0:5,XBOOLE_0:3;
then
A3: t in REAL+ by A2,XXREAL_0:def 5;
for x9 being Element of REAL, r st x9 = r holds *(x9,z1) = r * t
proof
let x9 be Element of REAL, r such that
A4: x9 = r;
consider x1,x2,y1,y2 being Element of REAL such that
A5: r = [* x1,x2 *] and
A6: t = [*y1,y2*] and
A7: r*t = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by XCMPLX_0:def 5
;
x2 = 0 by A5,Lm1;
then
A8: *(x2,y1) = 0 by ARYTM_0:12;
A9: y2 = 0 by A6,Lm1;
then *(x1,y2) = 0 by ARYTM_0:12;
then
A10: +(*(x1,y2),*(x2,y1)) = 0 by A8,ARYTM_0:11;
r = x1 & t = y1 by A5,A6,Lm1;
hence *(x9,z1) = +(*(x1,y1),*(opp x2,y2)) by A4,A9,ARYTM_0:11,12
.= +(*(x1,y1),opp*(x2,y2)) by ARYTM_0:15
.= r * t by A7,A10,ARYTM_0:def 5;
end;
then
A11: *(y1,z1) = s * t & *(x1,z1) = r * t;
assume
A12: not thesis;
then
A13: t <> 0;
per cases by A1,XXREAL_0:def 5;
suppose that
A14: r in REAL+ and
A15: s in REAL+;
consider s9,t99 being Element of REAL+ such that
A16: s = s9 and
A17: t = t99 & *(y1,z1) = s9 *' t99 by A3,A15,ARYTM_0:def 2;
consider x9,t9 being Element of REAL+ such that
A18: r = x9 and
A19: t = t9 & *(x1,z1) = x9 *' t9 by A3,A14,ARYTM_0:def 2;
ex x99,s99 being Element of REAL+ st r = x99 & s = s99 & x99 <=' s99
by A1,A14,A15,XXREAL_0:def 5;
then x9 *' t9 <=' s9 *' t9 by A18,A16,ARYTM_1:8;
hence contradiction by A11,A12,A19,A17,Lm2;
end;
suppose that
A20: r in [:{0},REAL+:] and
A21: s in REAL+;
ex x9,t9 being Element of REAL+ st r = [0,x9] & t = t9 & *(x1,z1) = [0
,t9 *' x9] by A3,A13,A20,ARYTM_0:def 2;
then *(x1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:87;
then
A22: not *(x1,z1) in REAL+ by ARYTM_0:5,XBOOLE_0:3;
ex s9,t99 being Element of REAL+ st s = s9 & t = t99 & * (y1,z1) = s9
*' t99 by A3,A21,ARYTM_0:def 2;
then not *(y1,z1) in [:{0},REAL+:] by ARYTM_0:5,XBOOLE_0:3;
hence contradiction by A11,A12,A22,XXREAL_0:def 5;
end;
suppose that
A23: r in [:{0},REAL+:] and
A24: s in [:{0},REAL+:];
consider s9,t99 being Element of REAL+ such that
A25: s = [0,s9] and
A26: t = t99 and
A27: *(y1,z1) = [0,t99 *' s9] by A3,A13,A24,ARYTM_0:def 2;
A28: *(y1,z1) in [:{0},REAL+:] by A27,Lm3,ZFMISC_1:87;
consider x99,s99 being Element of REAL+ such that
A29: r = [0,x99] and
A30: s = [0,s99] and
A31: s99 <=' x99 by A1,A23,A24,XXREAL_0:def 5;
A32: s9 = s99 by A30,A25,XTUPLE_0:1;
consider x9,t9 being Element of REAL+ such that
A33: r = [0,x9] and
A34: t = t9 and
A35: *(x1,z1) = [0,t9 *' x9] by A3,A13,A23,ARYTM_0:def 2;
A36: *(x1,z1) in [:{0},REAL+:] by A35,Lm3,ZFMISC_1:87;
x9 = x99 by A29,A33,XTUPLE_0:1;
then s9 *' t9 <=' x9 *' t9 by A31,A32,ARYTM_1:8;
hence contradiction by A11,A12,A34,A35,A26,A27,A36,A28,Lm2;
end;
end;
Lm17: r > 0 & s > 0 implies r*s > 0
proof
assume
A1: r > 0 & s > 0;
then r * s >= 0 * s by Lm16;
hence thesis by A1,Lm4;
end;
Lm18: r > 0 & s < 0 implies r*s < 0
proof
assume
A1: r > 0 & s < 0;
then r * s <= r * 0 by Lm16;
hence thesis by A1,Lm4;
end;
Lm19: s<=t implies -t<=-s
proof
assume s<=t;
then s-t<=t-t by Lm5;
then s-t-s<=0-s by Lm5;
hence thesis;
end;
Lm20: r <= 0 & s >= 0 implies r*s <= 0
proof
assume
A1: r <= 0 & s >= 0;
per cases by A1,Lm4;
suppose
r = 0 or s = 0;
hence thesis;
end;
suppose
r < 0 & s > 0;
hence thesis by Lm18;
end;
end;
registration
cluster positive for Real;
existence
proof
take r = 1;
thus 0 < r by Lm4,Lm8;
end;
cluster negative for Real;
existence
proof
take r = -1;
1 + -1 = 0;
then consider x1,x2,y1,y2 being Element of REAL such that
Lm9: 1 = [*x1,x2*] and
Lm10: -1 = [*y1,y2*] & 0 = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
Lm11: x1 = 1 by Lm1,Lm9;
Lm12: y1 = -1 & +(x1,y1) = 0 by Lm1,Lm10;
reconsider z = 0 as Element of REAL+ by ARYTM_2:20;
now
assume -1 in REAL+;
then ex x9,y9 being Element of REAL+ st x1 = x9 & y1 = y9 & z = x9 + y9
by Lm11,Lm12,ARYTM_0:def 1,ARYTM_2:20;
hence contradiction by Lm11,ARYTM_2:5;
end;
hence 0 > r by Lm7,XXREAL_0:def 5;
end;
cluster zero for Real;
existence
proof
take 0;
thus thesis;
end;
end;
registration
let r,s be non negative Real;
cluster r + s -> non negative;
coherence
proof
A1: s >= 0 by XXREAL_0:def 7;
A2: r >= 0 by XXREAL_0:def 7;
per cases by A2,Lm4;
suppose
r = 0;
hence r + s >= 0 by XXREAL_0:def 7;
end;
suppose
r > 0;
hence r+s >= 0 by A1,Lm14;
end;
end;
end;
registration
let r,s be non positive Real;
cluster r + s -> non positive;
coherence
proof
A1: s <= 0 by XXREAL_0:def 6;
A2: r <= 0 by XXREAL_0:def 6;
per cases by A2,Lm4;
suppose
r = 0;
hence r + s <= 0 by XXREAL_0:def 6;
end;
suppose
r < 0;
hence r + s <= 0 by A1,Lm15;
end;
end;
end;
registration
let r be positive Real;
let s be non negative Real;
cluster r + s -> positive;
coherence
proof
r > 0 & s >= 0 by XXREAL_0:def 6;
hence r+s > 0 by Lm14;
end;
cluster s + r -> positive;
coherence;
end;
registration
let r be negative Real;
let s be non positive Real;
cluster r + s -> negative;
coherence
proof
r < 0 & s <= 0 by XXREAL_0:def 7;
hence r+s < 0 by Lm15;
end;
cluster s + r -> negative;
coherence;
end;
registration
let r be non positive Real;
cluster -r -> non negative;
coherence
proof
assume
A1: -r < 0;
--r <= 0 by XXREAL_0:def 6;
then -r+--r < 0 by A1,Lm15;
hence contradiction;
end;
end;
registration
let r be non negative Real;
cluster -r -> non positive;
coherence
proof
assume
A1: -r > 0;
--r >= 0 by XXREAL_0:def 7;
then -r+--r > 0 by A1,Lm14;
hence contradiction;
end;
end;
registration
let r be non negative Real, s be non positive Real;
cluster r - s -> non negative;
coherence;
cluster s - r -> non positive;
coherence;
end;
registration
let r be positive Real;
let s be non positive Real;
cluster r - s -> positive;
coherence;
cluster s - r -> negative;
coherence;
end;
registration
let r be negative Real;
let s be non negative Real;
cluster r - s -> negative;
coherence;
cluster s - r -> positive;
coherence;
end;
registration
let r be non positive Real, s be non negative Real;
cluster r*s -> non positive;
coherence
proof
r <= 0 & s >= 0 by XXREAL_0:def 6;
hence r*s <= 0 by Lm20;
end;
cluster s*r -> non positive;
coherence;
end;
registration
let r,s be non positive Real;
cluster r*s -> non negative;
coherence
proof
A1: r <= 0 & s <= 0 by XXREAL_0:def 6;
per cases by A1,Lm4;
suppose
r = 0 or s = 0;
hence r * s >= 0;
end;
suppose
A2: --r < --0 & s < 0;
then 0<-r by Lm19;
then s*(-r)<=0*(-r) by A2,Lm16;
then s*(-r)<0*(-r) by A2,Lm4;
then --0*r<--s*r by Lm19;
hence r * s >= 0;
end;
end;
end;
registration
let r,s be non negative Real;
cluster r*s -> non negative;
coherence
proof
A1: r >= 0 & s >= 0 by XXREAL_0:def 7;
per cases by A1,Lm4;
suppose
r = 0 or s = 0;
hence r * s >= 0;
end;
suppose
r > 0 & s > 0;
hence r * s >= 0 by Lm17;
end;
end;
end;
registration
let r be positive Real;
cluster r" -> positive;
coherence
proof
assume
A1: r" <= 0;
r"" > 0 by XXREAL_0:def 6;
then r"*r"" = 1 & r"*r"" <= 0 by A1,Lm20,XCMPLX_0:def 7;
hence contradiction by Lm4,Lm8;
end;
end;
registration
let r be non positive Real;
cluster r" -> non positive;
coherence
proof
A1: r"" <= 0 by XXREAL_0:def 6;
assume
A2: r" > 0;
per cases by A1,Lm4;
suppose
r"" = 0;
hence contradiction by A2;
end;
suppose
A3: r"" < 0;
r"*r"" = 1 by A2,XCMPLX_0:def 7;
hence contradiction by A2,A3,Lm8,Lm18;
end;
end;
end;
registration
let r be negative Real;
cluster r" -> negative;
coherence;
end;
registration
let r be non negative Real;
cluster r" -> non negative;
coherence
proof
A1: r"" >= 0 by XXREAL_0:def 7;
assume
A2: r" < 0;
per cases by A1,Lm4;
suppose
r"" = 0;
hence contradiction by A2;
end;
suppose
A3: r"" > 0;
r"*r"" = 1 by A2,XCMPLX_0:def 7;
hence contradiction by A2,A3,Lm8,Lm18;
end;
end;
end;
registration
let r be non negative Real, s be non positive Real;
cluster r/s -> non positive;
coherence;
cluster s/r -> non positive;
coherence;
end;
registration
let r,s be non negative Real;
cluster r/s -> non negative;
coherence;
end;
registration
let r,s be non positive Real;
cluster r/s -> non negative;
coherence;
end;
begin :: min & max
registration
let r,s be Real;
cluster min(r,s) -> real;
coherence by XXREAL_0:15;
cluster max(r,s) -> real;
coherence by XXREAL_0:16;
end;
definition
let r,s be Real;
func r -' s -> set equals
:Def2:
r - s if r -s >= 0 otherwise 0;
correctness;
end;
registration
let r,s be Real;
cluster r -' s -> real;
coherence
proof
r -' s = r - s or r -' s = 0 by Def2;
hence thesis;
end;
end;
registration
let r,s be Real;
cluster r -' s -> non negative for Real;
coherence
proof
r -' s = r - s & r - s >= 0 or r -' s = 0 by Def2;
hence thesis by XXREAL_0:def 7;
end;
end;
registration
sethood of Real
proof
take REAL;
thus thesis by Def1;
end;
end;
:: 16.04.20121, A.T.
registration let i be Real;
reduce In(i,REAL) to i;
reducibility
by Def1,SUBSET_1:def 8;
end;