<?xml version="1.0"?>
<div><span class="kw">theorem </span><a NAME="T20"><span class="comment"><font color="firebrick">:: EUCLID10:20</font></span><br/></a><div class="add">(  <a href="sin_cos.html#K17" title="SIN_COS:func.17">sin</a> <span class="p1">(<span class="default"><a href="xcmplx_0.html#K4" title="XCMPLX_0:func.4">-</a> <span class="p2">(<span class="default"><a href="sin_cos.html#K28" title="SIN_COS:func.28">PI</a> <a href="xcmplx_0.html#K7" title="XCMPLX_0:func.7">/</a> 6</span>)</span></span>)</span> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="xcmplx_0.html#K4" title="XCMPLX_0:func.4">-</a> <span class="p1">(<span class="default">1 <a href="xcmplx_0.html#K7" title="XCMPLX_0:func.7">/</a> 2</span>)</span> &amp;  <a href="sin_cos.html#K19" title="SIN_COS:func.19">cos</a> <span class="p1">(<span class="default"><a href="xcmplx_0.html#K4" title="XCMPLX_0:func.4">-</a> <span class="p2">(<span class="default"><a href="sin_cos.html#K28" title="SIN_COS:func.28">PI</a> <a href="xcmplx_0.html#K7" title="XCMPLX_0:func.7">/</a> 6</span>)</span></span>)</span> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> <span class="p1">(<span class="default"><a href="square_1.html#K3" title="SQUARE_1:func.3">sqrt</a> 3</span>)</span> <a href="xcmplx_0.html#K7" title="XCMPLX_0:func.7">/</a> 2 &amp;  <a href="sin_cos4.html#K1" title="SIN_COS4:func.1">tan</a> <span class="p1">(<span class="default"><a href="xcmplx_0.html#K4" title="XCMPLX_0:func.4">-</a> <span class="p2">(<span class="default"><a href="sin_cos.html#K28" title="SIN_COS:func.28">PI</a> <a href="xcmplx_0.html#K7" title="XCMPLX_0:func.7">/</a> 6</span>)</span></span>)</span> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="xcmplx_0.html#K4" title="XCMPLX_0:func.4">-</a> <span class="p1">(<span class="default"><span class="p2">(<span class="default"><a href="square_1.html#K3" title="SQUARE_1:func.3">sqrt</a> 3</span>)</span> <a href="xcmplx_0.html#K7" title="XCMPLX_0:func.7">/</a> 3</span>)</span> &amp;  <a href="sin_cos.html#K17" title="SIN_COS:func.17">sin</a> <span class="p1">(<span class="default"><a href="xcmplx_0.html#K4" title="XCMPLX_0:func.4">-</a> <span class="p2">(<span class="default"><a href="sin_cos.html#K28" title="SIN_COS:func.28">PI</a> <a href="xcmplx_0.html#K7" title="XCMPLX_0:func.7">/</a> 3</span>)</span></span>)</span> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="xcmplx_0.html#K4" title="XCMPLX_0:func.4">-</a> <span class="p1">(<span class="default"><span class="p2">(<span class="default"><a href="square_1.html#K3" title="SQUARE_1:func.3">sqrt</a> 3</span>)</span> <a href="xcmplx_0.html#K7" title="XCMPLX_0:func.7">/</a> 2</span>)</span> &amp;  <a href="sin_cos.html#K19" title="SIN_COS:func.19">cos</a> <span class="p1">(<span class="default"><a href="xcmplx_0.html#K4" title="XCMPLX_0:func.4">-</a> <span class="p2">(<span class="default"><a href="sin_cos.html#K28" title="SIN_COS:func.28">PI</a> <a href="xcmplx_0.html#K7" title="XCMPLX_0:func.7">/</a> 3</span>)</span></span>)</span> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 1 <a href="xcmplx_0.html#K7" title="XCMPLX_0:func.7">/</a> 2 &amp;  <a href="sin_cos4.html#K1" title="SIN_COS4:func.1">tan</a> <span class="p1">(<span class="default"><a href="xcmplx_0.html#K4" title="XCMPLX_0:func.4">-</a> <span class="p2">(<span class="default"><a href="sin_cos.html#K28" title="SIN_COS:func.28">PI</a> <a href="xcmplx_0.html#K7" title="XCMPLX_0:func.7">/</a> 3</span>)</span></span>)</span> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="xcmplx_0.html#K4" title="XCMPLX_0:func.4">-</a> <span class="p1">(<span class="default"><a href="square_1.html#K3" title="SQUARE_1:func.3">sqrt</a> 3</span>)</span> ) <span class="kw">by</span> <span class="lab"><a class="ref" href="sin_cos.html#T31" onmouseover="rs('sin_cos/T31')" onmouseout="rh()">SIN_COS:31</a>, <a class="ref" href="sin_cos4.html#T1" onmouseover="rs('sin_cos4/T1')" onmouseout="rh()">SIN_COS4:1</a>, <a class="ref" href="euclid10.html#T14" target="_self" onmouseover="rs('euclid10/T14')" onmouseout="rh()">Thm8</a>, <a class="ref" href="euclid10.html#T15" target="_self" onmouseover="rs('euclid10/T15')" onmouseout="rh()">Thm9</a>, <a class="ref" href="euclid10.html#T17" target="_self" onmouseover="rs('euclid10/T17')" onmouseout="rh()">Thm11</a>, <a class="ref" href="euclid10.html#T18" target="_self" onmouseover="rs('euclid10/T18')" onmouseout="rh()">Thm12</a>, <a class="ref" href="euclid10.html#T16" target="_self" onmouseover="rs('euclid10/T16')" onmouseout="rh()">Thm10</a>, <a class="ref" href="euclid10.html#T19" target="_self" onmouseover="rs('euclid10/T19')" onmouseout="rh()">Thm13</a></span>;<br/></div></div>
