---

Step * of Lemma rcos-is-1-iff

∀x:ℝ. (rcos(x) = r1 ⇐⇒ ∃n:ℤ. (x = 2 * n * π))
BY
{ Assert ⌜∀x:ℝ. ((rcos(x) = r1) ⇒ (∀n:ℕ. (((2 * π * r(n)) < x) ⇒ ((2 * π * r(n + 1)) ≤ x))))⌝⋅ }

1
.....assertion..... 
∀x:ℝ. ((rcos(x) = r1) ⇒ (∀n:ℕ. (((2 * π * r(n)) < x) ⇒ ((2 * π * r(n + 1)) ≤ x))))

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

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (rcos(x)  =  r1  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbZ{}.  (x  =  2  *  n  *  \mpi{}))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}x:\mBbbR{}.  ((rcos(x)  =  r1)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (((2  *  \mpi{}  *  r(n))  <  x)  {}\mRightarrow{}  ((2  *  \mpi{}  *  r(n  +  1))  \mleq{}  x))))\mkleeneclose{}\mcdot{}

---

Home Index