---

Step * of Lemma inverse-rpower

∀[x:ℝ]. ∀[n:ℕ]. ((r1/x^n) = (r1/x)^n) supposing x ≠ r0
BY
{ (Auto THEN EAuto 1 THEN (Assert ∀k:ℕ. x^k ≠ r0 BY EAuto 1)) }

1
1. x : ℝ
2. x ≠ r0
3. n : ℕ
4. ∀k:ℕ. x^k ≠ r0
⊢ (r1/x^n) = (r1/x)^n

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[n:\mBbbN{}].  ((r1/x\^{}n)  =  (r1/x)\^{}n)  supposing  x  \mneq{}  r0


By

---

Latex:
(Auto  THEN  EAuto  1  THEN  (Assert  \mforall{}k:\mBbbN{}.  x\^{}k  \mneq{}  r0  BY  EAuto  1))

---

Home Index