---

Step * of Lemma exp_unroll_q

No Annotations
∀[n:ℕ+]. ∀[e:ℚ].  (e ↑ n = (e ↑ n - 1 * e) ∈ ℚ)
BY
{ ((RWO "qexp-eq-q-rng-nexp" 0 THENA Auto)
   THEN (ProveSpecializedLemmaWReduce rng_nexp_unroll) 0 [⌜parm{i}⌝;⌜<ℚ+*>⌝]⋅
   THEN Fold `q-rng-nexp` (-1)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[e:\mBbbQ{}].    (e  \muparrow{}  n  =  (e  \muparrow{}  n  -  1  *  e))


By

---

Latex:
((RWO  "qexp-eq-q-rng-nexp"  0  THENA  Auto)
  THEN  (ProveSpecializedLemmaWReduce  rng\_nexp\_unroll)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}<\mBbbQ{}+*>\mkleeneclose{}]\mcdot{}
  THEN  Fold  `q-rng-nexp`  (-1)
  THEN  Auto)

---

Home Index