---

Step * of Lemma rmin-positive

∀x,y:ℝ.  ((rpositive(x) ∧ rpositive(y)) ⇒ rpositive(rmin(x;y)))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (RWO "rpositive-iff" 0 THENA Auto)
   THEN RepUR ``rmin`` 0
   THEN Auto
   THEN All (Unfold `rpositive2`)
   THEN ExRepD
   THEN With ⌜imax(n1;n)⌝ (D 0)⋅
   THEN Reduce 0
   THEN EAuto 1) }

1
1. x : ℝ
2. y : ℝ
3. n1 : ℕ+
4. ∀m:ℕ+. ((n1 ≤ m) ⇒ (m ≤ (n1 * (x m))))
5. n : ℕ+
6. ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * (y m))))
7. m : ℕ+
8. imax(n1;n) ≤ m
⊢ m ≤ (imax(n1;n) * imin(x m;y m))

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    ((rpositive(x)  \mwedge{}  rpositive(y))  {}\mRightarrow{}  rpositive(rmin(x;y)))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (RWO  "rpositive-iff"  0  THENA  Auto)
  THEN  RepUR  ``rmin``  0
  THEN  Auto
  THEN  All  (Unfold  `rpositive2`)
  THEN  ExRepD
  THEN  With  \mkleeneopen{}imax(n1;n)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Reduce  0
  THEN  EAuto  1)

---

Home Index