---

Step * of Lemma rmax-positive

∀x,y:ℝ.  ((rpositive(x) ∨ rpositive(y)) ⇒ rpositive(rmax(x;y)))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (RWO "rpositive-iff" 0 THENA Auto)
   THEN Auto
   THEN D -1
   THEN RepeatFor 4 (ParallelLast)
   THEN RepUR ``rmax`` 0
   THEN (RWO "imax_unfold" 0 THENA Auto)
   THEN AutoSplit) }

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

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

---

Latex:

---

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


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (RWO  "rpositive-iff"  0  THENA  Auto)
  THEN  Auto
  THEN  D  -1
  THEN  RepeatFor  4  (ParallelLast)
  THEN  RepUR  ``rmax``  0
  THEN  (RWO  "imax\_unfold"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index