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