Step
*
2
1
of Lemma
rational-inner-approx-property
1. x : ℝ
2. n : ℕ+
3. a : ℤ
4. (x (2 * n)) = a ∈ ℤ
5. |x - (r(a))/2 * 2 * n| ≤ (r1/r(2 * n))
6. ¬4 < a
7. a < -4
⊢ (|(r(a + 2))/2 * 2 * n| ≤ |x|) ∧ (|x - (r(a + 2))/2 * 2 * n| ≤ (r(2)/r(n)))
BY
{ Assert ⌜(r(a + 2))/2 * 2 * n = ((r(a))/2 * 2 * n + (r1/r(2 * n)))⌝⋅ }
1
.....assertion.....
1. x : ℝ
2. n : ℕ+
3. a : ℤ
4. (x (2 * n)) = a ∈ ℤ
5. |x - (r(a))/2 * 2 * n| ≤ (r1/r(2 * n))
6. ¬4 < a
7. a < -4
⊢ (r(a + 2))/2 * 2 * n = ((r(a))/2 * 2 * n + (r1/r(2 * n)))
2
1. x : ℝ
2. n : ℕ+
3. a : ℤ
4. (x (2 * n)) = a ∈ ℤ
5. |x - (r(a))/2 * 2 * n| ≤ (r1/r(2 * n))
6. ¬4 < a
7. a < -4
8. (r(a + 2))/2 * 2 * n = ((r(a))/2 * 2 * n + (r1/r(2 * n)))
⊢ (|(r(a + 2))/2 * 2 * n| ≤ |x|) ∧ (|x - (r(a + 2))/2 * 2 * n| ≤ (r(2)/r(n)))
Latex:
Latex:
1. x : \mBbbR{}
2. n : \mBbbN{}\msupplus{}
3. a : \mBbbZ{}
4. (x (2 * n)) = a
5. |x - (r(a))/2 * 2 * n| \mleq{} (r1/r(2 * n))
6. \mneg{}4 < a
7. a < -4
\mvdash{} (|(r(a + 2))/2 * 2 * n| \mleq{} |x|) \mwedge{} (|x - (r(a + 2))/2 * 2 * n| \mleq{} (r(2)/r(n)))
By
Latex:
Assert \mkleeneopen{}(r(a + 2))/2 * 2 * n = ((r(a))/2 * 2 * n + (r1/r(2 * n)))\mkleeneclose{}\mcdot{}
Home
Index