---

Step * of Lemma qexp1

∀[q:ℚ]. (q ↑ 1 = q ∈ ℚ)
BY
{ xxx(RWO "qexp-eq-q-rng-nexp" 0 THEN Auto)xxx }

1
1. q : ℚ
⊢ q-rng-nexp(q;1) = q ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[q:\mBbbQ{}].  (q  \muparrow{}  1  =  q)


By

---

Latex:
xxx(RWO  "qexp-eq-q-rng-nexp"  0  THEN  Auto)xxx

---

Home Index