:: Real Numbers - Basic Theorems
:: by Library Committee
::
:: Received February 9, 2005
:: Copyright (c) 2005-2021 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;

theorem Th1: :: XREAL_1:1

for a being Real ex b being Real st a < b

proof end;

theorem Th2: :: XREAL_1:2

for a being Real ex b being Real st b < a

proof end;

theorem :: XREAL_1:3

for a, b being Real ex c being Real st
( a < c & b < c )

proof end;

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

proof end;

theorem :: XREAL_1:4

for a, b being Real ex c being Real st
( c < a & c < 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;

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;

theorem Th5: :: XREAL_1:5

for a, b being Real st a < b holds
ex c being Real st
( a < c & c < b )

proof end;

theorem :: XREAL_1:6

for a, b, c being Real holds
( a <= b iff a + c <= b + c ) by Lm5, Lm10;

theorem :: XREAL_1:7

for a, b, c, d being Real st a <= b & c <= d holds
a + c <= b + d by Lm6;

theorem :: XREAL_1:8

for a, b, c, d being Real st a < b & c <= d holds
a + c < b + d by Lm8;

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;

theorem Th9: :: XREAL_1:9

for a, b, c being Real holds
( a <= b iff a - c <= b - c )

proof end;

theorem :: XREAL_1:10

for a, b, c being Real holds
( a <= b iff c - b <= c - a )

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;

theorem :: XREAL_1:11

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

proof end;

theorem :: XREAL_1:12

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

proof end;

theorem Th13: :: XREAL_1:13

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

proof end;

theorem Th14: :: XREAL_1:14

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

proof end;

theorem Th15: :: XREAL_1:15

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

proof end;

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

proof end;

theorem :: XREAL_1:16

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

proof end;

theorem :: XREAL_1:17

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

proof end;

theorem :: XREAL_1:18

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

proof end;

theorem :: XREAL_1:19

for a, b, c being Real holds
( a + b <= c iff a <= c - b ) by Lm16, Lm17;

theorem :: XREAL_1:20

for a, b, c being Real holds
( a <= b + c iff a - b <= c ) by Lm18, Lm19;

theorem :: XREAL_1:21

for a, b, c, d being Real holds
( a + b <= c + d iff a - c <= d - b )

proof end;

theorem :: XREAL_1:22

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

proof end;

theorem :: XREAL_1:23

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

proof end;

theorem :: XREAL_1:24

for a, b being Real holds
( a <= b iff - b <= - a ) by Lm14, Lm15;

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

proof end;

theorem Th25: :: XREAL_1:25

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

proof end;

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

proof end;

theorem Th26: :: XREAL_1:26

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

proof end;

theorem :: XREAL_1:27

for a, b being Real st 0 <= a & 0 <= b & a + b = 0 holds
a = 0 ;

theorem :: XREAL_1:28

for a, b being Real st a <= 0 & b <= 0 & a + b = 0 holds
a = 0 ;

theorem :: XREAL_1:29

for a, b being Real st 0 < a holds
b < b + a by Lm9;

theorem :: XREAL_1:30

for a, b being Real st a < 0 holds
a + b < b

proof end;

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

proof end;

theorem :: XREAL_1:31

for a, b being Real st 0 <= a holds
b <= a + b

proof end;

theorem :: XREAL_1:32

for a, b being Real st a <= 0 holds
a + b <= b

proof end;

theorem :: XREAL_1:33

for a, b being Real st 0 <= a & 0 <= b holds
0 <= a + b ;

theorem :: XREAL_1:34

for a, b being Real st 0 <= a & 0 < b holds
0 < a + b ;

theorem Th35: :: XREAL_1:35

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

proof end;

theorem Th36: :: XREAL_1:36

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

proof end;

theorem Th37: :: XREAL_1:37

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

proof end;

theorem Th38: :: XREAL_1:38

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

proof end;

theorem Th39: :: XREAL_1:39

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

proof end;

theorem Th40: :: XREAL_1:40

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

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;

theorem :: XREAL_1:41

for b, c being Real st ( for a being Real st a > 0 holds
c <= b + a ) holds
c <= b

proof end;

theorem :: XREAL_1:42

for b, c being Real st ( for a being Real st a < 0 holds
b + a <= c ) holds
b <= c

proof end;

theorem :: XREAL_1:43

for a, b being Real st 0 <= a holds
b - a <= b

proof end;

theorem Th44: :: XREAL_1:44

for a, b being Real st 0 < a holds
b - a < b

proof end;

theorem :: XREAL_1:45

for a, b being Real st a <= 0 holds
b <= b - a

proof end;

theorem :: XREAL_1:46

for a, b being Real st a < 0 holds
b < b - a

proof end;

theorem :: XREAL_1:47

for a, b being Real st a <= b holds
a - b <= 0

proof end;

theorem Th48: :: XREAL_1:48

for a, b being Real st a <= b holds
0 <= b - a

proof end;

theorem :: XREAL_1:49

for a, b being Real st a < b holds
a - b < 0 by Lm23;

theorem :: XREAL_1:50

for a, b being Real st a < b holds
0 < b - a by Lm21;

theorem :: XREAL_1:51

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

proof end;

theorem :: XREAL_1:52

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

proof end;

theorem :: XREAL_1:53

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

proof end;

theorem :: XREAL_1:54

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

proof end;

theorem :: XREAL_1:55

for a, b being Real holds
( not a <> b or 0 < a - b or 0 < b - a )

proof end;

theorem :: XREAL_1:56

for b, c being Real st ( for a being Real st a < 0 holds
c <= b - a ) holds
b >= c

proof end;

theorem :: XREAL_1:57

for b, c being Real st ( for a being Real st a > 0 holds
b - a <= c ) holds
b <= c

proof end;

theorem :: XREAL_1:58

for a being Real holds
( a < 0 iff 0 < - a ) ;

theorem :: XREAL_1:59

for a, b being Real st a <= - b holds
a + b <= 0

proof end;

theorem :: XREAL_1:60

for a, b being Real st - a <= b holds
0 <= a + b

proof end;

theorem :: XREAL_1:61

for a, b being Real st a < - b holds
a + b < 0

proof end;

theorem :: XREAL_1:62

for a, b being Real st - b < a holds
0 < a + b

proof end;

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

proof end;

theorem :: XREAL_1:63

for a being Real holds 0 <= a * a

proof end;

theorem :: XREAL_1:64

for a, b, c being Real st a <= b & 0 <= c holds
a * c <= b * c by Lm12;

theorem :: XREAL_1:65

for a, b, c being Real st a <= b & c <= 0 holds
b * c <= a * c by Lm28;

theorem Th66: :: XREAL_1:66

for a, b, c, d being Real 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 st a <= 0 & b <= a & c <= 0 & d <= c holds
a * c <= b * d

proof end;

theorem :: XREAL_1:68

for a, b, c being Real st 0 < c & a < b holds
a * c < b * c by Lm13;

theorem :: XREAL_1:69

for a, b, c being Real st c < 0 & a < b holds
b * c < a * c by Lm24;

theorem :: XREAL_1:70

for a, b, c, d being Real st a < 0 & b <= a & c < 0 & d < c holds
a * c < b * d

proof end;

theorem :: XREAL_1:71

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

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;

theorem :: XREAL_1:72

for a, b, c being Real st 0 <= c & b <= a holds
b / c <= a / c by Lm25;

theorem :: XREAL_1:73

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

theorem :: XREAL_1:74

for a, b, c being Real st 0 < c & a < b holds
a / c < b / c by Lm26;

theorem :: XREAL_1:75

for a, b, c being Real st c < 0 & a < b holds
b / c < a / c by Lm29;

theorem :: XREAL_1:76

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

proof end;

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

proof end;

theorem Th77: :: XREAL_1:77

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

proof end;

theorem Th78: :: XREAL_1:78

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

proof end;

theorem Th79: :: XREAL_1:79

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

proof end;

theorem Th80: :: XREAL_1:80

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

proof end;

theorem Th81: :: XREAL_1:81

for a, b, c being Real st 0 < b & a * b < c holds
a < c / b

proof end;

theorem Th82: :: XREAL_1:82

for a, b, c being Real st b < 0 & a * b < c holds
c / b < a

proof end;

theorem Th83: :: XREAL_1:83

for a, b, c being Real st 0 < b & c < a * b holds
c / b < a

proof end;

theorem Th84: :: XREAL_1:84

for a, b, c being Real st b < 0 & c < a * b holds
a < c / b

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;

theorem :: XREAL_1:85

for a, b being Real st 0 < a & a <= b holds
b " <= a " by Lm32;

theorem :: XREAL_1:86

for a, b being Real st b < 0 & a <= b holds
b " <= a " by Lm33;

theorem :: XREAL_1:87

for a, b being Real st b < 0 & a < b holds
b " < a " by Lm31;

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

proof end;

theorem :: XREAL_1:88

for a, b being Real st 0 < a & a < b holds
b " < a " by Lm34;

theorem :: XREAL_1:89

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

proof end;

theorem :: XREAL_1:90

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

proof end;

theorem :: XREAL_1:91

for a, b being Real st 0 < b " & b " < a " holds
a < b

proof end;

theorem :: XREAL_1:92

for a, b being Real st a " < 0 & b " < a " holds
a < b

proof end;

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

theorem :: XREAL_1:93

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

proof end;

theorem :: XREAL_1:94

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

proof end;

theorem :: XREAL_1:95

for a, b being Real holds
( not 0 <= (b - a) * (b + a) or b <= - a or a <= b )

proof end;

theorem :: XREAL_1:96

for a, b, c, d being Real st 0 <= a & 0 <= c & a < b & c < d holds
a * c < b * d

proof end;

theorem :: XREAL_1:97

for a, b, c, d being Real st 0 <= a & 0 < c & a < b & c <= d holds
a * c < b * d

proof end;

theorem Th98: :: XREAL_1:98

for a, b, c, d being Real st 0 < a & 0 < c & a <= b & c < d holds
a * c < b * d

proof end;

theorem :: XREAL_1:99

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

proof end;

theorem :: XREAL_1:100

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

proof end;

theorem :: XREAL_1:101

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

proof end;

theorem :: XREAL_1:102

for a, b, c, d being Real st 0 < b & 0 < d & a * d <= c * b holds
a / b <= c / d

proof end;

theorem :: XREAL_1:103

for a, b, c, d being Real st b < 0 & d < 0 & a * d <= c * b holds
a / b <= c / d

proof end;

theorem :: XREAL_1:104

for a, b, c, d being Real st 0 < b & d < 0 & a * d <= c * b holds
c / d <= a / b

proof end;

theorem :: XREAL_1:105

for a, b, c, d being Real st b < 0 & 0 < d & a * d <= c * b holds
c / d <= a / b

proof end;

theorem :: XREAL_1:106

for a, b, c, d being Real st 0 < b & 0 < d & a * d < c * b holds
a / b < c / d

proof end;

theorem :: XREAL_1:107

for a, b, c, d being Real st b < 0 & d < 0 & a * d < c * b holds
a / b < c / d

proof end;

theorem :: XREAL_1:108

for a, b, c, d being Real st 0 < b & d < 0 & a * d < c * b holds
c / d < a / b

proof end;

theorem :: XREAL_1:109

for a, b, c, d being Real st b < 0 & 0 < d & a * d < c * b holds
c / d < a / b

proof end;

theorem :: XREAL_1:110

for a, b, c, d being Real st b < 0 & d < 0 & a * b < c / d holds
a * d < c / b

proof end;

theorem :: XREAL_1:111

for a, b, c, d being Real st 0 < b & 0 < d & a * b < c / d holds
a * d < c / b

proof end;

theorem :: XREAL_1:112

for a, b, c, d being Real st b < 0 & d < 0 & c / d < a * b holds
c / b < a * d

proof end;

theorem :: XREAL_1:113

for a, b, c, d being Real st 0 < b & 0 < d & c / d < a * b holds
c / b < a * d

proof end;

theorem :: XREAL_1:114

for a, b, c, d being Real st b < 0 & 0 < d & a * b < c / d holds
c / b < a * d

proof end;

theorem :: XREAL_1:115

for a, b, c, d being Real st 0 < b & d < 0 & a * b < c / d holds
c / b < a * d

proof end;

theorem :: XREAL_1:116

for a, b, c, d being Real st b < 0 & 0 < d & c / d < a * b holds
a * d < c / b

proof end;

theorem :: XREAL_1:117

for a, b, c, d being Real st 0 < b & d < 0 & c / d < a * b holds
a * d < c / b

proof end;

theorem :: XREAL_1:118

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

proof end;

theorem :: XREAL_1:119

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

proof end;

theorem :: XREAL_1:120

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

proof end;

theorem :: XREAL_1:121

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

proof end;

theorem :: XREAL_1:122

for a being Real holds
( 0 < a iff 0 < a " ) ;

theorem :: XREAL_1:123

for a being Real holds
( a < 0 iff a " < 0 ) ;

theorem Th124: :: XREAL_1:124

for a, b being Real st a < 0 & 0 < b holds
a " < b "

proof end;

theorem :: XREAL_1:125

for a, b being Real st a " < 0 & 0 < b " holds
a < b

proof end;

theorem :: XREAL_1:126

for a, b being Real st a <= 0 & 0 <= a holds
0 = a * b by Lm35;

theorem :: XREAL_1:127

for a, b being Real st 0 <= a & 0 <= b holds
0 <= a * b ;

theorem :: XREAL_1:128

for a, b being Real st a <= 0 & b <= 0 holds
0 <= a * b ;

theorem :: XREAL_1:129

for a, b being Real st 0 < a & 0 < b holds
0 < a * b ;

theorem :: XREAL_1:130

for a, b being Real st a < 0 & b < 0 holds
0 < a * b ;

theorem :: XREAL_1:131

for a, b being Real st 0 <= a & b <= 0 holds
a * b <= 0 ;

theorem :: XREAL_1:132

for a, b being Real st 0 < a & b < 0 holds
a * b < 0 ;

theorem :: XREAL_1:133

for a, b being Real 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 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 st a <= 0 & b <= 0 holds
0 <= a / b ;

theorem :: XREAL_1:136

for a, b being Real st 0 <= a & 0 <= b holds
0 <= a / b ;

theorem :: XREAL_1:137

for a, b being Real st 0 <= a & b <= 0 holds
a / b <= 0 ;

theorem :: XREAL_1:138

for a, b being Real st a <= 0 & 0 <= b holds
a / b <= 0 ;

theorem :: XREAL_1:139

for a, b being Real st 0 < a & 0 < b holds
0 < a / b ;

theorem :: XREAL_1:140

for a, b being Real st a < 0 & b < 0 holds
0 < a / b ;

theorem :: XREAL_1:141

for a, b being Real st a < 0 & 0 < b holds
a / b < 0 ;

theorem :: XREAL_1:142

for a, b being Real st a < 0 & 0 < b holds
b / a < 0 ;

theorem :: XREAL_1:143

for a, b being Real 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 holds
( not a / b > 0 or ( b > 0 & a > 0 ) or ( b < 0 & a < 0 ) )

proof end;

theorem :: XREAL_1:145

for a, b being Real st a <= b holds
a < b + 1

proof end;

theorem :: XREAL_1:146

for a being Real holds a - 1 < a

proof end;

theorem :: XREAL_1:147

for a, b being Real st a <= b holds
a - 1 < b

proof end;

theorem :: XREAL_1:148

for a being Real st - 1 < a holds
0 < 1 + a

proof end;

theorem :: XREAL_1:149

for a being Real st a < 1 holds
1 - a > 0 by Lm21;

theorem :: XREAL_1:150

for a, b being Real st a <= 1 & 0 <= b & b <= 1 & a * b = 1 holds
a = 1

proof end;

theorem :: XREAL_1:151

for a, b being Real st 0 <= a & 1 <= b holds
a <= a * b

proof end;

theorem :: XREAL_1:152

for a, b being Real st a <= 0 & b <= 1 holds
a <= a * b

proof end;

theorem :: XREAL_1:153

for a, b being Real st 0 <= a & b <= 1 holds
a * b <= a

proof end;

theorem :: XREAL_1:154

for a, b being Real st a <= 0 & 1 <= b holds
a * b <= a

proof end;

theorem Th155: :: XREAL_1:155

for a, b being Real st 0 < a & 1 < b holds
a < a * b

proof end;

theorem :: XREAL_1:156

for a, b being Real st a < 0 & b < 1 holds
a < a * b

proof end;

theorem :: XREAL_1:157

for a, b being Real st 0 < a & b < 1 holds
a * b < a

proof end;

theorem :: XREAL_1:158

for a, b being Real st a < 0 & 1 < b holds
a * b < a

proof end;

theorem :: XREAL_1:159

for a, b being Real st 1 <= a & 1 <= b holds
1 <= a * b

proof end;

theorem :: XREAL_1:160

for a, b being Real st 0 <= a & a <= 1 & b <= 1 holds
a * b <= 1

proof end;

theorem :: XREAL_1:161

for a, b being Real st 1 < a & 1 <= b holds
1 < a * b

proof end;

theorem :: XREAL_1:162

for a, b being Real st 0 <= a & a < 1 & b <= 1 holds
a * b < 1

proof end;

theorem :: XREAL_1:163

for a, b being Real st a <= - 1 & b <= - 1 holds
1 <= a * b

proof end;

theorem :: XREAL_1:164

for a, b being Real st a < - 1 & b <= - 1 holds
1 < a * b

proof end;

theorem :: XREAL_1:165

for a, b being Real st a <= 0 & - 1 <= a & - 1 <= b holds
a * b <= 1

proof end;

theorem :: XREAL_1:166

for a, b being Real st a <= 0 & - 1 < a & - 1 <= b holds
a * b < 1

proof end;

theorem Th167: :: XREAL_1:167

for b, c being Real st ( for a being Real st 1 < a holds
c <= b * a ) holds
c <= b

proof end;

Lm36: for a being Real st 1 < a holds
a " < 1

proof end;

theorem :: XREAL_1:168

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

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:169

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

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 )

proof end;

theorem :: XREAL_1:171

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

proof end;

theorem :: XREAL_1:172

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

proof end;

theorem :: XREAL_1:173

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

proof end;

theorem :: XREAL_1:174

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

proof end;

theorem :: XREAL_1:175

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

proof end;

theorem :: XREAL_1:176

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

proof end;

theorem :: XREAL_1:177

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

proof end;

theorem :: XREAL_1:178

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

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

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

proof end;

theorem :: XREAL_1:181

for a, b being Real st 0 < a & a <= b holds
1 <= b / a

proof end;

theorem :: XREAL_1:182

for a, b being Real st a < 0 & b <= a holds
1 <= b / a

proof end;

theorem :: XREAL_1:183

for a, b being Real st 0 <= a & a <= b holds
a / b <= 1 by Lm37;

theorem :: XREAL_1:184

for a, b being Real st b <= a & a <= 0 holds
a / b <= 1

proof end;

theorem :: XREAL_1:185

for a, b being Real st 0 <= a & b <= a holds
b / a <= 1 by Lm38;

theorem :: XREAL_1:186

for a, b being Real st a <= 0 & a <= b holds
b / a <= 1

proof end;

theorem :: XREAL_1:187

for a, b being Real st 0 < a & a < b holds
1 < b / a

proof end;

theorem :: XREAL_1:188

for a, b being Real st a < 0 & b < a holds
1 < b / a

proof end;

theorem :: XREAL_1:189

for a, b being Real st 0 <= a & a < b holds
a / b < 1

proof end;

theorem :: XREAL_1:190

for a, b being Real st a <= 0 & b < a holds
a / b < 1

proof end;

theorem :: XREAL_1:191

for a, b being Real st 0 < a & b < a holds
b / a < 1

proof end;

theorem :: XREAL_1:192

for a, b being Real st a < 0 & a < b holds
b / a < 1

proof end;

theorem :: XREAL_1:193

for a, b being Real st 0 <= b & - b <= a holds
- 1 <= a / b

proof end;

theorem :: XREAL_1:194

for a, b being Real st 0 <= b & - a <= b holds
- 1 <= a / b

proof end;

theorem :: XREAL_1:195

for a, b being Real st b <= 0 & a <= - b holds
- 1 <= a / b

proof end;

theorem :: XREAL_1:196

for a, b being Real st b <= 0 & b <= - a holds
- 1 <= a / b

proof end;

theorem :: XREAL_1:197

for a, b being Real st 0 < b & - b < a holds
- 1 < a / b

proof end;

theorem :: XREAL_1:198

for a, b being Real st 0 < b & - a < b holds
- 1 < a / b

proof end;

theorem :: XREAL_1:199

for a, b being Real st b < 0 & a < - b holds
- 1 < a / b

proof end;

theorem :: XREAL_1:200

for a, b being Real st b < 0 & b < - a holds
- 1 < a / b

proof end;

theorem :: XREAL_1:201

for a, b being Real st 0 < b & a <= - b holds
a / b <= - 1

proof end;

theorem :: XREAL_1:202

for a, b being Real st 0 < b & b <= - a holds
a / b <= - 1

proof end;

theorem :: XREAL_1:203

for a, b being Real st b < 0 & - b <= a holds
a / b <= - 1

proof end;

theorem :: XREAL_1:204

for a, b being Real st b < 0 & - a <= b holds
a / b <= - 1

proof end;

theorem :: XREAL_1:205

for a, b being Real st 0 < b & a < - b holds
a / b < - 1

proof end;

theorem :: XREAL_1:206

for a, b being Real st 0 < b & b < - a holds
a / b < - 1

proof end;

theorem :: XREAL_1:207

for a, b being Real st b < 0 & - b < a holds
a / b < - 1

proof end;

theorem :: XREAL_1:208

for a, b being Real st b < 0 & - a < b holds
a / b < - 1

proof end;

theorem Th209: :: XREAL_1:209

for b, c being Real st ( for a being Real st 0 < a & a < 1 holds
c <= b / a ) holds
c <= b

proof end;

theorem :: XREAL_1:210

for b, c being Real st ( for a being Real st 1 < a holds
b / a <= c ) holds
b <= c

proof end;

theorem :: XREAL_1:211

for a being Real st 1 <= a holds
a " <= 1

proof end;

theorem :: XREAL_1:212

for a being Real st 1 < a holds
a " < 1 by Lm36;

theorem :: XREAL_1:213

for a being Real st a <= - 1 holds
- 1 <= a "

proof end;

theorem :: XREAL_1:214

for a being Real st a < - 1 holds
- 1 < a "

proof end;

theorem :: XREAL_1:215

for a being Real st 0 < a holds
0 < a / 2 ;

theorem :: XREAL_1:216

for a being Real st 0 < a holds
a / 2 < a by Lm27;

theorem :: XREAL_1:217

for a being Real st a <= 1 / 2 holds
(2 * a) - 1 <= 0

proof end;

theorem :: XREAL_1:218

for a being Real st a <= 1 / 2 holds
0 <= 1 - (2 * a)

proof end;

theorem :: XREAL_1:219

for a being Real st a >= 1 / 2 holds
(2 * a) - 1 >= 0

proof end;

theorem :: XREAL_1:220

for a being Real st a >= 1 / 2 holds
0 >= 1 - (2 * a)

proof end;

theorem :: XREAL_1:221

for a being Real st 0 < a holds
a / 3 < a

proof end;

theorem :: XREAL_1:222

for a being Real st 0 < a holds
0 < a / 3 ;

theorem :: XREAL_1:223

for a being Real st 0 < a holds
a / 4 < a

proof end;

theorem :: XREAL_1:224

for a being Real st 0 < a holds
0 < a / 4 ;

theorem :: XREAL_1:225

for a, b being Real st b <> 0 holds
ex c being Real st a = b / c

proof end;

:: from TOPREAL3, 2006.07.15, A.T.

theorem :: XREAL_1:226

for r, s being Real 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 b₁ being Element of REAL holds b₁ is ext-real ;

end;

theorem Th227: :: XREAL_1:227

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

proof end;

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

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

proof end;

:: missing, 2008.08.13, A.T.

theorem :: XREAL_1:230

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

proof end;

theorem :: XREAL_1:231

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

proof end;

theorem :: XREAL_1:232

for a being Real holds a -' a = 0

proof end;

theorem Th233: :: XREAL_1:233

for a, b being Real st b <= a holds
a -' b = a - b by Th48, XREAL_0:def 2;

theorem :: XREAL_1:234

for a, b, c being Real st c <= a & c <= b & a -' c = b -' c holds
a = b

proof end;

theorem :: XREAL_1:235

for a, b being Real 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 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 st 1 <= a holds
a -' 1 < a

proof end;