---

Step * of Lemma less-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