---

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

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  BLemma  `period-rsin-is-2pi`  THEN  Auto)

---

Home Index