---

Step * of Lemma efficient-exp

∀i:ℤ. ∀n:ℕ.  (∃j:{ℤ| (j = i^n ∈ ℤ)})
BY
{ ((D 0 THENA Auto) THEN (CompNatInd' THENA Auto) THEN CaseNat 1 `n') }

1
1. i : ℤ
2. n : ℕ
3. ∀n1:ℕn. (∃j:{ℤ| (j = i^n1 ∈ ℤ)})
4. n = 1 ∈ ℤ
⊢ ∃j:{ℤ| (j = i^1 ∈ ℤ)}

2
1. i : ℤ
2. n : ℕ
3. ∀n1:ℕn. (∃j:{ℤ| (j = i^n1 ∈ ℤ)})
4. ¬(n = 1 ∈ ℤ)
⊢ ∃j:{ℤ| (j = i^n ∈ ℤ)}

---

Latex:

---

Latex:
\mforall{}i:\mBbbZ{}.  \mforall{}n:\mBbbN{}.    (\mexists{}j:\{\mBbbZ{}|  (j  =  i\^{}n)\})


By

---

Latex:
((D  0  THENA  Auto)  THEN  (CompNatInd'  THENA  Auto)  THEN  CaseNat  1  `n')

---

Home Index