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	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℝ⁺ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( 𝑇 · ( log ‘ 𝐴 ) ) + ( ( 1 − 𝑇 ) · ( log ‘ 𝐵 ) ) ) < ( log ‘ ( ( 𝑇 · 𝐴 ) + ( ( 1 − 𝑇 ) · 𝐵 ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem logccv

Proof