---

Step * 1 of Lemma integral-additive-lemma


1. m : ℝ
2. M : ℝ
3. m ≤ M
4. f : {f:[m, M] ⟶ℝ| ifun(f;[m, M])} 
5. a : {x:ℝ| x ∈ [m, M]} 
6. b : {x:ℝ| x ∈ [m, M]} 
7. λx.f[x] ∈ {f:[m, M] ⟶ℝ| ifun(f;[m, M])} 
⊢ (∫ f[x] dx on [rmin(a;b), b] - ∫ f[x] dx on [rmin(a;b), a]) = (∫ f[x] dx on [m, b] - ∫ f[x] dx on [m, a])
BY
{ ((Assert m ≤ rmin(a;b) BY
          (BLemma `rmin_ub` THEN Auto))
   THEN (Assert rmin(a;b) ≤ M BY
               (BLemma `rmin_lb` THEN Auto))
   THEN (InstLemma `Riemann-integral-additive` [⌜m⌝;⌜b⌝;⌜f⌝;⌜rmin(a;b)⌝]⋅
         THENA ((Try (DoSubsume) THEN Auto) THEN Try ((BLemma `rmin_ub` THEN Auto)))
         )
   THEN (InstLemma `Riemann-integral-additive` [⌜m⌝;⌜a⌝;⌜f⌝;⌜rmin(a;b)⌝]⋅
         THENA ((Try (DoSubsume) THEN Auto) THEN Try ((BLemma `rmin_ub` THEN Auto)))
         )) }

1
1. m : ℝ
2. M : ℝ
3. m ≤ M
4. f : {f:[m, M] ⟶ℝ| ifun(f;[m, M])} 
5. a : {x:ℝ| x ∈ [m, M]} 
6. b : {x:ℝ| x ∈ [m, M]} 
7. λx.f[x] ∈ {f:[m, M] ⟶ℝ| ifun(f;[m, M])} 
8. m ≤ rmin(a;b)
9. rmin(a;b) ≤ M
10. ∫ f[x] dx on [m, b] = (∫ f[x] dx on [m, rmin(a;b)] + ∫ f[x] dx on [rmin(a;b), b])
11. ∫ f[x] dx on [m, a] = (∫ f[x] dx on [m, rmin(a;b)] + ∫ f[x] dx on [rmin(a;b), a])
⊢ (∫ f[x] dx on [rmin(a;b), b] - ∫ f[x] dx on [rmin(a;b), a]) = (∫ f[x] dx on [m, b] - ∫ f[x] dx on [m, a])

---

Latex:

---

Latex:

1.  m  :  \mBbbR{}
2.  M  :  \mBbbR{}
3.  m  \mleq{}  M
4.  f  :  \{f:[m,  M]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[m,  M])\} 
5.  a  :  \{x:\mBbbR{}|  x  \mmember{}  [m,  M]\} 
6.  b  :  \{x:\mBbbR{}|  x  \mmember{}  [m,  M]\} 
7.  \mlambda{}x.f[x]  \mmember{}  \{f:[m,  M]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[m,  M])\} 
\mvdash{}  (\mint{}  f[x]  dx  on  [rmin(a;b),  b]  -  \mint{}  f[x]  dx  on  [rmin(a;b),  a])
=  (\mint{}  f[x]  dx  on  [m,  b]  -  \mint{}  f[x]  dx  on  [m,  a])


By

---

Latex:
((Assert  m  \mleq{}  rmin(a;b)  BY
                (BLemma  `rmin\_ub`  THEN  Auto))
  THEN  (Assert  rmin(a;b)  \mleq{}  M  BY
                          (BLemma  `rmin\_lb`  THEN  Auto))
  THEN  (InstLemma  `Riemann-integral-additive`  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}rmin(a;b)\mkleeneclose{}]\mcdot{}
              THENA  ((Try  (DoSubsume)  THEN  Auto)  THEN  Try  ((BLemma  `rmin\_ub`  THEN  Auto)))
              )
  THEN  (InstLemma  `Riemann-integral-additive`  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}rmin(a;b)\mkleeneclose{}]\mcdot{}
              THENA  ((Try  (DoSubsume)  THEN  Auto)  THEN  Try  ((BLemma  `rmin\_ub`  THEN  Auto)))
              ))

---

Home Index