Proof of Theorem binomcxplemwb
Step | Hyp | Ref
| Expression |
1 | | binomcxplem.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) |
2 | | binomcxplem.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℕ) |
3 | 2 | nncnd 11725 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℂ) |
4 | 1, 3 | npcand 11072 |
. . . . 5
⊢ (𝜑 → ((𝐶 − 𝐾) + 𝐾) = 𝐶) |
5 | 4 | oveq1d 7179 |
. . . 4
⊢ (𝜑 → (((𝐶 − 𝐾) + 𝐾) · (𝐶 FallFac 𝐾)) = (𝐶 · (𝐶 FallFac 𝐾))) |
6 | 1, 3 | subcld 11068 |
. . . . 5
⊢ (𝜑 → (𝐶 − 𝐾) ∈ ℂ) |
7 | 2 | nnnn0d 12029 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
8 | | fallfaccl 15455 |
. . . . . 6
⊢ ((𝐶 ∈ ℂ ∧ 𝐾 ∈ ℕ0)
→ (𝐶 FallFac 𝐾) ∈
ℂ) |
9 | 1, 7, 8 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝐶 FallFac 𝐾) ∈ ℂ) |
10 | 6, 3, 9 | adddird 10737 |
. . . 4
⊢ (𝜑 → (((𝐶 − 𝐾) + 𝐾) · (𝐶 FallFac 𝐾)) = (((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) + (𝐾 · (𝐶 FallFac 𝐾)))) |
11 | 5, 10 | eqtr3d 2775 |
. . 3
⊢ (𝜑 → (𝐶 · (𝐶 FallFac 𝐾)) = (((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) + (𝐾 · (𝐶 FallFac 𝐾)))) |
12 | 11 | oveq1d 7179 |
. 2
⊢ (𝜑 → ((𝐶 · (𝐶 FallFac 𝐾)) / (!‘𝐾)) = ((((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) + (𝐾 · (𝐶 FallFac 𝐾))) / (!‘𝐾))) |
13 | 1, 7 | bccval 41478 |
. . . 4
⊢ (𝜑 → (𝐶C𝑐𝐾) = ((𝐶 FallFac 𝐾) / (!‘𝐾))) |
14 | 13 | oveq2d 7180 |
. . 3
⊢ (𝜑 → (𝐶 · (𝐶C𝑐𝐾)) = (𝐶 · ((𝐶 FallFac 𝐾) / (!‘𝐾)))) |
15 | | faccl 13728 |
. . . . . 6
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ∈
ℕ) |
16 | 15 | nncnd 11725 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ∈
ℂ) |
17 | 7, 16 | syl 17 |
. . . 4
⊢ (𝜑 → (!‘𝐾) ∈ ℂ) |
18 | | facne0 13731 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ≠
0) |
19 | 7, 18 | syl 17 |
. . . 4
⊢ (𝜑 → (!‘𝐾) ≠ 0) |
20 | 1, 9, 17, 19 | divassd 11522 |
. . 3
⊢ (𝜑 → ((𝐶 · (𝐶 FallFac 𝐾)) / (!‘𝐾)) = (𝐶 · ((𝐶 FallFac 𝐾) / (!‘𝐾)))) |
21 | 14, 20 | eqtr4d 2776 |
. 2
⊢ (𝜑 → (𝐶 · (𝐶C𝑐𝐾)) = ((𝐶 · (𝐶 FallFac 𝐾)) / (!‘𝐾))) |
22 | 6, 9, 17, 19 | divassd 11522 |
. . . 4
⊢ (𝜑 → (((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) / (!‘𝐾)) = ((𝐶 − 𝐾) · ((𝐶 FallFac 𝐾) / (!‘𝐾)))) |
23 | 22 | oveq1d 7179 |
. . 3
⊢ (𝜑 → ((((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) / (!‘𝐾)) + ((𝐾 · (𝐶 FallFac 𝐾)) / (!‘𝐾))) = (((𝐶 − 𝐾) · ((𝐶 FallFac 𝐾) / (!‘𝐾))) + ((𝐾 · (𝐶 FallFac 𝐾)) / (!‘𝐾)))) |
24 | 6, 9 | mulcld 10732 |
. . . 4
⊢ (𝜑 → ((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) ∈ ℂ) |
25 | 3, 9 | mulcld 10732 |
. . . 4
⊢ (𝜑 → (𝐾 · (𝐶 FallFac 𝐾)) ∈ ℂ) |
26 | 24, 25, 17, 19 | divdird 11525 |
. . 3
⊢ (𝜑 → ((((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) + (𝐾 · (𝐶 FallFac 𝐾))) / (!‘𝐾)) = ((((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) / (!‘𝐾)) + ((𝐾 · (𝐶 FallFac 𝐾)) / (!‘𝐾)))) |
27 | 13 | oveq2d 7180 |
. . . 4
⊢ (𝜑 → ((𝐶 − 𝐾) · (𝐶C𝑐𝐾)) = ((𝐶 − 𝐾) · ((𝐶 FallFac 𝐾) / (!‘𝐾)))) |
28 | | nnm1nn0 12010 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈
ℕ0) |
29 | 2, 28 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐾 − 1) ∈
ℕ0) |
30 | | faccl 13728 |
. . . . . . . 8
⊢ ((𝐾 − 1) ∈
ℕ0 → (!‘(𝐾 − 1)) ∈
ℕ) |
31 | 30 | nncnd 11725 |
. . . . . . 7
⊢ ((𝐾 − 1) ∈
ℕ0 → (!‘(𝐾 − 1)) ∈
ℂ) |
32 | 29, 31 | syl 17 |
. . . . . 6
⊢ (𝜑 → (!‘(𝐾 − 1)) ∈
ℂ) |
33 | | facne0 13731 |
. . . . . . 7
⊢ ((𝐾 − 1) ∈
ℕ0 → (!‘(𝐾 − 1)) ≠ 0) |
34 | 29, 33 | syl 17 |
. . . . . 6
⊢ (𝜑 → (!‘(𝐾 − 1)) ≠
0) |
35 | 2 | nnne0d 11759 |
. . . . . 6
⊢ (𝜑 → 𝐾 ≠ 0) |
36 | 9, 32, 3, 34, 35 | divcan5d 11513 |
. . . . 5
⊢ (𝜑 → ((𝐾 · (𝐶 FallFac 𝐾)) / (𝐾 · (!‘(𝐾 − 1)))) = ((𝐶 FallFac 𝐾) / (!‘(𝐾 − 1)))) |
37 | | 1cnd 10707 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
38 | 3, 37 | npcand 11072 |
. . . . . . . 8
⊢ (𝜑 → ((𝐾 − 1) + 1) = 𝐾) |
39 | 38 | fveq2d 6672 |
. . . . . . 7
⊢ (𝜑 → (!‘((𝐾 − 1) + 1)) =
(!‘𝐾)) |
40 | 38 | oveq2d 7180 |
. . . . . . . 8
⊢ (𝜑 → ((!‘(𝐾 − 1)) · ((𝐾 − 1) + 1)) =
((!‘(𝐾 − 1))
· 𝐾)) |
41 | | facp1 13723 |
. . . . . . . . 9
⊢ ((𝐾 − 1) ∈
ℕ0 → (!‘((𝐾 − 1) + 1)) = ((!‘(𝐾 − 1)) · ((𝐾 − 1) +
1))) |
42 | 29, 41 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (!‘((𝐾 − 1) + 1)) =
((!‘(𝐾 − 1))
· ((𝐾 − 1) +
1))) |
43 | 3, 32 | mulcomd 10733 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 · (!‘(𝐾 − 1))) = ((!‘(𝐾 − 1)) · 𝐾)) |
44 | 40, 42, 43 | 3eqtr4d 2783 |
. . . . . . 7
⊢ (𝜑 → (!‘((𝐾 − 1) + 1)) = (𝐾 · (!‘(𝐾 − 1)))) |
45 | 39, 44 | eqtr3d 2775 |
. . . . . 6
⊢ (𝜑 → (!‘𝐾) = (𝐾 · (!‘(𝐾 − 1)))) |
46 | 45 | oveq2d 7180 |
. . . . 5
⊢ (𝜑 → ((𝐾 · (𝐶 FallFac 𝐾)) / (!‘𝐾)) = ((𝐾 · (𝐶 FallFac 𝐾)) / (𝐾 · (!‘(𝐾 − 1))))) |
47 | 3, 37 | subcld 11068 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 − 1) ∈ ℂ) |
48 | 1, 47 | subcld 11068 |
. . . . . . 7
⊢ (𝜑 → (𝐶 − (𝐾 − 1)) ∈
ℂ) |
49 | | fallfaccl 15455 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℂ ∧ (𝐾 − 1) ∈
ℕ0) → (𝐶 FallFac (𝐾 − 1)) ∈
ℂ) |
50 | 1, 29, 49 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝐶 FallFac (𝐾 − 1)) ∈
ℂ) |
51 | 48, 50, 32, 34 | divassd 11522 |
. . . . . 6
⊢ (𝜑 → (((𝐶 − (𝐾 − 1)) · (𝐶 FallFac (𝐾 − 1))) / (!‘(𝐾 − 1))) = ((𝐶 − (𝐾 − 1)) · ((𝐶 FallFac (𝐾 − 1)) / (!‘(𝐾 − 1))))) |
52 | 38 | oveq2d 7180 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 FallFac ((𝐾 − 1) + 1)) = (𝐶 FallFac 𝐾)) |
53 | | fallfacp1 15469 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℂ ∧ (𝐾 − 1) ∈
ℕ0) → (𝐶 FallFac ((𝐾 − 1) + 1)) = ((𝐶 FallFac (𝐾 − 1)) · (𝐶 − (𝐾 − 1)))) |
54 | 1, 29, 53 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 FallFac ((𝐾 − 1) + 1)) = ((𝐶 FallFac (𝐾 − 1)) · (𝐶 − (𝐾 − 1)))) |
55 | 52, 54 | eqtr3d 2775 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 FallFac 𝐾) = ((𝐶 FallFac (𝐾 − 1)) · (𝐶 − (𝐾 − 1)))) |
56 | 48, 50 | mulcomd 10733 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶 − (𝐾 − 1)) · (𝐶 FallFac (𝐾 − 1))) = ((𝐶 FallFac (𝐾 − 1)) · (𝐶 − (𝐾 − 1)))) |
57 | 55, 56 | eqtr4d 2776 |
. . . . . . 7
⊢ (𝜑 → (𝐶 FallFac 𝐾) = ((𝐶 − (𝐾 − 1)) · (𝐶 FallFac (𝐾 − 1)))) |
58 | 57 | oveq1d 7179 |
. . . . . 6
⊢ (𝜑 → ((𝐶 FallFac 𝐾) / (!‘(𝐾 − 1))) = (((𝐶 − (𝐾 − 1)) · (𝐶 FallFac (𝐾 − 1))) / (!‘(𝐾 − 1)))) |
59 | 1, 29 | bccval 41478 |
. . . . . . 7
⊢ (𝜑 → (𝐶C𝑐(𝐾 − 1)) = ((𝐶 FallFac (𝐾 − 1)) / (!‘(𝐾 − 1)))) |
60 | 59 | oveq2d 7180 |
. . . . . 6
⊢ (𝜑 → ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1))) = ((𝐶 − (𝐾 − 1)) · ((𝐶 FallFac (𝐾 − 1)) / (!‘(𝐾 − 1))))) |
61 | 51, 58, 60 | 3eqtr4rd 2784 |
. . . . 5
⊢ (𝜑 → ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1))) = ((𝐶 FallFac 𝐾) / (!‘(𝐾 − 1)))) |
62 | 36, 46, 61 | 3eqtr4rd 2784 |
. . . 4
⊢ (𝜑 → ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1))) = ((𝐾 · (𝐶 FallFac 𝐾)) / (!‘𝐾))) |
63 | 27, 62 | oveq12d 7182 |
. . 3
⊢ (𝜑 → (((𝐶 − 𝐾) · (𝐶C𝑐𝐾)) + ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1)))) = (((𝐶 − 𝐾) · ((𝐶 FallFac 𝐾) / (!‘𝐾))) + ((𝐾 · (𝐶 FallFac 𝐾)) / (!‘𝐾)))) |
64 | 23, 26, 63 | 3eqtr4rd 2784 |
. 2
⊢ (𝜑 → (((𝐶 − 𝐾) · (𝐶C𝑐𝐾)) + ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1)))) = ((((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) + (𝐾 · (𝐶 FallFac 𝐾))) / (!‘𝐾))) |
65 | 12, 21, 64 | 3eqtr4rd 2784 |
1
⊢ (𝜑 → (((𝐶 − 𝐾) · (𝐶C𝑐𝐾)) + ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1)))) = (𝐶 · (𝐶C𝑐𝐾))) |