---

Step * of Lemma q-ceil_functionality

∀[a,b:ℚ].  q-ceil(a) ≤ q-ceil(b) supposing a ≤ b
BY
{ (Auto
   THEN (InstLemma `q-ceil-property` [⌜a⌝]⋅ THENA Auto)
   THEN (InstLemma `q-ceil-property` [⌜b⌝]⋅ THENA Auto)
   THEN SupposeNot
   THEN (Assert q-ceil(b) ≤ (q-ceil(a) - 1) BY
               Auto')
   THEN (RWO "qle-int<" (-1) THENA Auto)
   THEN (RWO "qsub-sub<" (-1) THENA Auto)) }

1
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)

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbQ{}].    q-ceil(a)  \mleq{}  q-ceil(b)  supposing  a  \mleq{}  b


By

---

Latex:
(Auto
  THEN  (InstLemma  `q-ceil-property`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `q-ceil-property`  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SupposeNot
  THEN  (Assert  q-ceil(b)  \mleq{}  (q-ceil(a)  -  1)  BY
                          Auto')
  THEN  (RWO  "qle-int<"  (-1)  THENA  Auto)
  THEN  (RWO  "qsub-sub<"  (-1)  THENA  Auto))

---

Home Index