---

Step * of Lemma rnexp-req-iff

∀n:ℕ+. ∀x,y:ℝ.  ((r0 ≤ x) ⇒ (r0 ≤ y) ⇒ (x = y ⇐⇒ x^n = y^n))
BY
{ (Auto THEN Try ((RWO "-1" 0 THEN Auto))) }

1
1. n : ℕ+@i
2. x : ℝ@i
3. y : ℝ@i
4. r0 ≤ x@i
5. r0 ≤ y@i
6. x^n = y^n@i
⊢ x = y

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x,y:\mBbbR{}.    ((r0  \mleq{}  x)  {}\mRightarrow{}  (r0  \mleq{}  y)  {}\mRightarrow{}  (x  =  y  \mLeftarrow{}{}\mRightarrow{}  x\^{}n  =  y\^{}n))


By

---

Latex:
(Auto  THEN  Try  ((RWO  "-1"  0  THEN  Auto)))

---

Home Index