---

Step * 1 1 1 2 2 of Lemma arctangent-bounds


1. x : ℝ
2. n : ℕ
3. (r(-n) ≤ x) ∧ (x ≤ r(n))
4. ∃a:{a:ℝ| a ∈ (r0, π/2)} . (((r(2 * n) * rcos(a)) < r1) ∧ ((r1/r(2)) ≤ rsin(a)))
⊢ ∃b:{a:ℝ| a ∈ (r0, π/2)} . (r(n) < (rsin(b)/rcos(b)))
BY
{ (InstLemma `rcos-positive` []
   THEN (Assert -(π/2) < r0 BY
               (nRAdd  ⌜π/2⌝ 0⋅ THEN Auto))
   THEN (Assert (r0, π/2) ⊆ (-(π/2), π/2)  BY
               ((D 0 THEN Auto) THEN All Reduce THEN Auto))
   THEN ExRepD
   THEN (Assert ∀a:{a:ℝ| a ∈ (r0, π/2)} . (r0 < rcos(a)) BY
               ((D 0 THENM BackThruSomeHyp) THEN Auto))
   THEN (D 0 With ⌜a⌝  THENW (Try ((Assert r0 < rcos(b) BY BackThruSomeHyp)) THEN Auto))
   THEN (Assert r0 < rcos(a) BY
               BackThruSomeHyp)
   THEN (nRMul ⌜rcos(a)⌝ 0⋅ THENA Auto)) }

1
1. x : ℝ
2. n : ℕ
3. r(-n) ≤ x
4. x ≤ r(n)
5. a : {a:ℝ| a ∈ (r0, π/2)} 
6. (r(2 * n) * rcos(a)) < r1
7. (r1/r(2)) ≤ rsin(a)
8. ∀x:{x:ℝ| x ∈ (-(π/2), π/2)} . (r0 < rcos(x))
9. -(π/2) < r0
10. (r0, π/2) ⊆ (-(π/2), π/2) 
11. ∀a:{a:ℝ| a ∈ (r0, π/2)} . (r0 < rcos(a))
12. r0 < rcos(a)
⊢ (r(n) * rcos(a)) < rsin(a)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  n  :  \mBbbN{}
3.  (r(-n)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r(n))
4.  \mexists{}a:\{a:\mBbbR{}|  a  \mmember{}  (r0,  \mpi{}/2)\}  .  (((r(2  *  n)  *  rcos(a))  <  r1)  \mwedge{}  ((r1/r(2))  \mleq{}  rsin(a)))
\mvdash{}  \mexists{}b:\{a:\mBbbR{}|  a  \mmember{}  (r0,  \mpi{}/2)\}  .  (r(n)  <  (rsin(b)/rcos(b)))


By

---

Latex:
(InstLemma  `rcos-positive`  []
  THEN  (Assert  -(\mpi{}/2)  <  r0  BY
                          (nRAdd    \mkleeneopen{}\mpi{}/2\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  (Assert  (r0,  \mpi{}/2)  \msubseteq{}  (-(\mpi{}/2),  \mpi{}/2)    BY
                          ((D  0  THEN  Auto)  THEN  All  Reduce  THEN  Auto))
  THEN  ExRepD
  THEN  (Assert  \mforall{}a:\{a:\mBbbR{}|  a  \mmember{}  (r0,  \mpi{}/2)\}  .  (r0  <  rcos(a))  BY
                          ((D  0  THENM  BackThruSomeHyp)  THEN  Auto))
  THEN  (D  0  With  \mkleeneopen{}a\mkleeneclose{}    THENW  (Try  ((Assert  r0  <  rcos(b)  BY  BackThruSomeHyp))  THEN  Auto))
  THEN  (Assert  r0  <  rcos(a)  BY
                          BackThruSomeHyp)
  THEN  (nRMul  \mkleeneopen{}rcos(a)\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index