Theorem pwdif 15904

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 14249. See Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number 14249, 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 12528	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		simp2 1138	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
3		simp3 1139	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
4		fzofi 14015	. . . . . . . . 9 ⊢ (0..^𝑁) ∈ Fin
5	4	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0..^𝑁) ∈ Fin)
6	2	adantr 480	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝐴 ∈ ℂ)
7		elfzonn0 13747	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℕ0)
8	7	adantl 481	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑘 ∈ ℕ0)
9	6, 8	expcld 14186	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴↑𝑘) ∈ ℂ)
10	3	adantr 480	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝐵 ∈ ℂ)
11		ubmelm1fzo 13802	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0..^𝑁) → ((𝑁 − 𝑘) − 1) ∈ (0..^𝑁))
12		elfzonn0 13747	. . . . . . . . . . . 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 14186	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵↑((𝑁 − 𝑘) − 1)) ∈ ℂ)
16	9, 15	mulcld 11281	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
17	5, 16	fsumcl 15769	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
18	2, 3, 17	subdird 11720	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) − (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))))
19	5, 2, 16	fsummulc2 15820	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)(𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
20	6, 9, 15	mulassd 11284	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴 · (𝐴↑𝑘)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
21	6, 9	mulcomd 11282	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · (𝐴↑𝑘)) = ((𝐴↑𝑘) · 𝐴))
22		expp1 14109	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
23	2, 7, 22	syl2an 596	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
24	21, 23	eqtr4d 2780	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · (𝐴↑𝑘)) = (𝐴↑(𝑘 + 1)))
25	24	oveq1d 7446	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴 · (𝐴↑𝑘)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
26	20, 25	eqtr3d 2779	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
27	26	sumeq2dv 15738	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)(𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
28	19, 27	eqtrd 2777	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
29	5, 3, 16	fsummulc2 15820	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)(𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
30	10, 16	mulcomd 11282	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = (((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) · 𝐵))
31	9, 15, 10	mulassd 11284	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) · 𝐵) = ((𝐴↑𝑘) · ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵)))
32		expp1 14109	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℂ ∧ ((𝑁 − 𝑘) − 1) ∈ ℕ0) → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵))
33	32	eqcomd 2743	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℂ ∧ ((𝑁 − 𝑘) − 1) ∈ ℕ0) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(((𝑁 − 𝑘) − 1) + 1)))
34	3, 13, 33	syl2an 596	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(((𝑁 − 𝑘) − 1) + 1)))
35		nncn 12274	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
36	35	3ad2ant1 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℂ)
37	36	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑁 ∈ ℂ)
38		elfzoelz 13699	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℤ)
39	38	zcnd 12723	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℂ)
40	39	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑘 ∈ ℂ)
41	37, 40	subcld 11620	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝑁 − 𝑘) ∈ ℂ)
42		npcan1 11688	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 𝑘) ∈ ℂ → (((𝑁 − 𝑘) − 1) + 1) = (𝑁 − 𝑘))
43	42	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 𝑘) ∈ ℂ → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = (𝐵↑(𝑁 − 𝑘)))
44	41, 43	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = (𝐵↑(𝑁 − 𝑘)))
45	34, 44	eqtrd 2777	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(𝑁 − 𝑘)))
46	45	oveq2d 7447	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴↑𝑘) · ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵)) = ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
47	30, 31, 46	3eqtrd 2781	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
48	47	sumeq2dv 15738	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)(𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
49	29, 48	eqtrd 2777	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
50	28, 49	oveq12d 7449	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) − (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))) = (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
51		nnz 12634	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
52	51	3ad2ant1 1134	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℤ)
53		fzoval 13700	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → (0..^𝑁) = (0...(𝑁 − 1)))
54	52, 53	syl 17	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0..^𝑁) = (0...(𝑁 − 1)))
55	54	sumeq1d 15736	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
56		nnm1nn0 12567	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
57		nn0uz 12920	. . . . . . . . . . . 12 ⊢ ℕ0 = (ℤ≥‘0)
58	56, 57	eleqtrdi 2851	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ≥‘0))
59	58	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 1) ∈ (ℤ≥‘0))
60	2	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝐴 ∈ ℂ)
61		elfznn0 13660	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
62		peano2nn0 12566	. . . . . . . . . . . . . 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 14186	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑(𝑘 + 1)) ∈ ℂ)
66	3	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝐵 ∈ ℂ)
67	36	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℂ)
68	61	nn0cnd 12589	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℂ)
69	68	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℂ)
70		1cnd 11256	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 1 ∈ ℂ)
71	67, 69, 70	sub32d 11652	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 𝑘) − 1) = ((𝑁 − 1) − 𝑘))
72		fznn0sub 13596	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
73	72	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
74	71, 73	eqeltrd 2841	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
75	66, 74	expcld 14186	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐵↑((𝑁 − 𝑘) − 1)) ∈ ℂ)
76	65, 75	mulcld 11281	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
77		oveq1 7438	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑁 − 1) → (𝑘 + 1) = ((𝑁 − 1) + 1))
78	77	oveq2d 7447	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑁 − 1) → (𝐴↑(𝑘 + 1)) = (𝐴↑((𝑁 − 1) + 1)))
79		oveq2 7439	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑁 − 1) → (𝑁 − 𝑘) = (𝑁 − (𝑁 − 1)))
80	79	oveq1d 7446	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑁 − 1) → ((𝑁 − 𝑘) − 1) = ((𝑁 − (𝑁 − 1)) − 1))
81	80	oveq2d 7447	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑁 − 1) → (𝐵↑((𝑁 − 𝑘) − 1)) = (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))
82	78, 81	oveq12d 7449	. . . . . . . . . 10 ⊢ (𝑘 = (𝑁 − 1) → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))))
83	59, 76, 82	fsumm1 15787	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))))
84	55, 83	eqtrd 2777	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))))
85	54	sumeq1d 15736	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
86	61	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0)
87	60, 86	expcld 14186	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑𝑘) ∈ ℂ)
88	54	eleq2d 2827	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (0..^𝑁) ↔ 𝑘 ∈ (0...(𝑁 − 1))))
89		fzonnsub 13724	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑁 − 𝑘) ∈ ℕ)
90	89	nnnn0d 12587	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑁 − 𝑘) ∈ ℕ0)
91	88, 90	biimtrrdi 254	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (0...(𝑁 − 1)) → (𝑁 − 𝑘) ∈ ℕ0))
92	91	imp 406	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑁 − 𝑘) ∈ ℕ0)
93	66, 92	expcld 14186	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐵↑(𝑁 − 𝑘)) ∈ ℂ)
94	87, 93	mulcld 11281	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
95		oveq2 7439	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (𝐴↑𝑘) = (𝐴↑0))
96		oveq2 7439	. . . . . . . . . . . 12 ⊢ (𝑘 = 0 → (𝑁 − 𝑘) = (𝑁 − 0))
97	96	oveq2d 7447	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (𝐵↑(𝑁 − 𝑘)) = (𝐵↑(𝑁 − 0)))
98	95, 97	oveq12d 7449	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐴↑0) · (𝐵↑(𝑁 − 0))))
99	59, 94, 98	fsum1p 15789	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = (((𝐴↑0) · (𝐵↑(𝑁 − 0))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
100	2	exp0d 14180	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) = 1)
101	36	subid1d 11609	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 0) = 𝑁)
102	101	oveq2d 7447	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑(𝑁 − 0)) = (𝐵↑𝑁))
103	100, 102	oveq12d 7449	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑0) · (𝐵↑(𝑁 − 0))) = (1 · (𝐵↑𝑁)))
104		simp1 1137	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℕ)
105	104	nnnn0d 12587	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℕ0)
106	3, 105	expcld 14186	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) ∈ ℂ)
107	106	mullidd 11279	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · (𝐵↑𝑁)) = (𝐵↑𝑁))
108	103, 107	eqtrd 2777	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑0) · (𝐵↑(𝑁 − 0))) = (𝐵↑𝑁))
109		0p1e1 12388	. . . . . . . . . . . . 13 ⊢ (0 + 1) = 1
110	109	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0 + 1) = 1)
111	110	oveq1d 7446	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((0 + 1)...(𝑁 − 1)) = (1...(𝑁 − 1)))
112	111	sumeq1d 15736	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
113	108, 112	oveq12d 7449	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑0) · (𝐵↑(𝑁 − 0))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
114	85, 99, 113	3eqtrd 2781	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
115	84, 114	oveq12d 7449	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))))
116		fzfid 14014	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1...(𝑁 − 1)) ∈ Fin)
117	2	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝐴 ∈ ℂ)
118		elfznn 13593	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ)
119	118	nnnn0d 12587	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
120	119	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℕ0)
121	117, 120	expcld 14186	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝐴↑𝑘) ∈ ℂ)
122	3	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝐵 ∈ ℂ)
123		fzoval 13700	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → (1..^𝑁) = (1...(𝑁 − 1)))
124	52, 123	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1..^𝑁) = (1...(𝑁 − 1)))
125	124	eleq2d 2827	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (1..^𝑁) ↔ 𝑘 ∈ (1...(𝑁 − 1))))
126		fzonnsub 13724	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1..^𝑁) → (𝑁 − 𝑘) ∈ ℕ)
127	126	nnnn0d 12587	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1..^𝑁) → (𝑁 − 𝑘) ∈ ℕ0)
128	125, 127	biimtrrdi 254	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (1...(𝑁 − 1)) → (𝑁 − 𝑘) ∈ ℕ0))
129	128	imp 406	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑁 − 𝑘) ∈ ℕ0)
130	122, 129	expcld 14186	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝐵↑(𝑁 − 𝑘)) ∈ ℂ)
131	121, 130	mulcld 11281	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
132	116, 131	fsumcl 15769	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
133	2, 105	expcld 14186	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) ∈ ℂ)
134		oveq1 7438	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → (𝑘 + 1) = (𝑙 + 1))
135	134	oveq2d 7447	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝐴↑(𝑘 + 1)) = (𝐴↑(𝑙 + 1)))
136		oveq2 7439	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → (𝑁 − 𝑘) = (𝑁 − 𝑙))
137	136	oveq1d 7446	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → ((𝑁 − 𝑘) − 1) = ((𝑁 − 𝑙) − 1))
138	137	oveq2d 7447	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝐵↑((𝑁 − 𝑘) − 1)) = (𝐵↑((𝑁 − 𝑙) − 1)))
139	135, 138	oveq12d 7449	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))))
140	139	cbvsumv 15732	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑙 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1)))
141		1m1e0 12338	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
142	141	eqcomi 2746	. . . . . . . . . . . . . . 15 ⊢ 0 = (1 − 1)
143	142	oveq1i 7441	. . . . . . . . . . . . . 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 13660	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 ∈ (0...((𝑁 − 1) − 1)) → 𝑙 ∈ ℕ0)
147	146	nn0cnd 12589	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 ∈ (0...((𝑁 − 1) − 1)) → 𝑙 ∈ ℂ)
148	147	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → 𝑙 ∈ ℂ)
149		1cnd 11256	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → 1 ∈ ℂ)
150	145, 148, 149	subsub4d 11651	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → ((𝑁 − 𝑙) − 1) = (𝑁 − (𝑙 + 1)))
151	150	oveq2d 7447	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → (𝐵↑((𝑁 − 𝑙) − 1)) = (𝐵↑(𝑁 − (𝑙 + 1))))
152	151	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → ((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
153	144, 152	sumeq12dv 15742	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑙 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
154	140, 153	eqtrid 2789	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
155		1zzd 12648	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈ ℤ)
156		peano2zm 12660	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
157	52, 156	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 1) ∈ ℤ)
158		oveq2 7439	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑙 + 1) → (𝐴↑𝑘) = (𝐴↑(𝑙 + 1)))
159		oveq2 7439	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑙 + 1) → (𝑁 − 𝑘) = (𝑁 − (𝑙 + 1)))
160	159	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑙 + 1) → (𝐵↑(𝑁 − 𝑘)) = (𝐵↑(𝑁 − (𝑙 + 1))))
161	158, 160	oveq12d 7449	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑙 + 1) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
162	155, 155, 157, 131, 161	fsumshftm 15817	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
163	154, 162	eqtr4d 2780	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
164		npcan1 11688	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
165	36, 164	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
166	165	oveq2d 7447	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑((𝑁 − 1) + 1)) = (𝐴↑𝑁))
167		peano2cnm 11575	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℂ → (𝑁 − 1) ∈ ℂ)
168	35, 167	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℂ)
169		1cnd 11256	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
170	35, 168, 169	sub32d 11652	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((𝑁 − (𝑁 − 1)) − 1) = ((𝑁 − 1) − (𝑁 − 1)))
171	168	subidd 11608	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) − (𝑁 − 1)) = 0)
172	170, 171	eqtrd 2777	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → ((𝑁 − (𝑁 − 1)) − 1) = 0)
173	172	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑁 − (𝑁 − 1)) − 1) = 0)
174	173	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑((𝑁 − (𝑁 − 1)) − 1)) = (𝐵↑0))
175		exp0 14106	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℂ → (𝐵↑0) = 1)
176	175	3ad2ant3 1136	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑0) = 1)
177	174, 176	eqtrd 2777	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑((𝑁 − (𝑁 − 1)) − 1)) = 1)
178	166, 177	oveq12d 7449	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))) = ((𝐴↑𝑁) · 1))
179	133	mulridd 11278	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) · 1) = (𝐴↑𝑁))
180	178, 179	eqtrd 2777	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))) = (𝐴↑𝑁))
181	163, 180	oveq12d 7449	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) = (Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) + (𝐴↑𝑁)))
182	132, 133, 181	comraddd 11475	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) = ((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
183	182	oveq1d 7446	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))) = (((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))))
184	133, 106, 132	pnpcan2d 11658	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))) = ((𝐴↑𝑁) − (𝐵↑𝑁)))
185	115, 183, 184	3eqtrd 2781	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((𝐴↑𝑁) − (𝐵↑𝑁)))
186	18, 50, 185	3eqtrrd 2782	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
187	186	3exp 1120	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))))
188		simp2 1138	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
189		simp3 1139	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
190	188, 189	subcld 11620	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
191	190	mul01d 11460	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · 0) = 0)
192		oveq2 7439	. . . . . . . . . . 11 ⊢ (𝑁 = 0 → (0..^𝑁) = (0..^0))
193		fzo0 13723	. . . . . . . . . . 11 ⊢ (0..^0) = ∅
194	192, 193	eqtrdi 2793	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (0..^𝑁) = ∅)
195	194	sumeq1d 15736	. . . . . . . . 9 ⊢ (𝑁 = 0 → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))
196	195	3ad2ant1 1134	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))
197		sum0 15757	. . . . . . . 8 ⊢ Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = 0
198	196, 197	eqtrdi 2793	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = 0)
199	198	oveq2d 7447	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴 − 𝐵) · 0))
200		oveq2 7439	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (𝐴↑𝑁) = (𝐴↑0))
201	200	3ad2ant1 1134	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) = (𝐴↑0))
202		exp0 14106	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1)
203	202	3ad2ant2 1135	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) = 1)
204	201, 203	eqtrd 2777	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) = 1)
205		oveq2 7439	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (𝐵↑𝑁) = (𝐵↑0))
206	205	3ad2ant1 1134	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) = (𝐵↑0))
207	175	3ad2ant3 1136	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑0) = 1)
208	206, 207	eqtrd 2777	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) = 1)
209	204, 208	oveq12d 7449	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = (1 − 1))
210	209, 141	eqtrdi 2793	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = 0)
211	191, 199, 210	3eqtr4rd 2788	. . . . 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 1540   ∈ wcel 2108  ∅c0 4333  ‘cfv 6561  (class class class)co 7431  Fincfn 8985  ℂcc 11153  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   − cmin 11492  ℕcn 12266  ℕ₀cn0 12526  ℤcz 12613  ℤ_≥cuz 12878  ...cfz 13547  ..^cfzo 13694  ↑cexp 14102  Σcsu 15722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-rp 13035  df-fz 13548  df-fzo 13695  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723

This theorem is referenced by:  pwm1geoser  15905  fltnltalem  42672  2pwp1prm  47576