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


1. : ℤ
2. 0 < n
3. ∀v1:ℤ. ∀v2:ℕ+.
     (mk-rational(v1^(n 1);v2^(n 1)) (Y itop,ub. if 0 <ub then (itop (ub 1)) * <v1, v2> else 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`` THEN (CallByValueReduce THENA Auto))
      THEN RepUR ``mk-rational`` 0
      THEN Fold `mk-rational` 0
      THEN (CallByValueReduce THENA Auto)
      THEN RepUR ``mk-rational`` 0
      THEN Fold `mk-rational` 0)xxx }

1
1. : ℤ
2. 0 < n
3. ∀v1:ℤ. ∀v2:ℕ+.
     (mk-rational(v1^(n 1);v2^(n 1)) (Y itop,ub. if 0 <ub then (itop (ub 1)) * <v1, v2> else 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