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 dvrelog 
 |-  ( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) )
42 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
43 f1of 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
44 42 43 ax-mp 
 |-  log : ( CC \ { 0 } ) --> ran log
45 44 a1i 
 |-  ( ph -> log : ( CC \ { 0 } ) --> ran log )
46 17 ssriv 
 |-  RR+ C_ CC
47 0nrp 
 |-  -. 0 e. RR+
48 ssdifsn 
 |-  ( RR+ C_ ( CC \ { 0 } ) <-> ( RR+ C_ CC /\ -. 0 e. RR+ ) )
49 46 47 48 mpbir2an 
 |-  RR+ C_ ( CC \ { 0 } )
50 49 a1i 
 |-  ( ph -> RR+ C_ ( CC \ { 0 } ) )
51 45 50 feqresmpt 
 |-  ( ph -> ( log |` RR+ ) = ( x e. RR+ |-> ( log ` x ) ) )
52 51 oveq2d 
 |-  ( ph -> ( RR _D ( log |` RR+ ) ) = ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) )
53 41 52 syl5reqr 
 |-  ( 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 46 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 50 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 51 97 eqeltrrdi 
 |-  ( ph -> ( x e. RR+ |-> ( log ` x ) ) e. ( RR+ -cn-> RR ) )
99 96 98 sseldi 
 |-  ( 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 46 40 sseldi 
 |-  ( ( 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 sseldi 
 |-  ( ( 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 sseldi 
 |-  ( ( 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 46 172 sseldi 
 |-  ( ( 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 ) ) )