---

Step * of Lemma integral-reverse

∀[a,c:ℝ]. ∀[f:{f:[rmin(a;c), rmax(a;c)] ⟶ℝ| ifun(f;[rmin(a;c), rmax(a;c)])} ].  (a_∫-c f[x] dx = -(c_∫-a f[x] dx))
BY
{ (Auto THEN (InstLemma `integral-additive` [⌜a⌝;⌜a⌝;⌜c⌝;⌜f⌝]⋅ THENA Try (Trivial))) }

1
.....wf..... 
1. a : ℝ
2. c : ℝ
3. f : {f:[rmin(a;c), rmax(a;c)] ⟶ℝ| ifun(f;[rmin(a;c), rmax(a;c)])} 
⊢ f ∈ {f:[rmin(a;rmin(a;c)), rmax(a;rmax(a;c))] ⟶ℝ| ifun(f;[rmin(a;rmin(a;c)), rmax(a;rmax(a;c))])} 

2
1. a : ℝ
2. c : ℝ
3. f : {f:[rmin(a;c), rmax(a;c)] ⟶ℝ| ifun(f;[rmin(a;c), rmax(a;c)])} 
4. a_∫-a f[x] dx = (a_∫-c f[x] dx + c_∫-a f[x] dx)
⊢ a_∫-c f[x] dx = -(c_∫-a f[x] dx)

---

Latex:

---

Latex:
\mforall{}[a,c:\mBbbR{}].  \mforall{}[f:\{f:[rmin(a;c),  rmax(a;c)]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[rmin(a;c),  rmax(a;c)])\}  ].
    (a\_\mint{}\msupminus{}c  f[x]  dx  =  -(c\_\mint{}\msupminus{}a  f[x]  dx))


By

---

Latex:
(Auto  THEN  (InstLemma  `integral-additive`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Try  (Trivial)))

---

Home Index