---

Step * of Lemma rmax-req

∀[x,y:ℝ].  rmax(x;y) = y supposing x ≤ y
BY
{ ((Auto THEN BLemma `rleq_antisymmetry` THEN Auto)
   THEN (All (RWO "rleq-iff") THENA Auto)
   THEN RepeatFor 3 (ParallelLast')) }

1
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. N : ℕ+
5. m : {N...}
6. ((-2) * m) ≤ (n * ((y m) - x m))
⊢ ((-2) * m) ≤ (n * ((y m) - rmax(x;y) m))

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    rmax(x;y)  =  y  supposing  x  \mleq{}  y


By

---

Latex:
((Auto  THEN  BLemma  `rleq\_antisymmetry`  THEN  Auto)
  THEN  (All  (RWO  "rleq-iff")  THENA  Auto)
  THEN  RepeatFor  3  (ParallelLast'))

---

Home Index