P. 91 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9001-9100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	5re 9001	The number 5 is real. (Contributed by NM, 27-May-1999.)
⊢ 5 ∈ ℝ
Theorem	5cn 9002	The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 5 ∈ ℂ
Theorem	6re 9003	The number 6 is real. (Contributed by NM, 27-May-1999.)
⊢ 6 ∈ ℝ
Theorem	6cn 9004	The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 6 ∈ ℂ
Theorem	7re 9005	The number 7 is real. (Contributed by NM, 27-May-1999.)
⊢ 7 ∈ ℝ
Theorem	7cn 9006	The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 7 ∈ ℂ
Theorem	8re 9007	The number 8 is real. (Contributed by NM, 27-May-1999.)
⊢ 8 ∈ ℝ
Theorem	8cn 9008	The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 8 ∈ ℂ
Theorem	9re 9009	The number 9 is real. (Contributed by NM, 27-May-1999.)
⊢ 9 ∈ ℝ
Theorem	9cn 9010	The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 9 ∈ ℂ
Theorem	0le0 9011	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ≤ 0
Theorem	0le2 9012	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ 0 ≤ 2
Theorem	2pos 9013	The number 2 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 2
Theorem	2ne0 9014	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
⊢ 2 ≠ 0
Theorem	2ap0 9015	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 2 # 0
Theorem	3pos 9016	The number 3 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 3
Theorem	3ne0 9017	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 3 ≠ 0
Theorem	3ap0 9018	The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
⊢ 3 # 0
Theorem	4pos 9019	The number 4 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 4
Theorem	4ne0 9020	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ 4 ≠ 0
Theorem	4ap0 9021	The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
⊢ 4 # 0
Theorem	5pos 9022	The number 5 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 5
Theorem	6pos 9023	The number 6 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 6
Theorem	7pos 9024	The number 7 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 7
Theorem	8pos 9025	The number 8 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 8
Theorem	9pos 9026	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 9027	-1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ -1 ∈ ℂ
Theorem	neg1rr 9028	-1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ -1 ∈ ℝ
Theorem	neg1ne0 9029	-1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 ≠ 0
Theorem	neg1lt0 9030	-1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 < 0
Theorem	neg1ap0 9031	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
⊢ -1 # 0
Theorem	negneg1e1 9032	--1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ --1 = 1
Theorem	1pneg1e0 9033	1 + -1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + -1) = 0
Theorem	0m0e0 9034	0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (0 − 0) = 0
Theorem	1m0e1 9035	1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 − 0) = 1
Theorem	0p1e1 9036	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (0 + 1) = 1
Theorem	fv0p1e1 9037	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 9038	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 0) = 1
Theorem	1p1e2 9039	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
⊢ (1 + 1) = 2
Theorem	2m1e1 9040	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 9067. (Contributed by David A. Wheeler, 4-Jan-2017.)
⊢ (2 − 1) = 1
Theorem	1e2m1 9041	1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 1 = (2 − 1)
Theorem	3m1e2 9042	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.)
⊢ (3 − 1) = 2
Theorem	4m1e3 9043	4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.)
⊢ (4 − 1) = 3
Theorem	5m1e4 9044	5 - 1 = 4. (Contributed by AV, 6-Sep-2021.)
⊢ (5 − 1) = 4
Theorem	6m1e5 9045	6 - 1 = 5. (Contributed by AV, 6-Sep-2021.)
⊢ (6 − 1) = 5
Theorem	7m1e6 9046	7 - 1 = 6. (Contributed by AV, 6-Sep-2021.)
⊢ (7 − 1) = 6
Theorem	8m1e7 9047	8 - 1 = 7. (Contributed by AV, 6-Sep-2021.)
⊢ (8 − 1) = 7
Theorem	9m1e8 9048	9 - 1 = 8. (Contributed by AV, 6-Sep-2021.)
⊢ (9 − 1) = 8
Theorem	2p2e4 9049	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 9050	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 9051	A number times 2. (Contributed by NM, 16-Oct-2007.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 2) = (𝐴 + 𝐴))
Theorem	2timesi 9052	Two times a number. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (2 · 𝐴) = (𝐴 + 𝐴)
Theorem	times2i 9053	A number times 2. (Contributed by NM, 11-May-2004.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · 2) = (𝐴 + 𝐴)
Theorem	2div2e1 9054	2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (2 / 2) = 1
Theorem	2p1e3 9055	2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (2 + 1) = 3
Theorem	1p2e3 9056	1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 2) = 3
Theorem	3p1e4 9057	3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (3 + 1) = 4
Theorem	4p1e5 9058	4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (4 + 1) = 5
Theorem	5p1e6 9059	5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (5 + 1) = 6
Theorem	6p1e7 9060	6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (6 + 1) = 7
Theorem	7p1e8 9061	7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (7 + 1) = 8
Theorem	8p1e9 9062	8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (8 + 1) = 9
Theorem	3p2e5 9063	3 + 2 = 5. (Contributed by NM, 11-May-2004.)
⊢ (3 + 2) = 5
Theorem	3p3e6 9064	3 + 3 = 6. (Contributed by NM, 11-May-2004.)
⊢ (3 + 3) = 6
Theorem	4p2e6 9065	4 + 2 = 6. (Contributed by NM, 11-May-2004.)
⊢ (4 + 2) = 6
Theorem	4p3e7 9066	4 + 3 = 7. (Contributed by NM, 11-May-2004.)
⊢ (4 + 3) = 7
Theorem	4p4e8 9067	4 + 4 = 8. (Contributed by NM, 11-May-2004.)
⊢ (4 + 4) = 8
Theorem	5p2e7 9068	5 + 2 = 7. (Contributed by NM, 11-May-2004.)
⊢ (5 + 2) = 7
Theorem	5p3e8 9069	5 + 3 = 8. (Contributed by NM, 11-May-2004.)
⊢ (5 + 3) = 8
Theorem	5p4e9 9070	5 + 4 = 9. (Contributed by NM, 11-May-2004.)
⊢ (5 + 4) = 9
Theorem	6p2e8 9071	6 + 2 = 8. (Contributed by NM, 11-May-2004.)
⊢ (6 + 2) = 8
Theorem	6p3e9 9072	6 + 3 = 9. (Contributed by NM, 11-May-2004.)
⊢ (6 + 3) = 9
Theorem	7p2e9 9073	7 + 2 = 9. (Contributed by NM, 11-May-2004.)
⊢ (7 + 2) = 9
Theorem	1t1e1 9074	1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (1 · 1) = 1
Theorem	2t1e2 9075	2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (2 · 1) = 2
Theorem	2t2e4 9076	2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.)
⊢ (2 · 2) = 4
Theorem	3t1e3 9077	3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (3 · 1) = 3
Theorem	3t2e6 9078	3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.)
⊢ (3 · 2) = 6
Theorem	3t3e9 9079	3 times 3 equals 9. (Contributed by NM, 11-May-2004.)
⊢ (3 · 3) = 9
Theorem	4t2e8 9080	4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.)
⊢ (4 · 2) = 8
Theorem	2t0e0 9081	2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (2 · 0) = 0
Theorem	4d2e2 9082	One half of four is two. (Contributed by NM, 3-Sep-1999.)
⊢ (4 / 2) = 2
Theorem	2nn 9083	2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
⊢ 2 ∈ ℕ
Theorem	3nn 9084	3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 3 ∈ ℕ
Theorem	4nn 9085	4 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 4 ∈ ℕ
Theorem	5nn 9086	5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 5 ∈ ℕ
Theorem	6nn 9087	6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 6 ∈ ℕ
Theorem	7nn 9088	7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 7 ∈ ℕ
Theorem	8nn 9089	8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 8 ∈ ℕ
Theorem	9nn 9090	9 is a positive integer. (Contributed by NM, 21-Oct-2012.)
⊢ 9 ∈ ℕ
Theorem	1lt2 9091	1 is less than 2. (Contributed by NM, 24-Feb-2005.)
⊢ 1 < 2
Theorem	2lt3 9092	2 is less than 3. (Contributed by NM, 26-Sep-2010.)
⊢ 2 < 3
Theorem	1lt3 9093	1 is less than 3. (Contributed by NM, 26-Sep-2010.)
⊢ 1 < 3
Theorem	3lt4 9094	3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 3 < 4
Theorem	2lt4 9095	2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 2 < 4
Theorem	1lt4 9096	1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 1 < 4
Theorem	4lt5 9097	4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 4 < 5
Theorem	3lt5 9098	3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 3 < 5
Theorem	2lt5 9099	2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 2 < 5
Theorem	1lt5 9100	1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 1 < 5