Theorem uzind4i

Description: Induction on the upper integers that start at M . The first four give us the substitution instances we need, and the last two are the basis and the induction step. This is a stronger version of uzind4 assuming that ps holds unconditionally. Notice that N e. ( ZZ>=M ) implies that the lower bound M is an integer ( M e. ZZ , see eluzel2 ). (Contributed by NM, 4-Sep-2005) (Revised by AV, 13-Jul-2022)

	Ref	Expression
Hypotheses	uzind4i.1	⊢ ( 𝑗 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
	uzind4i.2	⊢ ( 𝑗 = 𝑘 → ( 𝜑 ↔ 𝜒 ) )
	uzind4i.3	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
	uzind4i.4	⊢ ( 𝑗 = 𝑁 → ( 𝜑 ↔ 𝜏 ) )
	uzind4i.5	⊢ 𝜓
	uzind4i.6	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜒 → 𝜃 ) )
Assertion	uzind4i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		uzind4i.1	⊢ ( 𝑗 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
2		uzind4i.2	⊢ ( 𝑗 = 𝑘 → ( 𝜑 ↔ 𝜒 ) )
3		uzind4i.3	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
4		uzind4i.4	⊢ ( 𝑗 = 𝑁 → ( 𝜑 ↔ 𝜏 ) )
5		uzind4i.5	⊢ 𝜓
6		uzind4i.6	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜒 → 𝜃 ) )
7	5	a1i	⊢ ( 𝑀 ∈ ℤ → 𝜓 )
8	1 2 3 4 7 6	uzind4	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝜏 )