Theorem bposlem8

Description: Lemma for bpos . Evaluate F ( 6 4 ) and show it 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		3t2e6	$$⊢3\cdot 2=6$$
193	34 90 192	mulcomli	$$⊢2\cdot 3=6$$
194	52 90 59	mulcomli	$$⊢2\cdot 4=8$$
195	193 194	oveq12i	$$⊢\frac{2\cdot 3}{2\cdot 4}=\frac{6}{8}$$
196	191 195	eqtr3i	$$⊢\frac{3}{4}=\frac{6}{8}$$
197	196	oveq1i	$$⊢\left(\frac{3}{4}\right)+\left(\frac{1}{8}\right)=\left(\frac{6}{8}\right)+\left(\frac{1}{8}\right)$$
198	186 188 197	3eqtr4ri	$$⊢\left(\frac{3}{4}\right)+\left(\frac{1}{8}\right)=\frac{7}{8}$$
199	198	oveq1i	$$⊢\frac{\left(\frac{3}{4}\right)+\left(\frac{1}{8}\right)}{\sqrt{2}}=\frac{\frac{7}{8}}{\sqrt{2}}$$
200	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)$$
201		7cn	$$⊢7\in ℂ$$
202	201 7 49 40 72	divdiv32i	$$⊢\frac{\frac{7}{8}}{\sqrt{2}}=\frac{\frac{7}{\sqrt{2}}}{8}$$
203	199 200 202	3eqtr3i	$$⊢\left(\frac{\frac{3}{4}}{\sqrt{2}}\right)+\left(\frac{\frac{1}{8}}{\sqrt{2}}\right)=\frac{\frac{7}{\sqrt{2}}}{8}$$
204	203	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)$$
205	183 204	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)$$
206		4nn0	$$⊢4\in {\mathbb{N}}_0$$
207		9nn0	$$⊢9\in {\mathbb{N}}_0$$
208		0nn0	$$⊢0\in {\mathbb{N}}_0$$
209		9lt10	$$⊢9<10$$
210		4lt5	$$⊢4<5$$
211	206 91 207 208 209 210	decltc	$$⊢49<50$$
212		7t7e49	$$⊢7\cdot 7=49$$
213	57	oveq1i	$$⊢\sqrt{2}\sqrt{2}5\cdot 5=25\cdot 5$$
214	49 49 113 113	mul4i	$$⊢\sqrt{2}\sqrt{2}5\cdot 5=\sqrt{2}\cdot 5\sqrt{2}\cdot 5$$
215		5t2e10	$$⊢5\cdot 2=10$$
216	113 90 215	mulcomli	$$⊢2\cdot 5=10$$
217	216	oveq1i	$$⊢2\cdot 5\cdot 5=10\cdot 5$$
218	90 113 113	mulassi	$$⊢2\cdot 5\cdot 5=25\cdot 5$$
219	91	dec0u	$$⊢10\cdot 5=50$$
220	217 218 219	3eqtr3i	$$⊢25\cdot 5=50$$
221	213 214 220	3eqtr3i	$$⊢\sqrt{2}\cdot 5\sqrt{2}\cdot 5=50$$
222	211 212 221	3brtr4i	$$⊢7\cdot 7<\sqrt{2}\cdot 5\sqrt{2}\cdot 5$$
223		7re	$$⊢7\in ℝ$$
224		7pos	$$⊢0<7$$
225	12 223 224	ltleii	$$⊢0\le 7$$
226		nnrp	$$⊢5\in \mathbb{N}\to 5\in {ℝ}^{+}$$
227	106 226	ax-mp	$$⊢5\in {ℝ}^{+}$$
228		rpmulcl	$$⊢\left(\sqrt{2}\in {ℝ}^{+}\wedge 5\in {ℝ}^{+}\right)\to \sqrt{2}\cdot 5\in {ℝ}^{+}$$
229	66 227 228	mp2an	$$⊢\sqrt{2}\cdot 5\in {ℝ}^{+}$$
230		rpge0	$$⊢\sqrt{2}\cdot 5\in {ℝ}^{+}\to 0\le \sqrt{2}\cdot 5$$
231	229 230	ax-mp	$$⊢0\le \sqrt{2}\cdot 5$$
232		rpre	$$⊢\sqrt{2}\cdot 5\in {ℝ}^{+}\to \sqrt{2}\cdot 5\in ℝ$$
233	229 232	ax-mp	$$⊢\sqrt{2}\cdot 5\in ℝ$$
234	223 233	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)$$
235	225 231 234	mp2an	$$⊢7<\sqrt{2}\cdot 5\leftrightarrow 7\cdot 7<\sqrt{2}\cdot 5\sqrt{2}\cdot 5$$
236	222 235	mpbir	$$⊢7<\sqrt{2}\cdot 5$$
237		rpgt0	$$⊢\sqrt{2}\in {ℝ}^{+}\to 0<\sqrt{2}$$
238	26 65 237	mp2b	$$⊢0<\sqrt{2}$$
239		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)$$
240	223 173 239	mp3an12	$$⊢\left(\sqrt{2}\in ℝ\wedge 0<\sqrt{2}\right)\to \left(\frac{7}{\sqrt{2}}<5\leftrightarrow 7<\sqrt{2}\cdot 5\right)$$
241	48 238 240	mp2an	$$⊢\frac{7}{\sqrt{2}}<5\leftrightarrow 7<\sqrt{2}\cdot 5$$
242	236 241	mpbir	$$⊢\frac{7}{\sqrt{2}}<5$$
243	223 48 72	redivcli	$$⊢\frac{7}{\sqrt{2}}\in ℝ$$
244	243 173 13 14	ltdiv1ii	$$⊢\frac{7}{\sqrt{2}}<5\leftrightarrow \frac{\frac{7}{\sqrt{2}}}{8}<\frac{5}{8}$$
245	242 244	mpbi	$$⊢\frac{\frac{7}{\sqrt{2}}}{8}<\frac{5}{8}$$
246		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)$$
247	7 34 246	mp3an12	$$⊢\left(8\in ℂ\wedge 8\ne 0\right)\to \frac{8-3}{8}=\left(\frac{8}{8}\right)-\left(\frac{3}{8}\right)$$
248	7 40 247	mp2an	$$⊢\frac{8-3}{8}=\left(\frac{8}{8}\right)-\left(\frac{3}{8}\right)$$
249		5p3e8	$$⊢5+3=8$$
250	249	oveq1i	$$⊢5+3-3=8-3$$
251	113 34	pncan3oi	$$⊢5+3-3=5$$
252	250 251	eqtr3i	$$⊢8-3=5$$
253	252	oveq1i	$$⊢\frac{8-3}{8}=\frac{5}{8}$$
254	7 40	dividi	$$⊢\frac{8}{8}=1$$
255	254	oveq1i	$$⊢\left(\frac{8}{8}\right)-\left(\frac{3}{8}\right)=1-\left(\frac{3}{8}\right)$$
256	248 253 255	3eqtr3ri	$$⊢1-\left(\frac{3}{8}\right)=\frac{5}{8}$$
257		5lt8	$$⊢5<8$$
258	13 173	remulcli	$$⊢8\cdot 5\in ℝ$$
259	173 13 258	ltadd2i	$$⊢5<8\leftrightarrow 8\cdot 5+5<8\cdot 5+8$$
260	257 259	mpbi	$$⊢8\cdot 5+5<8\cdot 5+8$$
261		df-9	$$⊢9=8+1$$
262	261	oveq1i	$$⊢9\cdot 5=\left(8+1\right)\cdot 5$$
263	7 185 113	adddiri	$$⊢\left(8+1\right)\cdot 5=8\cdot 5+1\cdot 5$$
264	113	mulid2i	$$⊢1\cdot 5=5$$
265	264	oveq2i	$$⊢8\cdot 5+1\cdot 5=8\cdot 5+5$$
266	262 263 265	3eqtri	$$⊢9\cdot 5=8\cdot 5+5$$
267	87	oveq2i	$$⊢8\cdot 6=8\left(5+1\right)$$
268	7 113 185	adddii	$$⊢8\left(5+1\right)=8\cdot 5+8\cdot 1$$
269	7	mulid1i	$$⊢8\cdot 1=8$$
270	269	oveq2i	$$⊢8\cdot 5+8\cdot 1=8\cdot 5+8$$
271	267 268 270	3eqtri	$$⊢8\cdot 6=8\cdot 5+8$$
272	260 266 271	3brtr4i	$$⊢9\cdot 5<8\cdot 6$$
273	171 173	remulcli	$$⊢9\cdot 5\in ℝ$$
274		6re	$$⊢6\in ℝ$$
275	13 274	remulcli	$$⊢8\cdot 6\in ℝ$$
276	168 174	remulcli	$$⊢42^5\in ℝ$$
277	4 97	nnmulcli	$$⊢42^5\in \mathbb{N}$$
278	277	nngt0i	$$⊢0<42^5$$
279	273 275 276 278	ltdiv1ii	$$⊢9\cdot 5<8\cdot 6\leftrightarrow \frac{9\cdot 5}{42^5}<\frac{8\cdot 6}{42^5}$$
280	272 279	mpbi	$$⊢\frac{9\cdot 5}{42^5}<\frac{8\cdot 6}{42^5}$$
281	122 52 113 98 76 114	divmuldivi	$$⊢\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)=\frac{9\cdot 5}{42^5}$$
282		nnexpcl	$$⊢\left(2\in \mathbb{N}\wedge 4\in {\mathbb{N}}_0\right)\to 2^4\in \mathbb{N}$$
283	35 206 282	mp2an	$$⊢2^4\in \mathbb{N}$$
284	283	nncni	$$⊢2^4\in ℂ$$
285	283	nnne0i	$$⊢2^4\ne 0$$
286		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}$$
287	34 286	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}$$
288	7 40 284 285 287	mp4an	$$⊢\frac{2^4\cdot 3}{2^4\cdot 8}=\frac{3}{8}$$
289		df-4	$$⊢4=3+1$$
290	289	oveq2i	$$⊢2^4=2^{3+1}$$
291		3nn0	$$⊢3\in {\mathbb{N}}_0$$
292		expp1	$$⊢\left(2\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to 2^{3+1}=2^3\cdot 2$$
293	90 291 292	mp2an	$$⊢2^{3+1}=2^3\cdot 2$$
294	24	oveq1i	$$⊢2^3\cdot 2=8\cdot 2$$
295	290 293 294	3eqtri	$$⊢2^4=8\cdot 2$$
296	295	oveq1i	$$⊢2^4\cdot 3=8\cdot 2\cdot 3$$
297	7 90 34	mulassi	$$⊢8\cdot 2\cdot 3=82\cdot 3$$
298	193	oveq2i	$$⊢82\cdot 3=8\cdot 6$$
299	296 297 298	3eqtri	$$⊢2^4\cdot 3=8\cdot 6$$
300		4p3e7	$$⊢4+3=7$$
301		5p2e7	$$⊢5+2=7$$
302	113 90	addcomi	$$⊢5+2=2+5$$
303	300 301 302	3eqtr2i	$$⊢4+3=2+5$$
304	303	oveq2i	$$⊢2^{4+3}=2^{2+5}$$
305		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$$
306	90 206 291 305	mp3an	$$⊢2^{4+3}=2^4{2}^3$$
307		2nn0	$$⊢2\in {\mathbb{N}}_0$$
308		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$$
309	90 307 91 308	mp3an	$$⊢2^{2+5}=2^2{2}^5$$
310	304 306 309	3eqtr3i	$$⊢2^4{2}^3=2^2{2}^5$$
311	24	oveq2i	$$⊢2^4{2}^3=2^4\cdot 8$$
312		sq2	$$⊢2^2=4$$
313	312	oveq1i	$$⊢2^2{2}^5=42^5$$
314	310 311 313	3eqtr3i	$$⊢2^4\cdot 8=42^5$$
315	299 314	oveq12i	$$⊢\frac{2^4\cdot 3}{2^4\cdot 8}=\frac{8\cdot 6}{42^5}$$
316	288 315	eqtr3i	$$⊢\frac{3}{8}=\frac{8\cdot 6}{42^5}$$
317	280 281 316	3brtr4i	$$⊢\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)<\frac{3}{8}$$
318	167 13 40	redivcli	$$⊢\frac{3}{8}\in ℝ$$
319		1re	$$⊢1\in ℝ$$
320		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)$$
321	176 318 319 320	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)$$
322	317 321	mpbi	$$⊢1-\left(\frac{3}{8}\right)<1-\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)$$
323	256 322	eqbrtrri	$$⊢\frac{5}{8}<1-\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)$$
324	243 13 40	redivcli	$$⊢\frac{\frac{7}{\sqrt{2}}}{8}\in ℝ$$
325	173 13 40	redivcli	$$⊢\frac{5}{8}\in ℝ$$
326	319 176	resubcli	$$⊢1-\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)\in ℝ$$
327	324 325 326	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)$$
328	245 323 327	mp2an	$$⊢\frac{\frac{7}{\sqrt{2}}}{8}<1-\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)$$
329	324 176 319	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)$$
330	328 329	mpbir	$$⊢\left(\frac{\frac{7}{\sqrt{2}}}{8}\right)+\left(\frac{9}{4}\right)\left(\frac{5}{2^5}\right)<1$$
331	205 330	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$$
332		1lt2	$$⊢1<2$$
333		rplogcl	$$⊢\left(2\in ℝ\wedge 1<2\right)\to \log 2\in {ℝ}^{+}$$
334	54 332 333	mp2an	$$⊢\log 2\in {ℝ}^{+}$$
335		rpgt0	$$⊢\log 2\in {ℝ}^{+}\to 0<\log 2$$
336	334 335	ax-mp	$$⊢0<\log 2$$
337	180 319 38 336	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$$
338	331 337	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$$
339	39	mulid2i	$$⊢1\log 2=\log 2$$
340	339	eqcomi	$$⊢\log 2=1\log 2$$
341	338 166 340	3brtr4i	$$⊢F\left(64\right)<\log 2$$
342	182 341	pm3.2i	$$⊢\left(F\left(64\right)\in ℝ\wedge F\left(64\right)<\log 2\right)$$