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