---

Step * of Lemma absval-sqequal-imax

∀[a:Top]. (imax(a;-a) ~ |a|)
BY
{ (Assert ⌜∀[a:ℤ]. (imax(a;-a) ~ |a|)⌝⋅ THENA Auto) }

1
1. a : ℤ
⊢ imax(a;-a) = |a| ∈ ℤ

2
1. ∀[a:ℤ]. (imax(a;-a) ~ |a|)
⊢ ∀[a:Top]. (imax(a;-a) ~ |a|)

---

Latex:

---

Latex:
\mforall{}[a:Top].  (imax(a;-a)  \msim{}  |a|)


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}[a:\mBbbZ{}].  (imax(a;-a)  \msim{}  |a|)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index