---

Step * of Lemma rless-int-fractions2

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

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index