pwp1fsum

Description: The n-th power of a number increased by 1 expressed by a product with a finite sum. (Contributed by AV, 15-Aug-2021)

	Ref	Expression
Hypotheses	pwp1fsum.a	$⊢ φ \to A \in ℂ$
	pwp1fsum.n	$⊢ φ \to N \in ℕ$
Assertion	pwp1fsum	$⊢ φ \to {(- 1)}^{N - 1} A^{N} + 1 = (A + 1) \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k}$

Proof

Step	Hyp	Ref	Expression
1		pwp1fsum.a	$⊢ φ \to A \in ℂ$
2		pwp1fsum.n	$⊢ φ \to N \in ℕ$
3		1cnd	$⊢ φ \to 1 \in ℂ$
4		fzfid	$⊢ φ \to (0 \dots N - 1) \in Fin$
5		neg1cn	$⊢ - 1 \in ℂ$
6	5	a1i	$⊢ (φ \land k \in (0 \dots N - 1)) \to - 1 \in ℂ$
7		elfznn0	$⊢ k \in (0 \dots N - 1) \to k \in ℕ_{0}$
8	7	adantl	$⊢ (φ \land k \in (0 \dots N - 1)) \to k \in ℕ_{0}$
9	6 8	expcld	$⊢ (φ \land k \in (0 \dots N - 1)) \to {(- 1)}^{k} \in ℂ$
10	1	adantr	$⊢ (φ \land k \in (0 \dots N - 1)) \to A \in ℂ$
11	10 8	expcld	$⊢ (φ \land k \in (0 \dots N - 1)) \to A^{k} \in ℂ$
12	9 11	mulcld	$⊢ (φ \land k \in (0 \dots N - 1)) \to {(- 1)}^{k} A^{k} \in ℂ$
13	4 12	fsumcl	$⊢ φ \to \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k} \in ℂ$
14	1 3 13	adddird	$⊢ φ \to (A + 1) \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k} = A \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k} + 1 \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k}$
15	4 1 12	fsummulc2	$⊢ φ \to A \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k} = \sum_{k = 0}^{N - 1} A {(- 1)}^{k} A^{k}$
16	10 12	mulcomd	$⊢ (φ \land k \in (0 \dots N - 1)) \to A {(- 1)}^{k} A^{k} = {(- 1)}^{k} A^{k} A$
17	9 11 10	mulassd	$⊢ (φ \land k \in (0 \dots N - 1)) \to {(- 1)}^{k} A^{k} A = {(- 1)}^{k} A^{k} A$
18		expp1	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k + 1} = A^{k} A$
19	1 7 18	syl2an	$⊢ (φ \land k \in (0 \dots N - 1)) \to A^{k + 1} = A^{k} A$
20	19	eqcomd	$⊢ (φ \land k \in (0 \dots N - 1)) \to A^{k} A = A^{k + 1}$
21	20	oveq2d	$⊢ (φ \land k \in (0 \dots N - 1)) \to {(- 1)}^{k} A^{k} A = {(- 1)}^{k} A^{k + 1}$
22	16 17 21	3eqtrd	$⊢ (φ \land k \in (0 \dots N - 1)) \to A {(- 1)}^{k} A^{k} = {(- 1)}^{k} A^{k + 1}$
23	22	sumeq2dv	$⊢ φ \to \sum_{k = 0}^{N - 1} A {(- 1)}^{k} A^{k} = \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k + 1}$
24	15 23	eqtrd	$⊢ φ \to A \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k} = \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k + 1}$
25	13	mulid2d	$⊢ φ \to 1 \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k} = \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k}$
26	24 25	oveq12d	$⊢ φ \to A \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k} + 1 \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k} = \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k + 1} + \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k}$
27		1zzd	$⊢ φ \to 1 \in ℤ$
28		0zd	$⊢ φ \to 0 \in ℤ$
29		nnz	$⊢ N \in ℕ \to N \in ℤ$
30		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
31	29 30	syl	$⊢ N \in ℕ \to N - 1 \in ℤ$
32	2 31	syl	$⊢ φ \to N - 1 \in ℤ$
33		peano2nn0	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ_{0}$
34	7 33	syl	$⊢ k \in (0 \dots N - 1) \to k + 1 \in ℕ_{0}$
35	34	adantl	$⊢ (φ \land k \in (0 \dots N - 1)) \to k + 1 \in ℕ_{0}$
36	10 35	expcld	$⊢ (φ \land k \in (0 \dots N - 1)) \to A^{k + 1} \in ℂ$
37	9 36	mulcld	$⊢ (φ \land k \in (0 \dots N - 1)) \to {(- 1)}^{k} A^{k + 1} \in ℂ$
38		oveq2	$⊢ k = l - 1 \to {(- 1)}^{k} = {(- 1)}^{l - 1}$
39		oveq1	$⊢ k = l - 1 \to k + 1 = l - 1 + 1$
40	39	oveq2d	$⊢ k = l - 1 \to A^{k + 1} = A^{l - 1 + 1}$
41	38 40	oveq12d	$⊢ k = l - 1 \to {(- 1)}^{k} A^{k + 1} = {(- 1)}^{l - 1} A^{l - 1 + 1}$
42	27 28 32 37 41	fsumshft	$⊢ φ \to \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k + 1} = \sum_{l = 0 + 1}^{N - 1 + 1} {(- 1)}^{l - 1} A^{l - 1 + 1}$
43		elfzelz	$⊢ l \in (0 + 1 \dots N - 1 + 1) \to l \in ℤ$
44	43	zcnd	$⊢ l \in (0 + 1 \dots N - 1 + 1) \to l \in ℂ$
45	44	adantl	$⊢ (φ \land l \in (0 + 1 \dots N - 1 + 1)) \to l \in ℂ$
46		npcan1	$⊢ l \in ℂ \to l - 1 + 1 = l$
47	45 46	syl	$⊢ (φ \land l \in (0 + 1 \dots N - 1 + 1)) \to l - 1 + 1 = l$
48	47	oveq2d	$⊢ (φ \land l \in (0 + 1 \dots N - 1 + 1)) \to A^{l - 1 + 1} = A^{l}$
49	48	oveq2d	$⊢ (φ \land l \in (0 + 1 \dots N - 1 + 1)) \to {(- 1)}^{l - 1} A^{l - 1 + 1} = {(- 1)}^{l - 1} A^{l}$
50	49	sumeq2dv	$⊢ φ \to \sum_{l = 0 + 1}^{N - 1 + 1} {(- 1)}^{l - 1} A^{l - 1 + 1} = \sum_{l = 0 + 1}^{N - 1 + 1} {(- 1)}^{l - 1} A^{l}$
51	2	nncnd	$⊢ φ \to N \in ℂ$
52		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
53	51 52	syl	$⊢ φ \to N - 1 + 1 = N$
54		0p1e1	$⊢ 0 + 1 = 1$
55	54	fveq2i	$⊢ ℤ_{\geq (0 + 1)} = ℤ_{\geq 1}$
56		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
57	55 56	eqtr4i	$⊢ ℤ_{\geq (0 + 1)} = ℕ$
58	57	a1i	$⊢ φ \to ℤ_{\geq (0 + 1)} = ℕ$
59	2 53 58	3eltr4d	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (0 + 1)}$
60	54	oveq1i	$⊢ (0 + 1 \dots N - 1 + 1) = (1 \dots N - 1 + 1)$
61	60	eleq2i	$⊢ l \in (0 + 1 \dots N - 1 + 1) \leftrightarrow l \in (1 \dots N - 1 + 1)$
62	5	a1i	$⊢ (φ \land l \in ℕ) \to - 1 \in ℂ$
63		nnm1nn0	$⊢ l \in ℕ \to l - 1 \in ℕ_{0}$
64	63	adantl	$⊢ (φ \land l \in ℕ) \to l - 1 \in ℕ_{0}$
65	62 64	expcld	$⊢ (φ \land l \in ℕ) \to {(- 1)}^{l - 1} \in ℂ$
66	1	adantr	$⊢ (φ \land l \in ℕ) \to A \in ℂ$
67		nnnn0	$⊢ l \in ℕ \to l \in ℕ_{0}$
68	67	adantl	$⊢ (φ \land l \in ℕ) \to l \in ℕ_{0}$
69	66 68	expcld	$⊢ (φ \land l \in ℕ) \to A^{l} \in ℂ$
70	65 69	mulcld	$⊢ (φ \land l \in ℕ) \to {(- 1)}^{l - 1} A^{l} \in ℂ$
71	70	expcom	$⊢ l \in ℕ \to (φ \to {(- 1)}^{l - 1} A^{l} \in ℂ)$
72		elfznn	$⊢ l \in (1 \dots N - 1 + 1) \to l \in ℕ$
73	71 72	syl11	$⊢ φ \to (l \in (1 \dots N - 1 + 1) \to {(- 1)}^{l - 1} A^{l} \in ℂ)$
74	61 73	syl5bi	$⊢ φ \to (l \in (0 + 1 \dots N - 1 + 1) \to {(- 1)}^{l - 1} A^{l} \in ℂ)$
75	74	imp	$⊢ (φ \land l \in (0 + 1 \dots N - 1 + 1)) \to {(- 1)}^{l - 1} A^{l} \in ℂ$
76		oveq1	$⊢ l = N - 1 + 1 \to l - 1 = (N - 1) + 1 - 1$
77	76	oveq2d	$⊢ l = N - 1 + 1 \to {(- 1)}^{l - 1} = {(- 1)}^{(N - 1) + 1 - 1}$
78		oveq2	$⊢ l = N - 1 + 1 \to A^{l} = A^{N - 1 + 1}$
79	77 78	oveq12d	$⊢ l = N - 1 + 1 \to {(- 1)}^{l - 1} A^{l} = {(- 1)}^{(N - 1) + 1 - 1} A^{N - 1 + 1}$
80	59 75 79	fsumm1	$⊢ φ \to \sum_{l = 0 + 1}^{N - 1 + 1} {(- 1)}^{l - 1} A^{l} = \sum_{l = 0 + 1}^{(N - 1) + 1 - 1} {(- 1)}^{l - 1} A^{l} + {(- 1)}^{(N - 1) + 1 - 1} A^{N - 1 + 1}$
81	32	zcnd	$⊢ φ \to N - 1 \in ℂ$
82		pncan1	$⊢ N - 1 \in ℂ \to (N - 1) + 1 - 1 = N - 1$
83	81 82	syl	$⊢ φ \to (N - 1) + 1 - 1 = N - 1$
84	83	oveq2d	$⊢ φ \to (0 + 1 \dots (N - 1) + 1 - 1) = (0 + 1 \dots N - 1)$
85	84	sumeq1d	$⊢ φ \to \sum_{l = 0 + 1}^{(N - 1) + 1 - 1} {(- 1)}^{l - 1} A^{l} = \sum_{l = 0 + 1}^{N - 1} {(- 1)}^{l - 1} A^{l}$
86		oveq1	$⊢ l = k \to l - 1 = k - 1$
87	86	oveq2d	$⊢ l = k \to {(- 1)}^{l - 1} = {(- 1)}^{k - 1}$
88		oveq2	$⊢ l = k \to A^{l} = A^{k}$
89	87 88	oveq12d	$⊢ l = k \to {(- 1)}^{l - 1} A^{l} = {(- 1)}^{k - 1} A^{k}$
90	89	cbvsumv	$⊢ \sum_{l = 0 + 1}^{N - 1} {(- 1)}^{l - 1} A^{l} = \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k}$
91	85 90	eqtrdi	$⊢ φ \to \sum_{l = 0 + 1}^{(N - 1) + 1 - 1} {(- 1)}^{l - 1} A^{l} = \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k}$
92	83	oveq2d	$⊢ φ \to {(- 1)}^{(N - 1) + 1 - 1} = {(- 1)}^{N - 1}$
93	53	oveq2d	$⊢ φ \to A^{N - 1 + 1} = A^{N}$
94	92 93	oveq12d	$⊢ φ \to {(- 1)}^{(N - 1) + 1 - 1} A^{N - 1 + 1} = {(- 1)}^{N - 1} A^{N}$
95	91 94	oveq12d	$⊢ φ \to \sum_{l = 0 + 1}^{(N - 1) + 1 - 1} {(- 1)}^{l - 1} A^{l} + {(- 1)}^{(N - 1) + 1 - 1} A^{N - 1 + 1} = \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + {(- 1)}^{N - 1} A^{N}$
96	80 95	eqtrd	$⊢ φ \to \sum_{l = 0 + 1}^{N - 1 + 1} {(- 1)}^{l - 1} A^{l} = \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + {(- 1)}^{N - 1} A^{N}$
97	42 50 96	3eqtrd	$⊢ φ \to \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k + 1} = \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + {(- 1)}^{N - 1} A^{N}$
98		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
99		elnn0uz	$⊢ N - 1 \in ℕ_{0} \leftrightarrow N - 1 \in ℤ_{\geq 0}$
100	98 99	sylib	$⊢ N \in ℕ \to N - 1 \in ℤ_{\geq 0}$
101	2 100	syl	$⊢ φ \to N - 1 \in ℤ_{\geq 0}$
102		oveq2	$⊢ k = 0 \to {(- 1)}^{k} = {(- 1)}^{0}$
103		exp0	$⊢ - 1 \in ℂ \to {(- 1)}^{0} = 1$
104	5 103	ax-mp	$⊢ {(- 1)}^{0} = 1$
105	102 104	eqtrdi	$⊢ k = 0 \to {(- 1)}^{k} = 1$
106		oveq2	$⊢ k = 0 \to A^{k} = A^{0}$
107	105 106	oveq12d	$⊢ k = 0 \to {(- 1)}^{k} A^{k} = 1 A^{0}$
108	101 12 107	fsum1p	$⊢ φ \to \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k} = 1 A^{0} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k}$
109	1	exp0d	$⊢ φ \to A^{0} = 1$
110	109	oveq2d	$⊢ φ \to 1 A^{0} = 1 \cdot 1$
111		1t1e1	$⊢ 1 \cdot 1 = 1$
112	110 111	eqtrdi	$⊢ φ \to 1 A^{0} = 1$
113	112	oveq1d	$⊢ φ \to 1 A^{0} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} = 1 + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k}$
114		fzfid	$⊢ φ \to (0 + 1 \dots N - 1) \in Fin$
115		elfznn	$⊢ k \in (1 \dots N - 1) \to k \in ℕ$
116	5	a1i	$⊢ (φ \land k \in ℕ) \to - 1 \in ℂ$
117		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
118	117	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℕ_{0}$
119	116 118	expcld	$⊢ (φ \land k \in ℕ) \to {(- 1)}^{k} \in ℂ$
120	1	adantr	$⊢ (φ \land k \in ℕ) \to A \in ℂ$
121	120 118	expcld	$⊢ (φ \land k \in ℕ) \to A^{k} \in ℂ$
122	119 121	mulcld	$⊢ (φ \land k \in ℕ) \to {(- 1)}^{k} A^{k} \in ℂ$
123	122	expcom	$⊢ k \in ℕ \to (φ \to {(- 1)}^{k} A^{k} \in ℂ)$
124	115 123	syl	$⊢ k \in (1 \dots N - 1) \to (φ \to {(- 1)}^{k} A^{k} \in ℂ)$
125	54	oveq1i	$⊢ (0 + 1 \dots N - 1) = (1 \dots N - 1)$
126	124 125	eleq2s	$⊢ k \in (0 + 1 \dots N - 1) \to (φ \to {(- 1)}^{k} A^{k} \in ℂ)$
127	126	impcom	$⊢ (φ \land k \in (0 + 1 \dots N - 1)) \to {(- 1)}^{k} A^{k} \in ℂ$
128	114 127	fsumcl	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} \in ℂ$
129	3 128	addcomd	$⊢ φ \to 1 + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} = \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} + 1$
130	108 113 129	3eqtrd	$⊢ φ \to \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k} = \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} + 1$
131	97 130	oveq12d	$⊢ φ \to \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k + 1} + \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k} = \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + {(- 1)}^{N - 1} A^{N} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} + 1$
132		nnm1nn0	$⊢ k \in ℕ \to k - 1 \in ℕ_{0}$
133	132	adantl	$⊢ (φ \land k \in ℕ) \to k - 1 \in ℕ_{0}$
134	116 133	expcld	$⊢ (φ \land k \in ℕ) \to {(- 1)}^{k - 1} \in ℂ$
135	134 121	mulcld	$⊢ (φ \land k \in ℕ) \to {(- 1)}^{k - 1} A^{k} \in ℂ$
136	135	expcom	$⊢ k \in ℕ \to (φ \to {(- 1)}^{k - 1} A^{k} \in ℂ)$
137	115 136	syl	$⊢ k \in (1 \dots N - 1) \to (φ \to {(- 1)}^{k - 1} A^{k} \in ℂ)$
138	137 125	eleq2s	$⊢ k \in (0 + 1 \dots N - 1) \to (φ \to {(- 1)}^{k - 1} A^{k} \in ℂ)$
139	138	impcom	$⊢ (φ \land k \in (0 + 1 \dots N - 1)) \to {(- 1)}^{k - 1} A^{k} \in ℂ$
140	114 139	fsumcl	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} \in ℂ$
141	5	a1i	$⊢ φ \to - 1 \in ℂ$
142	2 98	syl	$⊢ φ \to N - 1 \in ℕ_{0}$
143	141 142	expcld	$⊢ φ \to {(- 1)}^{N - 1} \in ℂ$
144	2	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
145	1 144	expcld	$⊢ φ \to A^{N} \in ℂ$
146	143 145	mulcld	$⊢ φ \to {(- 1)}^{N - 1} A^{N} \in ℂ$
147	140 146	addcld	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + {(- 1)}^{N - 1} A^{N} \in ℂ$
148	147 128 3	addassd	$⊢ φ \to (\sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + {(- 1)}^{N - 1} A^{N}) + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} + 1 = \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + {(- 1)}^{N - 1} A^{N} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} + 1$
149	140 146	addcomd	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + {(- 1)}^{N - 1} A^{N} = {(- 1)}^{N - 1} A^{N} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k}$
150	149	oveq1d	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + {(- 1)}^{N - 1} A^{N} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} = {(- 1)}^{N - 1} A^{N} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k}$
151	146 140 128	addassd	$⊢ φ \to {(- 1)}^{N - 1} A^{N} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} = {(- 1)}^{N - 1} A^{N} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k}$
152		nncn	$⊢ k \in ℕ \to k \in ℂ$
153		npcan1	$⊢ k \in ℂ \to k - 1 + 1 = k$
154	152 153	syl	$⊢ k \in ℕ \to k - 1 + 1 = k$
155	154	eqcomd	$⊢ k \in ℕ \to k = k - 1 + 1$
156	155	oveq2d	$⊢ k \in ℕ \to {(- 1)}^{k} = {(- 1)}^{k - 1 + 1}$
157	5	a1i	$⊢ k \in ℕ \to - 1 \in ℂ$
158	157 132	expp1d	$⊢ k \in ℕ \to {(- 1)}^{k - 1 + 1} = {(- 1)}^{k - 1} -1$
159	157 132	expcld	$⊢ k \in ℕ \to {(- 1)}^{k - 1} \in ℂ$
160	159 157	mulcomd	$⊢ k \in ℕ \to {(- 1)}^{k - 1} -1 = -1 {(- 1)}^{k - 1}$
161	156 158 160	3eqtrd	$⊢ k \in ℕ \to {(- 1)}^{k} = -1 {(- 1)}^{k - 1}$
162	161	oveq2d	$⊢ k \in ℕ \to {(- 1)}^{k - 1} + {(- 1)}^{k} = {(- 1)}^{k - 1} + -1 {(- 1)}^{k - 1}$
163	159	mulm1d	$⊢ k \in ℕ \to -1 {(- 1)}^{k - 1} = - {(- 1)}^{k - 1}$
164	163	oveq2d	$⊢ k \in ℕ \to {(- 1)}^{k - 1} + -1 {(- 1)}^{k - 1} = {(- 1)}^{k - 1} + (- {(- 1)}^{k - 1})$
165	159	negidd	$⊢ k \in ℕ \to {(- 1)}^{k - 1} + (- {(- 1)}^{k - 1}) = 0$
166	162 164 165	3eqtrd	$⊢ k \in ℕ \to {(- 1)}^{k - 1} + {(- 1)}^{k} = 0$
167	166	adantl	$⊢ (φ \land k \in ℕ) \to {(- 1)}^{k - 1} + {(- 1)}^{k} = 0$
168	167	oveq1d	$⊢ (φ \land k \in ℕ) \to ({(- 1)}^{k - 1} + {(- 1)}^{k}) A^{k} = 0 \cdot A^{k}$
169	134 119 121	adddird	$⊢ (φ \land k \in ℕ) \to ({(- 1)}^{k - 1} + {(- 1)}^{k}) A^{k} = {(- 1)}^{k - 1} A^{k} + {(- 1)}^{k} A^{k}$
170	121	mul02d	$⊢ (φ \land k \in ℕ) \to 0 \cdot A^{k} = 0$
171	168 169 170	3eqtr3d	$⊢ (φ \land k \in ℕ) \to {(- 1)}^{k - 1} A^{k} + {(- 1)}^{k} A^{k} = 0$
172	171	expcom	$⊢ k \in ℕ \to (φ \to {(- 1)}^{k - 1} A^{k} + {(- 1)}^{k} A^{k} = 0)$
173	115 172	syl	$⊢ k \in (1 \dots N - 1) \to (φ \to {(- 1)}^{k - 1} A^{k} + {(- 1)}^{k} A^{k} = 0)$
174	173 125	eleq2s	$⊢ k \in (0 + 1 \dots N - 1) \to (φ \to {(- 1)}^{k - 1} A^{k} + {(- 1)}^{k} A^{k} = 0)$
175	174	impcom	$⊢ (φ \land k \in (0 + 1 \dots N - 1)) \to {(- 1)}^{k - 1} A^{k} + {(- 1)}^{k} A^{k} = 0$
176	175	sumeq2dv	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} ({(- 1)}^{k - 1} A^{k} + {(- 1)}^{k} A^{k}) = \sum_{k = 0 + 1}^{N - 1} 0$
177	114 139 127	fsumadd	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} ({(- 1)}^{k - 1} A^{k} + {(- 1)}^{k} A^{k}) = \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k}$
178	114	olcd	$⊢ φ \to ((0 + 1 \dots N - 1) \subseteq ℤ_{\geq 1} \lor (0 + 1 \dots N - 1) \in Fin)$
179		sumz	$⊢ ((0 + 1 \dots N - 1) \subseteq ℤ_{\geq 1} \lor (0 + 1 \dots N - 1) \in Fin) \to \sum_{k = 0 + 1}^{N - 1} 0 = 0$
180	178 179	syl	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} 0 = 0$
181	176 177 180	3eqtr3d	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} = 0$
182	181	oveq2d	$⊢ φ \to {(- 1)}^{N - 1} A^{N} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} = {(- 1)}^{N - 1} A^{N} + 0$
183	146	addid1d	$⊢ φ \to {(- 1)}^{N - 1} A^{N} + 0 = {(- 1)}^{N - 1} A^{N}$
184	182 183	eqtrd	$⊢ φ \to {(- 1)}^{N - 1} A^{N} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} = {(- 1)}^{N - 1} A^{N}$
185	150 151 184	3eqtrd	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + {(- 1)}^{N - 1} A^{N} + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} = {(- 1)}^{N - 1} A^{N}$
186	185	oveq1d	$⊢ φ \to (\sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k - 1} A^{k} + {(- 1)}^{N - 1} A^{N}) + \sum_{k = 0 + 1}^{N - 1} {(- 1)}^{k} A^{k} + 1 = {(- 1)}^{N - 1} A^{N} + 1$
187	131 148 186	3eqtr2d	$⊢ φ \to \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k + 1} + \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k} = {(- 1)}^{N - 1} A^{N} + 1$
188	14 26 187	3eqtrd	$⊢ φ \to (A + 1) \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k} = {(- 1)}^{N - 1} A^{N} + 1$
189	188	eqcomd	$⊢ φ \to {(- 1)}^{N - 1} A^{N} + 1 = (A + 1) \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k}$

Metamath Proof Explorer

Theorem pwp1fsum

Proof