Metamath Proof Explorer

Theorem pwdif

Description: The difference of two numbers to the same power is the difference of the two numbers multiplied with a finite sum. Generalization of subsq . See Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number , 5-Aug-2021. (Contributed by AV, 6-Aug-2021) (Revised by AV, 19-Aug-2021)

Ref Expression
Assertion pwdif ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐴 − 𝐵 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 simp2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
3 simp3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
4 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
5 4 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 0 ..^ 𝑁 ) ∈ Fin )
6 2 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ ℂ )
7 elfzonn0 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → 𝑘 ∈ ℕ0 )
8 7 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
9 6 8 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
10 3 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ∈ ℂ )
11 ubmelm1fzo ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑁 − 𝑘 ) − 1 ) ∈ ( 0 ..^ 𝑁 ) )
12 elfzonn0 ⊢ ( ( ( 𝑁 − 𝑘 ) − 1 ) ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑁 − 𝑘 ) − 1 ) ∈ ℕ0 )
13 11 12 syl ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑁 − 𝑘 ) − 1 ) ∈ ℕ0 )
14 13 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑁 − 𝑘 ) − 1 ) ∈ ℕ0 )
15 10 14 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ∈ ℂ )
16 9 15 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ∈ ℂ )
17 5 16 fsumcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ∈ ℂ )
18 2 3 17 subdird ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) = ( ( 𝐴 · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) − ( 𝐵 · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) ) )
19 5 2 16 fsummulc2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) = Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝐴 · ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) )
20 6 9 15 mulassd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 · ( 𝐴 ↑ 𝑘 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = ( 𝐴 · ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) )
21 6 9 mulcomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 · ( 𝐴 ↑ 𝑘 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
22 expp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
23 2 7 22 syl2an ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
24 21 23 eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 · ( 𝐴 ↑ 𝑘 ) ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
25 24 oveq1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 · ( 𝐴 ↑ 𝑘 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) )
26 20 25 eqtr3d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 · ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) = ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) )
27 26 sumeq2dv ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝐴 · ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) = Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) )
28 19 27 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) = Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) )
29 5 3 16 fsummulc2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) = Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝐵 · ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) )
30 10 16 mulcomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 · ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) = ( ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) · 𝐵 ) )
31 9 15 10 mulassd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) · 𝐵 ) = ( ( 𝐴 ↑ 𝑘 ) · ( ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) · 𝐵 ) ) )
32 expp1 ⊢ ( ( 𝐵 ∈ ℂ ∧ ( ( 𝑁 − 𝑘 ) − 1 ) ∈ ℕ0 ) → ( 𝐵 ↑ ( ( ( 𝑁 − 𝑘 ) − 1 ) + 1 ) ) = ( ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) · 𝐵 ) )
33 32 eqcomd ⊢ ( ( 𝐵 ∈ ℂ ∧ ( ( 𝑁 − 𝑘 ) − 1 ) ∈ ℕ0 ) → ( ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) · 𝐵 ) = ( 𝐵 ↑ ( ( ( 𝑁 − 𝑘 ) − 1 ) + 1 ) ) )
34 3 13 33 syl2an ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) · 𝐵 ) = ( 𝐵 ↑ ( ( ( 𝑁 − 𝑘 ) − 1 ) + 1 ) ) )
35 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
36 35 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝑁 ∈ ℂ )
37 36 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℂ )
38 elfzoelz ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → 𝑘 ∈ ℤ )
39 38 zcnd ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → 𝑘 ∈ ℂ )
40 39 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ℂ )
41 37 40 subcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑁 − 𝑘 ) ∈ ℂ )
42 npcan1 ⊢ ( ( 𝑁 − 𝑘 ) ∈ ℂ → ( ( ( 𝑁 − 𝑘 ) − 1 ) + 1 ) = ( 𝑁 − 𝑘 ) )
43 42 oveq2d ⊢ ( ( 𝑁 − 𝑘 ) ∈ ℂ → ( 𝐵 ↑ ( ( ( 𝑁 − 𝑘 ) − 1 ) + 1 ) ) = ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) )
44 41 43 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 ↑ ( ( ( 𝑁 − 𝑘 ) − 1 ) + 1 ) ) = ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) )
45 34 44 eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) · 𝐵 ) = ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) )
46 45 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 ↑ 𝑘 ) · ( ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) · 𝐵 ) ) = ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) )
47 30 31 46 3eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 · ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) = ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) )
48 47 sumeq2dv ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝐵 · ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) = Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) )
49 29 48 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) = Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) )
50 28 49 oveq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) − ( 𝐵 · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) − Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ) )
51 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
52 51 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝑁 ∈ ℤ )
53 fzoval ⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
54 52 53 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
55 54 sumeq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) )
56 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
57 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
58 56 57 eleqtrdi ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
59 58 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
60 2 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝐴 ∈ ℂ )
61 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ0 )
62 peano2nn0 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
63 61 62 syl ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑘 + 1 ) ∈ ℕ0 )
64 63 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ℕ0 )
65 60 64 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ∈ ℂ )
66 3 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝐵 ∈ ℂ )
67 36 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℂ )
68 61 nn0cnd ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℂ )
69 68 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℂ )
70 1cnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℂ )
71 67 69 70 sub32d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 𝑘 ) − 1 ) = ( ( 𝑁 − 1 ) − 𝑘 ) )
72 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) − 𝑘 ) ∈ ℕ0 )
73 72 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) − 𝑘 ) ∈ ℕ0 )
74 71 73 eqeltrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 𝑘 ) − 1 ) ∈ ℕ0 )
75 66 74 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ∈ ℂ )
76 65 75 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ∈ ℂ )
77 oveq1 ⊢ ( 𝑘 = ( 𝑁 − 1 ) → ( 𝑘 + 1 ) = ( ( 𝑁 − 1 ) + 1 ) )
78 77 oveq2d ⊢ ( 𝑘 = ( 𝑁 − 1 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) )
79 oveq2 ⊢ ( 𝑘 = ( 𝑁 − 1 ) → ( 𝑁 − 𝑘 ) = ( 𝑁 − ( 𝑁 − 1 ) ) )
80 79 oveq1d ⊢ ( 𝑘 = ( 𝑁 − 1 ) → ( ( 𝑁 − 𝑘 ) − 1 ) = ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) )
81 80 oveq2d ⊢ ( 𝑘 = ( 𝑁 − 1 ) → ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) = ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) )
82 78 81 oveq12d ⊢ ( 𝑘 = ( 𝑁 − 1 ) → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) )
83 59 76 82 fsumm1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) + ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) ) )
84 55 83 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) + ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) ) )
85 54 sumeq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) )
86 61 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℕ0 )
87 60 86 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
88 54 eleq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
89 fzonnsub ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ℕ )
90 89 nnnn0d ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
91 88 90 syl6bir ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 ) )
92 91 imp ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
93 66 92 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ∈ ℂ )
94 87 93 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ∈ ℂ )
95 oveq2 ⊢ ( 𝑘 = 0 → ( 𝐴 ↑ 𝑘 ) = ( 𝐴 ↑ 0 ) )
96 oveq2 ⊢ ( 𝑘 = 0 → ( 𝑁 − 𝑘 ) = ( 𝑁 − 0 ) )
97 96 oveq2d ⊢ ( 𝑘 = 0 → ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) = ( 𝐵 ↑ ( 𝑁 − 0 ) ) )
98 95 97 oveq12d ⊢ ( 𝑘 = 0 → ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) = ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ ( 𝑁 − 0 ) ) ) )
99 59 94 98 fsum1p ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) = ( ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ ( 𝑁 − 0 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ) )
100 2 exp0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 0 ) = 1 )
101 36 subid1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑁 − 0 ) = 𝑁 )
102 101 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ ( 𝑁 − 0 ) ) = ( 𝐵 ↑ 𝑁 ) )
103 100 102 oveq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ ( 𝑁 − 0 ) ) ) = ( 1 · ( 𝐵 ↑ 𝑁 ) ) )
104 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝑁 ∈ ℕ )
105 104 nnnn0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝑁 ∈ ℕ0 )
106 3 105 expcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ 𝑁 ) ∈ ℂ )
107 106 mulid2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 1 · ( 𝐵 ↑ 𝑁 ) ) = ( 𝐵 ↑ 𝑁 ) )
108 103 107 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ ( 𝑁 − 0 ) ) ) = ( 𝐵 ↑ 𝑁 ) )
109 0p1e1 ⊢ ( 0 + 1 ) = 1
110 109 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 0 + 1 ) = 1 )
111 110 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) = ( 1 ... ( 𝑁 − 1 ) ) )
112 111 sumeq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) = Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) )
113 108 112 oveq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ ( 𝑁 − 0 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ) = ( ( 𝐵 ↑ 𝑁 ) + Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ) )
114 85 99 113 3eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) = ( ( 𝐵 ↑ 𝑁 ) + Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ) )
115 84 114 oveq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) − Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ) = ( ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) + ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) ) − ( ( 𝐵 ↑ 𝑁 ) + Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ) ) )
116 fzfid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 1 ... ( 𝑁 − 1 ) ) ∈ Fin )
117 2 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝐴 ∈ ℂ )
118 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ )
119 118 nnnn0d ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ0 )
120 119 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℕ0 )
121 117 120 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
122 3 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝐵 ∈ ℂ )
123 fzoval ⊢ ( 𝑁 ∈ ℤ → ( 1 ..^ 𝑁 ) = ( 1 ... ( 𝑁 − 1 ) ) )
124 52 123 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 1 ..^ 𝑁 ) = ( 1 ... ( 𝑁 − 1 ) ) )
125 124 eleq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑘 ∈ ( 1 ..^ 𝑁 ) ↔ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
126 fzonnsub ⊢ ( 𝑘 ∈ ( 1 ..^ 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ℕ )
127 126 nnnn0d ⊢ ( 𝑘 ∈ ( 1 ..^ 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
128 125 127 syl6bir ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 ) )
129 128 imp ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
130 122 129 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ∈ ℂ )
131 121 130 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ∈ ℂ )
132 116 131 fsumcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ∈ ℂ )
133 2 105 expcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
134 oveq1 ⊢ ( 𝑘 = 𝑙 → ( 𝑘 + 1 ) = ( 𝑙 + 1 ) )
135 134 oveq2d ⊢ ( 𝑘 = 𝑙 → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( 𝐴 ↑ ( 𝑙 + 1 ) ) )
136 oveq2 ⊢ ( 𝑘 = 𝑙 → ( 𝑁 − 𝑘 ) = ( 𝑁 − 𝑙 ) )
137 136 oveq1d ⊢ ( 𝑘 = 𝑙 → ( ( 𝑁 − 𝑘 ) − 1 ) = ( ( 𝑁 − 𝑙 ) − 1 ) )
138 137 oveq2d ⊢ ( 𝑘 = 𝑙 → ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) = ( 𝐵 ↑ ( ( 𝑁 − 𝑙 ) − 1 ) ) )
139 135 138 oveq12d ⊢ ( 𝑘 = 𝑙 → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = ( ( 𝐴 ↑ ( 𝑙 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑙 ) − 1 ) ) ) )
140 139 cbvsumv ⊢ Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = Σ 𝑙 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐴 ↑ ( 𝑙 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑙 ) − 1 ) ) )
141 1m1e0 ⊢ ( 1 − 1 ) = 0
142 141 eqcomi ⊢ 0 = ( 1 − 1 )
143 142 oveq1i ⊢ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) = ( ( 1 − 1 ) ... ( ( 𝑁 − 1 ) − 1 ) )
144 143 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) = ( ( 1 − 1 ) ... ( ( 𝑁 − 1 ) − 1 ) ) )
145 36 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑙 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ) → 𝑁 ∈ ℂ )
146 elfznn0 ⊢ ( 𝑙 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) → 𝑙 ∈ ℕ0 )
147 146 nn0cnd ⊢ ( 𝑙 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) → 𝑙 ∈ ℂ )
148 147 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑙 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ) → 𝑙 ∈ ℂ )
149 1cnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑙 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ) → 1 ∈ ℂ )
150 145 148 149 subsub4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑙 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ) → ( ( 𝑁 − 𝑙 ) − 1 ) = ( 𝑁 − ( 𝑙 + 1 ) ) )
151 150 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑙 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ) → ( 𝐵 ↑ ( ( 𝑁 − 𝑙 ) − 1 ) ) = ( 𝐵 ↑ ( 𝑁 − ( 𝑙 + 1 ) ) ) )
152 151 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑙 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ) → ( ( 𝐴 ↑ ( 𝑙 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑙 ) − 1 ) ) ) = ( ( 𝐴 ↑ ( 𝑙 + 1 ) ) · ( 𝐵 ↑ ( 𝑁 − ( 𝑙 + 1 ) ) ) ) )
153 144 152 sumeq12dv ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑙 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐴 ↑ ( 𝑙 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑙 ) − 1 ) ) ) = Σ 𝑙 ∈ ( ( 1 − 1 ) ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐴 ↑ ( 𝑙 + 1 ) ) · ( 𝐵 ↑ ( 𝑁 − ( 𝑙 + 1 ) ) ) ) )
154 140 153 eqtrid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = Σ 𝑙 ∈ ( ( 1 − 1 ) ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐴 ↑ ( 𝑙 + 1 ) ) · ( 𝐵 ↑ ( 𝑁 − ( 𝑙 + 1 ) ) ) ) )
155 1zzd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 1 ∈ ℤ )
156 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
157 52 156 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑁 − 1 ) ∈ ℤ )
158 oveq2 ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( 𝐴 ↑ 𝑘 ) = ( 𝐴 ↑ ( 𝑙 + 1 ) ) )
159 oveq2 ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( 𝑁 − 𝑘 ) = ( 𝑁 − ( 𝑙 + 1 ) ) )
160 159 oveq2d ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) = ( 𝐵 ↑ ( 𝑁 − ( 𝑙 + 1 ) ) ) )
161 158 160 oveq12d ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) = ( ( 𝐴 ↑ ( 𝑙 + 1 ) ) · ( 𝐵 ↑ ( 𝑁 − ( 𝑙 + 1 ) ) ) ) )
162 155 155 157 131 161 fsumshftm ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) = Σ 𝑙 ∈ ( ( 1 − 1 ) ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐴 ↑ ( 𝑙 + 1 ) ) · ( 𝐵 ↑ ( 𝑁 − ( 𝑙 + 1 ) ) ) ) )
163 154 162 eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) )
164 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
165 36 164 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
166 165 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝐴 ↑ 𝑁 ) )
167 peano2cnm ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 − 1 ) ∈ ℂ )
168 35 167 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℂ )
169 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
170 35 168 169 sub32d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) = ( ( 𝑁 − 1 ) − ( 𝑁 − 1 ) ) )
171 168 subidd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) − ( 𝑁 − 1 ) ) = 0 )
172 170 171 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) = 0 )
173 172 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) = 0 )
174 173 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) = ( 𝐵 ↑ 0 ) )
175 exp0 ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ↑ 0 ) = 1 )
176 175 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ 0 ) = 1 )
177 174 176 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) = 1 )
178 166 177 oveq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) = ( ( 𝐴 ↑ 𝑁 ) · 1 ) )
179 133 mulid1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 𝑁 ) · 1 ) = ( 𝐴 ↑ 𝑁 ) )
180 178 179 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) = ( 𝐴 ↑ 𝑁 ) )
181 163 180 oveq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) + ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) + ( 𝐴 ↑ 𝑁 ) ) )
182 132 133 181 comraddd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) + ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) ) = ( ( 𝐴 ↑ 𝑁 ) + Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ) )
183 182 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) + ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) ) − ( ( 𝐵 ↑ 𝑁 ) + Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ) ) = ( ( ( 𝐴 ↑ 𝑁 ) + Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ) − ( ( 𝐵 ↑ 𝑁 ) + Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ) ) )
184 133 106 132 pnpcan2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 ↑ 𝑁 ) + Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ) − ( ( 𝐵 ↑ 𝑁 ) + Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ) ) = ( ( 𝐴 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) )
185 115 183 184 3eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) − Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( 𝑁 − 𝑘 ) ) ) ) = ( ( 𝐴 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) )
186 18 50 185 3eqtrrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐴 − 𝐵 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) )
187 186 3exp ⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ∈ ℂ → ( 𝐵 ∈ ℂ → ( ( 𝐴 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐴 − 𝐵 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) ) ) )
188 simp2 ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
189 simp3 ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
190 188 189 subcld ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
191 190 mul01d ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) · 0 ) = 0 )
192 oveq2 ⊢ ( 𝑁 = 0 → ( 0 ..^ 𝑁 ) = ( 0 ..^ 0 ) )
193 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
194 192 193 eqtrdi ⊢ ( 𝑁 = 0 → ( 0 ..^ 𝑁 ) = ∅ )
195 194 sumeq1d ⊢ ( 𝑁 = 0 → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = Σ 𝑘 ∈ ∅ ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) )
196 195 3ad2ant1 ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = Σ 𝑘 ∈ ∅ ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) )
197 sum0 ⊢ Σ 𝑘 ∈ ∅ ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = 0
198 196 197 eqtrdi ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = 0 )
199 198 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) = ( ( 𝐴 − 𝐵 ) · 0 ) )
200 oveq2 ⊢ ( 𝑁 = 0 → ( 𝐴 ↑ 𝑁 ) = ( 𝐴 ↑ 0 ) )
201 200 3ad2ant1 ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 𝑁 ) = ( 𝐴 ↑ 0 ) )
202 exp0 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
203 202 3ad2ant2 ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 0 ) = 1 )
204 201 203 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 𝑁 ) = 1 )
205 oveq2 ⊢ ( 𝑁 = 0 → ( 𝐵 ↑ 𝑁 ) = ( 𝐵 ↑ 0 ) )
206 205 3ad2ant1 ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ 𝑁 ) = ( 𝐵 ↑ 0 ) )
207 175 3ad2ant3 ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ 0 ) = 1 )
208 206 207 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ 𝑁 ) = 1 )
209 204 208 oveq12d ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) = ( 1 − 1 ) )
210 209 141 eqtrdi ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) = 0 )
211 191 199 210 3eqtr4rd ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐴 − 𝐵 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) )
212 211 3exp ⊢ ( 𝑁 = 0 → ( 𝐴 ∈ ℂ → ( 𝐵 ∈ ℂ → ( ( 𝐴 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐴 − 𝐵 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) ) ) )
213 187 212 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 𝐴 ∈ ℂ → ( 𝐵 ∈ ℂ → ( ( 𝐴 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐴 − 𝐵 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) ) ) )
214 1 213 sylbi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ ℂ → ( 𝐵 ∈ ℂ → ( ( 𝐴 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐴 − 𝐵 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) ) ) )
215 214 3imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐴 − 𝐵 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) )