Metamath Proof Explorer

Theorem binomrisefac

Description: A version of the binomial theorem using rising factorials instead of exponentials. (Contributed by Scott Fenton, 16-Mar-2018)

Ref Expression
Assertion binomrisefac ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) RiseFac 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 RiseFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 RiseFac 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 negdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 + 𝐵 ) = ( - 𝐴 + - 𝐵 ) )
2 1 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → - ( 𝐴 + 𝐵 ) = ( - 𝐴 + - 𝐵 ) )
3 2 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - ( 𝐴 + 𝐵 ) FallFac 𝑁 ) = ( ( - 𝐴 + - 𝐵 ) FallFac 𝑁 ) )
4 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
5 negcl ⊢ ( 𝐵 ∈ ℂ → - 𝐵 ∈ ℂ )
6 id ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
7 binomfallfac ⊢ ( ( - 𝐴 ∈ ℂ ∧ - 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( - 𝐴 + - 𝐵 ) FallFac 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) )
8 4 5 6 7 syl3an ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( - 𝐴 + - 𝐵 ) FallFac 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) )
9 3 8 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - ( 𝐴 + 𝐵 ) FallFac 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) )
10 9 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( - ( 𝐴 + 𝐵 ) FallFac 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) ) )
11 fzfid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 0 ... 𝑁 ) ∈ Fin )
12 neg1cn ⊢ - 1 ∈ ℂ
13 expcl ⊢ ( ( - 1 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - 1 ↑ 𝑁 ) ∈ ℂ )
14 12 13 mpan ⊢ ( 𝑁 ∈ ℕ0 → ( - 1 ↑ 𝑁 ) ∈ ℂ )
15 14 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - 1 ↑ 𝑁 ) ∈ ℂ )
16 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
17 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℤ )
18 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
19 16 17 18 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
20 19 nn0cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) ∈ ℂ )
21 simpl1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
22 21 negcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → - 𝐴 ∈ ℂ )
23 16 nn0zd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
24 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑁 − 𝑘 ) ∈ ℤ )
25 23 17 24 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑘 ) ∈ ℤ )
26 elfzle2 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ≤ 𝑁 )
27 26 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ≤ 𝑁 )
28 simpl3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℕ0 )
29 28 nn0red ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℝ )
30 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
31 30 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
32 31 nn0red ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℝ )
33 29 32 subge0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 0 ≤ ( 𝑁 − 𝑘 ) ↔ 𝑘 ≤ 𝑁 ) )
34 27 33 mpbird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ ( 𝑁 − 𝑘 ) )
35 elnn0z ⊢ ( ( 𝑁 − 𝑘 ) ∈ ℕ0 ↔ ( ( 𝑁 − 𝑘 ) ∈ ℤ ∧ 0 ≤ ( 𝑁 − 𝑘 ) ) )
36 25 34 35 sylanbrc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
37 fallfaccl ⊢ ( ( - 𝐴 ∈ ℂ ∧ ( 𝑁 − 𝑘 ) ∈ ℕ0 ) → ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) ∈ ℂ )
38 22 36 37 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) ∈ ℂ )
39 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
40 39 negcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → - 𝐵 ∈ ℂ )
41 fallfaccl ⊢ ( ( - 𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( - 𝐵 FallFac 𝑘 ) ∈ ℂ )
42 40 30 41 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( - 𝐵 FallFac 𝑘 ) ∈ ℂ )
43 38 42 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ∈ ℂ )
44 20 43 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) ∈ ℂ )
45 11 15 44 fsummulc2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑁 ) · ( ( 𝑁 C 𝑘 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) ) )
46 10 45 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( - ( 𝐴 + 𝐵 ) FallFac 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑁 ) · ( ( 𝑁 C 𝑘 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) ) )
47 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
48 risefallfac ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) RiseFac 𝑁 ) = ( ( - 1 ↑ 𝑁 ) · ( - ( 𝐴 + 𝐵 ) FallFac 𝑁 ) ) )
49 47 48 stoic3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) RiseFac 𝑁 ) = ( ( - 1 ↑ 𝑁 ) · ( - ( 𝐴 + 𝐵 ) FallFac 𝑁 ) ) )
50 risefallfac ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 − 𝑘 ) ∈ ℕ0 ) → ( 𝐴 RiseFac ( 𝑁 − 𝑘 ) ) = ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) ) )
51 21 36 50 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 RiseFac ( 𝑁 − 𝑘 ) ) = ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) ) )
52 simpl2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ ℂ )
53 risefallfac ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 RiseFac 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( - 𝐵 FallFac 𝑘 ) ) )
54 52 31 53 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐵 RiseFac 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( - 𝐵 FallFac 𝑘 ) ) )
55 51 54 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 RiseFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 RiseFac 𝑘 ) ) = ( ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) ) · ( ( - 1 ↑ 𝑘 ) · ( - 𝐵 FallFac 𝑘 ) ) ) )
56 expcl ⊢ ( ( - 1 ∈ ℂ ∧ ( 𝑁 − 𝑘 ) ∈ ℕ0 ) → ( - 1 ↑ ( 𝑁 − 𝑘 ) ) ∈ ℂ )
57 12 36 56 sylancr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( - 1 ↑ ( 𝑁 − 𝑘 ) ) ∈ ℂ )
58 expcl ⊢ ( ( - 1 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
59 12 30 58 sylancr ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
60 59 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
61 57 38 60 42 mul4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) ) · ( ( - 1 ↑ 𝑘 ) · ( - 𝐵 FallFac 𝑘 ) ) ) = ( ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 1 ↑ 𝑘 ) ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) )
62 12 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → - 1 ∈ ℂ )
63 62 31 36 expaddd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( - 1 ↑ ( ( 𝑁 − 𝑘 ) + 𝑘 ) ) = ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 1 ↑ 𝑘 ) ) )
64 16 nn0cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
65 30 nn0cnd ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℂ )
66 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑁 − 𝑘 ) + 𝑘 ) = 𝑁 )
67 64 65 66 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝑘 ) + 𝑘 ) = 𝑁 )
68 67 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( - 1 ↑ ( ( 𝑁 − 𝑘 ) + 𝑘 ) ) = ( - 1 ↑ 𝑁 ) )
69 63 68 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 1 ↑ 𝑘 ) ) = ( - 1 ↑ 𝑁 ) )
70 69 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 1 ↑ 𝑘 ) ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) )
71 55 61 70 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 RiseFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 RiseFac 𝑘 ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) )
72 71 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 RiseFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 RiseFac 𝑘 ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ 𝑁 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) ) )
73 15 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( - 1 ↑ 𝑁 ) ∈ ℂ )
74 20 73 43 mul12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ 𝑁 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( 𝑁 C 𝑘 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) ) )
75 72 74 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 RiseFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 RiseFac 𝑘 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( 𝑁 C 𝑘 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) ) )
76 75 sumeq2dv ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 RiseFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 RiseFac 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑁 ) · ( ( 𝑁 C 𝑘 ) · ( ( - 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( - 𝐵 FallFac 𝑘 ) ) ) ) )
77 46 49 76 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) RiseFac 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 RiseFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 RiseFac 𝑘 ) ) ) )