Proof of Theorem fnn0ind
| Step | Hyp | Ref
| Expression |
| 1 | | elnn0z 12626 |
. . . 4
⊢ (𝐾 ∈ ℕ0
↔ (𝐾 ∈ ℤ
∧ 0 ≤ 𝐾)) |
| 2 | | nn0z 12638 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
| 3 | | 0z 12624 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
| 4 | | fnn0ind.1 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝜑 ↔ 𝜓)) |
| 5 | | fnn0ind.2 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
| 6 | | fnn0ind.3 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) |
| 7 | | fnn0ind.4 |
. . . . . . . . 9
⊢ (𝑥 = 𝐾 → (𝜑 ↔ 𝜏)) |
| 8 | | elnn0z 12626 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℤ
∧ 0 ≤ 𝑁)) |
| 9 | | fnn0ind.5 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 𝜓) |
| 10 | 8, 9 | sylbir 235 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 0 ≤
𝑁) → 𝜓) |
| 11 | 10 | 3adant1 1131 |
. . . . . . . . 9
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 0 ≤ 𝑁) → 𝜓) |
| 12 | | 0re 11263 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
| 13 | | zre 12617 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℝ) |
| 14 | | zre 12617 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
| 15 | | lelttr 11351 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ ∧ 𝑦
∈ ℝ ∧ 𝑁
∈ ℝ) → ((0 ≤ 𝑦 ∧ 𝑦 < 𝑁) → 0 < 𝑁)) |
| 16 | | ltle 11349 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ ∧ 𝑁
∈ ℝ) → (0 < 𝑁 → 0 ≤ 𝑁)) |
| 17 | 16 | 3adant2 1132 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ ∧ 𝑦
∈ ℝ ∧ 𝑁
∈ ℝ) → (0 < 𝑁 → 0 ≤ 𝑁)) |
| 18 | 15, 17 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ 𝑦
∈ ℝ ∧ 𝑁
∈ ℝ) → ((0 ≤ 𝑦 ∧ 𝑦 < 𝑁) → 0 ≤ 𝑁)) |
| 19 | 12, 13, 14, 18 | mp3an3an 1469 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((0 ≤
𝑦 ∧ 𝑦 < 𝑁) → 0 ≤ 𝑁)) |
| 20 | 19 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℤ → (𝑁 ∈ ℤ → ((0 ≤
𝑦 ∧ 𝑦 < 𝑁) → 0 ≤ 𝑁))) |
| 21 | 20 | com23 86 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℤ → ((0 ≤
𝑦 ∧ 𝑦 < 𝑁) → (𝑁 ∈ ℤ → 0 ≤ 𝑁))) |
| 22 | 21 | 3impib 1117 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℤ ∧ 0 ≤
𝑦 ∧ 𝑦 < 𝑁) → (𝑁 ∈ ℤ → 0 ≤ 𝑁)) |
| 23 | 22 | impcom 407 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ (𝑦 ∈ ℤ ∧ 0 ≤
𝑦 ∧ 𝑦 < 𝑁)) → 0 ≤ 𝑁) |
| 24 | | elnn0z 12626 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ0
↔ (𝑦 ∈ ℤ
∧ 0 ≤ 𝑦)) |
| 25 | 24 | anbi1i 624 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ0
∧ 𝑦 < 𝑁) ↔ ((𝑦 ∈ ℤ ∧ 0 ≤ 𝑦) ∧ 𝑦 < 𝑁)) |
| 26 | | fnn0ind.6 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ 𝑦 ∈
ℕ0 ∧ 𝑦
< 𝑁) → (𝜒 → 𝜃)) |
| 27 | 26 | 3expb 1121 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ (𝑦 ∈
ℕ0 ∧ 𝑦
< 𝑁)) → (𝜒 → 𝜃)) |
| 28 | 8, 25, 27 | syl2anbr 599 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 0 ≤
𝑁) ∧ ((𝑦 ∈ ℤ ∧ 0 ≤
𝑦) ∧ 𝑦 < 𝑁)) → (𝜒 → 𝜃)) |
| 29 | 28 | expcom 413 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ ℤ ∧ 0 ≤
𝑦) ∧ 𝑦 < 𝑁) → ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (𝜒 → 𝜃))) |
| 30 | 29 | 3impa 1110 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℤ ∧ 0 ≤
𝑦 ∧ 𝑦 < 𝑁) → ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (𝜒 → 𝜃))) |
| 31 | 30 | expd 415 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℤ ∧ 0 ≤
𝑦 ∧ 𝑦 < 𝑁) → (𝑁 ∈ ℤ → (0 ≤ 𝑁 → (𝜒 → 𝜃)))) |
| 32 | 31 | impcom 407 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ (𝑦 ∈ ℤ ∧ 0 ≤
𝑦 ∧ 𝑦 < 𝑁)) → (0 ≤ 𝑁 → (𝜒 → 𝜃))) |
| 33 | 23, 32 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ (𝑦 ∈ ℤ ∧ 0 ≤
𝑦 ∧ 𝑦 < 𝑁)) → (𝜒 → 𝜃)) |
| 34 | 33 | adantll 714 |
. . . . . . . . 9
⊢ (((0
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ (𝑦
∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁)) → (𝜒 → 𝜃)) |
| 35 | 4, 5, 6, 7, 11, 34 | fzind 12716 |
. . . . . . . 8
⊢ (((0
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ (𝐾
∈ ℤ ∧ 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → 𝜏) |
| 36 | 3, 35 | mpanl1 700 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 0 ≤
𝐾 ∧ 𝐾 ≤ 𝑁)) → 𝜏) |
| 37 | 36 | expcom 413 |
. . . . . 6
⊢ ((𝐾 ∈ ℤ ∧ 0 ≤
𝐾 ∧ 𝐾 ≤ 𝑁) → (𝑁 ∈ ℤ → 𝜏)) |
| 38 | 2, 37 | syl5 34 |
. . . . 5
⊢ ((𝐾 ∈ ℤ ∧ 0 ≤
𝐾 ∧ 𝐾 ≤ 𝑁) → (𝑁 ∈ ℕ0 → 𝜏)) |
| 39 | 38 | 3expa 1119 |
. . . 4
⊢ (((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) ∧ 𝐾 ≤ 𝑁) → (𝑁 ∈ ℕ0 → 𝜏)) |
| 40 | 1, 39 | sylanb 581 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝐾 ≤ 𝑁) → (𝑁 ∈ ℕ0 → 𝜏)) |
| 41 | 40 | impcom 407 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐾
≤ 𝑁)) → 𝜏) |
| 42 | 41 | 3impb 1115 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝐾
≤ 𝑁) → 𝜏) |