Metamath Proof Explorer

Theorem efcvx

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

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

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> A e. RR )
2 simpl2 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> B e. RR )
3 simpl3 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> A < B )
4 reeff1o 
 |-  ( exp |` RR ) : RR -1-1-onto-> RR+
5 f1of 
 |-  ( ( exp |` RR ) : RR -1-1-onto-> RR+ -> ( exp |` RR ) : RR --> RR+ )
6 4 5 ax-mp 
 |-  ( exp |` RR ) : RR --> RR+
7 rpssre 
 |-  RR+ C_ RR
8 fss 
 |-  ( ( ( exp |` RR ) : RR --> RR+ /\ RR+ C_ RR ) -> ( exp |` RR ) : RR --> RR )
9 6 7 8 mp2an 
 |-  ( exp |` RR ) : RR --> RR
10 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
11 1 2 10 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( A [,] B ) C_ RR )
12 fssres2 
 |-  ( ( ( exp |` RR ) : RR --> RR /\ ( A [,] B ) C_ RR ) -> ( exp |` ( A [,] B ) ) : ( A [,] B ) --> RR )
13 9 11 12 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( exp |` ( A [,] B ) ) : ( A [,] B ) --> RR )
14 ax-resscn 
 |-  RR C_ CC
15 11 14 sstrdi 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( A [,] B ) C_ CC )
16 efcn 
 |-  exp e. ( CC -cn-> CC )
17 rescncf 
 |-  ( ( A [,] B ) C_ CC -> ( exp e. ( CC -cn-> CC ) -> ( exp |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
18 15 16 17 mpisyl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( exp |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
19 cncfcdm 
 |-  ( ( RR C_ CC /\ ( exp |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( ( exp |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) <-> ( exp |` ( A [,] B ) ) : ( A [,] B ) --> RR ) )
20 14 18 19 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( exp |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) <-> ( exp |` ( A [,] B ) ) : ( A [,] B ) --> RR ) )
21 13 20 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( exp |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
22 reefiso 
 |-  ( exp |` RR ) Isom < , < ( RR , RR+ )
23 22 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( exp |` RR ) Isom < , < ( RR , RR+ ) )
24 ioossre 
 |-  ( A (,) B ) C_ RR
25 24 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( A (,) B ) C_ RR )
26 eqidd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( exp |` RR ) " ( A (,) B ) ) = ( ( exp |` RR ) " ( A (,) B ) ) )
27 isores3 
 |-  ( ( ( exp |` RR ) Isom < , < ( RR , RR+ ) /\ ( A (,) B ) C_ RR /\ ( ( exp |` RR ) " ( A (,) B ) ) = ( ( exp |` RR ) " ( A (,) B ) ) ) -> ( ( exp |` RR ) |` ( A (,) B ) ) Isom < , < ( ( A (,) B ) , ( ( exp |` RR ) " ( A (,) B ) ) ) )
28 23 25 26 27 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( exp |` RR ) |` ( A (,) B ) ) Isom < , < ( ( A (,) B ) , ( ( exp |` RR ) " ( A (,) B ) ) ) )
29 ssid 
 |-  RR C_ RR
30 fss 
 |-  ( ( ( exp |` RR ) : RR --> RR /\ RR C_ CC ) -> ( exp |` RR ) : RR --> CC )
31 9 14 30 mp2an 
 |-  ( exp |` RR ) : RR --> CC
32 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
33 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
34 32 33 dvres 
 |-  ( ( ( RR C_ CC /\ ( exp |` RR ) : RR --> CC ) /\ ( RR C_ RR /\ ( A [,] B ) C_ RR ) ) -> ( RR _D ( ( exp |` RR ) |` ( A [,] B ) ) ) = ( ( RR _D ( exp |` RR ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) )
35 14 31 34 mpanl12 
 |-  ( ( RR C_ RR /\ ( A [,] B ) C_ RR ) -> ( RR _D ( ( exp |` RR ) |` ( A [,] B ) ) ) = ( ( RR _D ( exp |` RR ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) )
36 29 11 35 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( RR _D ( ( exp |` RR ) |` ( A [,] B ) ) ) = ( ( RR _D ( exp |` RR ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) )
37 11 resabs1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( exp |` RR ) |` ( A [,] B ) ) = ( exp |` ( A [,] B ) ) )
38 37 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( RR _D ( ( exp |` RR ) |` ( A [,] B ) ) ) = ( RR _D ( exp |` ( A [,] B ) ) ) )
39 reelprrecn 
 |-  RR e. { RR , CC }
40 eff 
 |-  exp : CC --> CC
41 ssid 
 |-  CC C_ CC
42 dvef 
 |-  ( CC _D exp ) = exp
43 42 dmeqi 
 |-  dom ( CC _D exp ) = dom exp
44 40 fdmi 
 |-  dom exp = CC
45 43 44 eqtri 
 |-  dom ( CC _D exp ) = CC
46 14 45 sseqtrri 
 |-  RR C_ dom ( CC _D exp )
47 dvres3 
 |-  ( ( ( RR e. { RR , CC } /\ exp : CC --> CC ) /\ ( CC C_ CC /\ RR C_ dom ( CC _D exp ) ) ) -> ( RR _D ( exp |` RR ) ) = ( ( CC _D exp ) |` RR ) )
48 39 40 41 46 47 mp4an 
 |-  ( RR _D ( exp |` RR ) ) = ( ( CC _D exp ) |` RR )
49 42 reseq1i 
 |-  ( ( CC _D exp ) |` RR ) = ( exp |` RR )
50 48 49 eqtri 
 |-  ( RR _D ( exp |` RR ) ) = ( exp |` RR )
51 50 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( RR _D ( exp |` RR ) ) = ( exp |` RR ) )
52 iccntr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
53 1 2 52 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
54 51 53 reseq12d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( RR _D ( exp |` RR ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) = ( ( exp |` RR ) |` ( A (,) B ) ) )
55 36 38 54 3eqtr3d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( RR _D ( exp |` ( A [,] B ) ) ) = ( ( exp |` RR ) |` ( A (,) B ) ) )
56 isoeq1 
 |-  ( ( RR _D ( exp |` ( A [,] B ) ) ) = ( ( exp |` RR ) |` ( A (,) B ) ) -> ( ( RR _D ( exp |` ( A [,] B ) ) ) Isom < , < ( ( A (,) B ) , ( ( exp |` RR ) " ( A (,) B ) ) ) <-> ( ( exp |` RR ) |` ( A (,) B ) ) Isom < , < ( ( A (,) B ) , ( ( exp |` RR ) " ( A (,) B ) ) ) ) )
57 55 56 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( RR _D ( exp |` ( A [,] B ) ) ) Isom < , < ( ( A (,) B ) , ( ( exp |` RR ) " ( A (,) B ) ) ) <-> ( ( exp |` RR ) |` ( A (,) B ) ) Isom < , < ( ( A (,) B ) , ( ( exp |` RR ) " ( A (,) B ) ) ) ) )
58 28 57 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( RR _D ( exp |` ( A [,] B ) ) ) Isom < , < ( ( A (,) B ) , ( ( exp |` RR ) " ( A (,) B ) ) ) )
59 simpr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> T e. ( 0 (,) 1 ) )
60 eqid 
 |-  ( ( T x. A ) + ( ( 1 - T ) x. B ) ) = ( ( T x. A ) + ( ( 1 - T ) x. B ) )
61 1 2 3 21 58 59 60 dvcvx 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( exp |` ( A [,] B ) ) ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) < ( ( T x. ( ( exp |` ( A [,] B ) ) ` A ) ) + ( ( 1 - T ) x. ( ( exp |` ( A [,] B ) ) ` B ) ) ) )
62 ax-1cn 
 |-  1 e. CC
63 ioossre 
 |-  ( 0 (,) 1 ) C_ RR
64 63 59 sselid 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> T e. RR )
65 64 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> T e. CC )
66 nncan 
 |-  ( ( 1 e. CC /\ T e. CC ) -> ( 1 - ( 1 - T ) ) = T )
67 62 65 66 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( 1 - ( 1 - T ) ) = T )
68 67 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( 1 - ( 1 - T ) ) x. A ) = ( T x. A ) )
69 68 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 ) ) )
70 ioossicc 
 |-  ( 0 (,) 1 ) C_ ( 0 [,] 1 )
71 70 59 sselid 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> T e. ( 0 [,] 1 ) )
72 iirev 
 |-  ( T e. ( 0 [,] 1 ) -> ( 1 - T ) e. ( 0 [,] 1 ) )
73 71 72 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( 1 - T ) e. ( 0 [,] 1 ) )
74 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 ) )
75 73 74 syldan 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( ( 1 - ( 1 - T ) ) x. A ) + ( ( 1 - T ) x. B ) ) e. ( A [,] B ) )
76 69 75 eqeltrrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( T x. A ) + ( ( 1 - T ) x. B ) ) e. ( A [,] B ) )
77 76 fvresd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( exp |` ( A [,] B ) ) ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) = ( exp ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) )
78 1 rexrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> A e. RR* )
79 2 rexrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> B e. RR* )
80 1 2 3 ltled 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> A <_ B )
81 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
82 78 79 80 81 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> A e. ( A [,] B ) )
83 82 fvresd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( exp |` ( A [,] B ) ) ` A ) = ( exp ` A ) )
84 83 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( T x. ( ( exp |` ( A [,] B ) ) ` A ) ) = ( T x. ( exp ` A ) ) )
85 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
86 78 79 80 85 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> B e. ( A [,] B ) )
87 86 fvresd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( exp |` ( A [,] B ) ) ` B ) = ( exp ` B ) )
88 87 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( 1 - T ) x. ( ( exp |` ( A [,] B ) ) ` B ) ) = ( ( 1 - T ) x. ( exp ` B ) ) )
89 84 88 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( T x. ( ( exp |` ( A [,] B ) ) ` A ) ) + ( ( 1 - T ) x. ( ( exp |` ( A [,] B ) ) ` B ) ) ) = ( ( T x. ( exp ` A ) ) + ( ( 1 - T ) x. ( exp ` B ) ) ) )
90 61 77 89 3brtr3d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( exp ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) < ( ( T x. ( exp ` A ) ) + ( ( 1 - T ) x. ( exp ` B ) ) ) )