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


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


Latex:


Latex:

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


By


Latex:
((nRAdd  \mkleeneopen{}(r1/r(k))\mkleeneclose{}  (-5)\mcdot{}  THENA  Auto)  THEN  nRAdd  \mkleeneopen{}u\mkleeneclose{}  (-3)\mcdot{}  THEN  Auto  THEN  nRNorm  0  THEN  Auto)




Home Index