---

Step * 1 of Lemma cosine-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) + 2) * ((2 * k) + 2)!)
⊢ ((|x|^(2 * k) + 2/r(((2 * k) + 2)!)) + (r1/r(N))) ≤ (r(2)/r(N))
BY
{ (Assert ⌜(|x|^(2 * k) + 2/r(((2 * k) + 2)!)) ≤ (r1/r(N))⌝⋅
THENM (RWO  "-1" 0 THEN Auto THEN RWO "radd-int-fractions" 0 THEN Auto)
) }

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


By

---

Latex:
(Assert  \mkleeneopen{}(|x|\^{}(2  *  k)  +  2/r(((2  *  k)  +  2)!))  \mleq{}  (r1/r(N))\mkleeneclose{}\mcdot{}
THENM  (RWO    "-1"  0  THEN  Auto  THEN  RWO  "radd-int-fractions"  0  THEN  Auto)
)

---

Home Index