Metamath Proof Explorer

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 
|- ( ph -> A e. CC )
pwp1fsum.n 
|- ( ph -> N e. NN )
oddpwp1fsum.n 
|- ( ph -> -. 2 || N )
Assertion oddpwp1fsum 
|- ( ph -> ( ( A ^ N ) + 1 ) = ( ( A + 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) ) )

Proof

Step Hyp Ref Expression
1 pwp1fsum.a 
 |-  ( ph -> A e. CC )
2 pwp1fsum.n 
 |-  ( ph -> N e. NN )
3 oddpwp1fsum.n 
 |-  ( ph -> -. 2 || N )
4 2 nnzd 
 |-  ( ph -> N e. ZZ )
5 oddm1even 
 |-  ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N - 1 ) ) )
6 4 5 syl 
 |-  ( ph -> ( -. 2 || N <-> 2 || ( N - 1 ) ) )
7 3 6 mpbid 
 |-  ( ph -> 2 || ( N - 1 ) )
8 m1expe 
 |-  ( 2 || ( N - 1 ) -> ( -u 1 ^ ( N - 1 ) ) = 1 )
9 7 8 syl 
 |-  ( ph -> ( -u 1 ^ ( N - 1 ) ) = 1 )
10 9 oveq1d 
 |-  ( ph -> ( ( -u 1 ^ ( N - 1 ) ) x. ( A ^ N ) ) = ( 1 x. ( A ^ N ) ) )
11 10 oveq1d 
 |-  ( ph -> ( ( ( -u 1 ^ ( N - 1 ) ) x. ( A ^ N ) ) + 1 ) = ( ( 1 x. ( A ^ N ) ) + 1 ) )
12 1 2 pwp1fsum 
 |-  ( ph -> ( ( ( -u 1 ^ ( N - 1 ) ) x. ( A ^ N ) ) + 1 ) = ( ( A + 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) ) )
13 2 nnnn0d 
 |-  ( ph -> N e. NN0 )
14 1 13 expcld 
 |-  ( ph -> ( A ^ N ) e. CC )
15 14 mullidd 
 |-  ( ph -> ( 1 x. ( A ^ N ) ) = ( A ^ N ) )
16 15 oveq1d 
 |-  ( ph -> ( ( 1 x. ( A ^ N ) ) + 1 ) = ( ( A ^ N ) + 1 ) )
17 11 12 16 3eqtr3rd 
 |-  ( ph -> ( ( A ^ N ) + 1 ) = ( ( A + 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) ) )