---

Step * 1 1 1 1 1 of Lemma sine-approx-for-small


1. a : {2...}
2. N : ℕ+
3. x : {x:ℝ| |x| ≤ (r1/r(a))} 
4. (r1/r(a)) ≤ (r1/r(2))
5. |x| ≤ (r1/r(2))
6. k : ℕ
7. N ≤ (a^((2 * k) + 3) * ((2 * k) + 3)!)
8. |x|^(2 * k) + 3 ≤ (r1/r(a^((2 * k) + 3)))
9. r0 < r(a)^(2 * k) + 3
⊢ (|x|^(2 * k) + 3/r(((2 * k) + 3)!)) ≤ (r1/r(N))
BY
{ (RepeatFor 2 (MoveToConcl (-2))
   THEN (GenConclTerm ⌜|x|^(2 * k) + 3⌝⋅ THENA Auto)
   THEN (GenConcl ⌜a^((2 * k) + 3) = M ∈ ℕ+⌝⋅ THENA Auto)
   THEN (GenConcl ⌜((2 * k) + 3)! = B ∈ ℕ+⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto
   THEN (nRMul ⌜r(B)⌝ 0⋅ THENA Auto)
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \{2...\}
2.  N  :  \mBbbN{}\msupplus{}
3.  x  :  \{x:\mBbbR{}|  |x|  \mleq{}  (r1/r(a))\} 
4.  (r1/r(a))  \mleq{}  (r1/r(2))
5.  |x|  \mleq{}  (r1/r(2))
6.  k  :  \mBbbN{}
7.  N  \mleq{}  (a\^{}((2  *  k)  +  3)  *  ((2  *  k)  +  3)!)
8.  |x|\^{}(2  *  k)  +  3  \mleq{}  (r1/r(a\^{}((2  *  k)  +  3)))
9.  r0  <  r(a)\^{}(2  *  k)  +  3
\mvdash{}  (|x|\^{}(2  *  k)  +  3/r(((2  *  k)  +  3)!))  \mleq{}  (r1/r(N))


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-2))
  THEN  (GenConclTerm  \mkleeneopen{}|x|\^{}(2  *  k)  +  3\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}a\^{}((2  *  k)  +  3)  =  M\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}((2  *  k)  +  3)!  =  B\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto
  THEN  (nRMul  \mkleeneopen{}r(B)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index