---

Step * of Lemma r-archimedean-rabs

∀x:ℝ. ∃n:ℕ. (|x| ≤ r(n))
BY
{ (InstLemma `r-archimedean` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (RWO "rabs-as-rmax" 0 THENA Auto)
   THEN BLemma `rmax_lb`
   THEN Auto) }

1
1. x : ℝ
2. n : ℕ
3. r(-n) ≤ x
4. x ≤ r(n)
5. x ≤ r(n)
⊢ -(x) ≤ r(n)

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \mexists{}n:\mBbbN{}.  (|x|  \mleq{}  r(n))


By

---

Latex:
(InstLemma  `r-archimedean`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (RWO  "rabs-as-rmax"  0  THENA  Auto)
  THEN  BLemma  `rmax\_lb`
  THEN  Auto)

---

Home Index