---

Step * of Lemma rleq-int-fractions3

∀[a,b:ℤ]. ∀[d:ℕ+].  uiff((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{}].    uiff((r(b)/r(d))  \mleq{}  r(a);b  \mleq{}  (a  *  d))


By

---

Latex:
Auto

---

Home Index