Proof of Theorem binomcxplemwb
| Step | Hyp | Ref
| Expression |
| 1 | | binomcxplem.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 2 | | binomcxplem.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℕ) |
| 3 | 2 | nncnd 12282 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℂ) |
| 4 | 1, 3 | npcand 11624 |
. . . . 5
⊢ (𝜑 → ((𝐶 − 𝐾) + 𝐾) = 𝐶) |
| 5 | 4 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → (((𝐶 − 𝐾) + 𝐾) · (𝐶 FallFac 𝐾)) = (𝐶 · (𝐶 FallFac 𝐾))) |
| 6 | 1, 3 | subcld 11620 |
. . . . 5
⊢ (𝜑 → (𝐶 − 𝐾) ∈ ℂ) |
| 7 | 2 | nnnn0d 12587 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
| 8 | | fallfaccl 16052 |
. . . . . 6
⊢ ((𝐶 ∈ ℂ ∧ 𝐾 ∈ ℕ0)
→ (𝐶 FallFac 𝐾) ∈
ℂ) |
| 9 | 1, 7, 8 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐶 FallFac 𝐾) ∈ ℂ) |
| 10 | 6, 3, 9 | adddird 11286 |
. . . 4
⊢ (𝜑 → (((𝐶 − 𝐾) + 𝐾) · (𝐶 FallFac 𝐾)) = (((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) + (𝐾 · (𝐶 FallFac 𝐾)))) |
| 11 | 5, 10 | eqtr3d 2779 |
. . 3
⊢ (𝜑 → (𝐶 · (𝐶 FallFac 𝐾)) = (((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) + (𝐾 · (𝐶 FallFac 𝐾)))) |
| 12 | 11 | oveq1d 7446 |
. 2
⊢ (𝜑 → ((𝐶 · (𝐶 FallFac 𝐾)) / (!‘𝐾)) = ((((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) + (𝐾 · (𝐶 FallFac 𝐾))) / (!‘𝐾))) |
| 13 | 1, 7 | bccval 44357 |
. . . 4
⊢ (𝜑 → (𝐶C𝑐𝐾) = ((𝐶 FallFac 𝐾) / (!‘𝐾))) |
| 14 | 13 | oveq2d 7447 |
. . 3
⊢ (𝜑 → (𝐶 · (𝐶C𝑐𝐾)) = (𝐶 · ((𝐶 FallFac 𝐾) / (!‘𝐾)))) |
| 15 | | faccl 14322 |
. . . . . 6
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ∈
ℕ) |
| 16 | 15 | nncnd 12282 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ∈
ℂ) |
| 17 | 7, 16 | syl 17 |
. . . 4
⊢ (𝜑 → (!‘𝐾) ∈ ℂ) |
| 18 | | facne0 14325 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ≠
0) |
| 19 | 7, 18 | syl 17 |
. . . 4
⊢ (𝜑 → (!‘𝐾) ≠ 0) |
| 20 | 1, 9, 17, 19 | divassd 12078 |
. . 3
⊢ (𝜑 → ((𝐶 · (𝐶 FallFac 𝐾)) / (!‘𝐾)) = (𝐶 · ((𝐶 FallFac 𝐾) / (!‘𝐾)))) |
| 21 | 14, 20 | eqtr4d 2780 |
. 2
⊢ (𝜑 → (𝐶 · (𝐶C𝑐𝐾)) = ((𝐶 · (𝐶 FallFac 𝐾)) / (!‘𝐾))) |
| 22 | 6, 9, 17, 19 | divassd 12078 |
. . . 4
⊢ (𝜑 → (((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) / (!‘𝐾)) = ((𝐶 − 𝐾) · ((𝐶 FallFac 𝐾) / (!‘𝐾)))) |
| 23 | 22 | oveq1d 7446 |
. . 3
⊢ (𝜑 → ((((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) / (!‘𝐾)) + ((𝐾 · (𝐶 FallFac 𝐾)) / (!‘𝐾))) = (((𝐶 − 𝐾) · ((𝐶 FallFac 𝐾) / (!‘𝐾))) + ((𝐾 · (𝐶 FallFac 𝐾)) / (!‘𝐾)))) |
| 24 | 6, 9 | mulcld 11281 |
. . . 4
⊢ (𝜑 → ((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) ∈ ℂ) |
| 25 | 3, 9 | mulcld 11281 |
. . . 4
⊢ (𝜑 → (𝐾 · (𝐶 FallFac 𝐾)) ∈ ℂ) |
| 26 | 24, 25, 17, 19 | divdird 12081 |
. . 3
⊢ (𝜑 → ((((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) + (𝐾 · (𝐶 FallFac 𝐾))) / (!‘𝐾)) = ((((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) / (!‘𝐾)) + ((𝐾 · (𝐶 FallFac 𝐾)) / (!‘𝐾)))) |
| 27 | 13 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → ((𝐶 − 𝐾) · (𝐶C𝑐𝐾)) = ((𝐶 − 𝐾) · ((𝐶 FallFac 𝐾) / (!‘𝐾)))) |
| 28 | | nnm1nn0 12567 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈
ℕ0) |
| 29 | 2, 28 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐾 − 1) ∈
ℕ0) |
| 30 | | faccl 14322 |
. . . . . . . 8
⊢ ((𝐾 − 1) ∈
ℕ0 → (!‘(𝐾 − 1)) ∈
ℕ) |
| 31 | 30 | nncnd 12282 |
. . . . . . 7
⊢ ((𝐾 − 1) ∈
ℕ0 → (!‘(𝐾 − 1)) ∈
ℂ) |
| 32 | 29, 31 | syl 17 |
. . . . . 6
⊢ (𝜑 → (!‘(𝐾 − 1)) ∈
ℂ) |
| 33 | | facne0 14325 |
. . . . . . 7
⊢ ((𝐾 − 1) ∈
ℕ0 → (!‘(𝐾 − 1)) ≠ 0) |
| 34 | 29, 33 | syl 17 |
. . . . . 6
⊢ (𝜑 → (!‘(𝐾 − 1)) ≠
0) |
| 35 | 2 | nnne0d 12316 |
. . . . . 6
⊢ (𝜑 → 𝐾 ≠ 0) |
| 36 | 9, 32, 3, 34, 35 | divcan5d 12069 |
. . . . 5
⊢ (𝜑 → ((𝐾 · (𝐶 FallFac 𝐾)) / (𝐾 · (!‘(𝐾 − 1)))) = ((𝐶 FallFac 𝐾) / (!‘(𝐾 − 1)))) |
| 37 | | 1cnd 11256 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
| 38 | 3, 37 | npcand 11624 |
. . . . . . . 8
⊢ (𝜑 → ((𝐾 − 1) + 1) = 𝐾) |
| 39 | 38 | fveq2d 6910 |
. . . . . . 7
⊢ (𝜑 → (!‘((𝐾 − 1) + 1)) =
(!‘𝐾)) |
| 40 | 38 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → ((!‘(𝐾 − 1)) · ((𝐾 − 1) + 1)) =
((!‘(𝐾 − 1))
· 𝐾)) |
| 41 | | facp1 14317 |
. . . . . . . . 9
⊢ ((𝐾 − 1) ∈
ℕ0 → (!‘((𝐾 − 1) + 1)) = ((!‘(𝐾 − 1)) · ((𝐾 − 1) +
1))) |
| 42 | 29, 41 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (!‘((𝐾 − 1) + 1)) =
((!‘(𝐾 − 1))
· ((𝐾 − 1) +
1))) |
| 43 | 3, 32 | mulcomd 11282 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 · (!‘(𝐾 − 1))) = ((!‘(𝐾 − 1)) · 𝐾)) |
| 44 | 40, 42, 43 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (𝜑 → (!‘((𝐾 − 1) + 1)) = (𝐾 · (!‘(𝐾 − 1)))) |
| 45 | 39, 44 | eqtr3d 2779 |
. . . . . 6
⊢ (𝜑 → (!‘𝐾) = (𝐾 · (!‘(𝐾 − 1)))) |
| 46 | 45 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → ((𝐾 · (𝐶 FallFac 𝐾)) / (!‘𝐾)) = ((𝐾 · (𝐶 FallFac 𝐾)) / (𝐾 · (!‘(𝐾 − 1))))) |
| 47 | 3, 37 | subcld 11620 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 − 1) ∈ ℂ) |
| 48 | 1, 47 | subcld 11620 |
. . . . . . 7
⊢ (𝜑 → (𝐶 − (𝐾 − 1)) ∈
ℂ) |
| 49 | | fallfaccl 16052 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℂ ∧ (𝐾 − 1) ∈
ℕ0) → (𝐶 FallFac (𝐾 − 1)) ∈
ℂ) |
| 50 | 1, 29, 49 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐶 FallFac (𝐾 − 1)) ∈
ℂ) |
| 51 | 48, 50, 32, 34 | divassd 12078 |
. . . . . 6
⊢ (𝜑 → (((𝐶 − (𝐾 − 1)) · (𝐶 FallFac (𝐾 − 1))) / (!‘(𝐾 − 1))) = ((𝐶 − (𝐾 − 1)) · ((𝐶 FallFac (𝐾 − 1)) / (!‘(𝐾 − 1))))) |
| 52 | 38 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 FallFac ((𝐾 − 1) + 1)) = (𝐶 FallFac 𝐾)) |
| 53 | | fallfacp1 16066 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℂ ∧ (𝐾 − 1) ∈
ℕ0) → (𝐶 FallFac ((𝐾 − 1) + 1)) = ((𝐶 FallFac (𝐾 − 1)) · (𝐶 − (𝐾 − 1)))) |
| 54 | 1, 29, 53 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 FallFac ((𝐾 − 1) + 1)) = ((𝐶 FallFac (𝐾 − 1)) · (𝐶 − (𝐾 − 1)))) |
| 55 | 52, 54 | eqtr3d 2779 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 FallFac 𝐾) = ((𝐶 FallFac (𝐾 − 1)) · (𝐶 − (𝐾 − 1)))) |
| 56 | 48, 50 | mulcomd 11282 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶 − (𝐾 − 1)) · (𝐶 FallFac (𝐾 − 1))) = ((𝐶 FallFac (𝐾 − 1)) · (𝐶 − (𝐾 − 1)))) |
| 57 | 55, 56 | eqtr4d 2780 |
. . . . . . 7
⊢ (𝜑 → (𝐶 FallFac 𝐾) = ((𝐶 − (𝐾 − 1)) · (𝐶 FallFac (𝐾 − 1)))) |
| 58 | 57 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → ((𝐶 FallFac 𝐾) / (!‘(𝐾 − 1))) = (((𝐶 − (𝐾 − 1)) · (𝐶 FallFac (𝐾 − 1))) / (!‘(𝐾 − 1)))) |
| 59 | 1, 29 | bccval 44357 |
. . . . . . 7
⊢ (𝜑 → (𝐶C𝑐(𝐾 − 1)) = ((𝐶 FallFac (𝐾 − 1)) / (!‘(𝐾 − 1)))) |
| 60 | 59 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1))) = ((𝐶 − (𝐾 − 1)) · ((𝐶 FallFac (𝐾 − 1)) / (!‘(𝐾 − 1))))) |
| 61 | 51, 58, 60 | 3eqtr4rd 2788 |
. . . . 5
⊢ (𝜑 → ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1))) = ((𝐶 FallFac 𝐾) / (!‘(𝐾 − 1)))) |
| 62 | 36, 46, 61 | 3eqtr4rd 2788 |
. . . 4
⊢ (𝜑 → ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1))) = ((𝐾 · (𝐶 FallFac 𝐾)) / (!‘𝐾))) |
| 63 | 27, 62 | oveq12d 7449 |
. . 3
⊢ (𝜑 → (((𝐶 − 𝐾) · (𝐶C𝑐𝐾)) + ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1)))) = (((𝐶 − 𝐾) · ((𝐶 FallFac 𝐾) / (!‘𝐾))) + ((𝐾 · (𝐶 FallFac 𝐾)) / (!‘𝐾)))) |
| 64 | 23, 26, 63 | 3eqtr4rd 2788 |
. 2
⊢ (𝜑 → (((𝐶 − 𝐾) · (𝐶C𝑐𝐾)) + ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1)))) = ((((𝐶 − 𝐾) · (𝐶 FallFac 𝐾)) + (𝐾 · (𝐶 FallFac 𝐾))) / (!‘𝐾))) |
| 65 | 12, 21, 64 | 3eqtr4rd 2788 |
1
⊢ (𝜑 → (((𝐶 − 𝐾) · (𝐶C𝑐𝐾)) + ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1)))) = (𝐶 · (𝐶C𝑐𝐾))) |