Metamath Proof Explorer

Theorem pwm1geoser

Description: The n-th power of a number decreased by 1 expressed by the finite geometric series 1 + A ^ 1 + A ^ 2 + ... + A ^ ( N - 1 ) . (Contributed by AV, 14-Aug-2021) (Proof shortened by AV, 19-Aug-2021)

Ref Expression
Hypotheses pwm1geoser.a 
|- ( ph -> A e. CC )
pwm1geoser.n 
|- ( ph -> N e. NN0 )
Assertion pwm1geoser 
|- ( ph -> ( ( A ^ N ) - 1 ) = ( ( A - 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) )

Proof

Step Hyp Ref Expression
1 pwm1geoser.a 
 |-  ( ph -> A e. CC )
2 pwm1geoser.n 
 |-  ( ph -> N e. NN0 )
3 2 nn0zd 
 |-  ( ph -> N e. ZZ )
4 1exp 
 |-  ( N e. ZZ -> ( 1 ^ N ) = 1 )
5 3 4 syl 
 |-  ( ph -> ( 1 ^ N ) = 1 )
6 5 eqcomd 
 |-  ( ph -> 1 = ( 1 ^ N ) )
7 6 oveq2d 
 |-  ( ph -> ( ( A ^ N ) - 1 ) = ( ( A ^ N ) - ( 1 ^ N ) ) )
8 1cnd 
 |-  ( ph -> 1 e. CC )
9 pwdif 
 |-  ( ( N e. NN0 /\ A e. CC /\ 1 e. CC ) -> ( ( A ^ N ) - ( 1 ^ N ) ) = ( ( A - 1 ) x. sum_ k e. ( 0 ..^ N ) ( ( A ^ k ) x. ( 1 ^ ( ( N - k ) - 1 ) ) ) ) )
10 2 1 8 9 syl3anc 
 |-  ( ph -> ( ( A ^ N ) - ( 1 ^ N ) ) = ( ( A - 1 ) x. sum_ k e. ( 0 ..^ N ) ( ( A ^ k ) x. ( 1 ^ ( ( N - k ) - 1 ) ) ) ) )
11 fzoval 
 |-  ( N e. ZZ -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
12 3 11 syl 
 |-  ( ph -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
13 3 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> N e. ZZ )
14 elfzoelz 
 |-  ( k e. ( 0 ..^ N ) -> k e. ZZ )
15 14 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k e. ZZ )
16 13 15 zsubcld 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( N - k ) e. ZZ )
17 peano2zm 
 |-  ( ( N - k ) e. ZZ -> ( ( N - k ) - 1 ) e. ZZ )
18 1exp 
 |-  ( ( ( N - k ) - 1 ) e. ZZ -> ( 1 ^ ( ( N - k ) - 1 ) ) = 1 )
19 16 17 18 3syl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( 1 ^ ( ( N - k ) - 1 ) ) = 1 )
20 19 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( A ^ k ) x. ( 1 ^ ( ( N - k ) - 1 ) ) ) = ( ( A ^ k ) x. 1 ) )
21 1 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> A e. CC )
22 elfzonn0 
 |-  ( k e. ( 0 ..^ N ) -> k e. NN0 )
23 22 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k e. NN0 )
24 21 23 expcld 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( A ^ k ) e. CC )
25 24 mulid1d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( A ^ k ) x. 1 ) = ( A ^ k ) )
26 20 25 eqtrd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( A ^ k ) x. ( 1 ^ ( ( N - k ) - 1 ) ) ) = ( A ^ k ) )
27 12 26 sumeq12dv 
 |-  ( ph -> sum_ k e. ( 0 ..^ N ) ( ( A ^ k ) x. ( 1 ^ ( ( N - k ) - 1 ) ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) )
28 27 oveq2d 
 |-  ( ph -> ( ( A - 1 ) x. sum_ k e. ( 0 ..^ N ) ( ( A ^ k ) x. ( 1 ^ ( ( N - k ) - 1 ) ) ) ) = ( ( A - 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) )
29 7 10 28 3eqtrd 
 |-  ( ph -> ( ( A ^ N ) - 1 ) = ( ( A - 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) )