---

Step * of Lemma rless-int-fractions

∀a,b:ℤ. ∀c,d:ℕ+.  ((r(a)/r(c)) < (r(b)/r(d)) ⇐⇒ a * d < b * c)
BY
{ Auto }

1
1. a : ℤ@i
2. b : ℤ@i
3. c : ℕ+@i
4. d : ℕ+@i
5. (r(a)/r(c)) < (r(b)/r(d))@i
⊢ a * d < b * c

2
1. a : ℤ@i
2. b : ℤ@i
3. c : ℕ+@i
4. d : ℕ+@i
5. a * d < b * c@i
⊢ (r(a)/r(c)) < (r(b)/r(d))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.  \mforall{}c,d:\mBbbN{}\msupplus{}.    ((r(a)/r(c))  <  (r(b)/r(d))  \mLeftarrow{}{}\mRightarrow{}  a  *  d  <  b  *  c)


By

---

Latex:
Auto

---

Home Index