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	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → [ 𝑁 / 𝑘 ] 𝜑 )