---

Step * 1 1 of Lemma radd_rcos_wf


1. x : ℝ
2. v : ℕ+ ⟶ ℤ
3. ∀n:ℕ+. (|(v n) - (x + rcos(x)) n| ≤ 4)
⊢ 3-regular-seq(v)
BY
{ (MoveToConcl (-1)
   THEN (GenConcl ⌜(x + rcos(x)) = z ∈ ℝ⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto
   THEN D 2
   THEN (Unhide THENA Auto)) }

1
1. v : ℕ+ ⟶ ℤ
2. z : ℕ+ ⟶ ℤ
3. regular-seq(z)
4. ∀n:ℕ+. (|(v n) - z n| ≤ 4)
⊢ 3-regular-seq(v)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  v  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  \mforall{}n:\mBbbN{}\msupplus{}.  (|(v  n)  -  (x  +  rcos(x))  n|  \mleq{}  4)
\mvdash{}  3-regular-seq(v)


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}(x  +  rcos(x))  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto
  THEN  D  2
  THEN  (Unhide  THENA  Auto))

---

Home Index