Home | Intuitionistic Logic Explorer Theorem List (p. 89 of 133) | < 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 | 9cn 8801 | The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 0le0 8802 | Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | 0le2 8803 | 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.) |
Theorem | 2pos 8804 | The number 2 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 2ne0 8805 | The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.) |
Theorem | 2ap0 8806 | The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# | ||
Theorem | 3pos 8807 | The number 3 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 3ne0 8808 | The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Theorem | 3ap0 8809 | The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
# | ||
Theorem | 4pos 8810 | The number 4 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 4ne0 8811 | The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.) |
Theorem | 4ap0 8812 | The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
# | ||
Theorem | 5pos 8813 | The number 5 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 6pos 8814 | The number 6 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 7pos 8815 | The number 7 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 8pos 8816 | The number 8 is positive. (Contributed by NM, 27-May-1999.) |
Theorem | 9pos 8817 | 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 8818 | -1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | neg1rr 8819 | -1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.) |
Theorem | neg1ne0 8820 | -1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | neg1lt0 8821 | -1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | neg1ap0 8822 | -1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.) |
# | ||
Theorem | negneg1e1 8823 | is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 1pneg1e0 8824 | is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 0m0e0 8825 | 0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 1m0e1 8826 | 1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 0p1e1 8827 | 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | fv0p1e1 8828 | Function value at with replaced by . Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.) |
Theorem | 1p0e1 8829 | 1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 1p1e2 8830 | 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.) |
Theorem | 2m1e1 8831 | 2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 8858. (Contributed by David A. Wheeler, 4-Jan-2017.) |
Theorem | 1e2m1 8832 | 1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 3m1e2 8833 | 3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.) |
Theorem | 4m1e3 8834 | 4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.) |
Theorem | 5m1e4 8835 | 5 - 1 = 4. (Contributed by AV, 6-Sep-2021.) |
Theorem | 6m1e5 8836 | 6 - 1 = 5. (Contributed by AV, 6-Sep-2021.) |
Theorem | 7m1e6 8837 | 7 - 1 = 6. (Contributed by AV, 6-Sep-2021.) |
Theorem | 8m1e7 8838 | 8 - 1 = 7. (Contributed by AV, 6-Sep-2021.) |
Theorem | 9m1e8 8839 | 9 - 1 = 8. (Contributed by AV, 6-Sep-2021.) |
Theorem | 2p2e4 8840 | 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 8841 | 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 8842 | A number times 2. (Contributed by NM, 16-Oct-2007.) |
Theorem | 2timesi 8843 | Two times a number. (Contributed by NM, 1-Aug-1999.) |
Theorem | times2i 8844 | A number times 2. (Contributed by NM, 11-May-2004.) |
Theorem | 2div2e1 8845 | 2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 2p1e3 8846 | 2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 1p2e3 8847 | 1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 3p1e4 8848 | 3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 4p1e5 8849 | 4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 5p1e6 8850 | 5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 6p1e7 8851 | 6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 7p1e8 8852 | 7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 8p1e9 8853 | 8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Theorem | 3p2e5 8854 | 3 + 2 = 5. (Contributed by NM, 11-May-2004.) |
Theorem | 3p3e6 8855 | 3 + 3 = 6. (Contributed by NM, 11-May-2004.) |
Theorem | 4p2e6 8856 | 4 + 2 = 6. (Contributed by NM, 11-May-2004.) |
Theorem | 4p3e7 8857 | 4 + 3 = 7. (Contributed by NM, 11-May-2004.) |
Theorem | 4p4e8 8858 | 4 + 4 = 8. (Contributed by NM, 11-May-2004.) |
Theorem | 5p2e7 8859 | 5 + 2 = 7. (Contributed by NM, 11-May-2004.) |
Theorem | 5p3e8 8860 | 5 + 3 = 8. (Contributed by NM, 11-May-2004.) |
Theorem | 5p4e9 8861 | 5 + 4 = 9. (Contributed by NM, 11-May-2004.) |
Theorem | 6p2e8 8862 | 6 + 2 = 8. (Contributed by NM, 11-May-2004.) |
Theorem | 6p3e9 8863 | 6 + 3 = 9. (Contributed by NM, 11-May-2004.) |
Theorem | 7p2e9 8864 | 7 + 2 = 9. (Contributed by NM, 11-May-2004.) |
Theorem | 1t1e1 8865 | 1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | 2t1e2 8866 | 2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | 2t2e4 8867 | 2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.) |
Theorem | 3t1e3 8868 | 3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 3t2e6 8869 | 3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.) |
Theorem | 3t3e9 8870 | 3 times 3 equals 9. (Contributed by NM, 11-May-2004.) |
Theorem | 4t2e8 8871 | 4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.) |
Theorem | 2t0e0 8872 | 2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 4d2e2 8873 | One half of four is two. (Contributed by NM, 3-Sep-1999.) |
Theorem | 2nn 8874 | 2 is a positive integer. (Contributed by NM, 20-Aug-2001.) |
Theorem | 3nn 8875 | 3 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
Theorem | 4nn 8876 | 4 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
Theorem | 5nn 8877 | 5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 6nn 8878 | 6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 7nn 8879 | 7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 8nn 8880 | 8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 9nn 8881 | 9 is a positive integer. (Contributed by NM, 21-Oct-2012.) |
Theorem | 1lt2 8882 | 1 is less than 2. (Contributed by NM, 24-Feb-2005.) |
Theorem | 2lt3 8883 | 2 is less than 3. (Contributed by NM, 26-Sep-2010.) |
Theorem | 1lt3 8884 | 1 is less than 3. (Contributed by NM, 26-Sep-2010.) |
Theorem | 3lt4 8885 | 3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 2lt4 8886 | 2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 1lt4 8887 | 1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 4lt5 8888 | 4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 3lt5 8889 | 3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 2lt5 8890 | 2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 1lt5 8891 | 1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 5lt6 8892 | 5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 4lt6 8893 | 4 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 3lt6 8894 | 3 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 2lt6 8895 | 2 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 1lt6 8896 | 1 is less than 6. (Contributed by NM, 19-Oct-2012.) |
Theorem | 6lt7 8897 | 6 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 5lt7 8898 | 5 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 4lt7 8899 | 4 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Theorem | 3lt7 8900 | 3 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |