Step * of Lemma nat-mul-absval

[n:ℕ]. ∀[x:ℤ].  ((n |x|) |n x| ∈ ℤ)
BY
(Auto THEN RWO "absval_mul" THEN Auto) }


Latex:


Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbZ{}].    ((n  *  |x|)  =  |n  *  x|)


By


Latex:
(Auto  THEN  RWO  "absval\_mul"  0  THEN  Auto)




Home Index