This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
geoserg.2 ⊢ ( 𝜑 → 𝐴 ≠ 1 )
geoserg.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
geoserg.4 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
Assertion geoserg ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) = ( ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) / ( 1 − 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 geoserg.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 geoserg.2 ⊢ ( 𝜑 → 𝐴 ≠ 1 )
3 geoserg.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
4 geoserg.4 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5 fzofi ⊢ ( 𝑀 ..^ 𝑁 ) ∈ Fin
6 5 a1i ⊢ ( 𝜑 → ( 𝑀 ..^ 𝑁 ) ∈ Fin )
7 ax-1cn ⊢ 1 ∈ ℂ
8 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 − 𝐴 ) ∈ ℂ )
9 7 1 8 sylancr ⊢ ( 𝜑 → ( 1 − 𝐴 ) ∈ ℂ )
10 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐴 ∈ ℂ )
11 elfzouz ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
12 eluznn0 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ0 )
13 3 11 12 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
14 10 13 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
15 6 9 14 fsummulc1 ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) · ( 1 − 𝐴 ) ) = Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 1 − 𝐴 ) ) )
16 7 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 1 ∈ ℂ )
17 14 16 10 subdid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐴 ↑ 𝑘 ) · ( 1 − 𝐴 ) ) = ( ( ( 𝐴 ↑ 𝑘 ) · 1 ) − ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) )
18 14 mulridd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐴 ↑ 𝑘 ) · 1 ) = ( 𝐴 ↑ 𝑘 ) )
19 10 13 expp1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
20 19 eqcomd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
21 18 20 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝐴 ↑ 𝑘 ) · 1 ) − ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) = ( ( 𝐴 ↑ 𝑘 ) − ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) )
22 17 21 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐴 ↑ 𝑘 ) · ( 1 − 𝐴 ) ) = ( ( 𝐴 ↑ 𝑘 ) − ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) )
23 22 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 1 − 𝐴 ) ) = Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) − ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) )
24 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑘 ) )
25 oveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
26 oveq2 ⊢ ( 𝑗 = 𝑀 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑀 ) )
27 oveq2 ⊢ ( 𝑗 = 𝑁 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑁 ) )
28 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
29 elfzuz ⊢ ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
30 eluznn0 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑗 ∈ ℕ0 )
31 3 29 30 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑗 ∈ ℕ0 )
32 28 31 expcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐴 ↑ 𝑗 ) ∈ ℂ )
33 24 25 26 27 4 32 telfsumo ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) − ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) )
34 15 23 33 3eqtrrd ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) = ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) · ( 1 − 𝐴 ) ) )
35 1 3 expcld ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑀 ) ∈ ℂ )
36 eluznn0 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ ℕ0 )
37 3 4 36 syl2anc ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
38 1 37 expcld ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
39 35 38 subcld ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) ∈ ℂ )
40 6 14 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
41 2 necomd ⊢ ( 𝜑 → 1 ≠ 𝐴 )
42 subeq0 ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
43 7 1 42 sylancr ⊢ ( 𝜑 → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
44 43 necon3bid ⊢ ( 𝜑 → ( ( 1 − 𝐴 ) ≠ 0 ↔ 1 ≠ 𝐴 ) )
45 41 44 mpbird ⊢ ( 𝜑 → ( 1 − 𝐴 ) ≠ 0 )
46 39 40 9 45 divmul3d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) / ( 1 − 𝐴 ) ) = Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) ↔ ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) = ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) · ( 1 − 𝐴 ) ) ) )
47 34 46 mpbird ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) / ( 1 − 𝐴 ) ) = Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) )
48 47 eqcomd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) = ( ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) / ( 1 − 𝐴 ) ) )