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