Step | Hyp | Ref
| Expression |
1 | | binomfallfaclem.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
2 | | elfzelz 13253 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ) |
3 | | bccl 14032 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) |
4 | 1, 2, 3 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈
ℕ0) |
5 | 4 | nn0cnd 12293 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈ ℂ) |
6 | | binomfallfaclem.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
7 | | fznn0sub 13285 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → (𝑁 − 𝑘) ∈
ℕ0) |
8 | | fallfaccl 15722 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝑁 − 𝑘) ∈ ℕ0) → (𝐴 FallFac (𝑁 − 𝑘)) ∈ ℂ) |
9 | 6, 7, 8 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 FallFac (𝑁 − 𝑘)) ∈ ℂ) |
10 | | binomfallfaclem.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
11 | | elfznn0 13346 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
12 | | fallfaccl 15722 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐵 FallFac 𝑘) ∈
ℂ) |
13 | 10, 11, 12 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐵 FallFac 𝑘) ∈ ℂ) |
14 | 9, 13 | mulcld 10994 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) ∈ ℂ) |
15 | 6, 10 | addcld 10993 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ) |
16 | 1 | nn0cnd 12293 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℂ) |
17 | 15, 16 | subcld 11330 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 + 𝐵) − 𝑁) ∈ ℂ) |
18 | 17 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 + 𝐵) − 𝑁) ∈ ℂ) |
19 | 5, 14, 18 | mulassd 10997 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁)) = ((𝑁C𝑘) · (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · ((𝐴 + 𝐵) − 𝑁)))) |
20 | 7 | nn0cnd 12293 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → (𝑁 − 𝑘) ∈ ℂ) |
21 | | subcl 11218 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ (𝑁 − 𝑘) ∈ ℂ) → (𝐴 − (𝑁 − 𝑘)) ∈ ℂ) |
22 | 6, 20, 21 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 − (𝑁 − 𝑘)) ∈ ℂ) |
23 | 11 | nn0cnd 12293 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℂ) |
24 | | subcl 11218 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐵 − 𝑘) ∈ ℂ) |
25 | 10, 23, 24 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐵 − 𝑘) ∈ ℂ) |
26 | 14, 22, 25 | adddid 10998 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · ((𝐴 − (𝑁 − 𝑘)) + (𝐵 − 𝑘))) = ((((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐴 − (𝑁 − 𝑘))) + (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐵 − 𝑘)))) |
27 | 6 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ ℂ) |
28 | 16 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑁 ∈ ℂ) |
29 | 27, 28 | subcld 11330 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 − 𝑁) ∈ ℂ) |
30 | 23 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ) |
31 | 10 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ ℂ) |
32 | 29, 30, 31 | ppncand 11370 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 − 𝑁) + 𝑘) + (𝐵 − 𝑘)) = ((𝐴 − 𝑁) + 𝐵)) |
33 | 27, 28, 30 | subsubd 11358 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 − (𝑁 − 𝑘)) = ((𝐴 − 𝑁) + 𝑘)) |
34 | 33 | oveq1d 7284 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 − (𝑁 − 𝑘)) + (𝐵 − 𝑘)) = (((𝐴 − 𝑁) + 𝑘) + (𝐵 − 𝑘))) |
35 | 27, 31, 28 | addsubd 11351 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 + 𝐵) − 𝑁) = ((𝐴 − 𝑁) + 𝐵)) |
36 | 32, 34, 35 | 3eqtr4d 2790 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 − (𝑁 − 𝑘)) + (𝐵 − 𝑘)) = ((𝐴 + 𝐵) − 𝑁)) |
37 | 36 | oveq2d 7285 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · ((𝐴 − (𝑁 − 𝑘)) + (𝐵 − 𝑘))) = (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · ((𝐴 + 𝐵) − 𝑁))) |
38 | 9, 13, 22 | mul32d 11183 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐴 − (𝑁 − 𝑘))) = (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐴 − (𝑁 − 𝑘))) · (𝐵 FallFac 𝑘))) |
39 | | 1cnd 10969 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 1 ∈ ℂ) |
40 | 28, 39, 30 | addsubd 11351 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 + 1) − 𝑘) = ((𝑁 − 𝑘) + 1)) |
41 | 40 | oveq2d 7285 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 FallFac ((𝑁 + 1) − 𝑘)) = (𝐴 FallFac ((𝑁 − 𝑘) + 1))) |
42 | | fallfacp1 15736 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ (𝑁 − 𝑘) ∈ ℕ0) → (𝐴 FallFac ((𝑁 − 𝑘) + 1)) = ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐴 − (𝑁 − 𝑘)))) |
43 | 6, 7, 42 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 FallFac ((𝑁 − 𝑘) + 1)) = ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐴 − (𝑁 − 𝑘)))) |
44 | 41, 43 | eqtrd 2780 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 FallFac ((𝑁 + 1) − 𝑘)) = ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐴 − (𝑁 − 𝑘)))) |
45 | 44 | oveq1d 7284 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) = (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐴 − (𝑁 − 𝑘))) · (𝐵 FallFac 𝑘))) |
46 | 38, 45 | eqtr4d 2783 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐴 − (𝑁 − 𝑘))) = ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) |
47 | 9, 13, 25 | mulassd 10997 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐵 − 𝑘)) = ((𝐴 FallFac (𝑁 − 𝑘)) · ((𝐵 FallFac 𝑘) · (𝐵 − 𝑘)))) |
48 | | fallfacp1 15736 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐵 FallFac (𝑘 + 1)) = ((𝐵 FallFac 𝑘) · (𝐵 − 𝑘))) |
49 | 10, 11, 48 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐵 FallFac (𝑘 + 1)) = ((𝐵 FallFac 𝑘) · (𝐵 − 𝑘))) |
50 | 49 | oveq2d 7285 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))) = ((𝐴 FallFac (𝑁 − 𝑘)) · ((𝐵 FallFac 𝑘) · (𝐵 − 𝑘)))) |
51 | 47, 50 | eqtr4d 2783 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐵 − 𝑘)) = ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))) |
52 | 46, 51 | oveq12d 7287 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐴 − (𝑁 − 𝑘))) + (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐵 − 𝑘))) = (((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) + ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) |
53 | 26, 37, 52 | 3eqtr3d 2788 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · ((𝐴 + 𝐵) − 𝑁)) = (((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) + ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) |
54 | 53 | oveq2d 7285 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · ((𝐴 + 𝐵) − 𝑁))) = ((𝑁C𝑘) · (((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) + ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) |
55 | 1 | nn0zd 12421 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) |
56 | | uzid 12594 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
57 | | peano2uz 12638 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝑁) → (𝑁 + 1) ∈
(ℤ≥‘𝑁)) |
58 | | fzss2 13293 |
. . . . . . . . . 10
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...(𝑁 + 1))) |
59 | 55, 56, 57, 58 | 4syl 19 |
. . . . . . . . 9
⊢ (𝜑 → (0...𝑁) ⊆ (0...(𝑁 + 1))) |
60 | 59 | sselda 3926 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ (0...(𝑁 + 1))) |
61 | | fznn0sub 13285 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) |
62 | | fallfaccl 15722 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ ((𝑁 + 1) − 𝑘) ∈ ℕ0) → (𝐴 FallFac ((𝑁 + 1) − 𝑘)) ∈ ℂ) |
63 | 6, 61, 62 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝐴 FallFac ((𝑁 + 1) − 𝑘)) ∈ ℂ) |
64 | 60, 63 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 FallFac ((𝑁 + 1) − 𝑘)) ∈ ℂ) |
65 | 64, 13 | mulcld 10994 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) ∈ ℂ) |
66 | | peano2nn0 12271 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
67 | 11, 66 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → (𝑘 + 1) ∈
ℕ0) |
68 | | fallfaccl 15722 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ (𝑘 + 1) ∈
ℕ0) → (𝐵 FallFac (𝑘 + 1)) ∈ ℂ) |
69 | 10, 67, 68 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐵 FallFac (𝑘 + 1)) ∈ ℂ) |
70 | 9, 69 | mulcld 10994 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))) ∈ ℂ) |
71 | 5, 65, 70 | adddid 10998 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) + ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) = (((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) |
72 | 19, 54, 71 | 3eqtrd 2784 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁)) = (((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) |
73 | 72 | sumeq2dv 15411 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁)) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) |
74 | 73 | adantr 481 |
. 2
⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁)) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) |
75 | 15, 1 | fallfacp1d 15738 |
. . . 4
⊢ (𝜑 → ((𝐴 + 𝐵) FallFac (𝑁 + 1)) = (((𝐴 + 𝐵) FallFac 𝑁) · ((𝐴 + 𝐵) − 𝑁))) |
76 | | binomfallfaclem.4 |
. . . . 5
⊢ (𝜓 → ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))) |
77 | 76 | oveq1d 7284 |
. . . 4
⊢ (𝜓 → (((𝐴 + 𝐵) FallFac 𝑁) · ((𝐴 + 𝐵) − 𝑁)) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁))) |
78 | 75, 77 | sylan9eq 2800 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + 𝐵) FallFac (𝑁 + 1)) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁))) |
79 | | fzfid 13689 |
. . . . 5
⊢ (𝜑 → (0...𝑁) ∈ Fin) |
80 | 5, 14 | mulcld 10994 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) ∈ ℂ) |
81 | 79, 17, 80 | fsummulc1 15493 |
. . . 4
⊢ (𝜑 → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁)) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁))) |
82 | 81 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁)) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁))) |
83 | 78, 82 | eqtrd 2780 |
. 2
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + 𝐵) FallFac (𝑁 + 1)) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁))) |
84 | | elfzelz 13253 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
85 | | bcpasc 14031 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ ((𝑁C𝑘) + (𝑁C(𝑘 − 1))) = ((𝑁 + 1)C𝑘)) |
86 | 1, 84, 85 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) + (𝑁C(𝑘 − 1))) = ((𝑁 + 1)C𝑘)) |
87 | 86 | oveq1d 7284 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = (((𝑁 + 1)C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) |
88 | 1, 84, 3 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C𝑘) ∈
ℕ0) |
89 | 88 | nn0cnd 12293 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C𝑘) ∈ ℂ) |
90 | | peano2zm 12361 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈
ℤ) |
91 | 84, 90 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → (𝑘 − 1) ∈ ℤ) |
92 | | bccl 14032 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑘 − 1) ∈
ℤ) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
93 | 1, 91, 92 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
94 | 93 | nn0cnd 12293 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈ ℂ) |
95 | | elfznn0 13346 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℕ0) |
96 | 10, 95, 12 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝐵 FallFac 𝑘) ∈ ℂ) |
97 | 63, 96 | mulcld 10994 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) ∈ ℂ) |
98 | 89, 94, 97 | adddird 10999 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = (((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))) |
99 | 87, 98 | eqtr3d 2782 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁 + 1)C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = (((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))) |
100 | 99 | sumeq2dv 15411 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))) |
101 | | nn0uz 12617 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
102 | 1, 101 | eleqtrdi 2851 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
103 | 89, 97 | mulcld 10994 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) ∈ ℂ) |
104 | | oveq2 7277 |
. . . . . . . . 9
⊢ (𝑘 = (𝑁 + 1) → (𝑁C𝑘) = (𝑁C(𝑁 + 1))) |
105 | | oveq2 7277 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑁 + 1) → ((𝑁 + 1) − 𝑘) = ((𝑁 + 1) − (𝑁 + 1))) |
106 | 105 | oveq2d 7285 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑁 + 1) → (𝐴 FallFac ((𝑁 + 1) − 𝑘)) = (𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1)))) |
107 | | oveq2 7277 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑁 + 1) → (𝐵 FallFac 𝑘) = (𝐵 FallFac (𝑁 + 1))) |
108 | 106, 107 | oveq12d 7287 |
. . . . . . . . 9
⊢ (𝑘 = (𝑁 + 1) → ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1)))) |
109 | 104, 108 | oveq12d 7287 |
. . . . . . . 8
⊢ (𝑘 = (𝑁 + 1) → ((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑁C(𝑁 + 1)) · ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1))))) |
110 | 102, 103,
109 | fsump1 15464 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C(𝑁 + 1)) · ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1)))))) |
111 | | peano2nn0 12271 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
112 | 1, 111 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
113 | 112 | nn0zd 12421 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
114 | 1 | nn0red 12292 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℝ) |
115 | 114 | ltp1d 11903 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 < (𝑁 + 1)) |
116 | 115 | olcd 871 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 + 1) < 0 ∨ 𝑁 < (𝑁 + 1))) |
117 | | bcval4 14017 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑁 + 1) ∈
ℤ ∧ ((𝑁 + 1) <
0 ∨ 𝑁 < (𝑁 + 1))) → (𝑁C(𝑁 + 1)) = 0) |
118 | 1, 113, 116, 117 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁C(𝑁 + 1)) = 0) |
119 | 118 | oveq1d 7284 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁C(𝑁 + 1)) · ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1)))) = (0 · ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1))))) |
120 | 112 | nn0cnd 12293 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 + 1) ∈ ℂ) |
121 | 120 | subidd 11318 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 + 1) − (𝑁 + 1)) = 0) |
122 | 121 | oveq2d 7285 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) = (𝐴 FallFac 0)) |
123 | | 0nn0 12246 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
124 | | fallfaccl 15722 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 0 ∈
ℕ0) → (𝐴 FallFac 0) ∈ ℂ) |
125 | 6, 123, 124 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 FallFac 0) ∈ ℂ) |
126 | 122, 125 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) ∈ ℂ) |
127 | | fallfaccl 15722 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℂ ∧ (𝑁 + 1) ∈
ℕ0) → (𝐵 FallFac (𝑁 + 1)) ∈ ℂ) |
128 | 10, 112, 127 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 FallFac (𝑁 + 1)) ∈ ℂ) |
129 | 126, 128 | mulcld 10994 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1))) ∈ ℂ) |
130 | 129 | mul02d 11171 |
. . . . . . . . 9
⊢ (𝜑 → (0 · ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1)))) = 0) |
131 | 119, 130 | eqtrd 2780 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁C(𝑁 + 1)) · ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1)))) = 0) |
132 | 131 | oveq2d 7285 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C(𝑁 + 1)) · ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1))))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + 0)) |
133 | 60, 103 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) ∈ ℂ) |
134 | 79, 133 | fsumcl 15441 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) ∈ ℂ) |
135 | 134 | addid1d 11173 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + 0) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) |
136 | 110, 132,
135 | 3eqtrd 2784 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) |
137 | 112, 101 | eleqtrdi 2851 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘0)) |
138 | 94, 97 | mulcld 10994 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) ∈ ℂ) |
139 | | oveq1 7276 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1)) |
140 | | df-neg 11206 |
. . . . . . . . . . 11
⊢ -1 = (0
− 1) |
141 | 139, 140 | eqtr4di 2798 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (𝑘 − 1) = -1) |
142 | 141 | oveq2d 7285 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑁C(𝑘 − 1)) = (𝑁C-1)) |
143 | | oveq2 7277 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → ((𝑁 + 1) − 𝑘) = ((𝑁 + 1) − 0)) |
144 | 143 | oveq2d 7285 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (𝐴 FallFac ((𝑁 + 1) − 𝑘)) = (𝐴 FallFac ((𝑁 + 1) − 0))) |
145 | | oveq2 7277 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (𝐵 FallFac 𝑘) = (𝐵 FallFac 0)) |
146 | 144, 145 | oveq12d 7287 |
. . . . . . . . 9
⊢ (𝑘 = 0 → ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0))) |
147 | 142, 146 | oveq12d 7287 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑁C-1) · ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0)))) |
148 | 137, 138,
147 | fsum1p 15461 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = (((𝑁C-1) · ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))) |
149 | | neg1z 12354 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℤ |
150 | | neg1lt0 12088 |
. . . . . . . . . . . . 13
⊢ -1 <
0 |
151 | 150 | orci 862 |
. . . . . . . . . . . 12
⊢ (-1 <
0 ∨ 𝑁 <
-1) |
152 | | bcval4 14017 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ -1 ∈ ℤ ∧ (-1 < 0 ∨ 𝑁 < -1)) → (𝑁C-1) = 0) |
153 | 149, 151,
152 | mp3an23 1452 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (𝑁C-1) =
0) |
154 | 1, 153 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁C-1) = 0) |
155 | 154 | oveq1d 7284 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁C-1) · ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0))) = (0 ·
((𝐴 FallFac ((𝑁 + 1) − 0)) ·
(𝐵 FallFac
0)))) |
156 | 120 | subid1d 11319 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 + 1) − 0) = (𝑁 + 1)) |
157 | 156 | oveq2d 7285 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 FallFac ((𝑁 + 1) − 0)) = (𝐴 FallFac (𝑁 + 1))) |
158 | | fallfaccl 15722 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ (𝑁 + 1) ∈
ℕ0) → (𝐴 FallFac (𝑁 + 1)) ∈ ℂ) |
159 | 6, 112, 158 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 FallFac (𝑁 + 1)) ∈ ℂ) |
160 | 157, 159 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 FallFac ((𝑁 + 1) − 0)) ∈
ℂ) |
161 | | fallfaccl 15722 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℂ ∧ 0 ∈
ℕ0) → (𝐵 FallFac 0) ∈ ℂ) |
162 | 10, 123, 161 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 FallFac 0) ∈ ℂ) |
163 | 160, 162 | mulcld 10994 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0)) ∈
ℂ) |
164 | 163 | mul02d 11171 |
. . . . . . . . 9
⊢ (𝜑 → (0 · ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0))) =
0) |
165 | 155, 164 | eqtrd 2780 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁C-1) · ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0))) =
0) |
166 | | 1zzd 12349 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℤ) |
167 | | 0zd 12329 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℤ) |
168 | 6, 10, 1 | binomfallfaclem1 15745 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑁C𝑗) · ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1)))) ∈ ℂ) |
169 | | oveq2 7277 |
. . . . . . . . . . . 12
⊢ (𝑗 = (𝑘 − 1) → (𝑁C𝑗) = (𝑁C(𝑘 − 1))) |
170 | | oveq2 7277 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑘 − 1) → (𝑁 − 𝑗) = (𝑁 − (𝑘 − 1))) |
171 | 170 | oveq2d 7285 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑘 − 1) → (𝐴 FallFac (𝑁 − 𝑗)) = (𝐴 FallFac (𝑁 − (𝑘 − 1)))) |
172 | | oveq1 7276 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑘 − 1) → (𝑗 + 1) = ((𝑘 − 1) + 1)) |
173 | 172 | oveq2d 7285 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑘 − 1) → (𝐵 FallFac (𝑗 + 1)) = (𝐵 FallFac ((𝑘 − 1) + 1))) |
174 | 171, 173 | oveq12d 7287 |
. . . . . . . . . . . 12
⊢ (𝑗 = (𝑘 − 1) → ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1))) = ((𝐴 FallFac (𝑁 − (𝑘 − 1))) · (𝐵 FallFac ((𝑘 − 1) + 1)))) |
175 | 169, 174 | oveq12d 7287 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑘 − 1) → ((𝑁C𝑗) · ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1)))) = ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac (𝑁 − (𝑘 − 1))) · (𝐵 FallFac ((𝑘 − 1) + 1))))) |
176 | 166, 167,
55, 168, 175 | fsumshft 15488 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑁)((𝑁C𝑗) · ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1)))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac (𝑁 − (𝑘 − 1))) · (𝐵 FallFac ((𝑘 − 1) + 1))))) |
177 | 16 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑁 ∈ ℂ) |
178 | | elfzelz 13253 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
179 | 178 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑘 ∈ ℤ) |
180 | 179 | zcnd 12424 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑘 ∈ ℂ) |
181 | | 1cnd 10969 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 1 ∈
ℂ) |
182 | 177, 180,
181 | subsub3d 11360 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑁 − (𝑘 − 1)) = ((𝑁 + 1) − 𝑘)) |
183 | 182 | oveq2d 7285 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝐴 FallFac (𝑁 − (𝑘 − 1))) = (𝐴 FallFac ((𝑁 + 1) − 𝑘))) |
184 | 180, 181 | npcand 11334 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑘 − 1) + 1) = 𝑘) |
185 | 184 | oveq2d 7285 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝐵 FallFac ((𝑘 − 1) + 1)) = (𝐵 FallFac 𝑘)) |
186 | 183, 185 | oveq12d 7287 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝐴 FallFac (𝑁 − (𝑘 − 1))) · (𝐵 FallFac ((𝑘 − 1) + 1))) = ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) |
187 | 186 | oveq2d 7285 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac (𝑁 − (𝑘 − 1))) · (𝐵 FallFac ((𝑘 − 1) + 1)))) = ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) |
188 | 187 | sumeq2dv 15411 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac (𝑁 − (𝑘 − 1))) · (𝐵 FallFac ((𝑘 − 1) + 1)))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) |
189 | 176, 188 | eqtr2d 2781 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑗 ∈ (0...𝑁)((𝑁C𝑗) · ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1))))) |
190 | | oveq2 7277 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → (𝑁C𝑘) = (𝑁C𝑗)) |
191 | | oveq2 7277 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → (𝑁 − 𝑘) = (𝑁 − 𝑗)) |
192 | 191 | oveq2d 7285 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (𝐴 FallFac (𝑁 − 𝑘)) = (𝐴 FallFac (𝑁 − 𝑗))) |
193 | | oveq1 7276 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → (𝑘 + 1) = (𝑗 + 1)) |
194 | 193 | oveq2d 7285 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (𝐵 FallFac (𝑘 + 1)) = (𝐵 FallFac (𝑗 + 1))) |
195 | 192, 194 | oveq12d 7287 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))) = ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1)))) |
196 | 190, 195 | oveq12d 7287 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))) = ((𝑁C𝑗) · ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1))))) |
197 | 196 | cbvsumv 15404 |
. . . . . . . . 9
⊢
Σ𝑘 ∈
(0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))) = Σ𝑗 ∈ (0...𝑁)((𝑁C𝑗) · ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1)))) |
198 | 189, 197 | eqtr4di 2798 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) |
199 | 165, 198 | oveq12d 7287 |
. . . . . . 7
⊢ (𝜑 → (((𝑁C-1) · ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) = (0 + Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) |
200 | 6, 10, 1 | binomfallfaclem1 15745 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))) ∈ ℂ) |
201 | 79, 200 | fsumcl 15441 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))) ∈ ℂ) |
202 | 201 | addid2d 11174 |
. . . . . . 7
⊢ (𝜑 → (0 + Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) |
203 | 148, 199,
202 | 3eqtrd 2784 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) |
204 | 136, 203 | oveq12d 7287 |
. . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) |
205 | | fzfid 13689 |
. . . . . 6
⊢ (𝜑 → (0...(𝑁 + 1)) ∈ Fin) |
206 | 205, 103,
138 | fsumadd 15448 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) = (Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))) |
207 | 79, 133, 200 | fsumadd 15448 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) |
208 | 204, 206,
207 | 3eqtr4d 2790 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) |
209 | 100, 208 | eqtrd 2780 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) |
210 | 209 | adantr 481 |
. 2
⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) |
211 | 74, 83, 210 | 3eqtr4d 2790 |
1
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + 𝐵) FallFac (𝑁 + 1)) = Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) |