Step * of Lemma exp1

[i:ℤ]. (i^1 i ∈ ℤ)
BY
(Unfold `exp` THEN Reduce THEN Auto) }


Latex:


Latex:
\mforall{}[i:\mBbbZ{}].  (i\^{}1  =  i)


By


Latex:
(Unfold  `exp`  0  THEN  Reduce  0  THEN  Auto)




Home Index