Theorem log2ublem2

Description: Lemma for log2ub . (Contributed by Mario Carneiro, 17-Apr-2015)

	Ref	Expression
Hypotheses	log2ublem2.1	$$⊢3^{7}5\cdot 7\sum _{n=0}^K\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le 2B$$
	log2ublem2.2	$$⊢B\in {\mathbb{N}}_0$$
	log2ublem2.3	$$⊢F\in {\mathbb{N}}_0$$
	log2ublem2.4	$$⊢N\in {\mathbb{N}}_0$$
	log2ublem2.5	$$⊢N-1=K$$
	log2ublem2.6	$$⊢B+F=G$$
	log2ublem2.7	$$⊢M\in {\mathbb{N}}_0$$
	log2ublem2.8	$$⊢M+N=3$$
	log2ublem2.9	$$⊢5\cdot 79^M=\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)F$$
Assertion	log2ublem2	$$⊢3^{7}5\cdot 7\sum _{n=0}^N\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le 2G$$

Proof

Step	Hyp	Ref	Expression
1		log2ublem2.1	$$⊢3^{7}5\cdot 7\sum _{n=0}^K\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le 2B$$
2		log2ublem2.2	$$⊢B\in {\mathbb{N}}_0$$
3		log2ublem2.3	$$⊢F\in {\mathbb{N}}_0$$
4		log2ublem2.4	$$⊢N\in {\mathbb{N}}_0$$
5		log2ublem2.5	$$⊢N-1=K$$
6		log2ublem2.6	$$⊢B+F=G$$
7		log2ublem2.7	$$⊢M\in {\mathbb{N}}_0$$
8		log2ublem2.8	$$⊢M+N=3$$
9		log2ublem2.9	$$⊢5\cdot 79^M=\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)F$$
10		fzfid	$$⊢\top \to \left(0\dots K\right)\in \mathrm{Fin}$$
11		elfznn0	$$⊢n\in \left(0\dots K\right)\to n\in {\mathbb{N}}_0$$
12	11	adantl	$$⊢\left(\top \wedge n\in \left(0\dots K\right)\right)\to n\in {\mathbb{N}}_0$$
13		2re	$$⊢2\in ℝ$$
14		3nn	$$⊢3\in \mathbb{N}$$
15		2nn0	$$⊢2\in {\mathbb{N}}_0$$
16		nn0mulcl	$$⊢\left(2\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to 2n\in {\mathbb{N}}_0$$
17	15 16	mpan	$$⊢n\in {\mathbb{N}}_0\to 2n\in {\mathbb{N}}_0$$
18		nn0p1nn	$$⊢2n\in {\mathbb{N}}_0\to 2n+1\in \mathbb{N}$$
19	17 18	syl	$$⊢n\in {\mathbb{N}}_0\to 2n+1\in \mathbb{N}$$
20		nnmulcl	$$⊢\left(3\in \mathbb{N}\wedge 2n+1\in \mathbb{N}\right)\to 3\left(2n+1\right)\in \mathbb{N}$$
21	14 19 20	sylancr	$$⊢n\in {\mathbb{N}}_0\to 3\left(2n+1\right)\in \mathbb{N}$$
22		9nn	$$⊢9\in \mathbb{N}$$
23		nnexpcl	$$⊢\left(9\in \mathbb{N}\wedge n\in {\mathbb{N}}_0\right)\to 9^n\in \mathbb{N}$$
24	22 23	mpan	$$⊢n\in {\mathbb{N}}_0\to 9^n\in \mathbb{N}$$
25	21 24	nnmulcld	$$⊢n\in {\mathbb{N}}_0\to 3\left(2n+1\right)9^n\in \mathbb{N}$$
26		nndivre	$$⊢\left(2\in ℝ\wedge 3\left(2n+1\right)9^n\in \mathbb{N}\right)\to \frac{2}{3\left(2n+1\right)9^n}\in ℝ$$
27	13 25 26	sylancr	$$⊢n\in {\mathbb{N}}_0\to \frac{2}{3\left(2n+1\right)9^n}\in ℝ$$
28	12 27	syl	$$⊢\left(\top \wedge n\in \left(0\dots K\right)\right)\to \frac{2}{3\left(2n+1\right)9^n}\in ℝ$$
29	10 28	fsumrecl	$$⊢\top \to \sum _{n=0}^K\left(\frac{2}{3\left(2n+1\right)9^n}\right)\in ℝ$$
30	29	mptru	$$⊢\sum _{n=0}^K\left(\frac{2}{3\left(2n+1\right)9^n}\right)\in ℝ$$
31	15 4	nn0mulcli	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0$$
32		nn0p1nn	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in \mathbb{N}$$
33	31 32	ax-mp	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in \mathbb{N}$$
34	14 33	nnmulcli	$$⊢3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\in \mathbb{N}$$
35		nnexpcl	$$⊢\left(9\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to 9^N\in \mathbb{N}$$
36	22 4 35	mp2an	$$⊢9^N\in \mathbb{N}$$
37	34 36	nnmulcli	$$⊢3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^N\in \mathbb{N}$$
38	15 2	nn0mulcli	$$⊢2B\in {\mathbb{N}}_0$$
39	15 3	nn0mulcli	$$⊢2F\in {\mathbb{N}}_0$$
40		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
41	4 40	eleqtri	$$⊢N\in {\mathbb{Z}}_{\ge 0}$$
42	41	a1i	$$⊢\top \to N\in {\mathbb{Z}}_{\ge 0}$$
43		elfznn0	$$⊢n\in \left(0\dots N\right)\to n\in {\mathbb{N}}_0$$
44	43	adantl	$$⊢\left(\top \wedge n\in \left(0\dots N\right)\right)\to n\in {\mathbb{N}}_0$$
45	27	recnd	$$⊢n\in {\mathbb{N}}_0\to \frac{2}{3\left(2n+1\right)9^n}\in ℂ$$
46	44 45	syl	$$⊢\left(\top \wedge n\in \left(0\dots N\right)\right)\to \frac{2}{3\left(2n+1\right)9^n}\in ℂ$$
47		oveq2	$$⊢n=N\to 2n=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
48	47	oveq1d	$$⊢n=N\to 2n+1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
49	48	oveq2d	$$⊢n=N\to 3\left(2n+1\right)=3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)$$
50		oveq2	$$⊢n=N\to 9^n=9^N$$
51	49 50	oveq12d	$$⊢n=N\to 3\left(2n+1\right)9^n=3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^N$$
52	51	oveq2d	$$⊢n=N\to \frac{2}{3\left(2n+1\right)9^n}=\frac{2}{3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^N}$$
53	42 46 52	fsumm1	$$⊢\top \to \sum _{n=0}^N\left(\frac{2}{3\left(2n+1\right)9^n}\right)=\sum _{n=0}^{N-1}\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{2}{3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^N}\right)$$
54	53	mptru	$$⊢\sum _{n=0}^N\left(\frac{2}{3\left(2n+1\right)9^n}\right)=\sum _{n=0}^{N-1}\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{2}{3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^N}\right)$$
55	5	oveq2i	$$⊢\left(0\dots N-1\right)=\left(0\dots K\right)$$
56	55	sumeq1i	$$⊢\sum _{n=0}^{N-1}\left(\frac{2}{3\left(2n+1\right)9^n}\right)=\sum _{n=0}^K\left(\frac{2}{3\left(2n+1\right)9^n}\right)$$
57	56	oveq1i	$$⊢\sum _{n=0}^{N-1}\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{2}{3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^N}\right)=\sum _{n=0}^K\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{2}{3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^N}\right)$$
58	54 57	eqtri	$$⊢\sum _{n=0}^N\left(\frac{2}{3\left(2n+1\right)9^n}\right)=\sum _{n=0}^K\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{2}{3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^N}\right)$$
59		2cn	$$⊢2\in ℂ$$
60	2	nn0cni	$$⊢B\in ℂ$$
61	3	nn0cni	$$⊢F\in ℂ$$
62	59 60 61	adddii	$$⊢2\left(B+F\right)=2B+2F$$
63	6	oveq2i	$$⊢2\left(B+F\right)=2G$$
64	62 63	eqtr3i	$$⊢2B+2F=2G$$
65		7nn	$$⊢7\in \mathbb{N}$$
66	65	nnnn0i	$$⊢7\in {\mathbb{N}}_0$$
67		nnexpcl	$$⊢\left(3\in \mathbb{N}\wedge 7\in {\mathbb{N}}_0\right)\to 3^7\in \mathbb{N}$$
68	14 66 67	mp2an	$$⊢3^7\in \mathbb{N}$$
69		5nn	$$⊢5\in \mathbb{N}$$
70	69 65	nnmulcli	$$⊢5\cdot 7\in \mathbb{N}$$
71	68 70	nnmulcli	$$⊢3^{7}5\cdot 7\in \mathbb{N}$$
72	71	nnrei	$$⊢3^{7}5\cdot 7\in ℝ$$
73	72 13	remulcli	$$⊢3^{7}5\cdot 7\cdot 2\in ℝ$$
74	73	leidi	$$⊢3^{7}5\cdot 7\cdot 2\le 3^{7}5\cdot 7\cdot 2$$
75	14	nnnn0i	$$⊢3\in {\mathbb{N}}_0$$
76		nnexpcl	$$⊢\left(9\in \mathbb{N}\wedge 3\in {\mathbb{N}}_0\right)\to 9^3\in \mathbb{N}$$
77	22 75 76	mp2an	$$⊢9^3\in \mathbb{N}$$
78	77	nncni	$$⊢9^3\in ℂ$$
79	70	nncni	$$⊢5\cdot 7\in ℂ$$
80	78 79	mulcomi	$$⊢9^{3}5\cdot 7=5\cdot 79^3$$
81	7	nn0cni	$$⊢M\in ℂ$$
82	4	nn0cni	$$⊢N\in ℂ$$
83	81 82	addcomi	$$⊢M+N=N+M$$
84	8 83	eqtr3i	$$⊢3=N+M$$
85	84	oveq2i	$$⊢9^3=9^{N+M}$$
86	22	nncni	$$⊢9\in ℂ$$
87		expadd	$$⊢\left(9\in ℂ\wedge N\in {\mathbb{N}}_0\wedge M\in {\mathbb{N}}_0\right)\to 9^{N+M}=9^N{9}^M$$
88	86 4 7 87	mp3an	$$⊢9^{N+M}=9^N{9}^M$$
89	85 88	eqtri	$$⊢9^3=9^N{9}^M$$
90	89	oveq2i	$$⊢5\cdot 79^3=5\cdot 79^N{9}^M$$
91	36	nncni	$$⊢9^N\in ℂ$$
92		nnexpcl	$$⊢\left(9\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 9^M\in \mathbb{N}$$
93	22 7 92	mp2an	$$⊢9^M\in \mathbb{N}$$
94	93	nncni	$$⊢9^M\in ℂ$$
95	79 91 94	mul12i	$$⊢5\cdot 79^N{9}^M=9^{N}5\cdot 79^M$$
96	80 90 95	3eqtri	$$⊢9^{3}5\cdot 7=9^{N}5\cdot 79^M$$
97	9	oveq2i	$$⊢9^{N}5\cdot 79^M=9^N\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)F$$
98	96 97	eqtri	$$⊢9^{3}5\cdot 7=9^N\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)F$$
99	98	oveq2i	$$⊢39^{3}5\cdot 7=39^N\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)F$$
100		df-7	$$⊢7=6+1$$
101	100	oveq2i	$$⊢3^7=3^{6+1}$$
102		3cn	$$⊢3\in ℂ$$
103		6nn0	$$⊢6\in {\mathbb{N}}_0$$
104		expp1	$$⊢\left(3\in ℂ\wedge 6\in {\mathbb{N}}_0\right)\to 3^{6+1}=3^6\cdot 3$$
105	102 103 104	mp2an	$$⊢3^{6+1}=3^6\cdot 3$$
106		expmul	$$⊢\left(3\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\to 3^{2\cdot 3}={\left(3^2\right)}^3$$
107	102 15 75 106	mp3an	$$⊢3^{2\cdot 3}={\left(3^2\right)}^3$$
108	59 102	mulcomi	$$⊢2\cdot 3=3\cdot 2$$
109		3t2e6	$$⊢3\cdot 2=6$$
110	108 109	eqtri	$$⊢2\cdot 3=6$$
111	110	oveq2i	$$⊢3^{2\cdot 3}=3^6$$
112		sq3	$$⊢3^2=9$$
113	112	oveq1i	$$⊢{\left(3^2\right)}^3=9^3$$
114	107 111 113	3eqtr3i	$$⊢3^6=9^3$$
115	114	oveq1i	$$⊢3^6\cdot 3=9^3\cdot 3$$
116	105 115	eqtri	$$⊢3^{6+1}=9^3\cdot 3$$
117	78 102	mulcomi	$$⊢9^3\cdot 3=39^3$$
118	101 116 117	3eqtri	$$⊢3^7=39^3$$
119	118	oveq1i	$$⊢3^{7}5\cdot 7=39^{3}5\cdot 7$$
120	102 78 79	mulassi	$$⊢39^{3}5\cdot 7=39^{3}5\cdot 7$$
121	119 120	eqtri	$$⊢3^{7}5\cdot 7=39^{3}5\cdot 7$$
122	33	nncni	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in ℂ$$
123	102 122 91	mul32i	$$⊢3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^N=39^N\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)$$
124	123	oveq1i	$$⊢3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^{N}F=39^N\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)F$$
125	102 91	mulcli	$$⊢39^N\in ℂ$$
126	125 122 61	mulassi	$$⊢39^N\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)F=39^N\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)F$$
127	122 61	mulcli	$$⊢\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)F\in ℂ$$
128	102 91 127	mulassi	$$⊢39^N\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)F=39^N\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)F$$
129	124 126 128	3eqtri	$$⊢3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^{N}F=39^N\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)F$$
130	99 121 129	3eqtr4i	$$⊢3^{7}5\cdot 7=3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^{N}F$$
131	130	oveq2i	$$⊢23^{7}5\cdot 7=23\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^{N}F$$
132	68	nncni	$$⊢3^7\in ℂ$$
133	132 79	mulcli	$$⊢3^{7}5\cdot 7\in ℂ$$
134	133 59	mulcomi	$$⊢3^{7}5\cdot 7\cdot 2=23^{7}5\cdot 7$$
135	37	nncni	$$⊢3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^N\in ℂ$$
136	135 59 61	mul12i	$$⊢3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^{N}2F=23\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^{N}F$$
137	131 134 136	3eqtr4i	$$⊢3^{7}5\cdot 7\cdot 2=3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^{N}2F$$
138	74 137	breqtri	$$⊢3^{7}5\cdot 7\cdot 2\le 3\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)9^{N}2F$$
139	1 30 15 37 38 39 58 64 138	log2ublem1	$$⊢3^{7}5\cdot 7\sum _{n=0}^N\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le 2G$$