---

Step * 4 1 of Lemma i-member-proper-iff


1. y : ℝ
2. y1 : Top
3. iproper(<inl (inr y ), inr y1 >)
4. r : ℝ
5. b : {2...}
6. r(-b) < r
7. r < r(b)
8. m : ℕ+
9. y ≤ (r - (r1/r(m)))
10. ∃k:ℕ+. ((r(b) ≤ r(k)) ∧ ((r - (r1/r(m))) ≤ (r - (r1/r(k)))))
⊢ ∃n:ℕ+. (iproper([y + (r1/r(n)), r(n)]) ∧ ((y + (r1/r(n))) ≤ r) ∧ (r ≤ r(n)))
BY
{ TACTIC:(ParallelLast THEN Auto THEN RepUR ``iproper`` 0 THEN Auto) }

1
1. y : ℝ
2. y1 : Top
3. iproper(<inl (inr y ), inr y1 >)
4. r : ℝ
5. b : {2...}
6. r(-b) < r
7. r < r(b)
8. m : ℕ+
9. y ≤ (r - (r1/r(m)))
10. k : ℕ+
11. r(b) ≤ r(k)
12. (r - (r1/r(m))) ≤ (r - (r1/r(k)))
13. i-finite([y + (r1/r(k)), r(k)])
⊢ (y + (r1/r(k))) < r(k)

2
1. y : ℝ
2. y1 : Top
3. iproper(<inl (inr y ), inr y1 >)
4. r : ℝ
5. b : {2...}
6. r(-b) < r
7. r < r(b)
8. m : ℕ+
9. y ≤ (r - (r1/r(m)))
10. k : ℕ+
11. r(b) ≤ r(k)
12. (r - (r1/r(m))) ≤ (r - (r1/r(k)))
13. iproper([y + (r1/r(k)), r(k)])
⊢ (y + (r1/r(k))) ≤ r

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:(ParallelLast  THEN  Auto  THEN  RepUR  ``iproper``  0  THEN  Auto)

---

Home Index