Theorem uzind3

Description: Induction on the upper integers that start at an integer M . The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction step. (Contributed by NM, 26-Jul-2005)

	Ref	Expression
Hypotheses	uzind3.1	⊢ ( 𝑗 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
	uzind3.2	⊢ ( 𝑗 = 𝑚 → ( 𝜑 ↔ 𝜒 ) )
	uzind3.3	⊢ ( 𝑗 = ( 𝑚 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
	uzind3.4	⊢ ( 𝑗 = 𝑁 → ( 𝜑 ↔ 𝜏 ) )
	uzind3.5	⊢ ( 𝑀 ∈ ℤ → 𝜓 )
	uzind3.6	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑚 ∈ { 𝑘 ∈ ℤ ∣ 𝑀 ≤ 𝑘 } ) → ( 𝜒 → 𝜃 ) )
Assertion	uzind3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ { 𝑘 ∈ ℤ ∣ 𝑀 ≤ 𝑘 } ) → 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		uzind3.1	⊢ ( 𝑗 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
2		uzind3.2	⊢ ( 𝑗 = 𝑚 → ( 𝜑 ↔ 𝜒 ) )
3		uzind3.3	⊢ ( 𝑗 = ( 𝑚 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
4		uzind3.4	⊢ ( 𝑗 = 𝑁 → ( 𝜑 ↔ 𝜏 ) )
5		uzind3.5	⊢ ( 𝑀 ∈ ℤ → 𝜓 )
6		uzind3.6	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑚 ∈ { 𝑘 ∈ ℤ ∣ 𝑀 ≤ 𝑘 } ) → ( 𝜒 → 𝜃 ) )
7		breq2	⊢ ( 𝑘 = 𝑁 → ( 𝑀 ≤ 𝑘 ↔ 𝑀 ≤ 𝑁 ) )
8	7	elrab	⊢ ( 𝑁 ∈ { 𝑘 ∈ ℤ ∣ 𝑀 ≤ 𝑘 } ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
9		breq2	⊢ ( 𝑘 = 𝑚 → ( 𝑀 ≤ 𝑘 ↔ 𝑀 ≤ 𝑚 ) )
10	9	elrab	⊢ ( 𝑚 ∈ { 𝑘 ∈ ℤ ∣ 𝑀 ≤ 𝑘 } ↔ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ) )
11	10 6	sylan2br	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ) ) → ( 𝜒 → 𝜃 ) )
12	11	3impb	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ) → ( 𝜒 → 𝜃 ) )
13	1 2 3 4 5 12	uzind	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝜏 )
14	13	3expb	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) ) → 𝜏 )
15	8 14	sylan2b	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ { 𝑘 ∈ ℤ ∣ 𝑀 ≤ 𝑘 } ) → 𝜏 )