---

Step * of Lemma rdiv-factorial-lemma3

∀x:ℝ. ∀b:ℕ.
  (((x * x) ≤ r(b * b)) ⇒ (∀n:ℕ. (((b ÷ 2) ≤ n) ⇒ ((x * x) ≤ (r(((2 * (n + 1)) + 1)!)/r(((2 * n) + 1)!))))))
BY
{ (InstLemma `rdiv-factorial-lemma2` [] THEN RepeatFor 5 ((ParallelLast' THENA Auto)) THEN RWO "-1" 0 THEN Auto) }

1
1. x : ℝ
2. b : ℕ
3. (x * x) ≤ r(b * b)
4. n : ℕ
5. (b ÷ 2) ≤ n
6. (x * x) ≤ (r((2 * (n + 1))!)/r((2 * n)!))
⊢ (r((2 * (n + 1))!)/r((2 * n)!)) ≤ (r(((2 * (n + 1)) + 1)!)/r(((2 * n) + 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))  +  1)!)/r(((2  *  n)  +  1)!))))))


By

---

Latex:
(InstLemma  `rdiv-factorial-lemma2`  []
  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index