---

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


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))
11. x : ℝ
12. y : ℝ
13. x ∈ I
14. y ∈ I
15. x = y
⊢ f[x] = f[y]
BY
{ ((InstLemma `differentiable-functional2` [⌜I⌝;⌜g⌝;⌜h⌝]⋅ THENA Auto)
   THEN InstLemma `differentiable-functional2` [⌜I⌝;⌜f⌝;⌜g⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  iproper(I)
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  g  :  I  {}\mrightarrow{}\mBbbR{}
5.  h  :  I  {}\mrightarrow{}\mBbbR{}
6.  \mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (h[x]  =  h[y]))
7.  d(f[x])/dx  =  \mlambda{}x.g[x]  on  I
8.  d(g[x])/dx  =  \mlambda{}x.h[x]  on  I
9.  \mforall{}x:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  (r0  \mleq{}  h[x])
10.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  I)  {}\mRightarrow{}  (f[x]  <  r0))
11.  x  :  \mBbbR{}
12.  y  :  \mBbbR{}
13.  x  \mmember{}  I
14.  y  \mmember{}  I
15.  x  =  y
\mvdash{}  f[x]  =  f[y]


By

---

Latex:
((InstLemma  `differentiable-functional2`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstLemma  `differentiable-functional2`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index