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

Metamath Proof Explorer

Theorem uzind2

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

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

Proof

Step Hyp Ref Expression
1 uzind2.1 ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( 𝜑 ↔ 𝜓 ) )
2 uzind2.2 ⊢ ( 𝑗 = 𝑘 → ( 𝜑 ↔ 𝜒 ) )
3 uzind2.3 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
4 uzind2.4 ⊢ ( 𝑗 = 𝑁 → ( 𝜑 ↔ 𝜏 ) )
5 uzind2.5 ⊢ ( 𝑀 ∈ ℤ → 𝜓 )
6 uzind2.6 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 < 𝑘 ) → ( 𝜒 → 𝜃 ) )
7 zltp1le ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑀 + 1 ) ≤ 𝑁 ) )
8 peano2z ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 + 1 ) ∈ ℤ )
9 1 imbi2d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( ( 𝑀 ∈ ℤ → 𝜑 ) ↔ ( 𝑀 ∈ ℤ → 𝜓 ) ) )
10 2 imbi2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑀 ∈ ℤ → 𝜑 ) ↔ ( 𝑀 ∈ ℤ → 𝜒 ) ) )
11 3 imbi2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑀 ∈ ℤ → 𝜑 ) ↔ ( 𝑀 ∈ ℤ → 𝜃 ) ) )
12 4 imbi2d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑀 ∈ ℤ → 𝜑 ) ↔ ( 𝑀 ∈ ℤ → 𝜏 ) ) )
13 5 a1i ⊢ ( ( 𝑀 + 1 ) ∈ ℤ → ( 𝑀 ∈ ℤ → 𝜓 ) )
14 zltp1le ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑀 < 𝑘 ↔ ( 𝑀 + 1 ) ≤ 𝑘 ) )
15 6 3expia ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑀 < 𝑘 → ( 𝜒 → 𝜃 ) ) )
16 14 15 sylbird ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀 + 1 ) ≤ 𝑘 → ( 𝜒 → 𝜃 ) ) )
17 16 ex ⊢ ( 𝑀 ∈ ℤ → ( 𝑘 ∈ ℤ → ( ( 𝑀 + 1 ) ≤ 𝑘 → ( 𝜒 → 𝜃 ) ) ) )
18 17 com3l ⊢ ( 𝑘 ∈ ℤ → ( ( 𝑀 + 1 ) ≤ 𝑘 → ( 𝑀 ∈ ℤ → ( 𝜒 → 𝜃 ) ) ) )
19 18 imp ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑘 ) → ( 𝑀 ∈ ℤ → ( 𝜒 → 𝜃 ) ) )
20 19 3adant1 ⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑘 ) → ( 𝑀 ∈ ℤ → ( 𝜒 → 𝜃 ) ) )
21 20 a2d ⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑘 ) → ( ( 𝑀 ∈ ℤ → 𝜒 ) → ( 𝑀 ∈ ℤ → 𝜃 ) ) )
22 9 10 11 12 13 21 uzind ⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) → ( 𝑀 ∈ ℤ → 𝜏 ) )
23 22 3exp ⊢ ( ( 𝑀 + 1 ) ∈ ℤ → ( 𝑁 ∈ ℤ → ( ( 𝑀 + 1 ) ≤ 𝑁 → ( 𝑀 ∈ ℤ → 𝜏 ) ) ) )
24 8 23 syl ⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → ( ( 𝑀 + 1 ) ≤ 𝑁 → ( 𝑀 ∈ ℤ → 𝜏 ) ) ) )
25 24 com34 ⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) ≤ 𝑁 → 𝜏 ) ) ) )
26 25 pm2.43a ⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → ( ( 𝑀 + 1 ) ≤ 𝑁 → 𝜏 ) ) )
27 26 imp ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 + 1 ) ≤ 𝑁 → 𝜏 ) )
28 7 27 sylbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 → 𝜏 ) )
29 28 3impia ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → 𝜏 )