---

Step * 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
⊢ (|x|^(2 * k) + 3/r(((2 * k) + 3)!)) ≤ (r1/r(N))
BY
{ ((Assert r0 < r(a)^(2 * k) + 3 BY EAuto 1) THEN (RWO "rnexp-rdiv<" (-2) THENA Auto)) }

1
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^(2 * k) + 3/r(a)^(2 * k) + 3)
9. r0 < r(a)^(2 * k) + 3
⊢ (|x|^(2 * k) + 3/r(((2 * k) + 3)!)) ≤ (r1/r(N))

---

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
\mvdash{}  (|x|\^{}(2  *  k)  +  3/r(((2  *  k)  +  3)!))  \mleq{}  (r1/r(N))


By

---

Latex:
((Assert  r0  <  r(a)\^{}(2  *  k)  +  3  BY  EAuto  1)  THEN  (RWO  "rnexp-rdiv<"  (-2)  THENA  Auto))

---

Home Index