Theorem List for Intuitionistic Logic Explorer - 8801-8900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 1m0e1 8801 |
1 - 0 = 1 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ (1 − 0) = 1 |
|
Theorem | 0p1e1 8802 |
0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
|
⊢ (0 + 1) = 1 |
|
Theorem | fv0p1e1 8803 |
Function value at 𝑁 + 1 with 𝑁 replaced by 0. Technical
theorem to be used to reduce the size of a significant number of proofs.
(Contributed by AV, 13-Aug-2022.)
|
⊢ (𝑁 = 0 → (𝐹‘(𝑁 + 1)) = (𝐹‘1)) |
|
Theorem | 1p0e1 8804 |
1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ (1 + 0) = 1 |
|
Theorem | 1p1e2 8805 |
1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
|
⊢ (1 + 1) = 2 |
|
Theorem | 2m1e1 8806 |
2 - 1 = 1. The result is on the right-hand-side to be consistent with
similar proofs like 4p4e8 8833. (Contributed by David A. Wheeler,
4-Jan-2017.)
|
⊢ (2 − 1) = 1 |
|
Theorem | 1e2m1 8807 |
1 = 2 - 1 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ 1 = (2 − 1) |
|
Theorem | 3m1e2 8808 |
3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM,
10-Dec-2017.)
|
⊢ (3 − 1) = 2 |
|
Theorem | 4m1e3 8809 |
4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV,
6-Sep-2021.)
|
⊢ (4 − 1) = 3 |
|
Theorem | 5m1e4 8810 |
5 - 1 = 4. (Contributed by AV, 6-Sep-2021.)
|
⊢ (5 − 1) = 4 |
|
Theorem | 6m1e5 8811 |
6 - 1 = 5. (Contributed by AV, 6-Sep-2021.)
|
⊢ (6 − 1) = 5 |
|
Theorem | 7m1e6 8812 |
7 - 1 = 6. (Contributed by AV, 6-Sep-2021.)
|
⊢ (7 − 1) = 6 |
|
Theorem | 8m1e7 8813 |
8 - 1 = 7. (Contributed by AV, 6-Sep-2021.)
|
⊢ (8 − 1) = 7 |
|
Theorem | 9m1e8 8814 |
9 - 1 = 8. (Contributed by AV, 6-Sep-2021.)
|
⊢ (9 − 1) = 8 |
|
Theorem | 2p2e4 8815 |
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.)
|
⊢ (2 + 2) = 4 |
|
Theorem | 2times 8816 |
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 8817 |
A number times 2. (Contributed by NM, 16-Oct-2007.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 · 2) = (𝐴 + 𝐴)) |
|
Theorem | 2timesi 8818 |
Two times a number. (Contributed by NM, 1-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (2 · 𝐴) = (𝐴 + 𝐴) |
|
Theorem | times2i 8819 |
A number times 2. (Contributed by NM, 11-May-2004.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 · 2) = (𝐴 + 𝐴) |
|
Theorem | 2div2e1 8820 |
2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ (2 / 2) = 1 |
|
Theorem | 2p1e3 8821 |
2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
|
⊢ (2 + 1) = 3 |
|
Theorem | 1p2e3 8822 |
1 + 2 = 3 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ (1 + 2) = 3 |
|
Theorem | 3p1e4 8823 |
3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
|
⊢ (3 + 1) = 4 |
|
Theorem | 4p1e5 8824 |
4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
|
⊢ (4 + 1) = 5 |
|
Theorem | 5p1e6 8825 |
5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
|
⊢ (5 + 1) = 6 |
|
Theorem | 6p1e7 8826 |
6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
|
⊢ (6 + 1) = 7 |
|
Theorem | 7p1e8 8827 |
7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
|
⊢ (7 + 1) = 8 |
|
Theorem | 8p1e9 8828 |
8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
|
⊢ (8 + 1) = 9 |
|
Theorem | 3p2e5 8829 |
3 + 2 = 5. (Contributed by NM, 11-May-2004.)
|
⊢ (3 + 2) = 5 |
|
Theorem | 3p3e6 8830 |
3 + 3 = 6. (Contributed by NM, 11-May-2004.)
|
⊢ (3 + 3) = 6 |
|
Theorem | 4p2e6 8831 |
4 + 2 = 6. (Contributed by NM, 11-May-2004.)
|
⊢ (4 + 2) = 6 |
|
Theorem | 4p3e7 8832 |
4 + 3 = 7. (Contributed by NM, 11-May-2004.)
|
⊢ (4 + 3) = 7 |
|
Theorem | 4p4e8 8833 |
4 + 4 = 8. (Contributed by NM, 11-May-2004.)
|
⊢ (4 + 4) = 8 |
|
Theorem | 5p2e7 8834 |
5 + 2 = 7. (Contributed by NM, 11-May-2004.)
|
⊢ (5 + 2) = 7 |
|
Theorem | 5p3e8 8835 |
5 + 3 = 8. (Contributed by NM, 11-May-2004.)
|
⊢ (5 + 3) = 8 |
|
Theorem | 5p4e9 8836 |
5 + 4 = 9. (Contributed by NM, 11-May-2004.)
|
⊢ (5 + 4) = 9 |
|
Theorem | 6p2e8 8837 |
6 + 2 = 8. (Contributed by NM, 11-May-2004.)
|
⊢ (6 + 2) = 8 |
|
Theorem | 6p3e9 8838 |
6 + 3 = 9. (Contributed by NM, 11-May-2004.)
|
⊢ (6 + 3) = 9 |
|
Theorem | 7p2e9 8839 |
7 + 2 = 9. (Contributed by NM, 11-May-2004.)
|
⊢ (7 + 2) = 9 |
|
Theorem | 1t1e1 8840 |
1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
|
⊢ (1 · 1) = 1 |
|
Theorem | 2t1e2 8841 |
2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.)
|
⊢ (2 · 1) = 2 |
|
Theorem | 2t2e4 8842 |
2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.)
|
⊢ (2 · 2) = 4 |
|
Theorem | 3t1e3 8843 |
3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ (3 · 1) = 3 |
|
Theorem | 3t2e6 8844 |
3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.)
|
⊢ (3 · 2) = 6 |
|
Theorem | 3t3e9 8845 |
3 times 3 equals 9. (Contributed by NM, 11-May-2004.)
|
⊢ (3 · 3) = 9 |
|
Theorem | 4t2e8 8846 |
4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.)
|
⊢ (4 · 2) = 8 |
|
Theorem | 2t0e0 8847 |
2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ (2 · 0) = 0 |
|
Theorem | 4d2e2 8848 |
One half of four is two. (Contributed by NM, 3-Sep-1999.)
|
⊢ (4 / 2) = 2 |
|
Theorem | 2nn 8849 |
2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
|
⊢ 2 ∈ ℕ |
|
Theorem | 3nn 8850 |
3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
|
⊢ 3 ∈ ℕ |
|
Theorem | 4nn 8851 |
4 is a positive integer. (Contributed by NM, 8-Jan-2006.)
|
⊢ 4 ∈ ℕ |
|
Theorem | 5nn 8852 |
5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 5 ∈ ℕ |
|
Theorem | 6nn 8853 |
6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 6 ∈ ℕ |
|
Theorem | 7nn 8854 |
7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 7 ∈ ℕ |
|
Theorem | 8nn 8855 |
8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 8 ∈ ℕ |
|
Theorem | 9nn 8856 |
9 is a positive integer. (Contributed by NM, 21-Oct-2012.)
|
⊢ 9 ∈ ℕ |
|
Theorem | 1lt2 8857 |
1 is less than 2. (Contributed by NM, 24-Feb-2005.)
|
⊢ 1 < 2 |
|
Theorem | 2lt3 8858 |
2 is less than 3. (Contributed by NM, 26-Sep-2010.)
|
⊢ 2 < 3 |
|
Theorem | 1lt3 8859 |
1 is less than 3. (Contributed by NM, 26-Sep-2010.)
|
⊢ 1 < 3 |
|
Theorem | 3lt4 8860 |
3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 4 |
|
Theorem | 2lt4 8861 |
2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 4 |
|
Theorem | 1lt4 8862 |
1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 1 < 4 |
|
Theorem | 4lt5 8863 |
4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 4 < 5 |
|
Theorem | 3lt5 8864 |
3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 5 |
|
Theorem | 2lt5 8865 |
2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 5 |
|
Theorem | 1lt5 8866 |
1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 1 < 5 |
|
Theorem | 5lt6 8867 |
5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 5 < 6 |
|
Theorem | 4lt6 8868 |
4 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 4 < 6 |
|
Theorem | 3lt6 8869 |
3 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 6 |
|
Theorem | 2lt6 8870 |
2 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 6 |
|
Theorem | 1lt6 8871 |
1 is less than 6. (Contributed by NM, 19-Oct-2012.)
|
⊢ 1 < 6 |
|
Theorem | 6lt7 8872 |
6 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 6 < 7 |
|
Theorem | 5lt7 8873 |
5 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 5 < 7 |
|
Theorem | 4lt7 8874 |
4 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 4 < 7 |
|
Theorem | 3lt7 8875 |
3 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 7 |
|
Theorem | 2lt7 8876 |
2 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 7 |
|
Theorem | 1lt7 8877 |
1 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 1 < 7 |
|
Theorem | 7lt8 8878 |
7 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 7 < 8 |
|
Theorem | 6lt8 8879 |
6 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 6 < 8 |
|
Theorem | 5lt8 8880 |
5 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 5 < 8 |
|
Theorem | 4lt8 8881 |
4 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 4 < 8 |
|
Theorem | 3lt8 8882 |
3 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 8 |
|
Theorem | 2lt8 8883 |
2 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 8 |
|
Theorem | 1lt8 8884 |
1 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 1 < 8 |
|
Theorem | 8lt9 8885 |
8 is less than 9. (Contributed by Mario Carneiro, 19-Feb-2014.)
|
⊢ 8 < 9 |
|
Theorem | 7lt9 8886 |
7 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 7 < 9 |
|
Theorem | 6lt9 8887 |
6 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 6 < 9 |
|
Theorem | 5lt9 8888 |
5 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 5 < 9 |
|
Theorem | 4lt9 8889 |
4 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 4 < 9 |
|
Theorem | 3lt9 8890 |
3 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 3 < 9 |
|
Theorem | 2lt9 8891 |
2 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 2 < 9 |
|
Theorem | 1lt9 8892 |
1 is less than 9. (Contributed by NM, 19-Oct-2012.) (Revised by Mario
Carneiro, 9-Mar-2015.)
|
⊢ 1 < 9 |
|
Theorem | 0ne2 8893 |
0 is not equal to 2. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ 0 ≠ 2 |
|
Theorem | 1ne2 8894 |
1 is not equal to 2. (Contributed by NM, 19-Oct-2012.)
|
⊢ 1 ≠ 2 |
|
Theorem | 1ap2 8895 |
1 is apart from 2. (Contributed by Jim Kingdon, 29-Oct-2022.)
|
⊢ 1 # 2 |
|
Theorem | 1le2 8896 |
1 is less than or equal to 2 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ 1 ≤ 2 |
|
Theorem | 2cnne0 8897 |
2 is a nonzero complex number (common case). (Contributed by David A.
Wheeler, 7-Dec-2018.)
|
⊢ (2 ∈ ℂ ∧ 2 ≠
0) |
|
Theorem | 2rene0 8898 |
2 is a nonzero real number (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ (2 ∈ ℝ ∧ 2 ≠
0) |
|
Theorem | 1le3 8899 |
1 is less than or equal to 3. (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ 1 ≤ 3 |
|
Theorem | neg1mulneg1e1 8900 |
-1 · -1 is 1 (common case). (Contributed by
David A. Wheeler,
8-Dec-2018.)
|
⊢ (-1 · -1) = 1 |