---

Step * 1 of Lemma q-ceil_functionality


1. a : ℚ
2. b : ℚ
3. a ≤ b
4. q-ceil(a) - 1 < a ∧ (a ≤ q-ceil(a))
5. q-ceil(b) - 1 < b ∧ (b ≤ q-ceil(b))
6. ¬(q-ceil(a) ≤ q-ceil(b))
7. q-ceil(b) ≤ (q-ceil(a) - 1)
⊢ q-ceil(a) ≤ q-ceil(b)
BY
{ (Auto THEN (RelRST THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  a  \mleq{}  b
4.  q-ceil(a)  -  1  <  a  \mwedge{}  (a  \mleq{}  q-ceil(a))
5.  q-ceil(b)  -  1  <  b  \mwedge{}  (b  \mleq{}  q-ceil(b))
6.  \mneg{}(q-ceil(a)  \mleq{}  q-ceil(b))
7.  q-ceil(b)  \mleq{}  (q-ceil(a)  -  1)
\mvdash{}  q-ceil(a)  \mleq{}  q-ceil(b)


By

---

Latex:
(Auto  THEN  (RelRST  THEN  Auto)\mcdot{})

---

Home Index