---

Step * 1 1 1 1 1 2 1 1 of Lemma rsin-pi-over-4


1. r0 = (rcos((π/r(4)))^2 - rsin((π/r(4)))^2)
2. rcos((π/r(4)) + (π/r(4))) = rcos(π/2)
3. rcos((π/r(4)))^2 = rsin((π/r(4)))^2
4. v : ℝ
5. rsin((π/r(4)))^2 = v ∈ ℝ
⊢ ((v + v) = r1) ⇒ (v = (r1/r(2)))
BY
{ ((All Thin THEN Auto) THEN nRMul ⌜r(2)⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  r0  =  (rcos((\mpi{}/r(4)))\^{}2  -  rsin((\mpi{}/r(4)))\^{}2)
2.  rcos((\mpi{}/r(4))  +  (\mpi{}/r(4)))  =  rcos(\mpi{}/2)
3.  rcos((\mpi{}/r(4)))\^{}2  =  rsin((\mpi{}/r(4)))\^{}2
4.  v  :  \mBbbR{}
5.  rsin((\mpi{}/r(4)))\^{}2  =  v
\mvdash{}  ((v  +  v)  =  r1)  {}\mRightarrow{}  (v  =  (r1/r(2)))


By

---

Latex:
((All  Thin  THEN  Auto)  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index