---

Step * 1 1 1 of Lemma addrcos_wf2


1. x : ℝ
2. n : ℕ+
3. m : ℤ
4. (16 * n) = m ∈ ℤ
5. xm : ℤ
6. (x m) = xm ∈ ℤ
7. z : ℤ
8. (cosine((r(xm))/2 * m) m) = z ∈ ℤ
⊢ |((((m * z) ÷ 4 * m) + (xm ÷ 4)) ÷ 4) - ((0 + (x (4 * n))) + (z ÷ 4)) ÷ 4| ≤ 4
BY
{ ((Subst' m * z ~ z * m 0 THENA Auto) THEN (RWO "div-mul-cancel" 0 THENA Auto)) }

1
1. x : ℝ
2. n : ℕ+
3. m : ℤ
4. (16 * n) = m ∈ ℤ
5. xm : ℤ
6. (x m) = xm ∈ ℤ
7. z : ℤ
8. (cosine((r(xm))/2 * m) m) = z ∈ ℤ
⊢ |(((z ÷ 4) + (xm ÷ 4)) ÷ 4) - ((0 + (x (4 * n))) + (z ÷ 4)) ÷ 4| ≤ 4

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  n  :  \mBbbN{}\msupplus{}
3.  m  :  \mBbbZ{}
4.  (16  *  n)  =  m
5.  xm  :  \mBbbZ{}
6.  (x  m)  =  xm
7.  z  :  \mBbbZ{}
8.  (cosine((r(xm))/2  *  m)  m)  =  z
\mvdash{}  |((((m  *  z)  \mdiv{}  4  *  m)  +  (xm  \mdiv{}  4))  \mdiv{}  4)  -  ((0  +  (x  (4  *  n)))  +  (z  \mdiv{}  4))  \mdiv{}  4|  \mleq{}  4


By

---

Latex:
((Subst'  m  *  z  \msim{}  z  *  m  0  THENA  Auto)  THEN  (RWO  "div-mul-cancel"  0  THENA  Auto))

---

Home Index