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 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 mulid2i ⊢ ( 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 mulid1i ⊢ ( 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 mulid2i ⊢ ( 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 ) )