---

Step * of Lemma antiderivatives-differ-by-constant

∀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 ⇒ (∃c:ℝ. ∀x:{x:ℝ| x ∈ I} . (g[x] = (h[x] + c))))))
BY
{ (Auto THEN (InstLemma `derivative-is-zero` [⌜I⌝;⌜λ2x.g[x] - h[x]⌝]⋅ THENA Auto) THEN D -1 THEN Thin (-1) THEN D -1) }

1
.....antecedent..... 
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
⊢ d(g[x] - h[x])/dx = λx.r0 on I

2
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:ℝ. ∀x:{x:ℝ| x ∈ I} . ((g[x] - h[x]) = c)
⊢ ∃c:ℝ. ∀x:{x:ℝ| x ∈ I} . (g[x] = (h[x] + c))

---

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{}c:\mBbbR{}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (g[x]  =  (h[x]  +  c))))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `derivative-is-zero`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.g[x]  -  h[x]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  D  -1)

---

Home Index