---

Step * of Lemma integral-rnexp

∀[a,b:ℝ]. ∀[m:ℕ].  (a_∫-b x^m dx = (b^m + 1 - a^m + 1/r(m + 1)))
BY
{ (Auto
   THEN ((InstLemma `ftc-total-integral` [⌜λ2x.x^m⌝;⌜λ2x.(x^m + 1/r(m + 1))⌝]⋅ THENA Auto)
        THENM (RWO "-1" 0 THEN Auto THEN nRMul ⌜r(m + 1)⌝ 0⋅ THEN Auto)
        )
   ) }

1
.....antecedent..... 
1. a : ℝ
2. b : ℝ
3. m : ℕ
⊢ d((x^m + 1/r(m + 1)))/dx = λx.x^m on (-∞, ∞)

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbR{}].  \mforall{}[m:\mBbbN{}].    (a\_\mint{}\msupminus{}b  x\^{}m  dx  =  (b\^{}m  +  1  -  a\^{}m  +  1/r(m  +  1)))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `ftc-total-integral`  [\mkleeneopen{}\mlambda{}\msubtwo{}x.x\^{}m\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(x\^{}m  +  1/r(m  +  1))\mkleeneclose{}]\mcdot{}  THENA  Auto)
            THENM  (RWO  "-1"  0  THEN  Auto  THEN  nRMul  \mkleeneopen{}r(m  +  1)\mkleeneclose{}  0\mcdot{}  THEN  Auto)
            )
  )

---

Home Index