---

Step * 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. u ≤ r
8. m : ℕ+
9. r ≤ (v - (r1/r(m)))
10. u < v
11. ∃k:ℕ+. (u < (v - (r1/r(k))))
⊢ ∃n:ℕ+. (iproper([u, v - (r1/r(n))]) ∧ (u ≤ r) ∧ (r ≤ (v - (r1/r(n)))))
BY
{ (D -1
   THEN (Assert ∃N:ℕ+. (((v - (r1/r(k))) ≤ (v - (r1/r(N)))) ∧ ((v - (r1/r(m))) ≤ (v - (r1/r(N))))) BY
               (With ⌜imax(k;m)⌝ (D 0)⋅
                THEN Auto
                THEN Repeat ((RWO "imax_unfold" 0 THEN Auto))
                THEN AutoSplit
                THEN nRAdd ⌜-(v)⌝ 0⋅
                THEN Auto
                THEN RWW "rminus-rdiv rminus-int" 0
                THEN Auto))
   ) }

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
11. k : ℕ+
12. u < (v - (r1/r(k)))
13. ∃N:ℕ+. (((v - (r1/r(k))) ≤ (v - (r1/r(N)))) ∧ ((v - (r1/r(m))) ≤ (v - (r1/r(N)))))
⊢ ∃n:ℕ+. (iproper([u, v - (r1/r(n))]) ∧ (u ≤ r) ∧ (r ≤ (v - (r1/r(n)))))

---

Latex:

---

Latex:

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


By

---

Latex:
(D  -1
  THEN  (Assert  \mexists{}N:\mBbbN{}\msupplus{}.  (((v  -  (r1/r(k)))  \mleq{}  (v  -  (r1/r(N))))  \mwedge{}  ((v  -  (r1/r(m)))  \mleq{}  (v  -  (r1/r(N)))))  BY
                          (With  \mkleeneopen{}imax(k;m)\mkleeneclose{}  (D  0)\mcdot{}
                            THEN  Auto
                            THEN  Repeat  ((RWO  "imax\_unfold"  0  THEN  Auto))
                            THEN  AutoSplit
                            THEN  nRAdd  \mkleeneopen{}-(v)\mkleeneclose{}  0\mcdot{}
                            THEN  Auto
                            THEN  RWW  "rminus-rdiv  rminus-int"  0
                            THEN  Auto))
  )

---

Home Index