:: Real Numbers - Basic Theorems
:: 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;

theorem Th1: :: XREAL_1:1
for a being real number ex b being real number st a < b
proof end;

theorem Th2: :: XREAL_1:2
for a being real number ex b being real number st b < a
proof end;

theorem :: XREAL_1:3
for a, b being real number ex c being real number st
( a < c & b < c )
proof end;

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

theorem :: XREAL_1:4
for a, b being real number ex c being real number st
( c < a & c < 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;

theorem Th5: :: XREAL_1:5
for a, b being real number st a < b holds
ex c being real number st
( a < c & c < b )
proof end;

begin

theorem :: XREAL_1:6
for a, b, c being real number holds
( a <= b iff a + c <= b + c ) by Lm5, Lm10;

theorem :: XREAL_1:7
for a, b, c, d being real number st a <= b & c <= d holds
a + c <= b + d by Lm6;

theorem :: XREAL_1:8
for a, b, c, d being real number st a < b & c <= d holds
a + c < b + d by Lm8;

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

theorem Th9: :: XREAL_1:9
for a, b, c being real number holds
( a <= b iff a - c <= b - c )
proof end;

theorem :: XREAL_1:10
for a, b, c being real number holds
( a <= b iff c - b <= c - a )
proof end;

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;

theorem :: XREAL_1:11
for a, b, c being real number st a <= b - c holds
c <= b - a
proof end;

theorem :: XREAL_1:12
for a, b, c being real number st a - b <= c holds
a - c <= b
proof end;

theorem Th13: :: XREAL_1:13
for a, b, c, d being real number st a <= b & c <= d holds
a - d <= b - c
proof end;

theorem Th14: :: XREAL_1:14
for a, b, c, d being real number st a < b & c <= d holds
a - d < b - c
proof end;

theorem Th15: :: XREAL_1:15
for a, b, c, d being real number st a <= b & c < d holds
a - d < 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;

theorem :: XREAL_1:16
for a, b, c, d being real number st a - b <= c - d holds
a - c <= b - d
proof end;

theorem :: XREAL_1:17
for a, b, c, d being real number st a - b <= c - d holds
d - b <= c - a
proof end;

theorem :: XREAL_1:18
for a, b, c, d being real number st a - b <= c - d holds
d - c <= b - a
proof end;

begin

theorem :: XREAL_1:19
for a, b, c being real number holds
( a + b <= c iff a <= c - b ) by Lm16, Lm17;

theorem :: XREAL_1:20
for a, b, c being real number holds
( a <= b + c iff a - b <= c ) by Lm18, Lm19;

theorem :: XREAL_1:21
for a, b, c, d being real number holds
( a + b <= c + d iff a - c <= d - b )
proof end;

theorem :: XREAL_1:22
for a, b, c, d being real number st a + b <= c - d holds
a + d <= c - b
proof end;

theorem :: XREAL_1:23
for a, b, c, d being real number st a - b <= c + d holds
a - d <= c + b
proof end;

begin

theorem :: XREAL_1:24
for a, b being real number holds
( a <= b iff - b <= - a ) by Lm14, Lm15;

Lm21: for a, b being real number st a < b holds
0 < b - a
proof end;

theorem Th25: :: XREAL_1:25
for a, b being real number st a <= - b holds
b <= - a
proof end;

Lm22: for a, b being real number st a <= b holds
0 <= b - a
proof end;

theorem Th26: :: XREAL_1:26
for b, a being real number st - b <= a holds
- a <= b
proof end;

begin

theorem :: XREAL_1:27
for a, b being real number st 0 <= a & 0 <= b & a + b = 0 holds
a = 0 ;

theorem :: XREAL_1:28
for a, b being real number st a <= 0 & b <= 0 & a + b = 0 holds
a = 0 ;

begin

theorem :: XREAL_1:29
for a, b being real number st 0 < a holds
b < b + a by Lm9;

theorem :: XREAL_1:30
for a, b being real number st a < 0 holds
a + b < b
proof end;

Lm23: for a, b being real number st a < b holds
a - b < 0
proof end;

theorem :: XREAL_1:31
for a, b being real number st 0 <= a holds
b <= a + b
proof end;

theorem :: XREAL_1:32
for a, b being real number st a <= 0 holds
a + b <= b
proof end;

begin

theorem :: XREAL_1:33
for a, b being real number st 0 <= a & 0 <= b holds
0 <= a + b ;

theorem :: XREAL_1:34
for a, b being real number st 0 <= a & 0 < b holds
0 < a + b ;

theorem Th35: :: XREAL_1:35
for a, c, b being real number st a <= 0 & c <= b holds
c + a <= b
proof end;

theorem Th36: :: XREAL_1:36
for a, c, b being real number st a <= 0 & c < b holds
c + a < b
proof end;

theorem Th37: :: XREAL_1:37
for a, c, b being real number st a < 0 & c <= b holds
c + a < b
proof end;

theorem Th38: :: XREAL_1:38
for a, b, c being real number st 0 <= a & b <= c holds
b <= a + c
proof end;

theorem Th39: :: XREAL_1:39
for a, b, c being real number st 0 < a & b <= c holds
b < a + c
proof end;

theorem Th40: :: XREAL_1:40
for a, b, c being real number st 0 <= a & b < c holds
b < a + c
proof end;

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

theorem :: XREAL_1:41
for c, b being real number st ( for a being real number st a > 0 holds
c <= b + a ) holds
c <= b
proof end;

theorem :: XREAL_1:42
for b, c being real number st ( for a being real number st a < 0 holds
b + a <= c ) holds
b <= c
proof end;

begin

theorem :: XREAL_1:43
for a, b being real number st 0 <= a holds
b - a <= b
proof end;

theorem Th44: :: XREAL_1:44
for a, b being real number st 0 < a holds
b - a < b
proof end;

theorem :: XREAL_1:45
for a, b being real number st a <= 0 holds
b <= b - a
proof end;

theorem :: XREAL_1:46
for a, b being real number st a < 0 holds
b < b - a
proof end;

theorem :: XREAL_1:47
for a, b being real number st a <= b holds
a - b <= 0
proof end;

theorem Th48: :: XREAL_1:48
for a, b being real number st a <= b holds
0 <= b - a
proof end;

theorem :: XREAL_1:49
for a, b being real number st a < b holds
a - b < 0 by Lm23;

theorem :: XREAL_1:50
for a, b being real number st a < b holds
0 < b - a by Lm21;

theorem :: XREAL_1:51
for a, b, c being real number st 0 <= a & b < c holds
b - a < c
proof end;

theorem :: XREAL_1:52
for a, b, c being real number st a <= 0 & b <= c holds
b <= c - a
proof end;

theorem :: XREAL_1:53
for a, b, c being real number st a <= 0 & b < c holds
b < c - a
proof end;

theorem :: XREAL_1:54
for a, b, c being real number st a < 0 & b <= c holds
b < c - a
proof end;

theorem :: XREAL_1:55
for a, b being real number holds
( not a <> b or 0 < a - b or 0 < b - a )
proof end;

begin

theorem :: XREAL_1:56
for c, b being real number st ( for a being real number st a < 0 holds
c <= b - a ) holds
b >= c
proof end;

theorem :: XREAL_1:57
for b, c being real number st ( for a being real number st a > 0 holds
b - a <= c ) holds
b <= c
proof end;

begin

theorem :: XREAL_1:58
for a being real number holds
( a < 0 iff 0 < - a ) ;

theorem :: XREAL_1:59
for a, b being real number st a <= - b holds
a + b <= 0
proof end;

theorem :: XREAL_1:60
for a, b being real number st - a <= b holds
0 <= a + b
proof end;

theorem :: XREAL_1:61
for a, b being real number st a < - b holds
a + b < 0
proof end;

theorem :: XREAL_1:62
for b, a being real number st - b < a holds
0 < a + b
proof end;

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

begin

theorem :: XREAL_1:63
for a being real number holds 0 <= a * a
proof end;

theorem :: XREAL_1:64
for a, b, c being real number st a <= b & 0 <= c holds
a * c <= b * c by Lm12;

theorem :: XREAL_1:65
for a, b, c being real number st a <= b & c <= 0 holds
b * c <= a * c by Lm28;

theorem Th66: :: XREAL_1:66
for a, b, c, d being real number st 0 <= a & a <= b & 0 <= c & c <= d holds
a * c <= b * d
proof end;

theorem :: XREAL_1:67
for a, b, c, d being real number st a <= 0 & b <= a & c <= 0 & d <= c holds
a * c <= b * d
proof end;

theorem :: XREAL_1:68
for c, a, b being real number st 0 < c & a < b holds
a * c < b * c by Lm13;

theorem :: XREAL_1:69
for c, a, b being real number st c < 0 & a < b holds
b * c < a * c by Lm24;

theorem :: XREAL_1:70
for a, b, c, d being real number st a < 0 & b <= a & c < 0 & d < c holds
a * c < b * d
proof end;

begin

theorem :: XREAL_1:71
for a, b, c, d being real number st 0 <= a & 0 <= b & 0 <= c & 0 <= d & (a * c) + (b * d) = 0 & not a = 0 holds
c = 0 ;

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

theorem :: XREAL_1:73
for c, a, b being real number st c <= 0 & a <= b holds
b / c <= a / c by Lm30;

theorem :: XREAL_1:74
for c, a, b being real number st 0 < c & a < b holds
a / c < b / c by Lm26;

theorem :: XREAL_1:75
for c, a, b being real number st c < 0 & a < b holds
b / c < a / c by Lm29;

theorem :: XREAL_1:76
for c, a, b being real number st 0 < c & 0 < a & a < b holds
c / b < c / a
proof end;

Lm31: for b, a being real number st b < 0 & a < b holds
b " < a "
proof end;

begin

theorem Th77: :: XREAL_1:77
for b, a, c being real number st 0 < b & a * b <= c holds
a <= c / b
proof end;

theorem Th78: :: XREAL_1:78
for b, a, c being real number st b < 0 & a * b <= c holds
c / b <= a
proof end;

theorem Th79: :: XREAL_1:79
for b, c, a being real number st 0 < b & c <= a * b holds
c / b <= a
proof end;

theorem Th80: :: XREAL_1:80
for b, c, a being real number st b < 0 & c <= a * b holds
a <= c / b
proof end;

theorem Th81: :: XREAL_1:81
for b, a, c being real number st 0 < b & a * b < c holds
a < c / b
proof end;

theorem Th82: :: XREAL_1:82
for b, a, c being real number st b < 0 & a * b < c holds
c / b < a
proof end;

theorem Th83: :: XREAL_1:83
for b, c, a being real number st 0 < b & c < a * b holds
c / b < a
proof end;

theorem Th84: :: XREAL_1:84
for b, c, a being real number st b < 0 & c < a * b holds
a < c / b
proof end;

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

theorem :: XREAL_1:85
for a, b being real number st 0 < a & a <= b holds
b " <= a " by Lm32;

theorem :: XREAL_1:86
for b, a being real number st b < 0 & a <= b holds
b " <= a " by Lm33;

theorem :: XREAL_1:87
for b, a being real number st b < 0 & a < b holds
b " < a " by Lm31;

Lm34: for a, b being real number st 0 < a & a < b holds
b " < a "
proof end;

theorem :: XREAL_1:88
for a, b being real number st 0 < a & a < b holds
b " < a " by Lm34;

theorem :: XREAL_1:89
for b, a being real number st 0 < b " & b " <= a " holds
a <= b
proof end;

theorem :: XREAL_1:90
for a, b being real number st a " < 0 & b " <= a " holds
a <= b
proof end;

theorem :: XREAL_1:91
for b, a being real number st 0 < b " & b " < a " holds
a < b
proof end;

theorem :: XREAL_1:92
for a, b being real number st a " < 0 & b " < a " holds
a < b
proof end;

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

begin

theorem :: XREAL_1:93
for a, b being real number st 0 <= a & (b - a) * (b + a) <= 0 holds
( - a <= b & b <= a )
proof end;

theorem :: XREAL_1:94
for a, b being real number st 0 <= a & (b - a) * (b + a) < 0 holds
( - a < b & b < a )
proof end;

theorem :: XREAL_1:95
for b, a being real number holds
( not 0 <= (b - a) * (b + a) or b <= - a or a <= b )
proof end;

theorem :: XREAL_1:96
for a, c, b, d being real number st 0 <= a & 0 <= c & a < b & c < d holds
a * c < b * d
proof end;

theorem :: XREAL_1:97
for a, c, b, d being real number st 0 <= a & 0 < c & a < b & c <= d holds
a * c < b * d
proof end;

theorem Th98: :: XREAL_1:98
for a, c, b, d being real number st 0 < a & 0 < c & a <= b & c < d holds
a * c < b * d
proof end;

theorem :: XREAL_1:99
for c, b, a being real number st 0 < c & b < 0 & a < b holds
c / b < c / a
proof end;

theorem :: XREAL_1:100
for c, a, b being real number st c < 0 & 0 < a & a < b holds
c / a < c / b
proof end;

theorem :: XREAL_1:101
for c, b, a being real number st c < 0 & b < 0 & a < b holds
c / a < c / b
proof end;

theorem :: XREAL_1:102
for b, d, a, c being real number st 0 < b & 0 < d & a * d <= c * b holds
a / b <= c / d
proof end;

theorem :: XREAL_1:103
for b, d, a, c being real number st b < 0 & d < 0 & a * d <= c * b holds
a / b <= c / d
proof end;

theorem :: XREAL_1:104
for b, d, a, c being real number st 0 < b & d < 0 & a * d <= c * b holds
c / d <= a / b
proof end;

theorem :: XREAL_1:105
for b, d, a, c being real number st b < 0 & 0 < d & a * d <= c * b holds
c / d <= a / b
proof end;

theorem :: XREAL_1:106
for b, d, a, c being real number st 0 < b & 0 < d & a * d < c * b holds
a / b < c / d
proof end;

theorem :: XREAL_1:107
for b, d, a, c being real number st b < 0 & d < 0 & a * d < c * b holds
a / b < c / d
proof end;

theorem :: XREAL_1:108
for b, d, a, c being real number st 0 < b & d < 0 & a * d < c * b holds
c / d < a / b
proof end;

theorem :: XREAL_1:109
for b, d, a, c being real number st b < 0 & 0 < d & a * d < c * b holds
c / d < a / b
proof end;

theorem :: XREAL_1:110
for b, d, a, c being real number st b < 0 & d < 0 & a * b < c / d holds
a * d < c / b
proof end;

theorem :: XREAL_1:111
for b, d, a, c being real number st 0 < b & 0 < d & a * b < c / d holds
a * d < c / b
proof end;

theorem :: XREAL_1:112
for b, d, c, a being real number st b < 0 & d < 0 & c / d < a * b holds
c / b < a * d
proof end;

theorem :: XREAL_1:113
for b, d, c, a being real number st 0 < b & 0 < d & c / d < a * b holds
c / b < a * d
proof end;

theorem :: XREAL_1:114
for b, d, a, c being real number st b < 0 & 0 < d & a * b < c / d holds
c / b < a * d
proof end;

theorem :: XREAL_1:115
for b, d, a, c being real number st 0 < b & d < 0 & a * b < c / d holds
c / b < a * d
proof end;

theorem :: XREAL_1:116
for b, d, c, a being real number st b < 0 & 0 < d & c / d < a * b holds
a * d < c / b
proof end;

theorem :: XREAL_1:117
for b, d, c, a being real number st 0 < b & d < 0 & c / d < a * b holds
a * d < c / b
proof end;

theorem :: XREAL_1:118
for a, c, b being real number st 0 < a & 0 <= c & a <= b holds
c / b <= c / a
proof end;

theorem :: XREAL_1:119
for c, b, a being real number st 0 <= c & b < 0 & a <= b holds
c / b <= c / a
proof end;

theorem :: XREAL_1:120
for c, a, b being real number st c <= 0 & 0 < a & a <= b holds
c / a <= c / b
proof end;

theorem :: XREAL_1:121
for c, b, a being real number st c <= 0 & b < 0 & a <= b holds
c / a <= c / b
proof end;

theorem :: XREAL_1:122
for a being real number holds
( 0 < a iff 0 < a " ) ;

theorem :: XREAL_1:123
for a being real number holds
( a < 0 iff a " < 0 ) ;

theorem Th124: :: XREAL_1:124
for a, b being real number st a < 0 & 0 < b holds
a " < b "
proof end;

theorem :: XREAL_1:125
for a, b being real number st a " < 0 & 0 < b " holds
a < b
proof end;

begin

theorem :: XREAL_1:126
for a, b being real number st a <= 0 & 0 <= a holds
0 = a * b by Lm35;

theorem :: XREAL_1:127
for a, b being real number st 0 <= a & 0 <= b holds
0 <= a * b ;

theorem :: XREAL_1:128
for a, b being real number st a <= 0 & b <= 0 holds
0 <= a * b ;

theorem :: XREAL_1:129
for a, b being real number st 0 < a & 0 < b holds
0 < a * b ;

theorem :: XREAL_1:130
for a, b being real number st a < 0 & b < 0 holds
0 < a * b ;

theorem :: XREAL_1:131
for a, b being real number st 0 <= a & b <= 0 holds
a * b <= 0 ;

theorem :: XREAL_1:132
for a, b being real number st 0 < a & b < 0 holds
a * b < 0 ;

theorem :: XREAL_1:133
for a, b being real number holds
( not a * b < 0 or ( a > 0 & b < 0 ) or ( a < 0 & b > 0 ) )
proof end;

theorem :: XREAL_1:134
for a, b being real number holds
( not a * b > 0 or ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) )
proof end;

theorem :: XREAL_1:135
for a, b being real number st a <= 0 & b <= 0 holds
0 <= a / b ;

theorem :: XREAL_1:136
for a, b being real number st 0 <= a & 0 <= b holds
0 <= a / b ;

theorem :: XREAL_1:137
for a, b being real number st 0 <= a & b <= 0 holds
a / b <= 0 ;

theorem :: XREAL_1:138
for a, b being real number st a <= 0 & 0 <= b holds
a / b <= 0 ;

theorem :: XREAL_1:139
for a, b being real number st 0 < a & 0 < b holds
0 < a / b ;

theorem :: XREAL_1:140
for a, b being real number st a < 0 & b < 0 holds
0 < a / b ;

theorem :: XREAL_1:141
for a, b being real number st a < 0 & 0 < b holds
a / b < 0 ;

theorem :: XREAL_1:142
for a, b being real number st a < 0 & 0 < b holds
b / a < 0 ;

theorem :: XREAL_1:143
for a, b being real number holds
( not a / b < 0 or ( b < 0 & a > 0 ) or ( b > 0 & a < 0 ) )
proof end;

theorem :: XREAL_1:144
for a, b being real number holds
( not a / b > 0 or ( b > 0 & a > 0 ) or ( b < 0 & a < 0 ) )
proof end;

begin

theorem :: XREAL_1:145
for a, b being real number st a <= b holds
a < b + 1
proof end;

theorem :: XREAL_1:146
for a being real number holds a - 1 < a
proof end;

theorem :: XREAL_1:147
for a, b being real number st a <= b holds
a - 1 < b
proof end;

theorem :: XREAL_1:148
for a being real number st - 1 < a holds
0 < 1 + a
proof end;

theorem :: XREAL_1:149
for a being real number st a < 1 holds
1 - a > 0 by Lm21;

begin

theorem :: XREAL_1:150
for a, b being real number st a <= 1 & 0 <= b & b <= 1 & a * b = 1 holds
a = 1
proof end;

theorem :: XREAL_1:151
for a, b being real number st 0 <= a & 1 <= b holds
a <= a * b
proof end;

theorem :: XREAL_1:152
for a, b being real number st a <= 0 & b <= 1 holds
a <= a * b
proof end;

theorem :: XREAL_1:153
for a, b being real number st 0 <= a & b <= 1 holds
a * b <= a
proof end;

theorem :: XREAL_1:154
for a, b being real number st a <= 0 & 1 <= b holds
a * b <= a
proof end;

theorem Th155: :: XREAL_1:155
for a, b being real number st 0 < a & 1 < b holds
a < a * b
proof end;

theorem :: XREAL_1:156
for a, b being real number st a < 0 & b < 1 holds
a < a * b
proof end;

theorem :: XREAL_1:157
for a, b being real number st 0 < a & b < 1 holds
a * b < a
proof end;

theorem :: XREAL_1:158
for a, b being real number st a < 0 & 1 < b holds
a * b < a
proof end;

theorem :: XREAL_1:159
for a, b being real number st 1 <= a & 1 <= b holds
1 <= a * b
proof end;

theorem :: XREAL_1:160
for a, b being real number st 0 <= a & a <= 1 & b <= 1 holds
a * b <= 1
proof end;

theorem :: XREAL_1:161
for a, b being real number st 1 < a & 1 <= b holds
1 < a * b
proof end;

theorem :: XREAL_1:162
for a, b being real number st 0 <= a & a < 1 & b <= 1 holds
a * b < 1
proof end;

theorem :: XREAL_1:163
for a, b being real number st a <= - 1 & b <= - 1 holds
1 <= a * b
proof end;

theorem :: XREAL_1:164
for a, b being real number st a < - 1 & b <= - 1 holds
1 < a * b
proof end;

theorem :: XREAL_1:165
for a, b being real number st a <= 0 & - 1 <= a & - 1 <= b holds
a * b <= 1
proof end;

theorem :: XREAL_1:166
for a, b being real number st a <= 0 & - 1 < a & - 1 <= b holds
a * b < 1
proof end;

begin

theorem Th167: :: XREAL_1:167
for c, b being real number st ( for a being real number st 1 < a holds
c <= b * a ) holds
c <= b
proof end;

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
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
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 )
proof end;

theorem :: XREAL_1:171
for d, a, b being real number st 0 <= d & a <= b holds
a <= ((1 - d) * a) + (d * b)
proof end;

theorem :: XREAL_1:172
for d, a, b being real number st d <= 1 & a <= b holds
((1 - d) * a) + (d * b) <= b
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)
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
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)
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
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)
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
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
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
proof end;

begin

theorem :: XREAL_1:181
for a, b being real number st 0 < a & a <= b holds
1 <= b / a
proof end;

theorem :: XREAL_1:182
for a, b being real number st a < 0 & b <= a holds
1 <= b / a
proof end;

theorem :: XREAL_1:183
for a, b being real number st 0 <= a & a <= b holds
a / b <= 1 by Lm37;

theorem :: XREAL_1:184
for b, a being real number st b <= a & a <= 0 holds
a / b <= 1
proof end;

theorem :: XREAL_1:185
for a, b being real number st 0 <= a & b <= a holds
b / a <= 1 by Lm38;

theorem :: XREAL_1:186
for a, b being real number st a <= 0 & a <= b holds
b / a <= 1
proof end;

theorem :: XREAL_1:187
for a, b being real number st 0 < a & a < b holds
1 < b / a
proof end;

theorem :: XREAL_1:188
for a, b being real number st a < 0 & b < a holds
1 < b / a
proof end;

theorem :: XREAL_1:189
for a, b being real number st 0 <= a & a < b holds
a / b < 1
proof end;

theorem :: XREAL_1:190
for a, b being real number st a <= 0 & b < a holds
a / b < 1
proof end;

theorem :: XREAL_1:191
for a, b being real number st 0 < a & b < a holds
b / a < 1
proof end;

theorem :: XREAL_1:192
for a, b being real number st a < 0 & a < b holds
b / a < 1
proof end;

begin

theorem :: XREAL_1:193
for b, a being real number st 0 <= b & - b <= a holds
- 1 <= a / b
proof end;

theorem :: XREAL_1:194
for b, a being real number st 0 <= b & - a <= b holds
- 1 <= a / b
proof end;

theorem :: XREAL_1:195
for b, a being real number st b <= 0 & a <= - b holds
- 1 <= a / b
proof end;

theorem :: XREAL_1:196
for b, a being real number st b <= 0 & b <= - a holds
- 1 <= a / b
proof end;

theorem :: XREAL_1:197
for b, a being real number st 0 < b & - b < a holds
- 1 < a / b
proof end;

theorem :: XREAL_1:198
for b, a being real number st 0 < b & - a < b holds
- 1 < a / b
proof end;

theorem :: XREAL_1:199
for b, a being real number st b < 0 & a < - b holds
- 1 < a / b
proof end;

theorem :: XREAL_1:200
for b, a being real number st b < 0 & b < - a holds
- 1 < a / b
proof end;

theorem :: XREAL_1:201
for b, a being real number st 0 < b & a <= - b holds
a / b <= - 1
proof end;

theorem :: XREAL_1:202
for b, a being real number st 0 < b & b <= - a holds
a / b <= - 1
proof end;

theorem :: XREAL_1:203
for b, a being real number st b < 0 & - b <= a holds
a / b <= - 1
proof end;

theorem :: XREAL_1:204
for b, a being real number st b < 0 & - a <= b holds
a / b <= - 1
proof end;

theorem :: XREAL_1:205
for b, a being real number st 0 < b & a < - b holds
a / b < - 1
proof end;

theorem :: XREAL_1:206
for b, a being real number st 0 < b & b < - a holds
a / b < - 1
proof end;

theorem :: XREAL_1:207
for b, a being real number st b < 0 & - b < a holds
a / b < - 1
proof end;

theorem :: XREAL_1:208
for b, a being real number st b < 0 & - a < b holds
a / b < - 1
proof end;

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
proof end;

theorem :: XREAL_1:210
for b, c being real number st ( for a being real number st 1 < a holds
b / a <= c ) holds
b <= c
proof end;

theorem :: XREAL_1:211
for a being real number st 1 <= a holds
a " <= 1
proof end;

theorem :: XREAL_1:212
for a being real number st 1 < a holds
a " < 1 by Lm36;

theorem :: XREAL_1:213
for a being real number st a <= - 1 holds
- 1 <= a "
proof end;

theorem :: XREAL_1:214
for a being real number st a < - 1 holds
- 1 < a "
proof end;

begin

theorem :: XREAL_1:215
for a being real number st 0 < a holds
0 < a / 2 ;

theorem :: XREAL_1:216
for a being real number st 0 < a holds
a / 2 < a by Lm27;

theorem :: XREAL_1:217
for a being real number st a <= 1 / 2 holds
(2 * a) - 1 <= 0
proof end;

theorem :: XREAL_1:218
for a being real number st a <= 1 / 2 holds
0 <= 1 - (2 * a)
proof end;

theorem :: XREAL_1:219
for a being real number st a >= 1 / 2 holds
(2 * a) - 1 >= 0
proof end;

theorem :: XREAL_1:220
for a being real number st a >= 1 / 2 holds
0 >= 1 - (2 * a)
proof end;

begin

theorem :: XREAL_1:221
for a being real number st 0 < a holds
a / 3 < a
proof end;

theorem :: XREAL_1:222
for a being real number st 0 < a holds
0 < a / 3 ;

begin

theorem :: XREAL_1:223
for a being real number st 0 < a holds
a / 4 < a
proof end;

theorem :: XREAL_1:224
for a being real number st 0 < a holds
0 < a / 4 ;

theorem :: XREAL_1:225
for a, b being real number st b <> 0 holds
ex c being real number st a = b / c
proof end;

begin

:: from TOPREAL3, 2006.07.15, A.T.
theorem :: XREAL_1:226
for r, s being real number st r < s holds
( r < (r + s) / 2 & (r + s) / 2 < s )
proof end;

:: missing, 2007.01.16, A.T.
registration
cluster -> ext-real for Element of REAL ;
coherence
for b1 being Element of REAL holds b1 is ext-real ;
end;

theorem Th227: :: XREAL_1:227
for r, t being ext-real number st r < t holds
ex s being ext-real number st
( r < s & s < t )
proof end;

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
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
proof end;

:: missing, 2008.08.13, A.T.
theorem :: XREAL_1:230
for a, b, c being real number st 0 <= a & b <= c holds
b - a <= c
proof end;

theorem :: XREAL_1:231
for a, b, c being real number st 0 < a & b <= c holds
b - a < c
proof end;

begin

theorem :: XREAL_1:232
for a being real number holds a -' a = 0
proof end;

theorem Th233: :: XREAL_1:233
for b, a being real number st b <= a holds
a -' b = a - b
proof end;

theorem :: XREAL_1:234
for c, a, b being real number st c <= a & c <= b & a -' c = b -' c holds
a = b
proof end;

theorem :: XREAL_1:235
for a, b being real number st a >= b holds
(a -' b) + b = a
proof end;

:: from LEXBFS, 2008.08.23, A.T.
theorem :: XREAL_1:236
for a, b, c being real number st a <= b & c < a holds
b -' a < b -' c
proof end;

:: missing, 2010.05.18, A.T.
theorem :: XREAL_1:237
for a being real number st 1 <= a holds
a -' 1 < a
proof end;