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		cncfcdm	⊢ ( ( ℝ ⊆ ℂ ∧ ( 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 ‘ 𝐵 ) ) ) )