Theorem pwdif 15208

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 13562. See Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number 13562, 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 11886	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		simp2 1133	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
3		simp3 1134	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
4		fzofi 13332	. . . . . . . . 9 ⊢ (0..^𝑁) ∈ Fin
5	4	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0..^𝑁) ∈ Fin)
6	2	adantr 483	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝐴 ∈ ℂ)
7		elfzonn0 13072	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℕ0)
8	7	adantl 484	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑘 ∈ ℕ0)
9	6, 8	expcld 13500	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴↑𝑘) ∈ ℂ)
10	3	adantr 483	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝐵 ∈ ℂ)
11		ubmelm1fzo 13123	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0..^𝑁) → ((𝑁 − 𝑘) − 1) ∈ (0..^𝑁))
12		elfzonn0 13072	. . . . . . . . . . . 12 ⊢ (((𝑁 − 𝑘) − 1) ∈ (0..^𝑁) → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
13	11, 12	syl 17	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0..^𝑁) → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
14	13	adantl 484	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
15	10, 14	expcld 13500	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵↑((𝑁 − 𝑘) − 1)) ∈ ℂ)
16	9, 15	mulcld 10647	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
17	5, 16	fsumcl 15075	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
18	2, 3, 17	subdird 11083	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) − (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))))
19	5, 2, 16	fsummulc2 15124	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)(𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
20	6, 9, 15	mulassd 10650	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴 · (𝐴↑𝑘)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
21	6, 9	mulcomd 10648	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · (𝐴↑𝑘)) = ((𝐴↑𝑘) · 𝐴))
22		expp1 13426	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
23	2, 7, 22	syl2an 597	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
24	21, 23	eqtr4d 2859	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · (𝐴↑𝑘)) = (𝐴↑(𝑘 + 1)))
25	24	oveq1d 7157	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴 · (𝐴↑𝑘)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
26	20, 25	eqtr3d 2858	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
27	26	sumeq2dv 15045	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)(𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
28	19, 27	eqtrd 2856	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
29	5, 3, 16	fsummulc2 15124	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)(𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
30	10, 16	mulcomd 10648	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = (((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) · 𝐵))
31	9, 15, 10	mulassd 10650	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) · 𝐵) = ((𝐴↑𝑘) · ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵)))
32		expp1 13426	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℂ ∧ ((𝑁 − 𝑘) − 1) ∈ ℕ0) → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵))
33	32	eqcomd 2827	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℂ ∧ ((𝑁 − 𝑘) − 1) ∈ ℕ0) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(((𝑁 − 𝑘) − 1) + 1)))
34	3, 13, 33	syl2an 597	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(((𝑁 − 𝑘) − 1) + 1)))
35		nncn 11632	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
36	35	3ad2ant1 1129	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℂ)
37	36	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑁 ∈ ℂ)
38		elfzoelz 13028	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℤ)
39	38	zcnd 12075	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℂ)
40	39	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑘 ∈ ℂ)
41	37, 40	subcld 10983	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝑁 − 𝑘) ∈ ℂ)
42		npcan1 11051	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 𝑘) ∈ ℂ → (((𝑁 − 𝑘) − 1) + 1) = (𝑁 − 𝑘))
43	42	oveq2d 7158	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 𝑘) ∈ ℂ → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = (𝐵↑(𝑁 − 𝑘)))
44	41, 43	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = (𝐵↑(𝑁 − 𝑘)))
45	34, 44	eqtrd 2856	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(𝑁 − 𝑘)))
46	45	oveq2d 7158	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴↑𝑘) · ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵)) = ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
47	30, 31, 46	3eqtrd 2860	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
48	47	sumeq2dv 15045	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)(𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
49	29, 48	eqtrd 2856	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
50	28, 49	oveq12d 7160	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) − (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))) = (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
51		nnz 11991	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
52	51	3ad2ant1 1129	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℤ)
53		fzoval 13029	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → (0..^𝑁) = (0...(𝑁 − 1)))
54	52, 53	syl 17	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0..^𝑁) = (0...(𝑁 − 1)))
55	54	sumeq1d 15043	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
56		nnm1nn0 11925	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
57		nn0uz 12267	. . . . . . . . . . . 12 ⊢ ℕ0 = (ℤ≥‘0)
58	56, 57	eleqtrdi 2923	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ≥‘0))
59	58	3ad2ant1 1129	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 1) ∈ (ℤ≥‘0))
60	2	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝐴 ∈ ℂ)
61		elfznn0 12990	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
62		peano2nn0 11924	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
63	61, 62	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → (𝑘 + 1) ∈ ℕ0)
64	63	adantl 484	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑘 + 1) ∈ ℕ0)
65	60, 64	expcld 13500	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑(𝑘 + 1)) ∈ ℂ)
66	3	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝐵 ∈ ℂ)
67	36	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℂ)
68	61	nn0cnd 11944	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℂ)
69	68	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℂ)
70		1cnd 10622	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 1 ∈ ℂ)
71	67, 69, 70	sub32d 11015	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 𝑘) − 1) = ((𝑁 − 1) − 𝑘))
72		fznn0sub 12929	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
73	72	adantl 484	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
74	71, 73	eqeltrd 2913	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
75	66, 74	expcld 13500	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐵↑((𝑁 − 𝑘) − 1)) ∈ ℂ)
76	65, 75	mulcld 10647	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
77		oveq1 7149	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑁 − 1) → (𝑘 + 1) = ((𝑁 − 1) + 1))
78	77	oveq2d 7158	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑁 − 1) → (𝐴↑(𝑘 + 1)) = (𝐴↑((𝑁 − 1) + 1)))
79		oveq2 7150	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑁 − 1) → (𝑁 − 𝑘) = (𝑁 − (𝑁 − 1)))
80	79	oveq1d 7157	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑁 − 1) → ((𝑁 − 𝑘) − 1) = ((𝑁 − (𝑁 − 1)) − 1))
81	80	oveq2d 7158	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑁 − 1) → (𝐵↑((𝑁 − 𝑘) − 1)) = (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))
82	78, 81	oveq12d 7160	. . . . . . . . . 10 ⊢ (𝑘 = (𝑁 − 1) → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))))
83	59, 76, 82	fsumm1 15091	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))))
84	55, 83	eqtrd 2856	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))))
85	54	sumeq1d 15043	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
86	61	adantl 484	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0)
87	60, 86	expcld 13500	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑𝑘) ∈ ℂ)
88	54	eleq2d 2898	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (0..^𝑁) ↔ 𝑘 ∈ (0...(𝑁 − 1))))
89		fzonnsub 13052	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑁 − 𝑘) ∈ ℕ)
90	89	nnnn0d 11942	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑁 − 𝑘) ∈ ℕ0)
91	88, 90	syl6bir 256	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (0...(𝑁 − 1)) → (𝑁 − 𝑘) ∈ ℕ0))
92	91	imp 409	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑁 − 𝑘) ∈ ℕ0)
93	66, 92	expcld 13500	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐵↑(𝑁 − 𝑘)) ∈ ℂ)
94	87, 93	mulcld 10647	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
95		oveq2 7150	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (𝐴↑𝑘) = (𝐴↑0))
96		oveq2 7150	. . . . . . . . . . . 12 ⊢ (𝑘 = 0 → (𝑁 − 𝑘) = (𝑁 − 0))
97	96	oveq2d 7158	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (𝐵↑(𝑁 − 𝑘)) = (𝐵↑(𝑁 − 0)))
98	95, 97	oveq12d 7160	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐴↑0) · (𝐵↑(𝑁 − 0))))
99	59, 94, 98	fsum1p 15093	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = (((𝐴↑0) · (𝐵↑(𝑁 − 0))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
100	2	exp0d 13494	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) = 1)
101	36	subid1d 10972	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 0) = 𝑁)
102	101	oveq2d 7158	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑(𝑁 − 0)) = (𝐵↑𝑁))
103	100, 102	oveq12d 7160	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑0) · (𝐵↑(𝑁 − 0))) = (1 · (𝐵↑𝑁)))
104		simp1 1132	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℕ)
105	104	nnnn0d 11942	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℕ0)
106	3, 105	expcld 13500	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) ∈ ℂ)
107	106	mulid2d 10645	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · (𝐵↑𝑁)) = (𝐵↑𝑁))
108	103, 107	eqtrd 2856	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑0) · (𝐵↑(𝑁 − 0))) = (𝐵↑𝑁))
109		0p1e1 11746	. . . . . . . . . . . . 13 ⊢ (0 + 1) = 1
110	109	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0 + 1) = 1)
111	110	oveq1d 7157	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((0 + 1)...(𝑁 − 1)) = (1...(𝑁 − 1)))
112	111	sumeq1d 15043	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
113	108, 112	oveq12d 7160	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑0) · (𝐵↑(𝑁 − 0))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
114	85, 99, 113	3eqtrd 2860	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
115	84, 114	oveq12d 7160	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))))
116		fzfid 13331	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1...(𝑁 − 1)) ∈ Fin)
117	2	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝐴 ∈ ℂ)
118		elfznn 12926	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ)
119	118	nnnn0d 11942	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
120	119	adantl 484	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℕ0)
121	117, 120	expcld 13500	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝐴↑𝑘) ∈ ℂ)
122	3	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝐵 ∈ ℂ)
123		fzoval 13029	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → (1..^𝑁) = (1...(𝑁 − 1)))
124	52, 123	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1..^𝑁) = (1...(𝑁 − 1)))
125	124	eleq2d 2898	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (1..^𝑁) ↔ 𝑘 ∈ (1...(𝑁 − 1))))
126		fzonnsub 13052	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1..^𝑁) → (𝑁 − 𝑘) ∈ ℕ)
127	126	nnnn0d 11942	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1..^𝑁) → (𝑁 − 𝑘) ∈ ℕ0)
128	125, 127	syl6bir 256	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (1...(𝑁 − 1)) → (𝑁 − 𝑘) ∈ ℕ0))
129	128	imp 409	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑁 − 𝑘) ∈ ℕ0)
130	122, 129	expcld 13500	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝐵↑(𝑁 − 𝑘)) ∈ ℂ)
131	121, 130	mulcld 10647	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
132	116, 131	fsumcl 15075	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
133	2, 105	expcld 13500	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) ∈ ℂ)
134		oveq1 7149	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → (𝑘 + 1) = (𝑙 + 1))
135	134	oveq2d 7158	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝐴↑(𝑘 + 1)) = (𝐴↑(𝑙 + 1)))
136		oveq2 7150	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → (𝑁 − 𝑘) = (𝑁 − 𝑙))
137	136	oveq1d 7157	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → ((𝑁 − 𝑘) − 1) = ((𝑁 − 𝑙) − 1))
138	137	oveq2d 7158	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝐵↑((𝑁 − 𝑘) − 1)) = (𝐵↑((𝑁 − 𝑙) − 1)))
139	135, 138	oveq12d 7160	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))))
140	139	cbvsumv 15038	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑙 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1)))
141		1m1e0 11696	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
142	141	eqcomi 2830	. . . . . . . . . . . . . . 15 ⊢ 0 = (1 − 1)
143	142	oveq1i 7152	. . . . . . . . . . . . . 14 ⊢ (0...((𝑁 − 1) − 1)) = ((1 − 1)...((𝑁 − 1) − 1))
144	143	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0...((𝑁 − 1) − 1)) = ((1 − 1)...((𝑁 − 1) − 1)))
145	36	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → 𝑁 ∈ ℂ)
146		elfznn0 12990	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 ∈ (0...((𝑁 − 1) − 1)) → 𝑙 ∈ ℕ0)
147	146	nn0cnd 11944	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 ∈ (0...((𝑁 − 1) − 1)) → 𝑙 ∈ ℂ)
148	147	adantl 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → 𝑙 ∈ ℂ)
149		1cnd 10622	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → 1 ∈ ℂ)
150	145, 148, 149	subsub4d 11014	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → ((𝑁 − 𝑙) − 1) = (𝑁 − (𝑙 + 1)))
151	150	oveq2d 7158	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → (𝐵↑((𝑁 − 𝑙) − 1)) = (𝐵↑(𝑁 − (𝑙 + 1))))
152	151	oveq2d 7158	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → ((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
153	144, 152	sumeq12dv 15048	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑙 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
154	140, 153	syl5eq 2868	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
155		1zzd 12000	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈ ℤ)
156		peano2zm 12012	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
157	52, 156	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 1) ∈ ℤ)
158		oveq2 7150	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑙 + 1) → (𝐴↑𝑘) = (𝐴↑(𝑙 + 1)))
159		oveq2 7150	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑙 + 1) → (𝑁 − 𝑘) = (𝑁 − (𝑙 + 1)))
160	159	oveq2d 7158	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑙 + 1) → (𝐵↑(𝑁 − 𝑘)) = (𝐵↑(𝑁 − (𝑙 + 1))))
161	158, 160	oveq12d 7160	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑙 + 1) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
162	155, 155, 157, 131, 161	fsumshftm 15121	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
163	154, 162	eqtr4d 2859	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
164		npcan1 11051	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
165	36, 164	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
166	165	oveq2d 7158	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑((𝑁 − 1) + 1)) = (𝐴↑𝑁))
167		peano2cnm 10938	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℂ → (𝑁 − 1) ∈ ℂ)
168	35, 167	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℂ)
169		1cnd 10622	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
170	35, 168, 169	sub32d 11015	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((𝑁 − (𝑁 − 1)) − 1) = ((𝑁 − 1) − (𝑁 − 1)))
171	168	subidd 10971	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) − (𝑁 − 1)) = 0)
172	170, 171	eqtrd 2856	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → ((𝑁 − (𝑁 − 1)) − 1) = 0)
173	172	3ad2ant1 1129	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑁 − (𝑁 − 1)) − 1) = 0)
174	173	oveq2d 7158	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑((𝑁 − (𝑁 − 1)) − 1)) = (𝐵↑0))
175		exp0 13423	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℂ → (𝐵↑0) = 1)
176	175	3ad2ant3 1131	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑0) = 1)
177	174, 176	eqtrd 2856	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑((𝑁 − (𝑁 − 1)) − 1)) = 1)
178	166, 177	oveq12d 7160	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))) = ((𝐴↑𝑁) · 1))
179	133	mulid1d 10644	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) · 1) = (𝐴↑𝑁))
180	178, 179	eqtrd 2856	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))) = (𝐴↑𝑁))
181	163, 180	oveq12d 7160	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) = (Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) + (𝐴↑𝑁)))
182	132, 133, 181	comraddd 10840	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) = ((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
183	182	oveq1d 7157	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))) = (((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))))
184	133, 106, 132	pnpcan2d 11021	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))) = ((𝐴↑𝑁) − (𝐵↑𝑁)))
185	115, 183, 184	3eqtrd 2860	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((𝐴↑𝑁) − (𝐵↑𝑁)))
186	18, 50, 185	3eqtrrd 2861	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
187	186	3exp 1115	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))))
188		simp2 1133	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
189		simp3 1134	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
190	188, 189	subcld 10983	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
191	190	mul01d 10825	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · 0) = 0)
192		oveq2 7150	. . . . . . . . . . 11 ⊢ (𝑁 = 0 → (0..^𝑁) = (0..^0))
193		fzo0 13051	. . . . . . . . . . 11 ⊢ (0..^0) = ∅
194	192, 193	syl6eq 2872	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (0..^𝑁) = ∅)
195	194	sumeq1d 15043	. . . . . . . . 9 ⊢ (𝑁 = 0 → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))
196	195	3ad2ant1 1129	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))
197		sum0 15063	. . . . . . . 8 ⊢ Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = 0
198	196, 197	syl6eq 2872	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = 0)
199	198	oveq2d 7158	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴 − 𝐵) · 0))
200		oveq2 7150	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (𝐴↑𝑁) = (𝐴↑0))
201	200	3ad2ant1 1129	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) = (𝐴↑0))
202		exp0 13423	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1)
203	202	3ad2ant2 1130	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) = 1)
204	201, 203	eqtrd 2856	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) = 1)
205		oveq2 7150	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (𝐵↑𝑁) = (𝐵↑0))
206	205	3ad2ant1 1129	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) = (𝐵↑0))
207	175	3ad2ant3 1131	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑0) = 1)
208	206, 207	eqtrd 2856	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) = 1)
209	204, 208	oveq12d 7160	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = (1 − 1))
210	209, 141	syl6eq 2872	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = 0)
211	191, 199, 210	3eqtr4rd 2867	. . . . 5 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
212	211	3exp 1115	. . . 4 ⊢ (𝑁 = 0 → (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))))
213	187, 212	jaoi 853	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))))
214	1, 213	sylbi 219	. 2 ⊢ (𝑁 ∈ ℕ0 → (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))))
215	214	3imp 1107	1 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))

Syntax hints:   → wi 4   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ∅c0 4279  ‘cfv 6341  (class class class)co 7142  Fincfn 8495  ℂcc 10521  0cc0 10523  1c1 10524   + caddc 10526   · cmul 10528   − cmin 10856  ℕcn 11624  ℕ₀cn0 11884  ℤcz 11968  ℤ_≥cuz 12230  ...cfz 12882  ..^cfzo 13023  ↑cexp 13419  Σcsu 15027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447  ax-inf2 9090  ax-cnex 10579  ax-resscn 10580  ax-1cn 10581  ax-icn 10582  ax-addcl 10583  ax-addrcl 10584  ax-mulcl 10585  ax-mulrcl 10586  ax-mulcom 10587  ax-addass 10588  ax-mulass 10589  ax-distr 10590  ax-i2m1 10591  ax-1ne0 10592  ax-1rid 10593  ax-rnegex 10594  ax-rrecex 10595  ax-cnre 10596  ax-pre-lttri 10597  ax-pre-lttrn 10598  ax-pre-ltadd 10599  ax-pre-mulgt0 10600  ax-pre-sup 10601

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-pss 3942  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-tp 4558  df-op 4560  df-uni 4825  df-int 4863  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5446  df-eprel 5451  df-po 5460  df-so 5461  df-fr 5500  df-se 5501  df-we 5502  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-pred 6134  df-ord 6180  df-on 6181  df-lim 6182  df-suc 6183  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-isom 6350  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-om 7567  df-1st 7675  df-2nd 7676  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-oadd 8092  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-sup 8892  df-oi 8960  df-card 9354  df-pnf 10663  df-mnf 10664  df-xr 10665  df-ltxr 10666  df-le 10667  df-sub 10858  df-neg 10859  df-div 11284  df-nn 11625  df-2 11687  df-3 11688  df-n0 11885  df-z 11969  df-uz 12231  df-rp 12377  df-fz 12883  df-fzo 13024  df-seq 13360  df-exp 13420  df-hash 13681  df-cj 14443  df-re 14444  df-im 14445  df-sqrt 14579  df-abs 14580  df-clim 14830  df-sum 15028

This theorem is referenced by:  pwm1geoser  15209  fltnltalem  39366  2pwp1prm  43836