---

Step * of Lemma rat2real-qmax

∀[a,b:ℚ].  (rat2real(qmax(a;b)) = rmax(rat2real(a);rat2real(b)))
BY
{ (Auto
   THEN Assert ⌜(rat2real(qmax(a;b)) ≤ rmax(rat2real(a);rat2real(b)))
                ∧ (rmax(rat2real(a);rat2real(b)) ≤ rat2real(qmax(a;b)))⌝⋅
   THEN Auto
   THEN ((BLemma `rmax_lb` ORELSE BLemma `rmax_ub`) THENA Auto)
   THEN (RWO "rleq-rat2real" 0 THENA Auto)
   THEN RWO "qmax_ub qmax_lb" 0
   THEN Auto) }

1
1. a : ℚ
2. b : ℚ
⊢ ((a ≤ a) ∧ (b ≤ a)) ∨ ((a ≤ b) ∧ (b ≤ b))

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbQ{}].    (rat2real(qmax(a;b))  =  rmax(rat2real(a);rat2real(b)))


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}(rat2real(qmax(a;b))  \mleq{}  rmax(rat2real(a);rat2real(b)))
                            \mwedge{}  (rmax(rat2real(a);rat2real(b))  \mleq{}  rat2real(qmax(a;b)))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  ((BLemma  `rmax\_lb`  ORELSE  BLemma  `rmax\_ub`)  THENA  Auto)
  THEN  (RWO  "rleq-rat2real"  0  THENA  Auto)
  THEN  RWO  "qmax\_ub  qmax\_lb"  0
  THEN  Auto)

---

Home Index