---

Step * of Lemma rmul_preserves_rneq

∀a,b,x:ℝ.  (x ≠ r0 ⇒ a ≠ b ⇒ x * a ≠ x * b)
BY
{ (Auto THEN (All (Unfold `rneq`)⋅ THEN SplitOrHyps)) }

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

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

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (All  (Unfold  `rneq`)\mcdot{}  THEN  SplitOrHyps))

---

Home Index