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	⊢ ( 𝜑 → 𝐴 ∈ ( 0 [,) +∞ ) )
Assertion	sge0ad2en	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝐴 / ( 2 ↑ 𝑛 ) ) ) ) = 𝐴 )

Proof

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