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 \in ℝ \land B \in ℝ \land A < B) \land T \in (0, 1)) \to e^{T A + (1 - T) B} < T e^{A} + (1 - T) e^{B}$

Proof

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

Metamath Proof Explorer

Theorem efcvx

Proof