---

Step * of Lemma rnexp_step

∀[x:ℝ]. ∀[n:ℕ+].  (x^n = (x^n - 1 * x))
BY
{ (Auto THEN (RW (AddrC [1] (LemmaC `rnexp_unroll`)) 0 THEN Auto) THEN RepeatFor 2 (AutoSplit)) }

1
1. x : ℝ
2. n : ℕ+
3. n ≠ 0
4. n = 1 ∈ ℤ
⊢ x = (x^n - 1 * x)

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    (x\^{}n  =  (x\^{}n  -  1  *  x))


By

---

Latex:
(Auto  THEN  (RW  (AddrC  [1]  (LemmaC  `rnexp\_unroll`))  0  THEN  Auto)  THEN  RepeatFor  2  (AutoSplit))

---

Home Index