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	nn0ssxnn0 9201	The standard nonnegative integers are a subset of the extended nonnegative integers. (Contributed by AV, 10-Dec-2020.)
|- NN0 C_ NN0*
Theorem	nn0xnn0 9202	A standard nonnegative integer is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020.)
|- ( A e. NN0 -> A e. NN0* )
Theorem	xnn0xr 9203	An extended nonnegative integer is an extended real. (Contributed by AV, 10-Dec-2020.)
|- ( A e. NN0* -> A e. RR* )
Theorem	0xnn0 9204	Zero is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020.)
|- 0 e. NN0*
Theorem	pnf0xnn0 9205	Positive infinity is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020.)
|- +oo e. NN0*
Theorem	nn0nepnf 9206	No standard nonnegative integer equals positive infinity. (Contributed by AV, 10-Dec-2020.)
|- ( A e. NN0 -> A =/= +oo )
Theorem	nn0xnn0d 9207	A standard nonnegative integer is an extended nonnegative integer, deduction form. (Contributed by AV, 10-Dec-2020.)
|- ( ph -> A e. NN0 )   =>    |- ( ph -> A e. NN0* )
Theorem	nn0nepnfd 9208	No standard nonnegative integer equals positive infinity, deduction form. (Contributed by AV, 10-Dec-2020.)
|- ( ph -> A e. NN0 )   =>    |- ( ph -> A =/= +oo )
Theorem	xnn0nemnf 9209	No extended nonnegative integer equals negative infinity. (Contributed by AV, 10-Dec-2020.)
|- ( A e. NN0* -> A =/= -oo )
Theorem	xnn0xrnemnf 9210	The extended nonnegative integers are extended reals without negative infinity. (Contributed by AV, 10-Dec-2020.)
|- ( A e. NN0* -> ( A e. RR* /\ A =/= -oo ) )
Theorem	xnn0nnn0pnf 9211	An extended nonnegative integer which is not a standard nonnegative integer is positive infinity. (Contributed by AV, 10-Dec-2020.)
|- ( ( N e. NN0* /\ -. N e. NN0 ) -> N = +oo )
4.4.9  Integers (as a subset of complex numbers)
Syntax	cz 9212	Extend class notation to include the class of integers.
class ZZ
Definition	df-z 9213	Define the set of integers, which are the positive and negative integers together with zero. Definition of integers in [Apostol] p. 22. The letter Z abbreviates the German word Zahlen meaning "numbers." (Contributed by NM, 8-Jan-2002.)
|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
Theorem	elz 9214	Membership in the set of integers. (Contributed by NM, 8-Jan-2002.)
|- ( N e. ZZ <-> ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) )
Theorem	nnnegz 9215	The negative of a positive integer is an integer. (Contributed by NM, 12-Jan-2002.)
|- ( N e. NN -> -u N e. ZZ )
Theorem	zre 9216	An integer is a real. (Contributed by NM, 8-Jan-2002.)
|- ( N e. ZZ -> N e. RR )
Theorem	zcn 9217	An integer is a complex number. (Contributed by NM, 9-May-2004.)
|- ( N e. ZZ -> N e. CC )
Theorem	zrei 9218	An integer is a real number. (Contributed by NM, 14-Jul-2005.)
|- A e. ZZ   =>    |- A e. RR
Theorem	zssre 9219	The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.)
|- ZZ C_ RR
Theorem	zsscn 9220	The integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
|- ZZ C_ CC
Theorem	zex 9221	The set of integers exists. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ZZ e. _V
Theorem	elnnz 9222	Positive integer property expressed in terms of integers. (Contributed by NM, 8-Jan-2002.)
|- ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
Theorem	0z 9223	Zero is an integer. (Contributed by NM, 12-Jan-2002.)
|- 0 e. ZZ
Theorem	0zd 9224	Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ph -> 0 e. ZZ )
Theorem	elnn0z 9225	Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004.)
|- ( N e. NN0 <-> ( N e. ZZ /\ 0 <_ N ) )
Theorem	elznn0nn 9226	Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004.)
|- ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
Theorem	elznn0 9227	Integer property expressed in terms of nonnegative integers. (Contributed by NM, 9-May-2004.)
|- ( N e. ZZ <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) )
Theorem	elznn 9228	Integer property expressed in terms of positive integers and nonnegative integers. (Contributed by NM, 12-Jul-2005.)
|- ( N e. ZZ <-> ( N e. RR /\ ( N e. NN \/ -u N e. NN0 ) ) )
Theorem	nnssz 9229	Positive integers are a subset of integers. (Contributed by NM, 9-Jan-2002.)
|- NN C_ ZZ
Theorem	nn0ssz 9230	Nonnegative integers are a subset of the integers. (Contributed by NM, 9-May-2004.)
|- NN0 C_ ZZ
Theorem	nnz 9231	A positive integer is an integer. (Contributed by NM, 9-May-2004.)
|- ( N e. NN -> N e. ZZ )
Theorem	nn0z 9232	A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
|- ( N e. NN0 -> N e. ZZ )
Theorem	nnzi 9233	A positive integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- N e. NN   =>    |- N e. ZZ
Theorem	nn0zi 9234	A nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- N e. NN0   =>    |- N e. ZZ
Theorem	elnnz1 9235	Positive integer property expressed in terms of integers. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|- ( N e. NN <-> ( N e. ZZ /\ 1 <_ N ) )
Theorem	nnzrab 9236	Positive integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.)
|- NN = { x e. ZZ | 1 <_ x }
Theorem	nn0zrab 9237	Nonnegative integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.)
|- NN0 = { x e. ZZ | 0 <_ x }
Theorem	1z 9238	One is an integer. (Contributed by NM, 10-May-2004.)
|- 1 e. ZZ
Theorem	1zzd 9239	1 is an integer, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 1 e. ZZ )
Theorem	2z 9240	Two is an integer. (Contributed by NM, 10-May-2004.)
|- 2 e. ZZ
Theorem	3z 9241	3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 3 e. ZZ
Theorem	4z 9242	4 is an integer. (Contributed by BJ, 26-Mar-2020.)
|- 4 e. ZZ
Theorem	znegcl 9243	Closure law for negative integers. (Contributed by NM, 9-May-2004.)
|- ( N e. ZZ -> -u N e. ZZ )
Theorem	neg1z 9244	-1 is an integer (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
|- -u 1 e. ZZ
Theorem	znegclb 9245	A number is an integer iff its negative is. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( A e. CC -> ( A e. ZZ <-> -u A e. ZZ ) )
Theorem	nn0negz 9246	The negative of a nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
|- ( N e. NN0 -> -u N e. ZZ )
Theorem	nn0negzi 9247	The negative of a nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- N e. NN0   =>    |- -u N e. ZZ
Theorem	peano2z 9248	Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005.)
|- ( N e. ZZ -> ( N + 1 ) e. ZZ )
Theorem	zaddcllempos 9249	Lemma for zaddcl 9252. Special case in which N is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- ( ( M e. ZZ /\ N e. NN ) -> ( M + N ) e. ZZ )
Theorem	peano2zm 9250	"Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005.)
|- ( N e. ZZ -> ( N - 1 ) e. ZZ )
Theorem	zaddcllemneg 9251	Lemma for zaddcl 9252. Special case in which -u N is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- ( ( M e. ZZ /\ N e. RR /\ -u N e. NN ) -> ( M + N ) e. ZZ )
Theorem	zaddcl 9252	Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )
Theorem	zsubcl 9253	Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M - N ) e. ZZ )
Theorem	ztri3or0 9254	Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.)
|- ( N e. ZZ -> ( N < 0 \/ N = 0 \/ 0 < N ) )
Theorem	ztri3or 9255	Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N \/ M = N \/ N < M ) )
Theorem	zletric 9256	Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A <_ B \/ B <_ A ) )
Theorem	zlelttric 9257	Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A <_ B \/ B < A ) )
Theorem	zltnle 9258	'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A < B <-> -. B <_ A ) )
Theorem	zleloe 9259	Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
Theorem	znnnlt1 9260	An integer is not a positive integer iff it is less than one. (Contributed by NM, 13-Jul-2005.)
|- ( N e. ZZ -> ( -. N e. NN <-> N < 1 ) )
Theorem	zletr 9261	Transitive law of ordering for integers. (Contributed by Alexander van der Vekens, 3-Apr-2018.)
|- ( ( J e. ZZ /\ K e. ZZ /\ L e. ZZ ) -> ( ( J <_ K /\ K <_ L ) -> J <_ L ) )
Theorem	zrevaddcl 9262	Reverse closure law for addition of integers. (Contributed by NM, 11-May-2004.)
|- ( N e. ZZ -> ( ( M e. CC /\ ( M + N ) e. ZZ ) <-> M e. ZZ ) )
Theorem	znnsub 9263	The positive difference of unequal integers is a positive integer. (Generalization of nnsub 8917.) (Contributed by NM, 11-May-2004.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( N - M ) e. NN ) )
Theorem	nzadd 9264	The sum of a real number not being an integer and an integer is not an integer. Note that "not being an integer" in this case means "the negation of is an integer" rather than "is apart from any integer" (given excluded middle, those two would be equivalent). (Contributed by AV, 19-Jul-2021.)
|- ( ( A e. ( RR \ ZZ ) /\ B e. ZZ ) -> ( A + B ) e. ( RR \ ZZ ) )
Theorem	zmulcl 9265	Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )
Theorem	zltp1le 9266	Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( M + 1 ) <_ N ) )
Theorem	zleltp1 9267	Integer ordering relation. (Contributed by NM, 10-May-2004.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> M < ( N + 1 ) ) )
Theorem	zlem1lt 9268	Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( M - 1 ) < N ) )
Theorem	zltlem1 9269	Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> M <_ ( N - 1 ) ) )
Theorem	zgt0ge1 9270	An integer greater than 0 is greater than or equal to 1. (Contributed by AV, 14-Oct-2018.)
|- ( Z e. ZZ -> ( 0 < Z <-> 1 <_ Z ) )
Theorem	nnleltp1 9271	Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|- ( ( A e. NN /\ B e. NN ) -> ( A <_ B <-> A < ( B + 1 ) ) )
Theorem	nnltp1le 9272	Positive integer ordering relation. (Contributed by NM, 19-Aug-2001.)
|- ( ( A e. NN /\ B e. NN ) -> ( A < B <-> ( A + 1 ) <_ B ) )
Theorem	nnaddm1cl 9273	Closure of addition of positive integers minus one. (Contributed by NM, 6-Aug-2003.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|- ( ( A e. NN /\ B e. NN ) -> ( ( A + B ) - 1 ) e. NN )
Theorem	nn0ltp1le 9274	Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M < N <-> ( M + 1 ) <_ N ) )
Theorem	nn0leltp1 9275	Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-2004.)
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M <_ N <-> M < ( N + 1 ) ) )
Theorem	nn0ltlem1 9276	Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M < N <-> M <_ ( N - 1 ) ) )
Theorem	znn0sub 9277	The nonnegative difference of integers is a nonnegative integer. (Generalization of nn0sub 9278.) (Contributed by NM, 14-Jul-2005.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( N - M ) e. NN0 ) )
Theorem	nn0sub 9278	Subtraction of nonnegative integers. (Contributed by NM, 9-May-2004.)
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M <_ N <-> ( N - M ) e. NN0 ) )
Theorem	ltsubnn0 9279	Subtracting a nonnegative integer from a nonnegative integer which is greater than the first one results in a nonnegative integer. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( B < A -> ( A - B ) e. NN0 ) )
Theorem	nn0negleid 9280	A nonnegative integer is greater than or equal to its negative. (Contributed by AV, 13-Aug-2021.)
|- ( A e. NN0 -> -u A <_ A )
Theorem	difgtsumgt 9281	If the difference of a real number and a nonnegative integer is greater than another real number, the sum of the real number and the nonnegative integer is also greater than the other real number. (Contributed by AV, 13-Aug-2021.)
|- ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> ( C < ( A - B ) -> C < ( A + B ) ) )
Theorem	nn0n0n1ge2 9282	A nonnegative integer which is neither 0 nor 1 is greater than or equal to 2. (Contributed by Alexander van der Vekens, 6-Dec-2017.)
|- ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> 2 <_ N )
Theorem	elz2 9283*	Membership in the set of integers. Commonly used in constructions of the integers as equivalence classes under subtraction of the positive integers. (Contributed by Mario Carneiro, 16-May-2014.)
|- ( N e. ZZ <-> E. x e. NN E. y e. NN N = ( x - y ) )
Theorem	dfz2 9284	Alternate definition of the integers, based on elz2 9283. (Contributed by Mario Carneiro, 16-May-2014.)
|- ZZ = ( - " ( NN X. NN ) )
Theorem	nn0sub2 9285	Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005.)
|- ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( N - M ) e. NN0 )
Theorem	zapne 9286	Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M # N <-> M =/= N ) )
Theorem	zdceq 9287	Equality of integers is decidable. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> DECID A = B )
Theorem	zdcle 9288	Integer <_ is decidable. (Contributed by Jim Kingdon, 7-Apr-2020.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> DECID A <_ B )
Theorem	zdclt 9289	Integer < is decidable. (Contributed by Jim Kingdon, 1-Jun-2020.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> DECID A < B )
Theorem	zltlen 9290	Integer 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 8551 which is a similar result for real numbers. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A < B <-> ( A <_ B /\ B =/= A ) ) )
Theorem	nn0n0n1ge2b 9291	A nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by Alexander van der Vekens, 17-Jan-2018.)
|- ( N e. NN0 -> ( ( N =/= 0 /\ N =/= 1 ) <-> 2 <_ N ) )
Theorem	nn0lt10b 9292	A nonnegative integer less than 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( N e. NN0 -> ( N < 1 <-> N = 0 ) )
Theorem	nn0lt2 9293	A nonnegative integer less than 2 must be 0 or 1. (Contributed by Alexander van der Vekens, 16-Sep-2018.)
|- ( ( N e. NN0 /\ N < 2 ) -> ( N = 0 \/ N = 1 ) )
Theorem	nn0le2is012 9294	A nonnegative integer which is less than or equal to 2 is either 0 or 1 or 2. (Contributed by AV, 16-Mar-2019.)
|- ( ( N e. NN0 /\ N <_ 2 ) -> ( N = 0 \/ N = 1 \/ N = 2 ) )
Theorem	nn0lem1lt 9295	Nonnegative integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M <_ N <-> ( M - 1 ) < N ) )
Theorem	nnlem1lt 9296	Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|- ( ( M e. NN /\ N e. NN ) -> ( M <_ N <-> ( M - 1 ) < N ) )
Theorem	nnltlem1 9297	Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|- ( ( M e. NN /\ N e. NN ) -> ( M < N <-> M <_ ( N - 1 ) ) )
Theorem	nnm1ge0 9298	A positive integer decreased by 1 is greater than or equal to 0. (Contributed by AV, 30-Oct-2018.)
|- ( N e. NN -> 0 <_ ( N - 1 ) )
Theorem	nn0ge0div 9299	Division of a nonnegative integer by a positive number is not negative. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
|- ( ( K e. NN0 /\ L e. NN ) -> 0 <_ ( K / L ) )
Theorem	zdiv 9300*	Two ways to express " M divides N. (Contributed by NM, 3-Oct-2008.)
|- ( ( M e. NN /\ N e. ZZ ) -> ( E. k e. ZZ ( M x. k ) = N <-> ( N / M ) e. ZZ ) )