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