---

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


1. ∀x:ℝ. ((rcos(x) = r1) ⇒ (∀n:ℕ. (((2 * π * r(n)) < x) ⇒ ((2 * π * r(n + 1)) ≤ x))))
⊢ ∀x:ℝ. (rcos(x) = r1 ⇐⇒ ∃n:ℤ. (x = 2 * n * π))
BY
{ ((Assert ∀x:ℝ. ((rcos(x) = r1) ⇒ (∀n:ℕ. (((2 * π * r(n)) < |x|) ⇒ ((2 * π * r(n + 1)) ≤ |x|)))) BY
          (Auto THEN BHyp 1 THEN Auto THEN RWO "rcos-rabs" 0 THEN Auto))
   THEN ParallelLast
   THEN Auto
   THEN RepeatFor 2 (Thin 1)
   THEN ExRepD
   THEN Try ((RWO "-1" 0 THEN Auto))) }

1
1. x : ℝ
2. rcos(x) = r1
3. ∀n:ℕ. (((2 * π * r(n)) < |x|) ⇒ ((2 * π * r(n + 1)) ≤ |x|))
⊢ ∃n:ℤ. (x = 2 * n * π)

---

Latex:

---

Latex:

1.  \mforall{}x:\mBbbR{}.  ((rcos(x)  =  r1)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (((2  *  \mpi{}  *  r(n))  <  x)  {}\mRightarrow{}  ((2  *  \mpi{}  *  r(n  +  1))  \mleq{}  x))))
\mvdash{}  \mforall{}x:\mBbbR{}.  (rcos(x)  =  r1  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbZ{}.  (x  =  2  *  n  *  \mpi{}))


By

---

Latex:
((Assert  \mforall{}x:\mBbbR{}.  ((rcos(x)  =  r1)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (((2  *  \mpi{}  *  r(n))  <  |x|)  {}\mRightarrow{}  ((2  *  \mpi{}  *  r(n  +  1))  \mleq{}  |x|))))  BY
                (Auto  THEN  BHyp  1  THEN  Auto  THEN  RWO  "rcos-rabs"  0  THEN  Auto))
  THEN  ParallelLast
  THEN  Auto
  THEN  RepeatFor  2  (Thin  1)
  THEN  ExRepD
  THEN  Try  ((RWO  "-1"  0  THEN  Auto)))

---

Home Index