---

Step * 1 1 1 of Lemma blended-real-req


1. k : ℕ+
2. x : ℝ
3. y : ℝ
4. |x - y| ≤ (r1/r(k))
5. ∀z:ℝ. 3-regular-seq(z)
6. n : {k...}
⊢ (if 6 * n <z k then x (6 * n) else y (6 * n) fi  ÷ 6) = ((y (6 * n)) ÷ 6) ∈ ℤ
BY
{ AutoSplit }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  x  :  \mBbbR{}
3.  y  :  \mBbbR{}
4.  |x  -  y|  \mleq{}  (r1/r(k))
5.  \mforall{}z:\mBbbR{}.  3-regular-seq(z)
6.  n  :  \{k...\}
\mvdash{}  (if  6  *  n  <z  k  then  x  (6  *  n)  else  y  (6  *  n)  fi    \mdiv{}  6)  =  ((y  (6  *  n))  \mdiv{}  6)


By

---

Latex:
AutoSplit

---

Home Index