Metamath Proof Explorer

Theorem sge0ad2en

Description: The value of the infinite geometric series 2 ^ -u 1 + 2 ^ -u 2 + ... , multiplied by a constant. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis sge0ad2en.1 ⊢φ→A∈0+∞
Assertion sge0ad2en ⊢φ→sum^⁡n∈ℕ⟼A2n=A

Proof

Step Hyp Ref Expression
1 sge0ad2en.1 ⊢φ→A∈0+∞
2 nfv ⊢Ⅎnφ
3 0xr ⊢0∈ℝ*
4 3 a1i ⊢φ∧n∈ℕ→0∈ℝ*
5 pnfxr ⊢+∞∈ℝ*
6 5 a1i ⊢φ∧n∈ℕ→+∞∈ℝ*
7 rge0ssre ⊢0+∞⊆ℝ
8 7 1 sselid ⊢φ→A∈ℝ
9 8 adantr ⊢φ∧n∈ℕ→A∈ℝ
10 2re ⊢2∈ℝ
11 10 a1i ⊢φ∧n∈ℕ→2∈ℝ
12 nnnn0 ⊢n∈ℕ→n∈ℕ0
13 12 adantl ⊢φ∧n∈ℕ→n∈ℕ0
14 11 13 reexpcld ⊢φ∧n∈ℕ→2n∈ℝ
15 2cnd ⊢φ∧n∈ℕ→2∈ℂ
16 2ne0 ⊢2≠0
17 16 a1i ⊢φ∧n∈ℕ→2≠0
18 13 nn0zd ⊢φ∧n∈ℕ→n∈ℤ
19 15 17 18 expne0d ⊢φ∧n∈ℕ→2n≠0
20 9 14 19 redivcld ⊢φ∧n∈ℕ→A2n∈ℝ
21 20 rexrd ⊢φ∧n∈ℕ→A2n∈ℝ*
22 2rp ⊢2∈ℝ+
23 22 a1i ⊢φ∧n∈ℕ→2∈ℝ+
24 23 18 rpexpcld ⊢φ∧n∈ℕ→2n∈ℝ+
25 3 a1i ⊢φ→0∈ℝ*
26 5 a1i ⊢φ→+∞∈ℝ*
27 icogelb ⊢0∈ℝ*∧+∞∈ℝ*∧A∈0+∞→0≤A
28 25 26 1 27 syl3anc ⊢φ→0≤A
29 28 adantr ⊢φ∧n∈ℕ→0≤A
30 9 24 29 divge0d ⊢φ∧n∈ℕ→0≤A2n
31 20 ltpnfd ⊢φ∧n∈ℕ→A2n<+∞
32 4 6 21 30 31 elicod ⊢φ∧n∈ℕ→A2n∈0+∞
33 1zzd ⊢φ→1∈ℤ
34 nnuz ⊢ℕ=ℤ≥1
35 8 recnd ⊢φ→A∈ℂ
36 eqid ⊢n∈ℕ⟼A2n=n∈ℕ⟼A2n
37 36 geo2lim ⊢A∈ℂ→seq1+n∈ℕ⟼A2n⇝A
38 35 37 syl ⊢φ→seq1+n∈ℕ⟼A2n⇝A
39 2 32 33 34 38 sge0isummpt ⊢φ→sum^⁡n∈ℕ⟼A2n=A