Home | Metamath
Proof Explorer Theorem List (p. 111 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
This includes adding two pairs of values 1..10 (where the right is less than the left) and where the left is less than the right for the values 1..10. | ||
Theorem | neg1cn 11001 | -1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ -1 ∈ ℂ | ||
Theorem | neg1rr 11002 | -1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.) |
⊢ -1 ∈ ℝ | ||
Theorem | neg1ne0 11003 | -1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -1 ≠ 0 | ||
Theorem | neg1lt0 11004 | -1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -1 < 0 | ||
Theorem | negneg1e1 11005 | --1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ --1 = 1 | ||
Theorem | 1pneg1e0 11006 | 1 + -1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 + -1) = 0 | ||
Theorem | 0m0e0 11007 | 0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (0 − 0) = 0 | ||
Theorem | 1m0e1 11008 | 1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 − 0) = 1 | ||
Theorem | 0p1e1 11009 | 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ (0 + 1) = 1 | ||
Theorem | 1p0e1 11010 | 1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 + 0) = 1 | ||
Theorem | 1p1e2 11011 | 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.) |
⊢ (1 + 1) = 2 | ||
Theorem | 2m1e1 11012 | 2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 11041. (Contributed by David A. Wheeler, 4-Jan-2017.) |
⊢ (2 − 1) = 1 | ||
Theorem | 1e2m1 11013 | 1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 1 = (2 − 1) | ||
Theorem | 3m1e2 11014 | 3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.) (Proof shortened by AV, 6-Sep-2021.) |
⊢ (3 − 1) = 2 | ||
Theorem | 4m1e3 11015 | 4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.) |
⊢ (4 − 1) = 3 | ||
Theorem | 5m1e4 11016 | 5 - 1 = 4. (Contributed by AV, 6-Sep-2021.) |
⊢ (5 − 1) = 4 | ||
Theorem | 6m1e5 11017 | 6 - 1 = 5. (Contributed by AV, 6-Sep-2021.) |
⊢ (6 − 1) = 5 | ||
Theorem | 7m1e6 11018 | 7 - 1 = 6. (Contributed by AV, 6-Sep-2021.) |
⊢ (7 − 1) = 6 | ||
Theorem | 8m1e7 11019 | 8 - 1 = 7. (Contributed by AV, 6-Sep-2021.) |
⊢ (8 − 1) = 7 | ||
Theorem | 9m1e8 11020 | 9 - 1 = 8. (Contributed by AV, 6-Sep-2021.) |
⊢ (9 − 1) = 8 | ||
Theorem | 2p2e4 11021 | 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 7508 is similar but proves 2 + 2 = 4 using ordinal natural numbers (finite integers starting at 0), so that proof depends on fewer intermediate steps. (Contributed by NM, 27-May-1999.) |
⊢ (2 + 2) = 4 | ||
Theorem | 2times 11022 | Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.) |
⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴)) | ||
Theorem | times2 11023 | A number times 2. (Contributed by NM, 16-Oct-2007.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · 2) = (𝐴 + 𝐴)) | ||
Theorem | 2timesi 11024 | Two times a number. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (2 · 𝐴) = (𝐴 + 𝐴) | ||
Theorem | times2i 11025 | A number times 2. (Contributed by NM, 11-May-2004.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · 2) = (𝐴 + 𝐴) | ||
Theorem | 2txmxeqx 11026 | Two times a complex number minus the number itself results in the number itself. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
⊢ (𝑋 ∈ ℂ → ((2 · 𝑋) − 𝑋) = 𝑋) | ||
Theorem | 2div2e1 11027 | 2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (2 / 2) = 1 | ||
Theorem | 2p1e3 11028 | 2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.) |
⊢ (2 + 1) = 3 | ||
Theorem | 1p2e3 11029 | 1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 + 2) = 3 | ||
Theorem | 3p1e4 11030 | 3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.) |
⊢ (3 + 1) = 4 | ||
Theorem | 4p1e5 11031 | 4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.) |
⊢ (4 + 1) = 5 | ||
Theorem | 5p1e6 11032 | 5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.) |
⊢ (5 + 1) = 6 | ||
Theorem | 6p1e7 11033 | 6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.) |
⊢ (6 + 1) = 7 | ||
Theorem | 7p1e8 11034 | 7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.) |
⊢ (7 + 1) = 8 | ||
Theorem | 8p1e9 11035 | 8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.) |
⊢ (8 + 1) = 9 | ||
Theorem | 9p1e10OLD 11036 | 9 + 1 = 10. (Contributed by Mario Carneiro, 18-Apr-2015.) Obsolete version of 9p1e10 11372 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (9 + 1) = 10 | ||
Theorem | 3p2e5 11037 | 3 + 2 = 5. (Contributed by NM, 11-May-2004.) |
⊢ (3 + 2) = 5 | ||
Theorem | 3p3e6 11038 | 3 + 3 = 6. (Contributed by NM, 11-May-2004.) |
⊢ (3 + 3) = 6 | ||
Theorem | 4p2e6 11039 | 4 + 2 = 6. (Contributed by NM, 11-May-2004.) |
⊢ (4 + 2) = 6 | ||
Theorem | 4p3e7 11040 | 4 + 3 = 7. (Contributed by NM, 11-May-2004.) |
⊢ (4 + 3) = 7 | ||
Theorem | 4p4e8 11041 | 4 + 4 = 8. (Contributed by NM, 11-May-2004.) |
⊢ (4 + 4) = 8 | ||
Theorem | 5p2e7 11042 | 5 + 2 = 7. (Contributed by NM, 11-May-2004.) |
⊢ (5 + 2) = 7 | ||
Theorem | 5p3e8 11043 | 5 + 3 = 8. (Contributed by NM, 11-May-2004.) |
⊢ (5 + 3) = 8 | ||
Theorem | 5p4e9 11044 | 5 + 4 = 9. (Contributed by NM, 11-May-2004.) |
⊢ (5 + 4) = 9 | ||
Theorem | 5p5e10OLD 11045 | 5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) Obsolete version of 5p5e10 11472 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (5 + 5) = 10 | ||
Theorem | 6p2e8 11046 | 6 + 2 = 8. (Contributed by NM, 11-May-2004.) |
⊢ (6 + 2) = 8 | ||
Theorem | 6p3e9 11047 | 6 + 3 = 9. (Contributed by NM, 11-May-2004.) |
⊢ (6 + 3) = 9 | ||
Theorem | 6p4e10OLD 11048 | 6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) Obsolete version of 6p4e10 11474 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (6 + 4) = 10 | ||
Theorem | 7p2e9 11049 | 7 + 2 = 9. (Contributed by NM, 11-May-2004.) |
⊢ (7 + 2) = 9 | ||
Theorem | 7p3e10OLD 11050 | 7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) Obsolete version of 7p3e10 11479 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (7 + 3) = 10 | ||
Theorem | 8p2e10OLD 11051 | 8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) Obsolete version of 8p2e10 11486 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (8 + 2) = 10 | ||
Theorem | 1t1e1 11052 | 1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ (1 · 1) = 1 | ||
Theorem | 2t1e2 11053 | 2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ (2 · 1) = 2 | ||
Theorem | 2t2e4 11054 | 2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.) |
⊢ (2 · 2) = 4 | ||
Theorem | 3t1e3 11055 | 3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (3 · 1) = 3 | ||
Theorem | 3t2e6 11056 | 3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.) |
⊢ (3 · 2) = 6 | ||
Theorem | 3t3e9 11057 | 3 times 3 equals 9. (Contributed by NM, 11-May-2004.) |
⊢ (3 · 3) = 9 | ||
Theorem | 4t2e8 11058 | 4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.) |
⊢ (4 · 2) = 8 | ||
Theorem | 5t2e10OLD 11059 | 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) Obsolete version of 5t2e10 11510 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (5 · 2) = 10 | ||
Theorem | 2t0e0 11060 | 2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (2 · 0) = 0 | ||
Theorem | 4d2e2 11061 | One half of four is two. (Contributed by NM, 3-Sep-1999.) |
⊢ (4 / 2) = 2 | ||
Theorem | 2nn 11062 | 2 is a positive integer. (Contributed by NM, 20-Aug-2001.) |
⊢ 2 ∈ ℕ | ||
Theorem | 3nn 11063 | 3 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
⊢ 3 ∈ ℕ | ||
Theorem | 4nn 11064 | 4 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
⊢ 4 ∈ ℕ | ||
Theorem | 5nn 11065 | 5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 5 ∈ ℕ | ||
Theorem | 6nn 11066 | 6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 6 ∈ ℕ | ||
Theorem | 7nn 11067 | 7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 7 ∈ ℕ | ||
Theorem | 8nn 11068 | 8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 8 ∈ ℕ | ||
Theorem | 9nn 11069 | 9 is a positive integer. (Contributed by NM, 21-Oct-2012.) |
⊢ 9 ∈ ℕ | ||
Theorem | 10nnOLD 11070 | Obsolete version of 10nn 11390 as of 6-Sep-2021. (Contributed by NM, 8-Nov-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 10 ∈ ℕ | ||
Theorem | 1lt2 11071 | 1 is less than 2. (Contributed by NM, 24-Feb-2005.) |
⊢ 1 < 2 | ||
Theorem | 2lt3 11072 | 2 is less than 3. (Contributed by NM, 26-Sep-2010.) |
⊢ 2 < 3 | ||
Theorem | 1lt3 11073 | 1 is less than 3. (Contributed by NM, 26-Sep-2010.) |
⊢ 1 < 3 | ||
Theorem | 3lt4 11074 | 3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 3 < 4 | ||
Theorem | 2lt4 11075 | 2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 2 < 4 | ||
Theorem | 1lt4 11076 | 1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 1 < 4 | ||
Theorem | 4lt5 11077 | 4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 4 < 5 | ||
Theorem | 3lt5 11078 | 3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 3 < 5 | ||
Theorem | 2lt5 11079 | 2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 2 < 5 | ||
Theorem | 1lt5 11080 | 1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 1 < 5 | ||
Theorem | 5lt6 11081 | 5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 5 < 6 | ||
Theorem | 4lt6 11082 | 4 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 4 < 6 | ||
Theorem | 3lt6 11083 | 3 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 3 < 6 | ||
Theorem | 2lt6 11084 | 2 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 2 < 6 | ||
Theorem | 1lt6 11085 | 1 is less than 6. (Contributed by NM, 19-Oct-2012.) |
⊢ 1 < 6 | ||
Theorem | 6lt7 11086 | 6 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 6 < 7 | ||
Theorem | 5lt7 11087 | 5 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 5 < 7 | ||
Theorem | 4lt7 11088 | 4 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 4 < 7 | ||
Theorem | 3lt7 11089 | 3 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 3 < 7 | ||
Theorem | 2lt7 11090 | 2 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 2 < 7 | ||
Theorem | 1lt7 11091 | 1 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 1 < 7 | ||
Theorem | 7lt8 11092 | 7 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 7 < 8 | ||
Theorem | 6lt8 11093 | 6 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 6 < 8 | ||
Theorem | 5lt8 11094 | 5 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 5 < 8 | ||
Theorem | 4lt8 11095 | 4 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 4 < 8 | ||
Theorem | 3lt8 11096 | 3 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 3 < 8 | ||
Theorem | 2lt8 11097 | 2 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 2 < 8 | ||
Theorem | 1lt8 11098 | 1 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 1 < 8 | ||
Theorem | 8lt9 11099 | 8 is less than 9. (Contributed by Mario Carneiro, 19-Feb-2014.) |
⊢ 8 < 9 | ||
Theorem | 7lt9 11100 | 7 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 7 < 9 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |