Home | Intuitionistic Logic Explorer Theorem List (p. 81 of 102) | < 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 | 8cn 8001 | The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 9re 8002 | The number 9 is real. (Contributed by NM, 27-May-1999.) |
Theorem | 9cn 8003 | The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 10re 8004 | The number 10 is real. (Contributed by NM, 5-Feb-2007.) |
Theorem | 0le0 8005 | Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | 0le2 8006 | 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.) |
Theorem | 2pos 8007 | The number 2 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 2ne0 8008 | The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.) |
Theorem | 2ap0 8009 | The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# | ||
Theorem | 3pos 8010 | The number 3 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 3ne0 8011 | The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Theorem | 3ap0 8012 | The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
# | ||
Theorem | 4pos 8013 | The number 4 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 4ne0 8014 | The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.) |
Theorem | 4ap0 8015 | The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
# | ||
Theorem | 5pos 8016 | The number 5 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 6pos 8017 | The number 6 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 7pos 8018 | The number 7 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 8pos 8019 | The number 8 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 9pos 8020 | The number 9 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 10pos 8021 | The number 10 is positive. (Contributed by NM, 5-Feb-2007.) |
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 8022 | -1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | neg1rr 8023 | -1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.) |
Theorem | neg1ne0 8024 | -1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | neg1lt0 8025 | -1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | neg1ap0 8026 | -1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.) |
# | ||
Theorem | negneg1e1 8027 | is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 1pneg1e0 8028 | is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 0m0e0 8029 | 0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 1m0e1 8030 | 1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 0p1e1 8031 | 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | 1p0e1 8032 | 1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 1p1e2 8033 | 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.) |
Theorem | 2m1e1 8034 | 2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 8056. (Contributed by David A. Wheeler, 4-Jan-2017.) |
Theorem | 1e2m1 8035 | 1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 3m1e2 8036 | 3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.) |
Theorem | 2p2e4 8037 | Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: http://us.metamath.org/mpeuni/mmset.html#trivia. (Contributed by NM, 27-May-1999.) |
Theorem | 2times 8038 | 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 8039 | A number times 2. (Contributed by NM, 16-Oct-2007.) |
Theorem | 2timesi 8040 | Two times a number. (Contributed by NM, 1-Aug-1999.) |
Theorem | times2i 8041 | A number times 2. (Contributed by NM, 11-May-2004.) |
Theorem | 2div2e1 8042 | 2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 2p1e3 8043 | 2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 1p2e3 8044 | 1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 3p1e4 8045 | 3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 4p1e5 8046 | 4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 5p1e6 8047 | 5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 6p1e7 8048 | 6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 7p1e8 8049 | 7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 8p1e9 8050 | 8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 9p1e10 8051 | 9 + 1 = 10. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 3p2e5 8052 | 3 + 2 = 5. (Contributed by NM, 11-May-2004.) |
Theorem | 3p3e6 8053 | 3 + 3 = 6. (Contributed by NM, 11-May-2004.) |
Theorem | 4p2e6 8054 | 4 + 2 = 6. (Contributed by NM, 11-May-2004.) |
Theorem | 4p3e7 8055 | 4 + 3 = 7. (Contributed by NM, 11-May-2004.) |
Theorem | 4p4e8 8056 | 4 + 4 = 8. (Contributed by NM, 11-May-2004.) |
Theorem | 5p2e7 8057 | 5 + 2 = 7. (Contributed by NM, 11-May-2004.) |
Theorem | 5p3e8 8058 | 5 + 3 = 8. (Contributed by NM, 11-May-2004.) |
Theorem | 5p4e9 8059 | 5 + 4 = 9. (Contributed by NM, 11-May-2004.) |
Theorem | 5p5e10 8060 | 5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) |
Theorem | 6p2e8 8061 | 6 + 2 = 8. (Contributed by NM, 11-May-2004.) |
Theorem | 6p3e9 8062 | 6 + 3 = 9. (Contributed by NM, 11-May-2004.) |
Theorem | 6p4e10 8063 | 6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) |
Theorem | 7p2e9 8064 | 7 + 2 = 9. (Contributed by NM, 11-May-2004.) |
Theorem | 7p3e10 8065 | 7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) |
Theorem | 8p2e10 8066 | 8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) |
Theorem | 1t1e1 8067 | 1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | 2t1e2 8068 | 2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | 2t2e4 8069 | 2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.) |
Theorem | 3t1e3 8070 | 3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 3t2e6 8071 | 3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.) |
Theorem | 3t3e9 8072 | 3 times 3 equals 9. (Contributed by NM, 11-May-2004.) |
Theorem | 4t2e8 8073 | 4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.) |
Theorem | 5t2e10 8074 | 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) |
Theorem | 2t0e0 8075 | 2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 4d2e2 8076 | One half of four is two. (Contributed by NM, 3-Sep-1999.) |
Theorem | 2nn 8077 | 2 is a positive integer. (Contributed by NM, 20-Aug-2001.) |
Theorem | 3nn 8078 | 3 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
Theorem | 4nn 8079 | 4 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
Theorem | 5nn 8080 | 5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 6nn 8081 | 6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 7nn 8082 | 7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 8nn 8083 | 8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 9nn 8084 | 9 is a positive integer. (Contributed by NM, 21-Oct-2012.) |
Theorem | 10nn 8085 | 10 is a positive integer. (Contributed by NM, 8-Nov-2012.) |
Theorem | 1lt2 8086 | 1 is less than 2. (Contributed by NM, 24-Feb-2005.) |
Theorem | 2lt3 8087 | 2 is less than 3. (Contributed by NM, 26-Sep-2010.) |
Theorem | 1lt3 8088 | 1 is less than 3. (Contributed by NM, 26-Sep-2010.) |
Theorem | 3lt4 8089 | 3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 2lt4 8090 | 2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 1lt4 8091 | 1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 4lt5 8092 | 4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 3lt5 8093 | 3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 2lt5 8094 | 2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 1lt5 8095 | 1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 5lt6 8096 | 5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 4lt6 8097 | 4 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 3lt6 8098 | 3 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 2lt6 8099 | 2 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 1lt6 8100 | 1 is less than 6. (Contributed by NM, 19-Oct-2012.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |