---

Step * of Lemma rnexp-rleq-iff

∀x,y:ℝ.  ((r0 ≤ x) ⇒ (r0 ≤ y) ⇒ (∀n:ℕ+. (x ≤ y ⇐⇒ x^n ≤ y^n)))
BY
{ EAuto 1 }

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

---

Latex:

---

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


By

---

Latex:
EAuto  1

---

Home Index