---

Step * 1 1 of Lemma inverse-rpower


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)
BY
{ (RWO "-2<" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  x  \mneq{}  r0
3.  \mforall{}k:\mBbbN{}.  x\^{}k  \mneq{}  r0
4.  n  :  \mBbbZ{}
5.  0  <  n
6.  (r1/x\^{}n  -  1)  =  (r1/x)\^{}n  -  1
7.  x  *  x\^{}n  -  1  \mneq{}  r0
\mvdash{}  (r1/x  *  x\^{}n  -  1)  =  ((r1/x)  *  (r1/x)\^{}n  -  1)


By

---

Latex:
(RWO  "-2<"  0  THEN  Auto)

---

Home Index