Step * of Lemma rneq-rmul

x,y,a,b:ℝ.  (x y ≠  (x ≠ a ∨ y ≠ b))
BY
(RWO "rneq-iff-rabs" THEN Auto) }

1
1. : ℝ
2. : ℝ
3. : ℝ
4. : ℝ
5. r0 < |(x y) b|
⊢ (r0 < |x a|) ∨ (r0 < |y b|)


Latex:


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


By


Latex:
(RWO  "rneq-iff-rabs"  0  THEN  Auto)




Home Index