Metamath Proof Explorer


Theorem logdivsqrle

Description: Conditions for ( ( log x ) / ( sqrt x ) ) to be decreasing. (Contributed by Thierry Arnoux, 20-Dec-2021)

Ref Expression
Hypotheses logdivsqrle.a
|- ( ph -> A e. RR+ )
logdivsqrle.b
|- ( ph -> B e. RR+ )
logdivsqrle.1
|- ( ph -> ( exp ` 2 ) <_ A )
logdivsqrle.2
|- ( ph -> A <_ B )
Assertion logdivsqrle
|- ( ph -> ( ( log ` B ) / ( sqrt ` B ) ) <_ ( ( log ` A ) / ( sqrt ` A ) ) )

Proof

Step Hyp Ref Expression
1 logdivsqrle.a
 |-  ( ph -> A e. RR+ )
2 logdivsqrle.b
 |-  ( ph -> B e. RR+ )
3 logdivsqrle.1
 |-  ( ph -> ( exp ` 2 ) <_ A )
4 logdivsqrle.2
 |-  ( ph -> A <_ B )
5 ioorp
 |-  ( 0 (,) +oo ) = RR+
6 5 eqcomi
 |-  RR+ = ( 0 (,) +oo )
7 simpr
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
8 7 relogcld
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
9 7 rpsqrtcld
 |-  ( ( ph /\ x e. RR+ ) -> ( sqrt ` x ) e. RR+ )
10 9 rpred
 |-  ( ( ph /\ x e. RR+ ) -> ( sqrt ` x ) e. RR )
11 rpsqrtcl
 |-  ( x e. RR+ -> ( sqrt ` x ) e. RR+ )
12 rpne0
 |-  ( ( sqrt ` x ) e. RR+ -> ( sqrt ` x ) =/= 0 )
13 11 12 syl
 |-  ( x e. RR+ -> ( sqrt ` x ) =/= 0 )
14 13 adantl
 |-  ( ( ph /\ x e. RR+ ) -> ( sqrt ` x ) =/= 0 )
15 8 10 14 redivcld
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) / ( sqrt ` x ) ) e. RR )
16 15 fmpttd
 |-  ( ph -> ( x e. RR+ |-> ( ( log ` x ) / ( sqrt ` x ) ) ) : RR+ --> RR )
17 rpcn
 |-  ( x e. RR+ -> x e. CC )
18 17 adantl
 |-  ( ( ph /\ x e. RR+ ) -> x e. CC )
19 rpne0
 |-  ( x e. RR+ -> x =/= 0 )
20 19 adantl
 |-  ( ( ph /\ x e. RR+ ) -> x =/= 0 )
21 18 20 logcld
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
22 18 sqrtcld
 |-  ( ( ph /\ x e. RR+ ) -> ( sqrt ` x ) e. CC )
23 21 22 14 divrecd
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) / ( sqrt ` x ) ) = ( ( log ` x ) x. ( 1 / ( sqrt ` x ) ) ) )
24 2cnd
 |-  ( ph -> 2 e. CC )
25 24 adantr
 |-  ( ( ph /\ x e. RR+ ) -> 2 e. CC )
26 2ne0
 |-  2 =/= 0
27 26 a1i
 |-  ( ( ph /\ x e. RR+ ) -> 2 =/= 0 )
28 25 27 reccld
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / 2 ) e. CC )
29 18 20 28 cxpnegd
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^c -u ( 1 / 2 ) ) = ( 1 / ( x ^c ( 1 / 2 ) ) ) )
30 cxpsqrt
 |-  ( x e. CC -> ( x ^c ( 1 / 2 ) ) = ( sqrt ` x ) )
31 18 30 syl
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^c ( 1 / 2 ) ) = ( sqrt ` x ) )
32 31 oveq2d
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / ( x ^c ( 1 / 2 ) ) ) = ( 1 / ( sqrt ` x ) ) )
33 29 32 eqtrd
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^c -u ( 1 / 2 ) ) = ( 1 / ( sqrt ` x ) ) )
34 33 oveq2d
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( x ^c -u ( 1 / 2 ) ) ) = ( ( log ` x ) x. ( 1 / ( sqrt ` x ) ) ) )
35 23 34 eqtr4d
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) / ( sqrt ` x ) ) = ( ( log ` x ) x. ( x ^c -u ( 1 / 2 ) ) ) )
36 35 mpteq2dva
 |-  ( ph -> ( x e. RR+ |-> ( ( log ` x ) / ( sqrt ` x ) ) ) = ( x e. RR+ |-> ( ( log ` x ) x. ( x ^c -u ( 1 / 2 ) ) ) ) )
37 36 oveq2d
 |-  ( ph -> ( RR _D ( x e. RR+ |-> ( ( log ` x ) / ( sqrt ` x ) ) ) ) = ( RR _D ( x e. RR+ |-> ( ( log ` x ) x. ( x ^c -u ( 1 / 2 ) ) ) ) ) )
38 reelprrecn
 |-  RR e. { RR , CC }
39 38 a1i
 |-  ( ph -> RR e. { RR , CC } )
40 7 rpreccld
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / x ) e. RR+ )
41 logf1o
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
42 f1of
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
43 41 42 ax-mp
 |-  log : ( CC \ { 0 } ) --> ran log
44 43 a1i
 |-  ( ph -> log : ( CC \ { 0 } ) --> ran log )
45 17 ssriv
 |-  RR+ C_ CC
46 0nrp
 |-  -. 0 e. RR+
47 ssdifsn
 |-  ( RR+ C_ ( CC \ { 0 } ) <-> ( RR+ C_ CC /\ -. 0 e. RR+ ) )
48 45 46 47 mpbir2an
 |-  RR+ C_ ( CC \ { 0 } )
49 48 a1i
 |-  ( ph -> RR+ C_ ( CC \ { 0 } ) )
50 44 49 feqresmpt
 |-  ( ph -> ( log |` RR+ ) = ( x e. RR+ |-> ( log ` x ) ) )
51 50 oveq2d
 |-  ( ph -> ( RR _D ( log |` RR+ ) ) = ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) )
52 dvrelog
 |-  ( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) )
53 51 52 eqtr3di
 |-  ( ph -> ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) = ( x e. RR+ |-> ( 1 / x ) ) )
54 1cnd
 |-  ( ph -> 1 e. CC )
55 54 halfcld
 |-  ( ph -> ( 1 / 2 ) e. CC )
56 55 negcld
 |-  ( ph -> -u ( 1 / 2 ) e. CC )
57 56 adantr
 |-  ( ( ph /\ x e. RR+ ) -> -u ( 1 / 2 ) e. CC )
58 18 57 cxpcld
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^c -u ( 1 / 2 ) ) e. CC )
59 54 adantr
 |-  ( ( ph /\ x e. RR+ ) -> 1 e. CC )
60 57 59 subcld
 |-  ( ( ph /\ x e. RR+ ) -> ( -u ( 1 / 2 ) - 1 ) e. CC )
61 18 60 cxpcld
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^c ( -u ( 1 / 2 ) - 1 ) ) e. CC )
62 57 61 mulcld
 |-  ( ( ph /\ x e. RR+ ) -> ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) e. CC )
63 dvcxp1
 |-  ( -u ( 1 / 2 ) e. CC -> ( RR _D ( x e. RR+ |-> ( x ^c -u ( 1 / 2 ) ) ) ) = ( x e. RR+ |-> ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) ) )
64 56 63 syl
 |-  ( ph -> ( RR _D ( x e. RR+ |-> ( x ^c -u ( 1 / 2 ) ) ) ) = ( x e. RR+ |-> ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) ) )
65 39 21 40 53 58 62 64 dvmptmul
 |-  ( ph -> ( RR _D ( x e. RR+ |-> ( ( log ` x ) x. ( x ^c -u ( 1 / 2 ) ) ) ) ) = ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) )
66 37 65 eqtrd
 |-  ( ph -> ( RR _D ( x e. RR+ |-> ( ( log ` x ) / ( sqrt ` x ) ) ) ) = ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) )
67 ax-resscn
 |-  RR C_ CC
68 67 a1i
 |-  ( ph -> RR C_ CC )
69 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
70 69 addcn
 |-  + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
71 70 a1i
 |-  ( ph -> + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
72 45 a1i
 |-  ( ph -> RR+ C_ CC )
73 ssid
 |-  CC C_ CC
74 73 a1i
 |-  ( ph -> CC C_ CC )
75 cncfmptc
 |-  ( ( 1 e. CC /\ RR+ C_ CC /\ CC C_ CC ) -> ( x e. RR+ |-> 1 ) e. ( RR+ -cn-> CC ) )
76 54 72 74 75 syl3anc
 |-  ( ph -> ( x e. RR+ |-> 1 ) e. ( RR+ -cn-> CC ) )
77 difss
 |-  ( CC \ { 0 } ) C_ CC
78 cncfmptid
 |-  ( ( RR+ C_ ( CC \ { 0 } ) /\ ( CC \ { 0 } ) C_ CC ) -> ( x e. RR+ |-> x ) e. ( RR+ -cn-> ( CC \ { 0 } ) ) )
79 49 77 78 sylancl
 |-  ( ph -> ( x e. RR+ |-> x ) e. ( RR+ -cn-> ( CC \ { 0 } ) ) )
80 76 79 divcncf
 |-  ( ph -> ( x e. RR+ |-> ( 1 / x ) ) e. ( RR+ -cn-> CC ) )
81 ax-1
 |-  ( x e. RR+ -> ( x e. RR -> x e. RR+ ) )
82 17 81 jca
 |-  ( x e. RR+ -> ( x e. CC /\ ( x e. RR -> x e. RR+ ) ) )
83 eqid
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
84 83 ellogdm
 |-  ( x e. ( CC \ ( -oo (,] 0 ) ) <-> ( x e. CC /\ ( x e. RR -> x e. RR+ ) ) )
85 82 84 sylibr
 |-  ( x e. RR+ -> x e. ( CC \ ( -oo (,] 0 ) ) )
86 85 ssriv
 |-  RR+ C_ ( CC \ ( -oo (,] 0 ) )
87 86 a1i
 |-  ( ph -> RR+ C_ ( CC \ ( -oo (,] 0 ) ) )
88 56 87 cxpcncf1
 |-  ( ph -> ( x e. RR+ |-> ( x ^c -u ( 1 / 2 ) ) ) e. ( RR+ -cn-> CC ) )
89 80 88 mulcncf
 |-  ( ph -> ( x e. RR+ |-> ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) ) e. ( RR+ -cn-> CC ) )
90 cncfmptc
 |-  ( ( -u ( 1 / 2 ) e. CC /\ RR+ C_ CC /\ CC C_ CC ) -> ( x e. RR+ |-> -u ( 1 / 2 ) ) e. ( RR+ -cn-> CC ) )
91 56 72 74 90 syl3anc
 |-  ( ph -> ( x e. RR+ |-> -u ( 1 / 2 ) ) e. ( RR+ -cn-> CC ) )
92 56 54 subcld
 |-  ( ph -> ( -u ( 1 / 2 ) - 1 ) e. CC )
93 92 87 cxpcncf1
 |-  ( ph -> ( x e. RR+ |-> ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) e. ( RR+ -cn-> CC ) )
94 91 93 mulcncf
 |-  ( ph -> ( x e. RR+ |-> ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) ) e. ( RR+ -cn-> CC ) )
95 cncfss
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( RR+ -cn-> RR ) C_ ( RR+ -cn-> CC ) )
96 67 73 95 mp2an
 |-  ( RR+ -cn-> RR ) C_ ( RR+ -cn-> CC )
97 relogcn
 |-  ( log |` RR+ ) e. ( RR+ -cn-> RR )
98 50 97 eqeltrrdi
 |-  ( ph -> ( x e. RR+ |-> ( log ` x ) ) e. ( RR+ -cn-> RR ) )
99 96 98 sselid
 |-  ( ph -> ( x e. RR+ |-> ( log ` x ) ) e. ( RR+ -cn-> CC ) )
100 94 99 mulcncf
 |-  ( ph -> ( x e. RR+ |-> ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) e. ( RR+ -cn-> CC ) )
101 69 71 89 100 cncfmpt2f
 |-  ( ph -> ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) e. ( RR+ -cn-> CC ) )
102 rpre
 |-  ( x e. RR+ -> x e. RR )
103 102 19 rereccld
 |-  ( x e. RR+ -> ( 1 / x ) e. RR )
104 rpge0
 |-  ( x e. RR+ -> 0 <_ x )
105 halfre
 |-  ( 1 / 2 ) e. RR
106 105 renegcli
 |-  -u ( 1 / 2 ) e. RR
107 106 a1i
 |-  ( x e. RR+ -> -u ( 1 / 2 ) e. RR )
108 102 104 107 recxpcld
 |-  ( x e. RR+ -> ( x ^c -u ( 1 / 2 ) ) e. RR )
109 103 108 remulcld
 |-  ( x e. RR+ -> ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) e. RR )
110 1re
 |-  1 e. RR
111 106 110 resubcli
 |-  ( -u ( 1 / 2 ) - 1 ) e. RR
112 111 a1i
 |-  ( x e. RR+ -> ( -u ( 1 / 2 ) - 1 ) e. RR )
113 102 104 112 recxpcld
 |-  ( x e. RR+ -> ( x ^c ( -u ( 1 / 2 ) - 1 ) ) e. RR )
114 107 113 remulcld
 |-  ( x e. RR+ -> ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) e. RR )
115 relogcl
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
116 114 115 remulcld
 |-  ( x e. RR+ -> ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) e. RR )
117 109 116 readdcld
 |-  ( x e. RR+ -> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) e. RR )
118 117 adantl
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) e. RR )
119 118 fmpttd
 |-  ( ph -> ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) : RR+ --> RR )
120 cncffvrn
 |-  ( ( RR C_ CC /\ ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) e. ( RR+ -cn-> CC ) ) -> ( ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) e. ( RR+ -cn-> RR ) <-> ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) : RR+ --> RR ) )
121 120 biimpar
 |-  ( ( ( RR C_ CC /\ ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) e. ( RR+ -cn-> CC ) ) /\ ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) : RR+ --> RR ) -> ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) e. ( RR+ -cn-> RR ) )
122 68 101 119 121 syl21anc
 |-  ( ph -> ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) e. ( RR+ -cn-> RR ) )
123 66 122 eqeltrd
 |-  ( ph -> ( RR _D ( x e. RR+ |-> ( ( log ` x ) / ( sqrt ` x ) ) ) ) e. ( RR+ -cn-> RR ) )
124 66 fveq1d
 |-  ( ph -> ( ( RR _D ( x e. RR+ |-> ( ( log ` x ) / ( sqrt ` x ) ) ) ) ` y ) = ( ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) ` y ) )
125 124 adantr
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( RR _D ( x e. RR+ |-> ( ( log ` x ) / ( sqrt ` x ) ) ) ) ` y ) = ( ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) ` y ) )
126 59 negcld
 |-  ( ( ph /\ x e. RR+ ) -> -u 1 e. CC )
127 cxpadd
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ -u ( 1 / 2 ) e. CC /\ -u 1 e. CC ) -> ( x ^c ( -u ( 1 / 2 ) + -u 1 ) ) = ( ( x ^c -u ( 1 / 2 ) ) x. ( x ^c -u 1 ) ) )
128 18 20 57 126 127 syl211anc
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^c ( -u ( 1 / 2 ) + -u 1 ) ) = ( ( x ^c -u ( 1 / 2 ) ) x. ( x ^c -u 1 ) ) )
129 61 mulid2d
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) = ( x ^c ( -u ( 1 / 2 ) - 1 ) ) )
130 57 59 negsubd
 |-  ( ( ph /\ x e. RR+ ) -> ( -u ( 1 / 2 ) + -u 1 ) = ( -u ( 1 / 2 ) - 1 ) )
131 130 oveq2d
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^c ( -u ( 1 / 2 ) + -u 1 ) ) = ( x ^c ( -u ( 1 / 2 ) - 1 ) ) )
132 129 131 eqtr4d
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) = ( x ^c ( -u ( 1 / 2 ) + -u 1 ) ) )
133 45 40 sselid
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / x ) e. CC )
134 133 58 mulcomd
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) = ( ( x ^c -u ( 1 / 2 ) ) x. ( 1 / x ) ) )
135 cxpneg
 |-  ( ( x e. CC /\ x =/= 0 /\ 1 e. CC ) -> ( x ^c -u 1 ) = ( 1 / ( x ^c 1 ) ) )
136 18 20 59 135 syl3anc
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^c -u 1 ) = ( 1 / ( x ^c 1 ) ) )
137 18 cxp1d
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^c 1 ) = x )
138 137 oveq2d
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / ( x ^c 1 ) ) = ( 1 / x ) )
139 136 138 eqtr2d
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / x ) = ( x ^c -u 1 ) )
140 139 oveq2d
 |-  ( ( ph /\ x e. RR+ ) -> ( ( x ^c -u ( 1 / 2 ) ) x. ( 1 / x ) ) = ( ( x ^c -u ( 1 / 2 ) ) x. ( x ^c -u 1 ) ) )
141 134 140 eqtrd
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) = ( ( x ^c -u ( 1 / 2 ) ) x. ( x ^c -u 1 ) ) )
142 128 132 141 3eqtr4rd
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) = ( 1 x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) )
143 57 61 21 mul32d
 |-  ( ( ph /\ x e. RR+ ) -> ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) = ( ( -u ( 1 / 2 ) x. ( log ` x ) ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) )
144 142 143 oveq12d
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) = ( ( 1 x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) + ( ( -u ( 1 / 2 ) x. ( log ` x ) ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) ) )
145 57 21 mulcld
 |-  ( ( ph /\ x e. RR+ ) -> ( -u ( 1 / 2 ) x. ( log ` x ) ) e. CC )
146 59 145 61 adddird
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` x ) ) ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) = ( ( 1 x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) + ( ( -u ( 1 / 2 ) x. ( log ` x ) ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) ) )
147 144 146 eqtr4d
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) = ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` x ) ) ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) )
148 147 mpteq2dva
 |-  ( ph -> ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) = ( x e. RR+ |-> ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` x ) ) ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) ) )
149 148 fveq1d
 |-  ( ph -> ( ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) ` y ) = ( ( x e. RR+ |-> ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` x ) ) ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) ) ` y ) )
150 149 adantr
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) ` y ) = ( ( x e. RR+ |-> ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` x ) ) ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) ) ` y ) )
151 eqidd
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( x e. RR+ |-> ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` x ) ) ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) ) = ( x e. RR+ |-> ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` x ) ) ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) ) )
152 simpr
 |-  ( ( ( ph /\ y e. ( A (,) B ) ) /\ x = y ) -> x = y )
153 152 fveq2d
 |-  ( ( ( ph /\ y e. ( A (,) B ) ) /\ x = y ) -> ( log ` x ) = ( log ` y ) )
154 153 oveq2d
 |-  ( ( ( ph /\ y e. ( A (,) B ) ) /\ x = y ) -> ( -u ( 1 / 2 ) x. ( log ` x ) ) = ( -u ( 1 / 2 ) x. ( log ` y ) ) )
155 154 oveq2d
 |-  ( ( ( ph /\ y e. ( A (,) B ) ) /\ x = y ) -> ( 1 + ( -u ( 1 / 2 ) x. ( log ` x ) ) ) = ( 1 + ( -u ( 1 / 2 ) x. ( log ` y ) ) ) )
156 152 oveq1d
 |-  ( ( ( ph /\ y e. ( A (,) B ) ) /\ x = y ) -> ( x ^c ( -u ( 1 / 2 ) - 1 ) ) = ( y ^c ( -u ( 1 / 2 ) - 1 ) ) )
157 155 156 oveq12d
 |-  ( ( ( ph /\ y e. ( A (,) B ) ) /\ x = y ) -> ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` x ) ) ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) = ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` y ) ) ) x. ( y ^c ( -u ( 1 / 2 ) - 1 ) ) ) )
158 ioossicc
 |-  ( A (,) B ) C_ ( A [,] B )
159 158 a1i
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
160 6 1 2 fct2relem
 |-  ( ph -> ( A [,] B ) C_ RR+ )
161 159 160 sstrd
 |-  ( ph -> ( A (,) B ) C_ RR+ )
162 161 sselda
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. RR+ )
163 ovexd
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` y ) ) ) x. ( y ^c ( -u ( 1 / 2 ) - 1 ) ) ) e. _V )
164 151 157 162 163 fvmptd
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( x e. RR+ |-> ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` x ) ) ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) ) ` y ) = ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` y ) ) ) x. ( y ^c ( -u ( 1 / 2 ) - 1 ) ) ) )
165 110 a1i
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 1 e. RR )
166 106 a1i
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> -u ( 1 / 2 ) e. RR )
167 162 relogcld
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( log ` y ) e. RR )
168 166 167 remulcld
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( -u ( 1 / 2 ) x. ( log ` y ) ) e. RR )
169 165 168 readdcld
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( 1 + ( -u ( 1 / 2 ) x. ( log ` y ) ) ) e. RR )
170 0red
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 0 e. RR )
171 rpcxpcl
 |-  ( ( y e. RR+ /\ ( -u ( 1 / 2 ) - 1 ) e. RR ) -> ( y ^c ( -u ( 1 / 2 ) - 1 ) ) e. RR+ )
172 162 111 171 sylancl
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( y ^c ( -u ( 1 / 2 ) - 1 ) ) e. RR+ )
173 172 rpred
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( y ^c ( -u ( 1 / 2 ) - 1 ) ) e. RR )
174 172 rpge0d
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 0 <_ ( y ^c ( -u ( 1 / 2 ) - 1 ) ) )
175 2cn
 |-  2 e. CC
176 175 mulid2i
 |-  ( 1 x. 2 ) = 2
177 2re
 |-  2 e. RR
178 177 a1i
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 2 e. RR )
179 178 reefcld
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( exp ` 2 ) e. RR )
180 1 rpred
 |-  ( ph -> A e. RR )
181 180 adantr
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> A e. RR )
182 162 rpred
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. RR )
183 3 adantr
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( exp ` 2 ) <_ A )
184 eliooord
 |-  ( y e. ( A (,) B ) -> ( A < y /\ y < B ) )
185 184 simpld
 |-  ( y e. ( A (,) B ) -> A < y )
186 185 adantl
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> A < y )
187 181 182 186 ltled
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> A <_ y )
188 179 181 182 183 187 letrd
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( exp ` 2 ) <_ y )
189 reeflog
 |-  ( y e. RR+ -> ( exp ` ( log ` y ) ) = y )
190 162 189 syl
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( exp ` ( log ` y ) ) = y )
191 188 190 breqtrrd
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( exp ` 2 ) <_ ( exp ` ( log ` y ) ) )
192 efle
 |-  ( ( 2 e. RR /\ ( log ` y ) e. RR ) -> ( 2 <_ ( log ` y ) <-> ( exp ` 2 ) <_ ( exp ` ( log ` y ) ) ) )
193 177 167 192 sylancr
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( 2 <_ ( log ` y ) <-> ( exp ` 2 ) <_ ( exp ` ( log ` y ) ) ) )
194 191 193 mpbird
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 2 <_ ( log ` y ) )
195 176 194 eqbrtrid
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( 1 x. 2 ) <_ ( log ` y ) )
196 2rp
 |-  2 e. RR+
197 196 a1i
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 2 e. RR+ )
198 165 167 197 lemuldivd
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( 1 x. 2 ) <_ ( log ` y ) <-> 1 <_ ( ( log ` y ) / 2 ) ) )
199 195 198 mpbid
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 1 <_ ( ( log ` y ) / 2 ) )
200 67 167 sselid
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( log ` y ) e. CC )
201 24 adantr
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 2 e. CC )
202 26 a1i
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 2 =/= 0 )
203 200 201 202 divrec2d
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( log ` y ) / 2 ) = ( ( 1 / 2 ) x. ( log ` y ) ) )
204 199 203 breqtrd
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 1 <_ ( ( 1 / 2 ) x. ( log ` y ) ) )
205 55 adantr
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( 1 / 2 ) e. CC )
206 205 200 mulneg1d
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( -u ( 1 / 2 ) x. ( log ` y ) ) = -u ( ( 1 / 2 ) x. ( log ` y ) ) )
207 206 oveq2d
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( 0 - ( -u ( 1 / 2 ) x. ( log ` y ) ) ) = ( 0 - -u ( ( 1 / 2 ) x. ( log ` y ) ) ) )
208 67 170 sselid
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 0 e. CC )
209 205 200 mulcld
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( 1 / 2 ) x. ( log ` y ) ) e. CC )
210 208 209 subnegd
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( 0 - -u ( ( 1 / 2 ) x. ( log ` y ) ) ) = ( 0 + ( ( 1 / 2 ) x. ( log ` y ) ) ) )
211 209 addid2d
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( 0 + ( ( 1 / 2 ) x. ( log ` y ) ) ) = ( ( 1 / 2 ) x. ( log ` y ) ) )
212 207 210 211 3eqtrd
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( 0 - ( -u ( 1 / 2 ) x. ( log ` y ) ) ) = ( ( 1 / 2 ) x. ( log ` y ) ) )
213 204 212 breqtrrd
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 1 <_ ( 0 - ( -u ( 1 / 2 ) x. ( log ` y ) ) ) )
214 leaddsub
 |-  ( ( 1 e. RR /\ ( -u ( 1 / 2 ) x. ( log ` y ) ) e. RR /\ 0 e. RR ) -> ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` y ) ) ) <_ 0 <-> 1 <_ ( 0 - ( -u ( 1 / 2 ) x. ( log ` y ) ) ) ) )
215 165 168 170 214 syl3anc
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` y ) ) ) <_ 0 <-> 1 <_ ( 0 - ( -u ( 1 / 2 ) x. ( log ` y ) ) ) ) )
216 213 215 mpbird
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( 1 + ( -u ( 1 / 2 ) x. ( log ` y ) ) ) <_ 0 )
217 169 170 173 174 216 lemul1ad
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` y ) ) ) x. ( y ^c ( -u ( 1 / 2 ) - 1 ) ) ) <_ ( 0 x. ( y ^c ( -u ( 1 / 2 ) - 1 ) ) ) )
218 45 172 sselid
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( y ^c ( -u ( 1 / 2 ) - 1 ) ) e. CC )
219 218 mul02d
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( 0 x. ( y ^c ( -u ( 1 / 2 ) - 1 ) ) ) = 0 )
220 217 219 breqtrd
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` y ) ) ) x. ( y ^c ( -u ( 1 / 2 ) - 1 ) ) ) <_ 0 )
221 164 220 eqbrtrd
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( x e. RR+ |-> ( ( 1 + ( -u ( 1 / 2 ) x. ( log ` x ) ) ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) ) ` y ) <_ 0 )
222 150 221 eqbrtrd
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( x e. RR+ |-> ( ( ( 1 / x ) x. ( x ^c -u ( 1 / 2 ) ) ) + ( ( -u ( 1 / 2 ) x. ( x ^c ( -u ( 1 / 2 ) - 1 ) ) ) x. ( log ` x ) ) ) ) ` y ) <_ 0 )
223 125 222 eqbrtrd
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( RR _D ( x e. RR+ |-> ( ( log ` x ) / ( sqrt ` x ) ) ) ) ` y ) <_ 0 )
224 6 1 2 16 123 4 223 fdvnegge
 |-  ( ph -> ( ( x e. RR+ |-> ( ( log ` x ) / ( sqrt ` x ) ) ) ` B ) <_ ( ( x e. RR+ |-> ( ( log ` x ) / ( sqrt ` x ) ) ) ` A ) )
225 eqidd
 |-  ( ph -> ( x e. RR+ |-> ( ( log ` x ) / ( sqrt ` x ) ) ) = ( x e. RR+ |-> ( ( log ` x ) / ( sqrt ` x ) ) ) )
226 simpr
 |-  ( ( ph /\ x = B ) -> x = B )
227 226 fveq2d
 |-  ( ( ph /\ x = B ) -> ( log ` x ) = ( log ` B ) )
228 226 fveq2d
 |-  ( ( ph /\ x = B ) -> ( sqrt ` x ) = ( sqrt ` B ) )
229 227 228 oveq12d
 |-  ( ( ph /\ x = B ) -> ( ( log ` x ) / ( sqrt ` x ) ) = ( ( log ` B ) / ( sqrt ` B ) ) )
230 ovex
 |-  ( ( log ` B ) / ( sqrt ` B ) ) e. _V
231 230 a1i
 |-  ( ph -> ( ( log ` B ) / ( sqrt ` B ) ) e. _V )
232 225 229 2 231 fvmptd
 |-  ( ph -> ( ( x e. RR+ |-> ( ( log ` x ) / ( sqrt ` x ) ) ) ` B ) = ( ( log ` B ) / ( sqrt ` B ) ) )
233 simpr
 |-  ( ( ph /\ x = A ) -> x = A )
234 233 fveq2d
 |-  ( ( ph /\ x = A ) -> ( log ` x ) = ( log ` A ) )
235 233 fveq2d
 |-  ( ( ph /\ x = A ) -> ( sqrt ` x ) = ( sqrt ` A ) )
236 234 235 oveq12d
 |-  ( ( ph /\ x = A ) -> ( ( log ` x ) / ( sqrt ` x ) ) = ( ( log ` A ) / ( sqrt ` A ) ) )
237 ovex
 |-  ( ( log ` A ) / ( sqrt ` A ) ) e. _V
238 237 a1i
 |-  ( ph -> ( ( log ` A ) / ( sqrt ` A ) ) e. _V )
239 225 236 1 238 fvmptd
 |-  ( ph -> ( ( x e. RR+ |-> ( ( log ` x ) / ( sqrt ` x ) ) ) ` A ) = ( ( log ` A ) / ( sqrt ` A ) ) )
240 224 232 239 3brtr3d
 |-  ( ph -> ( ( log ` B ) / ( sqrt ` B ) ) <_ ( ( log ` A ) / ( sqrt ` A ) ) )