# Metamath Proof Explorer

## Theorem scvxcvx

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

Ref Expression
Hypotheses scvxcvx.1 ${⊢}{\phi }\to {D}\subseteq ℝ$
scvxcvx.2 ${⊢}{\phi }\to {F}:{D}⟶ℝ$
scvxcvx.3 ${⊢}\left({\phi }\wedge \left({a}\in {D}\wedge {b}\in {D}\right)\right)\to \left[{a},{b}\right]\subseteq {D}$
scvxcvx.4 ${⊢}\left({\phi }\wedge \left({x}\in {D}\wedge {y}\in {D}\wedge {x}<{y}\right)\wedge {t}\in \left(0,1\right)\right)\to {F}\left({t}{x}+\left(1-{t}\right){y}\right)<{t}{F}\left({x}\right)+\left(1-{t}\right){F}\left({y}\right)$
Assertion scvxcvx ${⊢}\left({\phi }\wedge \left({X}\in {D}\wedge {Y}\in {D}\wedge {T}\in \left[0,1\right]\right)\right)\to {F}\left({T}{X}+\left(1-{T}\right){Y}\right)\le {T}{F}\left({X}\right)+\left(1-{T}\right){F}\left({Y}\right)$

### Proof

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