---

Step * of Lemma rng_nexp-int

∀[n:ℕ]. ∀[a:ℤ].  ((a ↑ℤ-rng n) = a^n ∈ ℤ)
BY
{ (RepUR ``rng_nexp mon_nat_op nat_op exp`` 0
   THEN InductionOnNat
   THEN RecUnfold `itop` 0
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN RepeatFor 2 (OldAutoSplit)
   THEN RWO "3" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a:\mBbbZ{}].    ((a  \muparrow{}\mBbbZ{}-rng  n)  =  a\^{}n)


By

---

Latex:
(RepUR  ``rng\_nexp  mon\_nat\_op  nat\_op  exp``  0
  THEN  InductionOnNat
  THEN  RecUnfold  `itop`  0
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  RepeatFor  2  (OldAutoSplit)
  THEN  RWO  "3"  0
  THEN  Auto)

---

Home Index