---

Step * of Lemma rmin-int

∀[a,b:ℤ].  (rmin(r(a);r(b)) = r(imin(a;b)))
BY
{ ((Auto THEN (BLemma `req-iff-bdd-diff` THENA Auto))
   THEN BLemma `trivial-bdd-diff`
   THEN Auto
   THEN RepUR ``int-to-real rmin`` 0) }

1
1. a : ℤ
2. b : ℤ
3. n : ℕ+
⊢ imin(2 * n * a;2 * n * b) = (2 * n * imin(a;b)) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].    (rmin(r(a);r(b))  =  r(imin(a;b)))


By

---

Latex:
((Auto  THEN  (BLemma  `req-iff-bdd-diff`  THENA  Auto))
  THEN  BLemma  `trivial-bdd-diff`
  THEN  Auto
  THEN  RepUR  ``int-to-real  rmin``  0)

---

Home Index