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

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → 𝐴 ∈ ℝ )
2 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → 𝐵 ∈ ℝ )
3 simpl3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → 𝐴 < 𝐵 )
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 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
11 1 2 10 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
12 fssres2 ⊢ ( ( ( exp ↾ ℝ ) : ℝ ⟶ ℝ ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) → ( exp ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
13 9 11 12 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( exp ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
14 ax-resscn ⊢ ℝ ⊆ ℂ
15 11 14 sstrdi ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
16 efcn ⊢ exp ∈ ( ℂ –cn→ ℂ )
17 rescncf ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℂ → ( exp ∈ ( ℂ –cn→ ℂ ) → ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) )
18 15 16 17 mpisyl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
19 cncffvrn ⊢ ( ( ℝ ⊆ ℂ ∧ ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ↔ ( exp ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ) )
20 14 18 19 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ↔ ( exp ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ) )
21 13 20 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
22 reefiso ⊢ ( exp ↾ ℝ ) Isom < , < ( ℝ , ℝ+ )
23 22 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( exp ↾ ℝ ) Isom < , < ( ℝ , ℝ+ ) )
24 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
25 24 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
26 eqidd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( exp ↾ ℝ ) “ ( 𝐴 (,) 𝐵 ) ) = ( ( exp ↾ ℝ ) “ ( 𝐴 (,) 𝐵 ) ) )
27 isores3 ⊢ ( ( ( exp ↾ ℝ ) Isom < , < ( ℝ , ℝ+ ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ∧ ( ( exp ↾ ℝ ) “ ( 𝐴 (,) 𝐵 ) ) = ( ( exp ↾ ℝ ) “ ( 𝐴 (,) 𝐵 ) ) ) → ( ( exp ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) Isom < , < ( ( 𝐴 (,) 𝐵 ) , ( ( exp ↾ ℝ ) “ ( 𝐴 (,) 𝐵 ) ) ) )
28 23 25 26 27 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( exp ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) Isom < , < ( ( 𝐴 (,) 𝐵 ) , ( ( exp ↾ ℝ ) “ ( 𝐴 (,) 𝐵 ) ) ) )
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 ) ↾t ℝ )
34 32 33 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ ( exp ↾ ℝ ) : ℝ ⟶ ℂ ) ∧ ( ℝ ⊆ ℝ ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) ) → ( ℝ D ( ( exp ↾ ℝ ) ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( ( ℝ D ( exp ↾ ℝ ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
35 14 31 34 mpanl12 ⊢ ( ( ℝ ⊆ ℝ ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) → ( ℝ D ( ( exp ↾ ℝ ) ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( ( ℝ D ( exp ↾ ℝ ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
36 29 11 35 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ℝ D ( ( exp ↾ ℝ ) ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( ( ℝ D ( exp ↾ ℝ ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
37 11 resabs1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( exp ↾ ℝ ) ↾ ( 𝐴 [,] 𝐵 ) ) = ( exp ↾ ( 𝐴 [,] 𝐵 ) ) )
38 37 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ℝ D ( ( exp ↾ ℝ ) ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( ℝ D ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ) )
39 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
40 eff ⊢ exp : ℂ ⟶ ℂ
41 ssid ⊢ ℂ ⊆ ℂ
42 dvef ⊢ ( ℂ D exp ) = exp
43 42 dmeqi ⊢ dom ( ℂ D exp ) = dom exp
44 40 fdmi ⊢ dom exp = ℂ
45 43 44 eqtri ⊢ dom ( ℂ D exp ) = ℂ
46 14 45 sseqtrri ⊢ ℝ ⊆ dom ( ℂ D exp )
47 dvres3 ⊢ ( ( ( ℝ ∈ { ℝ , ℂ } ∧ exp : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D exp ) ) ) → ( ℝ D ( exp ↾ ℝ ) ) = ( ( ℂ D exp ) ↾ ℝ ) )
48 39 40 41 46 47 mp4an ⊢ ( ℝ D ( exp ↾ ℝ ) ) = ( ( ℂ D exp ) ↾ ℝ )
49 42 reseq1i ⊢ ( ( ℂ D exp ) ↾ ℝ ) = ( exp ↾ ℝ )
50 48 49 eqtri ⊢ ( ℝ D ( exp ↾ ℝ ) ) = ( exp ↾ ℝ )
51 50 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ℝ D ( exp ↾ ℝ ) ) = ( exp ↾ ℝ ) )
52 iccntr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
53 1 2 52 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
54 51 53 reseq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( ℝ D ( exp ↾ ℝ ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) = ( ( exp ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) )
55 36 38 54 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ℝ D ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( ( exp ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) )
56 isoeq1 ⊢ ( ( ℝ D ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( ( exp ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ) Isom < , < ( ( 𝐴 (,) 𝐵 ) , ( ( exp ↾ ℝ ) “ ( 𝐴 (,) 𝐵 ) ) ) ↔ ( ( exp ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) Isom < , < ( ( 𝐴 (,) 𝐵 ) , ( ( exp ↾ ℝ ) “ ( 𝐴 (,) 𝐵 ) ) ) ) )
57 55 56 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( ℝ D ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ) Isom < , < ( ( 𝐴 (,) 𝐵 ) , ( ( exp ↾ ℝ ) “ ( 𝐴 (,) 𝐵 ) ) ) ↔ ( ( exp ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) Isom < , < ( ( 𝐴 (,) 𝐵 ) , ( ( exp ↾ ℝ ) “ ( 𝐴 (,) 𝐵 ) ) ) ) )
58 28 57 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ℝ D ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ) Isom < , < ( ( 𝐴 (,) 𝐵 ) , ( ( exp ↾ ℝ ) “ ( 𝐴 (,) 𝐵 ) ) ) )
59 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → 𝑇 ∈ ( 0 (,) 1 ) )
60 eqid ⊢ ( ( 𝑇 · 𝐴 ) + ( ( 1 − 𝑇 ) · 𝐵 ) ) = ( ( 𝑇 · 𝐴 ) + ( ( 1 − 𝑇 ) · 𝐵 ) )
61 1 2 3 21 58 59 60 dvcvx ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ‘ ( ( 𝑇 · 𝐴 ) + ( ( 1 − 𝑇 ) · 𝐵 ) ) ) < ( ( 𝑇 · ( ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) + ( ( 1 − 𝑇 ) · ( ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) ) ) )
62 ax-1cn ⊢ 1 ∈ ℂ
63 ioossre ⊢ ( 0 (,) 1 ) ⊆ ℝ
64 63 59 sselid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → 𝑇 ∈ ℝ )
65 64 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → 𝑇 ∈ ℂ )
66 nncan ⊢ ( ( 1 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 1 − ( 1 − 𝑇 ) ) = 𝑇 )
67 62 65 66 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( 1 − ( 1 − 𝑇 ) ) = 𝑇 )
68 67 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( 1 − ( 1 − 𝑇 ) ) · 𝐴 ) = ( 𝑇 · 𝐴 ) )
69 68 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝐴 ) + ( ( 1 − 𝑇 ) · 𝐵 ) ) = ( ( 𝑇 · 𝐴 ) + ( ( 1 − 𝑇 ) · 𝐵 ) ) )
70 ioossicc ⊢ ( 0 (,) 1 ) ⊆ ( 0 [,] 1 )
71 70 59 sselid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → 𝑇 ∈ ( 0 [,] 1 ) )
72 iirev ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → ( 1 − 𝑇 ) ∈ ( 0 [,] 1 ) )
73 71 72 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( 1 − 𝑇 ) ∈ ( 0 [,] 1 ) )
74 lincmb01cmp ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 1 − 𝑇 ) ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝐴 ) + ( ( 1 − 𝑇 ) · 𝐵 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
75 73 74 syldan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝐴 ) + ( ( 1 − 𝑇 ) · 𝐵 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
76 69 75 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( 𝑇 · 𝐴 ) + ( ( 1 − 𝑇 ) · 𝐵 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
77 76 fvresd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ‘ ( ( 𝑇 · 𝐴 ) + ( ( 1 − 𝑇 ) · 𝐵 ) ) ) = ( exp ‘ ( ( 𝑇 · 𝐴 ) + ( ( 1 − 𝑇 ) · 𝐵 ) ) ) )
78 1 rexrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → 𝐴 ∈ ℝ* )
79 2 rexrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → 𝐵 ∈ ℝ* )
80 1 2 3 ltled ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → 𝐴 ≤ 𝐵 )
81 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
82 78 79 80 81 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
83 82 fvresd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) = ( exp ‘ 𝐴 ) )
84 83 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( 𝑇 · ( ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) = ( 𝑇 · ( exp ‘ 𝐴 ) ) )
85 ubicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
86 78 79 80 85 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
87 86 fvresd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) = ( exp ‘ 𝐵 ) )
88 87 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑇 ) · ( ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) ) = ( ( 1 − 𝑇 ) · ( exp ‘ 𝐵 ) ) )
89 84 88 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( 𝑇 · ( ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) + ( ( 1 − 𝑇 ) · ( ( exp ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) ) ) = ( ( 𝑇 · ( exp ‘ 𝐴 ) ) + ( ( 1 − 𝑇 ) · ( exp ‘ 𝐵 ) ) ) )
90 61 77 89 3brtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( exp ‘ ( ( 𝑇 · 𝐴 ) + ( ( 1 − 𝑇 ) · 𝐵 ) ) ) < ( ( 𝑇 · ( exp ‘ 𝐴 ) ) + ( ( 1 − 𝑇 ) · ( exp ‘ 𝐵 ) ) ) )