Metamath Proof Explorer


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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ { 𝑘 ∈ ℤ ∣ 𝑀𝑘 } ) → 𝜏 )