:: by Library Committee

::

:: Received February 9, 2005

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

begin

Lm1: for r, s being real number 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 number

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 number 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 number st a <= b holds

a + c <= b + c

proof end;

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

a + c <= b + d

proof end;

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

a - c <= b - c

proof end;

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

a + c < b + d

proof end;

Lm9: for a, b being real number st 0 < a holds

b < b + a

proof end;

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

a <= b

proof end;

Lm11: for a9, b9 being Element of REAL

for a, b being real number 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 number st a <= b & 0 <= c holds

a * c <= b * c

proof end;

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

a * c < b * c

proof end;

begin

theorem :: XREAL_1:6

theorem :: XREAL_1:7

Lm14: for a, b being real number st a <= b holds

- b <= - a

proof end;

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

a <= b

proof end;

begin

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

a <= c - b

proof end;

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

a + c <= b

proof end;

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

a - b <= c

proof end;

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

a <= b + c

proof end;

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

a - c <= d - b

proof end;

begin

theorem :: XREAL_1:19

theorem :: XREAL_1:20

begin

Lm21: for a, b being real number st a < b holds

0 < b - a

proof end;

Lm22: for a, b being real number st a <= b holds

0 <= b - a

proof end;

begin

begin

Lm23: for a, b being real number st a < b holds

a - b < 0

proof end;

begin

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

b * c < a * c

proof end;

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

b / c <= a / c

proof end;

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

a / c < b / c

proof end;

Lm27: for a being real number st 0 < a holds

a / 2 < a

proof end;

begin

begin

begin

begin

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

b * c <= a * c

proof end;

begin

theorem :: XREAL_1:64

theorem :: XREAL_1:65

begin

theorem :: XREAL_1:71

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

b / c < a / c

proof end;

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

a < b

proof end;

begin

theorem :: XREAL_1:72

theorem :: XREAL_1:73

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

b " < a "

proof end;

begin

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

b " <= a "

proof end;

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

b " <= a "

proof end;

begin

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

b " < a "

proof end;

Lm35: for b being real number

for a being non positive non negative real number holds 0 = a * b

;

begin

begin

begin

begin

begin

Lm36: for a being real number st 1 < a holds

a " < 1

proof end;

theorem :: XREAL_1:168

for b, c being real number st ( for a being real number st 0 < a & a < 1 holds

b * a <= c ) holds

b <= c

b * a <= c ) holds

b <= c

proof end;

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

a / b <= 1

proof end;

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

b / a <= 1

proof end;

theorem :: XREAL_1:169

for b, c being real number st ( for a being real number st 0 < a & a < 1 holds

b <= a * c ) holds

b <= 0

b <= a * c ) holds

b <= 0

proof end;

theorem :: XREAL_1:170

for d, a, b being real number 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:173

for d, a, b, c being real number st 0 <= d & d <= 1 & a <= b & a <= c holds

a <= ((1 - d) * b) + (d * c)

a <= ((1 - d) * b) + (d * c)

proof end;

theorem :: XREAL_1:174

for d, b, a, c being real number st 0 <= d & d <= 1 & b <= a & c <= a holds

((1 - d) * b) + (d * c) <= a

((1 - d) * b) + (d * c) <= a

proof end;

theorem :: XREAL_1:175

for d, a, b, c being real number st 0 <= d & d <= 1 & a < b & a < c holds

a < ((1 - d) * b) + (d * c)

a < ((1 - d) * b) + (d * c)

proof end;

theorem :: XREAL_1:176

for d, b, a, c being real number st 0 <= d & d <= 1 & b < a & c < a holds

((1 - d) * b) + (d * c) < a

((1 - d) * b) + (d * c) < a

proof end;

theorem :: XREAL_1:177

for d, a, b, c being real number st 0 < d & d < 1 & a <= b & a < c holds

a < ((1 - d) * b) + (d * c)

a < ((1 - d) * b) + (d * c)

proof end;

theorem :: XREAL_1:178

for d, b, a, c being real number st 0 < d & d < 1 & b < a & c <= a holds

((1 - d) * b) + (d * c) < a

((1 - d) * b) + (d * c) < a

proof end;

theorem :: XREAL_1:179

for d, a, b being real number 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 d, a, b being real number st 0 <= d & d <= 1 & ((1 - d) * a) + (d * b) <= a & ((1 - d) * a) + (d * b) < b holds

d = 0

d = 0

proof end;

begin

begin

begin

theorem Th209: :: XREAL_1:209

for c, b being real number st ( for a being real number st 0 < a & a < 1 holds

c <= b / a ) holds

c <= b

c <= b / a ) holds

c <= b

proof end;

begin

begin

begin

begin

:: from TOPREAL3, 2006.07.15, A.T.

:: missing, 2007.01.16, A.T.

theorem :: XREAL_1:228

for r, s, t being ext-real number st r < s & ( for q being ext-real number 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 ext-real number st r < s & ( for q being ext-real number st r < q & q < s holds

q <= t ) holds

s <= t

q <= t ) holds

s <= t

proof end;

:: missing, 2008.08.13, A.T.

begin

:: from LEXBFS, 2008.08.23, A.T.

:: missing, 2010.05.18, A.T.