Theorem bposlem8

Description: Lemma for bpos . Show that F ( 6 4 ) is less than log 2 . (Contributed by Mario Carneiro, 14-Mar-2014)

	Ref	Expression
Hypotheses	bposlem7.1	$$⊢F=\left(n\in \mathbb{N}⟼\sqrt{2}G\left(\sqrt{n}\right)+\left(\frac{9}{4}\right)G\left(\frac{n}{2}\right)+\left(\frac{\log 2}{\sqrt{2n}}\right)\right)$$
	bposlem7.2	$$⊢G=\left(x\in {ℝ}^{+}⟼\frac{\log x}{x}\right)$$
Assertion	bposlem8	$$⊢\left(F\left(64\right)\in ℝ\wedge F\left(64\right)<\log 2\right)$$

Proof

Step	Hyp	Ref	Expression
1		bposlem7.1	$$⊢F=\left(n\in \mathbb{N}⟼\sqrt{2}G\left(\sqrt{n}\right)+\left(\frac{9}{4}\right)G\left(\frac{n}{2}\right)+\left(\frac{\log 2}{\sqrt{2n}}\right)\right)$$
2		bposlem7.2	$$⊢G=\left(x\in {ℝ}^{+}⟼\frac{\log x}{x}\right)$$
3		6nn0	$$⊢6\in {\mathbb{N}}_0$$
4		4nn	$$⊢4\in \mathbb{N}$$
5	3 4	decnncl	$$⊢64\in \mathbb{N}$$
6		fveq2	$$⊢n=64\to \sqrt{n}=\sqrt{64}$$
7		8cn	$$⊢8\in ℂ$$
8	7	sqvali	$$⊢8^2=8\cdot 8$$
9		8t8e64	$$⊢8\cdot 8=64$$
10	8 9	eqtri	$$⊢8^2=64$$
11	10	fveq2i	$$⊢\sqrt{8^2}=\sqrt{64}$$
12		0re	$$⊢0\in ℝ$$
13		8re	$$⊢8\in ℝ$$
14		8pos	$$⊢0<8$$
15	12 13 14	ltleii	$$⊢0\le 8$$
16	13	sqrtsqi	$$⊢0\le 8\to \sqrt{8^2}=8$$
17	15 16	ax-mp	$$⊢\sqrt{8^2}=8$$
18	11 17	eqtr3i	$$⊢\sqrt{64}=8$$
19	6 18	eqtrdi	$$⊢n=64\to \sqrt{n}=8$$
20	19	fveq2d	$$⊢n=64\to G\left(\sqrt{n}\right)=G\left(8\right)$$
21		8nn	$$⊢8\in \mathbb{N}$$
22		nnrp	$$⊢8\in \mathbb{N}\to 8\in {ℝ}^{+}$$
23		fveq2	$$⊢x=8\to \log x=\log 8$$
24		cu2	$$⊢2^3=8$$
25	24	fveq2i	$$⊢\log 2^3=\log 8$$
26		2rp	$$⊢2\in {ℝ}^{+}$$
27		3z	$$⊢3\in \mathbb{Z}$$
28		relogexp	$$⊢\left(2\in {ℝ}^{+}\wedge 3\in \mathbb{Z}\right)\to \log 2^3=3\log 2$$
29	26 27 28	mp2an	$$⊢\log 2^3=3\log 2$$
30	25 29	eqtr3i	$$⊢\log 8=3\log 2$$
31	23 30	eqtrdi	$$⊢x=8\to \log x=3\log 2$$
32		id	$$⊢x=8\to x=8$$
33	31 32	oveq12d	$$⊢x=8\to \frac{\log x}{x}=\frac{3\log 2}{8}$$
34		3cn	$$⊢3\in ℂ$$
35		2nn	$$⊢2\in \mathbb{N}$$
36		nnrp	$$⊢2\in \mathbb{N}\to 2\in {ℝ}^{+}$$
37		relogcl	$$⊢2\in {ℝ}^{+}\to \log 2\in ℝ$$
38	35 36 37	mp2b	$$⊢\log 2\in ℝ$$
39	38	recni	$$⊢\log 2\in ℂ$$
40	21	nnne0i	$$⊢8\ne 0$$
41	34 39 7 40	div23i	$$⊢\frac{3\log 2}{8}=\left(\frac{3}{8}\right)\log 2$$
42	33 41	eqtrdi	$$⊢x=8\to \frac{\log x}{x}=\left(\frac{3}{8}\right)\log 2$$
43		ovex	$$⊢\left(\frac{3}{8}\right)\log 2\in \mathrm{V}$$
44	42 2 43	fvmpt	$$⊢8\in {ℝ}^{+}\to G\left(8\right)=\left(\frac{3}{8}\right)\log 2$$
45	21 22 44	mp2b	$$⊢G\left(8\right)=\left(\frac{3}{8}\right)\log 2$$
46	20 45	eqtrdi	$$⊢n=64\to G\left(\sqrt{n}\right)=\left(\frac{3}{8}\right)\log 2$$
47	46	oveq2d	$$⊢n=64\to \sqrt{2}G\left(\sqrt{n}\right)=\sqrt{2}\left(\frac{3}{8}\right)\log 2$$
48		sqrt2re	$$⊢\sqrt{2}\in ℝ$$
49	48	recni	$$⊢\sqrt{2}\in ℂ$$
50	34 7 40	divcli	$$⊢\frac{3}{8}\in ℂ$$
51	49 50 39	mulassi	$$⊢\sqrt{2}\left(\frac{3}{8}\right)\log 2=\sqrt{2}\left(\frac{3}{8}\right)\log 2$$
52		4cn	$$⊢4\in ℂ$$
53	49 52 49	mul12i	$$⊢\sqrt{2}4\sqrt{2}=4\sqrt{2}\sqrt{2}$$
54		2re	$$⊢2\in ℝ$$
55		0le2	$$⊢0\le 2$$
56		remsqsqrt	$$⊢\left(2\in ℝ\wedge 0\le 2\right)\to \sqrt{2}\sqrt{2}=2$$
57	54 55 56	mp2an	$$⊢\sqrt{2}\sqrt{2}=2$$
58	57	oveq2i	$$⊢4\sqrt{2}\sqrt{2}=4\cdot 2$$
59		4t2e8	$$⊢4\cdot 2=8$$
60	53 58 59	3eqtri	$$⊢\sqrt{2}4\sqrt{2}=8$$
61	60	oveq2i	$$⊢\frac{\sqrt{2}\cdot 3}{\sqrt{2}4\sqrt{2}}=\frac{\sqrt{2}\cdot 3}{8}$$
62	52 49	mulcli	$$⊢4\sqrt{2}\in ℂ$$
63		nnrp	$$⊢4\in \mathbb{N}\to 4\in {ℝ}^{+}$$
64	4 63	ax-mp	$$⊢4\in {ℝ}^{+}$$
65		rpsqrtcl	$$⊢2\in {ℝ}^{+}\to \sqrt{2}\in {ℝ}^{+}$$
66	35 36 65	mp2b	$$⊢\sqrt{2}\in {ℝ}^{+}$$
67		rpmulcl	$$⊢\left(4\in {ℝ}^{+}\wedge \sqrt{2}\in {ℝ}^{+}\right)\to 4\sqrt{2}\in {ℝ}^{+}$$
68	64 66 67	mp2an	$$⊢4\sqrt{2}\in {ℝ}^{+}$$
69		rpne0	$$⊢4\sqrt{2}\in {ℝ}^{+}\to 4\sqrt{2}\ne 0$$
70	68 69	ax-mp	$$⊢4\sqrt{2}\ne 0$$
71		rpne0	$$⊢\sqrt{2}\in {ℝ}^{+}\to \sqrt{2}\ne 0$$
72	26 65 71	mp2b	$$⊢\sqrt{2}\ne 0$$
73		divcan5	$$⊢\left(3\in ℂ\wedge \left(4\sqrt{2}\in ℂ\wedge 4\sqrt{2}\ne 0\right)\wedge \left(\sqrt{2}\in ℂ\wedge \sqrt{2}\ne 0\right)\right)\to \frac{\sqrt{2}\cdot 3}{\sqrt{2}4\sqrt{2}}=\frac{3}{4\sqrt{2}}$$
74	34 73	mp3an1	$$⊢\left(\left(4\sqrt{2}\in ℂ\wedge 4\sqrt{2}\ne 0\right)\wedge \left(\sqrt{2}\in ℂ\wedge \sqrt{2}\ne 0\right)\right)\to \frac{\sqrt{2}\cdot 3}{\sqrt{2}4\sqrt{2}}=\frac{3}{4\sqrt{2}}$$
75	62 70 49 72 74	mp4an	$$⊢\frac{\sqrt{2}\cdot 3}{\sqrt{2}4\sqrt{2}}=\frac{3}{4\sqrt{2}}$$
76		4ne0	$$⊢4\ne 0$$
77		divdiv1	$$⊢\left(3\in ℂ\wedge \left(4\in ℂ\wedge 4\ne 0\right)\wedge \left(\sqrt{2}\in ℂ\wedge \sqrt{2}\ne 0\right)\right)\to \frac{\frac{3}{4}}{\sqrt{2}}=\frac{3}{4\sqrt{2}}$$
78	34 77	mp3an1	$$⊢\left(\left(4\in ℂ\wedge 4\ne 0\right)\wedge \left(\sqrt{2}\in ℂ\wedge \sqrt{2}\ne 0\right)\right)\to \frac{\frac{3}{4}}{\sqrt{2}}=\frac{3}{4\sqrt{2}}$$
79	52 76 49 72 78	mp4an	$$⊢\frac{\frac{3}{4}}{\sqrt{2}}=\frac{3}{4\sqrt{2}}$$
80	75 79	eqtr4i	$$⊢\frac{\sqrt{2}\cdot 3}{\sqrt{2}4\sqrt{2}}=\frac{\frac{3}{4}}{\sqrt{2}}$$
81	49 34 7 40	divassi	$$⊢\frac{\sqrt{2}\cdot 3}{8}=\sqrt{2}\left(\frac{3}{8}\right)$$
82	61 80 81	3eqtr3ri	$$⊢\sqrt{2}\left(\frac{3}{8}\right)=\frac{\frac{3}{4}}{\sqrt{2}}$$
83	82	oveq1i	$$⊢\sqrt{2}\left(\frac{3}{8}\right)\log 2=\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)\log 2$$
84	51 83	eqtr3i	$$⊢\sqrt{2}\left(\frac{3}{8}\right)\log 2=\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)\log 2$$
85	47 84	eqtrdi	$$⊢n=64\to \sqrt{2}G\left(\sqrt{n}\right)=\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)\log 2$$
86		oveq1	$$⊢n=64\to \frac{n}{2}=\frac{64}{2}$$
87		df-6	$$⊢6=5+1$$
88	87	oveq2i	$$⊢2^6=2^{5+1}$$
89		2exp6	$$⊢2^6=64$$
90		2cn	$$⊢2\in ℂ$$
91		5nn0	$$⊢5\in {\mathbb{N}}_0$$
92		expp1	$$⊢\left(2\in ℂ\wedge 5\in {\mathbb{N}}_0\right)\to 2^{5+1}=2^5\cdot 2$$
93	90 91 92	mp2an	$$⊢2^{5+1}=2^5\cdot 2$$
94	88 89 93	3eqtr3i	$$⊢64=2^5\cdot 2$$
95	94	oveq1i	$$⊢\frac{64}{2}=\frac{2^5\cdot 2}{2}$$
96		nnexpcl	$$⊢\left(2\in \mathbb{N}\wedge 5\in {\mathbb{N}}_0\right)\to 2^5\in \mathbb{N}$$
97	35 91 96	mp2an	$$⊢2^5\in \mathbb{N}$$
98	97	nncni	$$⊢2^5\in ℂ$$
99		2ne0	$$⊢2\ne 0$$
100	98 90 99	divcan4i	$$⊢\frac{2^5\cdot 2}{2}=2^5$$
101	95 100	eqtri	$$⊢\frac{64}{2}=2^5$$
102	86 101	eqtrdi	$$⊢n=64\to \frac{n}{2}=2^5$$
103	102	fveq2d	$$⊢n=64\to G\left(\frac{n}{2}\right)=G\left(2^5\right)$$
104		nnrp	$$⊢2^5\in \mathbb{N}\to 2^5\in {ℝ}^{+}$$
105		fveq2	$$⊢x=2^5\to \log x=\log 2^5$$
106		5nn	$$⊢5\in \mathbb{N}$$
107	106	nnzi	$$⊢5\in \mathbb{Z}$$
108		relogexp	$$⊢\left(2\in {ℝ}^{+}\wedge 5\in \mathbb{Z}\right)\to \log 2^5=5\log 2$$
109	26 107 108	mp2an	$$⊢\log 2^5=5\log 2$$
110	105 109	eqtrdi	$$⊢x=2^5\to \log x=5\log 2$$
111		id	$$⊢x=2^5\to x=2^5$$
112	110 111	oveq12d	$$⊢x=2^5\to \frac{\log x}{x}=\frac{5\log 2}{2^5}$$
113		5cn	$$⊢5\in ℂ$$
114	97	nnne0i	$$⊢2^5\ne 0$$
115	113 39 98 114	div23i	$$⊢\frac{5\log 2}{2^5}=\left(\frac{5}{2^5}\right)\log 2$$
116	112 115	eqtrdi	$$⊢x=2^5\to \frac{\log x}{x}=\left(\frac{5}{2^5}\right)\log 2$$
117		ovex	$$⊢\left(\frac{5}{2^5}\right)\log 2\in \mathrm{V}$$
118	116 2 117	fvmpt	$$⊢2^5\in {ℝ}^{+}\to G\left(2^5\right)=\left(\frac{5}{2^5}\right)\log 2$$
119	97 104 118	mp2b	$$⊢G\left(2^5\right)=\left(\frac{5}{2^5}\right)\log 2$$
120	103 119	eqtrdi	$$⊢n=64\to G\left(\frac{n}{2}\right)=\left(\frac{5}{2^5}\right)\log 2$$
121	120	oveq2d	$$⊢n=64\to \left(\frac{9}{4}\right)G\left(\frac{n}{2}\right)=\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\log 2$$
122		9cn	$$⊢9\in ℂ$$
123	122 52 76	divcli	$$⊢\frac{9}{4}\in ℂ$$
124	113 98 114	divcli	$$⊢\frac{5}{2^5}\in ℂ$$
125	123 124 39	mulassi	$$⊢\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\log 2=\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\log 2$$
126	121 125	eqtr4di	$$⊢n=64\to \left(\frac{9}{4}\right)G\left(\frac{n}{2}\right)=\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\log 2$$
127	85 126	oveq12d	$$⊢n=64\to \sqrt{2}G\left(\sqrt{n}\right)+\left(\frac{9}{4}\right)G\left(\frac{n}{2}\right)=\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)\log 2+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\log 2$$
128	34 52 76	divcli	$$⊢\frac{3}{4}\in ℂ$$
129	128 49 72	divcli	$$⊢\frac{\frac{3}{4}}{\sqrt{2}}\in ℂ$$
130	123 124	mulcli	$$⊢\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\in ℂ$$
131	129 130 39	adddiri	$$⊢\left(\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\right)\log 2=\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)\log 2+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\log 2$$
132	127 131	eqtr4di	$$⊢n=64\to \sqrt{2}G\left(\sqrt{n}\right)+\left(\frac{9}{4}\right)G\left(\frac{n}{2}\right)=\left(\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\right)\log 2$$
133		oveq2	$$⊢n=64\to 2n=2\cdot 64$$
134	133	fveq2d	$$⊢n=64\to \sqrt{2n}=\sqrt{2\cdot 64}$$
135	5	nnrei	$$⊢64\in ℝ$$
136	5	nngt0i	$$⊢0<64$$
137	12 135 136	ltleii	$$⊢0\le 64$$
138	54 135 55 137	sqrtmulii	$$⊢\sqrt{2\cdot 64}=\sqrt{2}\sqrt{64}$$
139	18	oveq2i	$$⊢\sqrt{2}\sqrt{64}=\sqrt{2}\cdot 8$$
140	138 139	eqtri	$$⊢\sqrt{2\cdot 64}=\sqrt{2}\cdot 8$$
141	134 140	eqtrdi	$$⊢n=64\to \sqrt{2n}=\sqrt{2}\cdot 8$$
142	141	oveq2d	$$⊢n=64\to \frac{\log 2}{\sqrt{2n}}=\frac{\log 2}{\sqrt{2}\cdot 8}$$
143	49 7	mulcli	$$⊢\sqrt{2}\cdot 8\in ℂ$$
144		rpmulcl	$$⊢\left(\sqrt{2}\in {ℝ}^{+}\wedge 8\in {ℝ}^{+}\right)\to \sqrt{2}\cdot 8\in {ℝ}^{+}$$
145	66 22 144	sylancr	$$⊢8\in \mathbb{N}\to \sqrt{2}\cdot 8\in {ℝ}^{+}$$
146		rpne0	$$⊢\sqrt{2}\cdot 8\in {ℝ}^{+}\to \sqrt{2}\cdot 8\ne 0$$
147	21 145 146	mp2b	$$⊢\sqrt{2}\cdot 8\ne 0$$
148		divrec2	$$⊢\left(\log 2\in ℂ\wedge \sqrt{2}\cdot 8\in ℂ\wedge \sqrt{2}\cdot 8\ne 0\right)\to \frac{\log 2}{\sqrt{2}\cdot 8}=\left(\frac{1}{\sqrt{2}\cdot 8}\right)\log 2$$
149	39 143 147 148	mp3an	$$⊢\frac{\log 2}{\sqrt{2}\cdot 8}=\left(\frac{1}{\sqrt{2}\cdot 8}\right)\log 2$$
150	49 7	mulcomi	$$⊢\sqrt{2}\cdot 8=8\sqrt{2}$$
151	150	oveq2i	$$⊢\frac{1}{\sqrt{2}\cdot 8}=\frac{1}{8\sqrt{2}}$$
152		recdiv2	$$⊢\left(\left(8\in ℂ\wedge 8\ne 0\right)\wedge \left(\sqrt{2}\in ℂ\wedge \sqrt{2}\ne 0\right)\right)\to \frac{\frac{1}{8}}{\sqrt{2}}=\frac{1}{8\sqrt{2}}$$
153	7 40 49 72 152	mp4an	$$⊢\frac{\frac{1}{8}}{\sqrt{2}}=\frac{1}{8\sqrt{2}}$$
154	151 153	eqtr4i	$$⊢\frac{1}{\sqrt{2}\cdot 8}=\frac{\frac{1}{8}}{\sqrt{2}}$$
155	154	oveq1i	$$⊢\left(\frac{1}{\sqrt{2}\cdot 8}\right)\log 2=\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)\log 2$$
156	149 155	eqtri	$$⊢\frac{\log 2}{\sqrt{2}\cdot 8}=\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)\log 2$$
157	142 156	eqtrdi	$$⊢n=64\to \frac{\log 2}{\sqrt{2n}}=\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)\log 2$$
158	132 157	oveq12d	$$⊢n=64\to \sqrt{2}G\left(\sqrt{n}\right)+\left(\frac{9}{4}\right)G\left(\frac{n}{2}\right)+\left(\frac{\log 2}{\sqrt{2n}}\right)=\left(\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\right)\log 2+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)\log 2$$
159	129 130	addcli	$$⊢\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\in ℂ$$
160	7 40	reccli	$$⊢\frac{1}{8}\in ℂ$$
161	160 49 72	divcli	$$⊢\frac{\frac{1}{8}}{\sqrt{2}}\in ℂ$$
162	159 161 39	adddiri	$$⊢\left(\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)\right)\log 2=\left(\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\right)\log 2+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)\log 2$$
163	158 162	eqtr4di	$$⊢n=64\to \sqrt{2}G\left(\sqrt{n}\right)+\left(\frac{9}{4}\right)G\left(\frac{n}{2}\right)+\left(\frac{\log 2}{\sqrt{2n}}\right)=\left(\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)\right)\log 2$$
164		ovex	$$⊢\left(\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)\right)\log 2\in \mathrm{V}$$
165	163 1 164	fvmpt	$$⊢64\in \mathbb{N}\to F\left(64\right)=\left(\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)\right)\log 2$$
166	5 165	ax-mp	$$⊢F\left(64\right)=\left(\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)\right)\log 2$$
167		3re	$$⊢3\in ℝ$$
168		4re	$$⊢4\in ℝ$$
169	167 168 76	redivcli	$$⊢\frac{3}{4}\in ℝ$$
170	169 48 72	redivcli	$$⊢\frac{\frac{3}{4}}{\sqrt{2}}\in ℝ$$
171		9re	$$⊢9\in ℝ$$
172	171 168 76	redivcli	$$⊢\frac{9}{4}\in ℝ$$
173		5re	$$⊢5\in ℝ$$
174	97	nnrei	$$⊢2^5\in ℝ$$
175	173 174 114	redivcli	$$⊢\frac{5}{2^5}\in ℝ$$
176	172 175	remulcli	$$⊢\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\in ℝ$$
177	170 176	readdcli	$$⊢\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\in ℝ$$
178	13 40	rereccli	$$⊢\frac{1}{8}\in ℝ$$
179	178 48 72	redivcli	$$⊢\frac{\frac{1}{8}}{\sqrt{2}}\in ℝ$$
180	177 179	readdcli	$$⊢\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)\in ℝ$$
181	180 38	remulcli	$$⊢\left(\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)\right)\log 2\in ℝ$$
182	166 181	eqeltri	$$⊢F\left(64\right)\in ℝ$$
183	129 130 161	add32i	$$⊢\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)=\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)$$
184		6cn	$$⊢6\in ℂ$$
185		ax-1cn	$$⊢1\in ℂ$$
186	184 185 7 40	divdiri	$$⊢\frac{6+1}{8}=\left(\frac{6}{8}\right)+\left(\frac{1}{8}\right)$$
187		df-7	$$⊢7=6+1$$
188	187	oveq1i	$$⊢\frac{7}{8}=\frac{6+1}{8}$$
189		divcan5	$$⊢\left(3\in ℂ\wedge \left(4\in ℂ\wedge 4\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{2\cdot 3}{2\cdot 4}=\frac{3}{4}$$
190	34 189	mp3an1	$$⊢\left(\left(4\in ℂ\wedge 4\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{2\cdot 3}{2\cdot 4}=\frac{3}{4}$$
191	52 76 90 99 190	mp4an	$$⊢\frac{2\cdot 3}{2\cdot 4}=\frac{3}{4}$$
192		2t3e6	$$⊢2\cdot 3=6$$
193		2t4e8	$$⊢2\cdot 4=8$$
194	192 193	oveq12i	$$⊢\frac{2\cdot 3}{2\cdot 4}=\frac{6}{8}$$
195	191 194	eqtr3i	$$⊢\frac{3}{4}=\frac{6}{8}$$
196	195	oveq1i	$$⊢\left(\frac{3}{4}\right)+\left(\frac{1}{8}\right)=\left(\frac{6}{8}\right)+\left(\frac{1}{8}\right)$$
197	186 188 196	3eqtr4ri	$$⊢\left(\frac{3}{4}\right)+\left(\frac{1}{8}\right)=\frac{7}{8}$$
198	197	oveq1i	$$⊢\frac{\left(\frac{3}{4}\right)+\left(\frac{1}{8}\right)}{\sqrt{2}}=\frac{\frac{7}{8}}{\sqrt{2}}$$
199	128 160 49 72	divdiri	$$⊢\frac{\left(\frac{3}{4}\right)+\left(\frac{1}{8}\right)}{\sqrt{2}}=\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)$$
200		7cn	$$⊢7\in ℂ$$
201	200 7 49 40 72	divdiv32i	$$⊢\frac{\frac{7}{8}}{\sqrt{2}}=\frac{\frac{7}{\sqrt{2}}}{8}$$
202	198 199 201	3eqtr3i	$$⊢\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)=\frac{\frac{7}{\sqrt{2}}}{8}$$
203	202	oveq1i	$$⊢\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)=\left(\frac{\frac{7}{\sqrt{2}}}{8}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)$$
204	183 203	eqtri	$$⊢\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)=\left(\frac{\frac{7}{\sqrt{2}}}{8}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)$$
205		4nn0	$$⊢4\in {\mathbb{N}}_0$$
206		9nn0	$$⊢9\in {\mathbb{N}}_0$$
207		0nn0	$$⊢0\in {\mathbb{N}}_0$$
208		9lt10	$$⊢9<10$$
209		4lt5	$$⊢4<5$$
210	205 91 206 207 208 209	decltc	$$⊢49<50$$
211		7t7e49	$$⊢7\cdot 7=49$$
212	57	oveq1i	$$⊢\sqrt{2}\sqrt{2}5\cdot 5=25\cdot 5$$
213	49 49 113 113	mul4i	$$⊢\sqrt{2}\sqrt{2}5\cdot 5=\sqrt{2}\cdot 5\sqrt{2}\cdot 5$$
214		5t2e10	$$⊢5\cdot 2=10$$
215	113 90 214	mulcomli	$$⊢2\cdot 5=10$$
216	215	oveq1i	$$⊢2\cdot 5\cdot 5=10\cdot 5$$
217	90 113 113	mulassi	$$⊢2\cdot 5\cdot 5=25\cdot 5$$
218	91	dec0u	$$⊢10\cdot 5=50$$
219	216 217 218	3eqtr3i	$$⊢25\cdot 5=50$$
220	212 213 219	3eqtr3i	$$⊢\sqrt{2}\cdot 5\sqrt{2}\cdot 5=50$$
221	210 211 220	3brtr4i	$$⊢7\cdot 7<\sqrt{2}\cdot 5\sqrt{2}\cdot 5$$
222		7re	$$⊢7\in ℝ$$
223		7pos	$$⊢0<7$$
224	12 222 223	ltleii	$$⊢0\le 7$$
225		nnrp	$$⊢5\in \mathbb{N}\to 5\in {ℝ}^{+}$$
226	106 225	ax-mp	$$⊢5\in {ℝ}^{+}$$
227		rpmulcl	$$⊢\left(\sqrt{2}\in {ℝ}^{+}\wedge 5\in {ℝ}^{+}\right)\to \sqrt{2}\cdot 5\in {ℝ}^{+}$$
228	66 226 227	mp2an	$$⊢\sqrt{2}\cdot 5\in {ℝ}^{+}$$
229		rpge0	$$⊢\sqrt{2}\cdot 5\in {ℝ}^{+}\to 0\le \sqrt{2}\cdot 5$$
230	228 229	ax-mp	$$⊢0\le \sqrt{2}\cdot 5$$
231		rpre	$$⊢\sqrt{2}\cdot 5\in {ℝ}^{+}\to \sqrt{2}\cdot 5\in ℝ$$
232	228 231	ax-mp	$$⊢\sqrt{2}\cdot 5\in ℝ$$
233	222 232	lt2msqi	$$⊢\left(0\le 7\wedge 0\le \sqrt{2}\cdot 5\right)\to \left(7<\sqrt{2}\cdot 5\leftrightarrow 7\cdot 7<\sqrt{2}\cdot 5\sqrt{2}\cdot 5\right)$$
234	224 230 233	mp2an	$$⊢7<\sqrt{2}\cdot 5\leftrightarrow 7\cdot 7<\sqrt{2}\cdot 5\sqrt{2}\cdot 5$$
235	221 234	mpbir	$$⊢7<\sqrt{2}\cdot 5$$
236		rpgt0	$$⊢\sqrt{2}\in {ℝ}^{+}\to 0<\sqrt{2}$$
237	26 65 236	mp2b	$$⊢0<\sqrt{2}$$
238		ltdivmul	$$⊢\left(7\in ℝ\wedge 5\in ℝ\wedge \left(\sqrt{2}\in ℝ\wedge 0<\sqrt{2}\right)\right)\to \left(\frac{7}{\sqrt{2}}<5\leftrightarrow 7<\sqrt{2}\cdot 5\right)$$
239	222 173 238	mp3an12	$$⊢\left(\sqrt{2}\in ℝ\wedge 0<\sqrt{2}\right)\to \left(\frac{7}{\sqrt{2}}<5\leftrightarrow 7<\sqrt{2}\cdot 5\right)$$
240	48 237 239	mp2an	$$⊢\frac{7}{\sqrt{2}}<5\leftrightarrow 7<\sqrt{2}\cdot 5$$
241	235 240	mpbir	$$⊢\frac{7}{\sqrt{2}}<5$$
242	222 48 72	redivcli	$$⊢\frac{7}{\sqrt{2}}\in ℝ$$
243	242 173 13 14	ltdiv1ii	$$⊢\frac{7}{\sqrt{2}}<5\leftrightarrow \frac{\frac{7}{\sqrt{2}}}{8}<\frac{5}{8}$$
244	241 243	mpbi	$$⊢\frac{\frac{7}{\sqrt{2}}}{8}<\frac{5}{8}$$
245		divsubdir	$$⊢\left(8\in ℂ\wedge 3\in ℂ\wedge \left(8\in ℂ\wedge 8\ne 0\right)\right)\to \frac{8-3}{8}=\left(\frac{8}{8}\right)-\left(\frac{3}{8}\right)$$
246	7 34 245	mp3an12	$$⊢\left(8\in ℂ\wedge 8\ne 0\right)\to \frac{8-3}{8}=\left(\frac{8}{8}\right)-\left(\frac{3}{8}\right)$$
247	7 40 246	mp2an	$$⊢\frac{8-3}{8}=\left(\frac{8}{8}\right)-\left(\frac{3}{8}\right)$$
248		5p3e8	$$⊢5+3=8$$
249	248	oveq1i	$$⊢5+3-3=8-3$$
250	113 34	pncan3oi	$$⊢5+3-3=5$$
251	249 250	eqtr3i	$$⊢8-3=5$$
252	251	oveq1i	$$⊢\frac{8-3}{8}=\frac{5}{8}$$
253	7 40	dividi	$$⊢\frac{8}{8}=1$$
254	253	oveq1i	$$⊢\left(\frac{8}{8}\right)-\left(\frac{3}{8}\right)=1-\left(\frac{3}{8}\right)$$
255	247 252 254	3eqtr3ri	$$⊢1-\left(\frac{3}{8}\right)=\frac{5}{8}$$
256		5lt8	$$⊢5<8$$
257	13 173	remulcli	$$⊢8\cdot 5\in ℝ$$
258	173 13 257	ltadd2i	$$⊢5<8\leftrightarrow 8\cdot 5+5<8\cdot 5+8$$
259	256 258	mpbi	$$⊢8\cdot 5+5<8\cdot 5+8$$
260		df-9	$$⊢9=8+1$$
261	260	oveq1i	$$⊢9\cdot 5=\left(8+1\right)\cdot 5$$
262	7 185 113	adddiri	$$⊢\left(8+1\right)\cdot 5=8\cdot 5+1\cdot 5$$
263	113	mullidi	$$⊢1\cdot 5=5$$
264	263	oveq2i	$$⊢8\cdot 5+1\cdot 5=8\cdot 5+5$$
265	261 262 264	3eqtri	$$⊢9\cdot 5=8\cdot 5+5$$
266	87	oveq2i	$$⊢8\cdot 6=8\left(5+1\right)$$
267	7 113 185	adddii	$$⊢8\left(5+1\right)=8\cdot 5+8\cdot 1$$
268	7	mulridi	$$⊢8\cdot 1=8$$
269	268	oveq2i	$$⊢8\cdot 5+8\cdot 1=8\cdot 5+8$$
270	266 267 269	3eqtri	$$⊢8\cdot 6=8\cdot 5+8$$
271	259 265 270	3brtr4i	$$⊢9\cdot 5<8\cdot 6$$
272	171 173	remulcli	$$⊢9\cdot 5\in ℝ$$
273		6re	$$⊢6\in ℝ$$
274	13 273	remulcli	$$⊢8\cdot 6\in ℝ$$
275	168 174	remulcli	$$⊢42^5\in ℝ$$
276	4 97	nnmulcli	$$⊢42^5\in \mathbb{N}$$
277	276	nngt0i	$$⊢0<42^5$$
278	272 274 275 277	ltdiv1ii	$$⊢9\cdot 5<8\cdot 6\leftrightarrow \frac{9\cdot 5}{42^5}<\frac{8\cdot 6}{42^5}$$
279	271 278	mpbi	$$⊢\frac{9\cdot 5}{42^5}<\frac{8\cdot 6}{42^5}$$
280	122 52 113 98 76 114	divmuldivi	$$⊢\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)=\frac{9\cdot 5}{42^5}$$
281		nnexpcl	$$⊢\left(2\in \mathbb{N}\wedge 4\in {\mathbb{N}}_0\right)\to 2^4\in \mathbb{N}$$
282	35 205 281	mp2an	$$⊢2^4\in \mathbb{N}$$
283	282	nncni	$$⊢2^4\in ℂ$$
284	282	nnne0i	$$⊢2^4\ne 0$$
285		divcan5	$$⊢\left(3\in ℂ\wedge \left(8\in ℂ\wedge 8\ne 0\right)\wedge \left(2^4\in ℂ\wedge 2^4\ne 0\right)\right)\to \frac{2^4\cdot 3}{2^4\cdot 8}=\frac{3}{8}$$
286	34 285	mp3an1	$$⊢\left(\left(8\in ℂ\wedge 8\ne 0\right)\wedge \left(2^4\in ℂ\wedge 2^4\ne 0\right)\right)\to \frac{2^4\cdot 3}{2^4\cdot 8}=\frac{3}{8}$$
287	7 40 283 284 286	mp4an	$$⊢\frac{2^4\cdot 3}{2^4\cdot 8}=\frac{3}{8}$$
288		df-4	$$⊢4=3+1$$
289	288	oveq2i	$$⊢2^4=2^{3+1}$$
290		3nn0	$$⊢3\in {\mathbb{N}}_0$$
291		expp1	$$⊢\left(2\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to 2^{3+1}=2^3\cdot 2$$
292	90 290 291	mp2an	$$⊢2^{3+1}=2^3\cdot 2$$
293	24	oveq1i	$$⊢2^3\cdot 2=8\cdot 2$$
294	289 292 293	3eqtri	$$⊢2^4=8\cdot 2$$
295	294	oveq1i	$$⊢2^4\cdot 3=8\cdot 2\cdot 3$$
296	7 90 34	mulassi	$$⊢8\cdot 2\cdot 3=82\cdot 3$$
297	192	oveq2i	$$⊢82\cdot 3=8\cdot 6$$
298	295 296 297	3eqtri	$$⊢2^4\cdot 3=8\cdot 6$$
299		4p3e7	$$⊢4+3=7$$
300		5p2e7	$$⊢5+2=7$$
301	113 90	addcomi	$$⊢5+2=2+5$$
302	299 300 301	3eqtr2i	$$⊢4+3=2+5$$
303	302	oveq2i	$$⊢2^{4+3}=2^{2+5}$$
304		expadd	$$⊢\left(2\in ℂ\wedge 4\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\to 2^{4+3}=2^4{2}^3$$
305	90 205 290 304	mp3an	$$⊢2^{4+3}=2^4{2}^3$$
306		2nn0	$$⊢2\in {\mathbb{N}}_0$$
307		expadd	$$⊢\left(2\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\to 2^{2+5}=2^2{2}^5$$
308	90 306 91 307	mp3an	$$⊢2^{2+5}=2^2{2}^5$$
309	303 305 308	3eqtr3i	$$⊢2^4{2}^3=2^2{2}^5$$
310	24	oveq2i	$$⊢2^4{2}^3=2^4\cdot 8$$
311		sq2	$$⊢2^2=4$$
312	311	oveq1i	$$⊢2^2{2}^5=42^5$$
313	309 310 312	3eqtr3i	$$⊢2^4\cdot 8=42^5$$
314	298 313	oveq12i	$$⊢\frac{2^4\cdot 3}{2^4\cdot 8}=\frac{8\cdot 6}{42^5}$$
315	287 314	eqtr3i	$$⊢\frac{3}{8}=\frac{8\cdot 6}{42^5}$$
316	279 280 315	3brtr4i	$$⊢\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)<\frac{3}{8}$$
317	167 13 40	redivcli	$$⊢\frac{3}{8}\in ℝ$$
318		1re	$$⊢1\in ℝ$$
319		ltsub2	$$⊢\left(\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\in ℝ\wedge \frac{3}{8}\in ℝ\wedge 1\in ℝ\right)\to \left(\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)<\frac{3}{8}\leftrightarrow 1-\left(\frac{3}{8}\right)<1-\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\right)$$
320	176 317 318 319	mp3an	$$⊢\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)<\frac{3}{8}\leftrightarrow 1-\left(\frac{3}{8}\right)<1-\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)$$
321	316 320	mpbi	$$⊢1-\left(\frac{3}{8}\right)<1-\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)$$
322	255 321	eqbrtrri	$$⊢\frac{5}{8}<1-\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)$$
323	242 13 40	redivcli	$$⊢\frac{\frac{7}{\sqrt{2}}}{8}\in ℝ$$
324	173 13 40	redivcli	$$⊢\frac{5}{8}\in ℝ$$
325	318 176	resubcli	$$⊢1-\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\in ℝ$$
326	323 324 325	lttri	$$⊢\left(\frac{\frac{7}{\sqrt{2}}}{8}<\frac{5}{8}\wedge \frac{5}{8}<1-\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\right)\to \frac{\frac{7}{\sqrt{2}}}{8}<1-\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)$$
327	244 322 326	mp2an	$$⊢\frac{\frac{7}{\sqrt{2}}}{8}<1-\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)$$
328	323 176 318	ltaddsubi	$$⊢\left(\frac{\frac{7}{\sqrt{2}}}{8}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)<1\leftrightarrow \frac{\frac{7}{\sqrt{2}}}{8}<1-\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)$$
329	327 328	mpbir	$$⊢\left(\frac{\frac{7}{\sqrt{2}}}{8}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)<1$$
330	204 329	eqbrtri	$$⊢\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)<1$$
331		1lt2	$$⊢1<2$$
332		rplogcl	$$⊢\left(2\in ℝ\wedge 1<2\right)\to \log 2\in {ℝ}^{+}$$
333	54 331 332	mp2an	$$⊢\log 2\in {ℝ}^{+}$$
334		rpgt0	$$⊢\log 2\in {ℝ}^{+}\to 0<\log 2$$
335	333 334	ax-mp	$$⊢0<\log 2$$
336	180 318 38 335	ltmul1ii	$$⊢\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)<1\leftrightarrow \left(\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)\right)\log 2<1\log 2$$
337	330 336	mpbi	$$⊢\left(\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)\right)\log 2<1\log 2$$
338	39	mullidi	$$⊢1\log 2=\log 2$$
339	338	eqcomi	$$⊢\log 2=1\log 2$$
340	337 166 339	3brtr4i	$$⊢F\left(64\right)<\log 2$$
341	182 340	pm3.2i	$$⊢\left(F\left(64\right)\in ℝ\wedge F\left(64\right)<\log 2\right)$$