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

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