Step * 1 1 1 1 1 3 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. (rsin((π/r(4)))^2 rsin((π/r(4)))^2) r1
4. rcos((π/r(4)))^2 rsin((π/r(4)))^2
5. rsin((π/r(4))) rsqrt((r1/r(2)))
⊢ rsin((π/r(4))) (r1/rsqrt(r(2)))
BY
((Assert r0 < rsqrt(r(2)) BY EAuto 2) THEN (RWO "-2" THENA Auto)) }

1
1. r0 (rcos((π/r(4)))^2 rsin((π/r(4)))^2)
2. rcos((π/r(4)) /r(4))) rcos(π/2)
3. (rsin((π/r(4)))^2 rsin((π/r(4)))^2) r1
4. rcos((π/r(4)))^2 rsin((π/r(4)))^2
5. rsin((π/r(4))) rsqrt((r1/r(2)))
6. r0 < rsqrt(r(2))
⊢ rsqrt((r1/r(2))) (r1/rsqrt(r(2)))


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.  (rsin((\mpi{}/r(4)))\^{}2  +  rsin((\mpi{}/r(4)))\^{}2)  =  r1
4.  rcos((\mpi{}/r(4)))\^{}2  =  rsin((\mpi{}/r(4)))\^{}2
5.  rsin((\mpi{}/r(4)))  =  rsqrt((r1/r(2)))
\mvdash{}  rsin((\mpi{}/r(4)))  =  (r1/rsqrt(r(2)))


By


Latex:
((Assert  r0  <  rsqrt(r(2))  BY  EAuto  2)  THEN  (RWO  "-2"  0  THENA  Auto))




Home Index