Step
*
1
of Lemma
rational-approx-implies-req
1. k : ℕ+
2. x : ℝ
3. a : ℕ+ ⟶ ℤ
4. ∀n:ℕ+. (|x - (r(a n)/r(2 * n))| ≤ (r(k)/r(n)))
5. ∀n,m:ℕ+. (|(r(a n)/r(2 * n)) - (r(a m)/r(2 * m))| ≤ ((r(k)/r(n)) + (r(k)/r(m))))
⊢ k-regular-seq(a) ∧ (accelerate(k;a) = x)
BY
{ (Assert k-regular-seq(a) BY
(D 0
THEN Auto
THEN (BLemma `rleq-int` THENA Auto)
THEN (RWW "rabs-int< rmul-int< radd-int< rsub-int<" 0 THENA Auto)
THEN (Assert r0 < |r(2 * n * m)| BY
(RWO "rabs-of-nonneg" 0 THEN Auto))
THEN (Assert r0 < (r1/|r(2 * n * m)|) BY
(BLemma `rdiv-is-positive` THEN Auto))
THEN Using [`y',⌜(|r1|/|r(2 * n * m)|)⌝] (BLemma `rmul_preserves_rleq`)⋅
THEN Auto
THEN (RWW "rabs-rdiv< rabs-rmul<" 0⋅ THENA Auto))) }
1
1. k : ℕ+
2. x : ℝ
3. a : ℕ+ ⟶ ℤ
4. ∀n:ℕ+. (|x - (r(a n)/r(2 * n))| ≤ (r(k)/r(n)))
5. ∀n,m:ℕ+. (|(r(a n)/r(2 * n)) - (r(a m)/r(2 * m))| ≤ ((r(k)/r(n)) + (r(k)/r(m))))
6. n : ℕ+
7. m : ℕ+
8. r0 < |r(2 * n * m)|
9. r0 < (r1/|r(2 * n * m)|)
⊢ |((r(m) * r(a n)) - r(n) * r(a m)) * (r1/r(2 * n * m))| ≤ (((r(2) * r(k)) * (r(n) + r(m))) * |(r1/r(2 * n * m))|)
2
1. k : ℕ+
2. x : ℝ
3. a : ℕ+ ⟶ ℤ
4. ∀n:ℕ+. (|x - (r(a n)/r(2 * n))| ≤ (r(k)/r(n)))
5. ∀n,m:ℕ+. (|(r(a n)/r(2 * n)) - (r(a m)/r(2 * m))| ≤ ((r(k)/r(n)) + (r(k)/r(m))))
6. k-regular-seq(a)
⊢ k-regular-seq(a) ∧ (accelerate(k;a) = x)
Latex:
Latex:
1. k : \mBbbN{}\msupplus{}
2. x : \mBbbR{}
3. a : \mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}
4. \mforall{}n:\mBbbN{}\msupplus{}. (|x - (r(a n)/r(2 * n))| \mleq{} (r(k)/r(n)))
5. \mforall{}n,m:\mBbbN{}\msupplus{}. (|(r(a n)/r(2 * n)) - (r(a m)/r(2 * m))| \mleq{} ((r(k)/r(n)) + (r(k)/r(m))))
\mvdash{} k-regular-seq(a) \mwedge{} (accelerate(k;a) = x)
By
Latex:
(Assert k-regular-seq(a) BY
(D 0
THEN Auto
THEN (BLemma `rleq-int` THENA Auto)
THEN (RWW "rabs-int< rmul-int< radd-int< rsub-int<" 0 THENA Auto)
THEN (Assert r0 < |r(2 * n * m)| BY
(RWO "rabs-of-nonneg" 0 THEN Auto))
THEN (Assert r0 < (r1/|r(2 * n * m)|) BY
(BLemma `rdiv-is-positive` THEN Auto))
THEN Using [`y',\mkleeneopen{}(|r1|/|r(2 * n * m)|)\mkleeneclose{}] (BLemma `rmul\_preserves\_rleq`)\mcdot{}
THEN Auto
THEN (RWW "rabs-rdiv< rabs-rmul<" 0\mcdot{} THENA Auto)))
Home
Index