---

Step * 1 of Lemma near-arcsine-exists

.....assertion..... 
∀a:{a:ℝ| a ∈ (r0, r1)} . ∀N:ℕ+.  (∃y:{ℝ| (|y - arcsine(a)| ≤ (r1/r(N)))})
BY
{ (Auto THEN (Assert a ∈ (r0, r1) BY Auto) THEN D 1 THEN Thin 2 THEN MoveToConcl (-1)⋅) }

1
1. a : ℝ
2. N : ℕ+
⊢ (a ∈ (r0, r1)) ⇒ (∃y:{ℝ| (|y - arcsine(a)| ≤ (r1/r(N)))})

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}a:\{a:\mBbbR{}|  a  \mmember{}  (r0,  r1)\}  .  \mforall{}N:\mBbbN{}\msupplus{}.    (\mexists{}y:\{\mBbbR{}|  (|y  -  arcsine(a)|  \mleq{}  (r1/r(N)))\})


By

---

Latex:
(Auto  THEN  (Assert  a  \mmember{}  (r0,  r1)  BY  Auto)  THEN  D  1  THEN  Thin  2  THEN  MoveToConcl  (-1)\mcdot{})

---

Home Index