P. 94 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9301-9400   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-7 9301	Define the number 7. (Contributed by NM, 27-May-1999.)
|- 7 = ( 6 + 1 )
Definition	df-8 9302	Define the number 8. (Contributed by NM, 27-May-1999.)
|- 8 = ( 7 + 1 )
Definition	df-9 9303	Define the number 9. (Contributed by NM, 27-May-1999.)
|- 9 = ( 8 + 1 )
Theorem	0ne1 9304	0 =/= 1 (common case). See aso 1ap0 8864. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 =/= 1
Theorem	1ne0 9305	1 =/= 0. See aso 1ap0 8864. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 1 =/= 0
Theorem	1m1e0 9306	( 1 - 1 ) = 0 (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 1 - 1 ) = 0
Theorem	2re 9307	The number 2 is real. (Contributed by NM, 27-May-1999.)
|- 2 e. RR
Theorem	2cn 9308	The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
|- 2 e. CC
Theorem	2ex 9309	2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 2 e. _V
Theorem	2cnd 9310	2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ph -> 2 e. CC )
Theorem	3re 9311	The number 3 is real. (Contributed by NM, 27-May-1999.)
|- 3 e. RR
Theorem	3cn 9312	The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
|- 3 e. CC
Theorem	3ex 9313	3 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 3 e. _V
Theorem	4re 9314	The number 4 is real. (Contributed by NM, 27-May-1999.)
|- 4 e. RR
Theorem	4cn 9315	The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 4 e. CC
Theorem	5re 9316	The number 5 is real. (Contributed by NM, 27-May-1999.)
|- 5 e. RR
Theorem	5cn 9317	The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 5 e. CC
Theorem	6re 9318	The number 6 is real. (Contributed by NM, 27-May-1999.)
|- 6 e. RR
Theorem	6cn 9319	The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 6 e. CC
Theorem	7re 9320	The number 7 is real. (Contributed by NM, 27-May-1999.)
|- 7 e. RR
Theorem	7cn 9321	The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 7 e. CC
Theorem	8re 9322	The number 8 is real. (Contributed by NM, 27-May-1999.)
|- 8 e. RR
Theorem	8cn 9323	The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 8 e. CC
Theorem	9re 9324	The number 9 is real. (Contributed by NM, 27-May-1999.)
|- 9 e. RR
Theorem	9cn 9325	The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 9 e. CC
Theorem	0le0 9326	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 0 <_ 0
Theorem	0le2 9327	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
|- 0 <_ 2
Theorem	2pos 9328	The number 2 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 2
Theorem	2ne0 9329	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
|- 2 =/= 0
Theorem	2ap0 9330	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 2 # 0
Theorem	3pos 9331	The number 3 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 3
Theorem	3ne0 9332	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- 3 =/= 0
Theorem	3ap0 9333	The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- 3 # 0
Theorem	4pos 9334	The number 4 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 4
Theorem	4ne0 9335	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
|- 4 =/= 0
Theorem	4ap0 9336	The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- 4 # 0
Theorem	5pos 9337	The number 5 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 5
Theorem	6pos 9338	The number 6 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 6
Theorem	7pos 9339	The number 7 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 7
Theorem	8pos 9340	The number 8 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 8
Theorem	9pos 9341	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 9342	-1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- -u 1 e. CC
Theorem	neg1rr 9343	-1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
|- -u 1 e. RR
Theorem	neg1ne0 9344	-1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u 1 =/= 0
Theorem	neg1lt0 9345	-1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u 1 < 0
Theorem	neg1ap0 9346	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
|- -u 1 # 0
Theorem	negneg1e1 9347	-u -u 1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u -u 1 = 1
Theorem	1pneg1e0 9348	1 + -u 1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + -u 1 ) = 0
Theorem	0m0e0 9349	0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 0 - 0 ) = 0
Theorem	1m0e1 9350	1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 - 0 ) = 1
Theorem	0p1e1 9351	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 0 + 1 ) = 1
Theorem	fv0p1e1 9352	Function value at N + 1 with N replaced by 0. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.)
|- ( N = 0 -> ( F ` ( N + 1 ) ) = ( F ` 1 ) )
Theorem	1p0e1 9353	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + 0 ) = 1
Theorem	1p1e2 9354	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
|- ( 1 + 1 ) = 2
Theorem	2m1e1 9355	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 9383. (Contributed by David A. Wheeler, 4-Jan-2017.)
|- ( 2 - 1 ) = 1
Theorem	1e2m1 9356	1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 1 = ( 2 - 1 )
Theorem	3m1e2 9357	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.)
|- ( 3 - 1 ) = 2
Theorem	4m1e3 9358	4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.)
|- ( 4 - 1 ) = 3
Theorem	5m1e4 9359	5 - 1 = 4. (Contributed by AV, 6-Sep-2021.)
|- ( 5 - 1 ) = 4
Theorem	6m1e5 9360	6 - 1 = 5. (Contributed by AV, 6-Sep-2021.)
|- ( 6 - 1 ) = 5
Theorem	7m1e6 9361	7 - 1 = 6. (Contributed by AV, 6-Sep-2021.)
|- ( 7 - 1 ) = 6
Theorem	8m1e7 9362	8 - 1 = 7. (Contributed by AV, 6-Sep-2021.)
|- ( 8 - 1 ) = 7
Theorem	9m1e8 9363	9 - 1 = 8. (Contributed by AV, 6-Sep-2021.)
|- ( 9 - 1 ) = 8
Theorem	2p2e4 9364	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 9365	Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.)
|- ( A e. CC -> ( 2 x. A ) = ( A + A ) )
Theorem	times2 9366	A number times 2. (Contributed by NM, 16-Oct-2007.)
|- ( A e. CC -> ( A x. 2 ) = ( A + A ) )
Theorem	2timesi 9367	Two times a number. (Contributed by NM, 1-Aug-1999.)
|- A e. CC   =>    |- ( 2 x. A ) = ( A + A )
Theorem	times2i 9368	A number times 2. (Contributed by NM, 11-May-2004.)
|- A e. CC   =>    |- ( A x. 2 ) = ( A + A )
Theorem	2txmxeqx 9369	Two times a complex number minus the number itself results in the number itself. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
|- ( X e. CC -> ( ( 2 x. X ) - X ) = X )
Theorem	2div2e1 9370	2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 2 / 2 ) = 1
Theorem	2p1e3 9371	2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 2 + 1 ) = 3
Theorem	1p2e3 9372	1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + 2 ) = 3
Theorem	3p1e4 9373	3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 3 + 1 ) = 4
Theorem	4p1e5 9374	4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 4 + 1 ) = 5
Theorem	5p1e6 9375	5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 5 + 1 ) = 6
Theorem	6p1e7 9376	6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 6 + 1 ) = 7
Theorem	7p1e8 9377	7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 7 + 1 ) = 8
Theorem	8p1e9 9378	8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 8 + 1 ) = 9
Theorem	3p2e5 9379	3 + 2 = 5. (Contributed by NM, 11-May-2004.)
|- ( 3 + 2 ) = 5
Theorem	3p3e6 9380	3 + 3 = 6. (Contributed by NM, 11-May-2004.)
|- ( 3 + 3 ) = 6
Theorem	4p2e6 9381	4 + 2 = 6. (Contributed by NM, 11-May-2004.)
|- ( 4 + 2 ) = 6
Theorem	4p3e7 9382	4 + 3 = 7. (Contributed by NM, 11-May-2004.)
|- ( 4 + 3 ) = 7
Theorem	4p4e8 9383	4 + 4 = 8. (Contributed by NM, 11-May-2004.)
|- ( 4 + 4 ) = 8
Theorem	5p2e7 9384	5 + 2 = 7. (Contributed by NM, 11-May-2004.)
|- ( 5 + 2 ) = 7
Theorem	5p3e8 9385	5 + 3 = 8. (Contributed by NM, 11-May-2004.)
|- ( 5 + 3 ) = 8
Theorem	5p4e9 9386	5 + 4 = 9. (Contributed by NM, 11-May-2004.)
|- ( 5 + 4 ) = 9
Theorem	6p2e8 9387	6 + 2 = 8. (Contributed by NM, 11-May-2004.)
|- ( 6 + 2 ) = 8
Theorem	6p3e9 9388	6 + 3 = 9. (Contributed by NM, 11-May-2004.)
|- ( 6 + 3 ) = 9
Theorem	7p2e9 9389	7 + 2 = 9. (Contributed by NM, 11-May-2004.)
|- ( 7 + 2 ) = 9
Theorem	1t1e1 9390	1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 1 x. 1 ) = 1
Theorem	2t1e2 9391	2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( 2 x. 1 ) = 2
Theorem	2t2e4 9392	2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.)
|- ( 2 x. 2 ) = 4
Theorem	3t1e3 9393	3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 3 x. 1 ) = 3
Theorem	3t2e6 9394	3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.)
|- ( 3 x. 2 ) = 6
Theorem	3t3e9 9395	3 times 3 equals 9. (Contributed by NM, 11-May-2004.)
|- ( 3 x. 3 ) = 9
Theorem	4t2e8 9396	4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.)
|- ( 4 x. 2 ) = 8
Theorem	2t0e0 9397	2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 2 x. 0 ) = 0
Theorem	4d2e2 9398	One half of four is two. (Contributed by NM, 3-Sep-1999.)
|- ( 4 / 2 ) = 2
Theorem	2nn 9399	2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
|- 2 e. NN
Theorem	3nn 9400	3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
|- 3 e. NN