---

Step * 1 1 of Lemma antiderivatives-equal


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. (h[x1] + c) = h[x1]
12. x : {x:ℝ| x ∈ I} 
⊢ (h[x] + c) = h[x]
BY
{ (nRAdd ⌜-(h[x1])⌝ (-2)⋅ THENA 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. c = r0
12. x : {x:ℝ| x ∈ I} 
⊢ (h[x] + c) = h[x]

---

Latex:

---

Latex:

1.  I  :  Interval
2.  iproper(I)
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  g  :  I  {}\mrightarrow{}\mBbbR{}
5.  h  :  I  {}\mrightarrow{}\mBbbR{}
6.  d(g[x])/dx  =  \mlambda{}x.f[x]  on  I
7.  d(h[x])/dx  =  \mlambda{}x.f[x]  on  I
8.  c  :  \mBbbR{}
9.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (g[x]  =  (h[x]  +  c))
10.  x1  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
11.  (h[x1]  +  c)  =  h[x1]
12.  x  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
\mvdash{}  (h[x]  +  c)  =  h[x]


By

---

Latex:
(nRAdd  \mkleeneopen{}-(h[x1])\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)

---

Home Index