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

Metamath Proof Explorer

Theorem fnn0ind

Description: Induction on the integers from 0 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 fnn0ind.1 ⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜓 ) )
fnn0ind.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
fnn0ind.3 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
fnn0ind.4 ⊢ ( 𝑥 = 𝐾 → ( 𝜑 ↔ 𝜏 ) )
fnn0ind.5 ⊢ ( 𝑁 ∈ ℕ0 → 𝜓 )
fnn0ind.6 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ∧ 𝑦 < 𝑁 ) → ( 𝜒 → 𝜃 ) )
Assertion fnn0ind ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) → 𝜏 )

Proof

Step Hyp Ref Expression
1 fnn0ind.1 ⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜓 ) )
2 fnn0ind.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3 fnn0ind.3 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
4 fnn0ind.4 ⊢ ( 𝑥 = 𝐾 → ( 𝜑 ↔ 𝜏 ) )
5 fnn0ind.5 ⊢ ( 𝑁 ∈ ℕ0 → 𝜓 )
6 fnn0ind.6 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ∧ 𝑦 < 𝑁 ) → ( 𝜒 → 𝜃 ) )
7 elnn0z ⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) )
8 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
9 0z ⊢ 0 ∈ ℤ
10 elnn0z ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )
11 10 5 sylbir ⊢ ( ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) → 𝜓 )
12 11 3adant1 ⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) → 𝜓 )
13 0re ⊢ 0 ∈ ℝ
14 zre ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℝ )
15 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
16 lelttr ⊢ ( ( 0 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → 0 < 𝑁 ) )
17 ltle ⊢ ( ( 0 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 < 𝑁 → 0 ≤ 𝑁 ) )
18 17 3adant2 ⊢ ( ( 0 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 < 𝑁 → 0 ≤ 𝑁 ) )
19 16 18 syld ⊢ ( ( 0 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → 0 ≤ 𝑁 ) )
20 13 14 15 19 mp3an3an ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → 0 ≤ 𝑁 ) )
21 20 ex ⊢ ( 𝑦 ∈ ℤ → ( 𝑁 ∈ ℤ → ( ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → 0 ≤ 𝑁 ) ) )
22 21 com23 ⊢ ( 𝑦 ∈ ℤ → ( ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( 𝑁 ∈ ℤ → 0 ≤ 𝑁 ) ) )
23 22 3impib ⊢ ( ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( 𝑁 ∈ ℤ → 0 ≤ 𝑁 ) )
24 23 impcom ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → 0 ≤ 𝑁 )
25 elnn0z ⊢ ( 𝑦 ∈ ℕ0 ↔ ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ) )
26 25 anbi1i ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑦 < 𝑁 ) ↔ ( ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ) ∧ 𝑦 < 𝑁 ) )
27 6 3expb ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑦 < 𝑁 ) ) → ( 𝜒 → 𝜃 ) )
28 10 26 27 syl2anbr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) ∧ ( ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ) ∧ 𝑦 < 𝑁 ) ) → ( 𝜒 → 𝜃 ) )
29 28 expcom ⊢ ( ( ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ) ∧ 𝑦 < 𝑁 ) → ( ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) → ( 𝜒 → 𝜃 ) ) )
30 29 3impa ⊢ ( ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) → ( 𝜒 → 𝜃 ) ) )
31 30 expd ⊢ ( ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( 𝑁 ∈ ℤ → ( 0 ≤ 𝑁 → ( 𝜒 → 𝜃 ) ) ) )
32 31 impcom ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 0 ≤ 𝑁 → ( 𝜒 → 𝜃 ) ) )
33 24 32 mpd ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 𝜒 → 𝜃 ) )
34 33 adantll ⊢ ( ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 𝜒 → 𝜃 ) )
35 1 2 3 4 12 34 fzind ⊢ ( ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) → 𝜏 )
36 9 35 mpanl1 ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) → 𝜏 )
37 36 expcom ⊢ ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → ( 𝑁 ∈ ℤ → 𝜏 ) )
38 8 37 syl5 ⊢ ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → ( 𝑁 ∈ ℕ0 → 𝜏 ) )
39 38 3expa ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) ∧ 𝐾 ≤ 𝑁 ) → ( 𝑁 ∈ ℕ0 → 𝜏 ) )
40 7 39 sylanb ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) → ( 𝑁 ∈ ℕ0 → 𝜏 ) )
41 40 impcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) ) → 𝜏 )
42 41 3impb ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) → 𝜏 )