---

Step * of Lemma qtruncate-property

∀[q:ℚ]. ∀[N:ℕ+].  (qtruncate(q;N) - (1/N) < q ∧ (q ≤ qtruncate(q;N)))
BY
{ ((UnivCD THENA Auto) THEN (InstLemma `q-ceil-property` [⌜q * N⌝]⋅ THENA Auto)) }

1
1. q : ℚ
2. N : ℕ+
3. q-ceil(q * N) - 1 < q * N ∧ ((q * N) ≤ q-ceil(q * N))
⊢ qtruncate(q;N) - (1/N) < q ∧ (q ≤ qtruncate(q;N))

---

Latex:

---

Latex:
\mforall{}[q:\mBbbQ{}].  \mforall{}[N:\mBbbN{}\msupplus{}].    (qtruncate(q;N)  -  (1/N)  <  q  \mwedge{}  (q  \mleq{}  qtruncate(q;N)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (InstLemma  `q-ceil-property`  [\mkleeneopen{}q  *  N\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index