Lm39: for a, b being real positive number holds 0 < a * b
;

Lm40: for a, b being real negative number holds 0 < a * b
;

Lm41: for a, b being real non negative number holds 0 <= a * b
;

Lm42: for a, b being real non positive number holds 0 <= a * b
;

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

Lm44: for a being real positive number
for b being real negative number holds a * b < 0
;

theorem :: XREAL_1:95

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

proof end;

theorem :: XREAL_1:96

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

proof end;

theorem :: XREAL_1:97

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

proof end;

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

proof end;

theorem Th100: :: XREAL_1:100

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

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

proof end;

theorem :: XREAL_1:102

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

proof end;

theorem :: XREAL_1:103

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

proof end;

theorem :: XREAL_1:104

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

proof end;

theorem :: XREAL_1:121

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

proof end;

theorem :: XREAL_1:122

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

proof end;

theorem :: XREAL_1:123

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

proof end;

theorem :: XREAL_1:124

for a being real number holds
( 0 < a iff 0 < a " )

proof end;

theorem :: XREAL_1:125

for a being real number holds
( a < 0 iff a " < 0 )

proof end;

theorem Th126: :: XREAL_1:126

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

proof end;

theorem :: XREAL_1:127

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

proof end;

theorem :: XREAL_1:128

for a, b being real number st a <= 0 & 0 <= a holds
0 = a * b by Lm43;

theorem :: XREAL_1:129

for a, b being real number st 0 <= a & 0 <= b holds
0 <= a * b by Lm41;

theorem :: XREAL_1:130

for a, b being real number st a <= 0 & b <= 0 holds
0 <= a * b by Lm42;

theorem :: XREAL_1:131

for a, b being real number st 0 < a & 0 < b holds
0 < a * b by Lm39;

theorem :: XREAL_1:132

for a, b being real number st a < 0 & b < 0 holds
0 < a * b by Lm40;

theorem Th133: :: XREAL_1:133

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

proof end;

theorem :: XREAL_1:134

for a, b being real number st 0 < a & b < 0 holds
a * b < 0 by Lm44;

theorem :: XREAL_1:135

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

for a, b being real number holds
( not a * b > 0 or ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) )

proof end;

theorem Th137: :: XREAL_1:137

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

proof end;

theorem Th138: :: XREAL_1:138

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

proof end;

theorem Th139: :: XREAL_1:139

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

proof end;

theorem Th140: :: XREAL_1:140

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

proof end;

theorem :: XREAL_1:141

for a, b being real number st 0 < a & 0 < b holds
0 < a / b by Lm37;

theorem :: XREAL_1:142

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

proof end;

theorem :: XREAL_1:143

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

proof end;

theorem :: XREAL_1:144

for a, b being real number st a < 0 & 0 < b holds
b / a < 0 by Lm33;

theorem :: XREAL_1:145

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

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

for a, b being real number st a <= b holds
a < b + 1

proof end;

theorem :: XREAL_1:148

for a being real number holds a - 1 < a

proof end;

theorem :: XREAL_1:149

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

proof end;

theorem :: XREAL_1:150

for a being real number st - 1 < a holds
0 < 1 + a

proof end;

theorem :: XREAL_1:151

for a being real number st a < 1 holds
1 - a > 0 by Lm20;

theorem :: XREAL_1:152

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

proof end;

theorem :: XREAL_1:153

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

proof end;

theorem :: XREAL_1:154

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

proof end;

theorem :: XREAL_1:155

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

proof end;

theorem :: XREAL_1:156

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

proof end;

theorem Th157: :: XREAL_1:157

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

proof end;

theorem :: XREAL_1:158

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

proof end;

theorem :: XREAL_1:159

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

proof end;

theorem :: XREAL_1:160

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

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 & 0 <= b & b <= 1 holds
a * b <= 1

proof end;

theorem :: XREAL_1:163

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

proof end;

theorem :: XREAL_1:164

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

proof end;

theorem :: XREAL_1:165

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

proof end;

theorem :: XREAL_1:166

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

proof end;

theorem :: XREAL_1:167

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

proof end;

theorem :: XREAL_1:168

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

proof end;

theorem Th169: :: XREAL_1:169

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

proof end;

Lm45: for a being real number st 1 < a holds
a " < 1

proof end;

theorem :: XREAL_1:170

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;

Lm46: for a, b being real number st a <= b & 0 <= a holds
a / b <= 1

proof end;

Lm47: for b, a being real number st b <= a & 0 <= a holds
b / a <= 1

proof end;

theorem :: XREAL_1:171

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

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