Metamath Proof Explorer


Theorem binomlem

Description: Lemma for binom (binomial theorem). Inductive step. (Contributed by NM, 6-Dec-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses binomlem.1 ( 𝜑𝐴 ∈ ℂ )
binomlem.2 ( 𝜑𝐵 ∈ ℂ )
binomlem.3 ( 𝜑𝑁 ∈ ℕ0 )
binomlem.4 ( 𝜓 → ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
Assertion binomlem ( ( 𝜑𝜓 ) → ( ( 𝐴 + 𝐵 ) ↑ ( 𝑁 + 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 binomlem.1 ( 𝜑𝐴 ∈ ℂ )
2 binomlem.2 ( 𝜑𝐵 ∈ ℂ )
3 binomlem.3 ( 𝜑𝑁 ∈ ℕ0 )
4 binomlem.4 ( 𝜓 → ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
5 4 adantl ( ( 𝜑𝜓 ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
6 5 oveq1d ( ( 𝜑𝜓 ) → ( ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) · 𝐴 ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐴 ) )
7 fzfid ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
8 fzelp1 ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
9 elfzelz ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
10 bccl ( ( 𝑁 ∈ ℕ0𝑘 ∈ ℤ ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
11 3 9 10 syl2an ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
12 11 nn0cnd ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C 𝑘 ) ∈ ℂ )
13 8 12 sylan2 ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) ∈ ℂ )
14 fznn0sub ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁𝑘 ) ∈ ℕ0 )
15 expcl ( ( 𝐴 ∈ ℂ ∧ ( 𝑁𝑘 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑁𝑘 ) ) ∈ ℂ )
16 1 14 15 syl2an ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ↑ ( 𝑁𝑘 ) ) ∈ ℂ )
17 elfznn0 ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ0 )
18 expcl ( ( 𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵𝑘 ) ∈ ℂ )
19 2 17 18 syl2an ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝐵𝑘 ) ∈ ℂ )
20 8 19 sylan2 ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐵𝑘 ) ∈ ℂ )
21 16 20 mulcld ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ∈ ℂ )
22 13 21 mulcld ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) ∈ ℂ )
23 7 1 22 fsummulc1 ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐴 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐴 ) )
24 1 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
25 13 21 24 mulassd ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐴 ) = ( ( 𝑁 C 𝑘 ) · ( ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) · 𝐴 ) ) )
26 3 nn0cnd ( 𝜑𝑁 ∈ ℂ )
27 26 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℂ )
28 1cnd ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → 1 ∈ ℂ )
29 elfzelz ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℤ )
30 29 adantl ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℤ )
31 30 zcnd ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
32 27 28 31 addsubd ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) = ( ( 𝑁𝑘 ) + 1 ) )
33 32 oveq2d ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) = ( 𝐴 ↑ ( ( 𝑁𝑘 ) + 1 ) ) )
34 expp1 ( ( 𝐴 ∈ ℂ ∧ ( 𝑁𝑘 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 𝑁𝑘 ) + 1 ) ) = ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · 𝐴 ) )
35 1 14 34 syl2an ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ↑ ( ( 𝑁𝑘 ) + 1 ) ) = ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · 𝐴 ) )
36 33 35 eqtrd ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) = ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · 𝐴 ) )
37 36 oveq1d ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) = ( ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · 𝐴 ) · ( 𝐵𝑘 ) ) )
38 16 24 20 mul32d ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · 𝐴 ) · ( 𝐵𝑘 ) ) = ( ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) · 𝐴 ) )
39 37 38 eqtrd ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) = ( ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) · 𝐴 ) )
40 39 oveq2d ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) · 𝐴 ) ) )
41 25 40 eqtr4d ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐴 ) = ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
42 41 sumeq2dv ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐴 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
43 fzssp1 ( 0 ... 𝑁 ) ⊆ ( 0 ... ( 𝑁 + 1 ) )
44 43 a1i ( 𝜑 → ( 0 ... 𝑁 ) ⊆ ( 0 ... ( 𝑁 + 1 ) ) )
45 fznn0sub ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
46 expcl ( ( 𝐴 ∈ ℂ ∧ ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) ∈ ℂ )
47 1 45 46 syl2an ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) ∈ ℂ )
48 47 19 mulcld ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ∈ ℂ )
49 12 48 mulcld ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) ∈ ℂ )
50 8 49 sylan2 ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) ∈ ℂ )
51 3 adantr ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
52 eldifi ( 𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
53 52 9 syl ( 𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℤ )
54 53 adantl ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑘 ∈ ℤ )
55 eldifn ( 𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 0 ... 𝑁 ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
56 55 adantl ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
57 bcval3 ( ( 𝑁 ∈ ℕ0𝑘 ∈ ℤ ∧ ¬ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) = 0 )
58 51 54 56 57 syl3anc ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑁 C 𝑘 ) = 0 )
59 58 oveq1d ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = ( 0 · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
60 48 mul02d ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 0 · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = 0 )
61 52 60 sylan2 ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 0 · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = 0 )
62 59 61 eqtrd ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = 0 )
63 fzssuz ( 0 ... ( 𝑁 + 1 ) ) ⊆ ( ℤ ‘ 0 )
64 63 a1i ( 𝜑 → ( 0 ... ( 𝑁 + 1 ) ) ⊆ ( ℤ ‘ 0 ) )
65 44 50 62 64 sumss ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
66 23 42 65 3eqtrd ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐴 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
67 66 adantr ( ( 𝜑𝜓 ) → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐴 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
68 6 67 eqtrd ( ( 𝜑𝜓 ) → ( ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) · 𝐴 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
69 4 oveq1d ( 𝜓 → ( ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) · 𝐵 ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐵 ) )
70 7 2 22 fsummulc1 ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐵 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐵 ) )
71 1zzd ( 𝜑 → 1 ∈ ℤ )
72 0z 0 ∈ ℤ
73 72 a1i ( 𝜑 → 0 ∈ ℤ )
74 3 nn0zd ( 𝜑𝑁 ∈ ℤ )
75 2 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ ℂ )
76 22 75 mulcld ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐵 ) ∈ ℂ )
77 oveq2 ( 𝑘 = ( 𝑗 − 1 ) → ( 𝑁 C 𝑘 ) = ( 𝑁 C ( 𝑗 − 1 ) ) )
78 oveq2 ( 𝑘 = ( 𝑗 − 1 ) → ( 𝑁𝑘 ) = ( 𝑁 − ( 𝑗 − 1 ) ) )
79 78 oveq2d ( 𝑘 = ( 𝑗 − 1 ) → ( 𝐴 ↑ ( 𝑁𝑘 ) ) = ( 𝐴 ↑ ( 𝑁 − ( 𝑗 − 1 ) ) ) )
80 oveq2 ( 𝑘 = ( 𝑗 − 1 ) → ( 𝐵𝑘 ) = ( 𝐵 ↑ ( 𝑗 − 1 ) ) )
81 79 80 oveq12d ( 𝑘 = ( 𝑗 − 1 ) → ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) = ( ( 𝐴 ↑ ( 𝑁 − ( 𝑗 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑗 − 1 ) ) ) )
82 77 81 oveq12d ( 𝑘 = ( 𝑗 − 1 ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) = ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( 𝐴 ↑ ( 𝑁 − ( 𝑗 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑗 − 1 ) ) ) ) )
83 82 oveq1d ( 𝑘 = ( 𝑗 − 1 ) → ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐵 ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( 𝐴 ↑ ( 𝑁 − ( 𝑗 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑗 − 1 ) ) ) ) · 𝐵 ) )
84 71 73 74 76 83 fsumshft ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐵 ) = Σ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( 𝐴 ↑ ( 𝑁 − ( 𝑗 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑗 − 1 ) ) ) ) · 𝐵 ) )
85 oveq1 ( 𝑗 = 𝑘 → ( 𝑗 − 1 ) = ( 𝑘 − 1 ) )
86 85 oveq2d ( 𝑗 = 𝑘 → ( 𝑁 C ( 𝑗 − 1 ) ) = ( 𝑁 C ( 𝑘 − 1 ) ) )
87 85 oveq2d ( 𝑗 = 𝑘 → ( 𝑁 − ( 𝑗 − 1 ) ) = ( 𝑁 − ( 𝑘 − 1 ) ) )
88 87 oveq2d ( 𝑗 = 𝑘 → ( 𝐴 ↑ ( 𝑁 − ( 𝑗 − 1 ) ) ) = ( 𝐴 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) )
89 85 oveq2d ( 𝑗 = 𝑘 → ( 𝐵 ↑ ( 𝑗 − 1 ) ) = ( 𝐵 ↑ ( 𝑘 − 1 ) ) )
90 88 89 oveq12d ( 𝑗 = 𝑘 → ( ( 𝐴 ↑ ( 𝑁 − ( 𝑗 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑗 − 1 ) ) ) = ( ( 𝐴 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) )
91 86 90 oveq12d ( 𝑗 = 𝑘 → ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( 𝐴 ↑ ( 𝑁 − ( 𝑗 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑗 − 1 ) ) ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) ) )
92 91 oveq1d ( 𝑗 = 𝑘 → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( 𝐴 ↑ ( 𝑁 − ( 𝑗 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑗 − 1 ) ) ) ) · 𝐵 ) = ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) ) · 𝐵 ) )
93 92 cbvsumv Σ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( 𝐴 ↑ ( 𝑁 − ( 𝑗 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑗 − 1 ) ) ) ) · 𝐵 ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) ) · 𝐵 )
94 84 93 eqtrdi ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐵 ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) ) · 𝐵 ) )
95 26 adantr ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ℂ )
96 elfzelz ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
97 96 adantl ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℤ )
98 97 zcnd ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℂ )
99 1cnd ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 1 ∈ ℂ )
100 95 98 99 subsub3d ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝑁 − ( 𝑘 − 1 ) ) = ( ( 𝑁 + 1 ) − 𝑘 ) )
101 100 oveq2d ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝐴 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) = ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) )
102 101 oveq1d ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝐴 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) = ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) )
103 102 oveq2d ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) ) )
104 103 oveq1d ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) ) · 𝐵 ) = ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) ) · 𝐵 ) )
105 fzp1ss ( 0 ∈ ℤ → ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ⊆ ( 0 ... ( 𝑁 + 1 ) ) )
106 72 105 ax-mp ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ⊆ ( 0 ... ( 𝑁 + 1 ) )
107 106 sseli ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
108 9 adantl ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℤ )
109 peano2zm ( 𝑘 ∈ ℤ → ( 𝑘 − 1 ) ∈ ℤ )
110 108 109 syl ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑘 − 1 ) ∈ ℤ )
111 bccl ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑘 − 1 ) ∈ ℤ ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
112 3 110 111 syl2an2r ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
113 112 nn0cnd ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℂ )
114 107 113 sylan2 ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℂ )
115 107 47 sylan2 ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) ∈ ℂ )
116 2 adantr ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝐵 ∈ ℂ )
117 elfznn ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ )
118 0p1e1 ( 0 + 1 ) = 1
119 118 oveq1i ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) = ( 1 ... ( 𝑁 + 1 ) )
120 117 119 eleq2s ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ )
121 120 adantl ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℕ )
122 nnm1nn0 ( 𝑘 ∈ ℕ → ( 𝑘 − 1 ) ∈ ℕ0 )
123 121 122 syl ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝑘 − 1 ) ∈ ℕ0 )
124 116 123 expcld ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝐵 ↑ ( 𝑘 − 1 ) ) ∈ ℂ )
125 115 124 mulcld ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) ∈ ℂ )
126 114 125 116 mulassd ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) ) · 𝐵 ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) · 𝐵 ) ) )
127 115 124 116 mulassd ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) · 𝐵 ) = ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( ( 𝐵 ↑ ( 𝑘 − 1 ) ) · 𝐵 ) ) )
128 expm1t ( ( 𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ ) → ( 𝐵𝑘 ) = ( ( 𝐵 ↑ ( 𝑘 − 1 ) ) · 𝐵 ) )
129 2 120 128 syl2an ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝐵𝑘 ) = ( ( 𝐵 ↑ ( 𝑘 − 1 ) ) · 𝐵 ) )
130 129 oveq2d ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) = ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( ( 𝐵 ↑ ( 𝑘 − 1 ) ) · 𝐵 ) ) )
131 127 130 eqtr4d ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) · 𝐵 ) = ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) )
132 131 oveq2d ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) · 𝐵 ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
133 104 126 132 3eqtrd ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) ) · 𝐵 ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
134 133 sumeq2dv ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 ↑ ( 𝑘 − 1 ) ) ) ) · 𝐵 ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
135 106 a1i ( 𝜑 → ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ⊆ ( 0 ... ( 𝑁 + 1 ) ) )
136 113 48 mulcld ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) ∈ ℂ )
137 107 136 sylan2 ( ( 𝜑𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) ∈ ℂ )
138 3 adantr ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → 𝑁 ∈ ℕ0 )
139 eldifi ( 𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
140 139 adantl ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
141 140 9 syl ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → 𝑘 ∈ ℤ )
142 141 109 syl ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → ( 𝑘 − 1 ) ∈ ℤ )
143 eldifn ( 𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ¬ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) )
144 143 adantl ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → ¬ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) )
145 72 a1i ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → 0 ∈ ℤ )
146 138 nn0zd ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → 𝑁 ∈ ℤ )
147 1zzd ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → 1 ∈ ℤ )
148 fzaddel ( ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑘 − 1 ) ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( ( 𝑘 − 1 ) ∈ ( 0 ... 𝑁 ) ↔ ( ( 𝑘 − 1 ) + 1 ) ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) )
149 145 146 142 147 148 syl22anc ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → ( ( 𝑘 − 1 ) ∈ ( 0 ... 𝑁 ) ↔ ( ( 𝑘 − 1 ) + 1 ) ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) )
150 141 zcnd ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → 𝑘 ∈ ℂ )
151 ax-1cn 1 ∈ ℂ
152 npcan ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑘 − 1 ) + 1 ) = 𝑘 )
153 150 151 152 sylancl ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → ( ( 𝑘 − 1 ) + 1 ) = 𝑘 )
154 153 eleq1d ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → ( ( ( 𝑘 − 1 ) + 1 ) ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↔ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) )
155 149 154 bitrd ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → ( ( 𝑘 − 1 ) ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) )
156 144 155 mtbird ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → ¬ ( 𝑘 − 1 ) ∈ ( 0 ... 𝑁 ) )
157 bcval3 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑘 − 1 ) ∈ ℤ ∧ ¬ ( 𝑘 − 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) = 0 )
158 138 142 156 157 syl3anc ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) = 0 )
159 158 oveq1d ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = ( 0 · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
160 139 60 sylan2 ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → ( 0 · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = 0 )
161 159 160 eqtrd ( ( 𝜑𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = 0 )
162 135 137 161 64 sumss ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
163 94 134 162 3eqtrd ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐵 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
164 70 163 eqtrd ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁𝑘 ) ) · ( 𝐵𝑘 ) ) ) · 𝐵 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
165 69 164 sylan9eqr ( ( 𝜑𝜓 ) → ( ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) · 𝐵 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
166 68 165 oveq12d ( ( 𝜑𝜓 ) → ( ( ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) · 𝐴 ) + ( ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) · 𝐵 ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) + Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) ) )
167 1 2 addcld ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℂ )
168 167 3 expp1d ( 𝜑 → ( ( 𝐴 + 𝐵 ) ↑ ( 𝑁 + 1 ) ) = ( ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) · ( 𝐴 + 𝐵 ) ) )
169 167 3 expcld ( 𝜑 → ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) ∈ ℂ )
170 169 1 2 adddid ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) · ( 𝐴 + 𝐵 ) ) = ( ( ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) · 𝐴 ) + ( ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) · 𝐵 ) ) )
171 168 170 eqtrd ( 𝜑 → ( ( 𝐴 + 𝐵 ) ↑ ( 𝑁 + 1 ) ) = ( ( ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) · 𝐴 ) + ( ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) · 𝐵 ) ) )
172 171 adantr ( ( 𝜑𝜓 ) → ( ( 𝐴 + 𝐵 ) ↑ ( 𝑁 + 1 ) ) = ( ( ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) · 𝐴 ) + ( ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) · 𝐵 ) ) )
173 bcpasc ( ( 𝑁 ∈ ℕ0𝑘 ∈ ℤ ) → ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝑘 ) )
174 3 9 173 syl2an ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝑘 ) )
175 174 oveq1d ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
176 12 113 48 adddird ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) ) )
177 175 176 eqtr3d ( ( 𝜑𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) ) )
178 177 sumeq2dv ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) ) )
179 fzfid ( 𝜑 → ( 0 ... ( 𝑁 + 1 ) ) ∈ Fin )
180 179 49 136 fsumadd ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) + Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) ) )
181 178 180 eqtrd ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) + Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) ) )
182 181 adantr ( ( 𝜑𝜓 ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) + Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) ) )
183 166 172 182 3eqtr4d ( ( 𝜑𝜓 ) → ( ( 𝐴 + 𝐵 ) ↑ ( 𝑁 + 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵𝑘 ) ) ) )