---

Step * of Lemma rinv_preserves_rneq

∀a,b:ℝ.  (a ≠ r0 ⇒ b ≠ r0 ⇒ a ≠ b ⇒ (r1/a) ≠ (r1/b))
BY
{ (Auto THEN (ParallelLast THEN SplitOrHyps)) }

1
1. a : ℝ
2. b : ℝ
3. a ≠ r0
4. b ≠ r0
5. a < b
⊢ ((r1/a) < (r1/b)) ∨ ((r1/b) < (r1/a))

2
1. a : ℝ
2. b : ℝ
3. a ≠ r0
4. b ≠ r0
5. b < a
⊢ ((r1/a) < (r1/b)) ∨ ((r1/b) < (r1/a))

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (ParallelLast  THEN  SplitOrHyps))

---

Home Index