Metamath Proof Explorer


Theorem fzind

Description: Induction on the integers from M to N inclusive . The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Hypotheses fzind.1 ( 𝑥 = 𝑀 → ( 𝜑𝜓 ) )
fzind.2 ( 𝑥 = 𝑦 → ( 𝜑𝜒 ) )
fzind.3 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑𝜃 ) )
fzind.4 ( 𝑥 = 𝐾 → ( 𝜑𝜏 ) )
fzind.5 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁 ) → 𝜓 )
fzind.6 ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑀𝑦𝑦 < 𝑁 ) ) → ( 𝜒𝜃 ) )
Assertion fzind ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀𝐾𝐾𝑁 ) ) → 𝜏 )

Proof

Step Hyp Ref Expression
1 fzind.1 ( 𝑥 = 𝑀 → ( 𝜑𝜓 ) )
2 fzind.2 ( 𝑥 = 𝑦 → ( 𝜑𝜒 ) )
3 fzind.3 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑𝜃 ) )
4 fzind.4 ( 𝑥 = 𝐾 → ( 𝜑𝜏 ) )
5 fzind.5 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁 ) → 𝜓 )
6 fzind.6 ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑀𝑦𝑦 < 𝑁 ) ) → ( 𝜒𝜃 ) )
7 breq1 ( 𝑥 = 𝑀 → ( 𝑥𝑁𝑀𝑁 ) )
8 7 anbi2d ( 𝑥 = 𝑀 → ( ( 𝑁 ∈ ℤ ∧ 𝑥𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀𝑁 ) ) )
9 8 1 imbi12d ( 𝑥 = 𝑀 → ( ( ( 𝑁 ∈ ℤ ∧ 𝑥𝑁 ) → 𝜑 ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝑀𝑁 ) → 𝜓 ) ) )
10 breq1 ( 𝑥 = 𝑦 → ( 𝑥𝑁𝑦𝑁 ) )
11 10 anbi2d ( 𝑥 = 𝑦 → ( ( 𝑁 ∈ ℤ ∧ 𝑥𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑦𝑁 ) ) )
12 11 2 imbi12d ( 𝑥 = 𝑦 → ( ( ( 𝑁 ∈ ℤ ∧ 𝑥𝑁 ) → 𝜑 ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝑦𝑁 ) → 𝜒 ) ) )
13 breq1 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥𝑁 ↔ ( 𝑦 + 1 ) ≤ 𝑁 ) )
14 13 anbi2d ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑁 ∈ ℤ ∧ 𝑥𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) ) )
15 14 3 imbi12d ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑁 ∈ ℤ ∧ 𝑥𝑁 ) → 𝜑 ) ↔ ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜃 ) ) )
16 breq1 ( 𝑥 = 𝐾 → ( 𝑥𝑁𝐾𝑁 ) )
17 16 anbi2d ( 𝑥 = 𝐾 → ( ( 𝑁 ∈ ℤ ∧ 𝑥𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝐾𝑁 ) ) )
18 17 4 imbi12d ( 𝑥 = 𝐾 → ( ( ( 𝑁 ∈ ℤ ∧ 𝑥𝑁 ) → 𝜑 ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝐾𝑁 ) → 𝜏 ) ) )
19 5 3expib ( 𝑀 ∈ ℤ → ( ( 𝑁 ∈ ℤ ∧ 𝑀𝑁 ) → 𝜓 ) )
20 zre ( 𝑦 ∈ ℤ → 𝑦 ∈ ℝ )
21 zre ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
22 p1le ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝑦𝑁 )
23 22 3expia ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑦 + 1 ) ≤ 𝑁𝑦𝑁 ) )
24 20 21 23 syl2an ( ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑦 + 1 ) ≤ 𝑁𝑦𝑁 ) )
25 24 imdistanda ( 𝑦 ∈ ℤ → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝑁 ∈ ℤ ∧ 𝑦𝑁 ) ) )
26 25 imim1d ( 𝑦 ∈ ℤ → ( ( ( 𝑁 ∈ ℤ ∧ 𝑦𝑁 ) → 𝜒 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜒 ) ) )
27 26 3ad2ant2 ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) → ( ( ( 𝑁 ∈ ℤ ∧ 𝑦𝑁 ) → 𝜒 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜒 ) ) )
28 zltp1le ( ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑦 < 𝑁 ↔ ( 𝑦 + 1 ) ≤ 𝑁 ) )
29 28 adantlr ( ( ( 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑦 < 𝑁 ↔ ( 𝑦 + 1 ) ≤ 𝑁 ) )
30 29 expcom ( 𝑁 ∈ ℤ → ( ( 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) → ( 𝑦 < 𝑁 ↔ ( 𝑦 + 1 ) ≤ 𝑁 ) ) )
31 30 pm5.32d ( 𝑁 ∈ ℤ → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) ∧ 𝑦 < 𝑁 ) ↔ ( ( 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) ) )
32 31 adantl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) ∧ 𝑦 < 𝑁 ) ↔ ( ( 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) ) )
33 6 expcom ( ( 𝑦 ∈ ℤ ∧ 𝑀𝑦𝑦 < 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝜒𝜃 ) ) )
34 33 3expa ( ( ( 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) ∧ 𝑦 < 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝜒𝜃 ) ) )
35 34 com12 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) ∧ 𝑦 < 𝑁 ) → ( 𝜒𝜃 ) ) )
36 32 35 sylbird ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝜒𝜃 ) ) )
37 36 ex ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝜒𝜃 ) ) ) )
38 37 com23 ( 𝑀 ∈ ℤ → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝑁 ∈ ℤ → ( 𝜒𝜃 ) ) ) )
39 38 expd ( 𝑀 ∈ ℤ → ( ( 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) → ( ( 𝑦 + 1 ) ≤ 𝑁 → ( 𝑁 ∈ ℤ → ( 𝜒𝜃 ) ) ) ) )
40 39 3impib ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) → ( ( 𝑦 + 1 ) ≤ 𝑁 → ( 𝑁 ∈ ℤ → ( 𝜒𝜃 ) ) ) )
41 40 impcomd ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝜒𝜃 ) ) )
42 41 a2d ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) → ( ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜒 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜃 ) ) )
43 27 42 syld ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀𝑦 ) → ( ( ( 𝑁 ∈ ℤ ∧ 𝑦𝑁 ) → 𝜒 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜃 ) ) )
44 9 12 15 18 19 43 uzind ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀𝐾 ) → ( ( 𝑁 ∈ ℤ ∧ 𝐾𝑁 ) → 𝜏 ) )
45 44 expcomd ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀𝐾 ) → ( 𝐾𝑁 → ( 𝑁 ∈ ℤ → 𝜏 ) ) )
46 45 3expb ( ( 𝑀 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝑀𝐾 ) ) → ( 𝐾𝑁 → ( 𝑁 ∈ ℤ → 𝜏 ) ) )
47 46 expcom ( ( 𝐾 ∈ ℤ ∧ 𝑀𝐾 ) → ( 𝑀 ∈ ℤ → ( 𝐾𝑁 → ( 𝑁 ∈ ℤ → 𝜏 ) ) ) )
48 47 com23 ( ( 𝐾 ∈ ℤ ∧ 𝑀𝐾 ) → ( 𝐾𝑁 → ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → 𝜏 ) ) ) )
49 48 3impia ( ( 𝐾 ∈ ℤ ∧ 𝑀𝐾𝐾𝑁 ) → ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → 𝜏 ) ) )
50 49 impd ( ( 𝐾 ∈ ℤ ∧ 𝑀𝐾𝐾𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝜏 ) )
51 50 impcom ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀𝐾𝐾𝑁 ) ) → 𝜏 )