Theorem aaliou3lem7

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	aaliou3lem7	$$⊢A\in \mathbb{N}\to \left(H\left(A\right)\ne L\wedge \left|L-H\left(A\right)\right|\le 22^{-\left(A+1\right)!}\right)$$

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		peano2nn	$$⊢A\in \mathbb{N}\to A+1\in \mathbb{N}$$
5		eqid	$$⊢\left(c\in {\mathbb{Z}}_{\ge \left(A+1\right)}⟼2^{-\left(A+1\right)!}{\left(\frac{1}{2}\right)}^{c-\left(A+1\right)}\right)=\left(c\in {\mathbb{Z}}_{\ge \left(A+1\right)}⟼2^{-\left(A+1\right)!}{\left(\frac{1}{2}\right)}^{c-\left(A+1\right)}\right)$$
6	5 1	aaliou3lem3	$$⊢A+1\in \mathbb{N}\to \left(seq\left(A+1\right)\left(+,F\right)\in \mathrm{dom}⇝\wedge \sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\in {ℝ}^{+}\wedge \sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\le 22^{-\left(A+1\right)!}\right)$$
7		3simpc	$$⊢\left(seq\left(A+1\right)\left(+,F\right)\in \mathrm{dom}⇝\wedge \sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\in {ℝ}^{+}\wedge \sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\le 22^{-\left(A+1\right)!}\right)\to \left(\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\in {ℝ}^{+}\wedge \sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\le 22^{-\left(A+1\right)!}\right)$$
8	4 6 7	3syl	$$⊢A\in \mathbb{N}\to \left(\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\in {ℝ}^{+}\wedge \sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\le 22^{-\left(A+1\right)!}\right)$$
9		nncn	$$⊢A\in \mathbb{N}\to A\in ℂ$$
10		ax-1cn	$$⊢1\in ℂ$$
11		pncan	$$⊢\left(A\in ℂ\wedge 1\in ℂ\right)\to A+1-1=A$$
12	9 10 11	sylancl	$$⊢A\in \mathbb{N}\to A+1-1=A$$
13	12	oveq2d	$$⊢A\in \mathbb{N}\to \left(1\dots A+1-1\right)=\left(1\dots A\right)$$
14	13	sumeq1d	$$⊢A\in \mathbb{N}\to \sum _{b=1}^{A+1-1}F\left(b\right)=\sum _{b=1}^{A}F\left(b\right)$$
15	14	oveq1d	$$⊢A\in \mathbb{N}\to \sum _{b=1}^{A+1-1}F\left(b\right)+\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)=\sum _{b=1}^{A}F\left(b\right)+\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)$$
16		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
17		eqid	$$⊢{\mathbb{Z}}_{\ge \left(A+1\right)}={\mathbb{Z}}_{\ge \left(A+1\right)}$$
18		eqidd	$$⊢\left(A\in \mathbb{N}\wedge b\in \mathbb{N}\right)\to F\left(b\right)=F\left(b\right)$$
19		fveq2	$$⊢a=b\to a!=b!$$
20	19	negeqd	$$⊢a=b\to -a!=-b!$$
21	20	oveq2d	$$⊢a=b\to 2^{-a!}=2^{-b!}$$
22		ovex	$$⊢2^{-b!}\in \mathrm{V}$$
23	21 1 22	fvmpt	$$⊢b\in \mathbb{N}\to F\left(b\right)=2^{-b!}$$
24		2rp	$$⊢2\in {ℝ}^{+}$$
25		nnnn0	$$⊢b\in \mathbb{N}\to b\in {\mathbb{N}}_0$$
26		faccl	$$⊢b\in {\mathbb{N}}_0\to b!\in \mathbb{N}$$
27	25 26	syl	$$⊢b\in \mathbb{N}\to b!\in \mathbb{N}$$
28	27	nnzd	$$⊢b\in \mathbb{N}\to b!\in \mathbb{Z}$$
29	28	znegcld	$$⊢b\in \mathbb{N}\to -b!\in \mathbb{Z}$$
30		rpexpcl	$$⊢\left(2\in {ℝ}^{+}\wedge -b!\in \mathbb{Z}\right)\to 2^{-b!}\in {ℝ}^{+}$$
31	24 29 30	sylancr	$$⊢b\in \mathbb{N}\to 2^{-b!}\in {ℝ}^{+}$$
32	31	rpcnd	$$⊢b\in \mathbb{N}\to 2^{-b!}\in ℂ$$
33	23 32	eqeltrd	$$⊢b\in \mathbb{N}\to F\left(b\right)\in ℂ$$
34	33	adantl	$$⊢\left(A\in \mathbb{N}\wedge b\in \mathbb{N}\right)\to F\left(b\right)\in ℂ$$
35		1nn	$$⊢1\in \mathbb{N}$$
36		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)$$
37	36 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)$$
38	37	simp1d	$$⊢1\in \mathbb{N}\to seq1\left(+,F\right)\in \mathrm{dom}⇝$$
39	35 38	mp1i	$$⊢A\in \mathbb{N}\to seq1\left(+,F\right)\in \mathrm{dom}⇝$$
40	16 17 4 18 34 39	isumsplit	$$⊢A\in \mathbb{N}\to \sum _{b\in \mathbb{N}}F\left(b\right)=\sum _{b=1}^{A+1-1}F\left(b\right)+\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)$$
41		oveq2	$$⊢c=A\to \left(1\dots c\right)=\left(1\dots A\right)$$
42	41	sumeq1d	$$⊢c=A\to \sum _{b=1}^{c}F\left(b\right)=\sum _{b=1}^{A}F\left(b\right)$$
43		sumex	$$⊢\sum _{b=1}^{A}F\left(b\right)\in \mathrm{V}$$
44	42 3 43	fvmpt	$$⊢A\in \mathbb{N}\to H\left(A\right)=\sum _{b=1}^{A}F\left(b\right)$$
45	44	oveq1d	$$⊢A\in \mathbb{N}\to H\left(A\right)+\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)=\sum _{b=1}^{A}F\left(b\right)+\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)$$
46	15 40 45	3eqtr4rd	$$⊢A\in \mathbb{N}\to H\left(A\right)+\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)=\sum _{b\in \mathbb{N}}F\left(b\right)$$
47	46 2	eqtr4di	$$⊢A\in \mathbb{N}\to H\left(A\right)+\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)=L$$
48	1 2 3	aaliou3lem4	$$⊢L\in ℝ$$
49	48	recni	$$⊢L\in ℂ$$
50	49	a1i	$$⊢A\in \mathbb{N}\to L\in ℂ$$
51	1 2 3	aaliou3lem5	$$⊢A\in \mathbb{N}\to H\left(A\right)\in ℝ$$
52	51	recnd	$$⊢A\in \mathbb{N}\to H\left(A\right)\in ℂ$$
53	6	simp2d	$$⊢A+1\in \mathbb{N}\to \sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\in {ℝ}^{+}$$
54	4 53	syl	$$⊢A\in \mathbb{N}\to \sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\in {ℝ}^{+}$$
55	54	rpcnd	$$⊢A\in \mathbb{N}\to \sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\in ℂ$$
56	50 52 55	subaddd	$$⊢A\in \mathbb{N}\to \left(L-H\left(A\right)=\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\leftrightarrow H\left(A\right)+\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)=L\right)$$
57	47 56	mpbird	$$⊢A\in \mathbb{N}\to L-H\left(A\right)=\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)$$
58	57	eqcomd	$$⊢A\in \mathbb{N}\to \sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)=L-H\left(A\right)$$
59		eleq1	$$⊢\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)=L-H\left(A\right)\to \left(\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\in {ℝ}^{+}\leftrightarrow L-H\left(A\right)\in {ℝ}^{+}\right)$$
60		breq1	$$⊢\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)=L-H\left(A\right)\to \left(\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\le 22^{-\left(A+1\right)!}\leftrightarrow L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)$$
61	59 60	anbi12d	$$⊢\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)=L-H\left(A\right)\to \left(\left(\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\in {ℝ}^{+}\wedge \sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\le 22^{-\left(A+1\right)!}\right)\leftrightarrow \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)$$
62	58 61	syl	$$⊢A\in \mathbb{N}\to \left(\left(\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\in {ℝ}^{+}\wedge \sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\le 22^{-\left(A+1\right)!}\right)\leftrightarrow \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)$$
63	51	adantr	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to H\left(A\right)\in ℝ$$
64		simprl	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to L-H\left(A\right)\in {ℝ}^{+}$$
65		difrp	$$⊢\left(H\left(A\right)\in ℝ\wedge L\in ℝ\right)\to \left(H\left(A\right)<L\leftrightarrow L-H\left(A\right)\in {ℝ}^{+}\right)$$
66	63 48 65	sylancl	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to \left(H\left(A\right)<L\leftrightarrow L-H\left(A\right)\in {ℝ}^{+}\right)$$
67	64 66	mpbird	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to H\left(A\right)<L$$
68	63 67	ltned	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to H\left(A\right)\ne L$$
69		nnnn0	$$⊢A+1\in \mathbb{N}\to A+1\in {\mathbb{N}}_0$$
70		faccl	$$⊢A+1\in {\mathbb{N}}_0\to \left(A+1\right)!\in \mathbb{N}$$
71	4 69 70	3syl	$$⊢A\in \mathbb{N}\to \left(A+1\right)!\in \mathbb{N}$$
72	71	nnzd	$$⊢A\in \mathbb{N}\to \left(A+1\right)!\in \mathbb{Z}$$
73	72	znegcld	$$⊢A\in \mathbb{N}\to -\left(A+1\right)!\in \mathbb{Z}$$
74		rpexpcl	$$⊢\left(2\in {ℝ}^{+}\wedge -\left(A+1\right)!\in \mathbb{Z}\right)\to 2^{-\left(A+1\right)!}\in {ℝ}^{+}$$
75	24 73 74	sylancr	$$⊢A\in \mathbb{N}\to 2^{-\left(A+1\right)!}\in {ℝ}^{+}$$
76		rpmulcl	$$⊢\left(2\in {ℝ}^{+}\wedge 2^{-\left(A+1\right)!}\in {ℝ}^{+}\right)\to 22^{-\left(A+1\right)!}\in {ℝ}^{+}$$
77	24 75 76	sylancr	$$⊢A\in \mathbb{N}\to 22^{-\left(A+1\right)!}\in {ℝ}^{+}$$
78	77	adantr	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to 22^{-\left(A+1\right)!}\in {ℝ}^{+}$$
79	78	rpred	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to 22^{-\left(A+1\right)!}\in ℝ$$
80	63 79	resubcld	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to H\left(A\right)-22^{-\left(A+1\right)!}\in ℝ$$
81	48	a1i	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to L\in ℝ$$
82	63 78	ltsubrpd	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to H\left(A\right)-22^{-\left(A+1\right)!}<H\left(A\right)$$
83	80 63 81 82 67	lttrd	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to H\left(A\right)-22^{-\left(A+1\right)!}<L$$
84	80 81 83	ltled	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to H\left(A\right)-22^{-\left(A+1\right)!}\le L$$
85		simprr	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to L-H\left(A\right)\le 22^{-\left(A+1\right)!}$$
86	81 63 79	lesubadd2d	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to \left(L-H\left(A\right)\le 22^{-\left(A+1\right)!}\leftrightarrow L\le H\left(A\right)+22^{-\left(A+1\right)!}\right)$$
87	85 86	mpbid	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to L\le H\left(A\right)+22^{-\left(A+1\right)!}$$
88	81 63 79	absdifled	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to \left(\left|L-H\left(A\right)\right|\le 22^{-\left(A+1\right)!}\leftrightarrow \left(H\left(A\right)-22^{-\left(A+1\right)!}\le L\wedge L\le H\left(A\right)+22^{-\left(A+1\right)!}\right)\right)$$
89	84 87 88	mpbir2and	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to \left|L-H\left(A\right)\right|\le 22^{-\left(A+1\right)!}$$
90	68 89	jca	$$⊢\left(A\in \mathbb{N}\wedge \left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\right)\to \left(H\left(A\right)\ne L\wedge \left|L-H\left(A\right)\right|\le 22^{-\left(A+1\right)!}\right)$$
91	90	ex	$$⊢A\in \mathbb{N}\to \left(\left(L-H\left(A\right)\in {ℝ}^{+}\wedge L-H\left(A\right)\le 22^{-\left(A+1\right)!}\right)\to \left(H\left(A\right)\ne L\wedge \left|L-H\left(A\right)\right|\le 22^{-\left(A+1\right)!}\right)\right)$$
92	62 91	sylbid	$$⊢A\in \mathbb{N}\to \left(\left(\sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\in {ℝ}^{+}\wedge \sum _{b\in {\mathbb{Z}}_{\ge \left(A+1\right)}}F\left(b\right)\le 22^{-\left(A+1\right)!}\right)\to \left(H\left(A\right)\ne L\wedge \left|L-H\left(A\right)\right|\le 22^{-\left(A+1\right)!}\right)\right)$$
93	8 92	mpd	$$⊢A\in \mathbb{N}\to \left(H\left(A\right)\ne L\wedge \left|L-H\left(A\right)\right|\le 22^{-\left(A+1\right)!}\right)$$