---

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


1. u : ℝ
2. v : ℝ
3. r : ℝ
4. b : {2...}
5. r(-b) < r
6. r < r(b)
7. m1 : ℕ+
8. u ≤ (r - (r1/r(m1)))
9. m : ℕ+
10. r ≤ (v - (r1/r(m)))
11. u < v
12. k : ℕ+
13. u < (v - (r1/r(k)))
14. N : ℕ+
15. (r1/r(N)) ≤ (r1/r(2 * k))
16. (r1/r(N)) ≤ (r1/r(m))
17. (r1/r(N)) ≤ (r1/r(m1))
18. i-finite([u + (r1/r(N)), v - (r1/r(N))])
⊢ (u + (r1/r(N))) < (v - (r1/r(N)))
BY
{ nRAdd ⌜(r1/r(N))⌝ 0⋅ }

1
1. u : ℝ
2. v : ℝ
3. r : ℝ
4. b : {2...}
5. r(-b) < r
6. r < r(b)
7. m1 : ℕ+
8. u ≤ (r - (r1/r(m1)))
9. m : ℕ+
10. r ≤ (v - (r1/r(m)))
11. u < v
12. k : ℕ+
13. u < (v - (r1/r(k)))
14. N : ℕ+
15. (r1/r(N)) ≤ (r1/r(2 * k))
16. (r1/r(N)) ≤ (r1/r(m))
17. (r1/r(N)) ≤ (r1/r(m1))
18. i-finite([u + (r1/r(N)), v - (r1/r(N))])
⊢ ((r(2)/r(N)) + u) < v

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  v  :  \mBbbR{}
3.  r  :  \mBbbR{}
4.  b  :  \{2...\}
5.  r(-b)  <  r
6.  r  <  r(b)
7.  m1  :  \mBbbN{}\msupplus{}
8.  u  \mleq{}  (r  -  (r1/r(m1)))
9.  m  :  \mBbbN{}\msupplus{}
10.  r  \mleq{}  (v  -  (r1/r(m)))
11.  u  <  v
12.  k  :  \mBbbN{}\msupplus{}
13.  u  <  (v  -  (r1/r(k)))
14.  N  :  \mBbbN{}\msupplus{}
15.  (r1/r(N))  \mleq{}  (r1/r(2  *  k))
16.  (r1/r(N))  \mleq{}  (r1/r(m))
17.  (r1/r(N))  \mleq{}  (r1/r(m1))
18.  i-finite([u  +  (r1/r(N)),  v  -  (r1/r(N))])
\mvdash{}  (u  +  (r1/r(N)))  <  (v  -  (r1/r(N)))


By

---

Latex:
nRAdd  \mkleeneopen{}(r1/r(N))\mkleeneclose{}  0\mcdot{}

---

Home Index