---

Step * 1 of Lemma integral-rnexp-from-0


1. b : ℝ
2. m : ℕ
⊢ (b^m + 1 - r0^m + 1/r(m + 1)) = (b^m + 1/r(m + 1))
BY
{ ((BLemma `rdiv_functionality` THEN Auto) THEN RWO "rnexp0" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  b  :  \mBbbR{}
2.  m  :  \mBbbN{}
\mvdash{}  (b\^{}m  +  1  -  r0\^{}m  +  1/r(m  +  1))  =  (b\^{}m  +  1/r(m  +  1))


By

---

Latex:
((BLemma  `rdiv\_functionality`  THEN  Auto)  THEN  RWO  "rnexp0"  0  THEN  Auto)

---

Home Index