---

Step * of Lemma ratreal-negative

∀r:ℤ × ℕ+. (ratreal(r) < r0 ⇐⇒ fst(r) < 0)
BY
{ ((D 0 THENA Auto) THEN D 1 THEN Reduce 0 THEN (RWO "ratreal-req" 0 THENA Auto)) }

1
1. r1 : ℤ
2. r2 : ℕ+
⊢ (r(r1)/r(r2)) < r0 ⇐⇒ r1 < 0

---

Latex:

---

Latex:
\mforall{}r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}.  (ratreal(r)  <  r0  \mLeftarrow{}{}\mRightarrow{}  fst(r)  <  0)


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  1  THEN  Reduce  0  THEN  (RWO  "ratreal-req"  0  THENA  Auto))

---

Home Index