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

Proof

Step Hyp Ref Expression
1 uzind4s.1 ⊢ ( 𝑀 ∈ ℤ → [ 𝑀 / 𝑘 ] 𝜑 )
2 uzind4s.2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → [ ( 𝑘 + 1 ) / 𝑘 ] 𝜑 ) )
3 dfsbcq2 ⊢ ( 𝑗 = 𝑀 → ( [ 𝑗 / 𝑘 ] 𝜑 ↔ [ 𝑀 / 𝑘 ] 𝜑 ) )
4 sbequ ⊢ ( 𝑗 = 𝑚 → ( [ 𝑗 / 𝑘 ] 𝜑 ↔ [ 𝑚 / 𝑘 ] 𝜑 ) )
5 dfsbcq2 ⊢ ( 𝑗 = ( 𝑚 + 1 ) → ( [ 𝑗 / 𝑘 ] 𝜑 ↔ [ ( 𝑚 + 1 ) / 𝑘 ] 𝜑 ) )
6 dfsbcq2 ⊢ ( 𝑗 = 𝑁 → ( [ 𝑗 / 𝑘 ] 𝜑 ↔ [ 𝑁 / 𝑘 ] 𝜑 ) )
7 nfv ⊢ Ⅎ 𝑘 𝑚 ∈ ( ℤ≥ ‘ 𝑀 )
8 nfs1v ⊢ Ⅎ 𝑘 [ 𝑚 / 𝑘 ] 𝜑
9 nfsbc1v ⊢ Ⅎ 𝑘 [ ( 𝑚 + 1 ) / 𝑘 ] 𝜑
10 8 9 nfim ⊢ Ⅎ 𝑘 ( [ 𝑚 / 𝑘 ] 𝜑 → [ ( 𝑚 + 1 ) / 𝑘 ] 𝜑 )
11 7 10 nfim ⊢ Ⅎ 𝑘 ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) → ( [ 𝑚 / 𝑘 ] 𝜑 → [ ( 𝑚 + 1 ) / 𝑘 ] 𝜑 ) )
12 eleq1w ⊢ ( 𝑘 = 𝑚 → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
13 sbequ12 ⊢ ( 𝑘 = 𝑚 → ( 𝜑 ↔ [ 𝑚 / 𝑘 ] 𝜑 ) )
14 oveq1 ⊢ ( 𝑘 = 𝑚 → ( 𝑘 + 1 ) = ( 𝑚 + 1 ) )
15 14 sbceq1d ⊢ ( 𝑘 = 𝑚 → ( [ ( 𝑘 + 1 ) / 𝑘 ] 𝜑 ↔ [ ( 𝑚 + 1 ) / 𝑘 ] 𝜑 ) )
16 13 15 imbi12d ⊢ ( 𝑘 = 𝑚 → ( ( 𝜑 → [ ( 𝑘 + 1 ) / 𝑘 ] 𝜑 ) ↔ ( [ 𝑚 / 𝑘 ] 𝜑 → [ ( 𝑚 + 1 ) / 𝑘 ] 𝜑 ) ) )
17 12 16 imbi12d ⊢ ( 𝑘 = 𝑚 → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → [ ( 𝑘 + 1 ) / 𝑘 ] 𝜑 ) ) ↔ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) → ( [ 𝑚 / 𝑘 ] 𝜑 → [ ( 𝑚 + 1 ) / 𝑘 ] 𝜑 ) ) ) )
18 11 17 2 chvarfv ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) → ( [ 𝑚 / 𝑘 ] 𝜑 → [ ( 𝑚 + 1 ) / 𝑘 ] 𝜑 ) )
19 3 4 5 6 1 18 uzind4 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → [ 𝑁 / 𝑘 ] 𝜑 )