---

Step * 1 1 of Lemma exp_mul


1. i : ℤ
2. n : ℤ
3. 0 < n
4. ∀[m:ℕ]. (i^(m * (n - 1)) = i^m^(n - 1) ∈ ℤ)
5. m : ℕ
6. i^((m * (n - 1)) + m) = (i^(m * (n - 1)) * i^m) ∈ ℤ
⊢ i^(m * n) = i^m^n ∈ ℤ
BY
{ ((NthHypEq (-1) THEN EqCD) THEN Auto) }

---

Latex:

---

Latex:

1.  i  :  \mBbbZ{}
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}[m:\mBbbN{}].  (i\^{}(m  *  (n  -  1))  =  i\^{}m\^{}(n  -  1))
5.  m  :  \mBbbN{}
6.  i\^{}((m  *  (n  -  1))  +  m)  =  (i\^{}(m  *  (n  -  1))  *  i\^{}m)
\mvdash{}  i\^{}(m  *  n)  =  i\^{}m\^{}n


By

---

Latex:
((NthHypEq  (-1)  THEN  EqCD)  THEN  Auto)

---

Home Index