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