Metamath Proof Explorer

Theorem geoisum1c

Description: The infinite sum of A x. ( R ^ 1 ) + A x. ( R ^ 2 ) ... is ( A x. R ) / ( 1 - R ) . (Contributed by NM, 2-Nov-2007) (Revised by Mario Carneiro, 26-Apr-2014)

Ref Expression
Assertion geoisum1c ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → Σ 𝑘 ∈ ℕ ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) = ( ( 𝐴 · 𝑅 ) / ( 1 − 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → 𝐴 ∈ ℂ )
2 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → 𝑅 ∈ ℂ )
3 ax-1cn ⊢ 1 ∈ ℂ
4 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( 1 − 𝑅 ) ∈ ℂ )
5 3 2 4 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → ( 1 − 𝑅 ) ∈ ℂ )
6 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → ( abs ‘ 𝑅 ) < 1 )
7 1re ⊢ 1 ∈ ℝ
8 7 ltnri ⊢ ¬ 1 < 1
9 abs1 ⊢ ( abs ‘ 1 ) = 1
10 fveq2 ⊢ ( 1 = 𝑅 → ( abs ‘ 1 ) = ( abs ‘ 𝑅 ) )
11 9 10 syl5eqr ⊢ ( 1 = 𝑅 → 1 = ( abs ‘ 𝑅 ) )
12 11 breq1d ⊢ ( 1 = 𝑅 → ( 1 < 1 ↔ ( abs ‘ 𝑅 ) < 1 ) )
13 8 12 mtbii ⊢ ( 1 = 𝑅 → ¬ ( abs ‘ 𝑅 ) < 1 )
14 13 necon2ai ⊢ ( ( abs ‘ 𝑅 ) < 1 → 1 ≠ 𝑅 )
15 6 14 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → 1 ≠ 𝑅 )
16 subeq0 ⊢ ( ( 1 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( ( 1 − 𝑅 ) = 0 ↔ 1 = 𝑅 ) )
17 16 necon3bid ⊢ ( ( 1 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( ( 1 − 𝑅 ) ≠ 0 ↔ 1 ≠ 𝑅 ) )
18 3 2 17 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → ( ( 1 − 𝑅 ) ≠ 0 ↔ 1 ≠ 𝑅 ) )
19 15 18 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → ( 1 − 𝑅 ) ≠ 0 )
20 1 2 5 19 divassd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → ( ( 𝐴 · 𝑅 ) / ( 1 − 𝑅 ) ) = ( 𝐴 · ( 𝑅 / ( 1 − 𝑅 ) ) ) )
21 geoisum1 ⊢ ( ( 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → Σ 𝑘 ∈ ℕ ( 𝑅 ↑ 𝑘 ) = ( 𝑅 / ( 1 − 𝑅 ) ) )
22 21 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → Σ 𝑘 ∈ ℕ ( 𝑅 ↑ 𝑘 ) = ( 𝑅 / ( 1 − 𝑅 ) ) )
23 22 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → ( 𝐴 · Σ 𝑘 ∈ ℕ ( 𝑅 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑅 / ( 1 − 𝑅 ) ) ) )
24 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
25 1zzd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → 1 ∈ ℤ )
26 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑅 ↑ 𝑛 ) = ( 𝑅 ↑ 𝑘 ) )
27 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) )
28 ovex ⊢ ( 𝑅 ↑ 𝑘 ) ∈ V
29 26 27 28 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝑅 ↑ 𝑘 ) )
30 29 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝑅 ↑ 𝑘 ) )
31 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
32 expcl ⊢ ( ( 𝑅 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑅 ↑ 𝑘 ) ∈ ℂ )
33 2 31 32 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑅 ↑ 𝑘 ) ∈ ℂ )
34 1nn0 ⊢ 1 ∈ ℕ0
35 34 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → 1 ∈ ℕ0 )
36 elnnuz ⊢ ( 𝑘 ∈ ℕ ↔ 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
37 36 30 sylan2br ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝑅 ↑ 𝑘 ) )
38 2 6 35 37 geolim2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ) ⇝ ( ( 𝑅 ↑ 1 ) / ( 1 − 𝑅 ) ) )
39 seqex ⊢ seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ) ∈ V
40 ovex ⊢ ( ( 𝑅 ↑ 1 ) / ( 1 − 𝑅 ) ) ∈ V
41 39 40 breldm ⊢ ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ) ⇝ ( ( 𝑅 ↑ 1 ) / ( 1 − 𝑅 ) ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ) ∈ dom ⇝ )
42 38 41 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ) ∈ dom ⇝ )
43 24 25 30 33 42 1 isummulc2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → ( 𝐴 · Σ 𝑘 ∈ ℕ ( 𝑅 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ℕ ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) )
44 20 23 43 3eqtr2rd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → Σ 𝑘 ∈ ℕ ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) = ( ( 𝐴 · 𝑅 ) / ( 1 − 𝑅 ) ) )