![]() |
Intuitionistic Logic Explorer Theorem List (p. 91 of 145) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2ap0 9001 | The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) |
![]() ![]() ![]() | ||
Theorem | 3pos 9002 | The number 3 is positive. (Contributed by NM, 27-May-1999.) |
![]() ![]() ![]() ![]() | ||
Theorem | 3ne0 9003 | The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
![]() ![]() ![]() ![]() | ||
Theorem | 3ap0 9004 | The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
![]() ![]() ![]() | ||
Theorem | 4pos 9005 | The number 4 is positive. (Contributed by NM, 27-May-1999.) |
![]() ![]() ![]() ![]() | ||
Theorem | 4ne0 9006 | The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.) |
![]() ![]() ![]() ![]() | ||
Theorem | 4ap0 9007 | The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
![]() ![]() ![]() | ||
Theorem | 5pos 9008 | The number 5 is positive. (Contributed by NM, 27-May-1999.) |
![]() ![]() ![]() ![]() | ||
Theorem | 6pos 9009 | The number 6 is positive. (Contributed by NM, 27-May-1999.) |
![]() ![]() ![]() ![]() | ||
Theorem | 7pos 9010 | The number 7 is positive. (Contributed by NM, 27-May-1999.) |
![]() ![]() ![]() ![]() | ||
Theorem | 8pos 9011 | The number 8 is positive. (Contributed by NM, 27-May-1999.) |
![]() ![]() ![]() ![]() | ||
Theorem | 9pos 9012 | The number 9 is positive. (Contributed by NM, 27-May-1999.) |
![]() ![]() ![]() ![]() | ||
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 9013 | -1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | neg1rr 9014 | -1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | neg1ne0 9015 | -1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | neg1lt0 9016 | -1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | neg1ap0 9017 | -1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.) |
![]() ![]() ![]() ![]() | ||
Theorem | negneg1e1 9018 |
![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 1pneg1e0 9019 |
![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 0m0e0 9020 | 0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 1m0e1 9021 | 1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 0p1e1 9022 | 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fv0p1e1 9023 |
Function value at ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 1p0e1 9024 | 1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 1p1e2 9025 | 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 2m1e1 9026 | 2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 9053. (Contributed by David A. Wheeler, 4-Jan-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 1e2m1 9027 | 1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 3m1e2 9028 | 3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 4m1e3 9029 | 4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 5m1e4 9030 | 5 - 1 = 4. (Contributed by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 6m1e5 9031 | 6 - 1 = 5. (Contributed by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7m1e6 9032 | 7 - 1 = 6. (Contributed by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8m1e7 9033 | 8 - 1 = 7. (Contributed by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9m1e8 9034 | 9 - 1 = 8. (Contributed by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 2p2e4 9035 | Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: https://us.metamath.org/mpeuni/mmset.html#trivia. (Contributed by NM, 27-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 2times 9036 | 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 9037 | A number times 2. (Contributed by NM, 16-Oct-2007.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 2timesi 9038 | Two times a number. (Contributed by NM, 1-Aug-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | times2i 9039 | A number times 2. (Contributed by NM, 11-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 2div2e1 9040 | 2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 2p1e3 9041 | 2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 1p2e3 9042 | 1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 3p1e4 9043 | 3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 4p1e5 9044 | 4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 5p1e6 9045 | 5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 6p1e7 9046 | 6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7p1e8 9047 | 7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8p1e9 9048 | 8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 3p2e5 9049 | 3 + 2 = 5. (Contributed by NM, 11-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 3p3e6 9050 | 3 + 3 = 6. (Contributed by NM, 11-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 4p2e6 9051 | 4 + 2 = 6. (Contributed by NM, 11-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 4p3e7 9052 | 4 + 3 = 7. (Contributed by NM, 11-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 4p4e8 9053 | 4 + 4 = 8. (Contributed by NM, 11-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 5p2e7 9054 | 5 + 2 = 7. (Contributed by NM, 11-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 5p3e8 9055 | 5 + 3 = 8. (Contributed by NM, 11-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 5p4e9 9056 | 5 + 4 = 9. (Contributed by NM, 11-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 6p2e8 9057 | 6 + 2 = 8. (Contributed by NM, 11-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 6p3e9 9058 | 6 + 3 = 9. (Contributed by NM, 11-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7p2e9 9059 | 7 + 2 = 9. (Contributed by NM, 11-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 1t1e1 9060 | 1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 2t1e2 9061 | 2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 2t2e4 9062 | 2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 3t1e3 9063 | 3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 3t2e6 9064 | 3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 3t3e9 9065 | 3 times 3 equals 9. (Contributed by NM, 11-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 4t2e8 9066 | 4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 2t0e0 9067 | 2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 4d2e2 9068 | One half of four is two. (Contributed by NM, 3-Sep-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 2nn 9069 | 2 is a positive integer. (Contributed by NM, 20-Aug-2001.) |
![]() ![]() ![]() ![]() | ||
Theorem | 3nn 9070 | 3 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
![]() ![]() ![]() ![]() | ||
Theorem | 4nn 9071 | 4 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
![]() ![]() ![]() ![]() | ||
Theorem | 5nn 9072 | 5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 6nn 9073 | 6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 7nn 9074 | 7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 8nn 9075 | 8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 9nn 9076 | 9 is a positive integer. (Contributed by NM, 21-Oct-2012.) |
![]() ![]() ![]() ![]() | ||
Theorem | 1lt2 9077 | 1 is less than 2. (Contributed by NM, 24-Feb-2005.) |
![]() ![]() ![]() ![]() | ||
Theorem | 2lt3 9078 | 2 is less than 3. (Contributed by NM, 26-Sep-2010.) |
![]() ![]() ![]() ![]() | ||
Theorem | 1lt3 9079 | 1 is less than 3. (Contributed by NM, 26-Sep-2010.) |
![]() ![]() ![]() ![]() | ||
Theorem | 3lt4 9080 | 3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 2lt4 9081 | 2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 1lt4 9082 | 1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 4lt5 9083 | 4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 3lt5 9084 | 3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 2lt5 9085 | 2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 1lt5 9086 | 1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 5lt6 9087 | 5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 4lt6 9088 | 4 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 3lt6 9089 | 3 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 2lt6 9090 | 2 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 1lt6 9091 | 1 is less than 6. (Contributed by NM, 19-Oct-2012.) |
![]() ![]() ![]() ![]() | ||
Theorem | 6lt7 9092 | 6 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 5lt7 9093 | 5 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 4lt7 9094 | 4 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 3lt7 9095 | 3 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 2lt7 9096 | 2 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 1lt7 9097 | 1 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 7lt8 9098 | 7 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 6lt8 9099 | 6 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() | ||
Theorem | 5lt8 9100 | 5 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
![]() ![]() ![]() ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |