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 
|- F = ( n e. NN |-> ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. n ) ) ) ) )
bposlem7.2 
|- G = ( x e. RR+ |-> ( ( log ` x ) / x ) )
Assertion bposlem8 
|- ( ( F ` ; 6 4 ) e. RR /\ ( F ` ; 6 4 ) < ( log ` 2 ) )

Proof

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