---

Step * of Lemma antiderivatives-equal

∀I:Interval
  (iproper(I)
  ⇒ (∀f,g,h:I ⟶ℝ.
        (d(g[x])/dx = λx.f[x] on I
        ⇒ d(h[x])/dx = λx.f[x] on I
        ⇒ (∃x:{x:ℝ| x ∈ I} . (g[x] = h[x]))
        ⇒ (∀x:{x:ℝ| x ∈ I} . (g[x] = h[x])))))
BY
{ (InstLemma `antiderivatives-differ-by-constant` []
   THEN RepeatFor 7 ((ParallelLast' THENA Auto))
   THEN ExRepD
   THEN Auto) }

1
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g : I ⟶ℝ
5. h : I ⟶ℝ
6. d(g[x])/dx = λx.f[x] on I
7. d(h[x])/dx = λx.f[x] on I
8. c : ℝ
9. ∀x:{x:ℝ| x ∈ I} . (g[x] = (h[x] + c))
10. x1 : {x:ℝ| x ∈ I} 
11. g[x1] = h[x1]
12. x : {x:ℝ| x ∈ I} 
⊢ g[x] = h[x]

---

Latex:

---

Latex:
\mforall{}I:Interval
    (iproper(I)
    {}\mRightarrow{}  (\mforall{}f,g,h:I  {}\mrightarrow{}\mBbbR{}.
                (d(g[x])/dx  =  \mlambda{}x.f[x]  on  I
                {}\mRightarrow{}  d(h[x])/dx  =  \mlambda{}x.f[x]  on  I
                {}\mRightarrow{}  (\mexists{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (g[x]  =  h[x]))
                {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (g[x]  =  h[x])))))


By

---

Latex:
(InstLemma  `antiderivatives-differ-by-constant`  []
  THEN  RepeatFor  7  ((ParallelLast'  THENA  Auto))
  THEN  ExRepD
  THEN  Auto)

---

Home Index