---

Step * of Lemma exp-is-zero

∀[x:ℤ]. ∀[n:ℕ].  uiff(x^n = 0 ∈ ℤ;0 < n ∧ (x = 0 ∈ ℤ))
BY
{ (InductionOnNat
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN RWO "exp1 exp_step" 0
   THEN Auto
   THEN Try ((HypSubst' (-1) 0 THEN Auto))
   THEN (FLemma `int_entire` [-1] THENM D -1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  \mforall{}[n:\mBbbN{}].    uiff(x\^{}n  =  0;0  <  n  \mwedge{}  (x  =  0))


By

---

Latex:
(InductionOnNat
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  RWO  "exp1  exp\_step"  0
  THEN  Auto
  THEN  Try  ((HypSubst'  (-1)  0  THEN  Auto))
  THEN  (FLemma  `int\_entire`  [-1]  THENM  D  -1)
  THEN  Auto)

---

Home Index