Theorem aaliou3lem4

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

	Ref	Expression
Hypotheses	aaliou3lem.c	$$⊢F=\left(a\in \mathbb{N}⟼2^{-a!}\right)$$
	aaliou3lem.d	$$⊢L=\sum _{b\in \mathbb{N}}F\left(b\right)$$
	aaliou3lem.e	$$⊢H=\left(c\in \mathbb{N}⟼\sum _{b=1}^{c}F\left(b\right)\right)$$
Assertion	aaliou3lem4	$$⊢L\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		aaliou3lem.c	$$⊢F=\left(a\in \mathbb{N}⟼2^{-a!}\right)$$
2		aaliou3lem.d	$$⊢L=\sum _{b\in \mathbb{N}}F\left(b\right)$$
3		aaliou3lem.e	$$⊢H=\left(c\in \mathbb{N}⟼\sum _{b=1}^{c}F\left(b\right)\right)$$
4		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
5	4	sumeq1i	$$⊢\sum _{b\in \mathbb{N}}F\left(b\right)=\sum _{b\in {\mathbb{Z}}_{\ge 1}}F\left(b\right)$$
6	2 5	eqtri	$$⊢L=\sum _{b\in {\mathbb{Z}}_{\ge 1}}F\left(b\right)$$
7		1nn	$$⊢1\in \mathbb{N}$$
8		eqid	$$⊢\left(c\in {\mathbb{Z}}_{\ge 1}⟼2^{-1!}{\left(\frac{1}{2}\right)}^{c-1}\right)=\left(c\in {\mathbb{Z}}_{\ge 1}⟼2^{-1!}{\left(\frac{1}{2}\right)}^{c-1}\right)$$
9	8 1	aaliou3lem3	$$⊢1\in \mathbb{N}\to \left(seq1\left(+,F\right)\in \mathrm{dom}⇝\wedge \sum _{b\in {\mathbb{Z}}_{\ge 1}}F\left(b\right)\in {ℝ}^{+}\wedge \sum _{b\in {\mathbb{Z}}_{\ge 1}}F\left(b\right)\le 22^{-1!}\right)$$
10	9	simp2d	$$⊢1\in \mathbb{N}\to \sum _{b\in {\mathbb{Z}}_{\ge 1}}F\left(b\right)\in {ℝ}^{+}$$
11		rpre	$$⊢\sum _{b\in {\mathbb{Z}}_{\ge 1}}F\left(b\right)\in {ℝ}^{+}\to \sum _{b\in {\mathbb{Z}}_{\ge 1}}F\left(b\right)\in ℝ$$
12	7 10 11	mp2b	$$⊢\sum _{b\in {\mathbb{Z}}_{\ge 1}}F\left(b\right)\in ℝ$$
13	6 12	eqeltri	$$⊢L\in ℝ$$