---

Step * 2 of Lemma i-member-proper-iff


1. y : ℝ
2. x1 : ℝ
3. r : ℝ
4. b : {2...}
5. r(-b) < r
6. r < r(b)
7. m : ℕ+
8. y ≤ (r - (r1/r(m)))
9. r ≤ x1
10. y < x1
⊢ ∃n:ℕ+. (iproper([y + (r1/r(n)), x1]) ∧ ((y + (r1/r(n))) ≤ r) ∧ (r ≤ x1))
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. m : ℕ+
8. u ≤ (r - (r1/r(m)))
9. r ≤ v
10. u < v
⊢ ∃n:ℕ+. (iproper([u + (r1/r(n)), v]) ∧ ((u + (r1/r(n))) ≤ r) ∧ (r ≤ v))

---

Latex:

---

Latex:

1.  y  :  \mBbbR{}
2.  x1  :  \mBbbR{}
3.  r  :  \mBbbR{}
4.  b  :  \{2...\}
5.  r(-b)  <  r
6.  r  <  r(b)
7.  m  :  \mBbbN{}\msupplus{}
8.  y  \mleq{}  (r  -  (r1/r(m)))
9.  r  \mleq{}  x1
10.  y  <  x1
\mvdash{}  \mexists{}n:\mBbbN{}\msupplus{}.  (iproper([y  +  (r1/r(n)),  x1])  \mwedge{}  ((y  +  (r1/r(n)))  \mleq{}  r)  \mwedge{}  (r  \mleq{}  x1))


By

---

Latex:
(RenameVar  `u'  1  THEN  RenameVar  `v'  2)

---

Home Index