Step
*
1
of Lemma
i-member-proper-iff
1. x1 : ℝ
2. y : ℝ
3. r : ℝ
4. b : {2...}
5. r(-b) < r
6. r < r(b)
7. x1 ≤ r
8. m : ℕ+
9. r ≤ (y - (r1/r(m)))
10. x1 < y
⊢ ∃n:ℕ+. (iproper([x1, y - (r1/r(n))]) ∧ (x1 ≤ r) ∧ (r ≤ (y - (r1/r(n)))))
BY
{ (RenameVar `u' 1 THEN RenameVar `v' 2) }
1
1. u : ℝ
2. v : ℝ
3. r : ℝ
4. b : {2...}
5. r(-b) < r
6. r < r(b)
7. u ≤ r
8. m : ℕ+
9. r ≤ (v - (r1/r(m)))
10. u < v
⊢ ∃n:ℕ+. (iproper([u, v - (r1/r(n))]) ∧ (u ≤ r) ∧ (r ≤ (v - (r1/r(n)))))
Latex:
Latex:
1. x1 : \mBbbR{}
2. y : \mBbbR{}
3. r : \mBbbR{}
4. b : \{2...\}
5. r(-b) < r
6. r < r(b)
7. x1 \mleq{} r
8. m : \mBbbN{}\msupplus{}
9. r \mleq{} (y - (r1/r(m)))
10. x1 < y
\mvdash{} \mexists{}n:\mBbbN{}\msupplus{}. (iproper([x1, y - (r1/r(n))]) \mwedge{} (x1 \mleq{} r) \mwedge{} (r \mleq{} (y - (r1/r(n)))))
By
Latex:
(RenameVar `u' 1 THEN RenameVar `v' 2)
Home
Index