:: by Library Committee

::

:: Received February 9, 2005

:: Copyright (c) 2005-2016 Association of Mizar Users

Lm1: for r, s being Real st ( ( 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+:] ) ) holds

r <= s

proof end;

Lm2: for a being Real

for x1, x2 being Element of REAL st a = [*x1,x2*] holds

( x2 = 0 & a = x1 )

proof end;

Lm3: for a9, b9 being Element of REAL

for a, b being Real st a9 = a & b9 = b holds

+ (a9,b9) = a + b

proof end;

Lm4: {} in {{}}

by TARSKI:def 1;

Lm5: for a, b, c being Real st a <= b holds

a + c <= b + c

proof end;

Lm6: for a, b, c, d being Real st a <= b & c <= d holds

a + c <= b + d

proof end;

Lm7: for a, b, c being Real st a <= b holds

a - c <= b - c

proof end;

Lm8: for a, b, c, d being Real st a < b & c <= d holds

a + c < b + d

proof end;

Lm9: for a, b being Real st 0 < a holds

b < b + a

proof end;

Lm10: for a, b, c being Real st a + c <= b + c holds

a <= b

proof end;

Lm11: for a9, b9 being Element of REAL

for a, b being Real st a9 = a & b9 = b holds

* (a9,b9) = a * b

proof end;

reconsider o = 0 as Element of REAL+ by ARYTM_2:20;

Lm12: for a, b, c being Real st a <= b & 0 <= c holds

a * c <= b * c

proof end;

Lm13: for a, b, c being Real st 0 < c & a < b holds

a * c < b * c

proof end;

Lm14: for a, b being Real st a <= b holds

- b <= - a

proof end;

Lm15: for a, b being Real st - b <= - a holds

a <= b

proof end;

Lm16: for a, b, c being Real st a + b <= c holds

a <= c - b

proof end;

Lm17: for a, b, c being Real st a <= b - c holds

a + c <= b

proof end;

Lm18: for a, b, c being Real st a <= b + c holds

a - b <= c

proof end;

Lm19: for a, b, c being Real st a - b <= c holds

a <= b + c

proof end;

Lm20: for a, b, c, d being Real st a + b <= c + d holds

a - c <= d - b

proof end;

Lm21: for a, b being Real st a < b holds

0 < b - a

proof end;

Lm22: for a, b being Real st a <= b holds

0 <= b - a

proof end;

Lm23: for a, b being Real st a < b holds

a - b < 0

proof end;

Lm24: for a, b, c being Real st c < 0 & a < b holds

b * c < a * c

proof end;

Lm25: for a, b, c being Real st 0 <= c & b <= a holds

b / c <= a / c

proof end;

Lm26: for a, b, c being Real st 0 < c & a < b holds

a / c < b / c

proof end;

Lm27: for a being Real st 0 < a holds

a / 2 < a

proof end;

Lm28: for a, b, c being Real st a <= b & c <= 0 holds

b * c <= a * c

proof end;

theorem :: XREAL_1:71

Lm29: for a, b, c being Real st c < 0 & a < b holds

b / c < a / c

proof end;

Lm30: for a, b, c being Real st c <= 0 & b / c < a / c holds

a < b

proof end;

Lm31: for a, b being Real st b < 0 & a < b holds

b " < a "

proof end;

Lm32: for a, b being Real st 0 < a & a <= b holds

b " <= a "

proof end;

Lm33: for a, b being Real st b < 0 & a <= b holds

b " <= a "

proof end;

Lm34: for a, b being Real st 0 < a & a < b holds

b " < a "

proof end;

Lm35: for b being Real

for a being non positive non negative Real holds 0 = a * b

;

Lm36: for a being Real st 1 < a holds

a " < 1

proof end;

Lm37: for a, b being Real st a <= b & 0 <= a holds

a / b <= 1

proof end;

Lm38: for a, b being Real st b <= a & 0 <= a holds

b / a <= 1

proof end;

theorem :: XREAL_1:170

for a, b, d being Real st 0 <= d & d <= 1 & 0 <= a & 0 <= b & (d * a) + ((1 - d) * b) = 0 & not ( d = 0 & b = 0 ) & not ( d = 1 & a = 0 ) holds

( a = 0 & b = 0 )

( a = 0 & b = 0 )

proof end;

theorem :: XREAL_1:179

for a, b, d being Real st 0 <= d & d <= 1 & a <= ((1 - d) * a) + (d * b) & b < ((1 - d) * a) + (d * b) holds

d = 0

d = 0

proof end;

theorem :: XREAL_1:180

for a, b, d being Real st 0 <= d & d <= 1 & ((1 - d) * a) + (d * b) <= a & ((1 - d) * a) + (d * b) < b holds

d = 0

d = 0

proof end;

:: from TOPREAL3, 2006.07.15, A.T.

:: missing, 2007.01.16, A.T.

theorem :: XREAL_1:228

for r, s, t being ExtReal st r < s & ( for q being ExtReal st r < q & q < s holds

t <= q ) holds

t <= r

t <= q ) holds

t <= r

proof end;

theorem :: XREAL_1:229

for r, s, t being ExtReal st r < s & ( for q being ExtReal st r < q & q < s holds

q <= t ) holds

s <= t

q <= t ) holds

s <= t

proof end;

:: missing, 2008.08.13, A.T.

:: from LEXBFS, 2008.08.23, A.T.

:: missing, 2010.05.18, A.T.