Home | Metamath
Proof Explorer Theorem List (p. 112 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 | 6re 11101 | The number 6 is real. (Contributed by NM, 27-May-1999.) |
Theorem | 6cn 11102 | The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 7re 11103 | The number 7 is real. (Contributed by NM, 27-May-1999.) |
Theorem | 7cn 11104 | The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 8re 11105 | The number 8 is real. (Contributed by NM, 27-May-1999.) |
Theorem | 8cn 11106 | The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 9re 11107 | The number 9 is real. (Contributed by NM, 27-May-1999.) |
Theorem | 9cn 11108 | The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 10reOLD 11109 | Obsolete version of 10re 11517 as of 8-Sep-2021. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 0le0 11110 | Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | 0le2 11111 | 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.) |
Theorem | 2pos 11112 | The number 2 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 2ne0 11113 | The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.) |
Theorem | 3pos 11114 | The number 3 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 3ne0 11115 | The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Theorem | 4pos 11116 | The number 4 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 4ne0 11117 | The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.) |
Theorem | 5pos 11118 | The number 5 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 6pos 11119 | The number 6 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 7pos 11120 | The number 7 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 8pos 11121 | The number 8 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 9pos 11122 | The number 9 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 10posOLD 11123 | The number 10 is positive. (Contributed by NM, 5-Feb-2007.) Obsolete version of 10pos 11515 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
This section includes specific theorems about one-digit natural numbers (membership, addition, subtraction, multiplication, division, ordering). | ||
Theorem | neg1cn 11124 | -1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | neg1rr 11125 | -1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.) |
Theorem | neg1ne0 11126 | -1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | neg1lt0 11127 | -1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | negneg1e1 11128 | is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 1pneg1e0 11129 | is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 0m0e0 11130 | 0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 1m0e1 11131 | 1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 0p1e1 11132 | 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | 1p0e1 11133 | 1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 1p1e2 11134 | 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.) |
Theorem | 2m1e1 11135 | 2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 11164. (Contributed by David A. Wheeler, 4-Jan-2017.) |
Theorem | 1e2m1 11136 | 1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 3m1e2 11137 | 3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.) (Proof shortened by AV, 6-Sep-2021.) |
Theorem | 4m1e3 11138 | 4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.) |
Theorem | 5m1e4 11139 | 5 - 1 = 4. (Contributed by AV, 6-Sep-2021.) |
Theorem | 6m1e5 11140 | 6 - 1 = 5. (Contributed by AV, 6-Sep-2021.) |
Theorem | 7m1e6 11141 | 7 - 1 = 6. (Contributed by AV, 6-Sep-2021.) |
Theorem | 8m1e7 11142 | 8 - 1 = 7. (Contributed by AV, 6-Sep-2021.) |
Theorem | 9m1e8 11143 | 9 - 1 = 8. (Contributed by AV, 6-Sep-2021.) |
Theorem | 2p2e4 11144 | Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: mmset.html#trivia. This proof is simple, but it depends on many other proof steps because 2 and 4 are complex numbers and thus it depends on our construction of complex numbers. The proof o2p2e4 7621 is similar but proves using ordinal natural numbers (finite integers starting at 0), so that proof depends on fewer intermediate steps. (Contributed by NM, 27-May-1999.) |
Theorem | 2times 11145 | Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.) |
Theorem | times2 11146 | A number times 2. (Contributed by NM, 16-Oct-2007.) |
Theorem | 2timesi 11147 | Two times a number. (Contributed by NM, 1-Aug-1999.) |
Theorem | times2i 11148 | A number times 2. (Contributed by NM, 11-May-2004.) |
Theorem | 2txmxeqx 11149 | Two times a complex number minus the number itself results in the number itself. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
Theorem | 2div2e1 11150 | 2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 2p1e3 11151 | 2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 1p2e3 11152 | 1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 3p1e4 11153 | 3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 4p1e5 11154 | 4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 5p1e6 11155 | 5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 6p1e7 11156 | 6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 7p1e8 11157 | 7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 8p1e9 11158 | 8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 9p1e10OLD 11159 | 9 + 1 = 10. (Contributed by Mario Carneiro, 18-Apr-2015.) Obsolete version of 9p1e10 11496 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 3p2e5 11160 | 3 + 2 = 5. (Contributed by NM, 11-May-2004.) |
Theorem | 3p3e6 11161 | 3 + 3 = 6. (Contributed by NM, 11-May-2004.) |
Theorem | 4p2e6 11162 | 4 + 2 = 6. (Contributed by NM, 11-May-2004.) |
Theorem | 4p3e7 11163 | 4 + 3 = 7. (Contributed by NM, 11-May-2004.) |
Theorem | 4p4e8 11164 | 4 + 4 = 8. (Contributed by NM, 11-May-2004.) |
Theorem | 5p2e7 11165 | 5 + 2 = 7. (Contributed by NM, 11-May-2004.) |
Theorem | 5p3e8 11166 | 5 + 3 = 8. (Contributed by NM, 11-May-2004.) |
Theorem | 5p4e9 11167 | 5 + 4 = 9. (Contributed by NM, 11-May-2004.) |
Theorem | 5p5e10OLD 11168 | 5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) Obsolete version of 5p5e10 11596 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 6p2e8 11169 | 6 + 2 = 8. (Contributed by NM, 11-May-2004.) |
Theorem | 6p3e9 11170 | 6 + 3 = 9. (Contributed by NM, 11-May-2004.) |
Theorem | 6p4e10OLD 11171 | 6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) Obsolete version of 6p4e10 11598 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 7p2e9 11172 | 7 + 2 = 9. (Contributed by NM, 11-May-2004.) |
Theorem | 7p3e10OLD 11173 | 7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) Obsolete version of 7p3e10 11603 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 8p2e10OLD 11174 | 8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) Obsolete version of 8p2e10 11610 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 1t1e1 11175 | 1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | 2t1e2 11176 | 2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | 2t2e4 11177 | 2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.) |
Theorem | 3t1e3 11178 | 3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 3t2e6 11179 | 3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.) |
Theorem | 3t3e9 11180 | 3 times 3 equals 9. (Contributed by NM, 11-May-2004.) |
Theorem | 4t2e8 11181 | 4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.) |
Theorem | 5t2e10OLD 11182 | 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) Obsolete version of 5t2e10 11634 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 2t0e0 11183 | 2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 4d2e2 11184 | One half of four is two. (Contributed by NM, 3-Sep-1999.) |
Theorem | 2nn 11185 | 2 is a positive integer. (Contributed by NM, 20-Aug-2001.) |
Theorem | 3nn 11186 | 3 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
Theorem | 4nn 11187 | 4 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
Theorem | 5nn 11188 | 5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 6nn 11189 | 6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 7nn 11190 | 7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 8nn 11191 | 8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 9nn 11192 | 9 is a positive integer. (Contributed by NM, 21-Oct-2012.) |
Theorem | 10nnOLD 11193 | Obsolete version of 10nn 11514 as of 6-Sep-2021. (Contributed by NM, 8-Nov-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 1lt2 11194 | 1 is less than 2. (Contributed by NM, 24-Feb-2005.) |
Theorem | 2lt3 11195 | 2 is less than 3. (Contributed by NM, 26-Sep-2010.) |
Theorem | 1lt3 11196 | 1 is less than 3. (Contributed by NM, 26-Sep-2010.) |
Theorem | 3lt4 11197 | 3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 2lt4 11198 | 2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 1lt4 11199 | 1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 4lt5 11200 | 4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |