---

Step * of Lemma period-rsin-is-2pi

∀a:ℝ. ((r0 < a) ⇒ (∀x:ℝ. (rsin(x + a) = rsin(x))) ⇒ (2 * π ≤ a))
BY
{ (Auto THEN BLemma `rcos-1-implies-at-least-2pi` THEN Auto) }

1
1. a : ℝ
2. r0 < a
3. ∀x:ℝ. (rsin(x + a) = rsin(x))
⊢ rcos(a) = r1

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  ((r0  <  a)  {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  (rsin(x  +  a)  =  rsin(x)))  {}\mRightarrow{}  (2  *  \mpi{}  \mleq{}  a))


By

---

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

---

Home Index