# 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 $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ N ∈ ℕ 0 → A + B N ‾ = ∑ k = 0 N ( N k) ⁢ A N − k ‾ ⁢ B k ‾$

### Proof

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