---

Step * of Lemma exp_zero_q

∀[e:ℚ]. (e ↑ 0 = 1 ∈ ℚ)
BY
{ xxx(Auto
      THEN Unfold `qexp` 0
      THEN (CallByValueReduce 0 THENA Auto)
      THEN (GenConclAtAddr [2;1] THENA Auto)
      THEN D -2
      THEN Reduce 0)xxx }

1
1. e : ℚ
2. v1 : ℤ
3. v2 : ℕ+
4. qrep(e) = <v1, v2> ∈ (ℤ × ℕ+)
⊢ mk-rational(v1^0;v2^0) = 1 ∈ ℚ

---

Latex:

---

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


By

---

Latex:
xxx(Auto
        THEN  Unfold  `qexp`  0
        THEN  (CallByValueReduce  0  THENA  Auto)
        THEN  (GenConclAtAddr  [2;1]  THENA  Auto)
        THEN  D  -2
        THEN  Reduce  0)xxx

---

Home Index