pwdif

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

		Ref	Expression
	Assertion	pwdif	$⊢ (N \in ℕ_{0} \land A \in ℂ \land B \in ℂ) \to A^{N} - B^{N} = (A - B) \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1}$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		simp2	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A \in ℂ$
3		simp3	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to B \in ℂ$
4		fzofi	$⊢ (0 ..^N) \in Fin$
5	4	a1i	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to (0 ..^N) \in Fin$
6	2	adantr	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to A \in ℂ$
7		elfzonn0	$⊢ k \in (0 ..^N) \to k \in ℕ_{0}$
8	7	adantl	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to k \in ℕ_{0}$
9	6 8	expcld	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to A^{k} \in ℂ$
10	3	adantr	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to B \in ℂ$
11		ubmelm1fzo	$⊢ k \in (0 ..^N) \to N - k - 1 \in (0 ..^N)$
12		elfzonn0	$⊢ N - k - 1 \in (0 ..^N) \to N - k - 1 \in ℕ_{0}$
13	11 12	syl	$⊢ k \in (0 ..^N) \to N - k - 1 \in ℕ_{0}$
14	13	adantl	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to N - k - 1 \in ℕ_{0}$
15	10 14	expcld	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to B^{N - k - 1} \in ℂ$
16	9 15	mulcld	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to A^{k} B^{N - k - 1} \in ℂ$
17	5 16	fsumcl	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1} \in ℂ$
18	2 3 17	subdird	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to (A - B) \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1} = A \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1} - B \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1}$
19	5 2 16	fsummulc2	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1} = \sum_{k \in (0 ..^N)} A A^{k} B^{N - k - 1}$
20	6 9 15	mulassd	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to A A^{k} B^{N - k - 1} = A A^{k} B^{N - k - 1}$
21	6 9	mulcomd	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to A A^{k} = A^{k} A$
22		expp1	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k + 1} = A^{k} A$
23	2 7 22	syl2an	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to A^{k + 1} = A^{k} A$
24	21 23	eqtr4d	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to A A^{k} = A^{k + 1}$
25	24	oveq1d	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to A A^{k} B^{N - k - 1} = A^{k + 1} B^{N - k - 1}$
26	20 25	eqtr3d	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to A A^{k} B^{N - k - 1} = A^{k + 1} B^{N - k - 1}$
27	26	sumeq2dv	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k \in (0 ..^N)} A A^{k} B^{N - k - 1} = \sum_{k \in (0 ..^N)} A^{k + 1} B^{N - k - 1}$
28	19 27	eqtrd	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1} = \sum_{k \in (0 ..^N)} A^{k + 1} B^{N - k - 1}$
29	5 3 16	fsummulc2	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to B \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1} = \sum_{k \in (0 ..^N)} B A^{k} B^{N - k - 1}$
30	10 16	mulcomd	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to B A^{k} B^{N - k - 1} = A^{k} B^{N - k - 1} B$
31	9 15 10	mulassd	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to A^{k} B^{N - k - 1} B = A^{k} B^{N - k - 1} B$
32		expp1	$⊢ (B \in ℂ \land N - k - 1 \in ℕ_{0}) \to B^{(N - k) - 1 + 1} = B^{N - k - 1} B$
33	32	eqcomd	$⊢ (B \in ℂ \land N - k - 1 \in ℕ_{0}) \to B^{N - k - 1} B = B^{(N - k) - 1 + 1}$
34	3 13 33	syl2an	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to B^{N - k - 1} B = B^{(N - k) - 1 + 1}$
35		nncn	$⊢ N \in ℕ \to N \in ℂ$
36	35	3ad2ant1	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to N \in ℂ$
37	36	adantr	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to N \in ℂ$
38		elfzoelz	$⊢ k \in (0 ..^N) \to k \in ℤ$
39	38	zcnd	$⊢ k \in (0 ..^N) \to k \in ℂ$
40	39	adantl	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to k \in ℂ$
41	37 40	subcld	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to N - k \in ℂ$
42		npcan1	$⊢ N - k \in ℂ \to (N - k) - 1 + 1 = N - k$
43	42	oveq2d	$⊢ N - k \in ℂ \to B^{(N - k) - 1 + 1} = B^{N - k}$
44	41 43	syl	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to B^{(N - k) - 1 + 1} = B^{N - k}$
45	34 44	eqtrd	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to B^{N - k - 1} B = B^{N - k}$
46	45	oveq2d	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to A^{k} B^{N - k - 1} B = A^{k} B^{N - k}$
47	30 31 46	3eqtrd	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 ..^N)) \to B A^{k} B^{N - k - 1} = A^{k} B^{N - k}$
48	47	sumeq2dv	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k \in (0 ..^N)} B A^{k} B^{N - k - 1} = \sum_{k \in (0 ..^N)} A^{k} B^{N - k}$
49	29 48	eqtrd	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to B \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1} = \sum_{k \in (0 ..^N)} A^{k} B^{N - k}$
50	28 49	oveq12d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1} - B \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1} = \sum_{k \in (0 ..^N)} A^{k + 1} B^{N - k - 1} - \sum_{k \in (0 ..^N)} A^{k} B^{N - k}$
51		nnz	$⊢ N \in ℕ \to N \in ℤ$
52	51	3ad2ant1	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to N \in ℤ$
53		fzoval	$⊢ N \in ℤ \to (0 ..^N) = (0 \dots N - 1)$
54	52 53	syl	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to (0 ..^N) = (0 \dots N - 1)$
55	54	sumeq1d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k \in (0 ..^N)} A^{k + 1} B^{N - k - 1} = \sum_{k = 0}^{N - 1} A^{k + 1} B^{N - k - 1}$
56		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
57		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
58	56 57	eleqtrdi	$⊢ N \in ℕ \to N - 1 \in ℤ_{\geq 0}$
59	58	3ad2ant1	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to N - 1 \in ℤ_{\geq 0}$
60	2	adantr	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to A \in ℂ$
61		elfznn0	$⊢ k \in (0 \dots N - 1) \to k \in ℕ_{0}$
62		peano2nn0	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ_{0}$
63	61 62	syl	$⊢ k \in (0 \dots N - 1) \to k + 1 \in ℕ_{0}$
64	63	adantl	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to k + 1 \in ℕ_{0}$
65	60 64	expcld	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to A^{k + 1} \in ℂ$
66	3	adantr	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to B \in ℂ$
67	36	adantr	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to N \in ℂ$
68	61	nn0cnd	$⊢ k \in (0 \dots N - 1) \to k \in ℂ$
69	68	adantl	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to k \in ℂ$
70		1cnd	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to 1 \in ℂ$
71	67 69 70	sub32d	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to N - k - 1 = N - 1 - k$
72		fznn0sub	$⊢ k \in (0 \dots N - 1) \to N - 1 - k \in ℕ_{0}$
73	72	adantl	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to N - 1 - k \in ℕ_{0}$
74	71 73	eqeltrd	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to N - k - 1 \in ℕ_{0}$
75	66 74	expcld	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to B^{N - k - 1} \in ℂ$
76	65 75	mulcld	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to A^{k + 1} B^{N - k - 1} \in ℂ$
77		oveq1	$⊢ k = N - 1 \to k + 1 = N - 1 + 1$
78	77	oveq2d	$⊢ k = N - 1 \to A^{k + 1} = A^{N - 1 + 1}$
79		oveq2	$⊢ k = N - 1 \to N - k = N - (N - 1)$
80	79	oveq1d	$⊢ k = N - 1 \to N - k - 1 = N - (N - 1) - 1$
81	80	oveq2d	$⊢ k = N - 1 \to B^{N - k - 1} = B^{N - (N - 1) - 1}$
82	78 81	oveq12d	$⊢ k = N - 1 \to A^{k + 1} B^{N - k - 1} = A^{N - 1 + 1} B^{N - (N - 1) - 1}$
83	59 76 82	fsumm1	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k = 0}^{N - 1} A^{k + 1} B^{N - k - 1} = \sum_{k = 0}^{N - 1 - 1} A^{k + 1} B^{N - k - 1} + A^{N - 1 + 1} B^{N - (N - 1) - 1}$
84	55 83	eqtrd	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k \in (0 ..^N)} A^{k + 1} B^{N - k - 1} = \sum_{k = 0}^{N - 1 - 1} A^{k + 1} B^{N - k - 1} + A^{N - 1 + 1} B^{N - (N - 1) - 1}$
85	54	sumeq1d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k \in (0 ..^N)} A^{k} B^{N - k} = \sum_{k = 0}^{N - 1} A^{k} B^{N - k}$
86	61	adantl	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to k \in ℕ_{0}$
87	60 86	expcld	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to A^{k} \in ℂ$
88	54	eleq2d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to (k \in (0 ..^N) \leftrightarrow k \in (0 \dots N - 1))$
89		fzonnsub	$⊢ k \in (0 ..^N) \to N - k \in ℕ$
90	89	nnnn0d	$⊢ k \in (0 ..^N) \to N - k \in ℕ_{0}$
91	88 90	syl6bir	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to (k \in (0 \dots N - 1) \to N - k \in ℕ_{0})$
92	91	imp	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to N - k \in ℕ_{0}$
93	66 92	expcld	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to B^{N - k} \in ℂ$
94	87 93	mulcld	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (0 \dots N - 1)) \to A^{k} B^{N - k} \in ℂ$
95		oveq2	$⊢ k = 0 \to A^{k} = A^{0}$
96		oveq2	$⊢ k = 0 \to N - k = N - 0$
97	96	oveq2d	$⊢ k = 0 \to B^{N - k} = B^{N - 0}$
98	95 97	oveq12d	$⊢ k = 0 \to A^{k} B^{N - k} = A^{0} B^{N - 0}$
99	59 94 98	fsum1p	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k = 0}^{N - 1} A^{k} B^{N - k} = A^{0} B^{N - 0} + \sum_{k = 0 + 1}^{N - 1} A^{k} B^{N - k}$
100	2	exp0d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A^{0} = 1$
101	36	subid1d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to N - 0 = N$
102	101	oveq2d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to B^{N - 0} = B^{N}$
103	100 102	oveq12d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A^{0} B^{N - 0} = 1 B^{N}$
104		simp1	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to N \in ℕ$
105	104	nnnn0d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to N \in ℕ_{0}$
106	3 105	expcld	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to B^{N} \in ℂ$
107	106	mulid2d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to 1 B^{N} = B^{N}$
108	103 107	eqtrd	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A^{0} B^{N - 0} = B^{N}$
109		0p1e1	$⊢ 0 + 1 = 1$
110	109	a1i	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to 0 + 1 = 1$
111	110	oveq1d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to (0 + 1 \dots N - 1) = (1 \dots N - 1)$
112	111	sumeq1d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k = 0 + 1}^{N - 1} A^{k} B^{N - k} = \sum_{k = 1}^{N - 1} A^{k} B^{N - k}$
113	108 112	oveq12d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A^{0} B^{N - 0} + \sum_{k = 0 + 1}^{N - 1} A^{k} B^{N - k} = B^{N} + \sum_{k = 1}^{N - 1} A^{k} B^{N - k}$
114	85 99 113	3eqtrd	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k \in (0 ..^N)} A^{k} B^{N - k} = B^{N} + \sum_{k = 1}^{N - 1} A^{k} B^{N - k}$
115	84 114	oveq12d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k \in (0 ..^N)} A^{k + 1} B^{N - k - 1} - \sum_{k \in (0 ..^N)} A^{k} B^{N - k} = \sum_{k = 0}^{N - 1 - 1} A^{k + 1} B^{N - k - 1} + A^{N - 1 + 1} B^{N - (N - 1) - 1} - (B^{N} + \sum_{k = 1}^{N - 1} A^{k} B^{N - k})$
116		fzfid	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to (1 \dots N - 1) \in Fin$
117	2	adantr	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (1 \dots N - 1)) \to A \in ℂ$
118		elfznn	$⊢ k \in (1 \dots N - 1) \to k \in ℕ$
119	118	nnnn0d	$⊢ k \in (1 \dots N - 1) \to k \in ℕ_{0}$
120	119	adantl	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (1 \dots N - 1)) \to k \in ℕ_{0}$
121	117 120	expcld	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (1 \dots N - 1)) \to A^{k} \in ℂ$
122	3	adantr	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (1 \dots N - 1)) \to B \in ℂ$
123		fzoval	$⊢ N \in ℤ \to (1 ..^N) = (1 \dots N - 1)$
124	52 123	syl	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to (1 ..^N) = (1 \dots N - 1)$
125	124	eleq2d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to (k \in (1 ..^N) \leftrightarrow k \in (1 \dots N - 1))$
126		fzonnsub	$⊢ k \in (1 ..^N) \to N - k \in ℕ$
127	126	nnnn0d	$⊢ k \in (1 ..^N) \to N - k \in ℕ_{0}$
128	125 127	syl6bir	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to (k \in (1 \dots N - 1) \to N - k \in ℕ_{0})$
129	128	imp	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (1 \dots N - 1)) \to N - k \in ℕ_{0}$
130	122 129	expcld	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (1 \dots N - 1)) \to B^{N - k} \in ℂ$
131	121 130	mulcld	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land k \in (1 \dots N - 1)) \to A^{k} B^{N - k} \in ℂ$
132	116 131	fsumcl	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k = 1}^{N - 1} A^{k} B^{N - k} \in ℂ$
133	2 105	expcld	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A^{N} \in ℂ$
134		oveq1	$⊢ k = l \to k + 1 = l + 1$
135	134	oveq2d	$⊢ k = l \to A^{k + 1} = A^{l + 1}$
136		oveq2	$⊢ k = l \to N - k = N - l$
137	136	oveq1d	$⊢ k = l \to N - k - 1 = N - l - 1$
138	137	oveq2d	$⊢ k = l \to B^{N - k - 1} = B^{N - l - 1}$
139	135 138	oveq12d	$⊢ k = l \to A^{k + 1} B^{N - k - 1} = A^{l + 1} B^{N - l - 1}$
140	139	cbvsumv	$⊢ \sum_{k = 0}^{N - 1 - 1} A^{k + 1} B^{N - k - 1} = \sum_{l = 0}^{N - 1 - 1} A^{l + 1} B^{N - l - 1}$
141		1m1e0	$⊢ 1 - 1 = 0$
142	141	eqcomi	$⊢ 0 = 1 - 1$
143	142	oveq1i	$⊢ (0 \dots N - 1 - 1) = (1 - 1 \dots N - 1 - 1)$
144	143	a1i	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to (0 \dots N - 1 - 1) = (1 - 1 \dots N - 1 - 1)$
145	36	adantr	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land l \in (0 \dots N - 1 - 1)) \to N \in ℂ$
146		elfznn0	$⊢ l \in (0 \dots N - 1 - 1) \to l \in ℕ_{0}$
147	146	nn0cnd	$⊢ l \in (0 \dots N - 1 - 1) \to l \in ℂ$
148	147	adantl	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land l \in (0 \dots N - 1 - 1)) \to l \in ℂ$
149		1cnd	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land l \in (0 \dots N - 1 - 1)) \to 1 \in ℂ$
150	145 148 149	subsub4d	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land l \in (0 \dots N - 1 - 1)) \to N - l - 1 = N - (l + 1)$
151	150	oveq2d	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land l \in (0 \dots N - 1 - 1)) \to B^{N - l - 1} = B^{N - (l + 1)}$
152	151	oveq2d	$⊢ ((N \in ℕ \land A \in ℂ \land B \in ℂ) \land l \in (0 \dots N - 1 - 1)) \to A^{l + 1} B^{N - l - 1} = A^{l + 1} B^{N - (l + 1)}$
153	144 152	sumeq12dv	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{l = 0}^{N - 1 - 1} A^{l + 1} B^{N - l - 1} = \sum_{l = 1 - 1}^{N - 1 - 1} A^{l + 1} B^{N - (l + 1)}$
154	140 153	eqtrid	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k = 0}^{N - 1 - 1} A^{k + 1} B^{N - k - 1} = \sum_{l = 1 - 1}^{N - 1 - 1} A^{l + 1} B^{N - (l + 1)}$
155		1zzd	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to 1 \in ℤ$
156		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
157	52 156	syl	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to N - 1 \in ℤ$
158		oveq2	$⊢ k = l + 1 \to A^{k} = A^{l + 1}$
159		oveq2	$⊢ k = l + 1 \to N - k = N - (l + 1)$
160	159	oveq2d	$⊢ k = l + 1 \to B^{N - k} = B^{N - (l + 1)}$
161	158 160	oveq12d	$⊢ k = l + 1 \to A^{k} B^{N - k} = A^{l + 1} B^{N - (l + 1)}$
162	155 155 157 131 161	fsumshftm	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k = 1}^{N - 1} A^{k} B^{N - k} = \sum_{l = 1 - 1}^{N - 1 - 1} A^{l + 1} B^{N - (l + 1)}$
163	154 162	eqtr4d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k = 0}^{N - 1 - 1} A^{k + 1} B^{N - k - 1} = \sum_{k = 1}^{N - 1} A^{k} B^{N - k}$
164		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
165	36 164	syl	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to N - 1 + 1 = N$
166	165	oveq2d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A^{N - 1 + 1} = A^{N}$
167		peano2cnm	$⊢ N \in ℂ \to N - 1 \in ℂ$
168	35 167	syl	$⊢ N \in ℕ \to N - 1 \in ℂ$
169		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
170	35 168 169	sub32d	$⊢ N \in ℕ \to N - (N - 1) - 1 = N - 1 - (N - 1)$
171	168	subidd	$⊢ N \in ℕ \to N - 1 - (N - 1) = 0$
172	170 171	eqtrd	$⊢ N \in ℕ \to N - (N - 1) - 1 = 0$
173	172	3ad2ant1	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to N - (N - 1) - 1 = 0$
174	173	oveq2d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to B^{N - (N - 1) - 1} = B^{0}$
175		exp0	$⊢ B \in ℂ \to B^{0} = 1$
176	175	3ad2ant3	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to B^{0} = 1$
177	174 176	eqtrd	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to B^{N - (N - 1) - 1} = 1$
178	166 177	oveq12d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A^{N - 1 + 1} B^{N - (N - 1) - 1} = A^{N} \cdot 1$
179	133	mulid1d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A^{N} \cdot 1 = A^{N}$
180	178 179	eqtrd	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A^{N - 1 + 1} B^{N - (N - 1) - 1} = A^{N}$
181	163 180	oveq12d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k = 0}^{N - 1 - 1} A^{k + 1} B^{N - k - 1} + A^{N - 1 + 1} B^{N - (N - 1) - 1} = \sum_{k = 1}^{N - 1} A^{k} B^{N - k} + A^{N}$
182	132 133 181	comraddd	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k = 0}^{N - 1 - 1} A^{k + 1} B^{N - k - 1} + A^{N - 1 + 1} B^{N - (N - 1) - 1} = A^{N} + \sum_{k = 1}^{N - 1} A^{k} B^{N - k}$
183	182	oveq1d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k = 0}^{N - 1 - 1} A^{k + 1} B^{N - k - 1} + A^{N - 1 + 1} B^{N - (N - 1) - 1} - (B^{N} + \sum_{k = 1}^{N - 1} A^{k} B^{N - k}) = A^{N} + \sum_{k = 1}^{N - 1} A^{k} B^{N - k} - (B^{N} + \sum_{k = 1}^{N - 1} A^{k} B^{N - k})$
184	133 106 132	pnpcan2d	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A^{N} + \sum_{k = 1}^{N - 1} A^{k} B^{N - k} - (B^{N} + \sum_{k = 1}^{N - 1} A^{k} B^{N - k}) = A^{N} - B^{N}$
185	115 183 184	3eqtrd	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to \sum_{k \in (0 ..^N)} A^{k + 1} B^{N - k - 1} - \sum_{k \in (0 ..^N)} A^{k} B^{N - k} = A^{N} - B^{N}$
186	18 50 185	3eqtrrd	$⊢ (N \in ℕ \land A \in ℂ \land B \in ℂ) \to A^{N} - B^{N} = (A - B) \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1}$
187	186	3exp	$⊢ N \in ℕ \to (A \in ℂ \to (B \in ℂ \to A^{N} - B^{N} = (A - B) \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1}))$
188		simp2	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to A \in ℂ$
189		simp3	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to B \in ℂ$
190	188 189	subcld	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to A - B \in ℂ$
191	190	mul01d	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to (A - B) \cdot 0 = 0$
192		oveq2	$⊢ N = 0 \to (0 ..^N) = (0 ..^0)$
193		fzo0	$⊢ (0 ..^0) = \emptyset$
194	192 193	eqtrdi	$⊢ N = 0 \to (0 ..^N) = \emptyset$
195	194	sumeq1d	$⊢ N = 0 \to \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1} = \sum_{k \in \emptyset} A^{k} B^{N - k - 1}$
196	195	3ad2ant1	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1} = \sum_{k \in \emptyset} A^{k} B^{N - k - 1}$
197		sum0	$⊢ \sum_{k \in \emptyset} A^{k} B^{N - k - 1} = 0$
198	196 197	eqtrdi	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1} = 0$
199	198	oveq2d	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to (A - B) \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1} = (A - B) \cdot 0$
200		oveq2	$⊢ N = 0 \to A^{N} = A^{0}$
201	200	3ad2ant1	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to A^{N} = A^{0}$
202		exp0	$⊢ A \in ℂ \to A^{0} = 1$
203	202	3ad2ant2	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to A^{0} = 1$
204	201 203	eqtrd	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to A^{N} = 1$
205		oveq2	$⊢ N = 0 \to B^{N} = B^{0}$
206	205	3ad2ant1	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to B^{N} = B^{0}$
207	175	3ad2ant3	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to B^{0} = 1$
208	206 207	eqtrd	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to B^{N} = 1$
209	204 208	oveq12d	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to A^{N} - B^{N} = 1 - 1$
210	209 141	eqtrdi	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to A^{N} - B^{N} = 0$
211	191 199 210	3eqtr4rd	$⊢ (N = 0 \land A \in ℂ \land B \in ℂ) \to A^{N} - B^{N} = (A - B) \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1}$
212	211	3exp	$⊢ N = 0 \to (A \in ℂ \to (B \in ℂ \to A^{N} - B^{N} = (A - B) \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1}))$
213	187 212	jaoi	$⊢ (N \in ℕ \lor N = 0) \to (A \in ℂ \to (B \in ℂ \to A^{N} - B^{N} = (A - B) \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1}))$
214	1 213	sylbi	$⊢ N \in ℕ_{0} \to (A \in ℂ \to (B \in ℂ \to A^{N} - B^{N} = (A - B) \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1}))$
215	214	3imp	$⊢ (N \in ℕ_{0} \land A \in ℂ \land B \in ℂ) \to A^{N} - B^{N} = (A - B) \sum_{k \in (0 ..^N)} A^{k} B^{N - k - 1}$

Metamath Proof Explorer

Theorem pwdif

Proof