---

Step * 1 of Lemma rnexp2-positive-iff


1. x : ℝ
2. r0 < x^2
⊢ x ≠ r0
BY
{ (InstLemma `square-rless-implies` [⌜r0⌝;⌜|x|⌝]⋅ THEN EAuto 1) }

1
.....antecedent..... 
1. x : ℝ
2. r0 < x^2
⊢ r0^2 < |x|^2

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  r0  <  x\^{}2
\mvdash{}  x  \mneq{}  r0


By

---

Latex:
(InstLemma  `square-rless-implies`  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}|x|\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index