---

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


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>) ∈ ℚ
BY
{ xxx((RepUR ``qmul`` 0 THEN (CallByValueReduce 0 THENA Auto))
      THEN RepUR ``mk-rational`` 0
      THEN Fold `mk-rational` 0
      THEN (CallByValueReduce 0 THENA Auto)
      THEN RepUR ``mk-rational`` 0
      THEN Fold `mk-rational` 0)xxx }

1
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) * v1;v2^(n - 1) * v2) ∈ ℚ

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}v1:\mBbbZ{}.  \mforall{}v2:\mBbbN{}\msupplus{}.
          (mk-rational(v1\^{}(n  -  1);v2\^{}(n  -  1))
          =  (Y  (\mlambda{}itop,ub.  if  0  <z  ub  then  (itop  (ub  -  1))  *  <v1,  v2>  else  1  fi  )  (n  -  1)))
4.  v1  :  \mBbbZ{}
5.  v2  :  \mBbbN{}\msupplus{}
6.  0  <  n
\mvdash{}  mk-rational(v1\^{}n;v2\^{}n)  =  (mk-rational(v1\^{}(n  -  1);v2\^{}(n  -  1))  *  <v1,  v2>)


By

---

Latex:
xxx((RepUR  ``qmul``  0  THEN  (CallByValueReduce  0  THENA  Auto))
        THEN  RepUR  ``mk-rational``  0
        THEN  Fold  `mk-rational`  0
        THEN  (CallByValueReduce  0  THENA  Auto)
        THEN  RepUR  ``mk-rational``  0
        THEN  Fold  `mk-rational`  0)xxx

---

Home Index