---

Step * 1 1 of Lemma rdiv-factorial-lemma2


1. x : ℝ@i
2. b : ℕ@i
3. (x * x) ≤ r(b * b)@i
4. n : ℕ@i
5. (b ÷ 2) ≤ n@i
6. b = (((b ÷ 2) * 2) + (b rem 2)) ∈ ℤ
7. 0 ≤ (b rem 2)
8. b rem 2 < 2
9. (r((2 * (n + 1))!)/r((2 * n)!)) = r(((n * 2) + 2) * ((n * 2) + 1))
⊢ (b * b) ≤ (((n * 2) + 2) * ((n * 2) + 1))
BY
{ ((Assert (b * b) ≤ (b * ((n * 2) + 2)) BY
          (BLemma `mul_preserves_le` THEN Auto))
   THEN (Assert (((n * 2) + 2) * b) ≤ (((n * 2) + 2) * ((n * 2) + 1)) BY
               (BLemma `mul_preserves_le` THEN Auto))
   THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}@i
2.  b  :  \mBbbN{}@i
3.  (x  *  x)  \mleq{}  r(b  *  b)@i
4.  n  :  \mBbbN{}@i
5.  (b  \mdiv{}  2)  \mleq{}  n@i
6.  b  =  (((b  \mdiv{}  2)  *  2)  +  (b  rem  2))
7.  0  \mleq{}  (b  rem  2)
8.  b  rem  2  <  2
9.  (r((2  *  (n  +  1))!)/r((2  *  n)!))  =  r(((n  *  2)  +  2)  *  ((n  *  2)  +  1))
\mvdash{}  (b  *  b)  \mleq{}  (((n  *  2)  +  2)  *  ((n  *  2)  +  1))


By

---

Latex:
((Assert  (b  *  b)  \mleq{}  (b  *  ((n  *  2)  +  2))  BY
                (BLemma  `mul\_preserves\_le`  THEN  Auto))
  THEN  (Assert  (((n  *  2)  +  2)  *  b)  \mleq{}  (((n  *  2)  +  2)  *  ((n  *  2)  +  1))  BY
                          (BLemma  `mul\_preserves\_le`  THEN  Auto))
  THEN  Auto')\mcdot{}

---

Home Index