:: Non negative real numbers. Part II
:: by Andrzej Trybulec
::
:: Received March 7, 1998
:: Copyright (c) 1998-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 SUBSET_1, ARYTM_2, ARYTM_3, XBOOLE_0, ARYTM_1;
notations TARSKI, SUBSET_1, ARYTM_3, ARYTM_2;
constructors ARYTM_2;
requirements SUBSET;
theorems ARYTM_2, TARSKI;
begin
reserve x,y,z for Element of REAL+;
theorem Th1:
x + y = y implies x = {}
proof
reconsider o = {} as Element of REAL+ by ARYTM_2:20;
assume x + y = y;
then x + y = y + o by ARYTM_2:def 8;
hence thesis by ARYTM_2:11;
end;
Lm1: x *' y = x *' z & x <> {} implies y = z
proof
assume
A1: x *' y = x *' z;
assume x <> {};
then consider x1 being Element of REAL+ such that
A2: x *' x1 = one by ARYTM_2:14;
thus y = x *' x1 *' y by A2,ARYTM_2:15
.= x1 *' (x *' z) by A1,ARYTM_2:12
.= x *' x1 *' z by ARYTM_2:12
.= z by A2,ARYTM_2:15;
end;
theorem
x *' y = {} implies x = {} or y = {}
proof
assume
A1: x *' y = {};
assume x <> {};
then consider x1 being Element of REAL+ such that
A2: x *' x1 = one by ARYTM_2:14;
thus y = x *' x1 *' y by A2,ARYTM_2:15
.= x *' y *' x1 by ARYTM_2:12
.= {} by A1,ARYTM_2:4;
end;
theorem Th3:
x <=' y & y <=' z implies x <=' z
proof
assume x <=' y;
then consider z1 being Element of REAL+ such that
A1: x + z1 = y by ARYTM_2:9;
assume y <=' z;
then consider z2 being Element of REAL+ such that
A2: y + z2 = z by ARYTM_2:9;
z = x + (z1 + z2) by A1,A2,ARYTM_2:6;
hence thesis by ARYTM_2:19;
end;
theorem Th4:
x <=' y & y <=' x implies x = y
proof
assume x <=' y;
then consider z1 being Element of REAL+ such that
A1: x + z1 = y by ARYTM_2:9;
assume y <=' x;
then consider z2 being Element of REAL+ such that
A2: y + z2 = x by ARYTM_2:9;
x = x + (z1 + z2) by A1,A2,ARYTM_2:6;
then z1 = {} by Th1,ARYTM_2:5;
hence thesis by A1,ARYTM_2:def 8;
end;
theorem Th5:
x <=' y & y = {} implies x = {}
proof
assume x <=' y;
then ex z being Element of REAL+ st x + z = y by ARYTM_2:9;
hence thesis by ARYTM_2:5;
end;
theorem Th6:
x = {} implies x <=' y
proof
assume x = {};
then x + y = y by ARYTM_2:def 8;
hence thesis by ARYTM_2:19;
end;
theorem Th7:
x <=' y iff x + z <=' y + z
proof
thus x <=' y implies x + z <=' y + z
proof
assume x <=' y;
then consider z0 being Element of REAL+ such that
A1: x + z0 = y by ARYTM_2:9;
x + z + z0 = y + z by A1,ARYTM_2:6;
hence thesis by ARYTM_2:19;
end;
assume x + z <=' y + z;
then consider z0 being Element of REAL+ such that
A2: x + z + z0 = y + z by ARYTM_2:9;
y + z = x + z0 + z by A2,ARYTM_2:6;
hence thesis by ARYTM_2:11,19;
end;
theorem Th8:
x <=' y implies x *' z <=' y *' z
proof
assume x <=' y;
then consider z0 being Element of REAL+ such that
A1: x + z0 = y by ARYTM_2:9;
y *' z = x *' z + z0 *' z by A1,ARYTM_2:13;
hence thesis by ARYTM_2:19;
end;
Lm2: x *' y <=' x *' z & x <> {} implies y <=' z
proof
reconsider u = one as Element of REAL+ by ARYTM_2:20;
assume x *' y <=' x *' z;
then consider z0 being Element of REAL+ such that
A1: x *' y + z0 = x *' z by ARYTM_2:9;
assume
A2: x <> {};
then consider x1 being Element of REAL+ such that
A3: x *' x1 = one by ARYTM_2:14;
x *' z = x *' y + u *' z0 by A1,ARYTM_2:15
.= x *' y + x *' (x1 *' z0) by A3,ARYTM_2:12
.= x *' (y + x1 *' z0) by ARYTM_2:13;
hence thesis by A2,Lm1,ARYTM_2:19;
end;
definition
let x,y be Element of REAL+;
func x -' y -> Element of REAL+ means
:Def1:
it + y = x if y <=' x otherwise it = {};
existence
proof
hereby
assume y <=' x;
then ex IT being Element of REAL+ st y + IT = x by ARYTM_2:9;
hence ex IT being Element of REAL+ st IT + y = x;
end;
thus thesis by ARYTM_2:20;
end;
correctness by ARYTM_2:11;
end;
Lm3: x -' x = {}
proof
x <=' x;
then x -' x + x = x by Def1;
hence thesis by Th1;
end;
theorem Th9:
x <=' y or x -' y <> {}
proof
assume
A1: not x <=' y;
assume
A2: x -' y = {};
x -' y + y = x by A1,Def1;
then x = y by A2,ARYTM_2:def 8;
hence contradiction by A1;
end;
theorem
x <=' y & y -' x = {} implies x = y
proof
assume
A1: x <=' y;
assume y -' x = {};
then y <=' x by Th9;
hence thesis by A1,Th4;
end;
theorem Th11:
x -' y <=' x
proof
per cases;
suppose
y <=' x;
then x -' y + y = x by Def1;
hence thesis by ARYTM_2:19;
end;
suppose
not y <=' x;
then x -' y = {} by Def1;
hence thesis by Th6;
end;
end;
Lm4: x = {} implies y -' x = y
proof
assume
A1: x = {};
then
A2: x <=' y by Th6;
thus y -' x = y -' x + x by A1,ARYTM_2:def 8
.= y by A2,Def1;
end;
Lm5: x + y -' y = x
proof
y <=' x + y by ARYTM_2:19;
hence thesis by Def1;
end;
Lm6: x <=' y implies y -' (y -' x) = x
proof
assume
A1: x <=' y;
y -' x <=' y by Th11;
then y -' (y -' x) + (y -' x) = y by Def1
.= y -' x + x by A1,Def1;
hence thesis by ARYTM_2:11;
end;
Lm7: z -' y <=' x iff z <=' x + y
proof
per cases;
suppose
y <=' z;
then z -' y + y = z by Def1;
hence thesis by Th7;
end;
suppose
A1: not y <=' z;
A2: y <=' x + y by ARYTM_2:19;
z -' y = {} by A1,Def1;
hence thesis by A1,A2,Th3,Th6;
end;
end;
Lm8: y <=' x implies (z + y <=' x iff z <=' x -' y)
proof
assume y <=' x;
then x -' y + y = x by Def1;
hence thesis by Th7;
end;
Lm9: z -' y -' x = z -' (x + y)
proof
per cases;
suppose
A1: x + y <=' z;
y <=' x + y by ARYTM_2:19;
then
A2: y <=' z by A1,Th3;
then
A3: x <=' z -' y by A1,Lm8;
z -' y -' x + (x + y) = z -' y -' x + x + y by ARYTM_2:6
.= z -' y + y by A3,Def1
.= z by A2,Def1;
hence thesis by A1,Def1;
end;
suppose
A4: x = {};
hence z -' y -' x = z -' y by Lm4
.= z -' (x + y) by A4,ARYTM_2:def 8;
end;
suppose that
A5: not y <=' z and
A6: x <> {};
y <=' y + x by ARYTM_2:19;
then
A7: not x + y <=' z by A5,Th3;
now
assume
A8: x <=' z -' y;
z -' y = {} by A5,Def1;
hence contradiction by A6,A8,Th5;
end;
hence z -' y -' x = {} by Def1
.= z -' (x + y) by A7,Def1;
end;
suppose that
A9: not x + y <=' z and
A10: y <=' z;
not x <=' z -' y by A9,A10,Lm8;
hence z -' y -' x = {} by Def1
.= z -' (x + y) by A9,Def1;
end;
end;
Lm10: y -' z -' x = y -' x -' z
proof
thus y -' z -' x = y -' (x + z) by Lm9
.= y -' x -' z by Lm9;
end;
theorem
y <=' x & y <=' z implies x + (z -' y) = x -' y + z
proof
assume that
A1: y <=' x and
A2: y <=' z;
x + (z -' y) + y = x + ((z -' y) + y) by ARYTM_2:6
.= x + z by A2,Def1
.= x -' y + y + z by A1,Def1
.= x -' y + z + y by ARYTM_2:6;
hence thesis by ARYTM_2:11;
end;
theorem Th13:
z <=' y implies x + (y -' z) = x + y -' z
proof
assume
A1: z <=' y;
y <=' x + y by ARYTM_2:19;
then
A2: z <=' x + y by A1,Th3;
x + (y -' z) + z = x + ((y -' z) + z) by ARYTM_2:6
.= x + y by A1,Def1
.= x + y -' z + z by A2,Def1;
hence thesis by ARYTM_2:11;
end;
Lm11: y <=' z implies x -' (z -' y) = x + y -' z
proof
assume
A1: y <=' z;
per cases;
suppose
A2: z -' y <=' x;
then
A3: z <=' x + y by Lm7;
x -' (z -' y) + (z -' y) = x by A2,Def1
.= (x + z) -' z by Lm5
.= (x + (y + (z -' y))) -' z by A1,Def1
.= (x + y + (z -' y)) -' z by ARYTM_2:6
.= x + y -' z + (z -' y) by A3,Th13;
hence thesis by ARYTM_2:11;
end;
suppose
A4: not z -' y <=' x;
then
A5: not z <=' x + y by Lm7;
thus x -' (z -' y) = {} by A4,Def1
.= x + y -' z by A5,Def1;
end;
end;
Lm12: z <=' x & y <=' z implies x -' (z -' y) = x -' z + y
proof
assume that
A1: z <=' x and
A2: y <=' z;
thus x -' (z -' y) = x + y -' z by A2,Lm11
.= x -' z + y by A1,Th13;
end;
Lm13: x <=' z & y <=' z implies x -' (z -' y) = y -' (z -' x)
proof
assume that
A1: x <=' z and
A2: y <=' z;
thus x -' (z -' y) = x + y -' z by A2,Lm11
.= y -' (z -' x) by A1,Lm11;
end;
theorem
z <=' x & y <=' z implies x -' z + y = x -' (z -' y)
proof
assume that
A1: z <=' x and
A2: y <=' z;
thus x -' (z -' y) = x + y -' z by A2,Lm11
.= x -' z + y by A1,Th13;
end;
theorem
y <=' x & y <=' z implies z -' y + x = x -' y + z
proof
assume that
A1: y <=' x and
A2: y <=' z;
z -' y + x + y = z -' y + y + x by ARYTM_2:6
.= z + x by A2,Def1
.= x -' y + y + z by A1,Def1
.= x -' y + z + y by ARYTM_2:6;
hence thesis by ARYTM_2:11;
end;
theorem
x <=' y implies z -' y <=' z -' x
proof
assume
A1: x <=' y;
per cases;
suppose
A2: y <=' z;
z -' y + x <=' z -' y + y by A1,Th7;
then
A3: z -' y + x <=' z by A2,Def1;
x <=' z by A1,A2,Th3;
then z -' y + x <=' z -' x + x by A3,Def1;
hence thesis by Th7;
end;
suppose
not y <=' z;
then z -' y = {} by Def1;
hence thesis by Th6;
end;
end;
theorem
x <=' y implies x -' z <=' y -' z
proof
assume
A1: x <=' y;
per cases;
suppose
A2: z <=' x;
then z <=' y by A1,Th3;
then
A3: y -' z + z = y by Def1;
x -' z + z = x by A2,Def1;
hence thesis by A1,A3,Th7;
end;
suppose
not z <=' x;
then x -' z = {} by Def1;
hence thesis by Th6;
end;
end;
Lm14: x *' (y -' z) = (x *' y) -' (x *' z)
proof
per cases;
suppose
A1: z <=' y;
then
A2: x *' z <=' x *' y by Th8;
x *' (y -' z) + (x *' z) = x *' (y -' z + z) by ARYTM_2:13
.= x *' y by A1,Def1
.= (x *' y) -' (x *' z) + (x *' z) by A2,Def1;
hence thesis by ARYTM_2:11;
end;
suppose
A3: x = {};
then x *' y = {} by ARYTM_2:4;
hence x *' (y -' z) = x *' y by A3,ARYTM_2:4
.= (x *' y) -' (x *' z) by A3,Lm4,ARYTM_2:4;
end;
suppose
A4: not z <=' y & x <> {};
then
A5: not x *' z <=' x *' y by Lm2;
y -' z = {} by A4,Def1;
hence x *' (y -' z) = {} by ARYTM_2:4
.= (x *' y) -' (x *' z) by A5,Def1;
end;
end;
definition
let x,y be Element of REAL+;
func x - y -> set equals
:Def2:
x -' y if y <=' x otherwise [{},y -' x];
correctness by TARSKI:1;
end;
theorem
x - x = {}
proof
x <=' x;
then x - x = x -' x by Def2;
hence thesis by Lm3;
end;
theorem
x = {} & y <> {} implies x - y = [{},y]
proof
assume that
A1: x = {} and
A2: y <> {};
x <=' y by A1,Th6;
then not y <=' x by A1,A2,Th4;
hence x - y =[{},y -' x] by Def2
.= [{},y] by A1,Lm4;
end;
theorem
z <=' y implies x + (y -' z) = x + y - z
proof
assume
A1: z <=' y;
y <=' x + y by ARYTM_2:19;
then z <=' x + y by A1,Th3;
then x + y - z = x + y -' z by Def2;
hence thesis by A1,Th13;
end;
theorem
not z <=' y implies x - (z -' y) = x + y - z
proof
assume
A1: not z <=' y;
per cases;
suppose
A2: z -' y <=' x;
then z <=' x + y by Lm7;
then
A3: x + y - z = x + y -' z by Def2;
x - (z -' y) = x -' (z -' y) by A2,Def2;
hence thesis by A1,A3,Lm11;
end;
suppose
A4: not z -' y <=' x;
then
A5: not z <=' x + y by Lm7;
(z -' y) -' x = z -' (x + y) by Lm9;
hence x - (z -' y) = [{},z -' (x + y)] by A4,Def2
.= x + y - z by A5,Def2;
end;
end;
theorem
y <=' x & not y <=' z implies x - (y -' z) = x -' y + z
proof
assume that
A1: y <=' x and
A2: not y <=' z;
y -' z <=' y by Th11;
then y -' z <=' x by A1,Th3;
then x - (y -' z) = x -' (y -' z) by Def2;
hence thesis by A1,A2,Lm12;
end;
theorem
not y <=' x & not y <=' z implies x - (y -' z) = z - (y -' x)
proof
assume
A1: ( not y <=' x)& not y <=' z;
per cases;
suppose
A2: y <=' x + z;
then y -' x <=' z by Lm7;
then
A3: z - (y -' x) = z -' (y -' x) by Def2;
y -' z <=' x by A2,Lm7;
then x - (y -' z) = x -' (y -' z) by Def2;
hence thesis by A1,A3,Lm13;
end;
suppose
A4: not y <=' x + z;
then
A5: not y -' x <=' z by Lm7;
A6: y -' z -' x = y -' x -' z by Lm10;
not y -' z <=' x by A4,Lm7;
hence x - (y -' z) = [{},y -' x -' z] by A6,Def2
.= z - (y -' x) by A5,Def2;
end;
end;
theorem
y <=' x implies x - (y + z) = x -' y - z
proof
assume
A1: y <=' x;
per cases;
suppose
A2: y + z <=' x;
then z <=' x -' y by A1,Lm8;
then
A3: x -' y - z = x -' y -' z by Def2;
x - (y + z) = x -' (y + z) by A2,Def2;
hence thesis by A3,Lm9;
end;
suppose that
A4: not y + z <=' x and
A5: x <=' y;
A6: not z <=' x -' y by A1,A4,Lm8;
A7: (x + z) -' x = z by Lm5
.= z -' (x -' x) by Lm3,Lm4;
x = y by A1,A5,Th4;
hence x - (y + z) = [{},z -' (x -' y)] by A4,A7,Def2
.= x -' y - z by A6,Def2;
end;
suppose that
A8: not y + z <=' x and
A9: not x <=' y;
A10: not z <=' x -' y by A1,A8,Lm8;
y + z -' x = z -' (x -' y) by A9,Lm11;
hence x - (y + z) = [{},z -' (x -' y)] by A8,Def2
.= x -' y - z by A10,Def2;
end;
end;
theorem
x <=' y & z <=' y implies y -' z - x = y -' x - z
proof
assume that
A1: x <=' y and
A2: z <=' y;
per cases;
suppose
A3: x + z <=' y;
then z <=' y -' x by A1,Lm8;
then
A4: y -' x -' z = y -' x - z by Def2;
x <=' y -' z by A2,A3,Lm8;
then y -' z -' x = y -' z - x by Def2;
hence thesis by A4,Lm10;
end;
suppose that
A5: not x + z <=' y and
A6: y <=' x;
A7: not x <=' y -' z by A2,A5,Lm8;
A8: not z <=' y -' x by A1,A5,Lm8;
A9: x = y by A1,A6,Th4;
then x -' (x -' z) = z by A2,Lm6
.= z -' (x -' x) by Lm3,Lm4;
hence y -' z - x = [{},z -' (y -' x)] by A7,A9,Def2
.= y -' x - z by A8,Def2;
end;
suppose that
A10: not x + z <=' y and
A11: y <=' z;
A12: not x <=' y -' z by A2,A10,Lm8;
A13: not z <=' y -' x by A1,A10,Lm8;
A14: z = y by A2,A11,Th4;
x -' (z -' z) = x by Lm3,Lm4
.= z -' (z -' x) by A1,A14,Lm6;
hence y -' z - x = [{},z -' (y -' x)] by A12,A14,Def2
.= y -' x - z by A13,Def2;
end;
suppose that
A15: not x + z <=' y and
A16: not y <=' x & not y <=' z;
A17: not z <=' y -' x by A1,A15,Lm8;
( not x <=' y -' z)& x -' (y -' z) = z -' (y -' x) by A15,A16,Lm8,Lm13;
hence y -' z - x = [{},z -' (y -' x)] by Def2
.= y -' x - z by A17,Def2;
end;
end;
theorem
z <=' y implies x *' (y -' z) = (x *' y) - (x *' z)
proof
assume z <=' y;
then x *' z <=' x *' y by Th8;
then (x *' y) - (x *' z) = (x *' y) -' (x *' z) by Def2;
hence thesis by Lm14;
end;
theorem Th27:
not z <=' y & x <> {} implies [{},x *' (z -' y)] = (x *' y) - (x *' z)
proof
assume ( not z <=' y)& x <> {};
then
A1: not x *' z <=' x *' y by Lm2;
thus [{},x *' (z -' y)] = [{},(x *' z) -' (x *' y)] by Lm14
.= (x *' y) - (x *' z) by A1,Def2;
end;
theorem
y -' z <> {} & z <=' y & x <> {} implies (x *' z) - (x *' y) = [{},x
*' (y -' z)]
proof
assume y -' z <> {};
then
A1: y <> z by Lm3;
assume z <=' y;
then not y <=' z by A1,Th4;
hence thesis by Th27;
end;