---

Step * 1 1 of Lemma rcos-is-1-iff

.....basecase..... 
1. x : ℝ
2. rcos(x) = r1
3. n : ℤ
⊢ ((2 * π * r0) < x) ⇒ ((2 * π * r(0 + 1)) ≤ x)
BY
{ (nRNorm 0 THEN (Auto THEN BLemma `rcos-1-implies-at-least-2pi`) THEN Auto) }

---

Latex:

---

Latex:
.....basecase..... 
1.  x  :  \mBbbR{}
2.  rcos(x)  =  r1
3.  n  :  \mBbbZ{}
\mvdash{}  ((2  *  \mpi{}  *  r0)  <  x)  {}\mRightarrow{}  ((2  *  \mpi{}  *  r(0  +  1))  \mleq{}  x)


By

---

Latex:
(nRNorm  0  THEN  (Auto  THEN  BLemma  `rcos-1-implies-at-least-2pi`)  THEN  Auto)

---

Home Index