Step | Hyp | Ref
| Expression |
1 | | bccval.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℂ) |
2 | | bccval.k |
. . . 4
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
3 | 1, 2 | bccval 41478 |
. . 3
⊢ (𝜑 → (𝐶C𝑐𝐾) = ((𝐶 FallFac 𝐾) / (!‘𝐾))) |
4 | 3 | eqeq1d 2740 |
. 2
⊢ (𝜑 → ((𝐶C𝑐𝐾) = 0 ↔ ((𝐶 FallFac 𝐾) / (!‘𝐾)) = 0)) |
5 | | fallfaccl 15455 |
. . . 4
⊢ ((𝐶 ∈ ℂ ∧ 𝐾 ∈ ℕ0)
→ (𝐶 FallFac 𝐾) ∈
ℂ) |
6 | 1, 2, 5 | syl2anc 587 |
. . 3
⊢ (𝜑 → (𝐶 FallFac 𝐾) ∈ ℂ) |
7 | | faccl 13728 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ∈
ℕ) |
8 | 2, 7 | syl 17 |
. . . 4
⊢ (𝜑 → (!‘𝐾) ∈ ℕ) |
9 | 8 | nncnd 11725 |
. . 3
⊢ (𝜑 → (!‘𝐾) ∈ ℂ) |
10 | | facne0 13731 |
. . . 4
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ≠
0) |
11 | 2, 10 | syl 17 |
. . 3
⊢ (𝜑 → (!‘𝐾) ≠ 0) |
12 | 6, 9, 11 | diveq0ad 11497 |
. 2
⊢ (𝜑 → (((𝐶 FallFac 𝐾) / (!‘𝐾)) = 0 ↔ (𝐶 FallFac 𝐾) = 0)) |
13 | | fallfacval 15448 |
. . . . 5
⊢ ((𝐶 ∈ ℂ ∧ 𝐾 ∈ ℕ0)
→ (𝐶 FallFac 𝐾) = ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘)) |
14 | 1, 2, 13 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝐶 FallFac 𝐾) = ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘)) |
15 | 14 | eqeq1d 2740 |
. . 3
⊢ (𝜑 → ((𝐶 FallFac 𝐾) = 0 ↔ ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) = 0)) |
16 | | elfzuz3 12988 |
. . . . . . 7
⊢ (𝐶 ∈ (0...(𝐾 − 1)) → (𝐾 − 1) ∈
(ℤ≥‘𝐶)) |
17 | 16 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) → (𝐾 − 1) ∈
(ℤ≥‘𝐶)) |
18 | | nn0uz 12355 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
19 | | elfznn0 13084 |
. . . . . . . 8
⊢ (𝐶 ∈ (0...(𝐾 − 1)) → 𝐶 ∈
ℕ0) |
20 | 19 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) → 𝐶 ∈
ℕ0) |
21 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈
ℂ) |
22 | | nn0cn 11979 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
23 | 22 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℂ) |
24 | 21, 23 | subcld 11068 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ ℕ0) → (𝐶 − 𝑘) ∈ ℂ) |
25 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 = 𝐶) → 𝐶 ∈ ℂ) |
26 | | eqcom 2745 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐶 ↔ 𝐶 = 𝑘) |
27 | 26 | biimpi 219 |
. . . . . . . . 9
⊢ (𝑘 = 𝐶 → 𝐶 = 𝑘) |
28 | 27 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 = 𝐶) → 𝐶 = 𝑘) |
29 | 25, 28 | subeq0bd 11137 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 = 𝐶) → (𝐶 − 𝑘) = 0) |
30 | 18, 20, 24, 29 | fprodeq0 15414 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) ∧ (𝐾 − 1) ∈
(ℤ≥‘𝐶)) → ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) = 0) |
31 | 17, 30 | mpdan 687 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ (0...(𝐾 − 1))) → ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) = 0) |
32 | 31 | ex 416 |
. . . 4
⊢ (𝜑 → (𝐶 ∈ (0...(𝐾 − 1)) → ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) = 0)) |
33 | | fzfid 13425 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) → (0...(𝐾 − 1)) ∈ Fin) |
34 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝐶 ∈ ℂ) |
35 | | elfznn0 13084 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝐾 − 1)) → 𝑘 ∈ ℕ0) |
36 | 35 | nn0cnd 12031 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...(𝐾 − 1)) → 𝑘 ∈ ℂ) |
37 | 36 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝑘 ∈ ℂ) |
38 | 34, 37 | subcld 11068 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → (𝐶 − 𝑘) ∈ ℂ) |
39 | | nelne2 3031 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ (0...(𝐾 − 1)) ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) → 𝑘 ≠ 𝐶) |
40 | 39 | necomd 2989 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ (0...(𝐾 − 1)) ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) → 𝐶 ≠ 𝑘) |
41 | 40 | ancoms 462 |
. . . . . . . . 9
⊢ ((¬
𝐶 ∈ (0...(𝐾 − 1)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝐶 ≠ 𝑘) |
42 | 41 | adantll 714 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝐶 ≠ 𝑘) |
43 | 34, 37, 42 | subne0d 11077 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → (𝐶 − 𝑘) ≠ 0) |
44 | 33, 38, 43 | fprodn0 15418 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ (0...(𝐾 − 1))) → ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) ≠ 0) |
45 | 44 | ex 416 |
. . . . 5
⊢ (𝜑 → (¬ 𝐶 ∈ (0...(𝐾 − 1)) → ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) ≠ 0)) |
46 | 45 | necon4bd 2954 |
. . . 4
⊢ (𝜑 → (∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) = 0 → 𝐶 ∈ (0...(𝐾 − 1)))) |
47 | 32, 46 | impbid 215 |
. . 3
⊢ (𝜑 → (𝐶 ∈ (0...(𝐾 − 1)) ↔ ∏𝑘 ∈ (0...(𝐾 − 1))(𝐶 − 𝑘) = 0)) |
48 | 15, 47 | bitr4d 285 |
. 2
⊢ (𝜑 → ((𝐶 FallFac 𝐾) = 0 ↔ 𝐶 ∈ (0...(𝐾 − 1)))) |
49 | 4, 12, 48 | 3bitrd 308 |
1
⊢ (𝜑 → ((𝐶C𝑐𝐾) = 0 ↔ 𝐶 ∈ (0...(𝐾 − 1)))) |