Theorem List for Intuitionistic Logic Explorer - 9001-9100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 6m1e5 9001 |
6 - 1 = 5. (Contributed by AV, 6-Sep-2021.)
|
⊢ (6 − 1) = 5 |
|
Theorem | 7m1e6 9002 |
7 - 1 = 6. (Contributed by AV, 6-Sep-2021.)
|
⊢ (7 − 1) = 6 |
|
Theorem | 8m1e7 9003 |
8 - 1 = 7. (Contributed by AV, 6-Sep-2021.)
|
⊢ (8 − 1) = 7 |
|
Theorem | 9m1e8 9004 |
9 - 1 = 8. (Contributed by AV, 6-Sep-2021.)
|
⊢ (9 − 1) = 8 |
|
Theorem | 2p2e4 9005 |
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 9006 |
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 9007 |
A number times 2. (Contributed by NM, 16-Oct-2007.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 · 2) = (𝐴 + 𝐴)) |
|
Theorem | 2timesi 9008 |
Two times a number. (Contributed by NM, 1-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (2 · 𝐴) = (𝐴 + 𝐴) |
|
Theorem | times2i 9009 |
A number times 2. (Contributed by NM, 11-May-2004.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 · 2) = (𝐴 + 𝐴) |
|
Theorem | 2div2e1 9010 |
2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ (2 / 2) = 1 |
|
Theorem | 2p1e3 9011 |
2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
|
⊢ (2 + 1) = 3 |
|
Theorem | 1p2e3 9012 |
1 + 2 = 3 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ (1 + 2) = 3 |
|
Theorem | 3p1e4 9013 |
3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
|
⊢ (3 + 1) = 4 |
|
Theorem | 4p1e5 9014 |
4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
|
⊢ (4 + 1) = 5 |
|
Theorem | 5p1e6 9015 |
5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
|
⊢ (5 + 1) = 6 |
|
Theorem | 6p1e7 9016 |
6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
|
⊢ (6 + 1) = 7 |
|
Theorem | 7p1e8 9017 |
7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
|
⊢ (7 + 1) = 8 |
|
Theorem | 8p1e9 9018 |
8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
|
⊢ (8 + 1) = 9 |
|
Theorem | 3p2e5 9019 |
3 + 2 = 5. (Contributed by NM, 11-May-2004.)
|
⊢ (3 + 2) = 5 |
|
Theorem | 3p3e6 9020 |
3 + 3 = 6. (Contributed by NM, 11-May-2004.)
|
⊢ (3 + 3) = 6 |
|
Theorem | 4p2e6 9021 |
4 + 2 = 6. (Contributed by NM, 11-May-2004.)
|
⊢ (4 + 2) = 6 |
|
Theorem | 4p3e7 9022 |
4 + 3 = 7. (Contributed by NM, 11-May-2004.)
|
⊢ (4 + 3) = 7 |
|
Theorem | 4p4e8 9023 |
4 + 4 = 8. (Contributed by NM, 11-May-2004.)
|
⊢ (4 + 4) = 8 |
|
Theorem | 5p2e7 9024 |
5 + 2 = 7. (Contributed by NM, 11-May-2004.)
|
⊢ (5 + 2) = 7 |
|
Theorem | 5p3e8 9025 |
5 + 3 = 8. (Contributed by NM, 11-May-2004.)
|
⊢ (5 + 3) = 8 |
|
Theorem | 5p4e9 9026 |
5 + 4 = 9. (Contributed by NM, 11-May-2004.)
|
⊢ (5 + 4) = 9 |
|
Theorem | 6p2e8 9027 |
6 + 2 = 8. (Contributed by NM, 11-May-2004.)
|
⊢ (6 + 2) = 8 |
|
Theorem | 6p3e9 9028 |
6 + 3 = 9. (Contributed by NM, 11-May-2004.)
|
⊢ (6 + 3) = 9 |
|
Theorem | 7p2e9 9029 |
7 + 2 = 9. (Contributed by NM, 11-May-2004.)
|
⊢ (7 + 2) = 9 |
|
Theorem | 1t1e1 9030 |
1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
|
⊢ (1 · 1) = 1 |
|
Theorem | 2t1e2 9031 |
2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.)
|
⊢ (2 · 1) = 2 |
|
Theorem | 2t2e4 9032 |
2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.)
|
⊢ (2 · 2) = 4 |
|
Theorem | 3t1e3 9033 |
3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ (3 · 1) = 3 |
|
Theorem | 3t2e6 9034 |
3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.)
|
⊢ (3 · 2) = 6 |
|
Theorem | 3t3e9 9035 |
3 times 3 equals 9. (Contributed by NM, 11-May-2004.)
|
⊢ (3 · 3) = 9 |
|
Theorem | 4t2e8 9036 |
4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.)
|
⊢ (4 · 2) = 8 |
|
Theorem | 2t0e0 9037 |
2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ (2 · 0) = 0 |
|
Theorem | 4d2e2 9038 |
One half of four is two. (Contributed by NM, 3-Sep-1999.)
|
⊢ (4 / 2) = 2 |
|
Theorem | 2nn 9039 |
2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
|
⊢ 2 ∈ ℕ |
|
Theorem | 3nn 9040 |
3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
|
⊢ 3 ∈ ℕ |
|
Theorem | 4nn 9041 |
4 is a positive integer. (Contributed by NM, 8-Jan-2006.)
|
⊢ 4 ∈ ℕ |
|
Theorem | 5nn 9042 |
5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 5 ∈ ℕ |
|
Theorem | 6nn 9043 |
6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 6 ∈ ℕ |
|
Theorem | 7nn 9044 |
7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 7 ∈ ℕ |
|
Theorem | 8nn 9045 |
8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 8 ∈ ℕ |
|
Theorem | 9nn 9046 |
9 is a positive integer. (Contributed by NM, 21-Oct-2012.)
|
⊢ 9 ∈ ℕ |
|
Theorem | 1lt2 9047 |
1 is less than 2. (Contributed by NM, 24-Feb-2005.)
|
⊢ 1 < 2 |
|
Theorem | 2lt3 9048 |
2 is less than 3. (Contributed by NM, 26-Sep-2010.)
|
⊢ 2 < 3 |
|
Theorem | 1lt3 9049 |
1 is less than 3. (Contributed by NM, 26-Sep-2010.)
|
⊢ 1 < 3 |
|
Theorem | 3lt4 9050 |
3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 4 |
|
Theorem | 2lt4 9051 |
2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 4 |
|
Theorem | 1lt4 9052 |
1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 1 < 4 |
|
Theorem | 4lt5 9053 |
4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 4 < 5 |
|
Theorem | 3lt5 9054 |
3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 5 |
|
Theorem | 2lt5 9055 |
2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 5 |
|
Theorem | 1lt5 9056 |
1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 1 < 5 |
|
Theorem | 5lt6 9057 |
5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 5 < 6 |
|
Theorem | 4lt6 9058 |
4 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 4 < 6 |
|
Theorem | 3lt6 9059 |
3 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 6 |
|
Theorem | 2lt6 9060 |
2 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 6 |
|
Theorem | 1lt6 9061 |
1 is less than 6. (Contributed by NM, 19-Oct-2012.)
|
⊢ 1 < 6 |
|
Theorem | 6lt7 9062 |
6 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 6 < 7 |
|
Theorem | 5lt7 9063 |
5 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 5 < 7 |
|
Theorem | 4lt7 9064 |
4 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 4 < 7 |
|
Theorem | 3lt7 9065 |
3 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 7 |
|
Theorem | 2lt7 9066 |
2 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 7 |
|
Theorem | 1lt7 9067 |
1 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 1 < 7 |
|
Theorem | 7lt8 9068 |
7 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 7 < 8 |
|
Theorem | 6lt8 9069 |
6 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 6 < 8 |
|
Theorem | 5lt8 9070 |
5 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 5 < 8 |
|
Theorem | 4lt8 9071 |
4 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 4 < 8 |
|
Theorem | 3lt8 9072 |
3 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 8 |
|
Theorem | 2lt8 9073 |
2 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 8 |
|
Theorem | 1lt8 9074 |
1 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 1 < 8 |
|
Theorem | 8lt9 9075 |
8 is less than 9. (Contributed by Mario Carneiro, 19-Feb-2014.)
|
⊢ 8 < 9 |
|
Theorem | 7lt9 9076 |
7 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 7 < 9 |
|
Theorem | 6lt9 9077 |
6 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 6 < 9 |
|
Theorem | 5lt9 9078 |
5 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 5 < 9 |
|
Theorem | 4lt9 9079 |
4 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 4 < 9 |
|
Theorem | 3lt9 9080 |
3 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 3 < 9 |
|
Theorem | 2lt9 9081 |
2 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 2 < 9 |
|
Theorem | 1lt9 9082 |
1 is less than 9. (Contributed by NM, 19-Oct-2012.) (Revised by Mario
Carneiro, 9-Mar-2015.)
|
⊢ 1 < 9 |
|
Theorem | 0ne2 9083 |
0 is not equal to 2. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ 0 ≠ 2 |
|
Theorem | 1ne2 9084 |
1 is not equal to 2. (Contributed by NM, 19-Oct-2012.)
|
⊢ 1 ≠ 2 |
|
Theorem | 1ap2 9085 |
1 is apart from 2. (Contributed by Jim Kingdon, 29-Oct-2022.)
|
⊢ 1 # 2 |
|
Theorem | 1le2 9086 |
1 is less than or equal to 2 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ 1 ≤ 2 |
|
Theorem | 2cnne0 9087 |
2 is a nonzero complex number (common case). (Contributed by David A.
Wheeler, 7-Dec-2018.)
|
⊢ (2 ∈ ℂ ∧ 2 ≠
0) |
|
Theorem | 2rene0 9088 |
2 is a nonzero real number (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ (2 ∈ ℝ ∧ 2 ≠
0) |
|
Theorem | 1le3 9089 |
1 is less than or equal to 3. (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ 1 ≤ 3 |
|
Theorem | neg1mulneg1e1 9090 |
-1 · -1 is 1 (common case). (Contributed by
David A. Wheeler,
8-Dec-2018.)
|
⊢ (-1 · -1) = 1 |
|
Theorem | halfre 9091 |
One-half is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ (1 / 2) ∈ ℝ |
|
Theorem | halfcn 9092 |
One-half is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ (1 / 2) ∈ ℂ |
|
Theorem | halfgt0 9093 |
One-half is greater than zero. (Contributed by NM, 24-Feb-2005.)
|
⊢ 0 < (1 / 2) |
|
Theorem | halfge0 9094 |
One-half is not negative. (Contributed by AV, 7-Jun-2020.)
|
⊢ 0 ≤ (1 / 2) |
|
Theorem | halflt1 9095 |
One-half is less than one. (Contributed by NM, 24-Feb-2005.)
|
⊢ (1 / 2) < 1 |
|
Theorem | 1mhlfehlf 9096 |
Prove that 1 - 1/2 = 1/2. (Contributed by David A. Wheeler,
4-Jan-2017.)
|
⊢ (1 − (1 / 2)) = (1 /
2) |
|
Theorem | 8th4div3 9097 |
An eighth of four thirds is a sixth. (Contributed by Paul Chapman,
24-Nov-2007.)
|
⊢ ((1 / 8) · (4 / 3)) = (1 /
6) |
|
Theorem | halfpm6th 9098 |
One half plus or minus one sixth. (Contributed by Paul Chapman,
17-Jan-2008.)
|
⊢ (((1 / 2) − (1 / 6)) = (1 / 3) ∧
((1 / 2) + (1 / 6)) = (2 / 3)) |
|
Theorem | it0e0 9099 |
i times 0 equals 0 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ (i · 0) = 0 |
|
Theorem | 2mulicn 9100 |
(2 · i) ∈ ℂ (common case).
(Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ (2 · i) ∈
ℂ |