Theorem aaliou3lem5

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	aaliou3lem5	$$⊢A\in \mathbb{N}\to H\left(A\right)\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		oveq2	$$⊢c=A\to \left(1\dots c\right)=\left(1\dots A\right)$$
5	4	sumeq1d	$$⊢c=A\to \sum _{b=1}^{c}F\left(b\right)=\sum _{b=1}^{A}F\left(b\right)$$
6		sumex	$$⊢\sum _{b=1}^{A}F\left(b\right)\in \mathrm{V}$$
7	5 3 6	fvmpt	$$⊢A\in \mathbb{N}\to H\left(A\right)=\sum _{b=1}^{A}F\left(b\right)$$
8		fzfid	$$⊢A\in \mathbb{N}\to \left(1\dots A\right)\in \mathrm{Fin}$$
9		elfznn	$$⊢b\in \left(1\dots A\right)\to b\in \mathbb{N}$$
10	9	adantl	$$⊢\left(A\in \mathbb{N}\wedge b\in \left(1\dots A\right)\right)\to b\in \mathbb{N}$$
11		fveq2	$$⊢a=b\to a!=b!$$
12	11	negeqd	$$⊢a=b\to -a!=-b!$$
13	12	oveq2d	$$⊢a=b\to 2^{-a!}=2^{-b!}$$
14		ovex	$$⊢2^{-b!}\in \mathrm{V}$$
15	13 1 14	fvmpt	$$⊢b\in \mathbb{N}\to F\left(b\right)=2^{-b!}$$
16		2rp	$$⊢2\in {ℝ}^{+}$$
17		nnnn0	$$⊢b\in \mathbb{N}\to b\in {\mathbb{N}}_0$$
18	17	faccld	$$⊢b\in \mathbb{N}\to b!\in \mathbb{N}$$
19	18	nnzd	$$⊢b\in \mathbb{N}\to b!\in \mathbb{Z}$$
20	19	znegcld	$$⊢b\in \mathbb{N}\to -b!\in \mathbb{Z}$$
21		rpexpcl	$$⊢\left(2\in {ℝ}^{+}\wedge -b!\in \mathbb{Z}\right)\to 2^{-b!}\in {ℝ}^{+}$$
22	16 20 21	sylancr	$$⊢b\in \mathbb{N}\to 2^{-b!}\in {ℝ}^{+}$$
23	22	rpred	$$⊢b\in \mathbb{N}\to 2^{-b!}\in ℝ$$
24	15 23	eqeltrd	$$⊢b\in \mathbb{N}\to F\left(b\right)\in ℝ$$
25	10 24	syl	$$⊢\left(A\in \mathbb{N}\wedge b\in \left(1\dots A\right)\right)\to F\left(b\right)\in ℝ$$
26	8 25	fsumrecl	$$⊢A\in \mathbb{N}\to \sum _{b=1}^{A}F\left(b\right)\in ℝ$$
27	7 26	eqeltrd	$$⊢A\in \mathbb{N}\to H\left(A\right)\in ℝ$$