P. 93 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9201-9300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	7re 9201	The number 7 is real. (Contributed by NM, 27-May-1999.)
⊢ 7 ∈ ℝ
Theorem	7cn 9202	The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 7 ∈ ℂ
Theorem	8re 9203	The number 8 is real. (Contributed by NM, 27-May-1999.)
⊢ 8 ∈ ℝ
Theorem	8cn 9204	The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 8 ∈ ℂ
Theorem	9re 9205	The number 9 is real. (Contributed by NM, 27-May-1999.)
⊢ 9 ∈ ℝ
Theorem	9cn 9206	The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 9 ∈ ℂ
Theorem	0le0 9207	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ≤ 0
Theorem	0le2 9208	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ 0 ≤ 2
Theorem	2pos 9209	The number 2 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 2
Theorem	2ne0 9210	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
⊢ 2 ≠ 0
Theorem	2ap0 9211	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 2 # 0
Theorem	3pos 9212	The number 3 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 3
Theorem	3ne0 9213	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 3 ≠ 0
Theorem	3ap0 9214	The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
⊢ 3 # 0
Theorem	4pos 9215	The number 4 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 4
Theorem	4ne0 9216	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ 4 ≠ 0
Theorem	4ap0 9217	The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
⊢ 4 # 0
Theorem	5pos 9218	The number 5 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 5
Theorem	6pos 9219	The number 6 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 6
Theorem	7pos 9220	The number 7 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 7
Theorem	8pos 9221	The number 8 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 8
Theorem	9pos 9222	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 9223	-1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ -1 ∈ ℂ
Theorem	neg1rr 9224	-1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ -1 ∈ ℝ
Theorem	neg1ne0 9225	-1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 ≠ 0
Theorem	neg1lt0 9226	-1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 < 0
Theorem	neg1ap0 9227	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
⊢ -1 # 0
Theorem	negneg1e1 9228	--1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ --1 = 1
Theorem	1pneg1e0 9229	1 + -1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + -1) = 0
Theorem	0m0e0 9230	0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (0 − 0) = 0
Theorem	1m0e1 9231	1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 − 0) = 1
Theorem	0p1e1 9232	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (0 + 1) = 1
Theorem	fv0p1e1 9233	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 9234	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 0) = 1
Theorem	1p1e2 9235	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
⊢ (1 + 1) = 2
Theorem	2m1e1 9236	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 9264. (Contributed by David A. Wheeler, 4-Jan-2017.)
⊢ (2 − 1) = 1
Theorem	1e2m1 9237	1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 1 = (2 − 1)
Theorem	3m1e2 9238	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.)
⊢ (3 − 1) = 2
Theorem	4m1e3 9239	4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.)
⊢ (4 − 1) = 3
Theorem	5m1e4 9240	5 - 1 = 4. (Contributed by AV, 6-Sep-2021.)
⊢ (5 − 1) = 4
Theorem	6m1e5 9241	6 - 1 = 5. (Contributed by AV, 6-Sep-2021.)
⊢ (6 − 1) = 5
Theorem	7m1e6 9242	7 - 1 = 6. (Contributed by AV, 6-Sep-2021.)
⊢ (7 − 1) = 6
Theorem	8m1e7 9243	8 - 1 = 7. (Contributed by AV, 6-Sep-2021.)
⊢ (8 − 1) = 7
Theorem	9m1e8 9244	9 - 1 = 8. (Contributed by AV, 6-Sep-2021.)
⊢ (9 − 1) = 8
Theorem	2p2e4 9245	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 9246	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 9247	A number times 2. (Contributed by NM, 16-Oct-2007.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 2) = (𝐴 + 𝐴))
Theorem	2timesi 9248	Two times a number. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (2 · 𝐴) = (𝐴 + 𝐴)
Theorem	times2i 9249	A number times 2. (Contributed by NM, 11-May-2004.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · 2) = (𝐴 + 𝐴)
Theorem	2txmxeqx 9250	Two times a complex number minus the number itself results in the number itself. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
⊢ (𝑋 ∈ ℂ → ((2 · 𝑋) − 𝑋) = 𝑋)
Theorem	2div2e1 9251	2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (2 / 2) = 1
Theorem	2p1e3 9252	2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (2 + 1) = 3
Theorem	1p2e3 9253	1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 2) = 3
Theorem	3p1e4 9254	3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (3 + 1) = 4
Theorem	4p1e5 9255	4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (4 + 1) = 5
Theorem	5p1e6 9256	5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (5 + 1) = 6
Theorem	6p1e7 9257	6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (6 + 1) = 7
Theorem	7p1e8 9258	7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (7 + 1) = 8
Theorem	8p1e9 9259	8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (8 + 1) = 9
Theorem	3p2e5 9260	3 + 2 = 5. (Contributed by NM, 11-May-2004.)
⊢ (3 + 2) = 5
Theorem	3p3e6 9261	3 + 3 = 6. (Contributed by NM, 11-May-2004.)
⊢ (3 + 3) = 6
Theorem	4p2e6 9262	4 + 2 = 6. (Contributed by NM, 11-May-2004.)
⊢ (4 + 2) = 6
Theorem	4p3e7 9263	4 + 3 = 7. (Contributed by NM, 11-May-2004.)
⊢ (4 + 3) = 7
Theorem	4p4e8 9264	4 + 4 = 8. (Contributed by NM, 11-May-2004.)
⊢ (4 + 4) = 8
Theorem	5p2e7 9265	5 + 2 = 7. (Contributed by NM, 11-May-2004.)
⊢ (5 + 2) = 7
Theorem	5p3e8 9266	5 + 3 = 8. (Contributed by NM, 11-May-2004.)
⊢ (5 + 3) = 8
Theorem	5p4e9 9267	5 + 4 = 9. (Contributed by NM, 11-May-2004.)
⊢ (5 + 4) = 9
Theorem	6p2e8 9268	6 + 2 = 8. (Contributed by NM, 11-May-2004.)
⊢ (6 + 2) = 8
Theorem	6p3e9 9269	6 + 3 = 9. (Contributed by NM, 11-May-2004.)
⊢ (6 + 3) = 9
Theorem	7p2e9 9270	7 + 2 = 9. (Contributed by NM, 11-May-2004.)
⊢ (7 + 2) = 9
Theorem	1t1e1 9271	1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (1 · 1) = 1
Theorem	2t1e2 9272	2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (2 · 1) = 2
Theorem	2t2e4 9273	2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.)
⊢ (2 · 2) = 4
Theorem	3t1e3 9274	3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (3 · 1) = 3
Theorem	3t2e6 9275	3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.)
⊢ (3 · 2) = 6
Theorem	3t3e9 9276	3 times 3 equals 9. (Contributed by NM, 11-May-2004.)
⊢ (3 · 3) = 9
Theorem	4t2e8 9277	4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.)
⊢ (4 · 2) = 8
Theorem	2t0e0 9278	2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (2 · 0) = 0
Theorem	4d2e2 9279	One half of four is two. (Contributed by NM, 3-Sep-1999.)
⊢ (4 / 2) = 2
Theorem	2nn 9280	2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
⊢ 2 ∈ ℕ
Theorem	3nn 9281	3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 3 ∈ ℕ
Theorem	4nn 9282	4 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 4 ∈ ℕ
Theorem	5nn 9283	5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 5 ∈ ℕ
Theorem	6nn 9284	6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 6 ∈ ℕ
Theorem	7nn 9285	7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 7 ∈ ℕ
Theorem	8nn 9286	8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 8 ∈ ℕ
Theorem	9nn 9287	9 is a positive integer. (Contributed by NM, 21-Oct-2012.)
⊢ 9 ∈ ℕ
Theorem	1lt2 9288	1 is less than 2. (Contributed by NM, 24-Feb-2005.)
⊢ 1 < 2
Theorem	2lt3 9289	2 is less than 3. (Contributed by NM, 26-Sep-2010.)
⊢ 2 < 3
Theorem	1lt3 9290	1 is less than 3. (Contributed by NM, 26-Sep-2010.)
⊢ 1 < 3
Theorem	3lt4 9291	3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 3 < 4
Theorem	2lt4 9292	2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 2 < 4
Theorem	1lt4 9293	1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 1 < 4
Theorem	4lt5 9294	4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 4 < 5
Theorem	3lt5 9295	3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 3 < 5
Theorem	2lt5 9296	2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 2 < 5
Theorem	1lt5 9297	1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 1 < 5
Theorem	5lt6 9298	5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 5 < 6
Theorem	4lt6 9299	4 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 4 < 6
Theorem	3lt6 9300	3 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 3 < 6