Step
*
1
1
of Lemma
rnexp-rdiv
1. y : ℝ
2. x : ℝ
3. x ≠ r0
4. n : ℕ
5. (r1/x^n) = (r1/x)^n
⊢ (y^n/x^n) = (y/x)^n
BY
{ (RWO "rinv-as-rdiv<" (-1) THENA EAuto 1) }
1
1. y : ℝ
2. x : ℝ
3. x ≠ r0
4. n : ℕ
5. rinv(x^n) = rinv(x)^n
⊢ (y^n/x^n) = (y/x)^n
Latex:
Latex:
1. y : \mBbbR{}
2. x : \mBbbR{}
3. x \mneq{} r0
4. n : \mBbbN{}
5. (r1/x\^{}n) = (r1/x)\^{}n
\mvdash{} (y\^{}n/x\^{}n) = (y/x)\^{}n
By
Latex:
(RWO "rinv-as-rdiv<" (-1) THENA EAuto 1)
Home
Index