Home | Metamath
Proof Explorer Theorem List (p. 113 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 3lt5 11201 | 3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 2lt5 11202 | 2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 1lt5 11203 | 1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 5lt6 11204 | 5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 4lt6 11205 | 4 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 3lt6 11206 | 3 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 2lt6 11207 | 2 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 1lt6 11208 | 1 is less than 6. (Contributed by NM, 19-Oct-2012.) |
Theorem | 6lt7 11209 | 6 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 5lt7 11210 | 5 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 4lt7 11211 | 4 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 3lt7 11212 | 3 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 2lt7 11213 | 2 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 1lt7 11214 | 1 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 7lt8 11215 | 7 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 6lt8 11216 | 6 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 5lt8 11217 | 5 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 4lt8 11218 | 4 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 3lt8 11219 | 3 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 2lt8 11220 | 2 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 1lt8 11221 | 1 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 8lt9 11222 | 8 is less than 9. (Contributed by Mario Carneiro, 19-Feb-2014.) |
Theorem | 7lt9 11223 | 7 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
Theorem | 6lt9 11224 | 6 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
Theorem | 5lt9 11225 | 5 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
Theorem | 4lt9 11226 | 4 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
Theorem | 3lt9 11227 | 3 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
Theorem | 2lt9 11228 | 2 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
Theorem | 1lt9 11229 | 1 is less than 9. (Contributed by NM, 19-Oct-2012.) (Revised by Mario Carneiro, 9-Mar-2015.) |
Theorem | 9lt10OLD 11230 | 9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) Obsolete version of 9lt10 11673 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 8lt10OLD 11231 | 8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) Obsolete version of 8lt10 11674 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 7lt10OLD 11232 | 7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) Obsolete version of 7lt10 11675 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 6lt10OLD 11233 | 6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) Obsolete version of 6lt10 11676 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 5lt10OLD 11234 | 5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) Obsolete version of 5lt10 11677 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 4lt10OLD 11235 | 4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) Obsolete version of 4lt10 11678 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 3lt10OLD 11236 | 3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) Obsolete version of 3lt10 11679 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 2lt10OLD 11237 | 2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) Obsolete version of 2lt10 11680 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 1lt10OLD 11238 | 1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario Carneiro, 9-Mar-2015.) Obsolete version of 1lt10 11681 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 0ne2 11239 | 0 is not equal to 2. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 1ne2 11240 | 1 is not equal to 2. (Contributed by NM, 19-Oct-2012.) |
Theorem | 1le2 11241 | 1 is less than or equal to 2 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 2cnne0 11242 | 2 is a nonzero complex number (common case). (Contributed by David A. Wheeler, 7-Dec-2018.) |
Theorem | 2rene0 11243 | 2 is a nonzero real number (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 1le3 11244 | 1 is less than or equal to 3. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | neg1mulneg1e1 11245 | is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | halfre 11246 | One-half is real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | halfcn 11247 | One-half is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | halfgt0 11248 | One-half is greater than zero. (Contributed by NM, 24-Feb-2005.) |
Theorem | halfge0 11249 | One-half is not negative. (Contributed by AV, 7-Jun-2020.) |
Theorem | halflt1 11250 | One-half is less than one. (Contributed by NM, 24-Feb-2005.) |
Theorem | 1mhlfehlf 11251 | Prove that 1 - 1/2 = 1/2. (Contributed by David A. Wheeler, 4-Jan-2017.) |
Theorem | 8th4div3 11252 | An eighth of four thirds is a sixth. (Contributed by Paul Chapman, 24-Nov-2007.) |
Theorem | halfpm6th 11253 | One half plus or minus one sixth. (Contributed by Paul Chapman, 17-Jan-2008.) |
Theorem | it0e0 11254 | i times 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 2mulicn 11255 | (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 2muline0 11256 | (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | halfcl 11257 | Closure of half of a number (common case). (Contributed by NM, 1-Jan-2006.) |
Theorem | rehalfcl 11258 | Real closure of half. (Contributed by NM, 1-Jan-2006.) |
Theorem | half0 11259 | Half of a number is zero iff the number is zero. (Contributed by NM, 20-Apr-2006.) |
Theorem | 2halves 11260 | Two halves make a whole. (Contributed by NM, 11-Apr-2005.) |
Theorem | halfpos2 11261 | A number is positive iff its half is positive. (Contributed by NM, 10-Apr-2005.) |
Theorem | halfpos 11262 | A positive number is greater than its half. (Contributed by NM, 28-Oct-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
Theorem | halfnneg2 11263 | A number is nonnegative iff its half is nonnegative. (Contributed by NM, 9-Dec-2005.) |
Theorem | halfaddsubcl 11264 | Closure of half-sum and half-difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
Theorem | halfaddsub 11265 | Sum and difference of half-sum and half-difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
Theorem | subhalfhalf 11266 | Subtracting the half of a number from the number yields the half of the number. (Contributed by AV, 28-Jun-2021.) |
Theorem | lt2halves 11267 | A sum is less than the whole if each term is less than half. (Contributed by NM, 13-Dec-2006.) |
Theorem | addltmul 11268 | Sum is less than product for numbers greater than 2. (Contributed by Stefan Allan, 24-Sep-2010.) |
Theorem | nominpos 11269* | There is no smallest positive real number. (Contributed by NM, 28-Oct-2004.) |
Theorem | avglt1 11270 | Ordering property for average. (Contributed by Mario Carneiro, 28-May-2014.) |
Theorem | avglt2 11271 | Ordering property for average. (Contributed by Mario Carneiro, 28-May-2014.) |
Theorem | avgle1 11272 | Ordering property for average. (Contributed by Mario Carneiro, 28-May-2014.) |
Theorem | avgle2 11273 | Ordering property for average. (Contributed by Jeff Hankins, 15-Sep-2013.) (Revised by Mario Carneiro, 28-May-2014.) |
Theorem | avgle 11274 | The average of two numbers is less than or equal to at least one of them. (Contributed by NM, 9-Dec-2005.) (Revised by Mario Carneiro, 28-May-2014.) |
Theorem | 2timesd 11275 | Two times a number. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | times2d 11276 | A number times 2. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | halfcld 11277 | Closure of half of a number (frequently used special case). (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | 2halvesd 11278 | Two halves make a whole. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | rehalfcld 11279 | Real closure of half. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lt2halvesd 11280 | A sum is less than the whole if each term is less than half. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | rehalfcli 11281 | Half a real number is real. Inference form. (Contributed by David Moews, 28-Feb-2017.) |
Theorem | lt2addmuld 11282 | If two real numbers are less than a third real number, the sum of the two real numbers is less than twice the third real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | add1p1 11283 | Adding two times 1 to a number. (Contributed by AV, 22-Sep-2018.) |
Theorem | sub1m1 11284 | Subtracting two times 1 from a number. (Contributed by AV, 23-Oct-2018.) |
Theorem | cnm2m1cnm3 11285 | Subtracting 2 and afterwards 1 from a number results in the difference between the number and 3. (Contributed by Alexander van der Vekens, 16-Sep-2018.) |
Theorem | xp1d2m1eqxm1d2 11286 | A complex number increased by 1, then divided by 2, then decreased by 1 equals the complex number decreased by 1 and then divided by 2. (Contributed by AV, 24-May-2020.) |
Theorem | div4p1lem1div2 11287 | An integer greater than 5, divided by 4 and increased by 1, is less than or equal to the half of the integer minus 1. (Contributed by AV, 8-Jul-2021.) |
Theorem | nnunb 11288* | The set of positive integers is unbounded above. Theorem I.28 of [Apostol] p. 26. (Contributed by NM, 21-Jan-1997.) |
Theorem | arch 11289* | Archimedean property of real numbers. For any real number, there is an integer greater than it. Theorem I.29 of [Apostol] p. 26. (Contributed by NM, 21-Jan-1997.) |
Theorem | nnrecl 11290* | There exists a positive integer whose reciprocal is less than a given positive real. Exercise 3 of [Apostol] p. 28. (Contributed by NM, 8-Nov-2004.) |
Theorem | bndndx 11291* | A bounded real sequence is less than or equal to at least one of its indices. (Contributed by NM, 18-Jan-2008.) |
Syntax | cn0 11292 | Extend class notation to include the class of nonnegative integers. |
Definition | df-n0 11293 | Define the set of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.) |
Theorem | elnn0 11294 | Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002.) |
Theorem | nnssnn0 11295 | Positive naturals are a subset of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.) |
Theorem | nn0ssre 11296 | Nonnegative integers are a subset of the reals. (Contributed by Raph Levien, 10-Dec-2002.) |
Theorem | nn0sscn 11297 | Nonnegative integers are a subset of the complex numbers.) (Contributed by NM, 9-May-2004.) |
Theorem | nn0ex 11298 | The set of nonnegative integers exists. (Contributed by NM, 18-Jul-2004.) |
Theorem | nnnn0 11299 | A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.) |
Theorem | nnnn0i 11300 | A positive integer is a nonnegative integer. (Contributed by NM, 20-Jun-2005.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |