---

Step * 2 1 1 1 1 2 1 1 of Lemma logseq-property


1. M : ℕ+
⊢ ((r1/r(2 * M)) + (r1/r(2 * M))) ≤ (r1/r(M))
BY
{ (Assert ((r1/r(2 * M)) + (r1/r(2 * M))) = (r1/r(M)) BY
         (RWO  "rmul-int<" 0 THEN Auto)) }

1
1. M : ℕ+
2. ((r1/r(2 * M)) + (r1/r(2 * M))) = (r1/r(M))
⊢ ((r1/r(2 * M)) + (r1/r(2 * M))) ≤ (r1/r(M))

---

Latex:

---

Latex:

1.  M  :  \mBbbN{}\msupplus{}
\mvdash{}  ((r1/r(2  *  M))  +  (r1/r(2  *  M)))  \mleq{}  (r1/r(M))


By

---

Latex:
(Assert  ((r1/r(2  *  M))  +  (r1/r(2  *  M)))  =  (r1/r(M))  BY
              (RWO    "rmul-int<"  0  THEN  Auto))

---

Home Index