---

Step * of Lemma rcos-positive-initially

∀x:{x:ℝ| x ∈ [r0, (r(1570796326)/r(1000000000))]} . (r0 < rcos(x))
BY
{ (Auto THEN InstLemma `rcos-positive-near-0` [] THEN InstLemma `rsin-positive-near-11/7` []) }

1
1. x : {x:ℝ| x ∈ [r0, (r(1570796326)/r(1000000000))]} 
2. ∀x:{x:ℝ| x ∈ (r(-1), r1)} . (r0 < rcos(x))
3. ∀x:{x:ℝ| x ∈ ((r(41)/r(70)), (r(179)/r(70)))} . (r0 < rsin(x))
⊢ r0 < rcos(x)

---

Latex:

---

Latex:
\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [r0,  (r(1570796326)/r(1000000000))]\}  .  (r0  <  rcos(x))


By

---

Latex:
(Auto  THEN  InstLemma  `rcos-positive-near-0`  []  THEN  InstLemma  `rsin-positive-near-11/7`  [])

---

Home Index