---

Step * 1 2 of Lemma qexp-eq-q-rng-nexp


1. n : ℕ
2. r : ℚ
3. v1 : ℤ
4. v2 : ℕ+
5. qrep(r) = <v1, v2> ∈ (ℤ × ℕ+)
⊢ mk-rational(v1^n;v2^n) = q-rng-nexp(<v1, v2>;n) ∈ ℚ
BY
{ xxx(ThinVar `r'
      THEN RepUR ``q-rng-nexp rng_nexp mon_nat_op nat_op itop`` 0
      THEN (RepeatFor 2 (MoveToConcl (-1)) THEN NatInd 1)
      THEN Reduce 0
      THEN Auto
      THEN (RW (AddrC [3] UnrollRecursionC) 0 THEN Reduce 0 THEN Try ((AutoSplit THEN RWO "3<" 0 THEN Auto)))⋅)xxx }

1
1. n : ℤ
2. v1 : ℤ
3. v2 : ℕ+
⊢ mk-rational(1;1) = 1 ∈ ℚ

2
1. n : ℤ
2. 0 < n
3. ∀v1:ℤ. ∀v2:ℕ+.
     (mk-rational(v1^(n - 1);v2^(n - 1)) = (Y (λitop,ub. if 0 <z ub then (itop (ub - 1)) * <v1, v2> else 1 fi ) (n - 1))\000C ∈ ℚ)
4. v1 : ℤ
5. v2 : ℕ+
6. 0 < n
⊢ mk-rational(v1^n;v2^n) = (mk-rational(v1^(n - 1);v2^(n - 1)) * <v1, v2>) ∈ ℚ

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  r  :  \mBbbQ{}
3.  v1  :  \mBbbZ{}
4.  v2  :  \mBbbN{}\msupplus{}
5.  qrep(r)  =  <v1,  v2>
\mvdash{}  mk-rational(v1\^{}n;v2\^{}n)  =  q-rng-nexp(<v1,  v2>n)


By

---

Latex:
xxx(ThinVar  `r'
        THEN  RepUR  ``q-rng-nexp  rng\_nexp  mon\_nat\_op  nat\_op  itop``  0
        THEN  (RepeatFor  2  (MoveToConcl  (-1))  THEN  NatInd  1)
        THEN  Reduce  0
        THEN  Auto
        THEN  (RW  (AddrC  [3]  UnrollRecursionC)  0
                    THEN  Reduce  0
                    THEN  Try  ((AutoSplit  THEN  RWO  "3<"  0  THEN  Auto)))\mcdot{})xxx

---

Home Index