---

Step * 1 2 of Lemma rcos-is-1

.....upcase..... 
1. n : ℤ
2. 0 < n
3. rcos(2 * (n - 1) * π) = r1
⊢ rcos(2 * n * π) = r1
BY
{ (Assert 2 * n * π = (2 * (n - 1) * π + 2 * π) BY
         ((Assert r(2 * n) = (r(2 * (n - 1)) + r(2)) BY
                 (RWO "radd-int" 0 THEN Auto))
          THEN (RWO "int-rmul-req" 0 THENA Auto)
          THEN RWO "-1" 0
          THEN Auto)) }

1
1. n : ℤ
2. 0 < n
3. rcos(2 * (n - 1) * π) = r1
4. 2 * n * π = (2 * (n - 1) * π + 2 * π)
⊢ rcos(2 * n * π) = r1

---

Latex:

---

Latex:
.....upcase..... 
1.  n  :  \mBbbZ{}
2.  0  <  n
3.  rcos(2  *  (n  -  1)  *  \mpi{})  =  r1
\mvdash{}  rcos(2  *  n  *  \mpi{})  =  r1


By

---

Latex:
(Assert  2  *  n  *  \mpi{}  =  (2  *  (n  -  1)  *  \mpi{}  +  2  *  \mpi{})  BY
              ((Assert  r(2  *  n)  =  (r(2  *  (n  -  1))  +  r(2))  BY
                              (RWO  "radd-int"  0  THEN  Auto))
                THEN  (RWO  "int-rmul-req"  0  THENA  Auto)
                THEN  RWO  "-1"  0
                THEN  Auto))

---

Home Index