Theorem pwdif 15803

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 14145. See Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number 14145, 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 12415	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		simp2 1138	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
3		simp3 1139	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
4		fzofi 13909	. . . . . . . . 9 ⊢ (0..^𝑁) ∈ Fin
5	4	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0..^𝑁) ∈ Fin)
6	2	adantr 480	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝐴 ∈ ℂ)
7		elfzonn0 13635	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℕ0)
8	7	adantl 481	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑘 ∈ ℕ0)
9	6, 8	expcld 14081	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴↑𝑘) ∈ ℂ)
10	3	adantr 480	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝐵 ∈ ℂ)
11		ubmelm1fzo 13691	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0..^𝑁) → ((𝑁 − 𝑘) − 1) ∈ (0..^𝑁))
12		elfzonn0 13635	. . . . . . . . . . . 12 ⊢ (((𝑁 − 𝑘) − 1) ∈ (0..^𝑁) → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
13	11, 12	syl 17	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0..^𝑁) → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
14	13	adantl 481	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
15	10, 14	expcld 14081	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵↑((𝑁 − 𝑘) − 1)) ∈ ℂ)
16	9, 15	mulcld 11164	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
17	5, 16	fsumcl 15668	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
18	2, 3, 17	subdird 11606	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) − (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))))
19	5, 2, 16	fsummulc2 15719	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)(𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
20	6, 9, 15	mulassd 11167	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴 · (𝐴↑𝑘)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
21	6, 9	mulcomd 11165	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · (𝐴↑𝑘)) = ((𝐴↑𝑘) · 𝐴))
22		expp1 14003	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
23	2, 7, 22	syl2an 597	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
24	21, 23	eqtr4d 2775	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · (𝐴↑𝑘)) = (𝐴↑(𝑘 + 1)))
25	24	oveq1d 7383	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴 · (𝐴↑𝑘)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
26	20, 25	eqtr3d 2774	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
27	26	sumeq2dv 15637	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)(𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
28	19, 27	eqtrd 2772	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
29	5, 3, 16	fsummulc2 15719	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)(𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
30	10, 16	mulcomd 11165	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = (((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) · 𝐵))
31	9, 15, 10	mulassd 11167	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) · 𝐵) = ((𝐴↑𝑘) · ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵)))
32		expp1 14003	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℂ ∧ ((𝑁 − 𝑘) − 1) ∈ ℕ0) → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵))
33	32	eqcomd 2743	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℂ ∧ ((𝑁 − 𝑘) − 1) ∈ ℕ0) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(((𝑁 − 𝑘) − 1) + 1)))
34	3, 13, 33	syl2an 597	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(((𝑁 − 𝑘) − 1) + 1)))
35		nncn 12165	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
36	35	3ad2ant1 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℂ)
37	36	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑁 ∈ ℂ)
38		elfzoelz 13587	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℤ)
39	38	zcnd 12609	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℂ)
40	39	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑘 ∈ ℂ)
41	37, 40	subcld 11504	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝑁 − 𝑘) ∈ ℂ)
42		npcan1 11574	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 𝑘) ∈ ℂ → (((𝑁 − 𝑘) − 1) + 1) = (𝑁 − 𝑘))
43	42	oveq2d 7384	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 𝑘) ∈ ℂ → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = (𝐵↑(𝑁 − 𝑘)))
44	41, 43	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = (𝐵↑(𝑁 − 𝑘)))
45	34, 44	eqtrd 2772	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(𝑁 − 𝑘)))
46	45	oveq2d 7384	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴↑𝑘) · ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵)) = ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
47	30, 31, 46	3eqtrd 2776	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
48	47	sumeq2dv 15637	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)(𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
49	29, 48	eqtrd 2772	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
50	28, 49	oveq12d 7386	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) − (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))) = (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
51		nnz 12521	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
52	51	3ad2ant1 1134	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℤ)
53		fzoval 13588	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → (0..^𝑁) = (0...(𝑁 − 1)))
54	52, 53	syl 17	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0..^𝑁) = (0...(𝑁 − 1)))
55	54	sumeq1d 15635	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
56		nnm1nn0 12454	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
57		nn0uz 12801	. . . . . . . . . . . 12 ⊢ ℕ0 = (ℤ≥‘0)
58	56, 57	eleqtrdi 2847	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ≥‘0))
59	58	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 1) ∈ (ℤ≥‘0))
60	2	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝐴 ∈ ℂ)
61		elfznn0 13548	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
62		peano2nn0 12453	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
63	61, 62	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → (𝑘 + 1) ∈ ℕ0)
64	63	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑘 + 1) ∈ ℕ0)
65	60, 64	expcld 14081	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑(𝑘 + 1)) ∈ ℂ)
66	3	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝐵 ∈ ℂ)
67	36	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℂ)
68	61	nn0cnd 12476	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℂ)
69	68	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℂ)
70		1cnd 11139	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 1 ∈ ℂ)
71	67, 69, 70	sub32d 11536	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 𝑘) − 1) = ((𝑁 − 1) − 𝑘))
72		fznn0sub 13484	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
73	72	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
74	71, 73	eqeltrd 2837	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
75	66, 74	expcld 14081	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐵↑((𝑁 − 𝑘) − 1)) ∈ ℂ)
76	65, 75	mulcld 11164	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
77		oveq1 7375	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑁 − 1) → (𝑘 + 1) = ((𝑁 − 1) + 1))
78	77	oveq2d 7384	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑁 − 1) → (𝐴↑(𝑘 + 1)) = (𝐴↑((𝑁 − 1) + 1)))
79		oveq2 7376	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑁 − 1) → (𝑁 − 𝑘) = (𝑁 − (𝑁 − 1)))
80	79	oveq1d 7383	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑁 − 1) → ((𝑁 − 𝑘) − 1) = ((𝑁 − (𝑁 − 1)) − 1))
81	80	oveq2d 7384	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑁 − 1) → (𝐵↑((𝑁 − 𝑘) − 1)) = (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))
82	78, 81	oveq12d 7386	. . . . . . . . . 10 ⊢ (𝑘 = (𝑁 − 1) → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))))
83	59, 76, 82	fsumm1 15686	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))))
84	55, 83	eqtrd 2772	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))))
85	54	sumeq1d 15635	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
86	61	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0)
87	60, 86	expcld 14081	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑𝑘) ∈ ℂ)
88	54	eleq2d 2823	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (0..^𝑁) ↔ 𝑘 ∈ (0...(𝑁 − 1))))
89		fzonnsub 13612	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑁 − 𝑘) ∈ ℕ)
90	89	nnnn0d 12474	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑁 − 𝑘) ∈ ℕ0)
91	88, 90	biimtrrdi 254	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (0...(𝑁 − 1)) → (𝑁 − 𝑘) ∈ ℕ0))
92	91	imp 406	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑁 − 𝑘) ∈ ℕ0)
93	66, 92	expcld 14081	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐵↑(𝑁 − 𝑘)) ∈ ℂ)
94	87, 93	mulcld 11164	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
95		oveq2 7376	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (𝐴↑𝑘) = (𝐴↑0))
96		oveq2 7376	. . . . . . . . . . . 12 ⊢ (𝑘 = 0 → (𝑁 − 𝑘) = (𝑁 − 0))
97	96	oveq2d 7384	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (𝐵↑(𝑁 − 𝑘)) = (𝐵↑(𝑁 − 0)))
98	95, 97	oveq12d 7386	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐴↑0) · (𝐵↑(𝑁 − 0))))
99	59, 94, 98	fsum1p 15688	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = (((𝐴↑0) · (𝐵↑(𝑁 − 0))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
100	2	exp0d 14075	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) = 1)
101	36	subid1d 11493	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 0) = 𝑁)
102	101	oveq2d 7384	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑(𝑁 − 0)) = (𝐵↑𝑁))
103	100, 102	oveq12d 7386	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑0) · (𝐵↑(𝑁 − 0))) = (1 · (𝐵↑𝑁)))
104		simp1 1137	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℕ)
105	104	nnnn0d 12474	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℕ0)
106	3, 105	expcld 14081	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) ∈ ℂ)
107	106	mullidd 11162	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · (𝐵↑𝑁)) = (𝐵↑𝑁))
108	103, 107	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑0) · (𝐵↑(𝑁 − 0))) = (𝐵↑𝑁))
109		0p1e1 12274	. . . . . . . . . . . . 13 ⊢ (0 + 1) = 1
110	109	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0 + 1) = 1)
111	110	oveq1d 7383	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((0 + 1)...(𝑁 − 1)) = (1...(𝑁 − 1)))
112	111	sumeq1d 15635	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
113	108, 112	oveq12d 7386	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑0) · (𝐵↑(𝑁 − 0))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
114	85, 99, 113	3eqtrd 2776	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
115	84, 114	oveq12d 7386	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))))
116		fzfid 13908	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1...(𝑁 − 1)) ∈ Fin)
117	2	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝐴 ∈ ℂ)
118		elfznn 13481	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ)
119	118	nnnn0d 12474	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
120	119	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℕ0)
121	117, 120	expcld 14081	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝐴↑𝑘) ∈ ℂ)
122	3	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝐵 ∈ ℂ)
123		fzoval 13588	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → (1..^𝑁) = (1...(𝑁 − 1)))
124	52, 123	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1..^𝑁) = (1...(𝑁 − 1)))
125	124	eleq2d 2823	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (1..^𝑁) ↔ 𝑘 ∈ (1...(𝑁 − 1))))
126		fzonnsub 13612	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1..^𝑁) → (𝑁 − 𝑘) ∈ ℕ)
127	126	nnnn0d 12474	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1..^𝑁) → (𝑁 − 𝑘) ∈ ℕ0)
128	125, 127	biimtrrdi 254	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (1...(𝑁 − 1)) → (𝑁 − 𝑘) ∈ ℕ0))
129	128	imp 406	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑁 − 𝑘) ∈ ℕ0)
130	122, 129	expcld 14081	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝐵↑(𝑁 − 𝑘)) ∈ ℂ)
131	121, 130	mulcld 11164	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
132	116, 131	fsumcl 15668	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
133	2, 105	expcld 14081	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) ∈ ℂ)
134		oveq1 7375	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → (𝑘 + 1) = (𝑙 + 1))
135	134	oveq2d 7384	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝐴↑(𝑘 + 1)) = (𝐴↑(𝑙 + 1)))
136		oveq2 7376	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → (𝑁 − 𝑘) = (𝑁 − 𝑙))
137	136	oveq1d 7383	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → ((𝑁 − 𝑘) − 1) = ((𝑁 − 𝑙) − 1))
138	137	oveq2d 7384	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝐵↑((𝑁 − 𝑘) − 1)) = (𝐵↑((𝑁 − 𝑙) − 1)))
139	135, 138	oveq12d 7386	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))))
140	139	cbvsumv 15631	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑙 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1)))
141		1m1e0 12229	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
142	141	eqcomi 2746	. . . . . . . . . . . . . . 15 ⊢ 0 = (1 − 1)
143	142	oveq1i 7378	. . . . . . . . . . . . . 14 ⊢ (0...((𝑁 − 1) − 1)) = ((1 − 1)...((𝑁 − 1) − 1))
144	143	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0...((𝑁 − 1) − 1)) = ((1 − 1)...((𝑁 − 1) − 1)))
145	36	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → 𝑁 ∈ ℂ)
146		elfznn0 13548	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 ∈ (0...((𝑁 − 1) − 1)) → 𝑙 ∈ ℕ0)
147	146	nn0cnd 12476	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 ∈ (0...((𝑁 − 1) − 1)) → 𝑙 ∈ ℂ)
148	147	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → 𝑙 ∈ ℂ)
149		1cnd 11139	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → 1 ∈ ℂ)
150	145, 148, 149	subsub4d 11535	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → ((𝑁 − 𝑙) − 1) = (𝑁 − (𝑙 + 1)))
151	150	oveq2d 7384	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → (𝐵↑((𝑁 − 𝑙) − 1)) = (𝐵↑(𝑁 − (𝑙 + 1))))
152	151	oveq2d 7384	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → ((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
153	144, 152	sumeq12dv 15641	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑙 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
154	140, 153	eqtrid 2784	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
155		1zzd 12534	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈ ℤ)
156		peano2zm 12546	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
157	52, 156	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 1) ∈ ℤ)
158		oveq2 7376	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑙 + 1) → (𝐴↑𝑘) = (𝐴↑(𝑙 + 1)))
159		oveq2 7376	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑙 + 1) → (𝑁 − 𝑘) = (𝑁 − (𝑙 + 1)))
160	159	oveq2d 7384	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑙 + 1) → (𝐵↑(𝑁 − 𝑘)) = (𝐵↑(𝑁 − (𝑙 + 1))))
161	158, 160	oveq12d 7386	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑙 + 1) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
162	155, 155, 157, 131, 161	fsumshftm 15716	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
163	154, 162	eqtr4d 2775	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
164		npcan1 11574	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
165	36, 164	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
166	165	oveq2d 7384	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑((𝑁 − 1) + 1)) = (𝐴↑𝑁))
167		peano2cnm 11459	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℂ → (𝑁 − 1) ∈ ℂ)
168	35, 167	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℂ)
169		1cnd 11139	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
170	35, 168, 169	sub32d 11536	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((𝑁 − (𝑁 − 1)) − 1) = ((𝑁 − 1) − (𝑁 − 1)))
171	168	subidd 11492	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) − (𝑁 − 1)) = 0)
172	170, 171	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → ((𝑁 − (𝑁 − 1)) − 1) = 0)
173	172	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑁 − (𝑁 − 1)) − 1) = 0)
174	173	oveq2d 7384	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑((𝑁 − (𝑁 − 1)) − 1)) = (𝐵↑0))
175		exp0 14000	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℂ → (𝐵↑0) = 1)
176	175	3ad2ant3 1136	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑0) = 1)
177	174, 176	eqtrd 2772	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑((𝑁 − (𝑁 − 1)) − 1)) = 1)
178	166, 177	oveq12d 7386	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))) = ((𝐴↑𝑁) · 1))
179	133	mulridd 11161	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) · 1) = (𝐴↑𝑁))
180	178, 179	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))) = (𝐴↑𝑁))
181	163, 180	oveq12d 7386	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) = (Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) + (𝐴↑𝑁)))
182	132, 133, 181	comraddd 11359	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) = ((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
183	182	oveq1d 7383	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))) = (((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))))
184	133, 106, 132	pnpcan2d 11542	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))) = ((𝐴↑𝑁) − (𝐵↑𝑁)))
185	115, 183, 184	3eqtrd 2776	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((𝐴↑𝑁) − (𝐵↑𝑁)))
186	18, 50, 185	3eqtrrd 2777	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
187	186	3exp 1120	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))))
188		simp2 1138	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
189		simp3 1139	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
190	188, 189	subcld 11504	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
191	190	mul01d 11344	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · 0) = 0)
192		oveq2 7376	. . . . . . . . . . 11 ⊢ (𝑁 = 0 → (0..^𝑁) = (0..^0))
193		fzo0 13611	. . . . . . . . . . 11 ⊢ (0..^0) = ∅
194	192, 193	eqtrdi 2788	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (0..^𝑁) = ∅)
195	194	sumeq1d 15635	. . . . . . . . 9 ⊢ (𝑁 = 0 → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))
196	195	3ad2ant1 1134	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))
197		sum0 15656	. . . . . . . 8 ⊢ Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = 0
198	196, 197	eqtrdi 2788	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = 0)
199	198	oveq2d 7384	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴 − 𝐵) · 0))
200		oveq2 7376	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (𝐴↑𝑁) = (𝐴↑0))
201	200	3ad2ant1 1134	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) = (𝐴↑0))
202		exp0 14000	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1)
203	202	3ad2ant2 1135	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) = 1)
204	201, 203	eqtrd 2772	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) = 1)
205		oveq2 7376	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (𝐵↑𝑁) = (𝐵↑0))
206	205	3ad2ant1 1134	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) = (𝐵↑0))
207	175	3ad2ant3 1136	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑0) = 1)
208	206, 207	eqtrd 2772	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) = 1)
209	204, 208	oveq12d 7386	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = (1 − 1))
210	209, 141	eqtrdi 2788	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = 0)
211	191, 199, 210	3eqtr4rd 2783	. . . . 5 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
212	211	3exp 1120	. . . 4 ⊢ (𝑁 = 0 → (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))))
213	187, 212	jaoi 858	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))))
214	1, 213	sylbi 217	. 2 ⊢ (𝑁 ∈ ℕ0 → (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))))
215	214	3imp 1111	1 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∅c0 4287  ‘cfv 6500  (class class class)co 7368  Fincfn 8895  ℂcc 11036  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043   − cmin 11376  ℕcn 12157  ℕ₀cn0 12413  ℤcz 12500  ℤ_≥cuz 12763  ...cfz 13435  ..^cfzo 13582  ↑cexp 13996  Σcsu 15621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-inf2 9562  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-1st 7943  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-sup 9357  df-oi 9427  df-card 9863  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-div 11807  df-nn 12158  df-2 12220  df-3 12221  df-n0 12414  df-z 12501  df-uz 12764  df-rp 12918  df-fz 13436  df-fzo 13583  df-seq 13937  df-exp 13997  df-hash 14266  df-cj 15034  df-re 15035  df-im 15036  df-sqrt 15170  df-abs 15171  df-clim 15423  df-sum 15622

This theorem is referenced by:  pwm1geoser  15804  fltnltalem  43014  2pwp1prm  47943