P. 87 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8601-8700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnge1 8601	A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.)
|- ( A e. NN -> 1 <_ A )
Theorem	nnle1eq1 8602	A positive integer is less than or equal to one iff it is equal to one. (Contributed by NM, 3-Apr-2005.)
|- ( A e. NN -> ( A <_ 1 <-> A = 1 ) )
Theorem	nngt0 8603	A positive integer is positive. (Contributed by NM, 26-Sep-1999.)
|- ( A e. NN -> 0 < A )
Theorem	nnnlt1 8604	A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( A e. NN -> -. A < 1 )
Theorem	0nnn 8605	Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.)
|- -. 0 e. NN
Theorem	nnne0 8606	A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.)
|- ( A e. NN -> A =/= 0 )
Theorem	nnap0 8607	A positive integer is apart from zero. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( A e. NN -> A # 0 )
Theorem	nngt0i 8608	A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.)
|- A e. NN   =>    |- 0 < A
Theorem	nnap0i 8609	A positive integer is apart from zero (inference version). (Contributed by Jim Kingdon, 1-Jan-2023.)
|- A e. NN   =>    |- A # 0
Theorem	nnne0i 8610	A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.)
|- A e. NN   =>    |- A =/= 0
Theorem	nn2ge 8611*	There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.)
|- ( ( A e. NN /\ B e. NN ) -> E. x e. NN ( A <_ x /\ B <_ x ) )
Theorem	nn1gt1 8612	A positive integer is either one or greater than one. This is for NN; 0elnn 4470 is a similar theorem for om (the natural numbers as ordinals). (Contributed by Jim Kingdon, 7-Mar-2020.)
|- ( A e. NN -> ( A = 1 \/ 1 < A ) )
Theorem	nngt1ne1 8613	A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.)
|- ( A e. NN -> ( 1 < A <-> A =/= 1 ) )
Theorem	nndivre 8614	The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.)
|- ( ( A e. RR /\ N e. NN ) -> ( A / N ) e. RR )
Theorem	nnrecre 8615	The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.)
|- ( N e. NN -> ( 1 / N ) e. RR )
Theorem	nnrecgt0 8616	The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.)
|- ( A e. NN -> 0 < ( 1 / A ) )
Theorem	nnsub 8617	Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.)
|- ( ( A e. NN /\ B e. NN ) -> ( A < B <-> ( B - A ) e. NN ) )
Theorem	nnsubi 8618	Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.)
|- A e. NN   &    |- B e. NN   =>    |- ( A < B <-> ( B - A ) e. NN )
Theorem	nndiv 8619*	Two ways to express " A divides B " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|- ( ( A e. NN /\ B e. NN ) -> ( E. x e. NN ( A x. x ) = B <-> ( B / A ) e. NN ) )
Theorem	nndivtr 8620	Transitive property of divisibility: if A divides B and B divides C, then A divides C. Typically, C would be an integer, although the theorem holds for complex C. (Contributed by NM, 3-May-2005.)
|- ( ( ( A e. NN /\ B e. NN /\ C e. CC ) /\ ( ( B / A ) e. NN /\ ( C / B ) e. NN ) ) -> ( C / A ) e. NN )
Theorem	nnge1d 8621	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> 1 <_ A )
Theorem	nngt0d 8622	A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> 0 < A )
Theorem	nnne0d 8623	A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A =/= 0 )
Theorem	nnap0d 8624	A positive integer is apart from zero. (Contributed by Jim Kingdon, 25-Aug-2021.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A # 0 )
Theorem	nnrecred 8625	The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> ( 1 / A ) e. RR )
Theorem	nnaddcld 8626	Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   =>    |- ( ph -> ( A + B ) e. NN )
Theorem	nnmulcld 8627	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   =>    |- ( ph -> ( A x. B ) e. NN )
Theorem	nndivred 8628	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. NN )   =>    |- ( ph -> ( A / B ) e. RR )
3.4.3  Decimal representation of numbers The decimal representation of numbers/integers is based on the decimal digits 0 through 9 (df-0 7507 through df-9 8644), which are explicitly defined in the following. Note that the numbers 0 and 1 are constants defined as primitives of the complex number axiom system (see df-0 7507 and df-1 7508). Integers can also be exhibited as sums of powers of 10 (e.g. the number 103 can be expressed as ( (; 1 0 ^ 2 ) + 3 )) or as some other expression built from operations on the numbers 0 through 9. For example, the prime number 823541 can be expressed as ( 7 ^ 7 ) - 2. Most abstract math rarely requires numbers larger than 4. Even in Wiles' proof of Fermat's Last Theorem, the largest number used appears to be 12.
Syntax	c2 8629	Extend class notation to include the number 2.
class 2
Syntax	c3 8630	Extend class notation to include the number 3.
class 3
Syntax	c4 8631	Extend class notation to include the number 4.
class 4
Syntax	c5 8632	Extend class notation to include the number 5.
class 5
Syntax	c6 8633	Extend class notation to include the number 6.
class 6
Syntax	c7 8634	Extend class notation to include the number 7.
class 7
Syntax	c8 8635	Extend class notation to include the number 8.
class 8
Syntax	c9 8636	Extend class notation to include the number 9.
class 9
Definition	df-2 8637	Define the number 2. (Contributed by NM, 27-May-1999.)
|- 2 = ( 1 + 1 )
Definition	df-3 8638	Define the number 3. (Contributed by NM, 27-May-1999.)
|- 3 = ( 2 + 1 )
Definition	df-4 8639	Define the number 4. (Contributed by NM, 27-May-1999.)
|- 4 = ( 3 + 1 )
Definition	df-5 8640	Define the number 5. (Contributed by NM, 27-May-1999.)
|- 5 = ( 4 + 1 )
Definition	df-6 8641	Define the number 6. (Contributed by NM, 27-May-1999.)
|- 6 = ( 5 + 1 )
Definition	df-7 8642	Define the number 7. (Contributed by NM, 27-May-1999.)
|- 7 = ( 6 + 1 )
Definition	df-8 8643	Define the number 8. (Contributed by NM, 27-May-1999.)
|- 8 = ( 7 + 1 )
Definition	df-9 8644	Define the number 9. (Contributed by NM, 27-May-1999.)
|- 9 = ( 8 + 1 )
Theorem	0ne1 8645	0 =/= 1 (common case). See aso 1ap0 8218. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 =/= 1
Theorem	1ne0 8646	1 =/= 0. See aso 1ap0 8218. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 1 =/= 0
Theorem	1m1e0 8647	( 1 - 1 ) = 0 (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 1 - 1 ) = 0
Theorem	2re 8648	The number 2 is real. (Contributed by NM, 27-May-1999.)
|- 2 e. RR
Theorem	2cn 8649	The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
|- 2 e. CC
Theorem	2ex 8650	2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 2 e. _V
Theorem	2cnd 8651	2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ph -> 2 e. CC )
Theorem	3re 8652	The number 3 is real. (Contributed by NM, 27-May-1999.)
|- 3 e. RR
Theorem	3cn 8653	The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
|- 3 e. CC
Theorem	3ex 8654	3 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 3 e. _V
Theorem	4re 8655	The number 4 is real. (Contributed by NM, 27-May-1999.)
|- 4 e. RR
Theorem	4cn 8656	The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 4 e. CC
Theorem	5re 8657	The number 5 is real. (Contributed by NM, 27-May-1999.)
|- 5 e. RR
Theorem	5cn 8658	The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 5 e. CC
Theorem	6re 8659	The number 6 is real. (Contributed by NM, 27-May-1999.)
|- 6 e. RR
Theorem	6cn 8660	The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 6 e. CC
Theorem	7re 8661	The number 7 is real. (Contributed by NM, 27-May-1999.)
|- 7 e. RR
Theorem	7cn 8662	The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 7 e. CC
Theorem	8re 8663	The number 8 is real. (Contributed by NM, 27-May-1999.)
|- 8 e. RR
Theorem	8cn 8664	The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 8 e. CC
Theorem	9re 8665	The number 9 is real. (Contributed by NM, 27-May-1999.)
|- 9 e. RR
Theorem	9cn 8666	The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 9 e. CC
Theorem	0le0 8667	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 0 <_ 0
Theorem	0le2 8668	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
|- 0 <_ 2
Theorem	2pos 8669	The number 2 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 2
Theorem	2ne0 8670	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
|- 2 =/= 0
Theorem	2ap0 8671	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 2 # 0
Theorem	3pos 8672	The number 3 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 3
Theorem	3ne0 8673	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- 3 =/= 0
Theorem	3ap0 8674	The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- 3 # 0
Theorem	4pos 8675	The number 4 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 4
Theorem	4ne0 8676	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
|- 4 =/= 0
Theorem	4ap0 8677	The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- 4 # 0
Theorem	5pos 8678	The number 5 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 5
Theorem	6pos 8679	The number 6 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 6
Theorem	7pos 8680	The number 7 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 7
Theorem	8pos 8681	The number 8 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 8
Theorem	9pos 8682	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 8683	-1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- -u 1 e. CC
Theorem	neg1rr 8684	-1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
|- -u 1 e. RR
Theorem	neg1ne0 8685	-1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u 1 =/= 0
Theorem	neg1lt0 8686	-1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u 1 < 0
Theorem	neg1ap0 8687	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
|- -u 1 # 0
Theorem	negneg1e1 8688	-u -u 1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u -u 1 = 1
Theorem	1pneg1e0 8689	1 + -u 1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + -u 1 ) = 0
Theorem	0m0e0 8690	0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 0 - 0 ) = 0
Theorem	1m0e1 8691	1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 - 0 ) = 1
Theorem	0p1e1 8692	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 0 + 1 ) = 1
Theorem	fv0p1e1 8693	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 8694	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + 0 ) = 1
Theorem	1p1e2 8695	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
|- ( 1 + 1 ) = 2
Theorem	2m1e1 8696	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 8717. (Contributed by David A. Wheeler, 4-Jan-2017.)
|- ( 2 - 1 ) = 1
Theorem	1e2m1 8697	1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 1 = ( 2 - 1 )
Theorem	3m1e2 8698	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.)
|- ( 3 - 1 ) = 2
Theorem	2p2e4 8699	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 8700	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 ) )