Theorem 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)

	Ref	Expression
Hypotheses	pwp1fsum.a	$$⊢\phi \to A\in ℂ$$
	pwp1fsum.n	$$⊢\phi \to N\in \mathbb{N}$$
	oddpwp1fsum.n	$$⊢\phi \to \neg 2\parallel N$$
Assertion	oddpwp1fsum	$$⊢\phi \to A^N+1=\left(A+1\right)\sum _{k=0}^{N-1}{\left(-1\right)}^k{A}^k$$

Proof

Step	Hyp	Ref	Expression
1		pwp1fsum.a	$$⊢\phi \to A\in ℂ$$
2		pwp1fsum.n	$$⊢\phi \to N\in \mathbb{N}$$
3		oddpwp1fsum.n	$$⊢\phi \to \neg 2\parallel N$$
4	2	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
5		oddm1even	$$⊢N\in \mathbb{Z}\to \left(\neg 2\parallel N\leftrightarrow 2\parallel \left(N-1\right)\right)$$
6	4 5	syl	$$⊢\phi \to \left(\neg 2\parallel N\leftrightarrow 2\parallel \left(N-1\right)\right)$$
7	3 6	mpbid	$$⊢\phi \to 2\parallel \left(N-1\right)$$
8		m1expe	$$⊢2\parallel \left(N-1\right)\to {\left(-1\right)}^{N-1}=1$$
9	7 8	syl	$$⊢\phi \to {\left(-1\right)}^{N-1}=1$$
10	9	oveq1d	$$⊢\phi \to {\left(-1\right)}^{N-1}{A}^N=1A^N$$
11	10	oveq1d	$$⊢\phi \to {\left(-1\right)}^{N-1}{A}^N+1=1A^N+1$$
12	1 2	pwp1fsum	$$⊢\phi \to {\left(-1\right)}^{N-1}{A}^N+1=\left(A+1\right)\sum _{k=0}^{N-1}{\left(-1\right)}^k{A}^k$$
13	2	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
14	1 13	expcld	$$⊢\phi \to A^N\in ℂ$$
15	14	mulid2d	$$⊢\phi \to 1A^N=A^N$$
16	15	oveq1d	$$⊢\phi \to 1A^N+1=A^N+1$$
17	11 12 16	3eqtr3rd	$$⊢\phi \to A^N+1=\left(A+1\right)\sum _{k=0}^{N-1}{\left(-1\right)}^k{A}^k$$