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 ∈ ℕ ⟼ A 2 n = 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 ∈ ℕ → 2 n ∈ ℝ
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 ∈ ℕ → 2 n ≠ 0
20 9 14 19 redivcld ⊢ φ ∧ n ∈ ℕ → A 2 n ∈ ℝ
21 20 rexrd ⊢ φ ∧ n ∈ ℕ → A 2 n ∈ ℝ *
22 2rp ⊢ 2 ∈ ℝ +
23 22 a1i ⊢ φ ∧ n ∈ ℕ → 2 ∈ ℝ +
24 23 18 rpexpcld ⊢ φ ∧ n ∈ ℕ → 2 n ∈ ℝ +
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 ≤ A 2 n
31 20 ltpnfd ⊢ φ ∧ n ∈ ℕ → A 2 n < +∞
32 4 6 21 30 31 elicod ⊢ φ ∧ n ∈ ℕ → A 2 n ∈ 0 +∞
33 1zzd ⊢ φ → 1 ∈ ℤ
34 nnuz ⊢ ℕ = ℤ ≥ 1
35 8 recnd ⊢ φ → A ∈ ℂ
36 eqid ⊢ n ∈ ℕ ⟼ A 2 n = n ∈ ℕ ⟼ A 2 n
37 36 geo2lim ⊢ A ∈ ℂ → seq 1 + n ∈ ℕ ⟼ A 2 n ⇝ A
38 35 37 syl ⊢ φ → seq 1 + n ∈ ℕ ⟼ A 2 n ⇝ A
39 2 32 33 34 38 sge0isummpt ⊢ φ → sum^ ⁡ n ∈ ℕ ⟼ A 2 n = A