P. 81 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8001-8100   *Has distinct variable group(s)

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