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 ) − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )