---

Step * 2 1 of Lemma absval-sqequal-imax


1. ∀[a:ℤ]. (imax(a;-a) ~ |a|)
2. a : Base
3. (imax(a;-a))↓
⊢ imax(a;-a) ≤ |a|
BY
{ (RWO "1" 0 THEN Auto THEN RepUR ``imax`` -1 THEN HasValueD (-1) THEN HasValueD (-2) THEN HasValueD (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}[a:\mBbbZ{}].  (imax(a;-a)  \msim{}  |a|)
2.  a  :  Base
3.  (imax(a;-a))\mdownarrow{}
\mvdash{}  imax(a;-a)  \mleq{}  |a|


By

---

Latex:
(RWO  "1"  0
  THEN  Auto
  THEN  RepUR  ``imax``  -1
  THEN  HasValueD  (-1)
  THEN  HasValueD  (-2)
  THEN  HasValueD  (-1)
  THEN  Auto)

---

Home Index