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 ⊢ ( 𝑀 ∈ ℤ → [ 𝑀 / 𝑗 ] 𝜑 )
uzind4s2.2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( [ 𝑘 / 𝑗 ] 𝜑 → [ ( 𝑘 + 1 ) / 𝑗 ] 𝜑 ) )
Assertion uzind4s2 ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → [ 𝑁 / 𝑗 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 uzind4s2.1 ⊢ ( 𝑀 ∈ ℤ → [ 𝑀 / 𝑗 ] 𝜑 )
2 uzind4s2.2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( [ 𝑘 / 𝑗 ] 𝜑 → [ ( 𝑘 + 1 ) / 𝑗 ] 𝜑 ) )
3 dfsbcq ⊢ ( 𝑚 = 𝑀 → ( [ 𝑚 / 𝑗 ] 𝜑 ↔ [ 𝑀 / 𝑗 ] 𝜑 ) )
4 dfsbcq ⊢ ( 𝑚 = 𝑛 → ( [ 𝑚 / 𝑗 ] 𝜑 ↔ [ 𝑛 / 𝑗 ] 𝜑 ) )
5 dfsbcq ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( [ 𝑚 / 𝑗 ] 𝜑 ↔ [ ( 𝑛 + 1 ) / 𝑗 ] 𝜑 ) )
6 dfsbcq ⊢ ( 𝑚 = 𝑁 → ( [ 𝑚 / 𝑗 ] 𝜑 ↔ [ 𝑁 / 𝑗 ] 𝜑 ) )
7 dfsbcq ⊢ ( 𝑘 = 𝑛 → ( [ 𝑘 / 𝑗 ] 𝜑 ↔ [ 𝑛 / 𝑗 ] 𝜑 ) )
8 oveq1 ⊢ ( 𝑘 = 𝑛 → ( 𝑘 + 1 ) = ( 𝑛 + 1 ) )
9 8 sbceq1d ⊢ ( 𝑘 = 𝑛 → ( [ ( 𝑘 + 1 ) / 𝑗 ] 𝜑 ↔ [ ( 𝑛 + 1 ) / 𝑗 ] 𝜑 ) )
10 7 9 imbi12d ⊢ ( 𝑘 = 𝑛 → ( ( [ 𝑘 / 𝑗 ] 𝜑 → [ ( 𝑘 + 1 ) / 𝑗 ] 𝜑 ) ↔ ( [ 𝑛 / 𝑗 ] 𝜑 → [ ( 𝑛 + 1 ) / 𝑗 ] 𝜑 ) ) )
11 10 2 vtoclga ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( [ 𝑛 / 𝑗 ] 𝜑 → [ ( 𝑛 + 1 ) / 𝑗 ] 𝜑 ) )
12 3 4 5 6 1 11 uzind4 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → [ 𝑁 / 𝑗 ] 𝜑 )