Metamath Proof Explorer


Theorem geoserg

Description: The value of the finite geometric series A ^ M + A ^ ( M + 1 ) + ... + A ^ ( N - 1 ) . (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses geoserg.1 φ A
geoserg.2 φ A 1
geoserg.3 φ M 0
geoserg.4 φ N M
Assertion geoserg φ k M ..^ N A k = A M A N 1 A

Proof

Step Hyp Ref Expression
1 geoserg.1 φ A
2 geoserg.2 φ A 1
3 geoserg.3 φ M 0
4 geoserg.4 φ N M
5 fzofi M ..^ N Fin
6 5 a1i φ M ..^ N Fin
7 ax-1cn 1
8 subcl 1 A 1 A
9 7 1 8 sylancr φ 1 A
10 1 adantr φ k M ..^ N A
11 elfzouz k M ..^ N k M
12 eluznn0 M 0 k M k 0
13 3 11 12 syl2an φ k M ..^ N k 0
14 10 13 expcld φ k M ..^ N A k
15 6 9 14 fsummulc1 φ k M ..^ N A k 1 A = k M ..^ N A k 1 A
16 7 a1i φ k M ..^ N 1
17 14 16 10 subdid φ k M ..^ N A k 1 A = A k 1 A k A
18 14 mulid1d φ k M ..^ N A k 1 = A k
19 10 13 expp1d φ k M ..^ N A k + 1 = A k A
20 19 eqcomd φ k M ..^ N A k A = A k + 1
21 18 20 oveq12d φ k M ..^ N A k 1 A k A = A k A k + 1
22 17 21 eqtrd φ k M ..^ N A k 1 A = A k A k + 1
23 22 sumeq2dv φ k M ..^ N A k 1 A = k M ..^ N A k A k + 1
24 oveq2 j = k A j = A k
25 oveq2 j = k + 1 A j = A k + 1
26 oveq2 j = M A j = A M
27 oveq2 j = N A j = A N
28 1 adantr φ j M N A
29 elfzuz j M N j M
30 eluznn0 M 0 j M j 0
31 3 29 30 syl2an φ j M N j 0
32 28 31 expcld φ j M N A j
33 24 25 26 27 4 32 telfsumo φ k M ..^ N A k A k + 1 = A M A N
34 15 23 33 3eqtrrd φ A M A N = k M ..^ N A k 1 A
35 1 3 expcld φ A M
36 eluznn0 M 0 N M N 0
37 3 4 36 syl2anc φ N 0
38 1 37 expcld φ A N
39 35 38 subcld φ A M A N
40 6 14 fsumcl φ k M ..^ N A k
41 2 necomd φ 1 A
42 subeq0 1 A 1 A = 0 1 = A
43 7 1 42 sylancr φ 1 A = 0 1 = A
44 43 necon3bid φ 1 A 0 1 A
45 41 44 mpbird φ 1 A 0
46 39 40 9 45 divmul3d φ A M A N 1 A = k M ..^ N A k A M A N = k M ..^ N A k 1 A
47 34 46 mpbird φ A M A N 1 A = k M ..^ N A k
48 47 eqcomd φ k M ..^ N A k = A M A N 1 A