---

Step * of Lemma qexp-qdiv

∀[a,b:ℚ].  ∀[n:ℕ]. ((a/b) ↑ n = (a ↑ n/b ↑ n) ∈ ℚ) supposing ¬(b = 0 ∈ ℚ)
BY
{ xxx(xxxInductionOnNatxxx
      THEN Try ((RepeatFor 2 ((RWW "exp_zero_q" 0 THENA Auto)⋅) THEN Auto))
      THEN (InstLemma `qexp-non-zero` [⌜n⌝;⌜b⌝]⋅ THENA Auto)
      THEN (DupHyp (-1)
            THEN (RWO "exp_unroll_q" (-1)⋅ THEN Auto)
            THEN DupHyp (-1)
            THEN RWO "qmul-not-zero" (-1)⋅
            THEN Auto
            THEN ((RWO "exp_unroll_q" 0⋅ THENM HypSubst' (-5) 0 THENM QNorm 0) THENA Auto))⋅)xxx }

1
1. a : ℚ
2. b : ℚ
3. ¬(b = 0 ∈ ℚ)
4. n : ℤ
5. 0 < n
6. (a/b) ↑ n - 1 = (a ↑ n - 1/b ↑ n - 1) ∈ ℚ
7. ¬(b ↑ n = 0 ∈ ℚ)
8. ¬((b ↑ n - 1 * b) = 0 ∈ ℚ)
9. ¬(b ↑ n - 1 = 0 ∈ ℚ)
10. ¬(b = 0 ∈ ℚ)
⊢ ((a ↑ n - 1/b ↑ n - 1) * (a/b)) = (a ↑ n - 1 * a/b ↑ n - 1 * b) ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbQ{}].    \mforall{}[n:\mBbbN{}].  ((a/b)  \muparrow{}  n  =  (a  \muparrow{}  n/b  \muparrow{}  n))  supposing  \mneg{}(b  =  0)


By

---

Latex:
xxx(xxxInductionOnNatxxx
        THEN  Try  ((RepeatFor  2  ((RWW  "exp\_zero\_q"  0  THENA  Auto)\mcdot{})  THEN  Auto))
        THEN  (InstLemma  `qexp-non-zero`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  (DupHyp  (-1)
                    THEN  (RWO  "exp\_unroll\_q"  (-1)\mcdot{}  THEN  Auto)
                    THEN  DupHyp  (-1)
                    THEN  RWO  "qmul-not-zero"  (-1)\mcdot{}
                    THEN  Auto
                    THEN  ((RWO  "exp\_unroll\_q"  0\mcdot{}  THENM  HypSubst'  (-5)  0  THENM  QNorm  0)  THENA  Auto))\mcdot{})xxx

---

Home Index