Step
*
2
1
of Lemma
rational-lower-approx-property
1. x : ℝ
2. n : ℕ+
3. a : ℤ
4. (x (2 * n)) = a ∈ ℤ
5. (r(a - 2))/2 * 2 * n = ((r(a))/2 * 2 * n - (r1/r(2 * n)))
6. r : ℝ
7. (r(a))/2 * 2 * n = r ∈ ℝ
⊢ (|x - r| ≤ (r1/r(2 * n)))
⇒ (((r - (r1/r(2 * n))) ≤ x) ∧ (x ≤ ((r - (r1/r(2 * n))) + (r1/r(n)))))
BY
{ ((D 0 THENA Auto) THEN RWO "rabs-difference-bound-rleq" (-1) THEN Auto) }
1
1. x : ℝ
2. n : ℕ+
3. a : ℤ
4. (x (2 * n)) = a ∈ ℤ
5. (r(a - 2))/2 * 2 * n = ((r(a))/2 * 2 * n - (r1/r(2 * n)))
6. r : ℝ
7. (r(a))/2 * 2 * n = r ∈ ℝ
8. (r - (r1/r(2 * n))) ≤ x
9. x ≤ (r + (r1/r(2 * n)))
10. (r - (r1/r(2 * n))) ≤ x
⊢ x ≤ ((r - (r1/r(2 * n))) + (r1/r(n)))
Latex:
Latex:
1. x : \mBbbR{}
2. n : \mBbbN{}\msupplus{}
3. a : \mBbbZ{}
4. (x (2 * n)) = a
5. (r(a - 2))/2 * 2 * n = ((r(a))/2 * 2 * n - (r1/r(2 * n)))
6. r : \mBbbR{}
7. (r(a))/2 * 2 * n = r
\mvdash{} (|x - r| \mleq{} (r1/r(2 * n))) {}\mRightarrow{} (((r - (r1/r(2 * n))) \mleq{} x) \mwedge{} (x \mleq{} ((r - (r1/r(2 * n))) + (r1/r(n)))))
By
Latex:
((D 0 THENA Auto) THEN RWO "rabs-difference-bound-rleq" (-1) THEN Auto)
Home
Index