---

Step * 1 of Lemma inverse-rpower


1. x : ℝ
2. x ≠ r0
3. n : ℕ
4. ∀k:ℕ. x^k ≠ r0
⊢ (r1/x^n) = (r1/x)^n
BY
{ (NatInd (-2)
   THEN Reduce 0
   THEN Auto
   THEN (Assert x^n ≠ r0 BY
               Auto)
   THEN ((RWO "rnexp-req" (-1) THENM OReduce (-1)) THENA Auto)
   THEN ((RWO "rnexp-req" 0 THENM OReduce 0) THENA Auto))⋅ }

1
1. x : ℝ
2. x ≠ r0
3. ∀k:ℕ. x^k ≠ r0
4. n : ℤ
5. 0 < n
6. (r1/x^n - 1) = (r1/x)^n - 1
7. x * x^n - 1 ≠ r0
⊢ (r1/x * x^n - 1) = ((r1/x) * (r1/x)^n - 1)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  x  \mneq{}  r0
3.  n  :  \mBbbN{}
4.  \mforall{}k:\mBbbN{}.  x\^{}k  \mneq{}  r0
\mvdash{}  (r1/x\^{}n)  =  (r1/x)\^{}n


By

---

Latex:
(NatInd  (-2)
  THEN  Reduce  0
  THEN  Auto
  THEN  (Assert  x\^{}n  \mneq{}  r0  BY
                          Auto)
  THEN  ((RWO  "rnexp-req"  (-1)  THENM  OReduce  (-1))  THENA  Auto)
  THEN  ((RWO  "rnexp-req"  0  THENM  OReduce  0)  THENA  Auto))\mcdot{}

---

Home Index