:: Real Numbers - Basic Theorems
:: by Library Committee
::
:: Received February 9, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ARYTM_2, SUBSET_1, ARYTM_3, ZFMISC_1, CARD_1, XXREAL_0,
ARYTM_0, FUNCOP_1, XBOOLE_0, ARYTM_1, RELAT_1, REAL_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FUNCT_4, ARYTM_2,
ARYTM_1, ARYTM_0, XCMPLX_0, XREAL_0, NUMBERS, XXREAL_0;
constructors FUNCT_4, ARYTM_1, ARYTM_0, XCMPLX_0, XXREAL_0, XREAL_0;
registrations ARYTM_2, XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin
reserve a,b,c,d for Real;
reserve r,s for Real;
theorem :: XREAL_1:1
ex b st a < b;
theorem :: XREAL_1:2
ex b st b < a;
theorem :: XREAL_1:3
ex c st a < c & b < c;
theorem :: XREAL_1:4
ex c st c < a & c < b;
theorem :: XREAL_1:5
a < b implies ex c st a < c & c < b;
begin
theorem :: XREAL_1:6
a <= b iff a + c <= b + c;
theorem :: XREAL_1:7
a <= b & c <= d implies a+c <= b+d;
theorem :: XREAL_1:8
a < b & c <= d implies a+c < b+d;
begin
theorem :: XREAL_1:9
a <= b iff a-c <= b-c;
theorem :: XREAL_1:10
a <= b iff c-b <= c-a;
theorem :: XREAL_1:11
a <= b-c implies c <= b-a;
theorem :: XREAL_1:12
a-b <= c implies a-c <= b;
theorem :: XREAL_1:13
a <= b & c <= d implies a-d <= b-c;
theorem :: XREAL_1:14
a < b & c <= d implies a-d < b-c;
theorem :: XREAL_1:15
a <= b & c < d implies a-d < b-c;
theorem :: XREAL_1:16
a-b <= c-d implies a-c <= b-d;
theorem :: XREAL_1:17
a-b <= c-d implies d-b <= c-a;
theorem :: XREAL_1:18
a-b <= c-d implies d-c <= b-a;
begin
theorem :: XREAL_1:19
a+b <= c iff a <= c-b;
theorem :: XREAL_1:20
a <= b+c iff a-b <= c;
theorem :: XREAL_1:21
a+b<=c+d iff a-c <= d-b;
theorem :: XREAL_1:22
a+b<=c-d implies a+d<=c-b;
theorem :: XREAL_1:23
a-b<=c+d implies a-d<=c+b;
begin
theorem :: XREAL_1:24
a<=b iff -b<=-a;
theorem :: XREAL_1:25
a<=-b implies b<=-a;
theorem :: XREAL_1:26
-b<=a implies -a<=b;
begin
theorem :: XREAL_1:27
0 <= a & 0 <= b & a+b = 0 implies a = 0;
theorem :: XREAL_1:28
a <= 0 & b <= 0 & a+b = 0 implies a = 0;
begin
theorem :: XREAL_1:29
0 < a implies b < b+a;
theorem :: XREAL_1:30
a < 0 implies a+b < b;
theorem :: XREAL_1:31
0 <= a implies b <= a+b;
theorem :: XREAL_1:32
a <= 0 implies a+b <= b;
begin
theorem :: XREAL_1:33
0 <= a & 0 <= b implies 0 <= a+b;
theorem :: XREAL_1:34
0 <= a & 0 < b implies 0 < a+b;
theorem :: XREAL_1:35
a <= 0 & c <= b implies c+a <= b;
theorem :: XREAL_1:36
a <= 0 & c < b implies c+a < b;
theorem :: XREAL_1:37
a < 0 & c <= b implies c+a < b;
theorem :: XREAL_1:38
0 <= a & b <= c implies b <= a+c;
theorem :: XREAL_1:39
0 < a & b <= c implies b < a+c;
theorem :: XREAL_1:40
0 <= a & b < c implies b < a+c;
begin
theorem :: XREAL_1:41
(for a being Real st a>0 holds c <= b+a) implies c <= b;
theorem :: XREAL_1:42
(for a being Real st a<0 holds b+a <= c) implies b <= c;
begin
theorem :: XREAL_1:43
0 <= a implies b-a <= b;
theorem :: XREAL_1:44
0 < a implies b-a < b;
theorem :: XREAL_1:45
a <= 0 implies b <= b-a;
theorem :: XREAL_1:46
a < 0 implies b < b-a;
theorem :: XREAL_1:47
a <= b implies a-b <= 0;
theorem :: XREAL_1:48
a <= b implies 0 <= b-a;
theorem :: XREAL_1:49
a < b implies a-b < 0;
theorem :: XREAL_1:50
a < b implies 0 < b-a;
theorem :: XREAL_1:51
0 <= a & b < c implies b-a < c;
theorem :: XREAL_1:52
a <= 0 & b <= c implies b <= c-a;
theorem :: XREAL_1:53
a <= 0 & b < c implies b < c-a;
theorem :: XREAL_1:54
a < 0 & b <= c implies b < c-a;
theorem :: XREAL_1:55
a <> b implies 0 < a-b or 0 < b-a;
begin
theorem :: XREAL_1:56
(for a being Real st a<0 holds c <= b-a) implies b>=c;
theorem :: XREAL_1:57
(for a being Real st a>0 holds b-a <= c) implies b<=c;
begin
theorem :: XREAL_1:58
a < 0 iff 0 < -a;
theorem :: XREAL_1:59
a <= -b implies a+b <= 0;
theorem :: XREAL_1:60
-a <= b implies 0 <= a+b;
theorem :: XREAL_1:61
a < -b implies a+b < 0;
theorem :: XREAL_1:62
-b < a implies 0 < a+b;
begin
theorem :: XREAL_1:63
0 <= a*a;
theorem :: XREAL_1:64
a <= b & 0 <= c implies a*c <= b*c;
theorem :: XREAL_1:65
a <= b & c <= 0 implies b*c <= a*c;
theorem :: XREAL_1:66
0 <= a & a <= b & 0 <= c & c <= d implies a*c <= b*d;
theorem :: XREAL_1:67
a <= 0 & b <= a & c <= 0 & d <= c implies a*c <= b*d;
theorem :: XREAL_1:68
0 < c & a < b implies a*c < b*c;
theorem :: XREAL_1:69
c < 0 & a < b implies b*c < a*c;
theorem :: XREAL_1:70
a < 0 & b <= a & c < 0 & d < c implies a*c < b*d;
begin
theorem :: XREAL_1:71
0 <= a & 0 <= b & 0 <= c & 0 <= d & a*c+b*d = 0 implies a = 0 or c = 0;
begin
theorem :: XREAL_1:72
0 <= c & b <= a implies b/c <= a/c;
theorem :: XREAL_1:73
c <= 0 & a <= b implies b/c <= a/c;
theorem :: XREAL_1:74
0 < c & a < b implies a/c < b/c;
theorem :: XREAL_1:75
c < 0 & a < b implies b/c < a/c;
theorem :: XREAL_1:76
0 < c & 0 < a & a < b implies c/b < c/a;
begin
theorem :: XREAL_1:77
0 < b & a*b <= c implies a <= c/b;
theorem :: XREAL_1:78
b < 0 & a*b <= c implies c/b <= a;
theorem :: XREAL_1:79
0 < b & c <= a*b implies c/b <= a;
theorem :: XREAL_1:80
b < 0 & c <= a*b implies a <= c/b;
theorem :: XREAL_1:81
0 < b & a*b < c implies a< c/b;
theorem :: XREAL_1:82
b < 0 & a*b < c implies c/b < a;
theorem :: XREAL_1:83
0 < b & c < a*b implies c/b < a;
theorem :: XREAL_1:84
b < 0 & c < a*b implies a < c/b;
begin
theorem :: XREAL_1:85
0 < a & a <= b implies b" <= a";
theorem :: XREAL_1:86
b < 0 & a <= b implies b" <= a";
theorem :: XREAL_1:87
b < 0 & a < b implies b" < a";
theorem :: XREAL_1:88
0 < a & a < b implies b" < a";
theorem :: XREAL_1:89
0 < b" & b" <= a" implies a <= b;
theorem :: XREAL_1:90
a" < 0 & b" <= a" implies a <= b;
theorem :: XREAL_1:91
0 < b" & b" < a" implies a < b;
theorem :: XREAL_1:92
a" < 0 & b" < a" implies a < b;
begin
theorem :: XREAL_1:93
0 <= a & (b-a)*(b+a) <= 0 implies -a <= b & b <= a;
theorem :: XREAL_1:94
0 <= a & (b-a)*(b+a) < 0 implies -a < b & b < a;
theorem :: XREAL_1:95
0 <= (b-a)*(b+a) implies b <= -a or a <= b;
theorem :: XREAL_1:96
0 <= a & 0 <= c & a < b & c < d implies a*c < b*d;
theorem :: XREAL_1:97
0 <= a & 0 < c & a < b & c <= d implies a*c < b*d;
theorem :: XREAL_1:98
0 < a & 0 < c & a <= b & c < d implies a*c < b*d;
theorem :: XREAL_1:99
0 < c & b < 0 & a < b implies c/b < c/a;
theorem :: XREAL_1:100
c < 0 & 0 < a & a < b implies c/a < c/b;
theorem :: XREAL_1:101
c < 0 & b < 0 & a < b implies c/a < c/b;
theorem :: XREAL_1:102
0 < b & 0 < d & a*d <= c*b implies a/b <= c/d;
theorem :: XREAL_1:103
b < 0 & d < 0 & a*d <= c*b implies a/b <= c/d;
theorem :: XREAL_1:104
0 < b & d < 0 & a*d <= c*b implies c/d <= a/b;
theorem :: XREAL_1:105
b < 0 & 0 < d & a*d <= c*b implies c/d <= a/b;
theorem :: XREAL_1:106
0 < b & 0 < d & a*d < c*b implies a/b < c/d;
theorem :: XREAL_1:107
b < 0 & d < 0 & a*d < c*b implies a/b < c/d;
theorem :: XREAL_1:108
0 < b & d < 0 & a*d < c*b implies c/d < a/b;
theorem :: XREAL_1:109
b < 0 & 0 < d & a*d < c*b implies c/d < a/b;
theorem :: XREAL_1:110
b < 0 & d < 0 & a*b < c/d implies a*d < c/b;
theorem :: XREAL_1:111
0 < b & 0 < d & a*b < c/d implies a*d < c/b;
theorem :: XREAL_1:112
b < 0 & d < 0 & c/d < a*b implies c/b < a*d;
theorem :: XREAL_1:113
0 < b & 0 < d & c/d < a*b implies c/b < a*d;
theorem :: XREAL_1:114
b < 0 & 0 < d & a*b < c/d implies c/b < a*d;
theorem :: XREAL_1:115
0 < b & d < 0 & a*b < c/d implies c/b < a*d;
theorem :: XREAL_1:116
b < 0 & 0 < d & c/d < a*b implies a*d < c/b;
theorem :: XREAL_1:117
0 < b & d < 0 & c/d < a*b implies a*d < c/b;
theorem :: XREAL_1:118
0 < a & 0 <= c & a <= b implies c/b <= c/a;
theorem :: XREAL_1:119
0 <= c & b < 0 & a <= b implies c/b <= c/a;
theorem :: XREAL_1:120
c <= 0 & 0 < a & a <= b implies c/a <= c/b;
theorem :: XREAL_1:121
c <= 0 & b < 0 & a <= b implies c/a <= c/b;
theorem :: XREAL_1:122
0 < a iff 0 < a";
theorem :: XREAL_1:123
a < 0 iff a" < 0;
theorem :: XREAL_1:124
a < 0 & 0 < b implies a" < b";
theorem :: XREAL_1:125
a" < 0 & 0 < b" implies a < b;
begin
theorem :: XREAL_1:126
a <= 0 & 0 <= a implies 0 = a*b;
theorem :: XREAL_1:127
0 <= a & 0 <= b implies 0 <= a*b;
theorem :: XREAL_1:128
a <= 0 & b <= 0 implies 0 <= a*b;
theorem :: XREAL_1:129
0 < a & 0 < b implies 0 < a*b;
theorem :: XREAL_1:130
a < 0 & b < 0 implies 0 < a*b;
theorem :: XREAL_1:131
0 <= a & b <= 0 implies a*b <= 0;
theorem :: XREAL_1:132
0 < a & b < 0 implies a*b < 0;
theorem :: XREAL_1:133
a*b<0 implies a>0 & b<0 or a<0 & b>0;
theorem :: XREAL_1:134
a*b>0 implies a>0 & b>0 or a<0 & b<0;
theorem :: XREAL_1:135
a <= 0 & b <= 0 implies 0 <= a/b;
theorem :: XREAL_1:136
0 <= a & 0 <= b implies 0 <= a/b;
theorem :: XREAL_1:137
0 <= a & b <= 0 implies a/b <= 0;
theorem :: XREAL_1:138
a <= 0 & 0 <= b implies a/b <= 0;
theorem :: XREAL_1:139
0 < a & 0 < b implies 0 < a/b;
theorem :: XREAL_1:140
a < 0 & b < 0 implies 0 < a/b;
theorem :: XREAL_1:141
a < 0 & 0 < b implies a/b < 0;
theorem :: XREAL_1:142
a < 0 & 0 < b implies b/a < 0;
theorem :: XREAL_1:143
a/b<0 implies b<0 & a>0 or b>0 & a<0;
theorem :: XREAL_1:144
a/b>0 implies b>0 & a>0 or b<0 & a<0;
begin
theorem :: XREAL_1:145
a <= b implies a < b+1;
theorem :: XREAL_1:146
a - 1 < a;
theorem :: XREAL_1:147
a <= b implies a-1 < b;
theorem :: XREAL_1:148
-1 < a implies 0 < 1+a;
theorem :: XREAL_1:149
a<1 implies 1-a>0;
begin
theorem :: XREAL_1:150
a <= 1 & 0 <= b & b <= 1 & a*b = 1 implies a=1;
theorem :: XREAL_1:151
0 <= a & 1 <= b implies a <= a*b;
theorem :: XREAL_1:152
a <= 0 & b <= 1 implies a <= a*b;
theorem :: XREAL_1:153
0 <= a & b <= 1 implies a*b <= a;
theorem :: XREAL_1:154
a <= 0 & 1 <= b implies a*b <= a;
theorem :: XREAL_1:155
0 < a & 1 < b implies a < a*b;
theorem :: XREAL_1:156
a < 0 & b < 1 implies a < a*b;
theorem :: XREAL_1:157
0 < a & b < 1 implies a*b < a;
theorem :: XREAL_1:158
a < 0 & 1 < b implies a*b < a;
theorem :: XREAL_1:159
1 <= a & 1 <= b implies 1 <= a*b;
theorem :: XREAL_1:160
0 <= a & a <= 1 & b <= 1 implies a*b <= 1;
theorem :: XREAL_1:161
1 < a & 1 <= b implies 1 < a*b;
theorem :: XREAL_1:162
0 <= a & a < 1 & b <= 1 implies a*b < 1;
theorem :: XREAL_1:163
a <= -1 & b <= -1 implies 1 <= a*b;
theorem :: XREAL_1:164
a < -1 & b <= -1 implies 1 < a*b;
theorem :: XREAL_1:165
a <= 0 & -1 <= a & -1 <= b implies a*b <= 1;
theorem :: XREAL_1:166
a <= 0 & -1 < a & -1 <= b implies a*b < 1;
begin
theorem :: XREAL_1:167
(for a st 1 < a holds c <= b*a) implies c <= b;
theorem :: XREAL_1:168
(for a st 0 < a & a < 1 holds b*a <= c) implies b <= c;
theorem :: XREAL_1:169
(for a st 0 < a & a < 1 holds b <= a*c) implies b <= 0;
theorem :: XREAL_1:170
0 <= d & d <= 1 & 0 <= a & 0 <= b & d*a+(1-d)*b=0 implies d=0 & b=0 or
d=1 & a=0 or a=0 & b=0;
theorem :: XREAL_1:171
0 <= d & a <= b implies a <= (1-d)*a+d*b;
theorem :: XREAL_1:172
d <= 1 & a <= b implies (1-d)*a+d*b <= b;
theorem :: XREAL_1:173
0 <= d & d <= 1 & a <= b & a <= c implies a <= (1-d)*b+d*c;
theorem :: XREAL_1:174
0 <= d & d <= 1 & b <= a & c <= a implies (1-d)*b+d*c <= a;
theorem :: XREAL_1:175
0 <= d & d <= 1 & a < b & a < c implies a < (1-d)*b+d*c;
theorem :: XREAL_1:176
0 <= d & d <= 1 & b < a & c < a implies (1-d)*b+d*c < a;
theorem :: XREAL_1:177
0 < d & d < 1 & a <= b & a < c implies a < (1-d)*b+d*c;
theorem :: XREAL_1:178
0 < d & d < 1 & b < a & c <= a implies (1-d)*b+d*c < a;
theorem :: XREAL_1:179
0 <= d & d <= 1 & a <= (1-d)*a+d*b & b < (1-d)*a+d*b implies d = 0;
theorem :: XREAL_1:180
0 <= d & d <= 1 & (1-d)*a+d*b <= a & (1-d)*a+d*b < b implies d = 0;
begin
theorem :: XREAL_1:181
0 < a & a <= b implies 1 <= b/a;
theorem :: XREAL_1:182
a < 0 & b <= a implies 1 <= b/a;
theorem :: XREAL_1:183
0 <= a & a <= b implies a/b <= 1;
theorem :: XREAL_1:184
b <= a & a <= 0 implies a/b <= 1;
theorem :: XREAL_1:185
0 <= a & b <= a implies b/a <= 1;
theorem :: XREAL_1:186
a <= 0 & a <= b implies b/a <= 1;
theorem :: XREAL_1:187
0 < a & a < b implies 1 < b/a;
theorem :: XREAL_1:188
a < 0 & b < a implies 1 < b/a;
theorem :: XREAL_1:189
0 <= a & a < b implies a/b < 1;
theorem :: XREAL_1:190
a <= 0 & b < a implies a/b < 1;
theorem :: XREAL_1:191
0 < a & b < a implies b/a < 1;
theorem :: XREAL_1:192
a < 0 & a < b implies b/a < 1;
begin
theorem :: XREAL_1:193
0 <= b & -b <= a implies -1 <= a/b;
theorem :: XREAL_1:194
0 <= b & -a <= b implies -1 <= a/b;
theorem :: XREAL_1:195
b <= 0 & a <= -b implies -1 <= a/b;
theorem :: XREAL_1:196
b <= 0 & b <= -a implies -1 <= a/b;
theorem :: XREAL_1:197
0 < b & -b < a implies -1 < a/b;
theorem :: XREAL_1:198
0 < b & -a < b implies -1 < a/b;
theorem :: XREAL_1:199
b < 0 & a < -b implies -1 < a/b;
theorem :: XREAL_1:200
b < 0 & b < -a implies -1 < a/b;
theorem :: XREAL_1:201
0 < b & a <= -b implies a/b <= -1;
theorem :: XREAL_1:202
0 < b & b <= -a implies a/b <= -1;
theorem :: XREAL_1:203
b < 0 & -b <= a implies a/b <= -1;
theorem :: XREAL_1:204
b < 0 & -a <= b implies a/b <= -1;
theorem :: XREAL_1:205
0 < b & a < -b implies a/b < -1;
theorem :: XREAL_1:206
0 < b & b < -a implies a/b < -1;
theorem :: XREAL_1:207
b < 0 & -b < a implies a/b < -1;
theorem :: XREAL_1:208
b < 0 & -a < b implies a/b < -1;
begin
theorem :: XREAL_1:209
(for a being Real st 0 < a & a < 1 holds c <= b/a)
implies c <= b;
theorem :: XREAL_1:210
(for a being Real st 1 < a holds b/a <= c) implies b <= c;
theorem :: XREAL_1:211
1 <= a implies a" <= 1;
theorem :: XREAL_1:212
1 < a implies a" < 1;
theorem :: XREAL_1:213
a <= -1 implies -1 <= a";
theorem :: XREAL_1:214
a < -1 implies -1 < a";
begin
theorem :: XREAL_1:215
0 < a implies 0 < a/2;
theorem :: XREAL_1:216
0 < a implies a/2 < a;
theorem :: XREAL_1:217
a <= 1/2 implies 2 * a - 1 <= 0;
theorem :: XREAL_1:218
a <= 1/2 implies 0 <= 1 - 2 * a;
theorem :: XREAL_1:219
a >= 1/2 implies 2 * a - 1 >= 0;
theorem :: XREAL_1:220
a >= 1/2 implies 0 >= 1 - 2 * a;
begin
theorem :: XREAL_1:221
0 < a implies a/3 < a;
theorem :: XREAL_1:222
0 < a implies 0 < a/3;
begin
theorem :: XREAL_1:223
0 < a implies a/4 < a;
theorem :: XREAL_1:224
0 < a implies 0 < a/4;
theorem :: XREAL_1:225
for a,b st b<>0 ex c st a=b/c;
begin :: Addenda
:: from TOPREAL3, 2006.07.15, A.T.
theorem :: XREAL_1:226
r~~ ext-real for Element of REAL;
end;
reserve p,q,r,s,t for ExtReal;
theorem :: XREAL_1:227
r < t implies ex s st r < s & s < t;
theorem :: XREAL_1:228
r < s & (for q st r < q & q < s holds t <= q) implies t <= r;
theorem :: XREAL_1:229
r < s & (for q st r < q & q < s holds q <= t) implies s <= t;
:: missing, 2008.08.13, A.T.
theorem :: XREAL_1:230
0 <= a & b <= c implies b-a <= c;
theorem :: XREAL_1:231
0 < a & b <= c implies b-a < c;
begin
theorem :: XREAL_1:232
a -' a = 0;
theorem :: XREAL_1:233
b <= a implies a -' b = a - b;
theorem :: XREAL_1:234
c <= a & c <= b & a -' c = b -' c implies a = b;
theorem :: XREAL_1:235
a >= b implies a -' b + b = a;
:: from LEXBFS, 2008.08.23, A.T.
theorem :: XREAL_1:236
a <= b & c < a implies b -' a < b -' c;
:: missing, 2010.05.18, A.T.
theorem :: XREAL_1:237
1 <= a implies a -' 1 < a;
~~