---

Step * 1 of Lemma exp_mul


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 ∈ ℤ
BY
{ (InstLemma `exp_add` [⌜m * (n - 1)⌝;⌜m⌝;⌜i⌝]⋅ THENA Auto) }

1
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 ∈ ℤ

---

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{}
\mvdash{}  i\^{}(m  *  n)  =  i\^{}m\^{}n


By

---

Latex:
(InstLemma  `exp\_add`  [\mkleeneopen{}m  *  (n  -  1)\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index