Theorem pwdif 15948

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 14266. See Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number 14266, 5-Aug-2021. (Contributed by AV, 6-Aug-2021.) (Revised by AV, 19-Aug-2021.)

Assertion

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

Distinct variable groups:   𝐴,𝑘   𝐵,𝑘   𝑘,𝑁

Proof of Theorem pwdif

Dummy variable 𝑙 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elnn0 12524	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		simp2 1155	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
3		simp3 1156	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
4		fzofi 14030	. . . . . . . . 9 ⊢ (0..^𝑁) ∈ Fin
5	4	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0..^𝑁) ∈ Fin)
6	2	adantr 486	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝐴 ∈ ℂ)
7		elfzonn0 13755	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℕ0)
8	7	adantl 487	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑘 ∈ ℕ0)
9	6, 8	expcld 14202	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴↑𝑘) ∈ ℂ)
10	3	adantr 486	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝐵 ∈ ℂ)
11		ubmelm1fzo 13811	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0..^𝑁) → ((𝑁 − 𝑘) − 1) ∈ (0..^𝑁))
12		elfzonn0 13755	. . . . . . . . . . . 12 ⊢ (((𝑁 − 𝑘) − 1) ∈ (0..^𝑁) → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
13	11, 12	syl 18	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0..^𝑁) → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
14	13	adantl 487	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
15	10, 14	expcld 14202	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵↑((𝑁 − 𝑘) − 1)) ∈ ℂ)
16	9, 15	mulcld 11247	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
17	5, 16	fsumcl 15810	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
18	2, 3, 17	subdird 11689	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) − (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))))
19	5, 2, 16	fsummulc2 15861	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)(𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
20	6, 9, 15	mulassd 11250	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴 · (𝐴↑𝑘)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
21	6, 9	mulcomd 11248	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · (𝐴↑𝑘)) = ((𝐴↑𝑘) · 𝐴))
22		expp1 14124	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
23	2, 7, 22	syl2an 608	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
24	21, 23	eqtr4d 2804	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · (𝐴↑𝑘)) = (𝐴↑(𝑘 + 1)))
25	24	oveq1d 7438	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴 · (𝐴↑𝑘)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
26	20, 25	eqtr3d 2803	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
27	26	sumeq2dv 15779	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)(𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
28	19, 27	eqtrd 2801	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
29	5, 3, 16	fsummulc2 15861	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)(𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
30	10, 16	mulcomd 11248	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = (((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) · 𝐵))
31	9, 15, 10	mulassd 11250	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) · 𝐵) = ((𝐴↑𝑘) · ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵)))
32		expp1 14124	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℂ ∧ ((𝑁 − 𝑘) − 1) ∈ ℕ0) → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵))
33	32	eqcomd 2772	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℂ ∧ ((𝑁 − 𝑘) − 1) ∈ ℕ0) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(((𝑁 − 𝑘) − 1) + 1)))
34	3, 13, 33	syl2an 608	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(((𝑁 − 𝑘) − 1) + 1)))
35		nncn 12259	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
36	35	3ad2ant1 1151	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℂ)
37	36	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑁 ∈ ℂ)
38		elfzoelz 13706	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℤ)
39	38	zcnd 12719	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℂ)
40	39	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑘 ∈ ℂ)
41	37, 40	subcld 11587	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝑁 − 𝑘) ∈ ℂ)
42		npcan1 11657	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 𝑘) ∈ ℂ → (((𝑁 − 𝑘) − 1) + 1) = (𝑁 − 𝑘))
43	42	oveq2d 7439	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 𝑘) ∈ ℂ → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = (𝐵↑(𝑁 − 𝑘)))
44	41, 43	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = (𝐵↑(𝑁 − 𝑘)))
45	34, 44	eqtrd 2801	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(𝑁 − 𝑘)))
46	45	oveq2d 7439	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴↑𝑘) · ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵)) = ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
47	30, 31, 46	3eqtrd 2805	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
48	47	sumeq2dv 15779	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)(𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
49	29, 48	eqtrd 2801	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
50	28, 49	oveq12d 7441	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) − (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))) = (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
51		nnz 12630	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
52	51	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℤ)
53		fzoval 13707	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → (0..^𝑁) = (0...(𝑁 − 1)))
54	52, 53	syl 18	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0..^𝑁) = (0...(𝑁 − 1)))
55	54	sumeq1d 15777	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
56		nnm1nn0 12563	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
57		nn0uz 12918	. . . . . . . . . . . 12 ⊢ ℕ0 = (ℤ≥‘0)
58	56, 57	eleqtrdi 2876	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ≥‘0))
59	58	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 1) ∈ (ℤ≥‘0))
60	2	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝐴 ∈ ℂ)
61		elfznn0 13667	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
62		peano2nn0 12562	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
63	61, 62	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → (𝑘 + 1) ∈ ℕ0)
64	63	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑘 + 1) ∈ ℕ0)
65	60, 64	expcld 14202	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑(𝑘 + 1)) ∈ ℂ)
66	3	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝐵 ∈ ℂ)
67	36	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℂ)
68	61	nn0cnd 12585	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℂ)
69	68	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℂ)
70		1cnd 11220	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 1 ∈ ℂ)
71	67, 69, 70	sub32d 11619	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 𝑘) − 1) = ((𝑁 − 1) − 𝑘))
72		fznn0sub 13603	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
73	72	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
74	71, 73	eqeltrd 2866	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
75	66, 74	expcld 14202	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐵↑((𝑁 − 𝑘) − 1)) ∈ ℂ)
76	65, 75	mulcld 11247	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
77		oveq1 7430	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑁 − 1) → (𝑘 + 1) = ((𝑁 − 1) + 1))
78	77	oveq2d 7439	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑁 − 1) → (𝐴↑(𝑘 + 1)) = (𝐴↑((𝑁 − 1) + 1)))
79		oveq2 7431	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑁 − 1) → (𝑁 − 𝑘) = (𝑁 − (𝑁 − 1)))
80	79	oveq1d 7438	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑁 − 1) → ((𝑁 − 𝑘) − 1) = ((𝑁 − (𝑁 − 1)) − 1))
81	80	oveq2d 7439	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑁 − 1) → (𝐵↑((𝑁 − 𝑘) − 1)) = (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))
82	78, 81	oveq12d 7441	. . . . . . . . . 10 ⊢ (𝑘 = (𝑁 − 1) → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))))
83	59, 76, 82	fsumm1 15828	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))))
84	55, 83	eqtrd 2801	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))))
85	54	sumeq1d 15777	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
86	61	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0)
87	60, 86	expcld 14202	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑𝑘) ∈ ℂ)
88	54	eleq2d 2852	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (0..^𝑁) ↔ 𝑘 ∈ (0...(𝑁 − 1))))
89		fzonnsub 13732	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑁 − 𝑘) ∈ ℕ)
90	89	nnnn0d 12583	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑁 − 𝑘) ∈ ℕ0)
91	88, 90	biimtrrdi 257	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (0...(𝑁 − 1)) → (𝑁 − 𝑘) ∈ ℕ0))
92	91	imp 412	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑁 − 𝑘) ∈ ℕ0)
93	66, 92	expcld 14202	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐵↑(𝑁 − 𝑘)) ∈ ℂ)
94	87, 93	mulcld 11247	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
95		oveq2 7431	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (𝐴↑𝑘) = (𝐴↑0))
96		oveq2 7431	. . . . . . . . . . . 12 ⊢ (𝑘 = 0 → (𝑁 − 𝑘) = (𝑁 − 0))
97	96	oveq2d 7439	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (𝐵↑(𝑁 − 𝑘)) = (𝐵↑(𝑁 − 0)))
98	95, 97	oveq12d 7441	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐴↑0) · (𝐵↑(𝑁 − 0))))
99	59, 94, 98	fsum1p 15830	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = (((𝐴↑0) · (𝐵↑(𝑁 − 0))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
100	2	exp0d 14196	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) = 1)
101	36	subid1d 11576	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 0) = 𝑁)
102	101	oveq2d 7439	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑(𝑁 − 0)) = (𝐵↑𝑁))
103	100, 102	oveq12d 7441	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑0) · (𝐵↑(𝑁 − 0))) = (1 · (𝐵↑𝑁)))
104		simp1 1154	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℕ)
105	104	nnnn0d 12583	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℕ0)
106	3, 105	expcld 14202	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) ∈ ℂ)
107	106	mullidd 11245	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · (𝐵↑𝑁)) = (𝐵↑𝑁))
108	103, 107	eqtrd 2801	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑0) · (𝐵↑(𝑁 − 0))) = (𝐵↑𝑁))
109		0p1e1 12379	. . . . . . . . . . . . 13 ⊢ (0 + 1) = 1
110	109	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0 + 1) = 1)
111	110	oveq1d 7438	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((0 + 1)...(𝑁 − 1)) = (1...(𝑁 − 1)))
112	111	sumeq1d 15777	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
113	108, 112	oveq12d 7441	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑0) · (𝐵↑(𝑁 − 0))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
114	85, 99, 113	3eqtrd 2805	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
115	84, 114	oveq12d 7441	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))))
116		fzfid 14029	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1...(𝑁 − 1)) ∈ Fin)
117	2	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝐴 ∈ ℂ)
118		elfznn 13600	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ)
119	118	nnnn0d 12583	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
120	119	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℕ0)
121	117, 120	expcld 14202	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝐴↑𝑘) ∈ ℂ)
122	3	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝐵 ∈ ℂ)
123		fzoval 13707	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → (1..^𝑁) = (1...(𝑁 − 1)))
124	52, 123	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1..^𝑁) = (1...(𝑁 − 1)))
125	124	eleq2d 2852	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (1..^𝑁) ↔ 𝑘 ∈ (1...(𝑁 − 1))))
126		fzonnsub 13732	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1..^𝑁) → (𝑁 − 𝑘) ∈ ℕ)
127	126	nnnn0d 12583	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1..^𝑁) → (𝑁 − 𝑘) ∈ ℕ0)
128	125, 127	biimtrrdi 257	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (1...(𝑁 − 1)) → (𝑁 − 𝑘) ∈ ℕ0))
129	128	imp 412	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑁 − 𝑘) ∈ ℕ0)
130	122, 129	expcld 14202	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝐵↑(𝑁 − 𝑘)) ∈ ℂ)
131	121, 130	mulcld 11247	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
132	116, 131	fsumcl 15810	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
133	2, 105	expcld 14202	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) ∈ ℂ)
134		oveq1 7430	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → (𝑘 + 1) = (𝑙 + 1))
135	134	oveq2d 7439	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝐴↑(𝑘 + 1)) = (𝐴↑(𝑙 + 1)))
136		oveq2 7431	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → (𝑁 − 𝑘) = (𝑁 − 𝑙))
137	136	oveq1d 7438	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → ((𝑁 − 𝑘) − 1) = ((𝑁 − 𝑙) − 1))
138	137	oveq2d 7439	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝐵↑((𝑁 − 𝑘) − 1)) = (𝐵↑((𝑁 − 𝑙) − 1)))
139	135, 138	oveq12d 7441	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))))
140	139	cbvsumv 15773	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑙 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1)))
141		1m1e0 12331	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
142	141	eqcomi 2775	. . . . . . . . . . . . . . 15 ⊢ 0 = (1 − 1)
143	142	oveq1i 7433	. . . . . . . . . . . . . 14 ⊢ (0...((𝑁 − 1) − 1)) = ((1 − 1)...((𝑁 − 1) − 1))
144	143	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0...((𝑁 − 1) − 1)) = ((1 − 1)...((𝑁 − 1) − 1)))
145	36	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → 𝑁 ∈ ℂ)
146		elfznn0 13667	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 ∈ (0...((𝑁 − 1) − 1)) → 𝑙 ∈ ℕ0)
147	146	nn0cnd 12585	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 ∈ (0...((𝑁 − 1) − 1)) → 𝑙 ∈ ℂ)
148	147	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → 𝑙 ∈ ℂ)
149		1cnd 11220	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → 1 ∈ ℂ)
150	145, 148, 149	subsub4d 11618	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → ((𝑁 − 𝑙) − 1) = (𝑁 − (𝑙 + 1)))
151	150	oveq2d 7439	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → (𝐵↑((𝑁 − 𝑙) − 1)) = (𝐵↑(𝑁 − (𝑙 + 1))))
152	151	oveq2d 7439	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → ((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
153	144, 152	sumeq12dv 15783	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑙 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
154	140, 153	eqtrid 2813	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
155		1zzd 12643	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈ ℤ)
156		peano2zm 12655	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
157	52, 156	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 1) ∈ ℤ)
158		oveq2 7431	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑙 + 1) → (𝐴↑𝑘) = (𝐴↑(𝑙 + 1)))
159		oveq2 7431	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑙 + 1) → (𝑁 − 𝑘) = (𝑁 − (𝑙 + 1)))
160	159	oveq2d 7439	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑙 + 1) → (𝐵↑(𝑁 − 𝑘)) = (𝐵↑(𝑁 − (𝑙 + 1))))
161	158, 160	oveq12d 7441	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑙 + 1) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
162	155, 155, 157, 131, 161	fsumshftm 15858	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
163	154, 162	eqtr4d 2804	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
164		npcan1 11657	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
165	36, 164	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
166	165	oveq2d 7439	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑((𝑁 − 1) + 1)) = (𝐴↑𝑁))
167		peano2cnm 11542	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℂ → (𝑁 − 1) ∈ ℂ)
168	35, 167	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℂ)
169		1cnd 11220	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
170	35, 168, 169	sub32d 11619	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((𝑁 − (𝑁 − 1)) − 1) = ((𝑁 − 1) − (𝑁 − 1)))
171	168	subidd 11575	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) − (𝑁 − 1)) = 0)
172	170, 171	eqtrd 2801	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → ((𝑁 − (𝑁 − 1)) − 1) = 0)
173	172	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑁 − (𝑁 − 1)) − 1) = 0)
174	173	oveq2d 7439	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑((𝑁 − (𝑁 − 1)) − 1)) = (𝐵↑0))
175		exp0 14121	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℂ → (𝐵↑0) = 1)
176	175	3ad2ant3 1153	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑0) = 1)
177	174, 176	eqtrd 2801	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑((𝑁 − (𝑁 − 1)) − 1)) = 1)
178	166, 177	oveq12d 7441	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))) = ((𝐴↑𝑁) · 1))
179	133	mulridd 11244	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) · 1) = (𝐴↑𝑁))
180	178, 179	eqtrd 2801	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))) = (𝐴↑𝑁))
181	163, 180	oveq12d 7441	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) = (Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) + (𝐴↑𝑁)))
182	132, 133, 181	comraddd 11442	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) = ((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
183	182	oveq1d 7438	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))) = (((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))))
184	133, 106, 132	pnpcan2d 11625	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))) = ((𝐴↑𝑁) − (𝐵↑𝑁)))
185	115, 183, 184	3eqtrd 2805	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((𝐴↑𝑁) − (𝐵↑𝑁)))
186	18, 50, 185	3eqtrrd 2806	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
187	186	3exp 1137	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))))
188		simp2 1155	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
189		simp3 1156	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
190	188, 189	subcld 11587	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
191	190	mul01d 11427	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · 0) = 0)
192		oveq2 7431	. . . . . . . . . . 11 ⊢ (𝑁 = 0 → (0..^𝑁) = (0..^0))
193		fzo0 13731	. . . . . . . . . . 11 ⊢ (0..^0) = ∅
194	192, 193	eqtrdi 2817	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (0..^𝑁) = ∅)
195	194	sumeq1d 15777	. . . . . . . . 9 ⊢ (𝑁 = 0 → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))
196	195	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))
197		sum0 15798	. . . . . . . 8 ⊢ Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = 0
198	196, 197	eqtrdi 2817	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = 0)
199	198	oveq2d 7439	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴 − 𝐵) · 0))
200		oveq2 7431	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (𝐴↑𝑁) = (𝐴↑0))
201	200	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) = (𝐴↑0))
202		exp0 14121	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1)
203	202	3ad2ant2 1152	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) = 1)
204	201, 203	eqtrd 2801	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) = 1)
205		oveq2 7431	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (𝐵↑𝑁) = (𝐵↑0))
206	205	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) = (𝐵↑0))
207	175	3ad2ant3 1153	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑0) = 1)
208	206, 207	eqtrd 2801	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) = 1)
209	204, 208	oveq12d 7441	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = (1 − 1))
210	209, 141	eqtrdi 2817	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = 0)
211	191, 199, 210	3eqtr4rd 2812	. . . . 5 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
212	211	3exp 1137	. . . 4 ⊢ (𝑁 = 0 → (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))))
213	187, 212	jaoi 871	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))))
214	1, 213	sylbi 220	. 2 ⊢ (𝑁 ∈ ℕ0 → (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))))
215	214	3imp 1128	1 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ∅c0 4289  ‘cfv 6543  (class class class)co 7423  Fincfn 8952  ℂcc 11116  0cc0 11118  1c1 11119   + caddc 11121   · cmul 11123   − cmin 11459  ℕcn 12251  ℕ₀cn0 12522  ℤcz 12609  ℤ_≥cuz 12880  ...cfz 13553  ..^cfzo 13701  ↑cexp 14117  Σcsu 15763

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-inf2 9620  ax-cnex 11174  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194  ax-pre-mulgt0 11195  ax-pre-sup 11196

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-int 4918  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-se 5620  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-1st 7995  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-sup 9412  df-oi 9482  df-card 9944  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11461  df-neg 11462  df-div 11890  df-nn 12252  df-2 12321  df-3 12322  df-n0 12523  df-z 12610  df-uz 12881  df-rp 13035  df-fz 13554  df-fzo 13702  df-seq 14058  df-exp 14118  df-hash 14387  df-cj 15176  df-re 15177  df-im 15178  df-sqrt 15312  df-abs 15313  df-clim 15565  df-sum 15764

This theorem is used by:  pwm1geoser  15949  fltnltalem  43435  2pwp1prm  48382