---

Step * 1 2 1 2 1 1 1 1 of Lemma slln-lemma2


1. B : ℚ@i
2. n : ℕ@i
3. 0 ≤ B@i
4. n = 0 ∈ ℤ
⊢ (B * 0) ≤ (2 * B)
BY
{ (QNorm 0 THEN QMul ⌈2⌉ 3⋅ THEN Auto) }

---

Latex:



1.  B  :  \mBbbQ{}@i
2.  n  :  \mBbbN{}@i
3.  0  \mleq{}  B@i
4.  n  =  0
\mvdash{}  (B  *  0)  \mleq{}  (2  *  B)


By

(QNorm  0  THEN  QMul  \mkleeneopen{}2\mkleeneclose{}  3\mcdot{}  THEN  Auto)

---

Home Index