---

Step * of Lemma rnexp-rless-odd

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index