| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . 5
⊢ (𝑚 = 0 → (𝑚C𝑘) = (0C𝑘)) |
| 2 | 1 | eleq1d 2826 |
. . . 4
⊢ (𝑚 = 0 → ((𝑚C𝑘) ∈ ℕ0 ↔ (0C𝑘) ∈
ℕ0)) |
| 3 | 2 | ralbidv 3178 |
. . 3
⊢ (𝑚 = 0 → (∀𝑘 ∈ ℤ (𝑚C𝑘) ∈ ℕ0 ↔
∀𝑘 ∈ ℤ
(0C𝑘) ∈
ℕ0)) |
| 4 | | oveq1 7438 |
. . . . 5
⊢ (𝑚 = 𝑛 → (𝑚C𝑘) = (𝑛C𝑘)) |
| 5 | 4 | eleq1d 2826 |
. . . 4
⊢ (𝑚 = 𝑛 → ((𝑚C𝑘) ∈ ℕ0 ↔ (𝑛C𝑘) ∈
ℕ0)) |
| 6 | 5 | ralbidv 3178 |
. . 3
⊢ (𝑚 = 𝑛 → (∀𝑘 ∈ ℤ (𝑚C𝑘) ∈ ℕ0 ↔
∀𝑘 ∈ ℤ
(𝑛C𝑘) ∈
ℕ0)) |
| 7 | | oveq1 7438 |
. . . . 5
⊢ (𝑚 = (𝑛 + 1) → (𝑚C𝑘) = ((𝑛 + 1)C𝑘)) |
| 8 | 7 | eleq1d 2826 |
. . . 4
⊢ (𝑚 = (𝑛 + 1) → ((𝑚C𝑘) ∈ ℕ0 ↔ ((𝑛 + 1)C𝑘) ∈
ℕ0)) |
| 9 | 8 | ralbidv 3178 |
. . 3
⊢ (𝑚 = (𝑛 + 1) → (∀𝑘 ∈ ℤ (𝑚C𝑘) ∈ ℕ0 ↔
∀𝑘 ∈ ℤ
((𝑛 + 1)C𝑘) ∈
ℕ0)) |
| 10 | | oveq1 7438 |
. . . . 5
⊢ (𝑚 = 𝑁 → (𝑚C𝑘) = (𝑁C𝑘)) |
| 11 | 10 | eleq1d 2826 |
. . . 4
⊢ (𝑚 = 𝑁 → ((𝑚C𝑘) ∈ ℕ0 ↔ (𝑁C𝑘) ∈
ℕ0)) |
| 12 | 11 | ralbidv 3178 |
. . 3
⊢ (𝑚 = 𝑁 → (∀𝑘 ∈ ℤ (𝑚C𝑘) ∈ ℕ0 ↔
∀𝑘 ∈ ℤ
(𝑁C𝑘) ∈
ℕ0)) |
| 13 | | elfz1eq 13575 |
. . . . . . 7
⊢ (𝑘 ∈ (0...0) → 𝑘 = 0) |
| 14 | 13 | adantl 481 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 𝑘 ∈ (0...0)) → 𝑘 = 0) |
| 15 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑘 = 0 → (0C𝑘) = (0C0)) |
| 16 | | 0nn0 12541 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
| 17 | | bcn0 14349 |
. . . . . . . . 9
⊢ (0 ∈
ℕ0 → (0C0) = 1) |
| 18 | 16, 17 | ax-mp 5 |
. . . . . . . 8
⊢ (0C0) =
1 |
| 19 | | 1nn0 12542 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
| 20 | 18, 19 | eqeltri 2837 |
. . . . . . 7
⊢ (0C0)
∈ ℕ0 |
| 21 | 15, 20 | eqeltrdi 2849 |
. . . . . 6
⊢ (𝑘 = 0 → (0C𝑘) ∈
ℕ0) |
| 22 | 14, 21 | syl 17 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 𝑘 ∈ (0...0)) → (0C𝑘) ∈
ℕ0) |
| 23 | | bcval3 14345 |
. . . . . . 7
⊢ ((0
∈ ℕ0 ∧ 𝑘 ∈ ℤ ∧ ¬ 𝑘 ∈ (0...0)) → (0C𝑘) = 0) |
| 24 | 16, 23 | mp3an1 1450 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
(0C𝑘) = 0) |
| 25 | 24, 16 | eqeltrdi 2849 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
(0C𝑘) ∈
ℕ0) |
| 26 | 22, 25 | pm2.61dan 813 |
. . . 4
⊢ (𝑘 ∈ ℤ → (0C𝑘) ∈
ℕ0) |
| 27 | 26 | rgen 3063 |
. . 3
⊢
∀𝑘 ∈
ℤ (0C𝑘) ∈
ℕ0 |
| 28 | | oveq2 7439 |
. . . . . 6
⊢ (𝑘 = 𝑚 → (𝑛C𝑘) = (𝑛C𝑚)) |
| 29 | 28 | eleq1d 2826 |
. . . . 5
⊢ (𝑘 = 𝑚 → ((𝑛C𝑘) ∈ ℕ0 ↔ (𝑛C𝑚) ∈
ℕ0)) |
| 30 | 29 | cbvralvw 3237 |
. . . 4
⊢
(∀𝑘 ∈
ℤ (𝑛C𝑘) ∈ ℕ0
↔ ∀𝑚 ∈
ℤ (𝑛C𝑚) ∈
ℕ0) |
| 31 | | bcpasc 14360 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ ((𝑛C𝑘) + (𝑛C(𝑘 − 1))) = ((𝑛 + 1)C𝑘)) |
| 32 | 31 | adantlr 715 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ0
∧ ∀𝑚 ∈
ℤ (𝑛C𝑚) ∈ ℕ0)
∧ 𝑘 ∈ ℤ)
→ ((𝑛C𝑘) + (𝑛C(𝑘 − 1))) = ((𝑛 + 1)C𝑘)) |
| 33 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → (𝑛C𝑚) = (𝑛C𝑘)) |
| 34 | 33 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑘 → ((𝑛C𝑚) ∈ ℕ0 ↔ (𝑛C𝑘) ∈
ℕ0)) |
| 35 | 34 | rspccva 3621 |
. . . . . . . . 9
⊢
((∀𝑚 ∈
ℤ (𝑛C𝑚) ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑛C𝑘) ∈
ℕ0) |
| 36 | | peano2zm 12660 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈
ℤ) |
| 37 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑘 − 1) → (𝑛C𝑚) = (𝑛C(𝑘 − 1))) |
| 38 | 37 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑘 − 1) → ((𝑛C𝑚) ∈ ℕ0 ↔ (𝑛C(𝑘 − 1)) ∈
ℕ0)) |
| 39 | 38 | rspccva 3621 |
. . . . . . . . . 10
⊢
((∀𝑚 ∈
ℤ (𝑛C𝑚) ∈ ℕ0
∧ (𝑘 − 1) ∈
ℤ) → (𝑛C(𝑘 − 1)) ∈
ℕ0) |
| 40 | 36, 39 | sylan2 593 |
. . . . . . . . 9
⊢
((∀𝑚 ∈
ℤ (𝑛C𝑚) ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑛C(𝑘 − 1)) ∈
ℕ0) |
| 41 | 35, 40 | nn0addcld 12591 |
. . . . . . . 8
⊢
((∀𝑚 ∈
ℤ (𝑛C𝑚) ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ ((𝑛C𝑘) + (𝑛C(𝑘 − 1))) ∈
ℕ0) |
| 42 | 41 | adantll 714 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ0
∧ ∀𝑚 ∈
ℤ (𝑛C𝑚) ∈ ℕ0)
∧ 𝑘 ∈ ℤ)
→ ((𝑛C𝑘) + (𝑛C(𝑘 − 1))) ∈
ℕ0) |
| 43 | 32, 42 | eqeltrrd 2842 |
. . . . . 6
⊢ (((𝑛 ∈ ℕ0
∧ ∀𝑚 ∈
ℤ (𝑛C𝑚) ∈ ℕ0)
∧ 𝑘 ∈ ℤ)
→ ((𝑛 + 1)C𝑘) ∈
ℕ0) |
| 44 | 43 | ralrimiva 3146 |
. . . . 5
⊢ ((𝑛 ∈ ℕ0
∧ ∀𝑚 ∈
ℤ (𝑛C𝑚) ∈ ℕ0)
→ ∀𝑘 ∈
ℤ ((𝑛 + 1)C𝑘) ∈
ℕ0) |
| 45 | 44 | ex 412 |
. . . 4
⊢ (𝑛 ∈ ℕ0
→ (∀𝑚 ∈
ℤ (𝑛C𝑚) ∈ ℕ0
→ ∀𝑘 ∈
ℤ ((𝑛 + 1)C𝑘) ∈
ℕ0)) |
| 46 | 30, 45 | biimtrid 242 |
. . 3
⊢ (𝑛 ∈ ℕ0
→ (∀𝑘 ∈
ℤ (𝑛C𝑘) ∈ ℕ0
→ ∀𝑘 ∈
ℤ ((𝑛 + 1)C𝑘) ∈
ℕ0)) |
| 47 | 3, 6, 9, 12, 27, 46 | nn0ind 12713 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ∀𝑘 ∈
ℤ (𝑁C𝑘) ∈
ℕ0) |
| 48 | | oveq2 7439 |
. . . 4
⊢ (𝑘 = 𝐾 → (𝑁C𝑘) = (𝑁C𝐾)) |
| 49 | 48 | eleq1d 2826 |
. . 3
⊢ (𝑘 = 𝐾 → ((𝑁C𝑘) ∈ ℕ0 ↔ (𝑁C𝐾) ∈
ℕ0)) |
| 50 | 49 | rspccva 3621 |
. 2
⊢
((∀𝑘 ∈
ℤ (𝑁C𝑘) ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ (𝑁C𝐾) ∈
ℕ0) |
| 51 | 47, 50 | sylan 580 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ (𝑁C𝐾) ∈
ℕ0) |