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

Metamath Proof Explorer

Theorem uzind4s2

Description: Induction on the upper set of integers that starts at an integer M , using explicit substitution. The hypotheses are the basis and the induction step. Use this instead of uzind4s when j and k must be distinct in [. ( k + 1 ) / j ]. ph . (Contributed by NM, 16-Nov-2005)

Ref Expression
Hypotheses uzind4s2.1 ⊢ M ∈ ℤ → [˙M / j]˙ φ
uzind4s2.2 ⊢ k ∈ ℤ ≥ M → [˙k / j]˙ φ → [˙k + 1 / j]˙ φ
Assertion uzind4s2 ⊢ N ∈ ℤ ≥ M → [˙N / j]˙ φ

Proof

Step Hyp Ref Expression
1 uzind4s2.1 ⊢ M ∈ ℤ → [˙M / j]˙ φ
2 uzind4s2.2 ⊢ k ∈ ℤ ≥ M → [˙k / j]˙ φ → [˙k + 1 / j]˙ φ
3 dfsbcq ⊢ m = M → [˙m / j]˙ φ ↔ [˙M / j]˙ φ
4 dfsbcq ⊢ m = n → [˙m / j]˙ φ ↔ [˙n / j]˙ φ
5 dfsbcq ⊢ m = n + 1 → [˙m / j]˙ φ ↔ [˙n + 1 / j]˙ φ
6 dfsbcq ⊢ m = N → [˙m / j]˙ φ ↔ [˙N / j]˙ φ
7 dfsbcq ⊢ k = n → [˙k / j]˙ φ ↔ [˙n / j]˙ φ
8 oveq1 ⊢ k = n → k + 1 = n + 1
9 8 sbceq1d ⊢ k = n → [˙k + 1 / j]˙ φ ↔ [˙n + 1 / j]˙ φ
10 7 9 imbi12d ⊢ k = n → [˙k / j]˙ φ → [˙k + 1 / j]˙ φ ↔ [˙n / j]˙ φ → [˙n + 1 / j]˙ φ
11 10 2 vtoclga ⊢ n ∈ ℤ ≥ M → [˙n / j]˙ φ → [˙n + 1 / j]˙ φ
12 3 4 5 6 1 11 uzind4 ⊢ N ∈ ℤ ≥ M → [˙N / j]˙ φ