P. 90 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8901-9000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnge1 8901	A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.)
|- ( A e. NN -> 1 <_ A )
Theorem	nnle1eq1 8902	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 8903	A positive integer is positive. (Contributed by NM, 26-Sep-1999.)
|- ( A e. NN -> 0 < A )
Theorem	nnnlt1 8904	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 8905	Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.)
|- -. 0 e. NN
Theorem	nnne0 8906	A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.)
|- ( A e. NN -> A =/= 0 )
Theorem	nnap0 8907	A positive integer is apart from zero. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( A e. NN -> A # 0 )
Theorem	nngt0i 8908	A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.)
|- A e. NN   =>    |- 0 < A
Theorem	nnap0i 8909	A positive integer is apart from zero (inference version). (Contributed by Jim Kingdon, 1-Jan-2023.)
|- A e. NN   =>    |- A # 0
Theorem	nnne0i 8910	A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.)
|- A e. NN   =>    |- A =/= 0
Theorem	nn2ge 8911*	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 8912	A positive integer is either one or greater than one. This is for NN; 0elnn 4603 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 8913	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 8914	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 8915	The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.)
|- ( N e. NN -> ( 1 / N ) e. RR )
Theorem	nnrecgt0 8916	The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.)
|- ( A e. NN -> 0 < ( 1 / A ) )
Theorem	nnsub 8917	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 8918	Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.)
|- A e. NN   &    |- B e. NN   =>    |- ( A < B <-> ( B - A ) e. NN )
Theorem	nndiv 8919*	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 8920	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 8921	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> 1 <_ A )
Theorem	nngt0d 8922	A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> 0 < A )
Theorem	nnne0d 8923	A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A =/= 0 )
Theorem	nnap0d 8924	A positive integer is apart from zero. (Contributed by Jim Kingdon, 25-Aug-2021.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A # 0 )
Theorem	nnrecred 8925	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 8926	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 8927	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 8928	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 )
4.4.3  Decimal representation of numbers The decimal representation of numbers/integers is based on the decimal digits 0 through 9 (df-0 7781 through df-9 8944), 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 7781 and df-1 7782). 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 8929	Extend class notation to include the number 2.
class 2
Syntax	c3 8930	Extend class notation to include the number 3.
class 3
Syntax	c4 8931	Extend class notation to include the number 4.
class 4
Syntax	c5 8932	Extend class notation to include the number 5.
class 5
Syntax	c6 8933	Extend class notation to include the number 6.
class 6
Syntax	c7 8934	Extend class notation to include the number 7.
class 7
Syntax	c8 8935	Extend class notation to include the number 8.
class 8
Syntax	c9 8936	Extend class notation to include the number 9.
class 9
Definition	df-2 8937	Define the number 2. (Contributed by NM, 27-May-1999.)
|- 2 = ( 1 + 1 )
Definition	df-3 8938	Define the number 3. (Contributed by NM, 27-May-1999.)
|- 3 = ( 2 + 1 )
Definition	df-4 8939	Define the number 4. (Contributed by NM, 27-May-1999.)
|- 4 = ( 3 + 1 )
Definition	df-5 8940	Define the number 5. (Contributed by NM, 27-May-1999.)
|- 5 = ( 4 + 1 )
Definition	df-6 8941	Define the number 6. (Contributed by NM, 27-May-1999.)
|- 6 = ( 5 + 1 )
Definition	df-7 8942	Define the number 7. (Contributed by NM, 27-May-1999.)
|- 7 = ( 6 + 1 )
Definition	df-8 8943	Define the number 8. (Contributed by NM, 27-May-1999.)
|- 8 = ( 7 + 1 )
Definition	df-9 8944	Define the number 9. (Contributed by NM, 27-May-1999.)
|- 9 = ( 8 + 1 )
Theorem	0ne1 8945	0 =/= 1 (common case). See aso 1ap0 8509. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 =/= 1
Theorem	1ne0 8946	1 =/= 0. See aso 1ap0 8509. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 1 =/= 0
Theorem	1m1e0 8947	( 1 - 1 ) = 0 (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 1 - 1 ) = 0
Theorem	2re 8948	The number 2 is real. (Contributed by NM, 27-May-1999.)
|- 2 e. RR
Theorem	2cn 8949	The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
|- 2 e. CC
Theorem	2ex 8950	2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 2 e. _V
Theorem	2cnd 8951	2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ph -> 2 e. CC )
Theorem	3re 8952	The number 3 is real. (Contributed by NM, 27-May-1999.)
|- 3 e. RR
Theorem	3cn 8953	The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
|- 3 e. CC
Theorem	3ex 8954	3 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 3 e. _V
Theorem	4re 8955	The number 4 is real. (Contributed by NM, 27-May-1999.)
|- 4 e. RR
Theorem	4cn 8956	The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 4 e. CC
Theorem	5re 8957	The number 5 is real. (Contributed by NM, 27-May-1999.)
|- 5 e. RR
Theorem	5cn 8958	The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 5 e. CC
Theorem	6re 8959	The number 6 is real. (Contributed by NM, 27-May-1999.)
|- 6 e. RR
Theorem	6cn 8960	The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 6 e. CC
Theorem	7re 8961	The number 7 is real. (Contributed by NM, 27-May-1999.)
|- 7 e. RR
Theorem	7cn 8962	The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 7 e. CC
Theorem	8re 8963	The number 8 is real. (Contributed by NM, 27-May-1999.)
|- 8 e. RR
Theorem	8cn 8964	The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 8 e. CC
Theorem	9re 8965	The number 9 is real. (Contributed by NM, 27-May-1999.)
|- 9 e. RR
Theorem	9cn 8966	The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 9 e. CC
Theorem	0le0 8967	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 0 <_ 0
Theorem	0le2 8968	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
|- 0 <_ 2
Theorem	2pos 8969	The number 2 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 2
Theorem	2ne0 8970	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
|- 2 =/= 0
Theorem	2ap0 8971	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 2 # 0
Theorem	3pos 8972	The number 3 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 3
Theorem	3ne0 8973	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- 3 =/= 0
Theorem	3ap0 8974	The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- 3 # 0
Theorem	4pos 8975	The number 4 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 4
Theorem	4ne0 8976	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
|- 4 =/= 0
Theorem	4ap0 8977	The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- 4 # 0
Theorem	5pos 8978	The number 5 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 5
Theorem	6pos 8979	The number 6 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 6
Theorem	7pos 8980	The number 7 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 7
Theorem	8pos 8981	The number 8 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 8
Theorem	9pos 8982	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 8983	-1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- -u 1 e. CC
Theorem	neg1rr 8984	-1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
|- -u 1 e. RR
Theorem	neg1ne0 8985	-1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u 1 =/= 0
Theorem	neg1lt0 8986	-1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u 1 < 0
Theorem	neg1ap0 8987	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
|- -u 1 # 0
Theorem	negneg1e1 8988	-u -u 1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u -u 1 = 1
Theorem	1pneg1e0 8989	1 + -u 1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + -u 1 ) = 0
Theorem	0m0e0 8990	0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 0 - 0 ) = 0
Theorem	1m0e1 8991	1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 - 0 ) = 1
Theorem	0p1e1 8992	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 0 + 1 ) = 1
Theorem	fv0p1e1 8993	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 8994	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + 0 ) = 1
Theorem	1p1e2 8995	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
|- ( 1 + 1 ) = 2
Theorem	2m1e1 8996	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 9023. (Contributed by David A. Wheeler, 4-Jan-2017.)
|- ( 2 - 1 ) = 1
Theorem	1e2m1 8997	1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 1 = ( 2 - 1 )
Theorem	3m1e2 8998	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.)
|- ( 3 - 1 ) = 2
Theorem	4m1e3 8999	4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.)
|- ( 4 - 1 ) = 3
Theorem	5m1e4 9000	5 - 1 = 4. (Contributed by AV, 6-Sep-2021.)
|- ( 5 - 1 ) = 4