Step
*
1
1
1
1
1
1
1
1
1
of Lemma
continuous-limit
∀I:Interval. ∀z:ℝ. ∀n:ℕ+. ∀v:ℝ.
((z ∈ i-approx(I;n))
⇒ (((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n)))
⇒ ((r1/r(2 * n)) ≤ r1)
⇒ (v ∈ I)
⇒ (((z - (r1/r(2 * n))) ≤ v) ∧ (v ≤ (z + (r1/r(2 * n)))))
⇒ (v ∈ i-approx(I;2 * n)))
BY
{ ((D 0 THENA Auto)
THEN RepeatFor 2 (D 1)
THEN D 2
THEN Try (DProdsAndUnions)
THEN RepUR ``i-approx i-member`` 0
THEN Auto) }
1
1. y : ℝ
2. x2 : ℝ
3. z : ℝ
4. n : ℕ+
5. v : ℝ
6. (y + (r1/r(n))) ≤ z
7. z ≤ x2
8. ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n))
9. (r1/r(2 * n)) ≤ r1
10. y < v
11. v ≤ x2
12. (z - (r1/r(2 * n))) ≤ v
13. v ≤ (z + (r1/r(2 * n)))
⊢ (y + (r1/r(2 * n))) ≤ v
2
1. x1 : ℝ
2. y : ℝ
3. z : ℝ
4. n : ℕ+
5. v : ℝ
6. x1 ≤ z
7. z ≤ (y - (r1/r(n)))
8. ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n))
9. (r1/r(2 * n)) ≤ r1
10. x1 ≤ v
11. v < y
12. (z - (r1/r(2 * n))) ≤ v
13. v ≤ (z + (r1/r(2 * n)))
14. x1 ≤ v
⊢ v ≤ (y - (r1/r(2 * n)))
3
1. y1 : ℝ
2. y : ℝ
3. z : ℝ
4. n : ℕ+
5. v : ℝ
6. (y1 + (r1/r(n))) ≤ z
7. z ≤ (y - (r1/r(n)))
8. ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n))
9. (r1/r(2 * n)) ≤ r1
10. y1 < v
11. v < y
12. (z - (r1/r(2 * n))) ≤ v
13. v ≤ (z + (r1/r(2 * n)))
⊢ (y1 + (r1/r(2 * n))) ≤ v
4
1. y1 : ℝ
2. y : ℝ
3. z : ℝ
4. n : ℕ+
5. v : ℝ
6. (y1 + (r1/r(n))) ≤ z
7. z ≤ (y - (r1/r(n)))
8. ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n))
9. (r1/r(2 * n)) ≤ r1
10. y1 < v
11. v < y
12. (z - (r1/r(2 * n))) ≤ v
13. v ≤ (z + (r1/r(2 * n)))
14. (y1 + (r1/r(2 * n))) ≤ v
⊢ v ≤ (y - (r1/r(2 * n)))
5
1. x1 : ℝ
2. y : Top
3. z : ℝ
4. n : ℕ+
5. v : ℝ
6. x1 ≤ z
7. z ≤ r(n)
8. ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n))
9. (r1/r(2 * n)) ≤ r1
10. x1 ≤ v
11. (z - (r1/r(2 * n))) ≤ v
12. v ≤ (z + (r1/r(2 * n)))
13. x1 ≤ v
⊢ v ≤ r(2 * n)
6
1. y1 : ℝ
2. y : Top
3. z : ℝ
4. n : ℕ+
5. v : ℝ
6. (y1 + (r1/r(n))) ≤ z
7. z ≤ r(n)
8. ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n))
9. (r1/r(2 * n)) ≤ r1
10. y1 < v
11. (z - (r1/r(2 * n))) ≤ v
12. v ≤ (z + (r1/r(2 * n)))
⊢ (y1 + (r1/r(2 * n))) ≤ v
7
1. y1 : ℝ
2. y : Top
3. z : ℝ
4. n : ℕ+
5. v : ℝ
6. (y1 + (r1/r(n))) ≤ z
7. z ≤ r(n)
8. ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n))
9. (r1/r(2 * n)) ≤ r1
10. y1 < v
11. (z - (r1/r(2 * n))) ≤ v
12. v ≤ (z + (r1/r(2 * n)))
13. (y1 + (r1/r(2 * n))) ≤ v
⊢ v ≤ r(2 * n)
8
1. y : Top
2. x1 : ℝ
3. z : ℝ
4. n : ℕ+
5. v : ℝ
6. r(-n) ≤ z
7. z ≤ x1
8. ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n))
9. (r1/r(2 * n)) ≤ r1
10. v ≤ x1
11. (z - (r1/r(2 * n))) ≤ v
12. v ≤ (z + (r1/r(2 * n)))
⊢ r(-(2 * n)) ≤ v
9
1. y : Top
2. y1 : ℝ
3. z : ℝ
4. n : ℕ+
5. v : ℝ
6. r(-n) ≤ z
7. z ≤ (y1 - (r1/r(n)))
8. ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n))
9. (r1/r(2 * n)) ≤ r1
10. v < y1
11. (z - (r1/r(2 * n))) ≤ v
12. v ≤ (z + (r1/r(2 * n)))
⊢ r(-(2 * n)) ≤ v
10
1. y : Top
2. y1 : ℝ
3. z : ℝ
4. n : ℕ+
5. v : ℝ
6. r(-n) ≤ z
7. z ≤ (y1 - (r1/r(n)))
8. ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n))
9. (r1/r(2 * n)) ≤ r1
10. v < y1
11. (z - (r1/r(2 * n))) ≤ v
12. v ≤ (z + (r1/r(2 * n)))
13. r(-(2 * n)) ≤ v
⊢ v ≤ (y1 - (r1/r(2 * n)))
11
1. y : Top
2. y1 : Top
3. z : ℝ
4. n : ℕ+
5. v : ℝ
6. r(-n) ≤ z
7. z ≤ r(n)
8. ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n))
9. (r1/r(2 * n)) ≤ r1
10. True
11. (z - (r1/r(2 * n))) ≤ v
12. v ≤ (z + (r1/r(2 * n)))
⊢ r(-(2 * n)) ≤ v
12
1. y : Top
2. y1 : Top
3. z : ℝ
4. n : ℕ+
5. v : ℝ
6. r(-n) ≤ z
7. z ≤ r(n)
8. ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n))
9. (r1/r(2 * n)) ≤ r1
10. True
11. (z - (r1/r(2 * n))) ≤ v
12. v ≤ (z + (r1/r(2 * n)))
13. r(-(2 * n)) ≤ v
⊢ v ≤ r(2 * n)
Latex:
Latex:
\mforall{}I:Interval. \mforall{}z:\mBbbR{}. \mforall{}n:\mBbbN{}\msupplus{}. \mforall{}v:\mBbbR{}.
((z \mmember{} i-approx(I;n))
{}\mRightarrow{} (((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n)))
{}\mRightarrow{} ((r1/r(2 * n)) \mleq{} r1)
{}\mRightarrow{} (v \mmember{} I)
{}\mRightarrow{} (((z - (r1/r(2 * n))) \mleq{} v) \mwedge{} (v \mleq{} (z + (r1/r(2 * n)))))
{}\mRightarrow{} (v \mmember{} i-approx(I;2 * n)))
By
Latex:
((D 0 THENA Auto)
THEN RepeatFor 2 (D 1)
THEN D 2
THEN Try (DProdsAndUnions)
THEN RepUR ``i-approx i-member`` 0
THEN Auto)
Home
Index