# Metamath Proof Explorer

## Theorem uzind4i

Description: 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 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 ). (Contributed by NM, 4-Sep-2005) (Revised by AV, 13-Jul-2022)

Ref Expression
Hypotheses uzind4i.1 ${⊢}{j}={M}\to \left({\phi }↔{\psi }\right)$
uzind4i.2 ${⊢}{j}={k}\to \left({\phi }↔{\chi }\right)$
uzind4i.3 ${⊢}{j}={k}+1\to \left({\phi }↔{\theta }\right)$
uzind4i.4 ${⊢}{j}={N}\to \left({\phi }↔{\tau }\right)$
uzind4i.5 ${⊢}{\psi }$
uzind4i.6 ${⊢}{k}\in {ℤ}_{\ge {M}}\to \left({\chi }\to {\theta }\right)$
Assertion uzind4i ${⊢}{N}\in {ℤ}_{\ge {M}}\to {\tau }$

### Proof

Step Hyp Ref Expression
1 uzind4i.1 ${⊢}{j}={M}\to \left({\phi }↔{\psi }\right)$
2 uzind4i.2 ${⊢}{j}={k}\to \left({\phi }↔{\chi }\right)$
3 uzind4i.3 ${⊢}{j}={k}+1\to \left({\phi }↔{\theta }\right)$
4 uzind4i.4 ${⊢}{j}={N}\to \left({\phi }↔{\tau }\right)$
5 uzind4i.5 ${⊢}{\psi }$
6 uzind4i.6 ${⊢}{k}\in {ℤ}_{\ge {M}}\to \left({\chi }\to {\theta }\right)$
7 5 a1i ${⊢}{M}\in ℤ\to {\psi }$
8 1 2 3 4 7 6 uzind4 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {\tau }$