---

Step * 1 2 2 1 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) * v1;v2^(n - 1) * v2) ∈ ℚ
BY
{ xxx(EqCD THEN Auto THEN RW (AddrC [2] (LemmaC `exp_step`)) 0 THEN Auto)xxx }

---

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)  *  v1;v2\^{}(n  -  1)  *  v2)


By

---

Latex:
xxx(EqCD  THEN  Auto  THEN  RW  (AddrC  [2]  (LemmaC  `exp\_step`))  0  THEN  Auto)xxx

---

Home Index