Theorem aaliou3lem4

Description: Lemma for aaliou3 . (Contributed by Stefan O'Rear, 16-Nov-2014)

	Ref	Expression
Hypotheses	aaliou3lem.c	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
	aaliou3lem.d	⊢ 𝐿 = Σ 𝑏 ∈ ℕ ( 𝐹 ‘ 𝑏 )
	aaliou3lem.e	⊢ 𝐻 = ( 𝑐 ∈ ℕ ↦ Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹 ‘ 𝑏 ) )
Assertion	aaliou3lem4	⊢ 𝐿 ∈ ℝ

Proof

Step	Hyp	Ref	Expression
1		aaliou3lem.c	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
2		aaliou3lem.d	⊢ 𝐿 = Σ 𝑏 ∈ ℕ ( 𝐹 ‘ 𝑏 )
3		aaliou3lem.e	⊢ 𝐻 = ( 𝑐 ∈ ℕ ↦ Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹 ‘ 𝑏 ) )
4		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
5	4	sumeq1i	⊢ Σ 𝑏 ∈ ℕ ( 𝐹 ‘ 𝑏 ) = Σ 𝑏 ∈ ( ℤ≥ ‘ 1 ) ( 𝐹 ‘ 𝑏 )
6	2 5	eqtri	⊢ 𝐿 = Σ 𝑏 ∈ ( ℤ≥ ‘ 1 ) ( 𝐹 ‘ 𝑏 )
7		1nn	⊢ 1 ∈ ℕ
8		eqid	⊢ ( 𝑐 ∈ ( ℤ≥ ‘ 1 ) ↦ ( ( 2 ↑ - ( ! ‘ 1 ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − 1 ) ) ) ) = ( 𝑐 ∈ ( ℤ≥ ‘ 1 ) ↦ ( ( 2 ↑ - ( ! ‘ 1 ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − 1 ) ) ) )
9	8 1	aaliou3lem3	⊢ ( 1 ∈ ℕ → ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ Σ 𝑏 ∈ ( ℤ≥ ‘ 1 ) ( 𝐹 ‘ 𝑏 ) ∈ ℝ+ ∧ Σ 𝑏 ∈ ( ℤ≥ ‘ 1 ) ( 𝐹 ‘ 𝑏 ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ 1 ) ) ) ) )
10	9	simp2d	⊢ ( 1 ∈ ℕ → Σ 𝑏 ∈ ( ℤ≥ ‘ 1 ) ( 𝐹 ‘ 𝑏 ) ∈ ℝ+ )
11		rpre	⊢ ( Σ 𝑏 ∈ ( ℤ≥ ‘ 1 ) ( 𝐹 ‘ 𝑏 ) ∈ ℝ+ → Σ 𝑏 ∈ ( ℤ≥ ‘ 1 ) ( 𝐹 ‘ 𝑏 ) ∈ ℝ )
12	7 10 11	mp2b	⊢ Σ 𝑏 ∈ ( ℤ≥ ‘ 1 ) ( 𝐹 ‘ 𝑏 ) ∈ ℝ
13	6 12	eqeltri	⊢ 𝐿 ∈ ℝ