Metamath Proof Explorer

Theorem scvxcvx

Description: A strictly convex function is convex. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses scvxcvx.1 ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
scvxcvx.2 ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
scvxcvx.3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝑎 [,] 𝑏 ) ⊆ 𝐷 )
scvxcvx.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) )
Assertion scvxcvx ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) ≤ ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 scvxcvx.1 ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
2 scvxcvx.2 ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
3 scvxcvx.3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝑎 [,] 𝑏 ) ⊆ 𝐷 )
4 scvxcvx.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) )
5 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝐷 ⊆ ℝ )
6 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑋 ∈ 𝐷 )
7 5 6 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑋 ∈ ℝ )
8 7 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → 𝑋 ∈ ℝ )
9 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑌 ∈ 𝐷 )
10 5 9 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑌 ∈ ℝ )
11 10 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → 𝑌 ∈ ℝ )
12 8 11 lttri4d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ∨ 𝑌 < 𝑋 ) )
13 oveq1 ⊢ ( 𝑡 = 𝑇 → ( 𝑡 · 𝑋 ) = ( 𝑇 · 𝑋 ) )
14 oveq2 ⊢ ( 𝑡 = 𝑇 → ( 1 − 𝑡 ) = ( 1 − 𝑇 ) )
15 14 oveq1d ⊢ ( 𝑡 = 𝑇 → ( ( 1 − 𝑡 ) · 𝑌 ) = ( ( 1 − 𝑇 ) · 𝑌 ) )
16 13 15 oveq12d ⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑌 ) ) = ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) )
17 16 fveq2d ⊢ ( 𝑡 = 𝑇 → ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑌 ) ) ) = ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) )
18 oveq1 ⊢ ( 𝑡 = 𝑇 → ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) = ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) )
19 14 oveq1d ⊢ ( 𝑡 = 𝑇 → ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑌 ) ) = ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) )
20 18 19 oveq12d ⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) )
21 17 20 breq12d ⊢ ( 𝑡 = 𝑇 → ( ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑌 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) )
22 6 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑋 < 𝑌 ) ) → 𝑋 ∈ 𝐷 )
23 9 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑋 < 𝑌 ) ) → 𝑌 ∈ 𝐷 )
24 22 23 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑋 < 𝑌 ) ) → ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) )
25 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑋 < 𝑌 ) ) → 𝑋 < 𝑌 )
26 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑋 < 𝑌 ) ) → 𝜑 )
27 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 < 𝑦 ↔ 𝑋 < 𝑦 ) )
28 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑡 · 𝑥 ) = ( 𝑡 · 𝑋 ) )
29 28 fvoveq1d ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) = ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) )
30 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
31 30 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) = ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) )
32 31 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) )
33 29 32 breq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) )
34 33 ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ↔ ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) )
35 34 imbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) ↔ ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
36 27 35 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 < 𝑦 → ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) ) ↔ ( 𝑋 < 𝑦 → ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) ) ) )
37 breq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 < 𝑦 ↔ 𝑋 < 𝑌 ) )
38 oveq2 ⊢ ( 𝑦 = 𝑌 → ( ( 1 − 𝑡 ) · 𝑦 ) = ( ( 1 − 𝑡 ) · 𝑌 ) )
39 38 oveq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) = ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑌 ) ) )
40 39 fveq2d ⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) = ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑌 ) ) ) )
41 fveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
42 41 oveq2d ⊢ ( 𝑦 = 𝑌 → ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) = ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑌 ) ) )
43 42 oveq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑌 ) ) ) )
44 40 43 breq12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑌 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) )
45 44 ralbidv ⊢ ( 𝑦 = 𝑌 → ( ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ↔ ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑌 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) )
46 45 imbi2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) ↔ ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑌 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) ) )
47 37 46 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 < 𝑦 → ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) ) ↔ ( 𝑋 < 𝑌 → ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑌 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) ) ) )
48 4 3expia ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦 ) ) → ( 𝑡 ∈ ( 0 (,) 1 ) → ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) )
49 48 ralrimiv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦 ) ) → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) )
50 49 expcom ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦 ) → ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) )
51 50 3expia ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 < 𝑦 → ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
52 36 47 51 vtocl2ga ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) → ( 𝑋 < 𝑌 → ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑌 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) ) )
53 24 25 26 52 syl3c ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑋 < 𝑌 ) ) → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑋 ) + ( ( 1 − 𝑡 ) · 𝑌 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑌 ) ) ) )
54 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑋 < 𝑌 ) ) → 𝑇 ∈ ( 0 (,) 1 ) )
55 21 53 54 rspcdva ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑋 < 𝑌 ) ) → ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) )
56 55 orcd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑋 < 𝑌 ) ) → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ∨ ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) )
57 56 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( 𝑋 < 𝑌 → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ∨ ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) ) )
58 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
59 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ( 0 [,] 1 ) )
60 58 59 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ℝ )
61 60 recnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ℂ )
62 ax-1cn ⊢ 1 ∈ ℂ
63 pncan3 ⊢ ( ( 𝑇 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑇 + ( 1 − 𝑇 ) ) = 1 )
64 61 62 63 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 + ( 1 − 𝑇 ) ) = 1 )
65 64 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 + ( 1 − 𝑇 ) ) · 𝑌 ) = ( 1 · 𝑌 ) )
66 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 1 − 𝑇 ) ∈ ℂ )
67 62 61 66 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑇 ) ∈ ℂ )
68 10 recnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑌 ∈ ℂ )
69 61 67 68 adddird ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 + ( 1 − 𝑇 ) ) · 𝑌 ) = ( ( 𝑇 · 𝑌 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) )
70 68 mulid2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 · 𝑌 ) = 𝑌 )
71 65 69 70 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · 𝑌 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = 𝑌 )
72 71 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑇 · 𝑌 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( 𝐹 ‘ 𝑌 ) )
73 64 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 + ( 1 − 𝑇 ) ) · ( 𝐹 ‘ 𝑌 ) ) = ( 1 · ( 𝐹 ‘ 𝑌 ) ) )
74 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝐹 : 𝐷 ⟶ ℝ )
75 74 9 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ 𝑌 ) ∈ ℝ )
76 75 recnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ 𝑌 ) ∈ ℂ )
77 61 67 76 adddird ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 + ( 1 − 𝑇 ) ) · ( 𝐹 ‘ 𝑌 ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) )
78 76 mulid2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 · ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ 𝑌 ) )
79 73 77 78 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) = ( 𝐹 ‘ 𝑌 ) )
80 72 79 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑇 · 𝑌 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) )
81 80 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( 𝐹 ‘ ( ( 𝑇 · 𝑌 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) )
82 oveq2 ⊢ ( 𝑋 = 𝑌 → ( 𝑇 · 𝑋 ) = ( 𝑇 · 𝑌 ) )
83 82 fvoveq1d ⊢ ( 𝑋 = 𝑌 → ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( 𝐹 ‘ ( ( 𝑇 · 𝑌 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) )
84 fveq2 ⊢ ( 𝑋 = 𝑌 → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
85 84 oveq2d ⊢ ( 𝑋 = 𝑌 → ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) = ( 𝑇 · ( 𝐹 ‘ 𝑌 ) ) )
86 85 oveq1d ⊢ ( 𝑋 = 𝑌 → ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) )
87 83 86 eqeq12d ⊢ ( 𝑋 = 𝑌 → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( 𝐹 ‘ ( ( 𝑇 · 𝑌 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) )
88 81 87 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( 𝑋 = 𝑌 → ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) )
89 olc ⊢ ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ∨ ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) )
90 88 89 syl6 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( 𝑋 = 𝑌 → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ∨ ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) ) )
91 oveq1 ⊢ ( 𝑡 = ( 1 − 𝑇 ) → ( 𝑡 · 𝑌 ) = ( ( 1 − 𝑇 ) · 𝑌 ) )
92 oveq2 ⊢ ( 𝑡 = ( 1 − 𝑇 ) → ( 1 − 𝑡 ) = ( 1 − ( 1 − 𝑇 ) ) )
93 92 oveq1d ⊢ ( 𝑡 = ( 1 − 𝑇 ) → ( ( 1 − 𝑡 ) · 𝑋 ) = ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) )
94 91 93 oveq12d ⊢ ( 𝑡 = ( 1 − 𝑇 ) → ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑋 ) ) = ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) ) )
95 94 fveq2d ⊢ ( 𝑡 = ( 1 − 𝑇 ) → ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑋 ) ) ) = ( 𝐹 ‘ ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) ) ) )
96 oveq1 ⊢ ( 𝑡 = ( 1 − 𝑇 ) → ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) = ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) )
97 92 oveq1d ⊢ ( 𝑡 = ( 1 − 𝑇 ) → ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑋 ) ) = ( ( 1 − ( 1 − 𝑇 ) ) · ( 𝐹 ‘ 𝑋 ) ) )
98 96 97 oveq12d ⊢ ( 𝑡 = ( 1 − 𝑇 ) → ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑋 ) ) ) = ( ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − ( 1 − 𝑇 ) ) · ( 𝐹 ‘ 𝑋 ) ) ) )
99 95 98 breq12d ⊢ ( 𝑡 = ( 1 − 𝑇 ) → ( ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑋 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑋 ) ) ) ↔ ( 𝐹 ‘ ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) ) ) < ( ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − ( 1 − 𝑇 ) ) · ( 𝐹 ‘ 𝑋 ) ) ) ) )
100 9 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑌 < 𝑋 ) ) → 𝑌 ∈ 𝐷 )
101 6 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑌 < 𝑋 ) ) → 𝑋 ∈ 𝐷 )
102 100 101 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑌 < 𝑋 ) ) → ( 𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷 ) )
103 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑌 < 𝑋 ) ) → 𝑌 < 𝑋 )
104 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑌 < 𝑋 ) ) → 𝜑 )
105 breq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 < 𝑦 ↔ 𝑌 < 𝑦 ) )
106 oveq2 ⊢ ( 𝑥 = 𝑌 → ( 𝑡 · 𝑥 ) = ( 𝑡 · 𝑌 ) )
107 106 fvoveq1d ⊢ ( 𝑥 = 𝑌 → ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) = ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) )
108 fveq2 ⊢ ( 𝑥 = 𝑌 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑌 ) )
109 108 oveq2d ⊢ ( 𝑥 = 𝑌 → ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) = ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) )
110 109 oveq1d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) )
111 107 110 breq12d ⊢ ( 𝑥 = 𝑌 → ( ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) )
112 111 ralbidv ⊢ ( 𝑥 = 𝑌 → ( ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ↔ ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) )
113 112 imbi2d ⊢ ( 𝑥 = 𝑌 → ( ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) ↔ ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
114 105 113 imbi12d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 < 𝑦 → ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) ) ↔ ( 𝑌 < 𝑦 → ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) ) ) )
115 breq2 ⊢ ( 𝑦 = 𝑋 → ( 𝑌 < 𝑦 ↔ 𝑌 < 𝑋 ) )
116 oveq2 ⊢ ( 𝑦 = 𝑋 → ( ( 1 − 𝑡 ) · 𝑦 ) = ( ( 1 − 𝑡 ) · 𝑋 ) )
117 116 oveq2d ⊢ ( 𝑦 = 𝑋 → ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) = ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑋 ) ) )
118 117 fveq2d ⊢ ( 𝑦 = 𝑋 → ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) = ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑋 ) ) ) )
119 fveq2 ⊢ ( 𝑦 = 𝑋 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
120 119 oveq2d ⊢ ( 𝑦 = 𝑋 → ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) = ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑋 ) ) )
121 120 oveq2d ⊢ ( 𝑦 = 𝑋 → ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑋 ) ) ) )
122 118 121 breq12d ⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑋 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑋 ) ) ) ) )
123 122 ralbidv ⊢ ( 𝑦 = 𝑋 → ( ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ↔ ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑋 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑋 ) ) ) ) )
124 123 imbi2d ⊢ ( 𝑦 = 𝑋 → ( ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) ↔ ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑋 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑋 ) ) ) ) ) )
125 115 124 imbi12d ⊢ ( 𝑦 = 𝑋 → ( ( 𝑌 < 𝑦 → ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) ) ) ↔ ( 𝑌 < 𝑋 → ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑋 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑋 ) ) ) ) ) ) )
126 114 125 51 vtocl2ga ⊢ ( ( 𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷 ) → ( 𝑌 < 𝑋 → ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑋 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑋 ) ) ) ) ) )
127 102 103 104 126 syl3c ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑌 < 𝑋 ) ) → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( 𝐹 ‘ ( ( 𝑡 · 𝑌 ) + ( ( 1 − 𝑡 ) · 𝑋 ) ) ) < ( ( 𝑡 · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑋 ) ) ) )
128 1re ⊢ 1 ∈ ℝ
129 elioore ⊢ ( 𝑇 ∈ ( 0 (,) 1 ) → 𝑇 ∈ ℝ )
130 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑇 ∈ ℝ ) → ( 1 − 𝑇 ) ∈ ℝ )
131 128 129 130 sylancr ⊢ ( 𝑇 ∈ ( 0 (,) 1 ) → ( 1 − 𝑇 ) ∈ ℝ )
132 eliooord ⊢ ( 𝑇 ∈ ( 0 (,) 1 ) → ( 0 < 𝑇 ∧ 𝑇 < 1 ) )
133 132 simprd ⊢ ( 𝑇 ∈ ( 0 (,) 1 ) → 𝑇 < 1 )
134 posdif ⊢ ( ( 𝑇 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑇 < 1 ↔ 0 < ( 1 − 𝑇 ) ) )
135 129 128 134 sylancl ⊢ ( 𝑇 ∈ ( 0 (,) 1 ) → ( 𝑇 < 1 ↔ 0 < ( 1 − 𝑇 ) ) )
136 133 135 mpbid ⊢ ( 𝑇 ∈ ( 0 (,) 1 ) → 0 < ( 1 − 𝑇 ) )
137 132 simpld ⊢ ( 𝑇 ∈ ( 0 (,) 1 ) → 0 < 𝑇 )
138 ltsubpos ⊢ ( ( 𝑇 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 0 < 𝑇 ↔ ( 1 − 𝑇 ) < 1 ) )
139 129 128 138 sylancl ⊢ ( 𝑇 ∈ ( 0 (,) 1 ) → ( 0 < 𝑇 ↔ ( 1 − 𝑇 ) < 1 ) )
140 137 139 mpbid ⊢ ( 𝑇 ∈ ( 0 (,) 1 ) → ( 1 − 𝑇 ) < 1 )
141 0xr ⊢ 0 ∈ ℝ*
142 1xr ⊢ 1 ∈ ℝ*
143 elioo2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( 1 − 𝑇 ) ∈ ( 0 (,) 1 ) ↔ ( ( 1 − 𝑇 ) ∈ ℝ ∧ 0 < ( 1 − 𝑇 ) ∧ ( 1 − 𝑇 ) < 1 ) ) )
144 141 142 143 mp2an ⊢ ( ( 1 − 𝑇 ) ∈ ( 0 (,) 1 ) ↔ ( ( 1 − 𝑇 ) ∈ ℝ ∧ 0 < ( 1 − 𝑇 ) ∧ ( 1 − 𝑇 ) < 1 ) )
145 131 136 140 144 syl3anbrc ⊢ ( 𝑇 ∈ ( 0 (,) 1 ) → ( 1 − 𝑇 ) ∈ ( 0 (,) 1 ) )
146 145 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑌 < 𝑋 ) ) → ( 1 − 𝑇 ) ∈ ( 0 (,) 1 ) )
147 99 127 146 rspcdva ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑌 < 𝑋 ) ) → ( 𝐹 ‘ ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) ) ) < ( ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − ( 1 − 𝑇 ) ) · ( 𝐹 ‘ 𝑋 ) ) ) )
148 128 60 130 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑇 ) ∈ ℝ )
149 148 10 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 1 − 𝑇 ) · 𝑌 ) ∈ ℝ )
150 149 recnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 1 − 𝑇 ) · 𝑌 ) ∈ ℂ )
151 60 7 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 · 𝑋 ) ∈ ℝ )
152 151 recnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 · 𝑋 ) ∈ ℂ )
153 nncan ⊢ ( ( 1 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 1 − ( 1 − 𝑇 ) ) = 𝑇 )
154 62 61 153 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 − ( 1 − 𝑇 ) ) = 𝑇 )
155 154 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) = ( 𝑇 · 𝑋 ) )
156 155 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) ) = ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( 𝑇 · 𝑋 ) ) )
157 150 152 156 comraddd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) ) = ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) )
158 157 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑌 < 𝑋 ) ) → ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) ) = ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) )
159 158 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑌 < 𝑋 ) ) → ( 𝐹 ‘ ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) ) ) = ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) )
160 148 75 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ∈ ℝ )
161 160 recnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ∈ ℂ )
162 74 6 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ℝ )
163 60 162 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ )
164 163 recnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) ∈ ℂ )
165 154 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 1 − ( 1 − 𝑇 ) ) · ( 𝐹 ‘ 𝑋 ) ) = ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) )
166 165 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − ( 1 − 𝑇 ) ) · ( 𝐹 ‘ 𝑋 ) ) ) = ( ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) + ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) ) )
167 161 164 166 comraddd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − ( 1 − 𝑇 ) ) · ( 𝐹 ‘ 𝑋 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) )
168 167 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑌 < 𝑋 ) ) → ( ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) + ( ( 1 − ( 1 − 𝑇 ) ) · ( 𝐹 ‘ 𝑋 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) )
169 147 159 168 3brtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑌 < 𝑋 ) ) → ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) )
170 169 orcd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑇 ∈ ( 0 (,) 1 ) ∧ 𝑌 < 𝑋 ) ) → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ∨ ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) )
171 170 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( 𝑌 < 𝑋 → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ∨ ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) ) )
172 57 90 171 3jaod ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ∨ 𝑌 < 𝑋 ) → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ∨ ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) ) )
173 12 172 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑇 ∈ ( 0 (,) 1 ) ) → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ∨ ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) )
174 173 ex ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 ∈ ( 0 (,) 1 ) → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ∨ ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) ) )
175 elpri ⊢ ( 𝑇 ∈ { 0 , 1 } → ( 𝑇 = 0 ∨ 𝑇 = 1 ) )
176 76 addid2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 0 + ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ 𝑌 ) )
177 162 recnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ℂ )
178 177 mul02d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 0 · ( 𝐹 ‘ 𝑋 ) ) = 0 )
179 178 78 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 0 · ( 𝐹 ‘ 𝑋 ) ) + ( 1 · ( 𝐹 ‘ 𝑌 ) ) ) = ( 0 + ( 𝐹 ‘ 𝑌 ) ) )
180 7 recnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑋 ∈ ℂ )
181 180 mul02d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 0 · 𝑋 ) = 0 )
182 181 70 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 0 · 𝑋 ) + ( 1 · 𝑌 ) ) = ( 0 + 𝑌 ) )
183 68 addid2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 0 + 𝑌 ) = 𝑌 )
184 182 183 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 0 · 𝑋 ) + ( 1 · 𝑌 ) ) = 𝑌 )
185 184 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 0 · 𝑋 ) + ( 1 · 𝑌 ) ) ) = ( 𝐹 ‘ 𝑌 ) )
186 176 179 185 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 0 · 𝑋 ) + ( 1 · 𝑌 ) ) ) = ( ( 0 · ( 𝐹 ‘ 𝑋 ) ) + ( 1 · ( 𝐹 ‘ 𝑌 ) ) ) )
187 oveq1 ⊢ ( 𝑇 = 0 → ( 𝑇 · 𝑋 ) = ( 0 · 𝑋 ) )
188 oveq2 ⊢ ( 𝑇 = 0 → ( 1 − 𝑇 ) = ( 1 − 0 ) )
189 1m0e1 ⊢ ( 1 − 0 ) = 1
190 188 189 eqtrdi ⊢ ( 𝑇 = 0 → ( 1 − 𝑇 ) = 1 )
191 190 oveq1d ⊢ ( 𝑇 = 0 → ( ( 1 − 𝑇 ) · 𝑌 ) = ( 1 · 𝑌 ) )
192 187 191 oveq12d ⊢ ( 𝑇 = 0 → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = ( ( 0 · 𝑋 ) + ( 1 · 𝑌 ) ) )
193 192 fveq2d ⊢ ( 𝑇 = 0 → ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( 𝐹 ‘ ( ( 0 · 𝑋 ) + ( 1 · 𝑌 ) ) ) )
194 oveq1 ⊢ ( 𝑇 = 0 → ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) = ( 0 · ( 𝐹 ‘ 𝑋 ) ) )
195 190 oveq1d ⊢ ( 𝑇 = 0 → ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) = ( 1 · ( 𝐹 ‘ 𝑌 ) ) )
196 194 195 oveq12d ⊢ ( 𝑇 = 0 → ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) = ( ( 0 · ( 𝐹 ‘ 𝑋 ) ) + ( 1 · ( 𝐹 ‘ 𝑌 ) ) ) )
197 193 196 eqeq12d ⊢ ( 𝑇 = 0 → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( 𝐹 ‘ ( ( 0 · 𝑋 ) + ( 1 · 𝑌 ) ) ) = ( ( 0 · ( 𝐹 ‘ 𝑋 ) ) + ( 1 · ( 𝐹 ‘ 𝑌 ) ) ) ) )
198 186 197 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 = 0 → ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) )
199 177 addid1d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝐹 ‘ 𝑋 ) + 0 ) = ( 𝐹 ‘ 𝑋 ) )
200 177 mulid2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 · ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )
201 76 mul02d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 0 · ( 𝐹 ‘ 𝑌 ) ) = 0 )
202 200 201 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 1 · ( 𝐹 ‘ 𝑋 ) ) + ( 0 · ( 𝐹 ‘ 𝑌 ) ) ) = ( ( 𝐹 ‘ 𝑋 ) + 0 ) )
203 180 mulid2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 · 𝑋 ) = 𝑋 )
204 68 mul02d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 0 · 𝑌 ) = 0 )
205 203 204 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 1 · 𝑋 ) + ( 0 · 𝑌 ) ) = ( 𝑋 + 0 ) )
206 180 addid1d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑋 + 0 ) = 𝑋 )
207 205 206 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 1 · 𝑋 ) + ( 0 · 𝑌 ) ) = 𝑋 )
208 207 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 1 · 𝑋 ) + ( 0 · 𝑌 ) ) ) = ( 𝐹 ‘ 𝑋 ) )
209 199 202 208 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 1 · 𝑋 ) + ( 0 · 𝑌 ) ) ) = ( ( 1 · ( 𝐹 ‘ 𝑋 ) ) + ( 0 · ( 𝐹 ‘ 𝑌 ) ) ) )
210 oveq1 ⊢ ( 𝑇 = 1 → ( 𝑇 · 𝑋 ) = ( 1 · 𝑋 ) )
211 oveq2 ⊢ ( 𝑇 = 1 → ( 1 − 𝑇 ) = ( 1 − 1 ) )
212 1m1e0 ⊢ ( 1 − 1 ) = 0
213 211 212 eqtrdi ⊢ ( 𝑇 = 1 → ( 1 − 𝑇 ) = 0 )
214 213 oveq1d ⊢ ( 𝑇 = 1 → ( ( 1 − 𝑇 ) · 𝑌 ) = ( 0 · 𝑌 ) )
215 210 214 oveq12d ⊢ ( 𝑇 = 1 → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = ( ( 1 · 𝑋 ) + ( 0 · 𝑌 ) ) )
216 215 fveq2d ⊢ ( 𝑇 = 1 → ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( 𝐹 ‘ ( ( 1 · 𝑋 ) + ( 0 · 𝑌 ) ) ) )
217 oveq1 ⊢ ( 𝑇 = 1 → ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) = ( 1 · ( 𝐹 ‘ 𝑋 ) ) )
218 213 oveq1d ⊢ ( 𝑇 = 1 → ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) = ( 0 · ( 𝐹 ‘ 𝑌 ) ) )
219 217 218 oveq12d ⊢ ( 𝑇 = 1 → ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) = ( ( 1 · ( 𝐹 ‘ 𝑋 ) ) + ( 0 · ( 𝐹 ‘ 𝑌 ) ) ) )
220 216 219 eqeq12d ⊢ ( 𝑇 = 1 → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( 𝐹 ‘ ( ( 1 · 𝑋 ) + ( 0 · 𝑌 ) ) ) = ( ( 1 · ( 𝐹 ‘ 𝑋 ) ) + ( 0 · ( 𝐹 ‘ 𝑌 ) ) ) ) )
221 209 220 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 = 1 → ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) )
222 198 221 jaod ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 = 0 ∨ 𝑇 = 1 ) → ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) )
223 175 222 89 syl56 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 ∈ { 0 , 1 } → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ∨ ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) ) )
224 0le1 ⊢ 0 ≤ 1
225 prunioo ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1 ) → ( ( 0 (,) 1 ) ∪ { 0 , 1 } ) = ( 0 [,] 1 ) )
226 141 142 224 225 mp3an ⊢ ( ( 0 (,) 1 ) ∪ { 0 , 1 } ) = ( 0 [,] 1 )
227 59 226 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ( ( 0 (,) 1 ) ∪ { 0 , 1 } ) )
228 elun ⊢ ( 𝑇 ∈ ( ( 0 (,) 1 ) ∪ { 0 , 1 } ) ↔ ( 𝑇 ∈ ( 0 (,) 1 ) ∨ 𝑇 ∈ { 0 , 1 } ) )
229 227 228 sylib ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 ∈ ( 0 (,) 1 ) ∨ 𝑇 ∈ { 0 , 1 } ) )
230 174 223 229 mpjaod ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ∨ ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) )
231 1 3 cvxcl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ 𝐷 )
232 74 231 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) ∈ ℝ )
233 163 160 readdcld ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ∈ ℝ )
234 232 233 leloed ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) ≤ ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) < ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ∨ ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) = ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) ) ) )
235 230 234 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ) ≤ ( ( 𝑇 · ( 𝐹 ‘ 𝑋 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝑌 ) ) ) )