---

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


By

---

Latex:
(RevHypSubst'  (-5)  0
  THEN  (Subst'  m  \msim{}  4  *  4  *  n  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(4  *  n)  =  k\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index