---

Step * 1 1 1 of Lemma r-archimedean-implies


1. x : ℝ
2. v : ℝ
3. v1 : ℝ
⊢ ((v1 * x) ≤ v) ⇒ (r0 < v) ⇒ (r0 < v1) ⇒ (((r1/v) * x) ≤ (r1/v1))
BY
{ Auto }

1
1. x : ℝ
2. v : ℝ
3. v1 : ℝ
4. (v1 * x) ≤ v
5. r0 < v
6. r0 < v1
⊢ ((r1/v) * x) ≤ (r1/v1)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  v  :  \mBbbR{}
3.  v1  :  \mBbbR{}
\mvdash{}  ((v1  *  x)  \mleq{}  v)  {}\mRightarrow{}  (r0  <  v)  {}\mRightarrow{}  (r0  <  v1)  {}\mRightarrow{}  (((r1/v)  *  x)  \mleq{}  (r1/v1))


By

---

Latex:
Auto

---

Home Index