This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 → τ