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

Metamath Proof Explorer

Theorem uzind4ALT

Description: Induction on the upper set of integers that starts at an integer M . The last four hypotheses give us the substitution instances we need; the first two are the basis and the induction step. Either uzind4 or uzind4ALT may be used; see comment for nnind . (Contributed by NM, 7-Sep-2005) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

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