---

Step * of Lemma efficient-exp

∀i:ℤ. ∀n:ℕ.  (∃j:ℤ [(j = i^n ∈ ℤ)])
BY
{ ((D 0 THENA Auto)
   THEN (Evaluate ⌜m = i ∈ ℤ⌝⋅ THENA Auto)
   THEN RevHypSubst' (-1) 0
   THEN ThinVar `i'
   THEN RenameVar `i' (-1)
   THEN (CompNatInd' THENA Auto)
   THEN CaseNat 1 `n'
   THEN Try (Complete ((With ⌜i⌝ (D 0)⋅ THEN Auto)))) }

1
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  (Evaluate  \mkleeneopen{}m  =  i\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RevHypSubst'  (-1)  0
  THEN  ThinVar  `i'
  THEN  RenameVar  `i'  (-1)
  THEN  (CompNatInd'  THENA  Auto)
  THEN  CaseNat  1  `n'
  THEN  Try  (Complete  ((With  \mkleeneopen{}i\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))))

---

Home Index