---

Step * of Lemma rnexp-int

No Annotations
∀[k:ℕ]. ∀[z:ℤ].  (r(z)^k = r(z^k))
BY
{ (InductionOnNat
   THEN Auto
   THEN RWO "rnexp-req" 0
   THEN Auto
   THEN Reduce 0
   THEN Try (AutoSplit)
   THEN RWO "-2" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbN{}].  \mforall{}[z:\mBbbZ{}].    (r(z)\^{}k  =  r(z\^{}k))


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  RWO  "rnexp-req"  0
  THEN  Auto
  THEN  Reduce  0
  THEN  Try  (AutoSplit)
  THEN  RWO  "-2"  0
  THEN  Auto)

---

Home Index