---

Step * of Lemma qexp-qmul

∀[a,b:ℚ]. ∀[n:ℕ].  (a * b ↑ n = (a ↑ n * b ↑ n) ∈ ℚ)
BY
{ xxx(xxxInductionOnNatxxx
      THEN (RWW "exp_zero_q" 0 THENA Auto)
      THEN Auto
      THEN ((RWO "exp_unroll_q" 0⋅ THENM HypSubst' (-1) 0 THENM QNorm 0) THENA Auto))xxx }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbQ{}].  \mforall{}[n:\mBbbN{}].    (a  *  b  \muparrow{}  n  =  (a  \muparrow{}  n  *  b  \muparrow{}  n))


By

---

Latex:
xxx(xxxInductionOnNatxxx
        THEN  (RWW  "exp\_zero\_q"  0  THENA  Auto)
        THEN  Auto
        THEN  ((RWO  "exp\_unroll\_q"  0\mcdot{}  THENM  HypSubst'  (-1)  0  THENM  QNorm  0)  THENA  Auto))xxx

---

Home Index