P. 98 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9701-9800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	7t6e42 9701	7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 x. 6 ) = ; 4 2
Theorem	7t7e49 9702	7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 x. 7 ) = ; 4 9
Theorem	8t2e16 9703	8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 x. 2 ) = ; 1 6
Theorem	8t3e24 9704	8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 x. 3 ) = ; 2 4
Theorem	8t4e32 9705	8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 x. 4 ) = ; 3 2
Theorem	8t5e40 9706	8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 8 x. 5 ) = ; 4 0
Theorem	8t6e48 9707	8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 8 x. 6 ) = ; 4 8
Theorem	8t7e56 9708	8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 x. 7 ) = ; 5 6
Theorem	8t8e64 9709	8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 x. 8 ) = ; 6 4
Theorem	9t2e18 9710	9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 2 ) = ; 1 8
Theorem	9t3e27 9711	9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 3 ) = ; 2 7
Theorem	9t4e36 9712	9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 4 ) = ; 3 6
Theorem	9t5e45 9713	9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 5 ) = ; 4 5
Theorem	9t6e54 9714	9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 6 ) = ; 5 4
Theorem	9t7e63 9715	9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 7 ) = ; 6 3
Theorem	9t8e72 9716	9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 8 ) = ; 7 2
Theorem	9t9e81 9717	9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 9 ) = ; 8 1
Theorem	9t11e99 9718	9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.)
|- ( 9 x. ; 1 1 ) = ; 9 9
Theorem	9lt10 9719	9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.)
|- 9 < ; 1 0
Theorem	8lt10 9720	8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.)
|- 8 < ; 1 0
Theorem	7lt10 9721	7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|- 7 < ; 1 0
Theorem	6lt10 9722	6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|- 6 < ; 1 0
Theorem	5lt10 9723	5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|- 5 < ; 1 0
Theorem	4lt10 9724	4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|- 4 < ; 1 0
Theorem	3lt10 9725	3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|- 3 < ; 1 0
Theorem	2lt10 9726	2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|- 2 < ; 1 0
Theorem	1lt10 9727	1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario Carneiro, 9-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|- 1 < ; 1 0
Theorem	decbin0 9728	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- A e. NN0   =>    |- ( 4 x. A ) = ( 2 x. ( 2 x. A ) )
Theorem	decbin2 9729	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- A e. NN0   =>    |- ( ( 4 x. A ) + 2 ) = ( 2 x. ( ( 2 x. A ) + 1 ) )
Theorem	decbin3 9730	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- A e. NN0   =>    |- ( ( 4 x. A ) + 3 ) = ( ( 2 x. ( ( 2 x. A ) + 1 ) ) + 1 )
Theorem	halfthird 9731	Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.)
|- ( ( 1 / 2 ) - ( 1 / 3 ) ) = ( 1 / 6 )
Theorem	5recm6rec 9732	One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.)
|- ( ( 1 / 5 ) - ( 1 / 6 ) ) = ( 1 / ; 3 0 )
4.4.11  Upper sets of integers
Syntax	cuz 9733	Extend class notation with the upper integer function. Read " ZZ>= ` M " as "the set of integers greater than or equal to M".
class ZZ>=
Definition	df-uz 9734*	Define a function whose value at j is the semi-infinite set of contiguous integers starting at j, which we will also call the upper integers starting at j. Read " ZZ>= ` M " as "the set of integers greater than or equal to M". See uzval 9735 for its value, uzssz 9754 for its relationship to ZZ, nnuz 9770 and nn0uz 9769 for its relationships to NN and NN0, and eluz1 9737 and eluz2 9739 for its membership relations. (Contributed by NM, 5-Sep-2005.)
|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
Theorem	uzval 9735*	The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( N e. ZZ -> ( ZZ>= ` N ) = { k e. ZZ | N <_ k } )
Theorem	uzf 9736	The domain and codomain of the upper integers function. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ZZ>= : ZZ --> ~P ZZ
Theorem	eluz1 9737	Membership in the upper set of integers starting at M. (Contributed by NM, 5-Sep-2005.)
|- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) )
Theorem	eluzel2 9738	Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
Theorem	eluz2 9739	Membership in an upper set of integers. We use the fact that a function's value (under our function value definition) is empty outside of its domain to show M e. ZZ. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
Theorem	eluzmn 9740	Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- ( ( M e. ZZ /\ N e. NN0 ) -> M e. ( ZZ>= ` ( M - N ) ) )
Theorem	eluz1i 9741	Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005.)
|- M e. ZZ   =>    |- ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) )
Theorem	eluzuzle 9742	An integer in an upper set of integers is an element of an upper set of integers with a smaller bound. (Contributed by Alexander van der Vekens, 17-Jun-2018.)
|- ( ( B e. ZZ /\ B <_ A ) -> ( C e. ( ZZ>= ` A ) -> C e. ( ZZ>= ` B ) ) )
Theorem	eluzelz 9743	A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)
|- ( N e. ( ZZ>= ` M ) -> N e. ZZ )
Theorem	eluzelre 9744	A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013.)
|- ( N e. ( ZZ>= ` M ) -> N e. RR )
Theorem	eluzelcn 9745	A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- ( N e. ( ZZ>= ` M ) -> N e. CC )
Theorem	eluzle 9746	Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.)
|- ( N e. ( ZZ>= ` M ) -> M <_ N )
Theorem	eluz 9747	Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) <-> M <_ N ) )
Theorem	uzid 9748	Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.)
|- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
Theorem	uzidd 9749	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   =>    |- ( ph -> M e. ( ZZ>= ` M ) )
Theorem	uzn0 9750	The upper integers are all nonempty. (Contributed by Mario Carneiro, 16-Jan-2014.)
|- ( M e. ran ZZ>= -> M =/= (/) )
Theorem	uztrn 9751	Transitive law for sets of upper integers. (Contributed by NM, 20-Sep-2005.)
|- ( ( M e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` N ) ) -> M e. ( ZZ>= ` N ) )
Theorem	uztrn2 9752	Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013.)
|- Z = ( ZZ>= ` K )   =>    |- ( ( N e. Z /\ M e. ( ZZ>= ` N ) ) -> M e. Z )
Theorem	uzneg 9753	Contraposition law for upper integers. (Contributed by NM, 28-Nov-2005.)
|- ( N e. ( ZZ>= ` M ) -> -u M e. ( ZZ>= ` -u N ) )
Theorem	uzssz 9754	An upper set of integers is a subset of all integers. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ZZ>= ` M ) C_ ZZ
Theorem	uzss 9755	Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005.)
|- ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
Theorem	uztric 9756	Trichotomy of the ordering relation on integers, stated in terms of upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 25-Jun-2013.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) \/ M e. ( ZZ>= ` N ) ) )
Theorem	uz11 9757	The upper integers function is one-to-one. (Contributed by NM, 12-Dec-2005.)
|- ( M e. ZZ -> ( ( ZZ>= ` M ) = ( ZZ>= ` N ) <-> M = N ) )
Theorem	eluzp1m1 9758	Membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.)
|- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
Theorem	eluzp1l 9759	Strict ordering implied by membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.)
|- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> M < N )
Theorem	eluzp1p1 9760	Membership in the next upper set of integers. (Contributed by NM, 5-Oct-2005.)
|- ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
Theorem	eluzaddi 9761	Membership in a later upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.)
|- M e. ZZ   &    |- K e. ZZ   =>    |- ( N e. ( ZZ>= ` M ) -> ( N + K ) e. ( ZZ>= ` ( M + K ) ) )
Theorem	eluzsubi 9762	Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.)
|- M e. ZZ   &    |- K e. ZZ   =>    |- ( N e. ( ZZ>= ` ( M + K ) ) -> ( N - K ) e. ( ZZ>= ` M ) )
Theorem	eluzadd 9763	Membership in a later upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) -> ( N + K ) e. ( ZZ>= ` ( M + K ) ) )
Theorem	eluzsub 9764	Membership in an earlier upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) ) -> ( N - K ) e. ( ZZ>= ` M ) )
Theorem	uzm1 9765	Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( N e. ( ZZ>= ` M ) -> ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) )
Theorem	uznn0sub 9766	The nonnegative difference of integers is a nonnegative integer. (Contributed by NM, 4-Sep-2005.)
|- ( N e. ( ZZ>= ` M ) -> ( N - M ) e. NN0 )
Theorem	uzin 9767	Intersection of two upper intervals of integers. (Contributed by Mario Carneiro, 24-Dec-2013.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ZZ>= ` M ) i^i ( ZZ>= ` N ) ) = ( ZZ>= ` if ( M <_ N , N , M ) ) )
Theorem	uzp1 9768	Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( N e. ( ZZ>= ` M ) -> ( N = M \/ N e. ( ZZ>= ` ( M + 1 ) ) ) )
Theorem	nn0uz 9769	Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
|- NN0 = ( ZZ>= ` 0 )
Theorem	nnuz 9770	Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
|- NN = ( ZZ>= ` 1 )
Theorem	elnnuz 9771	A positive integer expressed as a member of an upper set of integers. (Contributed by NM, 6-Jun-2006.)
|- ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
Theorem	elnn0uz 9772	A nonnegative integer expressed as a member an upper set of integers. (Contributed by NM, 6-Jun-2006.)
|- ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
Theorem	eluz2nn 9773	An integer is greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018.)
|- ( A e. ( ZZ>= ` 2 ) -> A e. NN )
Theorem	eluz4eluz2 9774	An integer greater than or equal to 4 is an integer greater than or equal to 2. (Contributed by AV, 30-May-2023.)
|- ( X e. ( ZZ>= ` 4 ) -> X e. ( ZZ>= ` 2 ) )
Theorem	eluz4nn 9775	An integer greater than or equal to 4 is a positive integer. (Contributed by AV, 30-May-2023.)
|- ( X e. ( ZZ>= ` 4 ) -> X e. NN )
Theorem	eluzge2nn0 9776	If an integer is greater than or equal to 2, then it is a nonnegative integer. (Contributed by AV, 27-Aug-2018.) (Proof shortened by AV, 3-Nov-2018.)
|- ( N e. ( ZZ>= ` 2 ) -> N e. NN0 )
Theorem	eluz2n0 9777	An integer greater than or equal to 2 is not 0. (Contributed by AV, 25-May-2020.)
|- ( N e. ( ZZ>= ` 2 ) -> N =/= 0 )
Theorem	uzuzle23 9778	An integer in the upper set of integers starting at 3 is element of the upper set of integers starting at 2. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
|- ( A e. ( ZZ>= ` 3 ) -> A e. ( ZZ>= ` 2 ) )
Theorem	eluzge3nn 9779	If an integer is greater than 3, then it is a positive integer. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
|- ( N e. ( ZZ>= ` 3 ) -> N e. NN )
Theorem	uz3m2nn 9780	An integer greater than or equal to 3 decreased by 2 is a positive integer. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
|- ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. NN )
Theorem	1eluzge0 9781	1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
|- 1 e. ( ZZ>= ` 0 )
Theorem	2eluzge0 9782	2 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- 2 e. ( ZZ>= ` 0 )
Theorem	2eluzge1 9783	2 is an integer greater than or equal to 1. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
|- 2 e. ( ZZ>= ` 1 )
Theorem	uznnssnn 9784	The upper integers starting from a natural are a subset of the naturals. (Contributed by Scott Fenton, 29-Jun-2013.)
|- ( N e. NN -> ( ZZ>= ` N ) C_ NN )
Theorem	raluz 9785*	Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
|- ( M e. ZZ -> ( A. n e. ( ZZ>= ` M ) ph <-> A. n e. ZZ ( M <_ n -> ph ) ) )
Theorem	raluz2 9786*	Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
|- ( A. n e. ( ZZ>= ` M ) ph <-> ( M e. ZZ -> A. n e. ZZ ( M <_ n -> ph ) ) )
Theorem	rexuz 9787*	Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
|- ( M e. ZZ -> ( E. n e. ( ZZ>= ` M ) ph <-> E. n e. ZZ ( M <_ n /\ ph ) ) )
Theorem	rexuz2 9788*	Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.)
|- ( E. n e. ( ZZ>= ` M ) ph <-> ( M e. ZZ /\ E. n e. ZZ ( M <_ n /\ ph ) ) )
Theorem	2rexuz 9789*	Double existential quantification in an upper set of integers. (Contributed by NM, 3-Nov-2005.)
|- ( E. m E. n e. ( ZZ>= ` m ) ph <-> E. m e. ZZ E. n e. ZZ ( m <_ n /\ ph ) )
Theorem	peano2uz 9790	Second Peano postulate for an upper set of integers. (Contributed by NM, 7-Sep-2005.)
|- ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
Theorem	peano2uzs 9791	Second Peano postulate for an upper set of integers. (Contributed by Mario Carneiro, 26-Dec-2013.)
|- Z = ( ZZ>= ` M )   =>    |- ( N e. Z -> ( N + 1 ) e. Z )
Theorem	peano2uzr 9792	Reversed second Peano axiom for upper integers. (Contributed by NM, 2-Jan-2006.)
|- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> N e. ( ZZ>= ` M ) )
Theorem	uzaddcl 9793	Addition closure law for an upper set of integers. (Contributed by NM, 4-Jun-2006.)
|- ( ( N e. ( ZZ>= ` M ) /\ K e. NN0 ) -> ( N + K ) e. ( ZZ>= ` M ) )
Theorem	nn0pzuz 9794	The sum of a nonnegative integer and an integer is an integer greater than or equal to that integer. (Contributed by Alexander van der Vekens, 3-Oct-2018.)
|- ( ( N e. NN0 /\ Z e. ZZ ) -> ( N + Z ) e. ( ZZ>= ` Z ) )
Theorem	uzind4 9795*	Induction on the upper set of integers that starts at an integer M. The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction step. (Contributed by NM, 7-Sep-2005.)
|- ( j = M -> ( ph <-> ps ) )   &    |- ( j = k -> ( ph <-> ch ) )   &    |- ( j = ( k + 1 ) -> ( ph <-> th ) )   &    |- ( j = N -> ( ph <-> ta ) )   &    |- ( M e. ZZ -> ps )   &    |- ( k e. ( ZZ>= ` M ) -> ( ch -> th ) )   =>    |- ( N e. ( ZZ>= ` M ) -> ta )
Theorem	uzind4ALT 9796*	Induction on the upper set of integers that starts at an integer M. The last four hypotheses give us the substitution instances we need; the first two are the basis and the induction step. Either uzind4 9795 or uzind4ALT 9796 may be used; see comment for nnind 9137. (Contributed by NM, 7-Sep-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( M e. ZZ -> ps )   &    |- ( k e. ( ZZ>= ` M ) -> ( ch -> th ) )   &    |- ( j = M -> ( ph <-> ps ) )   &    |- ( j = k -> ( ph <-> ch ) )   &    |- ( j = ( k + 1 ) -> ( ph <-> th ) )   &    |- ( j = N -> ( ph <-> ta ) )   =>    |- ( N e. ( ZZ>= ` M ) -> ta )
Theorem	uzind4s 9797*	Induction on the upper set of integers that starts at an integer M, using explicit substitution. The hypotheses are the basis and the induction step. (Contributed by NM, 4-Nov-2005.)
|- ( M e. ZZ -> [. M / k ]. ph )   &    |- ( k e. ( ZZ>= ` M ) -> ( ph -> [. ( k + 1 ) / k ]. ph ) )   =>    |- ( N e. ( ZZ>= ` M ) -> [. N / k ]. ph )
Theorem	uzind4s2 9798*	Induction on the upper set of integers that starts at an integer M, using explicit substitution. The hypotheses are the basis and the induction step. Use this instead of uzind4s 9797 when j and k must be distinct in [. ( k + 1 ) / j ]. ph. (Contributed by NM, 16-Nov-2005.)
|- ( M e. ZZ -> [. M / j ]. ph )   &    |- ( k e. ( ZZ>= ` M ) -> ( [. k / j ]. ph -> [. ( k + 1 ) / j ]. ph ) )   =>    |- ( N e. ( ZZ>= ` M ) -> [. N / j ]. ph )
Theorem	uzind4i 9799*	Induction on the upper integers that start at M. The first four give us the substitution instances we need, and the last two are the basis and the induction step. This is a stronger version of uzind4 9795 assuming that ps holds unconditionally. Notice that N e. ( ZZ>= ` M ) implies that the lower bound M is an integer ( M e. ZZ, see eluzel2 9738). (Contributed by NM, 4-Sep-2005.) (Revised by AV, 13-Jul-2022.)
|- ( j = M -> ( ph <-> ps ) )   &    |- ( j = k -> ( ph <-> ch ) )   &    |- ( j = ( k + 1 ) -> ( ph <-> th ) )   &    |- ( j = N -> ( ph <-> ta ) )   &    |- ps   &    |- ( k e. ( ZZ>= ` M ) -> ( ch -> th ) )   =>    |- ( N e. ( ZZ>= ` M ) -> ta )
Theorem	indstr 9800*	Strong Mathematical Induction for positive integers (inference schema). (Contributed by NM, 17-Aug-2001.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( x e. NN -> ( A. y e. NN ( y < x -> ps ) -> ph ) )   =>    |- ( x e. NN -> ph )