oddpwp1fsum

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

Step	Hyp	Ref	Expression
1		pwp1fsum.a	$⊢ φ \to A \in ℂ$
2		pwp1fsum.n	$⊢ φ \to N \in ℕ$
3		oddpwp1fsum.n	$⊢ φ \to \neg 2 ∥ N$
4	2	nnzd	$⊢ φ \to N \in ℤ$
5		oddm1even	$⊢ N \in ℤ \to (\neg 2 ∥ N \leftrightarrow 2 ∥ (N - 1))$
6	4 5	syl	$⊢ φ \to (\neg 2 ∥ N \leftrightarrow 2 ∥ (N - 1))$
7	3 6	mpbid	$⊢ φ \to 2 ∥ (N - 1)$
8		m1expe	$⊢ 2 ∥ (N - 1) \to {(- 1)}^{N - 1} = 1$
9	7 8	syl	$⊢ φ \to {(- 1)}^{N - 1} = 1$
10	9	oveq1d	$⊢ φ \to {(- 1)}^{N - 1} A^{N} = 1 A^{N}$
11	10	oveq1d	$⊢ φ \to {(- 1)}^{N - 1} A^{N} + 1 = 1 A^{N} + 1$
12	1 2	pwp1fsum	$⊢ φ \to {(- 1)}^{N - 1} A^{N} + 1 = (A + 1) \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k}$
13	2	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
14	1 13	expcld	$⊢ φ \to A^{N} \in ℂ$
15	14	mullidd	$⊢ φ \to 1 A^{N} = A^{N}$
16	15	oveq1d	$⊢ φ \to 1 A^{N} + 1 = A^{N} + 1$
17	11 12 16	3eqtr3rd	$⊢ φ \to A^{N} + 1 = (A + 1) \sum_{k = 0}^{N - 1} {(- 1)}^{k} A^{k}$

Metamath Proof Explorer