Metamath Proof Explorer

Theorem pwm1geoserOLD

Description: Obsolete version of pwm1geoser as of 22-Aug-2023. 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 modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pwm1geoserOLD.1 
 |-  ( ph -> A e. CC )
2 pwm1geoserOLD.3 
 |-  ( ph -> N e. NN0 )
3 1m1e0 
 |-  ( 1 - 1 ) = 0
4 2 nn0zd 
 |-  ( ph -> N e. ZZ )
5 1exp 
 |-  ( N e. ZZ -> ( 1 ^ N ) = 1 )
6 4 5 syl 
 |-  ( ph -> ( 1 ^ N ) = 1 )
7 6 oveq1d 
 |-  ( ph -> ( ( 1 ^ N ) - 1 ) = ( 1 - 1 ) )
8 fzfid 
 |-  ( ph -> ( 0 ... ( N - 1 ) ) e. Fin )
9 1cnd 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> 1 e. CC )
10 elfznn0 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. NN0 )
11 10 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> k e. NN0 )
12 9 11 expcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ^ k ) e. CC )
13 8 12 fsumcl 
 |-  ( ph -> sum_ k e. ( 0 ... ( N - 1 ) ) ( 1 ^ k ) e. CC )
14 13 mul02d 
 |-  ( ph -> ( 0 x. sum_ k e. ( 0 ... ( N - 1 ) ) ( 1 ^ k ) ) = 0 )
15 3 7 14 3eqtr4a 
 |-  ( ph -> ( ( 1 ^ N ) - 1 ) = ( 0 x. sum_ k e. ( 0 ... ( N - 1 ) ) ( 1 ^ k ) ) )
16 oveq1 
 |-  ( A = 1 -> ( A ^ N ) = ( 1 ^ N ) )
17 16 oveq1d 
 |-  ( A = 1 -> ( ( A ^ N ) - 1 ) = ( ( 1 ^ N ) - 1 ) )
18 oveq1 
 |-  ( A = 1 -> ( A - 1 ) = ( 1 - 1 ) )
19 18 3 eqtrdi 
 |-  ( A = 1 -> ( A - 1 ) = 0 )
20 oveq1 
 |-  ( A = 1 -> ( A ^ k ) = ( 1 ^ k ) )
21 20 sumeq2sdv 
 |-  ( A = 1 -> sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( 1 ^ k ) )
22 19 21 oveq12d 
 |-  ( A = 1 -> ( ( A - 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) = ( 0 x. sum_ k e. ( 0 ... ( N - 1 ) ) ( 1 ^ k ) ) )
23 17 22 eqeq12d 
 |-  ( A = 1 -> ( ( ( A ^ N ) - 1 ) = ( ( A - 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) <-> ( ( 1 ^ N ) - 1 ) = ( 0 x. sum_ k e. ( 0 ... ( N - 1 ) ) ( 1 ^ k ) ) ) )
24 15 23 syl5ibr 
 |-  ( A = 1 -> ( ph -> ( ( A ^ N ) - 1 ) = ( ( A - 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) ) )
25 1 adantl 
 |-  ( ( -. A = 1 /\ ph ) -> A e. CC )
26 neqne 
 |-  ( -. A = 1 -> A =/= 1 )
27 26 adantr 
 |-  ( ( -. A = 1 /\ ph ) -> A =/= 1 )
28 2 adantl 
 |-  ( ( -. A = 1 /\ ph ) -> N e. NN0 )
29 25 27 28 geoser 
 |-  ( ( -. A = 1 /\ ph ) -> sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) = ( ( 1 - ( A ^ N ) ) / ( 1 - A ) ) )
30 eqcom 
 |-  ( sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) = ( ( 1 - ( A ^ N ) ) / ( 1 - A ) ) <-> ( ( 1 - ( A ^ N ) ) / ( 1 - A ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) )
31 1cnd 
 |-  ( ( -. A = 1 /\ ph ) -> 1 e. CC )
32 1 2 expcld 
 |-  ( ph -> ( A ^ N ) e. CC )
33 32 adantl 
 |-  ( ( -. A = 1 /\ ph ) -> ( A ^ N ) e. CC )
34 nesym 
 |-  ( 1 =/= A <-> -. A = 1 )
35 34 biimpri 
 |-  ( -. A = 1 -> 1 =/= A )
36 35 adantr 
 |-  ( ( -. A = 1 /\ ph ) -> 1 =/= A )
37 31 33 31 25 36 div2subd 
 |-  ( ( -. A = 1 /\ ph ) -> ( ( 1 - ( A ^ N ) ) / ( 1 - A ) ) = ( ( ( A ^ N ) - 1 ) / ( A - 1 ) ) )
38 37 eqeq1d 
 |-  ( ( -. A = 1 /\ ph ) -> ( ( ( 1 - ( A ^ N ) ) / ( 1 - A ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) <-> ( ( ( A ^ N ) - 1 ) / ( A - 1 ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) )
39 peano2cnm 
 |-  ( ( A ^ N ) e. CC -> ( ( A ^ N ) - 1 ) e. CC )
40 32 39 syl 
 |-  ( ph -> ( ( A ^ N ) - 1 ) e. CC )
41 40 adantl 
 |-  ( ( -. A = 1 /\ ph ) -> ( ( A ^ N ) - 1 ) e. CC )
42 fzfid 
 |-  ( ( -. A = 1 /\ ph ) -> ( 0 ... ( N - 1 ) ) e. Fin )
43 25 adantr 
 |-  ( ( ( -. A = 1 /\ ph ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> A e. CC )
44 10 adantl 
 |-  ( ( ( -. A = 1 /\ ph ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> k e. NN0 )
45 43 44 expcld 
 |-  ( ( ( -. A = 1 /\ ph ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( A ^ k ) e. CC )
46 42 45 fsumcl 
 |-  ( ( -. A = 1 /\ ph ) -> sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) e. CC )
47 peano2cnm 
 |-  ( A e. CC -> ( A - 1 ) e. CC )
48 47 adantr 
 |-  ( ( A e. CC /\ -. A = 1 ) -> ( A - 1 ) e. CC )
49 simpl 
 |-  ( ( A e. CC /\ -. A = 1 ) -> A e. CC )
50 1cnd 
 |-  ( ( A e. CC /\ -. A = 1 ) -> 1 e. CC )
51 26 adantl 
 |-  ( ( A e. CC /\ -. A = 1 ) -> A =/= 1 )
52 49 50 51 subne0d 
 |-  ( ( A e. CC /\ -. A = 1 ) -> ( A - 1 ) =/= 0 )
53 48 52 jca 
 |-  ( ( A e. CC /\ -. A = 1 ) -> ( ( A - 1 ) e. CC /\ ( A - 1 ) =/= 0 ) )
54 53 ex 
 |-  ( A e. CC -> ( -. A = 1 -> ( ( A - 1 ) e. CC /\ ( A - 1 ) =/= 0 ) ) )
55 1 54 syl 
 |-  ( ph -> ( -. A = 1 -> ( ( A - 1 ) e. CC /\ ( A - 1 ) =/= 0 ) ) )
56 55 impcom 
 |-  ( ( -. A = 1 /\ ph ) -> ( ( A - 1 ) e. CC /\ ( A - 1 ) =/= 0 ) )
57 divmul2 
 |-  ( ( ( ( A ^ N ) - 1 ) e. CC /\ sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) e. CC /\ ( ( A - 1 ) e. CC /\ ( A - 1 ) =/= 0 ) ) -> ( ( ( ( A ^ N ) - 1 ) / ( A - 1 ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) <-> ( ( A ^ N ) - 1 ) = ( ( A - 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) ) )
58 41 46 56 57 syl3anc 
 |-  ( ( -. A = 1 /\ ph ) -> ( ( ( ( A ^ N ) - 1 ) / ( A - 1 ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) <-> ( ( A ^ N ) - 1 ) = ( ( A - 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) ) )
59 38 58 bitrd 
 |-  ( ( -. A = 1 /\ ph ) -> ( ( ( 1 - ( A ^ N ) ) / ( 1 - A ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) <-> ( ( A ^ N ) - 1 ) = ( ( A - 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) ) )
60 30 59 syl5bb 
 |-  ( ( -. A = 1 /\ ph ) -> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) = ( ( 1 - ( A ^ N ) ) / ( 1 - A ) ) <-> ( ( A ^ N ) - 1 ) = ( ( A - 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) ) )
61 29 60 mpbid 
 |-  ( ( -. A = 1 /\ ph ) -> ( ( A ^ N ) - 1 ) = ( ( A - 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) )
62 61 ex 
 |-  ( -. A = 1 -> ( ph -> ( ( A ^ N ) - 1 ) = ( ( A - 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) ) )
63 24 62 pm2.61i 
 |-  ( ph -> ( ( A ^ N ) - 1 ) = ( ( A - 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) )