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

Metamath Proof Explorer

Theorem logccv

Proof