P. 90 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8901-9000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	0le0 8901	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ≤ 0
Theorem	0le2 8902	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ 0 ≤ 2
Theorem	2pos 8903	The number 2 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 2
Theorem	2ne0 8904	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
⊢ 2 ≠ 0
Theorem	2ap0 8905	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 2 # 0
Theorem	3pos 8906	The number 3 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 3
Theorem	3ne0 8907	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 3 ≠ 0
Theorem	3ap0 8908	The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
⊢ 3 # 0
Theorem	4pos 8909	The number 4 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 4
Theorem	4ne0 8910	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ 4 ≠ 0
Theorem	4ap0 8911	The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
⊢ 4 # 0
Theorem	5pos 8912	The number 5 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 5
Theorem	6pos 8913	The number 6 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 6
Theorem	7pos 8914	The number 7 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 7
Theorem	8pos 8915	The number 8 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 8
Theorem	9pos 8916	The number 9 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 9
4.4.4  Some properties of specific numbers 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 8917	-1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ -1 ∈ ℂ
Theorem	neg1rr 8918	-1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ -1 ∈ ℝ
Theorem	neg1ne0 8919	-1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 ≠ 0
Theorem	neg1lt0 8920	-1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 < 0
Theorem	neg1ap0 8921	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
⊢ -1 # 0
Theorem	negneg1e1 8922	--1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ --1 = 1
Theorem	1pneg1e0 8923	1 + -1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + -1) = 0
Theorem	0m0e0 8924	0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (0 − 0) = 0
Theorem	1m0e1 8925	1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 − 0) = 1
Theorem	0p1e1 8926	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (0 + 1) = 1
Theorem	fv0p1e1 8927	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 8928	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 0) = 1
Theorem	1p1e2 8929	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
⊢ (1 + 1) = 2
Theorem	2m1e1 8930	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 8957. (Contributed by David A. Wheeler, 4-Jan-2017.)
⊢ (2 − 1) = 1
Theorem	1e2m1 8931	1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 1 = (2 − 1)
Theorem	3m1e2 8932	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.)
⊢ (3 − 1) = 2
Theorem	4m1e3 8933	4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.)
⊢ (4 − 1) = 3
Theorem	5m1e4 8934	5 - 1 = 4. (Contributed by AV, 6-Sep-2021.)
⊢ (5 − 1) = 4
Theorem	6m1e5 8935	6 - 1 = 5. (Contributed by AV, 6-Sep-2021.)
⊢ (6 − 1) = 5
Theorem	7m1e6 8936	7 - 1 = 6. (Contributed by AV, 6-Sep-2021.)
⊢ (7 − 1) = 6
Theorem	8m1e7 8937	8 - 1 = 7. (Contributed by AV, 6-Sep-2021.)
⊢ (8 − 1) = 7
Theorem	9m1e8 8938	9 - 1 = 8. (Contributed by AV, 6-Sep-2021.)
⊢ (9 − 1) = 8
Theorem	2p2e4 8939	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 8940	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 8941	A number times 2. (Contributed by NM, 16-Oct-2007.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 2) = (𝐴 + 𝐴))
Theorem	2timesi 8942	Two times a number. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (2 · 𝐴) = (𝐴 + 𝐴)
Theorem	times2i 8943	A number times 2. (Contributed by NM, 11-May-2004.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · 2) = (𝐴 + 𝐴)
Theorem	2div2e1 8944	2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (2 / 2) = 1
Theorem	2p1e3 8945	2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (2 + 1) = 3
Theorem	1p2e3 8946	1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 2) = 3
Theorem	3p1e4 8947	3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (3 + 1) = 4
Theorem	4p1e5 8948	4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (4 + 1) = 5
Theorem	5p1e6 8949	5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (5 + 1) = 6
Theorem	6p1e7 8950	6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (6 + 1) = 7
Theorem	7p1e8 8951	7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (7 + 1) = 8
Theorem	8p1e9 8952	8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (8 + 1) = 9
Theorem	3p2e5 8953	3 + 2 = 5. (Contributed by NM, 11-May-2004.)
⊢ (3 + 2) = 5
Theorem	3p3e6 8954	3 + 3 = 6. (Contributed by NM, 11-May-2004.)
⊢ (3 + 3) = 6
Theorem	4p2e6 8955	4 + 2 = 6. (Contributed by NM, 11-May-2004.)
⊢ (4 + 2) = 6
Theorem	4p3e7 8956	4 + 3 = 7. (Contributed by NM, 11-May-2004.)
⊢ (4 + 3) = 7
Theorem	4p4e8 8957	4 + 4 = 8. (Contributed by NM, 11-May-2004.)
⊢ (4 + 4) = 8
Theorem	5p2e7 8958	5 + 2 = 7. (Contributed by NM, 11-May-2004.)
⊢ (5 + 2) = 7
Theorem	5p3e8 8959	5 + 3 = 8. (Contributed by NM, 11-May-2004.)
⊢ (5 + 3) = 8
Theorem	5p4e9 8960	5 + 4 = 9. (Contributed by NM, 11-May-2004.)
⊢ (5 + 4) = 9
Theorem	6p2e8 8961	6 + 2 = 8. (Contributed by NM, 11-May-2004.)
⊢ (6 + 2) = 8
Theorem	6p3e9 8962	6 + 3 = 9. (Contributed by NM, 11-May-2004.)
⊢ (6 + 3) = 9
Theorem	7p2e9 8963	7 + 2 = 9. (Contributed by NM, 11-May-2004.)
⊢ (7 + 2) = 9
Theorem	1t1e1 8964	1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (1 · 1) = 1
Theorem	2t1e2 8965	2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (2 · 1) = 2
Theorem	2t2e4 8966	2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.)
⊢ (2 · 2) = 4
Theorem	3t1e3 8967	3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (3 · 1) = 3
Theorem	3t2e6 8968	3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.)
⊢ (3 · 2) = 6
Theorem	3t3e9 8969	3 times 3 equals 9. (Contributed by NM, 11-May-2004.)
⊢ (3 · 3) = 9
Theorem	4t2e8 8970	4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.)
⊢ (4 · 2) = 8
Theorem	2t0e0 8971	2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (2 · 0) = 0
Theorem	4d2e2 8972	One half of four is two. (Contributed by NM, 3-Sep-1999.)
⊢ (4 / 2) = 2
Theorem	2nn 8973	2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
⊢ 2 ∈ ℕ
Theorem	3nn 8974	3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 3 ∈ ℕ
Theorem	4nn 8975	4 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 4 ∈ ℕ
Theorem	5nn 8976	5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 5 ∈ ℕ
Theorem	6nn 8977	6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 6 ∈ ℕ
Theorem	7nn 8978	7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 7 ∈ ℕ
Theorem	8nn 8979	8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 8 ∈ ℕ
Theorem	9nn 8980	9 is a positive integer. (Contributed by NM, 21-Oct-2012.)
⊢ 9 ∈ ℕ
Theorem	1lt2 8981	1 is less than 2. (Contributed by NM, 24-Feb-2005.)
⊢ 1 < 2
Theorem	2lt3 8982	2 is less than 3. (Contributed by NM, 26-Sep-2010.)
⊢ 2 < 3
Theorem	1lt3 8983	1 is less than 3. (Contributed by NM, 26-Sep-2010.)
⊢ 1 < 3
Theorem	3lt4 8984	3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 3 < 4
Theorem	2lt4 8985	2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 2 < 4
Theorem	1lt4 8986	1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 1 < 4
Theorem	4lt5 8987	4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 4 < 5
Theorem	3lt5 8988	3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 3 < 5
Theorem	2lt5 8989	2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 2 < 5
Theorem	1lt5 8990	1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 1 < 5
Theorem	5lt6 8991	5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 5 < 6
Theorem	4lt6 8992	4 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 4 < 6
Theorem	3lt6 8993	3 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 3 < 6
Theorem	2lt6 8994	2 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 2 < 6
Theorem	1lt6 8995	1 is less than 6. (Contributed by NM, 19-Oct-2012.)
⊢ 1 < 6
Theorem	6lt7 8996	6 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 6 < 7
Theorem	5lt7 8997	5 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 5 < 7
Theorem	4lt7 8998	4 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 4 < 7
Theorem	3lt7 8999	3 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 3 < 7
Theorem	2lt7 9000	2 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 2 < 7