---

Step * of Lemma rdiv-factorial-lemma2

∀x:ℝ. ∀b:ℕ.  (((x * x) ≤ r(b * b)) ⇒ (∀n:ℕ. (((b ÷ 2) ≤ n) ⇒ ((x * x) ≤ (r((2 * (n + 1))!)/r((2 * n)!))))))
BY
{ (Auto
   THEN (InstLemma `div_rem_sum` [⌜b⌝;⌜2⌝]⋅ THENA Auto)
   THEN ((InstLemma `rem_bounds_1` [⌜b⌝;⌜2⌝]⋅ THENA Auto)
         THEN (InstLemma `rdiv-factorial-lemma1` [⌜n⌝]⋅ THENA Auto)
         THEN RWO "-1" 0
         THEN Auto')⋅) }

1
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))
⊢ (x * x) ≤ r(((n * 2) + 2) * ((n * 2) + 1))

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}b:\mBbbN{}.
    (((x  *  x)  \mleq{}  r(b  *  b))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (((b  \mdiv{}  2)  \mleq{}  n)  {}\mRightarrow{}  ((x  *  x)  \mleq{}  (r((2  *  (n  +  1))!)/r((2  *  n)!))))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `rdiv-factorial-lemma1`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  RWO  "-1"  0
              THEN  Auto')\mcdot{})

---

Home Index