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	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑛 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑛 / 2 ) ) ) ) + ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑛 ) ) ) ) )
	bposlem7.2	⊢ 𝐺 = ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / 𝑥 ) )
Assertion	bposlem8	⊢ ( ( 𝐹 ‘ ; 6 4 ) ∈ ℝ ∧ ( 𝐹 ‘ ; 6 4 ) < ( log ‘ 2 ) )

Proof

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