---

Step * of Lemma rmul-is-negative1

∀x,y:ℝ.  (((x * y) < r0) ⇒ (x ≠ r0 ∨ y ≠ r0))
BY
{ ((Auto THEN Unfold `rneq` 0)
   THEN All (RWO "rless-iff2" )
   THEN Auto
   THEN (RepUR ``int-to-real`` 0 THEN (RW IntNormC 0 THENA Auto))
   THEN RepUR ``int-to-real`` (-1)
   THEN (RW IntNormC (-1) THENA Auto)
   THEN RepUR ``rmul`` (-1)
   THEN RepeatFor 2 ((CallByValueReduce (-1) THENA Auto))
   THEN D -1
   THEN RepUR ``accelerate reg-seq-mul`` (-1)
   THEN CallByValueReduce (-1)
   THEN Auto
   THEN Reduce (-1)
   THEN CallByValueReduce (-1)
   THEN Auto) }

1
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. (((x ((2 * (imax(|x 1|;|y 1|) + 4)) * n)) * (y ((2 * (imax(|x 1|;|y 1|) + 4)) * n))) ÷ 2
* (2 * (imax(|x 1|;|y 1|) + 4))
* n ÷ 2 * (imax(|x 1|;|y 1|) + 4))
+ 4 < 2 * n * 0
⊢ ((∃n:ℕ+. (x n) + 4 < 2 * n * 0) ∨ (∃n:ℕ+. (2 * n * 0) + 4 < x n))
∨ (∃n:ℕ+. (y n) + 4 < 2 * n * 0)
∨ (∃n:ℕ+. (2 * n * 0) + 4 < y n)

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    (((x  *  y)  <  r0)  {}\mRightarrow{}  (x  \mneq{}  r0  \mvee{}  y  \mneq{}  r0))


By

---

Latex:
((Auto  THEN  Unfold  `rneq`  0)
  THEN  All  (RWO  "rless-iff2"  )
  THEN  Auto
  THEN  (RepUR  ``int-to-real``  0  THEN  (RW  IntNormC  0  THENA  Auto))
  THEN  RepUR  ``int-to-real``  (-1)
  THEN  (RW  IntNormC  (-1)  THENA  Auto)
  THEN  RepUR  ``rmul``  (-1)
  THEN  RepeatFor  2  ((CallByValueReduce  (-1)  THENA  Auto))
  THEN  D  -1
  THEN  RepUR  ``accelerate  reg-seq-mul``  (-1)
  THEN  CallByValueReduce  (-1)
  THEN  Auto
  THEN  Reduce  (-1)
  THEN  CallByValueReduce  (-1)
  THEN  Auto)

---

Home Index