Metamath Proof Explorer

Theorem logccv

Description: The natural logarithm function on the reals is a strictly concave function. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Assertion logccv 
|- ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( T x. ( log ` A ) ) + ( ( 1 - T ) x. ( log ` B ) ) ) < ( log ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> A e. RR+ )
2 1 rpred 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> A e. RR )
3 simpl2 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> B e. RR+ )
4 3 rpred 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> B e. RR )
5 simpl3 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> A < B )
6 1 rpgt0d 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> 0 < A )
7 4 ltpnfd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> B < +oo )
8 0xr 
 |-  0 e. RR*
9 pnfxr 
 |-  +oo e. RR*
10 iccssioo 
 |-  ( ( ( 0 e. RR* /\ +oo e. RR* ) /\ ( 0 < A /\ B < +oo ) ) -> ( A [,] B ) C_ ( 0 (,) +oo ) )
11 8 9 10 mpanl12 
 |-  ( ( 0 < A /\ B < +oo ) -> ( A [,] B ) C_ ( 0 (,) +oo ) )
12 6 7 11 syl2anc 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( A [,] B ) C_ ( 0 (,) +oo ) )
13 ioorp 
 |-  ( 0 (,) +oo ) = RR+
14 12 13 sseqtrdi 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( A [,] B ) C_ RR+ )
15 14 sselda 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ x e. ( A [,] B ) ) -> x e. RR+ )
16 15 relogcld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ x e. ( A [,] B ) ) -> ( log ` x ) e. RR )
17 16 renegcld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ x e. ( A [,] B ) ) -> -u ( log ` x ) e. RR )
18 17 fmpttd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( x e. ( A [,] B ) |-> -u ( log ` x ) ) : ( A [,] B ) --> RR )
19 ax-resscn 
 |-  RR C_ CC
20 14 resabs1d 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( log |` RR+ ) |` ( A [,] B ) ) = ( log |` ( A [,] B ) ) )
21 ssid 
 |-  CC C_ CC
22 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( RR+ -cn-> RR ) C_ ( RR+ -cn-> CC ) )
23 19 21 22 mp2an 
 |-  ( RR+ -cn-> RR ) C_ ( RR+ -cn-> CC )
24 relogcn 
 |-  ( log |` RR+ ) e. ( RR+ -cn-> RR )
25 23 24 sselii 
 |-  ( log |` RR+ ) e. ( RR+ -cn-> CC )
26 rescncf 
 |-  ( ( A [,] B ) C_ RR+ -> ( ( log |` RR+ ) e. ( RR+ -cn-> CC ) -> ( ( log |` RR+ ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
27 14 25 26 mpisyl 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( log |` RR+ ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
28 20 27 eqeltrrd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( log |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
29 fvres 
 |-  ( x e. ( A [,] B ) -> ( ( log |` ( A [,] B ) ) ` x ) = ( log ` x ) )
30 29 negeqd 
 |-  ( x e. ( A [,] B ) -> -u ( ( log |` ( A [,] B ) ) ` x ) = -u ( log ` x ) )
31 30 mpteq2ia 
 |-  ( x e. ( A [,] B ) |-> -u ( ( log |` ( A [,] B ) ) ` x ) ) = ( x e. ( A [,] B ) |-> -u ( log ` x ) )
32 31 eqcomi 
 |-  ( x e. ( A [,] B ) |-> -u ( log ` x ) ) = ( x e. ( A [,] B ) |-> -u ( ( log |` ( A [,] B ) ) ` x ) )
33 32 negfcncf 
 |-  ( ( log |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) -> ( x e. ( A [,] B ) |-> -u ( log ` x ) ) e. ( ( A [,] B ) -cn-> CC ) )
34 28 33 syl 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( x e. ( A [,] B ) |-> -u ( log ` x ) ) e. ( ( A [,] B ) -cn-> CC ) )
35 cncffvrn 
 |-  ( ( RR C_ CC /\ ( x e. ( A [,] B ) |-> -u ( log ` x ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) e. ( ( A [,] B ) -cn-> RR ) <-> ( x e. ( A [,] B ) |-> -u ( log ` x ) ) : ( A [,] B ) --> RR ) )
36 19 34 35 sylancr 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) e. ( ( A [,] B ) -cn-> RR ) <-> ( x e. ( A [,] B ) |-> -u ( log ` x ) ) : ( A [,] B ) --> RR ) )
37 18 36 mpbird 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( x e. ( A [,] B ) |-> -u ( log ` x ) ) e. ( ( A [,] B ) -cn-> RR ) )
38 ioossre 
 |-  ( A (,) B ) C_ RR
39 ltso 
 |-  < Or RR
40 soss 
 |-  ( ( A (,) B ) C_ RR -> ( < Or RR -> < Or ( A (,) B ) ) )
41 38 39 40 mp2 
 |-  < Or ( A (,) B )
42 41 a1i 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> < Or ( A (,) B ) )
43 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
44 43 14 sstrid 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( A (,) B ) C_ RR+ )
45 44 sselda 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ x e. ( A (,) B ) ) -> x e. RR+ )
46 45 rprecred 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ x e. ( A (,) B ) ) -> ( 1 / x ) e. RR )
47 46 renegcld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ x e. ( A (,) B ) ) -> -u ( 1 / x ) e. RR )
48 47 fmpttd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) : ( A (,) B ) --> RR )
49 48 frnd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) C_ RR )
50 soss 
 |-  ( ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) C_ RR -> ( < Or RR -> < Or ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ) )
51 49 39 50 mpisyl 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> < Or ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) )
52 sopo 
 |-  ( < Or ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) -> < Po ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) )
53 51 52 syl 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> < Po ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) )
54 negex 
 |-  -u ( 1 / x ) e. _V
55 eqid 
 |-  ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) = ( x e. ( A (,) B ) |-> -u ( 1 / x ) )
56 54 55 fnmpti 
 |-  ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) Fn ( A (,) B )
57 dffn4 
 |-  ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) Fn ( A (,) B ) <-> ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) : ( A (,) B ) -onto-> ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) )
58 56 57 mpbi 
 |-  ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) : ( A (,) B ) -onto-> ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) )
59 58 a1i 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) : ( A (,) B ) -onto-> ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) )
60 44 sselda 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ z e. ( A (,) B ) ) -> z e. RR+ )
61 60 adantrl 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ ( y e. ( A (,) B ) /\ z e. ( A (,) B ) ) ) -> z e. RR+ )
62 61 rprecred 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ ( y e. ( A (,) B ) /\ z e. ( A (,) B ) ) ) -> ( 1 / z ) e. RR )
63 44 sselda 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ y e. ( A (,) B ) ) -> y e. RR+ )
64 63 adantrr 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ ( y e. ( A (,) B ) /\ z e. ( A (,) B ) ) ) -> y e. RR+ )
65 64 rprecred 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ ( y e. ( A (,) B ) /\ z e. ( A (,) B ) ) ) -> ( 1 / y ) e. RR )
66 62 65 ltnegd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ ( y e. ( A (,) B ) /\ z e. ( A (,) B ) ) ) -> ( ( 1 / z ) < ( 1 / y ) <-> -u ( 1 / y ) < -u ( 1 / z ) ) )
67 64 61 ltrecd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ ( y e. ( A (,) B ) /\ z e. ( A (,) B ) ) ) -> ( y < z <-> ( 1 / z ) < ( 1 / y ) ) )
68 oveq2 
 |-  ( x = y -> ( 1 / x ) = ( 1 / y ) )
69 68 negeqd 
 |-  ( x = y -> -u ( 1 / x ) = -u ( 1 / y ) )
70 negex 
 |-  -u ( 1 / y ) e. _V
71 69 55 70 fvmpt 
 |-  ( y e. ( A (,) B ) -> ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ` y ) = -u ( 1 / y ) )
72 oveq2 
 |-  ( x = z -> ( 1 / x ) = ( 1 / z ) )
73 72 negeqd 
 |-  ( x = z -> -u ( 1 / x ) = -u ( 1 / z ) )
74 negex 
 |-  -u ( 1 / z ) e. _V
75 73 55 74 fvmpt 
 |-  ( z e. ( A (,) B ) -> ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ` z ) = -u ( 1 / z ) )
76 71 75 breqan12d 
 |-  ( ( y e. ( A (,) B ) /\ z e. ( A (,) B ) ) -> ( ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ` y ) < ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ` z ) <-> -u ( 1 / y ) < -u ( 1 / z ) ) )
77 76 adantl 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ ( y e. ( A (,) B ) /\ z e. ( A (,) B ) ) ) -> ( ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ` y ) < ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ` z ) <-> -u ( 1 / y ) < -u ( 1 / z ) ) )
78 66 67 77 3bitr4d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ ( y e. ( A (,) B ) /\ z e. ( A (,) B ) ) ) -> ( y < z <-> ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ` y ) < ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ` z ) ) )
79 78 biimpd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ ( y e. ( A (,) B ) /\ z e. ( A (,) B ) ) ) -> ( y < z -> ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ` y ) < ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ` z ) ) )
80 79 ralrimivva 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> A. y e. ( A (,) B ) A. z e. ( A (,) B ) ( y < z -> ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ` y ) < ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ` z ) ) )
81 soisoi 
 |-  ( ( ( < Or ( A (,) B ) /\ < Po ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ) /\ ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) : ( A (,) B ) -onto-> ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) /\ A. y e. ( A (,) B ) A. z e. ( A (,) B ) ( y < z -> ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ` y ) < ( ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ` z ) ) ) ) -> ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) Isom < , < ( ( A (,) B ) , ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ) )
82 42 53 59 80 81 syl22anc 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) Isom < , < ( ( A (,) B ) , ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ) )
83 reelprrecn 
 |-  RR e. { RR , CC }
84 83 a1i 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> RR e. { RR , CC } )
85 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
86 85 adantl 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ x e. RR+ ) -> ( log ` x ) e. RR )
87 86 recnd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ x e. RR+ ) -> ( log ` x ) e. CC )
88 87 negcld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ x e. RR+ ) -> -u ( log ` x ) e. CC )
89 54 a1i 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ x e. RR+ ) -> -u ( 1 / x ) e. _V )
90 ovexd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) /\ x e. RR+ ) -> ( 1 / x ) e. _V )
91 relogf1o 
 |-  ( log |` RR+ ) : RR+ -1-1-onto-> RR
92 f1of 
 |-  ( ( log |` RR+ ) : RR+ -1-1-onto-> RR -> ( log |` RR+ ) : RR+ --> RR )
93 91 92 mp1i 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( log |` RR+ ) : RR+ --> RR )
94 93 feqmptd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( log |` RR+ ) = ( x e. RR+ |-> ( ( log |` RR+ ) ` x ) ) )
95 fvres 
 |-  ( x e. RR+ -> ( ( log |` RR+ ) ` x ) = ( log ` x ) )
96 95 mpteq2ia 
 |-  ( x e. RR+ |-> ( ( log |` RR+ ) ` x ) ) = ( x e. RR+ |-> ( log ` x ) )
97 94 96 eqtrdi 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( log |` RR+ ) = ( x e. RR+ |-> ( log ` x ) ) )
98 97 oveq2d 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( RR _D ( log |` RR+ ) ) = ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) )
99 dvrelog 
 |-  ( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) )
100 98 99 eqtr3di 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) = ( x e. RR+ |-> ( 1 / x ) ) )
101 84 87 90 100 dvmptneg 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( RR _D ( x e. RR+ |-> -u ( log ` x ) ) ) = ( x e. RR+ |-> -u ( 1 / x ) ) )
102 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
103 102 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
104 iccntr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
105 2 4 104 syl2anc 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
106 84 88 89 101 14 103 102 105 dvmptres2 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( RR _D ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ) = ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) )
107 isoeq1 
 |-  ( ( RR _D ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ) = ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) -> ( ( RR _D ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ) Isom < , < ( ( A (,) B ) , ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ) <-> ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) Isom < , < ( ( A (,) B ) , ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ) ) )
108 106 107 syl 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( RR _D ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ) Isom < , < ( ( A (,) B ) , ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ) <-> ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) Isom < , < ( ( A (,) B ) , ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ) ) )
109 82 108 mpbird 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( RR _D ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ) Isom < , < ( ( A (,) B ) , ran ( x e. ( A (,) B ) |-> -u ( 1 / x ) ) ) )
110 simpr 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> T e. ( 0 (,) 1 ) )
111 eqid 
 |-  ( ( T x. A ) + ( ( 1 - T ) x. B ) ) = ( ( T x. A ) + ( ( 1 - T ) x. B ) )
112 2 4 5 37 109 110 111 dvcvx 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) < ( ( T x. ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` A ) ) + ( ( 1 - T ) x. ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` B ) ) ) )
113 ax-1cn 
 |-  1 e. CC
114 elioore 
 |-  ( T e. ( 0 (,) 1 ) -> T e. RR )
115 114 adantl 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> T e. RR )
116 115 recnd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> T e. CC )
117 nncan 
 |-  ( ( 1 e. CC /\ T e. CC ) -> ( 1 - ( 1 - T ) ) = T )
118 113 116 117 sylancr 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( 1 - ( 1 - T ) ) = T )
119 118 oveq1d 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( 1 - ( 1 - T ) ) x. A ) = ( T x. A ) )
120 119 oveq1d 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( ( 1 - ( 1 - T ) ) x. A ) + ( ( 1 - T ) x. B ) ) = ( ( T x. A ) + ( ( 1 - T ) x. B ) ) )
121 ioossicc 
 |-  ( 0 (,) 1 ) C_ ( 0 [,] 1 )
122 121 110 sselid 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> T e. ( 0 [,] 1 ) )
123 iirev 
 |-  ( T e. ( 0 [,] 1 ) -> ( 1 - T ) e. ( 0 [,] 1 ) )
124 122 123 syl 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( 1 - T ) e. ( 0 [,] 1 ) )
125 lincmb01cmp 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( 1 - T ) e. ( 0 [,] 1 ) ) -> ( ( ( 1 - ( 1 - T ) ) x. A ) + ( ( 1 - T ) x. B ) ) e. ( A [,] B ) )
126 2 4 5 124 125 syl31anc 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( ( 1 - ( 1 - T ) ) x. A ) + ( ( 1 - T ) x. B ) ) e. ( A [,] B ) )
127 120 126 eqeltrrd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( T x. A ) + ( ( 1 - T ) x. B ) ) e. ( A [,] B ) )
128 fveq2 
 |-  ( x = ( ( T x. A ) + ( ( 1 - T ) x. B ) ) -> ( log ` x ) = ( log ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) )
129 128 negeqd 
 |-  ( x = ( ( T x. A ) + ( ( 1 - T ) x. B ) ) -> -u ( log ` x ) = -u ( log ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) )
130 eqid 
 |-  ( x e. ( A [,] B ) |-> -u ( log ` x ) ) = ( x e. ( A [,] B ) |-> -u ( log ` x ) )
131 negex 
 |-  -u ( log ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) e. _V
132 129 130 131 fvmpt 
 |-  ( ( ( T x. A ) + ( ( 1 - T ) x. B ) ) e. ( A [,] B ) -> ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) = -u ( log ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) )
133 127 132 syl 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) = -u ( log ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) )
134 1 rpxrd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> A e. RR* )
135 3 rpxrd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> B e. RR* )
136 2 4 5 ltled 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> A <_ B )
137 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
138 134 135 136 137 syl3anc 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> A e. ( A [,] B ) )
139 fveq2 
 |-  ( x = A -> ( log ` x ) = ( log ` A ) )
140 139 negeqd 
 |-  ( x = A -> -u ( log ` x ) = -u ( log ` A ) )
141 negex 
 |-  -u ( log ` A ) e. _V
142 140 130 141 fvmpt 
 |-  ( A e. ( A [,] B ) -> ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` A ) = -u ( log ` A ) )
143 138 142 syl 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` A ) = -u ( log ` A ) )
144 143 oveq2d 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( T x. ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` A ) ) = ( T x. -u ( log ` A ) ) )
145 1 relogcld 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( log ` A ) e. RR )
146 145 recnd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( log ` A ) e. CC )
147 116 146 mulneg2d 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( T x. -u ( log ` A ) ) = -u ( T x. ( log ` A ) ) )
148 144 147 eqtrd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( T x. ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` A ) ) = -u ( T x. ( log ` A ) ) )
149 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
150 134 135 136 149 syl3anc 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> B e. ( A [,] B ) )
151 fveq2 
 |-  ( x = B -> ( log ` x ) = ( log ` B ) )
152 151 negeqd 
 |-  ( x = B -> -u ( log ` x ) = -u ( log ` B ) )
153 negex 
 |-  -u ( log ` B ) e. _V
154 152 130 153 fvmpt 
 |-  ( B e. ( A [,] B ) -> ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` B ) = -u ( log ` B ) )
155 150 154 syl 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` B ) = -u ( log ` B ) )
156 155 oveq2d 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( 1 - T ) x. ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` B ) ) = ( ( 1 - T ) x. -u ( log ` B ) ) )
157 1re 
 |-  1 e. RR
158 resubcl 
 |-  ( ( 1 e. RR /\ T e. RR ) -> ( 1 - T ) e. RR )
159 157 115 158 sylancr 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( 1 - T ) e. RR )
160 159 recnd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( 1 - T ) e. CC )
161 3 relogcld 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( log ` B ) e. RR )
162 161 recnd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( log ` B ) e. CC )
163 160 162 mulneg2d 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( 1 - T ) x. -u ( log ` B ) ) = -u ( ( 1 - T ) x. ( log ` B ) ) )
164 156 163 eqtrd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( 1 - T ) x. ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` B ) ) = -u ( ( 1 - T ) x. ( log ` B ) ) )
165 148 164 oveq12d 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( T x. ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` A ) ) + ( ( 1 - T ) x. ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` B ) ) ) = ( -u ( T x. ( log ` A ) ) + -u ( ( 1 - T ) x. ( log ` B ) ) ) )
166 115 145 remulcld 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( T x. ( log ` A ) ) e. RR )
167 166 recnd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( T x. ( log ` A ) ) e. CC )
168 159 161 remulcld 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( 1 - T ) x. ( log ` B ) ) e. RR )
169 168 recnd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( 1 - T ) x. ( log ` B ) ) e. CC )
170 167 169 negdid 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> -u ( ( T x. ( log ` A ) ) + ( ( 1 - T ) x. ( log ` B ) ) ) = ( -u ( T x. ( log ` A ) ) + -u ( ( 1 - T ) x. ( log ` B ) ) ) )
171 165 170 eqtr4d 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( T x. ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` A ) ) + ( ( 1 - T ) x. ( ( x e. ( A [,] B ) |-> -u ( log ` x ) ) ` B ) ) ) = -u ( ( T x. ( log ` A ) ) + ( ( 1 - T ) x. ( log ` B ) ) ) )
172 112 133 171 3brtr3d 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> -u ( log ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) < -u ( ( T x. ( log ` A ) ) + ( ( 1 - T ) x. ( log ` B ) ) ) )
173 166 168 readdcld 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( T x. ( log ` A ) ) + ( ( 1 - T ) x. ( log ` B ) ) ) e. RR )
174 14 127 sseldd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( T x. A ) + ( ( 1 - T ) x. B ) ) e. RR+ )
175 174 relogcld 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( log ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) e. RR )
176 173 175 ltnegd 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( ( T x. ( log ` A ) ) + ( ( 1 - T ) x. ( log ` B ) ) ) < ( log ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) <-> -u ( log ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) < -u ( ( T x. ( log ` A ) ) + ( ( 1 - T ) x. ( log ` B ) ) ) ) )
177 172 176 mpbird 
 |-  ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( T x. ( log ` A ) ) + ( ( 1 - T ) x. ( log ` B ) ) ) < ( log ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) )