---

Step * of Lemma second-deriv-implies-nonzero-on

∀I:Interval
  (iproper(I)
  ⇒ (∀f,g,h:I ⟶ℝ.
        ((∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (h[x] = h[y])))
        ⇒ d(f[x])/dx = λx.g[x] on I
        ⇒ d(g[x])/dx = λx.h[x] on I
        ⇒ (((∀x:{a:ℝ| a ∈ I} . (h[x] ≤ r0)) ∧ (∀x:ℝ. ((x ∈ I) ⇒ (r0 < f[x]))))
           ∨ ((∀x:{a:ℝ| a ∈ I} . (r0 ≤ h[x])) ∧ (∀x:ℝ. ((x ∈ I) ⇒ (f[x] < r0)))))
        ⇒ f[x]≠r0 for x ∈ I)))
BY
{ xxx(Auto THEN RepeatFor 2 (D -1))xxx }

1
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g : I ⟶ℝ
5. h : I ⟶ℝ
6. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (h[x] = h[y]))
7. d(f[x])/dx = λx.g[x] on I
8. d(g[x])/dx = λx.h[x] on I
9. ∀x:{a:ℝ| a ∈ I} . (h[x] ≤ r0)
10. ∀x:ℝ. ((x ∈ I) ⇒ (r0 < f[x]))
⊢ f[x]≠r0 for x ∈ I

2
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g : I ⟶ℝ
5. h : I ⟶ℝ
6. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (h[x] = h[y]))
7. d(f[x])/dx = λx.g[x] on I
8. d(g[x])/dx = λx.h[x] on I
9. ∀x:{a:ℝ| a ∈ I} . (r0 ≤ h[x])
10. ∀x:ℝ. ((x ∈ I) ⇒ (f[x] < r0))
⊢ f[x]≠r0 for x ∈ I

---

Latex:

---

Latex:
\mforall{}I:Interval
    (iproper(I)
    {}\mRightarrow{}  (\mforall{}f,g,h:I  {}\mrightarrow{}\mBbbR{}.
                ((\mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (h[x]  =  h[y])))
                {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.g[x]  on  I
                {}\mRightarrow{}  d(g[x])/dx  =  \mlambda{}x.h[x]  on  I
                {}\mRightarrow{}  (((\mforall{}x:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  (h[x]  \mleq{}  r0))  \mwedge{}  (\mforall{}x:\mBbbR{}.  ((x  \mmember{}  I)  {}\mRightarrow{}  (r0  <  f[x]))))
                      \mvee{}  ((\mforall{}x:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  (r0  \mleq{}  h[x]))  \mwedge{}  (\mforall{}x:\mBbbR{}.  ((x  \mmember{}  I)  {}\mRightarrow{}  (f[x]  <  r0)))))
                {}\mRightarrow{}  f[x]\mneq{}r0  for  x  \mmember{}  I)))


By

---

Latex:
xxx(Auto  THEN  RepeatFor  2  (D  -1))xxx

---

Home Index