P. 82 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8101-8200   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-5 8101	Define the number 5. (Contributed by NM, 27-May-1999.)
|- 5 = ( 4 + 1 )
Definition	df-6 8102	Define the number 6. (Contributed by NM, 27-May-1999.)
|- 6 = ( 5 + 1 )
Definition	df-7 8103	Define the number 7. (Contributed by NM, 27-May-1999.)
|- 7 = ( 6 + 1 )
Definition	df-8 8104	Define the number 8. (Contributed by NM, 27-May-1999.)
|- 8 = ( 7 + 1 )
Definition	df-9 8105	Define the number 9. (Contributed by NM, 27-May-1999.)
|- 9 = ( 8 + 1 )
Theorem	0ne1 8106	0 =/= 1 (common case). See aso 1ap0 7690. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 =/= 1
Theorem	1ne0 8107	1 =/= 0. See aso 1ap0 7690. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 1 =/= 0
Theorem	1m1e0 8108	( 1 - 1 ) = 0 (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 1 - 1 ) = 0
Theorem	2re 8109	The number 2 is real. (Contributed by NM, 27-May-1999.)
|- 2 e. RR
Theorem	2cn 8110	The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
|- 2 e. CC
Theorem	2ex 8111	2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 2 e. _V
Theorem	2cnd 8112	2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ph -> 2 e. CC )
Theorem	3re 8113	The number 3 is real. (Contributed by NM, 27-May-1999.)
|- 3 e. RR
Theorem	3cn 8114	The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
|- 3 e. CC
Theorem	3ex 8115	3 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 3 e. _V
Theorem	4re 8116	The number 4 is real. (Contributed by NM, 27-May-1999.)
|- 4 e. RR
Theorem	4cn 8117	The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 4 e. CC
Theorem	5re 8118	The number 5 is real. (Contributed by NM, 27-May-1999.)
|- 5 e. RR
Theorem	5cn 8119	The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 5 e. CC
Theorem	6re 8120	The number 6 is real. (Contributed by NM, 27-May-1999.)
|- 6 e. RR
Theorem	6cn 8121	The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 6 e. CC
Theorem	7re 8122	The number 7 is real. (Contributed by NM, 27-May-1999.)
|- 7 e. RR
Theorem	7cn 8123	The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 7 e. CC
Theorem	8re 8124	The number 8 is real. (Contributed by NM, 27-May-1999.)
|- 8 e. RR
Theorem	8cn 8125	The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 8 e. CC
Theorem	9re 8126	The number 9 is real. (Contributed by NM, 27-May-1999.)
|- 9 e. RR
Theorem	9cn 8127	The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 9 e. CC
Theorem	0le0 8128	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 0 <_ 0
Theorem	0le2 8129	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
|- 0 <_ 2
Theorem	2pos 8130	The number 2 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 2
Theorem	2ne0 8131	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
|- 2 =/= 0
Theorem	2ap0 8132	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 2 # 0
Theorem	3pos 8133	The number 3 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 3
Theorem	3ne0 8134	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- 3 =/= 0
Theorem	3ap0 8135	The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- 3 # 0
Theorem	4pos 8136	The number 4 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 4
Theorem	4ne0 8137	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
|- 4 =/= 0
Theorem	4ap0 8138	The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- 4 # 0
Theorem	5pos 8139	The number 5 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 5
Theorem	6pos 8140	The number 6 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 6
Theorem	7pos 8141	The number 7 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 7
Theorem	8pos 8142	The number 8 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 8
Theorem	9pos 8143	The number 9 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 9
3.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 8144	-1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- -u 1 e. CC
Theorem	neg1rr 8145	-1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
|- -u 1 e. RR
Theorem	neg1ne0 8146	-1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u 1 =/= 0
Theorem	neg1lt0 8147	-1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u 1 < 0
Theorem	neg1ap0 8148	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
|- -u 1 # 0
Theorem	negneg1e1 8149	-u -u 1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u -u 1 = 1
Theorem	1pneg1e0 8150	1 + -u 1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + -u 1 ) = 0
Theorem	0m0e0 8151	0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 0 - 0 ) = 0
Theorem	1m0e1 8152	1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 - 0 ) = 1
Theorem	0p1e1 8153	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 0 + 1 ) = 1
Theorem	1p0e1 8154	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + 0 ) = 1
Theorem	1p1e2 8155	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
|- ( 1 + 1 ) = 2
Theorem	2m1e1 8156	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 8177. (Contributed by David A. Wheeler, 4-Jan-2017.)
|- ( 2 - 1 ) = 1
Theorem	1e2m1 8157	1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 1 = ( 2 - 1 )
Theorem	3m1e2 8158	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.)
|- ( 3 - 1 ) = 2
Theorem	2p2e4 8159	Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: http://us.metamath.org/mpeuni/mmset.html#trivia. (Contributed by NM, 27-May-1999.)
|- ( 2 + 2 ) = 4
Theorem	2times 8160	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 8161	A number times 2. (Contributed by NM, 16-Oct-2007.)
|- ( A e. CC -> ( A x. 2 ) = ( A + A ) )
Theorem	2timesi 8162	Two times a number. (Contributed by NM, 1-Aug-1999.)
|- A e. CC   =>    |- ( 2 x. A ) = ( A + A )
Theorem	times2i 8163	A number times 2. (Contributed by NM, 11-May-2004.)
|- A e. CC   =>    |- ( A x. 2 ) = ( A + A )
Theorem	2div2e1 8164	2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 2 / 2 ) = 1
Theorem	2p1e3 8165	2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 2 + 1 ) = 3
Theorem	1p2e3 8166	1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + 2 ) = 3
Theorem	3p1e4 8167	3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 3 + 1 ) = 4
Theorem	4p1e5 8168	4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 4 + 1 ) = 5
Theorem	5p1e6 8169	5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 5 + 1 ) = 6
Theorem	6p1e7 8170	6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 6 + 1 ) = 7
Theorem	7p1e8 8171	7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 7 + 1 ) = 8
Theorem	8p1e9 8172	8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 8 + 1 ) = 9
Theorem	3p2e5 8173	3 + 2 = 5. (Contributed by NM, 11-May-2004.)
|- ( 3 + 2 ) = 5
Theorem	3p3e6 8174	3 + 3 = 6. (Contributed by NM, 11-May-2004.)
|- ( 3 + 3 ) = 6
Theorem	4p2e6 8175	4 + 2 = 6. (Contributed by NM, 11-May-2004.)
|- ( 4 + 2 ) = 6
Theorem	4p3e7 8176	4 + 3 = 7. (Contributed by NM, 11-May-2004.)
|- ( 4 + 3 ) = 7
Theorem	4p4e8 8177	4 + 4 = 8. (Contributed by NM, 11-May-2004.)
|- ( 4 + 4 ) = 8
Theorem	5p2e7 8178	5 + 2 = 7. (Contributed by NM, 11-May-2004.)
|- ( 5 + 2 ) = 7
Theorem	5p3e8 8179	5 + 3 = 8. (Contributed by NM, 11-May-2004.)
|- ( 5 + 3 ) = 8
Theorem	5p4e9 8180	5 + 4 = 9. (Contributed by NM, 11-May-2004.)
|- ( 5 + 4 ) = 9
Theorem	6p2e8 8181	6 + 2 = 8. (Contributed by NM, 11-May-2004.)
|- ( 6 + 2 ) = 8
Theorem	6p3e9 8182	6 + 3 = 9. (Contributed by NM, 11-May-2004.)
|- ( 6 + 3 ) = 9
Theorem	7p2e9 8183	7 + 2 = 9. (Contributed by NM, 11-May-2004.)
|- ( 7 + 2 ) = 9
Theorem	1t1e1 8184	1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 1 x. 1 ) = 1
Theorem	2t1e2 8185	2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( 2 x. 1 ) = 2
Theorem	2t2e4 8186	2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.)
|- ( 2 x. 2 ) = 4
Theorem	3t1e3 8187	3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 3 x. 1 ) = 3
Theorem	3t2e6 8188	3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.)
|- ( 3 x. 2 ) = 6
Theorem	3t3e9 8189	3 times 3 equals 9. (Contributed by NM, 11-May-2004.)
|- ( 3 x. 3 ) = 9
Theorem	4t2e8 8190	4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.)
|- ( 4 x. 2 ) = 8
Theorem	2t0e0 8191	2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 2 x. 0 ) = 0
Theorem	4d2e2 8192	One half of four is two. (Contributed by NM, 3-Sep-1999.)
|- ( 4 / 2 ) = 2
Theorem	2nn 8193	2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
|- 2 e. NN
Theorem	3nn 8194	3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
|- 3 e. NN
Theorem	4nn 8195	4 is a positive integer. (Contributed by NM, 8-Jan-2006.)
|- 4 e. NN
Theorem	5nn 8196	5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|- 5 e. NN
Theorem	6nn 8197	6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|- 6 e. NN
Theorem	7nn 8198	7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|- 7 e. NN
Theorem	8nn 8199	8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|- 8 e. NN
Theorem	9nn 8200	9 is a positive integer. (Contributed by NM, 21-Oct-2012.)
|- 9 e. NN