---

Step * of Lemma rnexp-is-positive

No Annotations
∀i:ℕ+. ∀x:ℝ.  ((r0 < |x^i|) ⇒ (r0 < |x|))
BY
{ (InductionOnNat THEN Auto THEN (RWO "rnexp-req" (-1) THENA Auto) THEN Reduce (-1)) }

1
1. i : ℤ
2. 0 < i
3. ∀x:ℝ. ((r0 < |x^i|) ⇒ (r0 < |x|))
4. x : ℝ
5. r0 < |if (i + 1 =z 0) then r1 else x * x^(i + 1) - 1 fi |
⊢ r0 < |x|

---

Latex:

---

Latex:
No  Annotations
\mforall{}i:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbR{}.    ((r0  <  |x\^{}i|)  {}\mRightarrow{}  (r0  <  |x|))


By

---

Latex:
(InductionOnNat  THEN  Auto  THEN  (RWO  "rnexp-req"  (-1)  THENA  Auto)  THEN  Reduce  (-1))

---

Home Index