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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	pwp1fsum.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	oddpwp1fsum.n	⊢ ( 𝜑 → ¬ 2 ∥ 𝑁 )
Assertion	oddpwp1fsum	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + 1 ) = ( ( 𝐴 + 1 ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pwp1fsum.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		pwp1fsum.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		oddpwp1fsum.n	⊢ ( 𝜑 → ¬ 2 ∥ 𝑁 )
4	2	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
5		oddm1even	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 − 1 ) ) )
6	4 5	syl	⊢ ( 𝜑 → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 − 1 ) ) )
7	3 6	mpbid	⊢ ( 𝜑 → 2 ∥ ( 𝑁 − 1 ) )
8		m1expe	⊢ ( 2 ∥ ( 𝑁 − 1 ) → ( - 1 ↑ ( 𝑁 − 1 ) ) = 1 )
9	7 8	syl	⊢ ( 𝜑 → ( - 1 ↑ ( 𝑁 − 1 ) ) = 1 )
10	9	oveq1d	⊢ ( 𝜑 → ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) = ( 1 · ( 𝐴 ↑ 𝑁 ) ) )
11	10	oveq1d	⊢ ( 𝜑 → ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + 1 ) = ( ( 1 · ( 𝐴 ↑ 𝑁 ) ) + 1 ) )
12	1 2	pwp1fsum	⊢ ( 𝜑 → ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + 1 ) = ( ( 𝐴 + 1 ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )
13	2	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
14	1 13	expcld	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
15	14	mulid2d	⊢ ( 𝜑 → ( 1 · ( 𝐴 ↑ 𝑁 ) ) = ( 𝐴 ↑ 𝑁 ) )
16	15	oveq1d	⊢ ( 𝜑 → ( ( 1 · ( 𝐴 ↑ 𝑁 ) ) + 1 ) = ( ( 𝐴 ↑ 𝑁 ) + 1 ) )
17	11 12 16	3eqtr3rd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + 1 ) = ( ( 𝐴 + 1 ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )