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
Definition	df-2 9201	Define the number 2. (Contributed by NM, 27-May-1999.)
|- 2 = ( 1 + 1 )
Definition	df-3 9202	Define the number 3. (Contributed by NM, 27-May-1999.)
|- 3 = ( 2 + 1 )
Definition	df-4 9203	Define the number 4. (Contributed by NM, 27-May-1999.)
|- 4 = ( 3 + 1 )
Definition	df-5 9204	Define the number 5. (Contributed by NM, 27-May-1999.)
|- 5 = ( 4 + 1 )
Definition	df-6 9205	Define the number 6. (Contributed by NM, 27-May-1999.)
|- 6 = ( 5 + 1 )
Definition	df-7 9206	Define the number 7. (Contributed by NM, 27-May-1999.)
|- 7 = ( 6 + 1 )
Definition	df-8 9207	Define the number 8. (Contributed by NM, 27-May-1999.)
|- 8 = ( 7 + 1 )
Definition	df-9 9208	Define the number 9. (Contributed by NM, 27-May-1999.)
|- 9 = ( 8 + 1 )
Theorem	0ne1 9209	0 =/= 1 (common case). See aso 1ap0 8769. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 =/= 1
Theorem	1ne0 9210	1 =/= 0. See aso 1ap0 8769. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 1 =/= 0
Theorem	1m1e0 9211	( 1 - 1 ) = 0 (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 1 - 1 ) = 0
Theorem	2re 9212	The number 2 is real. (Contributed by NM, 27-May-1999.)
|- 2 e. RR
Theorem	2cn 9213	The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
|- 2 e. CC
Theorem	2ex 9214	2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 2 e. _V
Theorem	2cnd 9215	2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ph -> 2 e. CC )
Theorem	3re 9216	The number 3 is real. (Contributed by NM, 27-May-1999.)
|- 3 e. RR
Theorem	3cn 9217	The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
|- 3 e. CC
Theorem	3ex 9218	3 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 3 e. _V
Theorem	4re 9219	The number 4 is real. (Contributed by NM, 27-May-1999.)
|- 4 e. RR
Theorem	4cn 9220	The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 4 e. CC
Theorem	5re 9221	The number 5 is real. (Contributed by NM, 27-May-1999.)
|- 5 e. RR
Theorem	5cn 9222	The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 5 e. CC
Theorem	6re 9223	The number 6 is real. (Contributed by NM, 27-May-1999.)
|- 6 e. RR
Theorem	6cn 9224	The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 6 e. CC
Theorem	7re 9225	The number 7 is real. (Contributed by NM, 27-May-1999.)
|- 7 e. RR
Theorem	7cn 9226	The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 7 e. CC
Theorem	8re 9227	The number 8 is real. (Contributed by NM, 27-May-1999.)
|- 8 e. RR
Theorem	8cn 9228	The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 8 e. CC
Theorem	9re 9229	The number 9 is real. (Contributed by NM, 27-May-1999.)
|- 9 e. RR
Theorem	9cn 9230	The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 9 e. CC
Theorem	0le0 9231	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 0 <_ 0
Theorem	0le2 9232	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
|- 0 <_ 2
Theorem	2pos 9233	The number 2 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 2
Theorem	2ne0 9234	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
|- 2 =/= 0
Theorem	2ap0 9235	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 2 # 0
Theorem	3pos 9236	The number 3 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 3
Theorem	3ne0 9237	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- 3 =/= 0
Theorem	3ap0 9238	The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- 3 # 0
Theorem	4pos 9239	The number 4 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 4
Theorem	4ne0 9240	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
|- 4 =/= 0
Theorem	4ap0 9241	The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- 4 # 0
Theorem	5pos 9242	The number 5 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 5
Theorem	6pos 9243	The number 6 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 6
Theorem	7pos 9244	The number 7 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 7
Theorem	8pos 9245	The number 8 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 8
Theorem	9pos 9246	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 9247	-1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- -u 1 e. CC
Theorem	neg1rr 9248	-1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
|- -u 1 e. RR
Theorem	neg1ne0 9249	-1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u 1 =/= 0
Theorem	neg1lt0 9250	-1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u 1 < 0
Theorem	neg1ap0 9251	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
|- -u 1 # 0
Theorem	negneg1e1 9252	-u -u 1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u -u 1 = 1
Theorem	1pneg1e0 9253	1 + -u 1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + -u 1 ) = 0
Theorem	0m0e0 9254	0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 0 - 0 ) = 0
Theorem	1m0e1 9255	1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 - 0 ) = 1
Theorem	0p1e1 9256	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 0 + 1 ) = 1
Theorem	fv0p1e1 9257	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 9258	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + 0 ) = 1
Theorem	1p1e2 9259	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
|- ( 1 + 1 ) = 2
Theorem	2m1e1 9260	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 9288. (Contributed by David A. Wheeler, 4-Jan-2017.)
|- ( 2 - 1 ) = 1
Theorem	1e2m1 9261	1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 1 = ( 2 - 1 )
Theorem	3m1e2 9262	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.)
|- ( 3 - 1 ) = 2
Theorem	4m1e3 9263	4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.)
|- ( 4 - 1 ) = 3
Theorem	5m1e4 9264	5 - 1 = 4. (Contributed by AV, 6-Sep-2021.)
|- ( 5 - 1 ) = 4
Theorem	6m1e5 9265	6 - 1 = 5. (Contributed by AV, 6-Sep-2021.)
|- ( 6 - 1 ) = 5
Theorem	7m1e6 9266	7 - 1 = 6. (Contributed by AV, 6-Sep-2021.)
|- ( 7 - 1 ) = 6
Theorem	8m1e7 9267	8 - 1 = 7. (Contributed by AV, 6-Sep-2021.)
|- ( 8 - 1 ) = 7
Theorem	9m1e8 9268	9 - 1 = 8. (Contributed by AV, 6-Sep-2021.)
|- ( 9 - 1 ) = 8
Theorem	2p2e4 9269	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 9270	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 9271	A number times 2. (Contributed by NM, 16-Oct-2007.)
|- ( A e. CC -> ( A x. 2 ) = ( A + A ) )
Theorem	2timesi 9272	Two times a number. (Contributed by NM, 1-Aug-1999.)
|- A e. CC   =>    |- ( 2 x. A ) = ( A + A )
Theorem	times2i 9273	A number times 2. (Contributed by NM, 11-May-2004.)
|- A e. CC   =>    |- ( A x. 2 ) = ( A + A )
Theorem	2txmxeqx 9274	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 9275	2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 2 / 2 ) = 1
Theorem	2p1e3 9276	2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 2 + 1 ) = 3
Theorem	1p2e3 9277	1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + 2 ) = 3
Theorem	3p1e4 9278	3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 3 + 1 ) = 4
Theorem	4p1e5 9279	4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 4 + 1 ) = 5
Theorem	5p1e6 9280	5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 5 + 1 ) = 6
Theorem	6p1e7 9281	6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 6 + 1 ) = 7
Theorem	7p1e8 9282	7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 7 + 1 ) = 8
Theorem	8p1e9 9283	8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 8 + 1 ) = 9
Theorem	3p2e5 9284	3 + 2 = 5. (Contributed by NM, 11-May-2004.)
|- ( 3 + 2 ) = 5
Theorem	3p3e6 9285	3 + 3 = 6. (Contributed by NM, 11-May-2004.)
|- ( 3 + 3 ) = 6
Theorem	4p2e6 9286	4 + 2 = 6. (Contributed by NM, 11-May-2004.)
|- ( 4 + 2 ) = 6
Theorem	4p3e7 9287	4 + 3 = 7. (Contributed by NM, 11-May-2004.)
|- ( 4 + 3 ) = 7
Theorem	4p4e8 9288	4 + 4 = 8. (Contributed by NM, 11-May-2004.)
|- ( 4 + 4 ) = 8
Theorem	5p2e7 9289	5 + 2 = 7. (Contributed by NM, 11-May-2004.)
|- ( 5 + 2 ) = 7
Theorem	5p3e8 9290	5 + 3 = 8. (Contributed by NM, 11-May-2004.)
|- ( 5 + 3 ) = 8
Theorem	5p4e9 9291	5 + 4 = 9. (Contributed by NM, 11-May-2004.)
|- ( 5 + 4 ) = 9
Theorem	6p2e8 9292	6 + 2 = 8. (Contributed by NM, 11-May-2004.)
|- ( 6 + 2 ) = 8
Theorem	6p3e9 9293	6 + 3 = 9. (Contributed by NM, 11-May-2004.)
|- ( 6 + 3 ) = 9
Theorem	7p2e9 9294	7 + 2 = 9. (Contributed by NM, 11-May-2004.)
|- ( 7 + 2 ) = 9
Theorem	1t1e1 9295	1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 1 x. 1 ) = 1
Theorem	2t1e2 9296	2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( 2 x. 1 ) = 2
Theorem	2t2e4 9297	2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.)
|- ( 2 x. 2 ) = 4
Theorem	3t1e3 9298	3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 3 x. 1 ) = 3
Theorem	3t2e6 9299	3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.)
|- ( 3 x. 2 ) = 6
Theorem	3t3e9 9300	3 times 3 equals 9. (Contributed by NM, 11-May-2004.)
|- ( 3 x. 3 ) = 9