P. 95 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9401-9500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	9re 9401	The number 9 is real. (Contributed by NM, 27-May-1999.)
⊢ 9 ∈ ℝ
Theorem	9cn 9402	The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 9 ∈ ℂ
Theorem	0le0 9403	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ≤ 0
Theorem	0le2 9404	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ 0 ≤ 2
Theorem	2pos 9405	The number 2 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 2
Theorem	2ne0 9406	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
⊢ 2 ≠ 0
Theorem	2ap0 9407	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 2 # 0
Theorem	3pos 9408	The number 3 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 3
Theorem	3ne0 9409	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 3 ≠ 0
Theorem	3ap0 9410	The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
⊢ 3 # 0
Theorem	4pos 9411	The number 4 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 4
Theorem	4ne0 9412	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ 4 ≠ 0
Theorem	4ap0 9413	The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
⊢ 4 # 0
Theorem	5pos 9414	The number 5 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 5
Theorem	6pos 9415	The number 6 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 6
Theorem	7pos 9416	The number 7 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 7
Theorem	8pos 9417	The number 8 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 8
Theorem	9pos 9418	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 9419	-1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ -1 ∈ ℂ
Theorem	neg1rr 9420	-1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ -1 ∈ ℝ
Theorem	neg1ne0 9421	-1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 ≠ 0
Theorem	neg1lt0 9422	-1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 < 0
Theorem	neg1ap0 9423	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
⊢ -1 # 0
Theorem	negneg1e1 9424	- -1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ - -1 = 1
Theorem	1pneg1e0 9425	1 + -1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + -1) = 0
Theorem	0m0e0 9426	0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (0 − 0) = 0
Theorem	1m0e1 9427	1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 − 0) = 1
Theorem	0p1e1 9428	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (0 + 1) = 1
Theorem	fv0p1e1 9429	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 9430	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 0) = 1
Theorem	1p1e2 9431	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
⊢ (1 + 1) = 2
Theorem	2m1e1 9432	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 9460. (Contributed by David A. Wheeler, 4-Jan-2017.)
⊢ (2 − 1) = 1
Theorem	1e2m1 9433	1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 1 = (2 − 1)
Theorem	3m1e2 9434	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.)
⊢ (3 − 1) = 2
Theorem	4m1e3 9435	4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.)
⊢ (4 − 1) = 3
Theorem	5m1e4 9436	5 - 1 = 4. (Contributed by AV, 6-Sep-2021.)
⊢ (5 − 1) = 4
Theorem	6m1e5 9437	6 - 1 = 5. (Contributed by AV, 6-Sep-2021.)
⊢ (6 − 1) = 5
Theorem	7m1e6 9438	7 - 1 = 6. (Contributed by AV, 6-Sep-2021.)
⊢ (7 − 1) = 6
Theorem	8m1e7 9439	8 - 1 = 7. (Contributed by AV, 6-Sep-2021.)
⊢ (8 − 1) = 7
Theorem	9m1e8 9440	9 - 1 = 8. (Contributed by AV, 6-Sep-2021.)
⊢ (9 − 1) = 8
Theorem	2p2e4 9441	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 9442	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 9443	A number times 2. (Contributed by NM, 16-Oct-2007.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 2) = (𝐴 + 𝐴))
Theorem	2timesi 9444	Two times a number. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (2 · 𝐴) = (𝐴 + 𝐴)
Theorem	times2i 9445	A number times 2. (Contributed by NM, 11-May-2004.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · 2) = (𝐴 + 𝐴)
Theorem	2txmxeqx 9446	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 9447	2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (2 / 2) = 1
Theorem	2p1e3 9448	2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (2 + 1) = 3
Theorem	1p2e3 9449	1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 2) = 3
Theorem	3p1e4 9450	3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (3 + 1) = 4
Theorem	4p1e5 9451	4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (4 + 1) = 5
Theorem	5p1e6 9452	5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (5 + 1) = 6
Theorem	6p1e7 9453	6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (6 + 1) = 7
Theorem	7p1e8 9454	7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (7 + 1) = 8
Theorem	8p1e9 9455	8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (8 + 1) = 9
Theorem	3p2e5 9456	3 + 2 = 5. (Contributed by NM, 11-May-2004.)
⊢ (3 + 2) = 5
Theorem	3p3e6 9457	3 + 3 = 6. (Contributed by NM, 11-May-2004.)
⊢ (3 + 3) = 6
Theorem	4p2e6 9458	4 + 2 = 6. (Contributed by NM, 11-May-2004.)
⊢ (4 + 2) = 6
Theorem	4p3e7 9459	4 + 3 = 7. (Contributed by NM, 11-May-2004.)
⊢ (4 + 3) = 7
Theorem	4p4e8 9460	4 + 4 = 8. (Contributed by NM, 11-May-2004.)
⊢ (4 + 4) = 8
Theorem	5p2e7 9461	5 + 2 = 7. (Contributed by NM, 11-May-2004.)
⊢ (5 + 2) = 7
Theorem	5p3e8 9462	5 + 3 = 8. (Contributed by NM, 11-May-2004.)
⊢ (5 + 3) = 8
Theorem	5p4e9 9463	5 + 4 = 9. (Contributed by NM, 11-May-2004.)
⊢ (5 + 4) = 9
Theorem	6p2e8 9464	6 + 2 = 8. (Contributed by NM, 11-May-2004.)
⊢ (6 + 2) = 8
Theorem	6p3e9 9465	6 + 3 = 9. (Contributed by NM, 11-May-2004.)
⊢ (6 + 3) = 9
Theorem	7p2e9 9466	7 + 2 = 9. (Contributed by NM, 11-May-2004.)
⊢ (7 + 2) = 9
Theorem	1t1e1 9467	1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (1 · 1) = 1
Theorem	2t1e2 9468	2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (2 · 1) = 2
Theorem	2t2e4 9469	2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.)
⊢ (2 · 2) = 4
Theorem	3t1e3 9470	3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (3 · 1) = 3
Theorem	3t2e6 9471	3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.)
⊢ (3 · 2) = 6
Theorem	2t3e6 9472	2 times 3 equals 6. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ (2 · 3) = 6
Theorem	3t3e9 9473	3 times 3 equals 9. (Contributed by NM, 11-May-2004.)
⊢ (3 · 3) = 9
Theorem	4t2e8 9474	4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.)
⊢ (4 · 2) = 8
Theorem	2t4e8 9475	2 times 4 equals 8. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ (2 · 4) = 8
Theorem	2t0e0 9476	2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (2 · 0) = 0
Theorem	4d2e2 9477	One half of four is two. (Contributed by NM, 3-Sep-1999.)
⊢ (4 / 2) = 2
Theorem	2nn 9478	2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
⊢ 2 ∈ ℕ
Theorem	3nn 9479	3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 3 ∈ ℕ
Theorem	4nn 9480	4 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 4 ∈ ℕ
Theorem	5nn 9481	5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 5 ∈ ℕ
Theorem	6nn 9482	6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 6 ∈ ℕ
Theorem	7nn 9483	7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 7 ∈ ℕ
Theorem	8nn 9484	8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 8 ∈ ℕ
Theorem	9nn 9485	9 is a positive integer. (Contributed by NM, 21-Oct-2012.)
⊢ 9 ∈ ℕ
Theorem	1lt2 9486	1 is less than 2. (Contributed by NM, 24-Feb-2005.)
⊢ 1 < 2
Theorem	2lt3 9487	2 is less than 3. (Contributed by NM, 26-Sep-2010.)
⊢ 2 < 3
Theorem	1lt3 9488	1 is less than 3. (Contributed by NM, 26-Sep-2010.)
⊢ 1 < 3
Theorem	3lt4 9489	3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 3 < 4
Theorem	2lt4 9490	2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 2 < 4
Theorem	1lt4 9491	1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 1 < 4
Theorem	4lt5 9492	4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 4 < 5
Theorem	3lt5 9493	3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 3 < 5
Theorem	2lt5 9494	2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 2 < 5
Theorem	1lt5 9495	1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 1 < 5
Theorem	5lt6 9496	5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 5 < 6
Theorem	4lt6 9497	4 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 4 < 6
Theorem	3lt6 9498	3 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 3 < 6
Theorem	2lt6 9499	2 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 2 < 6
Theorem	1lt6 9500	1 is less than 6. (Contributed by NM, 19-Oct-2012.)
⊢ 1 < 6