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 B A < B T 0 1 e T A + 1 T B < T e A + 1 T e B

Proof

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