Theorem aaliou3lem3

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

	Ref	Expression
Hypotheses	aaliou3lem.a	$$⊢G=\left(c\in {\mathbb{Z}}_{\ge A}⟼2^{-A!}{\left(\frac{1}{2}\right)}^{c-A}\right)$$
	aaliou3lem.b	$$⊢F=\left(a\in \mathbb{N}⟼2^{-a!}\right)$$
Assertion	aaliou3lem3	$$⊢A\in \mathbb{N}\to \left(seqA\left(+,F\right)\in \mathrm{dom}⇝\wedge \sum _{b\in {\mathbb{Z}}_{\ge A}}F\left(b\right)\in {ℝ}^{+}\wedge \sum _{b\in {\mathbb{Z}}_{\ge A}}F\left(b\right)\le 22^{-A!}\right)$$

Proof

Step	Hyp	Ref	Expression
1		aaliou3lem.a	$$⊢G=\left(c\in {\mathbb{Z}}_{\ge A}⟼2^{-A!}{\left(\frac{1}{2}\right)}^{c-A}\right)$$
2		aaliou3lem.b	$$⊢F=\left(a\in \mathbb{N}⟼2^{-a!}\right)$$
3		eqid	$$⊢{\mathbb{Z}}_{\ge A}={\mathbb{Z}}_{\ge A}$$
4		nnz	$$⊢A\in \mathbb{N}\to A\in \mathbb{Z}$$
5		uzid	$$⊢A\in \mathbb{Z}\to A\in {\mathbb{Z}}_{\ge A}$$
6	4 5	syl	$$⊢A\in \mathbb{N}\to A\in {\mathbb{Z}}_{\ge A}$$
7	1	aaliou3lem1	$$⊢\left(A\in \mathbb{N}\wedge b\in {\mathbb{Z}}_{\ge A}\right)\to G\left(b\right)\in ℝ$$
8	1 2	aaliou3lem2	$$⊢\left(A\in \mathbb{N}\wedge b\in {\mathbb{Z}}_{\ge A}\right)\to F\left(b\right)\in \left(0,G\left(b\right)\right]$$
9		0xr	$$⊢0\in {ℝ}^{*}$$
10		elioc2	$$⊢\left(0\in {ℝ}^{*}\wedge G\left(b\right)\in ℝ\right)\to \left(F\left(b\right)\in \left(0,G\left(b\right)\right]\leftrightarrow \left(F\left(b\right)\in ℝ\wedge 0<F\left(b\right)\wedge F\left(b\right)\le G\left(b\right)\right)\right)$$
11	9 7 10	sylancr	$$⊢\left(A\in \mathbb{N}\wedge b\in {\mathbb{Z}}_{\ge A}\right)\to \left(F\left(b\right)\in \left(0,G\left(b\right)\right]\leftrightarrow \left(F\left(b\right)\in ℝ\wedge 0<F\left(b\right)\wedge F\left(b\right)\le G\left(b\right)\right)\right)$$
12	8 11	mpbid	$$⊢\left(A\in \mathbb{N}\wedge b\in {\mathbb{Z}}_{\ge A}\right)\to \left(F\left(b\right)\in ℝ\wedge 0<F\left(b\right)\wedge F\left(b\right)\le G\left(b\right)\right)$$
13	12	simp1d	$$⊢\left(A\in \mathbb{N}\wedge b\in {\mathbb{Z}}_{\ge A}\right)\to F\left(b\right)\in ℝ$$
14		halfcn	$$⊢\frac{1}{2}\in ℂ$$
15	14	a1i	$$⊢A\in \mathbb{N}\to \frac{1}{2}\in ℂ$$
16		halfre	$$⊢\frac{1}{2}\in ℝ$$
17		halfgt0	$$⊢0<\frac{1}{2}$$
18	16 17	elrpii	$$⊢\frac{1}{2}\in {ℝ}^{+}$$
19		rprege0	$$⊢\frac{1}{2}\in {ℝ}^{+}\to \left(\frac{1}{2}\in ℝ\wedge 0\le \frac{1}{2}\right)$$
20		absid	$$⊢\left(\frac{1}{2}\in ℝ\wedge 0\le \frac{1}{2}\right)\to \left|\frac{1}{2}\right|=\frac{1}{2}$$
21	18 19 20	mp2b	$$⊢\left|\frac{1}{2}\right|=\frac{1}{2}$$
22		halflt1	$$⊢\frac{1}{2}<1$$
23	21 22	eqbrtri	$$⊢\left|\frac{1}{2}\right|<1$$
24	23	a1i	$$⊢A\in \mathbb{N}\to \left|\frac{1}{2}\right|<1$$
25		2rp	$$⊢2\in {ℝ}^{+}$$
26		nnnn0	$$⊢A\in \mathbb{N}\to A\in {\mathbb{N}}_0$$
27	26	faccld	$$⊢A\in \mathbb{N}\to A!\in \mathbb{N}$$
28	27	nnzd	$$⊢A\in \mathbb{N}\to A!\in \mathbb{Z}$$
29	28	znegcld	$$⊢A\in \mathbb{N}\to -A!\in \mathbb{Z}$$
30		rpexpcl	$$⊢\left(2\in {ℝ}^{+}\wedge -A!\in \mathbb{Z}\right)\to 2^{-A!}\in {ℝ}^{+}$$
31	25 29 30	sylancr	$$⊢A\in \mathbb{N}\to 2^{-A!}\in {ℝ}^{+}$$
32	31	rpcnd	$$⊢A\in \mathbb{N}\to 2^{-A!}\in ℂ$$
33	4 15 24 32 1	geolim3	$$⊢A\in \mathbb{N}\to seqA\left(+,G\right)⇝\left(\frac{2^{-A!}}{1-\left(\frac{1}{2}\right)}\right)$$
34		seqex	$$⊢seqA\left(+,G\right)\in \mathrm{V}$$
35		ovex	$$⊢\frac{2^{-A!}}{1-\left(\frac{1}{2}\right)}\in \mathrm{V}$$
36	34 35	breldm	$$⊢seqA\left(+,G\right)⇝\left(\frac{2^{-A!}}{1-\left(\frac{1}{2}\right)}\right)\to seqA\left(+,G\right)\in \mathrm{dom}⇝$$
37	33 36	syl	$$⊢A\in \mathbb{N}\to seqA\left(+,G\right)\in \mathrm{dom}⇝$$
38	12	simp2d	$$⊢\left(A\in \mathbb{N}\wedge b\in {\mathbb{Z}}_{\ge A}\right)\to 0<F\left(b\right)$$
39	13 38	elrpd	$$⊢\left(A\in \mathbb{N}\wedge b\in {\mathbb{Z}}_{\ge A}\right)\to F\left(b\right)\in {ℝ}^{+}$$
40	39	rpge0d	$$⊢\left(A\in \mathbb{N}\wedge b\in {\mathbb{Z}}_{\ge A}\right)\to 0\le F\left(b\right)$$
41	12	simp3d	$$⊢\left(A\in \mathbb{N}\wedge b\in {\mathbb{Z}}_{\ge A}\right)\to F\left(b\right)\le G\left(b\right)$$
42	3 6 7 13 37 40 41	cvgcmp	$$⊢A\in \mathbb{N}\to seqA\left(+,F\right)\in \mathrm{dom}⇝$$
43		eqidd	$$⊢\left(A\in \mathbb{N}\wedge b\in {\mathbb{Z}}_{\ge A}\right)\to F\left(b\right)=F\left(b\right)$$
44	3 3 6 43 39 42	isumrpcl	$$⊢A\in \mathbb{N}\to \sum _{b\in {\mathbb{Z}}_{\ge A}}F\left(b\right)\in {ℝ}^{+}$$
45		eqidd	$$⊢\left(A\in \mathbb{N}\wedge b\in {\mathbb{Z}}_{\ge A}\right)\to G\left(b\right)=G\left(b\right)$$
46	3 4 43 13 45 7 41 42 37	isumle	$$⊢A\in \mathbb{N}\to \sum _{b\in {\mathbb{Z}}_{\ge A}}F\left(b\right)\le \sum _{b\in {\mathbb{Z}}_{\ge A}}G\left(b\right)$$
47	7	recnd	$$⊢\left(A\in \mathbb{N}\wedge b\in {\mathbb{Z}}_{\ge A}\right)\to G\left(b\right)\in ℂ$$
48	3 4 45 47 33	isumclim	$$⊢A\in \mathbb{N}\to \sum _{b\in {\mathbb{Z}}_{\ge A}}G\left(b\right)=\frac{2^{-A!}}{1-\left(\frac{1}{2}\right)}$$
49		1mhlfehlf	$$⊢1-\left(\frac{1}{2}\right)=\frac{1}{2}$$
50	49	oveq2i	$$⊢\frac{2^{-A!}}{1-\left(\frac{1}{2}\right)}=\frac{2^{-A!}}{\frac{1}{2}}$$
51		2cn	$$⊢2\in ℂ$$
52		mulcl	$$⊢\left(2^{-A!}\in ℂ\wedge 2\in ℂ\right)\to 2^{-A!}\cdot 2\in ℂ$$
53	32 51 52	sylancl	$$⊢A\in \mathbb{N}\to 2^{-A!}\cdot 2\in ℂ$$
54	53	div1d	$$⊢A\in \mathbb{N}\to \frac{2^{-A!}\cdot 2}{1}=2^{-A!}\cdot 2$$
55		1rp	$$⊢1\in {ℝ}^{+}$$
56		rpcnne0	$$⊢1\in {ℝ}^{+}\to \left(1\in ℂ\wedge 1\ne 0\right)$$
57	55 56	ax-mp	$$⊢\left(1\in ℂ\wedge 1\ne 0\right)$$
58		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
59		divdiv2	$$⊢\left(2^{-A!}\in ℂ\wedge \left(1\in ℂ\wedge 1\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{2^{-A!}}{\frac{1}{2}}=\frac{2^{-A!}\cdot 2}{1}$$
60	57 58 59	mp3an23	$$⊢2^{-A!}\in ℂ\to \frac{2^{-A!}}{\frac{1}{2}}=\frac{2^{-A!}\cdot 2}{1}$$
61	32 60	syl	$$⊢A\in \mathbb{N}\to \frac{2^{-A!}}{\frac{1}{2}}=\frac{2^{-A!}\cdot 2}{1}$$
62		mulcom	$$⊢\left(2\in ℂ\wedge 2^{-A!}\in ℂ\right)\to 22^{-A!}=2^{-A!}\cdot 2$$
63	51 32 62	sylancr	$$⊢A\in \mathbb{N}\to 22^{-A!}=2^{-A!}\cdot 2$$
64	54 61 63	3eqtr4d	$$⊢A\in \mathbb{N}\to \frac{2^{-A!}}{\frac{1}{2}}=22^{-A!}$$
65	50 64	syl5eq	$$⊢A\in \mathbb{N}\to \frac{2^{-A!}}{1-\left(\frac{1}{2}\right)}=22^{-A!}$$
66	48 65	eqtrd	$$⊢A\in \mathbb{N}\to \sum _{b\in {\mathbb{Z}}_{\ge A}}G\left(b\right)=22^{-A!}$$
67	46 66	breqtrd	$$⊢A\in \mathbb{N}\to \sum _{b\in {\mathbb{Z}}_{\ge A}}F\left(b\right)\le 22^{-A!}$$
68	42 44 67	3jca	$$⊢A\in \mathbb{N}\to \left(seqA\left(+,F\right)\in \mathrm{dom}⇝\wedge \sum _{b\in {\mathbb{Z}}_{\ge A}}F\left(b\right)\in {ℝ}^{+}\wedge \sum _{b\in {\mathbb{Z}}_{\ge A}}F\left(b\right)\le 22^{-A!}\right)$$