Metamath Proof Explorer


Theorem uzind4ALT

Description: 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 or uzind4ALT may be used; see comment for nnind . (Contributed by NM, 7-Sep-2005) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses uzind4ALT.5
|- ( M e. ZZ -> ps )
uzind4ALT.6
|- ( k e. ( ZZ>= ` M ) -> ( ch -> th ) )
uzind4ALT.1
|- ( j = M -> ( ph <-> ps ) )
uzind4ALT.2
|- ( j = k -> ( ph <-> ch ) )
uzind4ALT.3
|- ( j = ( k + 1 ) -> ( ph <-> th ) )
uzind4ALT.4
|- ( j = N -> ( ph <-> ta ) )
Assertion uzind4ALT
|- ( N e. ( ZZ>= ` M ) -> ta )

Proof

Step Hyp Ref Expression
1 uzind4ALT.5
 |-  ( M e. ZZ -> ps )
2 uzind4ALT.6
 |-  ( k e. ( ZZ>= ` M ) -> ( ch -> th ) )
3 uzind4ALT.1
 |-  ( j = M -> ( ph <-> ps ) )
4 uzind4ALT.2
 |-  ( j = k -> ( ph <-> ch ) )
5 uzind4ALT.3
 |-  ( j = ( k + 1 ) -> ( ph <-> th ) )
6 uzind4ALT.4
 |-  ( j = N -> ( ph <-> ta ) )
7 3 4 5 6 1 2 uzind4
 |-  ( N e. ( ZZ>= ` M ) -> ta )