---

Step * 1 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 ∈ ℤ
⊢ |(((z ÷ 4) + (xm ÷ 4)) ÷ 4) - ((0 + (x (4 * n))) + (z ÷ 4)) ÷ 4| ≤ 4
BY
{ ((GenConcl ⌜(z ÷ 4) = A ∈ ℤ⌝⋅ THENA Auto) THEN (Subst' 0 + (x (4 * n)) ~ x (4 * n) 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 ∈ ℤ
9. A : ℤ
10. (z ÷ 4) = A ∈ ℤ
⊢ |((A + (xm ÷ 4)) ÷ 4) - ((x (4 * n)) + A) ÷ 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{}  |(((z  \mdiv{}  4)  +  (xm  \mdiv{}  4))  \mdiv{}  4)  -  ((0  +  (x  (4  *  n)))  +  (z  \mdiv{}  4))  \mdiv{}  4|  \mleq{}  4


By

---

Latex:
((GenConcl  \mkleeneopen{}(z  \mdiv{}  4)  =  A\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (Subst'  0  +  (x  (4  *  n))  \msim{}  x  (4  *  n)  0  THENA  Auto))

---

Home Index