---

Step * 1 1 1 1 2 1 of Lemma sine-exists


1. x : ℝ
2. b : ℕ
3. |x| ≤ r(b)
4. ∀n:ℕ. (r0 ≤ (x^2 * n/r(((2 * n) + 1)!)))
5. i : ℕ@i
6. b ÷ 2 < i
7. (x * x) ≤ (r(((2 * (i + 1)) + 1)!)/r(((2 * i) + 1)!))
8. r0 ≤ (x^2 * i/r(((2 * i) + 1)!))
⊢ (x^2 * (i + 1)/r(((2 * (i + 1)) + 1)!)) ≤ (x^2 * i/r(((2 * i) + 1)!))
BY
{ (Thin (-1)
   THEN MoveToConcl (-1)
   THEN (Assert r0 < r(((2 * (i + 1)) + 1)!) BY
               Auto)
   THEN (Assert r0 < r(((2 * i) + 1)!) BY
               Auto)
   THEN (MoveToConcl (-1) THEN (GenConclAtAddrType ⌜ℝ⌝ [1;2] ⋅ THENA Auto) THEN Thin (-1))
   THEN MoveToConcl (-2)
   THEN (GenConclAtAddrType ⌜ℝ⌝ [1;2] ⋅ THENA Auto)
   THEN All Thin) }

1
1. x : ℝ
2. i : ℕ@i
3. v : ℝ@i
4. v1 : ℝ@i
⊢ (r0 < v1) ⇒ (r0 < v) ⇒ ((x * x) ≤ (v1/v)) ⇒ ((x^2 * (i + 1)/v1) ≤ (x^2 * i/v))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  b  :  \mBbbN{}
3.  |x|  \mleq{}  r(b)
4.  \mforall{}n:\mBbbN{}.  (r0  \mleq{}  (x\^{}2  *  n/r(((2  *  n)  +  1)!)))
5.  i  :  \mBbbN{}@i
6.  b  \mdiv{}  2  <  i
7.  (x  *  x)  \mleq{}  (r(((2  *  (i  +  1))  +  1)!)/r(((2  *  i)  +  1)!))
8.  r0  \mleq{}  (x\^{}2  *  i/r(((2  *  i)  +  1)!))
\mvdash{}  (x\^{}2  *  (i  +  1)/r(((2  *  (i  +  1))  +  1)!))  \mleq{}  (x\^{}2  *  i/r(((2  *  i)  +  1)!))


By

---

Latex:
(Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  (Assert  r0  <  r(((2  *  (i  +  1))  +  1)!)  BY
                          Auto)
  THEN  (Assert  r0  <  r(((2  *  i)  +  1)!)  BY
                          Auto)
  THEN  (MoveToConcl  (-1)  THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbR{}\mkleeneclose{}  [1;2]  \mcdot{}  THENA  Auto)  THEN  Thin  (-1))
  THEN  MoveToConcl  (-2)
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbR{}\mkleeneclose{}  [1;2]  \mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index