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 φ ψ
uzind4i.2 j = k φ χ
uzind4i.3 j = k + 1 φ θ
uzind4i.4 j = N φ τ
uzind4i.5 ψ
uzind4i.6 k M χ θ
Assertion uzind4i N M τ

Proof

Step Hyp Ref Expression
1 uzind4i.1 j = M φ ψ
2 uzind4i.2 j = k φ χ
3 uzind4i.3 j = k + 1 φ θ
4 uzind4i.4 j = N φ τ
5 uzind4i.5 ψ
6 uzind4i.6 k M χ θ
7 5 a1i M ψ
8 1 2 3 4 7 6 uzind4 N M τ