---

Step * 1 1 of Lemma rcos-is-1


1. n : ℤ
⊢ rcos(0 * π) = r1
BY
{ ((RWO  "int-rmul-req" 0 THENA Auto) THEN nRNorm 0 THEN RWO "rcos0" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
\mvdash{}  rcos(0  *  \mpi{})  =  r1


By

---

Latex:
((RWO    "int-rmul-req"  0  THENA  Auto)  THEN  nRNorm  0  THEN  RWO  "rcos0"  0  THEN  Auto)

---

Home Index