---

Step * of Lemma integral-is-Riemann

∀[a,b:ℝ]. ∀[f:{f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} ].
  a_∫-b f[x] dx = ∫ f[x] dx on [a, b] supposing a ≤ b
BY
{ (Intros THEN (Assert a ≤ b BY (Unhide THEN Auto)) THEN Unfold `integral` 0) }

1
1. [a] : ℝ
2. [b] : ℝ
3. [f] : {f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} 
4. [%] : a ≤ b
5. a ≤ b
⊢ (∫ f[x] dx on [rmin(a;b), b] - ∫ f[x] dx on [rmin(a;b), a]) = ∫ f[x] dx on [a, b]

---

Latex:

---

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


By

---

Latex:
(Intros  THEN  (Assert  a  \mleq{}  b  BY  (Unhide  THEN  Auto))  THEN  Unfold  `integral`  0)

---

Home Index