Metamath Proof Explorer

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 2t3e6 ⊢ ( 2 · 3 ) = 6
193 2t4e8 ⊢ ( 2 · 4 ) = 8
194 192 193 oveq12i ⊢ ( ( 2 · 3 ) / ( 2 · 4 ) ) = ( 6 / 8 )
195 191 194 eqtr3i ⊢ ( 3 / 4 ) = ( 6 / 8 )
196 195 oveq1i ⊢ ( ( 3 / 4 ) + ( 1 / 8 ) ) = ( ( 6 / 8 ) + ( 1 / 8 ) )
197 186 188 196 3eqtr4ri ⊢ ( ( 3 / 4 ) + ( 1 / 8 ) ) = ( 7 / 8 )
198 197 oveq1i ⊢ ( ( ( 3 / 4 ) + ( 1 / 8 ) ) / ( √ ‘ 2 ) ) = ( ( 7 / 8 ) / ( √ ‘ 2 ) )
199 128 160 49 72 divdiri ⊢ ( ( ( 3 / 4 ) + ( 1 / 8 ) ) / ( √ ‘ 2 ) ) = ( ( ( 3 / 4 ) / ( √ ‘ 2 ) ) + ( ( 1 / 8 ) / ( √ ‘ 2 ) ) )
200 7cn ⊢ 7 ∈ ℂ
201 200 7 49 40 72 divdiv32i ⊢ ( ( 7 / 8 ) / ( √ ‘ 2 ) ) = ( ( 7 / ( √ ‘ 2 ) ) / 8 )
202 198 199 201 3eqtr3i ⊢ ( ( ( 3 / 4 ) / ( √ ‘ 2 ) ) + ( ( 1 / 8 ) / ( √ ‘ 2 ) ) ) = ( ( 7 / ( √ ‘ 2 ) ) / 8 )
203 202 oveq1i ⊢ ( ( ( ( 3 / 4 ) / ( √ ‘ 2 ) ) + ( ( 1 / 8 ) / ( √ ‘ 2 ) ) ) + ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) ) = ( ( ( 7 / ( √ ‘ 2 ) ) / 8 ) + ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) )
204 183 203 eqtri ⊢ ( ( ( ( 3 / 4 ) / ( √ ‘ 2 ) ) + ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) ) + ( ( 1 / 8 ) / ( √ ‘ 2 ) ) ) = ( ( ( 7 / ( √ ‘ 2 ) ) / 8 ) + ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) )
205 4nn0 ⊢ 4 ∈ ℕ0
206 9nn0 ⊢ 9 ∈ ℕ0
207 0nn0 ⊢ 0 ∈ ℕ0
208 9lt10 ⊢ 9 < 1 0
209 4lt5 ⊢ 4 < 5
210 205 91 206 207 208 209 decltc ⊢ 4 9 < 5 0
211 7t7e49 ⊢ ( 7 · 7 ) = 4 9
212 57 oveq1i ⊢ ( ( ( √ ‘ 2 ) · ( √ ‘ 2 ) ) · ( 5 · 5 ) ) = ( 2 · ( 5 · 5 ) )
213 49 49 113 113 mul4i ⊢ ( ( ( √ ‘ 2 ) · ( √ ‘ 2 ) ) · ( 5 · 5 ) ) = ( ( ( √ ‘ 2 ) · 5 ) · ( ( √ ‘ 2 ) · 5 ) )
214 5t2e10 ⊢ ( 5 · 2 ) = 1 0
215 113 90 214 mulcomli ⊢ ( 2 · 5 ) = 1 0
216 215 oveq1i ⊢ ( ( 2 · 5 ) · 5 ) = ( 1 0 · 5 )
217 90 113 113 mulassi ⊢ ( ( 2 · 5 ) · 5 ) = ( 2 · ( 5 · 5 ) )
218 91 dec0u ⊢ ( 1 0 · 5 ) = 5 0
219 216 217 218 3eqtr3i ⊢ ( 2 · ( 5 · 5 ) ) = 5 0
220 212 213 219 3eqtr3i ⊢ ( ( ( √ ‘ 2 ) · 5 ) · ( ( √ ‘ 2 ) · 5 ) ) = 5 0
221 210 211 220 3brtr4i ⊢ ( 7 · 7 ) < ( ( ( √ ‘ 2 ) · 5 ) · ( ( √ ‘ 2 ) · 5 ) )
222 7re ⊢ 7 ∈ ℝ
223 7pos ⊢ 0 < 7
224 12 222 223 ltleii ⊢ 0 ≤ 7
225 nnrp ⊢ ( 5 ∈ ℕ → 5 ∈ ℝ+ )
226 106 225 ax-mp ⊢ 5 ∈ ℝ+
227 rpmulcl ⊢ ( ( ( √ ‘ 2 ) ∈ ℝ+ ∧ 5 ∈ ℝ+ ) → ( ( √ ‘ 2 ) · 5 ) ∈ ℝ+ )
228 66 226 227 mp2an ⊢ ( ( √ ‘ 2 ) · 5 ) ∈ ℝ+
229 rpge0 ⊢ ( ( ( √ ‘ 2 ) · 5 ) ∈ ℝ+ → 0 ≤ ( ( √ ‘ 2 ) · 5 ) )
230 228 229 ax-mp ⊢ 0 ≤ ( ( √ ‘ 2 ) · 5 )
231 rpre ⊢ ( ( ( √ ‘ 2 ) · 5 ) ∈ ℝ+ → ( ( √ ‘ 2 ) · 5 ) ∈ ℝ )
232 228 231 ax-mp ⊢ ( ( √ ‘ 2 ) · 5 ) ∈ ℝ
233 222 232 lt2msqi ⊢ ( ( 0 ≤ 7 ∧ 0 ≤ ( ( √ ‘ 2 ) · 5 ) ) → ( 7 < ( ( √ ‘ 2 ) · 5 ) ↔ ( 7 · 7 ) < ( ( ( √ ‘ 2 ) · 5 ) · ( ( √ ‘ 2 ) · 5 ) ) ) )
234 224 230 233 mp2an ⊢ ( 7 < ( ( √ ‘ 2 ) · 5 ) ↔ ( 7 · 7 ) < ( ( ( √ ‘ 2 ) · 5 ) · ( ( √ ‘ 2 ) · 5 ) ) )
235 221 234 mpbir ⊢ 7 < ( ( √ ‘ 2 ) · 5 )
236 rpgt0 ⊢ ( ( √ ‘ 2 ) ∈ ℝ+ → 0 < ( √ ‘ 2 ) )
237 26 65 236 mp2b ⊢ 0 < ( √ ‘ 2 )
238 ltdivmul ⊢ ( ( 7 ∈ ℝ ∧ 5 ∈ ℝ ∧ ( ( √ ‘ 2 ) ∈ ℝ ∧ 0 < ( √ ‘ 2 ) ) ) → ( ( 7 / ( √ ‘ 2 ) ) < 5 ↔ 7 < ( ( √ ‘ 2 ) · 5 ) ) )
239 222 173 238 mp3an12 ⊢ ( ( ( √ ‘ 2 ) ∈ ℝ ∧ 0 < ( √ ‘ 2 ) ) → ( ( 7 / ( √ ‘ 2 ) ) < 5 ↔ 7 < ( ( √ ‘ 2 ) · 5 ) ) )
240 48 237 239 mp2an ⊢ ( ( 7 / ( √ ‘ 2 ) ) < 5 ↔ 7 < ( ( √ ‘ 2 ) · 5 ) )
241 235 240 mpbir ⊢ ( 7 / ( √ ‘ 2 ) ) < 5
242 222 48 72 redivcli ⊢ ( 7 / ( √ ‘ 2 ) ) ∈ ℝ
243 242 173 13 14 ltdiv1ii ⊢ ( ( 7 / ( √ ‘ 2 ) ) < 5 ↔ ( ( 7 / ( √ ‘ 2 ) ) / 8 ) < ( 5 / 8 ) )
244 241 243 mpbi ⊢ ( ( 7 / ( √ ‘ 2 ) ) / 8 ) < ( 5 / 8 )
245 divsubdir ⊢ ( ( 8 ∈ ℂ ∧ 3 ∈ ℂ ∧ ( 8 ∈ ℂ ∧ 8 ≠ 0 ) ) → ( ( 8 − 3 ) / 8 ) = ( ( 8 / 8 ) − ( 3 / 8 ) ) )
246 7 34 245 mp3an12 ⊢ ( ( 8 ∈ ℂ ∧ 8 ≠ 0 ) → ( ( 8 − 3 ) / 8 ) = ( ( 8 / 8 ) − ( 3 / 8 ) ) )
247 7 40 246 mp2an ⊢ ( ( 8 − 3 ) / 8 ) = ( ( 8 / 8 ) − ( 3 / 8 ) )
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 ⊢ ( ( 8 − 3 ) / 8 ) = ( 5 / 8 )
253 7 40 dividi ⊢ ( 8 / 8 ) = 1
254 253 oveq1i ⊢ ( ( 8 / 8 ) − ( 3 / 8 ) ) = ( 1 − ( 3 / 8 ) )
255 247 252 254 3eqtr3ri ⊢ ( 1 − ( 3 / 8 ) ) = ( 5 / 8 )
256 5lt8 ⊢ 5 < 8
257 13 173 remulcli ⊢ ( 8 · 5 ) ∈ ℝ
258 173 13 257 ltadd2i ⊢ ( 5 < 8 ↔ ( ( 8 · 5 ) + 5 ) < ( ( 8 · 5 ) + 8 ) )
259 256 258 mpbi ⊢ ( ( 8 · 5 ) + 5 ) < ( ( 8 · 5 ) + 8 )
260 df-9 ⊢ 9 = ( 8 + 1 )
261 260 oveq1i ⊢ ( 9 · 5 ) = ( ( 8 + 1 ) · 5 )
262 7 185 113 adddiri ⊢ ( ( 8 + 1 ) · 5 ) = ( ( 8 · 5 ) + ( 1 · 5 ) )
263 113 mullidi ⊢ ( 1 · 5 ) = 5
264 263 oveq2i ⊢ ( ( 8 · 5 ) + ( 1 · 5 ) ) = ( ( 8 · 5 ) + 5 )
265 261 262 264 3eqtri ⊢ ( 9 · 5 ) = ( ( 8 · 5 ) + 5 )
266 87 oveq2i ⊢ ( 8 · 6 ) = ( 8 · ( 5 + 1 ) )
267 7 113 185 adddii ⊢ ( 8 · ( 5 + 1 ) ) = ( ( 8 · 5 ) + ( 8 · 1 ) )
268 7 mulridi ⊢ ( 8 · 1 ) = 8
269 268 oveq2i ⊢ ( ( 8 · 5 ) + ( 8 · 1 ) ) = ( ( 8 · 5 ) + 8 )
270 266 267 269 3eqtri ⊢ ( 8 · 6 ) = ( ( 8 · 5 ) + 8 )
271 259 265 270 3brtr4i ⊢ ( 9 · 5 ) < ( 8 · 6 )
272 171 173 remulcli ⊢ ( 9 · 5 ) ∈ ℝ
273 6re ⊢ 6 ∈ ℝ
274 13 273 remulcli ⊢ ( 8 · 6 ) ∈ ℝ
275 168 174 remulcli ⊢ ( 4 · ( 2 ↑ 5 ) ) ∈ ℝ
276 4 97 nnmulcli ⊢ ( 4 · ( 2 ↑ 5 ) ) ∈ ℕ
277 276 nngt0i ⊢ 0 < ( 4 · ( 2 ↑ 5 ) )
278 272 274 275 277 ltdiv1ii ⊢ ( ( 9 · 5 ) < ( 8 · 6 ) ↔ ( ( 9 · 5 ) / ( 4 · ( 2 ↑ 5 ) ) ) < ( ( 8 · 6 ) / ( 4 · ( 2 ↑ 5 ) ) ) )
279 271 278 mpbi ⊢ ( ( 9 · 5 ) / ( 4 · ( 2 ↑ 5 ) ) ) < ( ( 8 · 6 ) / ( 4 · ( 2 ↑ 5 ) ) )
280 122 52 113 98 76 114 divmuldivi ⊢ ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) = ( ( 9 · 5 ) / ( 4 · ( 2 ↑ 5 ) ) )
281 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 4 ∈ ℕ0 ) → ( 2 ↑ 4 ) ∈ ℕ )
282 35 205 281 mp2an ⊢ ( 2 ↑ 4 ) ∈ ℕ
283 282 nncni ⊢ ( 2 ↑ 4 ) ∈ ℂ
284 282 nnne0i ⊢ ( 2 ↑ 4 ) ≠ 0
285 divcan5 ⊢ ( ( 3 ∈ ℂ ∧ ( 8 ∈ ℂ ∧ 8 ≠ 0 ) ∧ ( ( 2 ↑ 4 ) ∈ ℂ ∧ ( 2 ↑ 4 ) ≠ 0 ) ) → ( ( ( 2 ↑ 4 ) · 3 ) / ( ( 2 ↑ 4 ) · 8 ) ) = ( 3 / 8 ) )
286 34 285 mp3an1 ⊢ ( ( ( 8 ∈ ℂ ∧ 8 ≠ 0 ) ∧ ( ( 2 ↑ 4 ) ∈ ℂ ∧ ( 2 ↑ 4 ) ≠ 0 ) ) → ( ( ( 2 ↑ 4 ) · 3 ) / ( ( 2 ↑ 4 ) · 8 ) ) = ( 3 / 8 ) )
287 7 40 283 284 286 mp4an ⊢ ( ( ( 2 ↑ 4 ) · 3 ) / ( ( 2 ↑ 4 ) · 8 ) ) = ( 3 / 8 )
288 df-4 ⊢ 4 = ( 3 + 1 )
289 288 oveq2i ⊢ ( 2 ↑ 4 ) = ( 2 ↑ ( 3 + 1 ) )
290 3nn0 ⊢ 3 ∈ ℕ0
291 expp1 ⊢ ( ( 2 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 2 ↑ ( 3 + 1 ) ) = ( ( 2 ↑ 3 ) · 2 ) )
292 90 290 291 mp2an ⊢ ( 2 ↑ ( 3 + 1 ) ) = ( ( 2 ↑ 3 ) · 2 )
293 24 oveq1i ⊢ ( ( 2 ↑ 3 ) · 2 ) = ( 8 · 2 )
294 289 292 293 3eqtri ⊢ ( 2 ↑ 4 ) = ( 8 · 2 )
295 294 oveq1i ⊢ ( ( 2 ↑ 4 ) · 3 ) = ( ( 8 · 2 ) · 3 )
296 7 90 34 mulassi ⊢ ( ( 8 · 2 ) · 3 ) = ( 8 · ( 2 · 3 ) )
297 192 oveq2i ⊢ ( 8 · ( 2 · 3 ) ) = ( 8 · 6 )
298 295 296 297 3eqtri ⊢ ( ( 2 ↑ 4 ) · 3 ) = ( 8 · 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 ⊢ ( ( 2 ∈ ℂ ∧ 4 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) → ( 2 ↑ ( 4 + 3 ) ) = ( ( 2 ↑ 4 ) · ( 2 ↑ 3 ) ) )
305 90 205 290 304 mp3an ⊢ ( 2 ↑ ( 4 + 3 ) ) = ( ( 2 ↑ 4 ) · ( 2 ↑ 3 ) )
306 2nn0 ⊢ 2 ∈ ℕ0
307 expadd ⊢ ( ( 2 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) → ( 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 ) · 8 )
311 sq2 ⊢ ( 2 ↑ 2 ) = 4
312 311 oveq1i ⊢ ( ( 2 ↑ 2 ) · ( 2 ↑ 5 ) ) = ( 4 · ( 2 ↑ 5 ) )
313 309 310 312 3eqtr3i ⊢ ( ( 2 ↑ 4 ) · 8 ) = ( 4 · ( 2 ↑ 5 ) )
314 298 313 oveq12i ⊢ ( ( ( 2 ↑ 4 ) · 3 ) / ( ( 2 ↑ 4 ) · 8 ) ) = ( ( 8 · 6 ) / ( 4 · ( 2 ↑ 5 ) ) )
315 287 314 eqtr3i ⊢ ( 3 / 8 ) = ( ( 8 · 6 ) / ( 4 · ( 2 ↑ 5 ) ) )
316 279 280 315 3brtr4i ⊢ ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) < ( 3 / 8 )
317 167 13 40 redivcli ⊢ ( 3 / 8 ) ∈ ℝ
318 1re ⊢ 1 ∈ ℝ
319 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 ) ) ) ) ) )
320 176 317 318 319 mp3an ⊢ ( ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) < ( 3 / 8 ) ↔ ( 1 − ( 3 / 8 ) ) < ( 1 − ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) ) )
321 316 320 mpbi ⊢ ( 1 − ( 3 / 8 ) ) < ( 1 − ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) )
322 255 321 eqbrtrri ⊢ ( 5 / 8 ) < ( 1 − ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) )
323 242 13 40 redivcli ⊢ ( ( 7 / ( √ ‘ 2 ) ) / 8 ) ∈ ℝ
324 173 13 40 redivcli ⊢ ( 5 / 8 ) ∈ ℝ
325 318 176 resubcli ⊢ ( 1 − ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) ) ∈ ℝ
326 323 324 325 lttri ⊢ ( ( ( ( 7 / ( √ ‘ 2 ) ) / 8 ) < ( 5 / 8 ) ∧ ( 5 / 8 ) < ( 1 − ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) ) ) → ( ( 7 / ( √ ‘ 2 ) ) / 8 ) < ( 1 − ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) ) )
327 244 322 326 mp2an ⊢ ( ( 7 / ( √ ‘ 2 ) ) / 8 ) < ( 1 − ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) )
328 323 176 318 ltaddsubi ⊢ ( ( ( ( 7 / ( √ ‘ 2 ) ) / 8 ) + ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) ) < 1 ↔ ( ( 7 / ( √ ‘ 2 ) ) / 8 ) < ( 1 − ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) ) )
329 327 328 mpbir ⊢ ( ( ( 7 / ( √ ‘ 2 ) ) / 8 ) + ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) ) < 1
330 204 329 eqbrtri ⊢ ( ( ( ( 3 / 4 ) / ( √ ‘ 2 ) ) + ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) ) + ( ( 1 / 8 ) / ( √ ‘ 2 ) ) ) < 1
331 1lt2 ⊢ 1 < 2
332 rplogcl ⊢ ( ( 2 ∈ ℝ ∧ 1 < 2 ) → ( log ‘ 2 ) ∈ ℝ+ )
333 54 331 332 mp2an ⊢ ( log ‘ 2 ) ∈ ℝ+
334 rpgt0 ⊢ ( ( log ‘ 2 ) ∈ ℝ+ → 0 < ( log ‘ 2 ) )
335 333 334 ax-mp ⊢ 0 < ( log ‘ 2 )
336 180 318 38 335 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 ) ) )
337 330 336 mpbi ⊢ ( ( ( ( ( 3 / 4 ) / ( √ ‘ 2 ) ) + ( ( 9 / 4 ) · ( 5 / ( 2 ↑ 5 ) ) ) ) + ( ( 1 / 8 ) / ( √ ‘ 2 ) ) ) · ( 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 ⊢ ( 𝐹 ‘ 6 4 ) < ( log ‘ 2 )
341 182 340 pm3.2i ⊢ ( ( 𝐹 ‘ 6 4 ) ∈ ℝ ∧ ( 𝐹 ‘ 6 4 ) < ( log ‘ 2 ) )