---

Step * of Lemma exp_mul

No Annotations
∀[i:ℤ]. ∀[n,m:ℕ].  (i^(m * n) = i^m^n ∈ ℤ)
BY
{ (InductionOnNat THEN Reduce 0 THEN Auto) }

1
1. i : ℤ
2. n : ℤ
3. 0 < n
4. ∀[m:ℕ]. (i^(m * (n - 1)) = i^m^(n - 1) ∈ ℤ)
5. m : ℕ
⊢ i^(m * n) = i^m^n ∈ ℤ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[i:\mBbbZ{}].  \mforall{}[n,m:\mBbbN{}].    (i\^{}(m  *  n)  =  i\^{}m\^{}n)


By

---

Latex:
(InductionOnNat  THEN  Reduce  0  THEN  Auto)

---

Home Index