Metamath Proof Explorer

Theorem scvxcvx

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

Ref Expression
Hypotheses scvxcvx.1 ⊢φ→D⊆ℝ
scvxcvx.2 ⊢φ→F:D⟶ℝ
scvxcvx.3 ⊢φ∧a∈D∧b∈D→ab⊆D
scvxcvx.4 ⊢φ∧x∈D∧y∈D∧x<y∧t∈01→F⁡t⁢x+1−t⁢y<t⁢F⁡x+1−t⁢F⁡y
Assertion scvxcvx ⊢φ∧X∈D∧Y∈D∧T∈01→F⁡T⁢X+1−T⁢Y≤T⁢F⁡X+1−T⁢F⁡Y

Proof

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