Theorem pwdif 16069

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 14384. See Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number 14384, 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 12638	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		simp2 1155	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
3		simp3 1156	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
4		fzofi 14147	. . . . . . . . 9 ⊢ (0..^𝑁) ∈ Fin
5	4	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0..^𝑁) ∈ Fin)
6	2	adantr 486	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝐴 ∈ ℂ)
7		elfzonn0 13872	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℕ0)
8	7	adantl 487	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑘 ∈ ℕ0)
9	6, 8	expcld 14319	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴↑𝑘) ∈ ℂ)
10	3	adantr 486	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝐵 ∈ ℂ)
11		ubmelm1fzo 13928	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0..^𝑁) → ((𝑁 − 𝑘) − 1) ∈ (0..^𝑁))
12		elfzonn0 13872	. . . . . . . . . . . 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 14319	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵↑((𝑁 − 𝑘) − 1)) ∈ ℂ)
16	9, 15	mulcld 11359	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
17	5, 16	fsumcl 15931	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
18	2, 3, 17	subdird 11803	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) − (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))))
19	5, 2, 16	fsummulc2 15982	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)(𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
20	6, 9, 15	mulassd 11362	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴 · (𝐴↑𝑘)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
21	6, 9	mulcomd 11360	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · (𝐴↑𝑘)) = ((𝐴↑𝑘) · 𝐴))
22		expp1 14241	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
23	2, 7, 22	syl2an 608	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
24	21, 23	eqtr4d 2801	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · (𝐴↑𝑘)) = (𝐴↑(𝑘 + 1)))
25	24	oveq1d 7461	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴 · (𝐴↑𝑘)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
26	20, 25	eqtr3d 2800	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
27	26	sumeq2dv 15901	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)(𝐴 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
28	19, 27	eqtrd 2798	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
29	5, 3, 16	fsummulc2 15982	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)(𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
30	10, 16	mulcomd 11360	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = (((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) · 𝐵))
31	9, 15, 10	mulassd 11362	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) · 𝐵) = ((𝐴↑𝑘) · ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵)))
32		expp1 14241	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℂ ∧ ((𝑁 − 𝑘) − 1) ∈ ℕ0) → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵))
33	32	eqcomd 2769	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℂ ∧ ((𝑁 − 𝑘) − 1) ∈ ℕ0) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(((𝑁 − 𝑘) − 1) + 1)))
34	3, 13, 33	syl2an 608	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(((𝑁 − 𝑘) − 1) + 1)))
35		nncn 12373	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
36	35	3ad2ant1 1151	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℂ)
37	36	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑁 ∈ ℂ)
38		elfzoelz 13823	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℤ)
39	38	zcnd 12834	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℂ)
40	39	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → 𝑘 ∈ ℂ)
41	37, 40	subcld 11699	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝑁 − 𝑘) ∈ ℂ)
42		npcan1 11771	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 𝑘) ∈ ℂ → (((𝑁 − 𝑘) − 1) + 1) = (𝑁 − 𝑘))
43	42	oveq2d 7462	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 𝑘) ∈ ℂ → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = (𝐵↑(𝑁 − 𝑘)))
44	41, 43	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵↑(((𝑁 − 𝑘) − 1) + 1)) = (𝐵↑(𝑁 − 𝑘)))
45	34, 44	eqtrd 2798	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵) = (𝐵↑(𝑁 − 𝑘)))
46	45	oveq2d 7462	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐴↑𝑘) · ((𝐵↑((𝑁 − 𝑘) − 1)) · 𝐵)) = ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
47	30, 31, 46	3eqtrd 2802	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
48	47	sumeq2dv 15901	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)(𝐵 · ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
49	29, 48	eqtrd 2798	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
50	28, 49	oveq12d 7464	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) − (𝐵 · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))) = (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
51		nnz 12744	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
52	51	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℤ)
53		fzoval 13824	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → (0..^𝑁) = (0...(𝑁 − 1)))
54	52, 53	syl 18	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0..^𝑁) = (0...(𝑁 − 1)))
55	54	sumeq1d 15899	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))))
56		nnm1nn0 12677	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
57		nn0uz 13033	. . . . . . . . . . . 12 ⊢ ℕ0 = (ℤ≥‘0)
58	56, 57	eleqtrdi 2874	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ≥‘0))
59	58	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 1) ∈ (ℤ≥‘0))
60	2	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝐴 ∈ ℂ)
61		elfznn0 13784	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
62		peano2nn0 12676	. . . . . . . . . . . . . 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 14319	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑(𝑘 + 1)) ∈ ℂ)
66	3	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝐵 ∈ ℂ)
67	36	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℂ)
68	61	nn0cnd 12699	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℂ)
69	68	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℂ)
70		1cnd 11332	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 1 ∈ ℂ)
71	67, 69, 70	sub32d 11731	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 𝑘) − 1) = ((𝑁 − 1) − 𝑘))
72		fznn0sub 13720	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
73	72	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
74	71, 73	eqeltrd 2864	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
75	66, 74	expcld 14319	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐵↑((𝑁 − 𝑘) − 1)) ∈ ℂ)
76	65, 75	mulcld 11359	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈ ℂ)
77		oveq1 7453	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑁 − 1) → (𝑘 + 1) = ((𝑁 − 1) + 1))
78	77	oveq2d 7462	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑁 − 1) → (𝐴↑(𝑘 + 1)) = (𝐴↑((𝑁 − 1) + 1)))
79		oveq2 7454	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑁 − 1) → (𝑁 − 𝑘) = (𝑁 − (𝑁 − 1)))
80	79	oveq1d 7461	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑁 − 1) → ((𝑁 − 𝑘) − 1) = ((𝑁 − (𝑁 − 1)) − 1))
81	80	oveq2d 7462	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑁 − 1) → (𝐵↑((𝑁 − 𝑘) − 1)) = (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))
82	78, 81	oveq12d 7464	. . . . . . . . . 10 ⊢ (𝑘 = (𝑁 − 1) → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))))
83	59, 76, 82	fsumm1 15949	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))))
84	55, 83	eqtrd 2798	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))))
85	54	sumeq1d 15899	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
86	61	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0)
87	60, 86	expcld 14319	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑𝑘) ∈ ℂ)
88	54	eleq2d 2850	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (0..^𝑁) ↔ 𝑘 ∈ (0...(𝑁 − 1))))
89		fzonnsub 13849	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑁 − 𝑘) ∈ ℕ)
90	89	nnnn0d 12697	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑁 − 𝑘) ∈ ℕ0)
91	88, 90	biimtrrdi 257	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (0...(𝑁 − 1)) → (𝑁 − 𝑘) ∈ ℕ0))
92	91	imp 412	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑁 − 𝑘) ∈ ℕ0)
93	66, 92	expcld 14319	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐵↑(𝑁 − 𝑘)) ∈ ℂ)
94	87, 93	mulcld 11359	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
95		oveq2 7454	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (𝐴↑𝑘) = (𝐴↑0))
96		oveq2 7454	. . . . . . . . . . . 12 ⊢ (𝑘 = 0 → (𝑁 − 𝑘) = (𝑁 − 0))
97	96	oveq2d 7462	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (𝐵↑(𝑁 − 𝑘)) = (𝐵↑(𝑁 − 0)))
98	95, 97	oveq12d 7464	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐴↑0) · (𝐵↑(𝑁 − 0))))
99	59, 94, 98	fsum1p 15951	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = (((𝐴↑0) · (𝐵↑(𝑁 − 0))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
100	2	exp0d 14313	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) = 1)
101	36	subid1d 11688	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 0) = 𝑁)
102	101	oveq2d 7462	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑(𝑁 − 0)) = (𝐵↑𝑁))
103	100, 102	oveq12d 7464	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑0) · (𝐵↑(𝑁 − 0))) = (1 · (𝐵↑𝑁)))
104		simp1 1154	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℕ)
105	104	nnnn0d 12697	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℕ0)
106	3, 105	expcld 14319	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) ∈ ℂ)
107	106	mullidd 11357	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · (𝐵↑𝑁)) = (𝐵↑𝑁))
108	103, 107	eqtrd 2798	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑0) · (𝐵↑(𝑁 − 0))) = (𝐵↑𝑁))
109		0p1e1 12493	. . . . . . . . . . . . 13 ⊢ (0 + 1) = 1
110	109	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (0 + 1) = 1)
111	110	oveq1d 7461	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((0 + 1)...(𝑁 − 1)) = (1...(𝑁 − 1)))
112	111	sumeq1d 15899	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
113	108, 112	oveq12d 7464	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑0) · (𝐵↑(𝑁 − 0))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
114	85, 99, 113	3eqtrd 2802	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
115	84, 114	oveq12d 7464	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))))
116		fzfid 14146	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1...(𝑁 − 1)) ∈ Fin)
117	2	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝐴 ∈ ℂ)
118		elfznn 13717	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ)
119	118	nnnn0d 12697	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
120	119	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℕ0)
121	117, 120	expcld 14319	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝐴↑𝑘) ∈ ℂ)
122	3	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝐵 ∈ ℂ)
123		fzoval 13824	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → (1..^𝑁) = (1...(𝑁 − 1)))
124	52, 123	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1..^𝑁) = (1...(𝑁 − 1)))
125	124	eleq2d 2850	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (1..^𝑁) ↔ 𝑘 ∈ (1...(𝑁 − 1))))
126		fzonnsub 13849	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1..^𝑁) → (𝑁 − 𝑘) ∈ ℕ)
127	126	nnnn0d 12697	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1..^𝑁) → (𝑁 − 𝑘) ∈ ℕ0)
128	125, 127	biimtrrdi 257	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ (1...(𝑁 − 1)) → (𝑁 − 𝑘) ∈ ℕ0))
129	128	imp 412	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑁 − 𝑘) ∈ ℕ0)
130	122, 129	expcld 14319	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝐵↑(𝑁 − 𝑘)) ∈ ℂ)
131	121, 130	mulcld 11359	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
132	116, 131	fsumcl 15931	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) ∈ ℂ)
133	2, 105	expcld 14319	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) ∈ ℂ)
134		oveq1 7453	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → (𝑘 + 1) = (𝑙 + 1))
135	134	oveq2d 7462	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝐴↑(𝑘 + 1)) = (𝐴↑(𝑙 + 1)))
136		oveq2 7454	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → (𝑁 − 𝑘) = (𝑁 − 𝑙))
137	136	oveq1d 7461	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → ((𝑁 − 𝑘) − 1) = ((𝑁 − 𝑙) − 1))
138	137	oveq2d 7462	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝐵↑((𝑁 − 𝑘) − 1)) = (𝐵↑((𝑁 − 𝑙) − 1)))
139	135, 138	oveq12d 7464	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → ((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))))
140	139	cbvsumv 15895	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑙 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1)))
141		1m1e0 12445	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
142	141	eqcomi 2772	. . . . . . . . . . . . . . 15 ⊢ 0 = (1 − 1)
143	142	oveq1i 7456	. . . . . . . . . . . . . 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 13784	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 ∈ (0...((𝑁 − 1) − 1)) → 𝑙 ∈ ℕ0)
147	146	nn0cnd 12699	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 ∈ (0...((𝑁 − 1) − 1)) → 𝑙 ∈ ℂ)
148	147	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → 𝑙 ∈ ℂ)
149		1cnd 11332	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → 1 ∈ ℂ)
150	145, 148, 149	subsub4d 11730	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → ((𝑁 − 𝑙) − 1) = (𝑁 − (𝑙 + 1)))
151	150	oveq2d 7462	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → (𝐵↑((𝑁 − 𝑙) − 1)) = (𝐵↑(𝑁 − (𝑙 + 1))))
152	151	oveq2d 7462	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑙 ∈ (0...((𝑁 − 1) − 1))) → ((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
153	144, 152	sumeq12dv 15904	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑙 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑((𝑁 − 𝑙) − 1))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
154	140, 153	eqtrid 2810	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
155		1zzd 12757	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈ ℤ)
156		peano2zm 12769	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
157	52, 156	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 − 1) ∈ ℤ)
158		oveq2 7454	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑙 + 1) → (𝐴↑𝑘) = (𝐴↑(𝑙 + 1)))
159		oveq2 7454	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑙 + 1) → (𝑁 − 𝑘) = (𝑁 − (𝑙 + 1)))
160	159	oveq2d 7462	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑙 + 1) → (𝐵↑(𝑁 − 𝑘)) = (𝐵↑(𝑁 − (𝑙 + 1))))
161	158, 160	oveq12d 7464	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑙 + 1) → ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = ((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
162	155, 155, 157, 131, 161	fsumshftm 15979	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) = Σ𝑙 ∈ ((1 − 1)...((𝑁 − 1) − 1))((𝐴↑(𝑙 + 1)) · (𝐵↑(𝑁 − (𝑙 + 1)))))
163	154, 162	eqtr4d 2801	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))
164		npcan1 11771	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
165	36, 164	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
166	165	oveq2d 7462	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑((𝑁 − 1) + 1)) = (𝐴↑𝑁))
167		peano2cnm 11654	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℂ → (𝑁 − 1) ∈ ℂ)
168	35, 167	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℂ)
169		1cnd 11332	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
170	35, 168, 169	sub32d 11731	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((𝑁 − (𝑁 − 1)) − 1) = ((𝑁 − 1) − (𝑁 − 1)))
171	168	subidd 11687	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) − (𝑁 − 1)) = 0)
172	170, 171	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → ((𝑁 − (𝑁 − 1)) − 1) = 0)
173	172	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑁 − (𝑁 − 1)) − 1) = 0)
174	173	oveq2d 7462	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑((𝑁 − (𝑁 − 1)) − 1)) = (𝐵↑0))
175		exp0 14238	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℂ → (𝐵↑0) = 1)
176	175	3ad2ant3 1153	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑0) = 1)
177	174, 176	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑((𝑁 − (𝑁 − 1)) − 1)) = 1)
178	166, 177	oveq12d 7464	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))) = ((𝐴↑𝑁) · 1))
179	133	mulridd 11356	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) · 1) = (𝐴↑𝑁))
180	178, 179	eqtrd 2798	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))) = (𝐴↑𝑁))
181	163, 180	oveq12d 7464	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) = (Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))) + (𝐴↑𝑁)))
182	132, 133, 181	comraddd 11554	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) = ((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))))
183	182	oveq1d 7461	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((Σ𝑘 ∈ (0...((𝑁 − 1) − 1))((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐴↑((𝑁 − 1) + 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))) = (((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))))
184	133, 106, 132	pnpcan2d 11737	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) − ((𝐵↑𝑁) + Σ𝑘 ∈ (1...(𝑁 − 1))((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘))))) = ((𝐴↑𝑁) − (𝐵↑𝑁)))
185	115, 183, 184	3eqtrd 2802	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (Σ𝑘 ∈ (0..^𝑁)((𝐴↑(𝑘 + 1)) · (𝐵↑((𝑁 − 𝑘) − 1))) − Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)))) = ((𝐴↑𝑁) − (𝐵↑𝑁)))
186	18, 50, 185	3eqtrrd 2803	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))
187	186	3exp 1137	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))))))
188		simp2 1155	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
189		simp3 1156	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
190	188, 189	subcld 11699	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
191	190	mul01d 11539	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · 0) = 0)
192		oveq2 7454	. . . . . . . . . . 11 ⊢ (𝑁 = 0 → (0..^𝑁) = (0..^0))
193		fzo0 13848	. . . . . . . . . . 11 ⊢ (0..^0) = ∅
194	192, 193	eqtrdi 2814	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (0..^𝑁) = ∅)
195	194	sumeq1d 15899	. . . . . . . . 9 ⊢ (𝑁 = 0 → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))
196	195	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))
197		sum0 15919	. . . . . . . 8 ⊢ Σ𝑘 ∈ ∅ ((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = 0
198	196, 197	eqtrdi 2814	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = 0)
199	198	oveq2d 7462	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) = ((𝐴 − 𝐵) · 0))
200		oveq2 7454	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (𝐴↑𝑁) = (𝐴↑0))
201	200	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) = (𝐴↑0))
202		exp0 14238	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1)
203	202	3ad2ant2 1152	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) = 1)
204	201, 203	eqtrd 2798	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑁) = 1)
205		oveq2 7454	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (𝐵↑𝑁) = (𝐵↑0))
206	205	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) = (𝐵↑0))
207	175	3ad2ant3 1153	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑0) = 1)
208	206, 207	eqtrd 2798	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑁) = 1)
209	204, 208	oveq12d 7464	. . . . . . 7 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = (1 − 1))
210	209, 141	eqtrdi 2814	. . . . . 6 ⊢ ((𝑁 = 0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = 0)
211	191, 199, 210	3eqtr4rd 2809	. . . . 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 2147  ∅c0 4281  ‘cfv 6561  (class class class)co 7446  Fincfn 9004  ℂcc 11228  0cc0 11230  1c1 11231   + caddc 11233   · cmul 11235   − cmin 11571  ℕcn 12365  ℕ₀cn0 12636  ℤcz 12723  ℤ_≥cuz 12995  ...cfz 13669  ..^cfzo 13818  ↑cexp 14234  Σcsu 15885

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5236  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-inf2 9672  ax-cnex 11286  ax-resscn 11287  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-addrcl 11291  ax-mulcl 11292  ax-mulrcl 11293  ax-mulcom 11294  ax-addass 11295  ax-mulass 11296  ax-distr 11297  ax-i2m1 11298  ax-1ne0 11299  ax-1rid 11300  ax-rnegex 11301  ax-rrecex 11302  ax-cnre 11303  ax-pre-lttri 11304  ax-pre-lttrn 11305  ax-pre-ltadd 11306  ax-pre-mulgt0 11307  ax-pre-sup 11308

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-se 5610  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6325  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6515  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 7403  df-ov 7449  df-oprab 7450  df-mpo 7451  df-om 7905  df-1st 8028  df-2nd 8029  df-frecs 8330  df-wrecs 8361  df-recs 8410  df-rdg 8449  df-1o 8507  df-er 8748  df-en 9005  df-dom 9006  df-sdom 9007  df-fin 9008  df-sup 9464  df-oi 9534  df-card 10050  df-pnf 11375  df-mnf 11376  df-xr 11377  df-ltxr 11378  df-le 11379  df-sub 11573  df-neg 11574  df-div 12004  df-nn 12366  df-2 12435  df-3 12436  df-n0 12637  df-z 12724  df-uz 12996  df-rp 13151  df-fz 13670  df-fzo 13819  df-seq 14175  df-exp 14235  df-hash 14505  df-cj 15298  df-re 15299  df-im 15300  df-sqrt 15434  df-abs 15435  df-clim 15687  df-sum 15886

This theorem is used by:  pwm1geoser  16070  fltnltalem  43877  2pwp1prm  48889