---

Step * 1 of Lemma radd_rcos_wf

.....assertion..... 
1. x : ℝ
2. addrcos(x) ∈ {f:ℕ+ ⟶ ℤ| f = (x + rcos(x))} 
⊢ 3-regular-seq(addrcos(x))
BY
{ (Unfold `req` -1 THEN (GenConclTerm ⌜addrcos(x)⌝⋅ THENA Auto) THEN All Thin THEN D -1 THEN (Unhide THENA Auto)) }

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

---

Latex:

---

Latex:
.....assertion..... 
1.  x  :  \mBbbR{}
2.  addrcos(x)  \mmember{}  \{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  f  =  (x  +  rcos(x))\} 
\mvdash{}  3-regular-seq(addrcos(x))


By

---

Latex:
(Unfold  `req`  -1
  THEN  (GenConclTerm  \mkleeneopen{}addrcos(x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  D  -1
  THEN  (Unhide  THENA  Auto))

---

Home Index