This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 cncfcdm ⊢ ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 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 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
103 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
104 iccntr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
105 2 4 104 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
106 84 88 89 101 14 102 103 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 − 𝑇 ) · 𝐵 ) ) ) )