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

Metamath Proof Explorer

Theorem uzind4s

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. (Contributed by NM, 4-Nov-2005)

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

Proof

Step Hyp Ref Expression
1 uzind4s.1 ⊢ M ∈ ℤ → [˙M / k]˙ φ
2 uzind4s.2 ⊢ k ∈ ℤ ≥ M → φ → [˙k + 1 / k]˙ φ
3 dfsbcq2 ⊢ j = M → j k φ ↔ [˙M / k]˙ φ
4 sbequ ⊢ j = m → j k φ ↔ m k φ
5 dfsbcq2 ⊢ j = m + 1 → j k φ ↔ [˙m + 1 / k]˙ φ
6 dfsbcq2 ⊢ j = N → j k φ ↔ [˙N / k]˙ φ
7 nfv ⊢ Ⅎ k m ∈ ℤ ≥ M
8 nfs1v ⊢ Ⅎ k m k φ
9 nfsbc1v ⊢ Ⅎ k [˙m + 1 / k]˙ φ
10 8 9 nfim ⊢ Ⅎ k m k φ → [˙m + 1 / k]˙ φ
11 7 10 nfim ⊢ Ⅎ k m ∈ ℤ ≥ M → m k φ → [˙m + 1 / k]˙ φ
12 eleq1w ⊢ k = m → k ∈ ℤ ≥ M ↔ m ∈ ℤ ≥ M
13 sbequ12 ⊢ k = m → φ ↔ m k φ
14 oveq1 ⊢ k = m → k + 1 = m + 1
15 14 sbceq1d ⊢ k = m → [˙k + 1 / k]˙ φ ↔ [˙m + 1 / k]˙ φ
16 13 15 imbi12d ⊢ k = m → φ → [˙k + 1 / k]˙ φ ↔ m k φ → [˙m + 1 / k]˙ φ
17 12 16 imbi12d ⊢ k = m → k ∈ ℤ ≥ M → φ → [˙k + 1 / k]˙ φ ↔ m ∈ ℤ ≥ M → m k φ → [˙m + 1 / k]˙ φ
18 11 17 2 chvarfv ⊢ m ∈ ℤ ≥ M → m k φ → [˙m + 1 / k]˙ φ
19 3 4 5 6 1 18 uzind4 ⊢ N ∈ ℤ ≥ M → [˙N / k]˙ φ