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

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 ∈ ℤ → ψ
uzind4ALT.6 ⊢ k ∈ ℤ ≥ M → χ → θ
uzind4ALT.1 ⊢ j = M → φ ↔ ψ
uzind4ALT.2 ⊢ j = k → φ ↔ χ
uzind4ALT.3 ⊢ j = k + 1 → φ ↔ θ
uzind4ALT.4 ⊢ j = N → φ ↔ τ
Assertion uzind4ALT ⊢ N ∈ ℤ ≥ M → τ

Proof

Step Hyp Ref Expression
1 uzind4ALT.5 ⊢ M ∈ ℤ → ψ
2 uzind4ALT.6 ⊢ k ∈ ℤ ≥ M → χ → θ
3 uzind4ALT.1 ⊢ j = M → φ ↔ ψ
4 uzind4ALT.2 ⊢ j = k → φ ↔ χ
5 uzind4ALT.3 ⊢ j = k + 1 → φ ↔ θ
6 uzind4ALT.4 ⊢ j = N → φ ↔ τ
7 3 4 5 6 1 2 uzind4 ⊢ N ∈ ℤ ≥ M → τ