:: Non negative real numbers. Part II
:: by Andrzej Trybulec
::
:: Received March 7, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem Th1: :: ARYTM_1:1
reconsider u = one as Element of REAL+ by ARYTM_2:21;
Lm1:
for x, y, z being Element of REAL+ st x *' y = x *' z & x <> {} holds
y = z
theorem :: ARYTM_1:2
theorem Th3: :: ARYTM_1:3
theorem Th4: :: ARYTM_1:4
theorem Th5: :: ARYTM_1:5
theorem Th6: :: ARYTM_1:6
theorem Th7: :: ARYTM_1:7
theorem Th8: :: ARYTM_1:8
Lm2:
for x, y, z being Element of REAL+ st x *' y <=' x *' z & x <> {} holds
y <=' z
:: deftheorem Def1 defines -' ARYTM_1:def 1 :
for
x,
y,
b3 being
Element of
REAL+ holds
( (
y <=' x implies (
b3 = x -' y iff
b3 + y = x ) ) & ( not
y <=' x implies (
b3 = x -' y iff
b3 = {} ) ) );
Lm3:
for x being Element of REAL+ holds x -' x = {}
theorem Th9: :: ARYTM_1:9
theorem :: ARYTM_1:10
theorem Th11: :: ARYTM_1:11
Lm4:
for x, y being Element of REAL+ st x = {} holds
y -' x = y
Lm5:
for x, y being Element of REAL+ holds (x + y) -' y = x
Lm6:
for x, y being Element of REAL+ st x <=' y holds
y -' (y -' x) = x
Lm7:
for z, y, x being Element of REAL+ holds
( z -' y <=' x iff z <=' x + y )
Lm8:
for y, x, z being Element of REAL+ st y <=' x holds
( z + y <=' x iff z <=' x -' y )
Lm9:
for z, y, x being Element of REAL+ holds (z -' y) -' x = z -' (x + y)
Lm10:
for y, z, x being Element of REAL+ holds (y -' z) -' x = (y -' x) -' z
theorem :: ARYTM_1:12
theorem Th13: :: ARYTM_1:13
Lm11:
for y, z, x being Element of REAL+ st y <=' z holds
x -' (z -' y) = (x + y) -' z
Lm12:
for z, x, y being Element of REAL+ st z <=' x & y <=' z holds
x -' (z -' y) = (x -' z) + y
Lm13:
for x, z, y being Element of REAL+ st x <=' z & y <=' z holds
x -' (z -' y) = y -' (z -' x)
theorem :: ARYTM_1:14
theorem :: ARYTM_1:15
theorem :: ARYTM_1:16
theorem :: ARYTM_1:17
Lm14:
for x, y, z being Element of REAL+ holds x *' (y -' z) = (x *' y) -' (x *' z)
:: deftheorem Def2 defines - ARYTM_1:def 2 :
theorem :: ARYTM_1:18
theorem :: ARYTM_1:19
theorem :: ARYTM_1:20
theorem :: ARYTM_1:21
theorem :: ARYTM_1:22
theorem :: ARYTM_1:23
theorem :: ARYTM_1:24
theorem :: ARYTM_1:25
theorem :: ARYTM_1:26
theorem Th27: :: ARYTM_1:27
theorem :: ARYTM_1:28