---

Step * 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))
⊢ (x * x) ≤ r(((n * 2) + 2) * ((n * 2) + 1))
BY
{ (RWO "3" 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))
⊢ (b * b) ≤ (((n * 2) + 2) * ((n * 2) + 1))

---

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{}  (x  *  x)  \mleq{}  r(((n  *  2)  +  2)  *  ((n  *  2)  +  1))


By

---

Latex:
(RWO  "3"  0  THEN  Auto')

---

Home Index