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 ) |
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 ) |