---

Step * of Lemma rnexp-rdiv

∀[y,x:ℝ].  ∀[n:ℕ]. ((y^n/x^n) = (y/x)^n) supposing x ≠ r0
BY
{ EAuto 1 }

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

---

Latex:

---

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


By

---

Latex:
EAuto  1

---

Home Index