:: by Library Committee

::

:: Received February 9, 2005

:: Copyright (c) 2005-2011 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 :: XREAL_1:1

canceled;

theorem :: XREAL_1:2

canceled;

theorem Th3: :: XREAL_1:3

proof end;

theorem Th4: :: XREAL_1:4

proof end;

theorem :: XREAL_1:5

proof end;

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

a <= b

proof end;

theorem :: XREAL_1:6

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:21;

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 Th7: :: XREAL_1:7

proof end;

begin

theorem :: XREAL_1:8

theorem :: XREAL_1:9

theorem :: XREAL_1:10

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 Th11: :: XREAL_1:11

proof end;

theorem :: XREAL_1:12

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

proof end;

theorem :: XREAL_1:14

proof end;

theorem Th15: :: XREAL_1:15

proof end;

theorem Th16: :: XREAL_1:16

proof end;

theorem Th17: :: XREAL_1:17

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

proof end;

theorem :: XREAL_1:19

proof end;

theorem :: XREAL_1:20

proof end;

begin

theorem :: XREAL_1:21

theorem :: XREAL_1:22

theorem :: XREAL_1:23

proof end;

theorem :: XREAL_1:24

proof end;

theorem :: XREAL_1:25

proof end;

begin

theorem :: XREAL_1:26

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

0 < b - a

proof end;

theorem Th27: :: XREAL_1:27

proof end;

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

0 <= b - a

proof end;

theorem Th28: :: XREAL_1:28

proof end;

begin

theorem :: XREAL_1:29

theorem :: XREAL_1:30

begin

theorem :: XREAL_1:31

theorem :: XREAL_1:32

proof end;

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

a - b < 0

proof end;

theorem :: XREAL_1:33

proof end;

theorem :: XREAL_1:34

proof end;

begin

theorem :: XREAL_1:35

theorem :: XREAL_1:36

theorem Th37: :: XREAL_1:37

proof end;

theorem Th38: :: XREAL_1:38

proof end;

theorem Th39: :: XREAL_1:39

proof end;

theorem Th40: :: XREAL_1:40

proof end;

theorem Th41: :: XREAL_1:41

proof end;

theorem Th42: :: XREAL_1:42

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

proof end;

theorem :: XREAL_1:44

proof end;

begin

theorem :: XREAL_1:45

proof end;

theorem Th46: :: XREAL_1:46

proof end;

theorem :: XREAL_1:47

proof end;

theorem :: XREAL_1:48

proof end;

theorem :: XREAL_1:49

proof end;

theorem Th50: :: XREAL_1:50

proof end;

theorem :: XREAL_1:51

theorem :: XREAL_1:52

theorem :: XREAL_1:53

proof end;

theorem :: XREAL_1:54

proof end;

theorem :: XREAL_1:55

proof end;

theorem :: XREAL_1:56

proof end;

theorem :: XREAL_1:57

proof end;

begin

theorem :: XREAL_1:58

proof end;

theorem :: XREAL_1:59

proof end;

begin

theorem :: XREAL_1:60

theorem :: XREAL_1:61

proof end;

theorem :: XREAL_1:62

proof end;

theorem :: XREAL_1:63

proof end;

theorem :: XREAL_1:64

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

proof end;

theorem :: XREAL_1:66

theorem :: XREAL_1:67

theorem Th68: :: XREAL_1:68

proof end;

theorem :: XREAL_1:69

proof end;

theorem :: XREAL_1:70

theorem :: XREAL_1:71

theorem :: XREAL_1:72

proof end;

begin

theorem :: XREAL_1:73

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 ;

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

theorem :: XREAL_1:75

theorem :: XREAL_1:76

theorem :: XREAL_1:77

theorem :: XREAL_1:78

proof end;

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

b " < a "

proof end;

begin

theorem Th79: :: XREAL_1:79

proof end;

theorem Th80: :: XREAL_1:80

proof end;

theorem Th81: :: XREAL_1:81

proof end;

theorem Th82: :: XREAL_1:82

proof end;

theorem Th83: :: XREAL_1:83

proof end;

theorem Th84: :: XREAL_1:84

proof end;

theorem Th85: :: XREAL_1:85

proof end;

theorem Th86: :: XREAL_1:86

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

theorem :: XREAL_1:88

theorem :: XREAL_1:89

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

b " < a "

proof end;

theorem :: XREAL_1:90

theorem :: XREAL_1:91

proof end;

theorem :: XREAL_1:92

proof end;

theorem :: XREAL_1:93

proof end;

theorem :: XREAL_1:94

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

proof end;

theorem :: XREAL_1:96

proof end;

theorem :: XREAL_1:97

proof end;

theorem :: XREAL_1:98

proof end;

theorem :: XREAL_1:99

proof end;

theorem Th100: :: XREAL_1:100

proof end;

theorem :: XREAL_1:101

proof end;

theorem :: XREAL_1:102

proof end;

theorem :: XREAL_1:103

proof end;

theorem :: XREAL_1:104

proof end;

theorem :: XREAL_1:105

proof end;

theorem :: XREAL_1:106

proof end;

theorem :: XREAL_1:107

proof end;

theorem :: XREAL_1:108

proof end;

theorem :: XREAL_1:109

proof end;

theorem :: XREAL_1:110

proof end;

theorem :: XREAL_1:111

proof end;

theorem :: XREAL_1:112

proof end;

theorem :: XREAL_1:113

proof end;

theorem :: XREAL_1:114

proof end;

theorem :: XREAL_1:115

proof end;

theorem :: XREAL_1:116

proof end;

theorem :: XREAL_1:117

proof end;

theorem :: XREAL_1:118

proof end;

theorem :: XREAL_1:119

proof end;

theorem :: XREAL_1:120

proof end;

theorem :: XREAL_1:121

proof end;

theorem :: XREAL_1:122

proof end;

theorem :: XREAL_1:123

proof end;

theorem :: XREAL_1:124

theorem :: XREAL_1:125

theorem Th126: :: XREAL_1:126

proof end;

theorem :: XREAL_1:127

proof end;

begin

theorem :: XREAL_1:128

theorem :: XREAL_1:129

theorem :: XREAL_1:130

theorem :: XREAL_1:131

theorem :: XREAL_1:132

theorem :: XREAL_1:133

theorem :: XREAL_1:134

theorem :: XREAL_1:135

proof end;

theorem :: XREAL_1:136

proof end;

theorem :: XREAL_1:137

theorem :: XREAL_1:138

theorem :: XREAL_1:139

theorem :: XREAL_1:140

theorem :: XREAL_1:141

theorem :: XREAL_1:142

theorem :: XREAL_1:143

theorem :: XREAL_1:144

theorem :: XREAL_1:145

proof end;

theorem :: XREAL_1:146

proof end;

begin

theorem :: XREAL_1:147

proof end;

theorem :: XREAL_1:148

proof end;

theorem :: XREAL_1:149

proof end;

theorem :: XREAL_1:150

proof end;

theorem :: XREAL_1:151

begin

theorem :: XREAL_1:152

proof end;

theorem :: XREAL_1:153

proof end;

theorem :: XREAL_1:154

proof end;

theorem :: XREAL_1:155

proof end;

theorem :: XREAL_1:156

proof end;

theorem Th157: :: XREAL_1:157

proof end;

theorem :: XREAL_1:158

proof end;

theorem :: XREAL_1:159

proof end;

theorem :: XREAL_1:160

proof end;

theorem :: XREAL_1:161

proof end;

theorem :: XREAL_1:162

proof end;

theorem :: XREAL_1:163

proof end;

theorem :: XREAL_1:164

proof end;

theorem :: XREAL_1:165

proof end;

theorem :: XREAL_1:166

proof end;

theorem :: XREAL_1:167

proof end;

theorem :: XREAL_1:168

proof end;

begin

theorem Th169: :: XREAL_1:169

proof end;

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

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

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 )

( a = 0 & b = 0 )

proof end;

theorem :: XREAL_1:173

proof end;

theorem :: XREAL_1:174

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, 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:180

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

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

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

theorem :: XREAL_1:183

proof end;

theorem :: XREAL_1:184

proof end;

theorem :: XREAL_1:185

theorem :: XREAL_1:186

proof end;

theorem :: XREAL_1:187

theorem :: XREAL_1:188

proof end;

theorem :: XREAL_1:189

proof end;

theorem :: XREAL_1:190

proof end;

theorem :: XREAL_1:191

proof end;

theorem :: XREAL_1:192

proof end;

theorem :: XREAL_1:193

proof end;

theorem :: XREAL_1:194

proof end;

begin

theorem :: XREAL_1:195

proof end;

theorem :: XREAL_1:196

proof end;

theorem :: XREAL_1:197

proof end;

theorem :: XREAL_1:198

proof end;

theorem :: XREAL_1:199

proof end;

theorem :: XREAL_1:200

proof end;

theorem :: XREAL_1:201

proof end;

theorem :: XREAL_1:202

proof end;

theorem :: XREAL_1:203

proof end;

theorem :: XREAL_1:204

proof end;

theorem :: XREAL_1:205

proof end;

theorem :: XREAL_1:206

proof end;

theorem :: XREAL_1:207

proof end;

theorem :: XREAL_1:208

proof end;

theorem :: XREAL_1:209

proof end;

theorem :: XREAL_1:210

proof end;

begin

theorem Th211: :: XREAL_1:211

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;

theorem :: XREAL_1:212

proof end;

theorem :: XREAL_1:213

proof end;

theorem :: XREAL_1:214

theorem :: XREAL_1:215

proof end;

theorem :: XREAL_1:216

proof end;

begin

theorem :: XREAL_1:217

theorem :: XREAL_1:218

theorem :: XREAL_1:219

proof end;

theorem :: XREAL_1:220

proof end;

theorem :: XREAL_1:221

proof end;

theorem :: XREAL_1:222

proof end;

begin

theorem :: XREAL_1:223

proof end;

theorem :: XREAL_1:224

begin

theorem :: XREAL_1:225

proof end;

theorem :: XREAL_1:226

theorem :: XREAL_1:227

proof end;

begin

theorem :: XREAL_1:228

proof end;

registration

cluster -> ext-real Element of REAL ;

coherence

for b_{1} being Element of REAL holds b_{1} is ext-real

end;
coherence

for b

proof end;

theorem Th229: :: XREAL_1:229

proof end;

theorem :: XREAL_1:230

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

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;

theorem :: XREAL_1:232

proof end;

theorem :: XREAL_1:233

proof end;

begin

theorem :: XREAL_1:234

proof end;

theorem Th235: :: XREAL_1:235

proof end;

theorem :: XREAL_1:236

proof end;

theorem :: XREAL_1:237

proof end;

theorem :: XREAL_1:238

proof end;

theorem :: XREAL_1:239

proof end;