:: Real Numbers - Basic Theorems
:: by Library Committee
::
:: Received February 9, 2005
:: Copyright (c) 2005 Association of Mizar Users
Lm1:
for r, s being real number st ( ( r in REAL+ & s in REAL+ & ex x', y' being Element of REAL+ st
( r = x' & s = y' & x' <=' y' ) ) or ( r in [:{0 },REAL+ :] & s in [:{0 },REAL+ :] & ex x', y' being Element of REAL+ st
( r = [0 ,x'] & s = [0 ,y'] & y' <=' x' ) ) or ( s in REAL+ & r in [:{0 },REAL+ :] ) ) holds
r <= s
Lm2:
for a being real number
for x1, x2 being Element of REAL st a = [*x1,x2*] holds
( x2 = 0 & a = x1 )
Lm3:
for a', b' being Element of REAL
for a, b being real number st a' = a & b' = b holds
+ a',b' = a + b
Lm4:
{} in {{} }
by TARSKI:def 1;
Lm5:
for a, b, c being real number st a <= b holds
a + c <= b + c
Lm6:
for a, b, c, d being real number st a <= b & c <= d holds
a + c <= b + d
Lm7:
for a, b, c being real number st a <= b holds
a - c <= b - c
Lm8:
for a, b, c, d being real number st a < b & c <= d holds
a + c < b + d
Lm9:
for a, b being real number st 0 < a holds
b < b + a
theorem :: XREAL_1:1
canceled;
theorem :: XREAL_1:2
canceled;
theorem Th3: :: XREAL_1:3
theorem Th4: :: XREAL_1:4
theorem :: XREAL_1:5
Lm10:
for a, c, b being real number st a + c <= b + c holds
a <= b
theorem :: XREAL_1:6
Lm11:
for a', b' being Element of REAL
for a, b being real number st a' = a & b' = b holds
* a',b' = a * b
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
Lm13:
for c, a, b being real number st 0 < c & a < b holds
a * c < b * c
theorem Th7: :: XREAL_1:7
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
Lm15:
for b, a being real number st - b <= - a holds
a <= b
theorem Th11: :: XREAL_1:11
theorem :: XREAL_1:12
Lm16:
for a, b, c being real number st a + b <= c holds
a <= c - b
Lm17:
for a, b, c being real number st a <= b - c holds
a + c <= b
Lm18:
for a, b, c being real number st a <= b + c holds
a - b <= c
Lm19:
for a, b, c being real number st a - b <= c holds
a <= b + c
theorem :: XREAL_1:13
theorem :: XREAL_1:14
theorem Th15: :: XREAL_1:15
theorem Th16: :: XREAL_1:16
theorem Th17: :: XREAL_1:17
Lm20:
for a, b, c, d being real number st a + b <= c + d holds
a - c <= d - b
theorem :: XREAL_1:18
theorem :: XREAL_1:19
theorem :: XREAL_1:20
theorem :: XREAL_1:21
theorem :: XREAL_1:22
theorem :: XREAL_1:23
theorem :: XREAL_1:24
theorem :: XREAL_1:25
theorem :: XREAL_1:26
Lm21:
for a, b being real number st a < b holds
0 < b - a
theorem Th27: :: XREAL_1:27
Lm22:
for a, b being real number st a <= b holds
0 <= b - a
theorem Th28: :: XREAL_1:28
theorem :: XREAL_1:29
theorem :: XREAL_1:30
theorem :: XREAL_1:31
theorem :: XREAL_1:32
Lm23:
for a, b being real number st a < b holds
a - b < 0
theorem :: XREAL_1:33
theorem :: XREAL_1:34
theorem :: XREAL_1:35
theorem :: XREAL_1:36
theorem Th37: :: XREAL_1:37
theorem Th38: :: XREAL_1:38
theorem Th39: :: XREAL_1:39
theorem Th40: :: XREAL_1:40
theorem Th41: :: XREAL_1:41
theorem Th42: :: XREAL_1:42
Lm24:
for c, a, b being real number st c < 0 & a < b holds
b * c < a * c
Lm25:
for c, b, a being real number st 0 <= c & b <= a holds
b / c <= a / c
Lm26:
for c, a, b being real number st 0 < c & a < b holds
a / c < b / c
Lm27:
for a being real number st 0 < a holds
a / 2 < a
theorem :: XREAL_1:43
theorem :: XREAL_1:44
theorem :: XREAL_1:45
theorem :: XREAL_1:46
theorem :: XREAL_1:47
theorem :: XREAL_1:48
theorem :: XREAL_1:49
theorem Th50: :: XREAL_1:50
theorem :: XREAL_1:51
theorem :: XREAL_1:52
theorem :: XREAL_1:53
theorem :: XREAL_1:54
theorem :: XREAL_1:55
theorem :: XREAL_1:56
theorem :: XREAL_1:57
theorem :: XREAL_1:58
theorem :: XREAL_1:59
theorem :: XREAL_1:60
theorem :: XREAL_1:61
theorem :: XREAL_1:62
theorem :: XREAL_1:63
theorem :: XREAL_1:64
Lm28:
for a, b, c being real number st a <= b & c <= 0 holds
b * c <= a * c
theorem :: XREAL_1:65
theorem :: XREAL_1:66
theorem :: XREAL_1:67
theorem Th68: :: XREAL_1:68
theorem :: XREAL_1:69
theorem :: XREAL_1:70
theorem :: XREAL_1:71
theorem :: XREAL_1:72
theorem :: XREAL_1:73
Lm29:
for c, a, b being real number st c < 0 & a < b holds
b / c < a / c
Lm30:
for c, b, a being real number st c <= 0 & b / c < a / c holds
a < b
theorem :: XREAL_1:74
theorem :: XREAL_1:75
theorem :: XREAL_1:76
theorem :: XREAL_1:77
theorem :: XREAL_1:78
Lm31:
for b, a being real number st b < 0 & a < b holds
b " < a "
theorem Th79: :: XREAL_1:79
theorem Th80: :: XREAL_1:80
theorem Th81: :: XREAL_1:81
theorem Th82: :: XREAL_1:82
theorem Th83: :: XREAL_1:83
theorem Th84: :: XREAL_1:84
theorem Th85: :: XREAL_1:85
theorem Th86: :: XREAL_1:86
Lm32:
for a, b being real number st 0 < a & a <= b holds
b " <= a "
Lm33:
for b, a being real number st b < 0 & a <= b holds
b " <= a "
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 "
theorem :: XREAL_1:90
theorem :: XREAL_1:91
theorem :: XREAL_1:92
theorem :: XREAL_1:93
theorem :: XREAL_1:94
Lm35:
for b being real number
for a being non positive non negative real number holds 0 = a * b
;
theorem :: XREAL_1:95
theorem :: XREAL_1:96
theorem :: XREAL_1:97
theorem :: XREAL_1:98
theorem :: XREAL_1:99
theorem Th100: :: XREAL_1:100
theorem :: XREAL_1:101
theorem :: XREAL_1:102
theorem :: XREAL_1:103
theorem :: XREAL_1:104
theorem :: XREAL_1:105
theorem :: XREAL_1:106
theorem :: XREAL_1:107
theorem :: XREAL_1:108
theorem :: XREAL_1:109
theorem :: XREAL_1:110
theorem :: XREAL_1:111
theorem :: XREAL_1:112
theorem :: XREAL_1:113
theorem :: XREAL_1:114
theorem :: XREAL_1:115
theorem :: XREAL_1:116
theorem :: XREAL_1:117
theorem :: XREAL_1:118
theorem :: XREAL_1:119
theorem :: XREAL_1:120
theorem :: XREAL_1:121
theorem :: XREAL_1:122
theorem :: XREAL_1:123
theorem :: XREAL_1:124
theorem :: XREAL_1:125
theorem Th126: :: XREAL_1:126
theorem :: XREAL_1:127
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
theorem :: XREAL_1:136
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
theorem :: XREAL_1:146
theorem :: XREAL_1:147
theorem :: XREAL_1:148
theorem :: XREAL_1:149
theorem :: XREAL_1:150
theorem :: XREAL_1:151
theorem :: XREAL_1:152
theorem :: XREAL_1:153
theorem :: XREAL_1:154
theorem :: XREAL_1:155
theorem :: XREAL_1:156
theorem Th157: :: XREAL_1:157
theorem :: XREAL_1:158
theorem :: XREAL_1:159
theorem :: XREAL_1:160
theorem :: XREAL_1:161
theorem :: XREAL_1:162
theorem :: XREAL_1:163
theorem :: XREAL_1:164
theorem :: XREAL_1:165
theorem :: XREAL_1:166
theorem :: XREAL_1:167
theorem :: XREAL_1:168
theorem Th169: :: XREAL_1:169
Lm36:
for a being real number st 1 < a holds
a " < 1
theorem :: XREAL_1:170
Lm37:
for a, b being real number st a <= b & 0 <= a holds
a / b <= 1
Lm38:
for b, a being real number st b <= a & 0 <= a holds
b / a <= 1
theorem :: XREAL_1:171
theorem :: XREAL_1:172
theorem :: XREAL_1:173
theorem :: XREAL_1:174
theorem :: XREAL_1:175
theorem :: XREAL_1:176
theorem :: XREAL_1:177
theorem :: XREAL_1:178
theorem :: XREAL_1:179
theorem :: XREAL_1:180
theorem :: XREAL_1:181
theorem :: XREAL_1:182
theorem :: XREAL_1:183
theorem :: XREAL_1:184
theorem :: XREAL_1:185
theorem :: XREAL_1:186
theorem :: XREAL_1:187
theorem :: XREAL_1:188
theorem :: XREAL_1:189
theorem :: XREAL_1:190
theorem :: XREAL_1:191
theorem :: XREAL_1:192
theorem :: XREAL_1:193
theorem :: XREAL_1:194
theorem :: XREAL_1:195
theorem :: XREAL_1:196
theorem :: XREAL_1:197
theorem :: XREAL_1:198
theorem :: XREAL_1:199
theorem :: XREAL_1:200
theorem :: XREAL_1:201
theorem :: XREAL_1:202
theorem :: XREAL_1:203
theorem :: XREAL_1:204
theorem :: XREAL_1:205
theorem :: XREAL_1:206
theorem :: XREAL_1:207
theorem :: XREAL_1:208
theorem :: XREAL_1:209
theorem :: XREAL_1:210
theorem Th211: :: XREAL_1:211
theorem :: XREAL_1:212
theorem :: XREAL_1:213
theorem :: XREAL_1:214
theorem :: XREAL_1:215
theorem :: XREAL_1:216
theorem :: XREAL_1:217
theorem :: XREAL_1:218
theorem :: XREAL_1:219
theorem :: XREAL_1:220
theorem :: XREAL_1:221
theorem :: XREAL_1:222
theorem :: XREAL_1:223
theorem :: XREAL_1:224
theorem :: XREAL_1:225
theorem :: XREAL_1:226
theorem :: XREAL_1:227
theorem :: XREAL_1:228
theorem Th229: :: XREAL_1:229
theorem :: XREAL_1:230
theorem :: XREAL_1:231
theorem :: XREAL_1:232
theorem :: XREAL_1:233
theorem :: XREAL_1:234
theorem Th235: :: XREAL_1:235
theorem :: XREAL_1:236
theorem :: XREAL_1:237
theorem :: XREAL_1:238