---

Step * 1 of Lemma qexp1


1. q : ℚ
⊢ q-rng-nexp(q;1) = q ∈ ℚ
BY
{ (RepUR ``q-rng-nexp rng_nexp mon_nat_op nat_op`` 0 THEN RepeatFor 2 ((RecUnfold `itop` 0 THEN Reduce 0)) THEN QNorm 0)
⋅ }

---

Latex:

---

Latex:

1.  q  :  \mBbbQ{}
\mvdash{}  q-rng-nexp(q;1)  =  q


By

---

Latex:
(RepUR  ``q-rng-nexp  rng\_nexp  mon\_nat\_op  nat\_op``  0
  THEN  RepeatFor  2  ((RecUnfold  `itop`  0  THEN  Reduce  0))
  THEN  QNorm  0)\mcdot{}

---

Home Index