---

Step * 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...}
⊢ (blended-real(k;x;y) n) = (accelerate(3;y) n) ∈ ℤ
BY
{ (RepUR ``blended-real blend-seq accelerate`` 0 THEN (CallByValueReduce 0 THENA Auto)) }

1
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) ∈ ℤ

---

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{}  (blended-real(k;x;y)  n)  =  (accelerate(3;y)  n)


By

---

Latex:
(RepUR  ``blended-real  blend-seq  accelerate``  0  THEN  (CallByValueReduce  0  THENA  Auto))

---

Home Index