---

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


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index