---

Step * of Lemma rless-int-fractions3

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

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index