| Step | Hyp | Ref
| Expression |
| 1 | | bccval.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 2 | | bccval.k |
. . . 4
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
| 3 | 1, 2 | bccval 44357 |
. . 3
⊢ (𝜑 → (𝐶C𝑐𝐾) = ((𝐶 FallFac 𝐾) / (!‘𝐾))) |
| 4 | 3 | eqeq1d 2739 |
. 2
⊢ (𝜑 → ((𝐶C𝑐𝐾) = 0 ↔ ((𝐶 FallFac 𝐾) / (!‘𝐾)) = 0)) |
| 5 | | fallfaccl 16052 |
. . . 4
⊢ ((𝐶 ∈ ℂ ∧ 𝐾 ∈ ℕ0)
→ (𝐶 FallFac 𝐾) ∈
ℂ) |
| 6 | 1, 2, 5 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐶 FallFac 𝐾) ∈ ℂ) |
| 7 | | faccl 14322 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ∈
ℕ) |
| 8 | 2, 7 | syl 17 |
. . . 4
⊢ (𝜑 → (!‘𝐾) ∈ ℕ) |
| 9 | 8 | nncnd 12282 |
. . 3
⊢ (𝜑 → (!‘𝐾) ∈ ℂ) |
| 10 | | facne0 14325 |
. . . 4
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ≠
0) |
| 11 | 2, 10 | syl 17 |
. . 3
⊢ (𝜑 → (!‘𝐾) ≠ 0) |
| 12 | 6, 9, 11 | diveq0ad 12053 |
. 2
⊢ (𝜑 → (((𝐶 FallFac 𝐾) / (!‘𝐾)) = 0 ↔ (𝐶 FallFac 𝐾) = 0)) |
| 13 | | fallfacval 16045 |
. . . . 5
⊢ ((𝐶 ∈ ℂ ∧ 𝐾 ∈ ℕ0)
→ (𝐶 FallFac 𝐾) = ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘)) |
| 14 | 1, 2, 13 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐶 FallFac 𝐾) = ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘)) |
| 15 | 14 | eqeq1d 2739 |
. . 3
⊢ (𝜑 → ((𝐶 FallFac 𝐾) = 0 ↔ ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) = 0)) |
| 16 | | elfzuz3 13561 |
. . . . . . 7
⊢ (𝐶 ∈ (0...(𝐾 − 1)) → (𝐾 − 1) ∈
(ℤ≥‘𝐶)) |
| 17 | 16 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) → (𝐾 − 1) ∈
(ℤ≥‘𝐶)) |
| 18 | | nn0uz 12920 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
| 19 | | elfznn0 13660 |
. . . . . . . 8
⊢ (𝐶 ∈ (0...(𝐾 − 1)) → 𝐶 ∈
ℕ0) |
| 20 | 19 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) → 𝐶 ∈
ℕ0) |
| 21 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈
ℂ) |
| 22 | | nn0cn 12536 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
| 23 | 22 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℂ) |
| 24 | 21, 23 | subcld 11620 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ ℕ0) → (𝐶 − 𝑘) ∈ ℂ) |
| 25 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 = 𝐶) → 𝐶 ∈ ℂ) |
| 26 | | eqcom 2744 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐶 ↔ 𝐶 = 𝑘) |
| 27 | 26 | biimpi 216 |
. . . . . . . . 9
⊢ (𝑘 = 𝐶 → 𝐶 = 𝑘) |
| 28 | 27 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 = 𝐶) → 𝐶 = 𝑘) |
| 29 | 25, 28 | subeq0bd 11689 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 = 𝐶) → (𝐶 − 𝑘) = 0) |
| 30 | 18, 20, 24, 29 | fprodeq0 16011 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) ∧ (𝐾 − 1) ∈
(ℤ≥‘𝐶)) → ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) = 0) |
| 31 | 17, 30 | mpdan 687 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) → ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) = 0) |
| 32 | 31 | ex 412 |
. . . 4
⊢ (𝜑 → (𝐶 ∈ (0...(𝐾 − 1)) → ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) = 0)) |
| 33 | | fzfid 14014 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) → (0...(𝐾 − 1)) ∈ Fin) |
| 34 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝐶 ∈ ℂ) |
| 35 | | elfznn0 13660 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝐾 − 1)) → 𝑘 ∈ ℕ0) |
| 36 | 35 | nn0cnd 12589 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...(𝐾 − 1)) → 𝑘 ∈ ℂ) |
| 37 | 36 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝑘 ∈ ℂ) |
| 38 | 34, 37 | subcld 11620 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → (𝐶 − 𝑘) ∈ ℂ) |
| 39 | | nelne2 3040 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ (0...(𝐾 − 1)) ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) → 𝑘 ≠ 𝐶) |
| 40 | 39 | necomd 2996 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ (0...(𝐾 − 1)) ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) → 𝐶 ≠ 𝑘) |
| 41 | 40 | ancoms 458 |
. . . . . . . . 9
⊢ ((¬
𝐶 ∈ (0...(𝐾 − 1)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝐶 ≠ 𝑘) |
| 42 | 41 | adantll 714 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝐶 ≠ 𝑘) |
| 43 | 34, 37, 42 | subne0d 11629 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → (𝐶 − 𝑘) ≠ 0) |
| 44 | 33, 38, 43 | fprodn0 16015 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) → ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) ≠ 0) |
| 45 | 44 | ex 412 |
. . . . 5
⊢ (𝜑 → (¬ 𝐶 ∈ (0...(𝐾 − 1)) → ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) ≠ 0)) |
| 46 | 45 | necon4bd 2960 |
. . . 4
⊢ (𝜑 → (∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) = 0 → 𝐶 ∈ (0...(𝐾 − 1)))) |
| 47 | 32, 46 | impbid 212 |
. . 3
⊢ (𝜑 → (𝐶 ∈ (0...(𝐾 − 1)) ↔ ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) = 0)) |
| 48 | 15, 47 | bitr4d 282 |
. 2
⊢ (𝜑 → ((𝐶 FallFac 𝐾) = 0 ↔ 𝐶 ∈ (0...(𝐾 − 1)))) |
| 49 | 4, 12, 48 | 3bitrd 305 |
1
⊢ (𝜑 → ((𝐶C𝑐𝐾) = 0 ↔ 𝐶 ∈ (0...(𝐾 − 1)))) |