---

Step * 1 of Lemma implies-convex-on


1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:ℝ.  ((x ∈ I) ⇒ (y ∈ I) ⇒ (x = y) ⇒ (f[x] = f[y]))
4. ∀x,y:ℝ.
     ((x < y)
     ⇒ (∀t:ℝ
           ((x ∈ I) ⇒ (y ∈ I) ⇒ (t ∈ [r0, r1]) ⇒ (f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))))))
5. x : ℝ
6. y : ℝ
7. t : ℝ
8. x ∈ I
9. y ∈ I
10. t ∈ [r0, r1]
11. (t * x) + ((r1 - t) * y) ∈ I
⊢ f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))
BY
{ ((StableCases  ⌜x < y⌝⋅ THENA Auto) THENL [(BackThruSomeHyp THEN Auto); (StableCases  ⌜y < x⌝⋅ THENA Auto)]) }

1
1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:ℝ.  ((x ∈ I) ⇒ (y ∈ I) ⇒ (x = y) ⇒ (f[x] = f[y]))
4. ∀x,y:ℝ.
     ((x < y)
     ⇒ (∀t:ℝ
           ((x ∈ I) ⇒ (y ∈ I) ⇒ (t ∈ [r0, r1]) ⇒ (f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))))))
5. x : ℝ
6. y : ℝ
7. t : ℝ
8. x ∈ I
9. y ∈ I
10. t ∈ [r0, r1]
11. (t * x) + ((r1 - t) * y) ∈ I
12. ¬(x < y)
13. y < x
⊢ f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))

2
1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:ℝ.  ((x ∈ I) ⇒ (y ∈ I) ⇒ (x = y) ⇒ (f[x] = f[y]))
4. ∀x,y:ℝ.
     ((x < y)
     ⇒ (∀t:ℝ
           ((x ∈ I) ⇒ (y ∈ I) ⇒ (t ∈ [r0, r1]) ⇒ (f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))))))
5. x : ℝ
6. y : ℝ
7. t : ℝ
8. x ∈ I
9. y ∈ I
10. t ∈ [r0, r1]
11. (t * x) + ((r1 - t) * y) ∈ I
12. ¬(x < y)
13. ¬(y < x)
⊢ f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  \mforall{}x,y:\mBbbR{}.    ((x  \mmember{}  I)  {}\mRightarrow{}  (y  \mmember{}  I)  {}\mRightarrow{}  (x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))
4.  \mforall{}x,y:\mBbbR{}.
          ((x  <  y)
          {}\mRightarrow{}  (\mforall{}t:\mBbbR{}
                      ((x  \mmember{}  I)
                      {}\mRightarrow{}  (y  \mmember{}  I)
                      {}\mRightarrow{}  (t  \mmember{}  [r0,  r1])
                      {}\mRightarrow{}  (f[(t  *  x)  +  ((r1  -  t)  *  y)]  \mleq{}  ((t  *  f[x])  +  ((r1  -  t)  *  f[y]))))))
5.  x  :  \mBbbR{}
6.  y  :  \mBbbR{}
7.  t  :  \mBbbR{}
8.  x  \mmember{}  I
9.  y  \mmember{}  I
10.  t  \mmember{}  [r0,  r1]
11.  (t  *  x)  +  ((r1  -  t)  *  y)  \mmember{}  I
\mvdash{}  f[(t  *  x)  +  ((r1  -  t)  *  y)]  \mleq{}  ((t  *  f[x])  +  ((r1  -  t)  *  f[y]))


By

---

Latex:
((StableCases    \mkleeneopen{}x  <  y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THENL  [(BackThruSomeHyp  THEN  Auto);  (StableCases    \mkleeneopen{}y  <  x\mkleeneclose{}\mcdot{}  THENA  Auto)]
)

---

Home Index