Metamath Proof Explorer

Theorem bposlem7

Description: Lemma for bpos . The function F is decreasing. (Contributed by Mario Carneiro, 13-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 ) )
bposlem7.3 
|- ( ph -> A e. NN )
bposlem7.4 
|- ( ph -> B e. NN )
bposlem7.5 
|- ( ph -> ( _e ^ 2 ) <_ A )
bposlem7.6 
|- ( ph -> ( _e ^ 2 ) <_ B )
Assertion bposlem7 
|- ( ph -> ( A < B -> ( F ` B ) < ( F ` A ) ) )

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 bposlem7.3 
 |-  ( ph -> A e. NN )
4 bposlem7.4 
 |-  ( ph -> B e. NN )
5 bposlem7.5 
 |-  ( ph -> ( _e ^ 2 ) <_ A )
6 bposlem7.6 
 |-  ( ph -> ( _e ^ 2 ) <_ B )
7 4 nnrpd 
 |-  ( ph -> B e. RR+ )
8 7 rpsqrtcld 
 |-  ( ph -> ( sqrt ` B ) e. RR+ )
9 fveq2 
 |-  ( x = ( sqrt ` B ) -> ( log ` x ) = ( log ` ( sqrt ` B ) ) )
10 id 
 |-  ( x = ( sqrt ` B ) -> x = ( sqrt ` B ) )
11 9 10 oveq12d 
 |-  ( x = ( sqrt ` B ) -> ( ( log ` x ) / x ) = ( ( log ` ( sqrt ` B ) ) / ( sqrt ` B ) ) )
12 ovex 
 |-  ( ( log ` ( sqrt ` B ) ) / ( sqrt ` B ) ) e. _V
13 11 2 12 fvmpt 
 |-  ( ( sqrt ` B ) e. RR+ -> ( G ` ( sqrt ` B ) ) = ( ( log ` ( sqrt ` B ) ) / ( sqrt ` B ) ) )
14 8 13 syl 
 |-  ( ph -> ( G ` ( sqrt ` B ) ) = ( ( log ` ( sqrt ` B ) ) / ( sqrt ` B ) ) )
15 3 nnrpd 
 |-  ( ph -> A e. RR+ )
16 15 rpsqrtcld 
 |-  ( ph -> ( sqrt ` A ) e. RR+ )
17 fveq2 
 |-  ( x = ( sqrt ` A ) -> ( log ` x ) = ( log ` ( sqrt ` A ) ) )
18 id 
 |-  ( x = ( sqrt ` A ) -> x = ( sqrt ` A ) )
19 17 18 oveq12d 
 |-  ( x = ( sqrt ` A ) -> ( ( log ` x ) / x ) = ( ( log ` ( sqrt ` A ) ) / ( sqrt ` A ) ) )
20 ovex 
 |-  ( ( log ` ( sqrt ` A ) ) / ( sqrt ` A ) ) e. _V
21 19 2 20 fvmpt 
 |-  ( ( sqrt ` A ) e. RR+ -> ( G ` ( sqrt ` A ) ) = ( ( log ` ( sqrt ` A ) ) / ( sqrt ` A ) ) )
22 16 21 syl 
 |-  ( ph -> ( G ` ( sqrt ` A ) ) = ( ( log ` ( sqrt ` A ) ) / ( sqrt ` A ) ) )
23 14 22 breq12d 
 |-  ( ph -> ( ( G ` ( sqrt ` B ) ) < ( G ` ( sqrt ` A ) ) <-> ( ( log ` ( sqrt ` B ) ) / ( sqrt ` B ) ) < ( ( log ` ( sqrt ` A ) ) / ( sqrt ` A ) ) ) )
24 16 rpred 
 |-  ( ph -> ( sqrt ` A ) e. RR )
25 15 rprege0d 
 |-  ( ph -> ( A e. RR /\ 0 <_ A ) )
26 resqrtth 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( sqrt ` A ) ^ 2 ) = A )
27 25 26 syl 
 |-  ( ph -> ( ( sqrt ` A ) ^ 2 ) = A )
28 5 27 breqtrrd 
 |-  ( ph -> ( _e ^ 2 ) <_ ( ( sqrt ` A ) ^ 2 ) )
29 16 rpge0d 
 |-  ( ph -> 0 <_ ( sqrt ` A ) )
30 ere 
 |-  _e e. RR
31 0re 
 |-  0 e. RR
32 epos 
 |-  0 < _e
33 31 30 32 ltleii 
 |-  0 <_ _e
34 le2sq 
 |-  ( ( ( _e e. RR /\ 0 <_ _e ) /\ ( ( sqrt ` A ) e. RR /\ 0 <_ ( sqrt ` A ) ) ) -> ( _e <_ ( sqrt ` A ) <-> ( _e ^ 2 ) <_ ( ( sqrt ` A ) ^ 2 ) ) )
35 30 33 34 mpanl12 
 |-  ( ( ( sqrt ` A ) e. RR /\ 0 <_ ( sqrt ` A ) ) -> ( _e <_ ( sqrt ` A ) <-> ( _e ^ 2 ) <_ ( ( sqrt ` A ) ^ 2 ) ) )
36 24 29 35 syl2anc 
 |-  ( ph -> ( _e <_ ( sqrt ` A ) <-> ( _e ^ 2 ) <_ ( ( sqrt ` A ) ^ 2 ) ) )
37 28 36 mpbird 
 |-  ( ph -> _e <_ ( sqrt ` A ) )
38 8 rpred 
 |-  ( ph -> ( sqrt ` B ) e. RR )
39 7 rprege0d 
 |-  ( ph -> ( B e. RR /\ 0 <_ B ) )
40 resqrtth 
 |-  ( ( B e. RR /\ 0 <_ B ) -> ( ( sqrt ` B ) ^ 2 ) = B )
41 39 40 syl 
 |-  ( ph -> ( ( sqrt ` B ) ^ 2 ) = B )
42 6 41 breqtrrd 
 |-  ( ph -> ( _e ^ 2 ) <_ ( ( sqrt ` B ) ^ 2 ) )
43 8 rpge0d 
 |-  ( ph -> 0 <_ ( sqrt ` B ) )
44 le2sq 
 |-  ( ( ( _e e. RR /\ 0 <_ _e ) /\ ( ( sqrt ` B ) e. RR /\ 0 <_ ( sqrt ` B ) ) ) -> ( _e <_ ( sqrt ` B ) <-> ( _e ^ 2 ) <_ ( ( sqrt ` B ) ^ 2 ) ) )
45 30 33 44 mpanl12 
 |-  ( ( ( sqrt ` B ) e. RR /\ 0 <_ ( sqrt ` B ) ) -> ( _e <_ ( sqrt ` B ) <-> ( _e ^ 2 ) <_ ( ( sqrt ` B ) ^ 2 ) ) )
46 38 43 45 syl2anc 
 |-  ( ph -> ( _e <_ ( sqrt ` B ) <-> ( _e ^ 2 ) <_ ( ( sqrt ` B ) ^ 2 ) ) )
47 42 46 mpbird 
 |-  ( ph -> _e <_ ( sqrt ` B ) )
48 logdivlt 
 |-  ( ( ( ( sqrt ` A ) e. RR /\ _e <_ ( sqrt ` A ) ) /\ ( ( sqrt ` B ) e. RR /\ _e <_ ( sqrt ` B ) ) ) -> ( ( sqrt ` A ) < ( sqrt ` B ) <-> ( ( log ` ( sqrt ` B ) ) / ( sqrt ` B ) ) < ( ( log ` ( sqrt ` A ) ) / ( sqrt ` A ) ) ) )
49 24 37 38 47 48 syl22anc 
 |-  ( ph -> ( ( sqrt ` A ) < ( sqrt ` B ) <-> ( ( log ` ( sqrt ` B ) ) / ( sqrt ` B ) ) < ( ( log ` ( sqrt ` A ) ) / ( sqrt ` A ) ) ) )
50 24 38 29 43 lt2sqd 
 |-  ( ph -> ( ( sqrt ` A ) < ( sqrt ` B ) <-> ( ( sqrt ` A ) ^ 2 ) < ( ( sqrt ` B ) ^ 2 ) ) )
51 23 49 50 3bitr2rd 
 |-  ( ph -> ( ( ( sqrt ` A ) ^ 2 ) < ( ( sqrt ` B ) ^ 2 ) <-> ( G ` ( sqrt ` B ) ) < ( G ` ( sqrt ` A ) ) ) )
52 27 41 breq12d 
 |-  ( ph -> ( ( ( sqrt ` A ) ^ 2 ) < ( ( sqrt ` B ) ^ 2 ) <-> A < B ) )
53 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
54 rerpdivcl 
 |-  ( ( ( log ` x ) e. RR /\ x e. RR+ ) -> ( ( log ` x ) / x ) e. RR )
55 53 54 mpancom 
 |-  ( x e. RR+ -> ( ( log ` x ) / x ) e. RR )
56 2 55 fmpti 
 |-  G : RR+ --> RR
57 56 ffvelcdmi 
 |-  ( ( sqrt ` B ) e. RR+ -> ( G ` ( sqrt ` B ) ) e. RR )
58 8 57 syl 
 |-  ( ph -> ( G ` ( sqrt ` B ) ) e. RR )
59 56 ffvelcdmi 
 |-  ( ( sqrt ` A ) e. RR+ -> ( G ` ( sqrt ` A ) ) e. RR )
60 16 59 syl 
 |-  ( ph -> ( G ` ( sqrt ` A ) ) e. RR )
61 2rp 
 |-  2 e. RR+
62 rpsqrtcl 
 |-  ( 2 e. RR+ -> ( sqrt ` 2 ) e. RR+ )
63 61 62 mp1i 
 |-  ( ph -> ( sqrt ` 2 ) e. RR+ )
64 58 60 63 ltmul2d 
 |-  ( ph -> ( ( G ` ( sqrt ` B ) ) < ( G ` ( sqrt ` A ) ) <-> ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) < ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) ) )
65 51 52 64 3bitr3d 
 |-  ( ph -> ( A < B <-> ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) < ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) ) )
66 65 biimpd 
 |-  ( ph -> ( A < B -> ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) < ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) ) )
67 3 nnred 
 |-  ( ph -> A e. RR )
68 4 nnred 
 |-  ( ph -> B e. RR )
69 2re 
 |-  2 e. RR
70 2pos 
 |-  0 < 2
71 69 70 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
72 71 a1i 
 |-  ( ph -> ( 2 e. RR /\ 0 < 2 ) )
73 ltdiv1 
 |-  ( ( A e. RR /\ B e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( A < B <-> ( A / 2 ) < ( B / 2 ) ) )
74 67 68 72 73 syl3anc 
 |-  ( ph -> ( A < B <-> ( A / 2 ) < ( B / 2 ) ) )
75 15 rphalfcld 
 |-  ( ph -> ( A / 2 ) e. RR+ )
76 75 rpred 
 |-  ( ph -> ( A / 2 ) e. RR )
77 30 69 remulcli 
 |-  ( _e x. 2 ) e. RR
78 77 a1i 
 |-  ( ph -> ( _e x. 2 ) e. RR )
79 30 resqcli 
 |-  ( _e ^ 2 ) e. RR
80 79 a1i 
 |-  ( ph -> ( _e ^ 2 ) e. RR )
81 egt2lt3 
 |-  ( 2 < _e /\ _e < 3 )
82 81 simpli 
 |-  2 < _e
83 69 30 82 ltleii 
 |-  2 <_ _e
84 69 30 30 lemul2i 
 |-  ( 0 < _e -> ( 2 <_ _e <-> ( _e x. 2 ) <_ ( _e x. _e ) ) )
85 32 84 ax-mp 
 |-  ( 2 <_ _e <-> ( _e x. 2 ) <_ ( _e x. _e ) )
86 83 85 mpbi 
 |-  ( _e x. 2 ) <_ ( _e x. _e )
87 30 recni 
 |-  _e e. CC
88 87 sqvali 
 |-  ( _e ^ 2 ) = ( _e x. _e )
89 86 88 breqtrri 
 |-  ( _e x. 2 ) <_ ( _e ^ 2 )
90 89 a1i 
 |-  ( ph -> ( _e x. 2 ) <_ ( _e ^ 2 ) )
91 78 80 67 90 5 letrd 
 |-  ( ph -> ( _e x. 2 ) <_ A )
92 lemuldiv 
 |-  ( ( _e e. RR /\ A e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( _e x. 2 ) <_ A <-> _e <_ ( A / 2 ) ) )
93 30 71 92 mp3an13 
 |-  ( A e. RR -> ( ( _e x. 2 ) <_ A <-> _e <_ ( A / 2 ) ) )
94 67 93 syl 
 |-  ( ph -> ( ( _e x. 2 ) <_ A <-> _e <_ ( A / 2 ) ) )
95 91 94 mpbid 
 |-  ( ph -> _e <_ ( A / 2 ) )
96 7 rphalfcld 
 |-  ( ph -> ( B / 2 ) e. RR+ )
97 96 rpred 
 |-  ( ph -> ( B / 2 ) e. RR )
98 78 80 68 90 6 letrd 
 |-  ( ph -> ( _e x. 2 ) <_ B )
99 lemuldiv 
 |-  ( ( _e e. RR /\ B e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( _e x. 2 ) <_ B <-> _e <_ ( B / 2 ) ) )
100 30 71 99 mp3an13 
 |-  ( B e. RR -> ( ( _e x. 2 ) <_ B <-> _e <_ ( B / 2 ) ) )
101 68 100 syl 
 |-  ( ph -> ( ( _e x. 2 ) <_ B <-> _e <_ ( B / 2 ) ) )
102 98 101 mpbid 
 |-  ( ph -> _e <_ ( B / 2 ) )
103 logdivlt 
 |-  ( ( ( ( A / 2 ) e. RR /\ _e <_ ( A / 2 ) ) /\ ( ( B / 2 ) e. RR /\ _e <_ ( B / 2 ) ) ) -> ( ( A / 2 ) < ( B / 2 ) <-> ( ( log ` ( B / 2 ) ) / ( B / 2 ) ) < ( ( log ` ( A / 2 ) ) / ( A / 2 ) ) ) )
104 76 95 97 102 103 syl22anc 
 |-  ( ph -> ( ( A / 2 ) < ( B / 2 ) <-> ( ( log ` ( B / 2 ) ) / ( B / 2 ) ) < ( ( log ` ( A / 2 ) ) / ( A / 2 ) ) ) )
105 74 104 bitrd 
 |-  ( ph -> ( A < B <-> ( ( log ` ( B / 2 ) ) / ( B / 2 ) ) < ( ( log ` ( A / 2 ) ) / ( A / 2 ) ) ) )
106 fveq2 
 |-  ( x = ( B / 2 ) -> ( log ` x ) = ( log ` ( B / 2 ) ) )
107 id 
 |-  ( x = ( B / 2 ) -> x = ( B / 2 ) )
108 106 107 oveq12d 
 |-  ( x = ( B / 2 ) -> ( ( log ` x ) / x ) = ( ( log ` ( B / 2 ) ) / ( B / 2 ) ) )
109 ovex 
 |-  ( ( log ` ( B / 2 ) ) / ( B / 2 ) ) e. _V
110 108 2 109 fvmpt 
 |-  ( ( B / 2 ) e. RR+ -> ( G ` ( B / 2 ) ) = ( ( log ` ( B / 2 ) ) / ( B / 2 ) ) )
111 96 110 syl 
 |-  ( ph -> ( G ` ( B / 2 ) ) = ( ( log ` ( B / 2 ) ) / ( B / 2 ) ) )
112 fveq2 
 |-  ( x = ( A / 2 ) -> ( log ` x ) = ( log ` ( A / 2 ) ) )
113 id 
 |-  ( x = ( A / 2 ) -> x = ( A / 2 ) )
114 112 113 oveq12d 
 |-  ( x = ( A / 2 ) -> ( ( log ` x ) / x ) = ( ( log ` ( A / 2 ) ) / ( A / 2 ) ) )
115 ovex 
 |-  ( ( log ` ( A / 2 ) ) / ( A / 2 ) ) e. _V
116 114 2 115 fvmpt 
 |-  ( ( A / 2 ) e. RR+ -> ( G ` ( A / 2 ) ) = ( ( log ` ( A / 2 ) ) / ( A / 2 ) ) )
117 75 116 syl 
 |-  ( ph -> ( G ` ( A / 2 ) ) = ( ( log ` ( A / 2 ) ) / ( A / 2 ) ) )
118 111 117 breq12d 
 |-  ( ph -> ( ( G ` ( B / 2 ) ) < ( G ` ( A / 2 ) ) <-> ( ( log ` ( B / 2 ) ) / ( B / 2 ) ) < ( ( log ` ( A / 2 ) ) / ( A / 2 ) ) ) )
119 56 ffvelcdmi 
 |-  ( ( B / 2 ) e. RR+ -> ( G ` ( B / 2 ) ) e. RR )
120 96 119 syl 
 |-  ( ph -> ( G ` ( B / 2 ) ) e. RR )
121 56 ffvelcdmi 
 |-  ( ( A / 2 ) e. RR+ -> ( G ` ( A / 2 ) ) e. RR )
122 75 121 syl 
 |-  ( ph -> ( G ` ( A / 2 ) ) e. RR )
123 9nn 
 |-  9 e. NN
124 4nn 
 |-  4 e. NN
125 nnrp 
 |-  ( 9 e. NN -> 9 e. RR+ )
126 nnrp 
 |-  ( 4 e. NN -> 4 e. RR+ )
127 rpdivcl 
 |-  ( ( 9 e. RR+ /\ 4 e. RR+ ) -> ( 9 / 4 ) e. RR+ )
128 125 126 127 syl2an 
 |-  ( ( 9 e. NN /\ 4 e. NN ) -> ( 9 / 4 ) e. RR+ )
129 123 124 128 mp2an 
 |-  ( 9 / 4 ) e. RR+
130 129 a1i 
 |-  ( ph -> ( 9 / 4 ) e. RR+ )
131 120 122 130 ltmul2d 
 |-  ( ph -> ( ( G ` ( B / 2 ) ) < ( G ` ( A / 2 ) ) <-> ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) < ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) )
132 105 118 131 3bitr2d 
 |-  ( ph -> ( A < B <-> ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) < ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) )
133 132 biimpd 
 |-  ( ph -> ( A < B -> ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) < ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) )
134 66 133 jcad 
 |-  ( ph -> ( A < B -> ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) < ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) /\ ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) < ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) ) )
135 sqrt2re 
 |-  ( sqrt ` 2 ) e. RR
136 remulcl 
 |-  ( ( ( sqrt ` 2 ) e. RR /\ ( G ` ( sqrt ` B ) ) e. RR ) -> ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) e. RR )
137 135 58 136 sylancr 
 |-  ( ph -> ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) e. RR )
138 9re 
 |-  9 e. RR
139 4re 
 |-  4 e. RR
140 4ne0 
 |-  4 =/= 0
141 138 139 140 redivcli 
 |-  ( 9 / 4 ) e. RR
142 remulcl 
 |-  ( ( ( 9 / 4 ) e. RR /\ ( G ` ( B / 2 ) ) e. RR ) -> ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) e. RR )
143 141 120 142 sylancr 
 |-  ( ph -> ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) e. RR )
144 remulcl 
 |-  ( ( ( sqrt ` 2 ) e. RR /\ ( G ` ( sqrt ` A ) ) e. RR ) -> ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) e. RR )
145 135 60 144 sylancr 
 |-  ( ph -> ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) e. RR )
146 remulcl 
 |-  ( ( ( 9 / 4 ) e. RR /\ ( G ` ( A / 2 ) ) e. RR ) -> ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) e. RR )
147 141 122 146 sylancr 
 |-  ( ph -> ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) e. RR )
148 lt2add 
 |-  ( ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) e. RR /\ ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) e. RR ) /\ ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) e. RR /\ ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) e. RR ) ) -> ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) < ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) /\ ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) < ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) -> ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) < ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) ) )
149 137 143 145 147 148 syl22anc 
 |-  ( ph -> ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) < ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) /\ ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) < ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) -> ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) < ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) ) )
150 134 149 syld 
 |-  ( ph -> ( A < B -> ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) < ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) ) )
151 ltmul2 
 |-  ( ( A e. RR /\ B e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( A < B <-> ( 2 x. A ) < ( 2 x. B ) ) )
152 67 68 72 151 syl3anc 
 |-  ( ph -> ( A < B <-> ( 2 x. A ) < ( 2 x. B ) ) )
153 rpmulcl 
 |-  ( ( 2 e. RR+ /\ A e. RR+ ) -> ( 2 x. A ) e. RR+ )
154 61 15 153 sylancr 
 |-  ( ph -> ( 2 x. A ) e. RR+ )
155 154 rpsqrtcld 
 |-  ( ph -> ( sqrt ` ( 2 x. A ) ) e. RR+ )
156 rpmulcl 
 |-  ( ( 2 e. RR+ /\ B e. RR+ ) -> ( 2 x. B ) e. RR+ )
157 61 7 156 sylancr 
 |-  ( ph -> ( 2 x. B ) e. RR+ )
158 157 rpsqrtcld 
 |-  ( ph -> ( sqrt ` ( 2 x. B ) ) e. RR+ )
159 rprege0 
 |-  ( ( sqrt ` ( 2 x. A ) ) e. RR+ -> ( ( sqrt ` ( 2 x. A ) ) e. RR /\ 0 <_ ( sqrt ` ( 2 x. A ) ) ) )
160 rprege0 
 |-  ( ( sqrt ` ( 2 x. B ) ) e. RR+ -> ( ( sqrt ` ( 2 x. B ) ) e. RR /\ 0 <_ ( sqrt ` ( 2 x. B ) ) ) )
161 lt2sq 
 |-  ( ( ( ( sqrt ` ( 2 x. A ) ) e. RR /\ 0 <_ ( sqrt ` ( 2 x. A ) ) ) /\ ( ( sqrt ` ( 2 x. B ) ) e. RR /\ 0 <_ ( sqrt ` ( 2 x. B ) ) ) ) -> ( ( sqrt ` ( 2 x. A ) ) < ( sqrt ` ( 2 x. B ) ) <-> ( ( sqrt ` ( 2 x. A ) ) ^ 2 ) < ( ( sqrt ` ( 2 x. B ) ) ^ 2 ) ) )
162 159 160 161 syl2an 
 |-  ( ( ( sqrt ` ( 2 x. A ) ) e. RR+ /\ ( sqrt ` ( 2 x. B ) ) e. RR+ ) -> ( ( sqrt ` ( 2 x. A ) ) < ( sqrt ` ( 2 x. B ) ) <-> ( ( sqrt ` ( 2 x. A ) ) ^ 2 ) < ( ( sqrt ` ( 2 x. B ) ) ^ 2 ) ) )
163 155 158 162 syl2anc 
 |-  ( ph -> ( ( sqrt ` ( 2 x. A ) ) < ( sqrt ` ( 2 x. B ) ) <-> ( ( sqrt ` ( 2 x. A ) ) ^ 2 ) < ( ( sqrt ` ( 2 x. B ) ) ^ 2 ) ) )
164 154 rprege0d 
 |-  ( ph -> ( ( 2 x. A ) e. RR /\ 0 <_ ( 2 x. A ) ) )
165 resqrtth 
 |-  ( ( ( 2 x. A ) e. RR /\ 0 <_ ( 2 x. A ) ) -> ( ( sqrt ` ( 2 x. A ) ) ^ 2 ) = ( 2 x. A ) )
166 164 165 syl 
 |-  ( ph -> ( ( sqrt ` ( 2 x. A ) ) ^ 2 ) = ( 2 x. A ) )
167 157 rprege0d 
 |-  ( ph -> ( ( 2 x. B ) e. RR /\ 0 <_ ( 2 x. B ) ) )
168 resqrtth 
 |-  ( ( ( 2 x. B ) e. RR /\ 0 <_ ( 2 x. B ) ) -> ( ( sqrt ` ( 2 x. B ) ) ^ 2 ) = ( 2 x. B ) )
169 167 168 syl 
 |-  ( ph -> ( ( sqrt ` ( 2 x. B ) ) ^ 2 ) = ( 2 x. B ) )
170 166 169 breq12d 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. A ) ) ^ 2 ) < ( ( sqrt ` ( 2 x. B ) ) ^ 2 ) <-> ( 2 x. A ) < ( 2 x. B ) ) )
171 163 170 bitr2d 
 |-  ( ph -> ( ( 2 x. A ) < ( 2 x. B ) <-> ( sqrt ` ( 2 x. A ) ) < ( sqrt ` ( 2 x. B ) ) ) )
172 1lt2 
 |-  1 < 2
173 rplogcl 
 |-  ( ( 2 e. RR /\ 1 < 2 ) -> ( log ` 2 ) e. RR+ )
174 69 172 173 mp2an 
 |-  ( log ` 2 ) e. RR+
175 174 a1i 
 |-  ( ph -> ( log ` 2 ) e. RR+ )
176 155 158 175 ltdiv2d 
 |-  ( ph -> ( ( sqrt ` ( 2 x. A ) ) < ( sqrt ` ( 2 x. B ) ) <-> ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) < ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) ) )
177 152 171 176 3bitrd 
 |-  ( ph -> ( A < B <-> ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) < ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) ) )
178 177 biimpd 
 |-  ( ph -> ( A < B -> ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) < ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) ) )
179 150 178 jcad 
 |-  ( ph -> ( A < B -> ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) < ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) /\ ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) < ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) ) ) )
180 137 143 readdcld 
 |-  ( ph -> ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) e. RR )
181 rpre 
 |-  ( ( log ` 2 ) e. RR+ -> ( log ` 2 ) e. RR )
182 174 181 ax-mp 
 |-  ( log ` 2 ) e. RR
183 rerpdivcl 
 |-  ( ( ( log ` 2 ) e. RR /\ ( sqrt ` ( 2 x. B ) ) e. RR+ ) -> ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) e. RR )
184 182 158 183 sylancr 
 |-  ( ph -> ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) e. RR )
185 145 147 readdcld 
 |-  ( ph -> ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) e. RR )
186 rerpdivcl 
 |-  ( ( ( log ` 2 ) e. RR /\ ( sqrt ` ( 2 x. A ) ) e. RR+ ) -> ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) e. RR )
187 182 155 186 sylancr 
 |-  ( ph -> ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) e. RR )
188 lt2add 
 |-  ( ( ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) e. RR /\ ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) e. RR ) /\ ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) e. RR /\ ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) e. RR ) ) -> ( ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) < ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) /\ ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) < ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) ) -> ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) ) < ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) ) ) )
189 180 184 185 187 188 syl22anc 
 |-  ( ph -> ( ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) < ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) /\ ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) < ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) ) -> ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) ) < ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) ) ) )
190 179 189 syld 
 |-  ( ph -> ( A < B -> ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) ) < ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) ) ) )
191 2fveq3 
 |-  ( n = B -> ( G ` ( sqrt ` n ) ) = ( G ` ( sqrt ` B ) ) )
192 191 oveq2d 
 |-  ( n = B -> ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` n ) ) ) = ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) )
193 fvoveq1 
 |-  ( n = B -> ( G ` ( n / 2 ) ) = ( G ` ( B / 2 ) ) )
194 193 oveq2d 
 |-  ( n = B -> ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) = ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) )
195 192 194 oveq12d 
 |-  ( n = B -> ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) = ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) )
196 oveq2 
 |-  ( n = B -> ( 2 x. n ) = ( 2 x. B ) )
197 196 fveq2d 
 |-  ( n = B -> ( sqrt ` ( 2 x. n ) ) = ( sqrt ` ( 2 x. B ) ) )
198 197 oveq2d 
 |-  ( n = B -> ( ( log ` 2 ) / ( sqrt ` ( 2 x. n ) ) ) = ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) )
199 195 198 oveq12d 
 |-  ( n = B -> ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. n ) ) ) ) = ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) ) )
200 ovex 
 |-  ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) ) e. _V
201 199 1 200 fvmpt 
 |-  ( B e. NN -> ( F ` B ) = ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) ) )
202 4 201 syl 
 |-  ( ph -> ( F ` B ) = ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) ) )
203 2fveq3 
 |-  ( n = A -> ( G ` ( sqrt ` n ) ) = ( G ` ( sqrt ` A ) ) )
204 203 oveq2d 
 |-  ( n = A -> ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` n ) ) ) = ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) )
205 fvoveq1 
 |-  ( n = A -> ( G ` ( n / 2 ) ) = ( G ` ( A / 2 ) ) )
206 205 oveq2d 
 |-  ( n = A -> ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) = ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) )
207 204 206 oveq12d 
 |-  ( n = A -> ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) = ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) )
208 oveq2 
 |-  ( n = A -> ( 2 x. n ) = ( 2 x. A ) )
209 208 fveq2d 
 |-  ( n = A -> ( sqrt ` ( 2 x. n ) ) = ( sqrt ` ( 2 x. A ) ) )
210 209 oveq2d 
 |-  ( n = A -> ( ( log ` 2 ) / ( sqrt ` ( 2 x. n ) ) ) = ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) )
211 207 210 oveq12d 
 |-  ( n = A -> ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. n ) ) ) ) = ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) ) )
212 ovex 
 |-  ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) ) e. _V
213 211 1 212 fvmpt 
 |-  ( A e. NN -> ( F ` A ) = ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) ) )
214 3 213 syl 
 |-  ( ph -> ( F ` A ) = ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) ) )
215 202 214 breq12d 
 |-  ( ph -> ( ( F ` B ) < ( F ` A ) <-> ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` B ) ) ) + ( ( 9 / 4 ) x. ( G ` ( B / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. B ) ) ) ) < ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` A ) ) ) + ( ( 9 / 4 ) x. ( G ` ( A / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. A ) ) ) ) ) )
216 190 215 sylibrd 
 |-  ( ph -> ( A < B -> ( F ` B ) < ( F ` A ) ) )