---

Step * of Lemma rnexp-rless2

∀x,y:ℝ.  ((x < y) ⇒ (r0 < y) ⇒ (∀n:ℕ+. ((↑isOdd(n)) ⇒ (x^n < y^n))))
BY
{ (Auto
   THEN (InstLemma `rnexp-positive` [⌜y⌝;⌜n⌝]⋅ THENA Auto)
   THEN (InstLemma `rless-cases1` [⌜r0⌝;⌜y^n⌝;⌜x^n⌝]⋅ THENA Auto)
   THEN D (-1)⋅
   THEN Auto
   THEN BLemma `rnexp-rless`
   THEN Auto) }

1
1. x : ℝ
2. y : ℝ
3. x < y
4. r0 < y
5. n : ℕ+
6. ↑isOdd(n)
7. r0 < y^n
8. r0 < x^n
⊢ r0 ≤ x

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    ((x  <  y)  {}\mRightarrow{}  (r0  <  y)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}.  ((\muparrow{}isOdd(n))  {}\mRightarrow{}  (x\^{}n  <  y\^{}n))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `rnexp-positive`  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rless-cases1`  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}y\^{}n\mkleeneclose{};\mkleeneopen{}x\^{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  (-1)\mcdot{}
  THEN  Auto
  THEN  BLemma  `rnexp-rless`
  THEN  Auto)

---

Home Index