---

Step * of Lemma assert-is_power

∀n:ℕ+. ∀x:ℤ.  (↑is_power(n;x) ⇐⇒ ∃r:ℤ. (x = r^n ∈ ℤ))
BY
{ (Intros
   THEN (InstLemma `mod2-cases` [⌜n⌝]⋅ THENA Auto)
   THEN D -1
   THEN RepUR ``is_power`` 0
   THEN HypSubst' (-1) 0
   THEN Reduce 0
   THEN AutoSplit
   THEN (RWW "assert-is-power" 0 THENA Auto)
   THEN (All (RWO "mod2-is-zero mod2-is-one") THENA Auto)
   THEN ExRepD
   THEN Eliminate ⌜n⌝⋅
   THEN (Assert 0 ≤ n1 BY
               Auto)
   THEN ThinVar `n'
   THEN Auto
   THEN Try (Complete (ParallelLast))) }

1
1. n1 : ℤ
2. x : ℤ
3. x < 0
4. 0 ≤ n1
5. ∃r:ℤ. (x = r^(2 * n1) ∈ ℤ)
⊢ False

2
1. n1 : ℤ
2. x : ℤ
3. ¬x < 0
4. 0 ≤ n1
5. ∃r:ℤ. (x = r^(2 * n1) ∈ ℤ)
⊢ ∃r:ℕ. (x = r^(2 * n1) ∈ ℤ)

3
1. n1 : ℤ
2. x : ℤ
3. x < 0
4. 0 ≤ n1
5. ∃r:ℕ. ((-x) = r^((2 * n1) + 1) ∈ ℤ)
⊢ ∃r:ℤ. (x = r^((2 * n1) + 1) ∈ ℤ)

4
1. n1 : ℤ
2. x : ℤ
3. x < 0
4. 0 ≤ n1
5. ∃r:ℤ. (x = r^((2 * n1) + 1) ∈ ℤ)
⊢ ∃r:ℕ. ((-x) = r^((2 * n1) + 1) ∈ ℤ)

5
1. n1 : ℤ
2. x : ℤ
3. ¬x < 0
4. 0 ≤ n1
5. ∃r:ℤ. (x = r^((2 * n1) + 1) ∈ ℤ)
⊢ ∃r:ℕ. (x = r^((2 * n1) + 1) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbZ{}.    (\muparrow{}is\_power(n;x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}r:\mBbbZ{}.  (x  =  r\^{}n))


By

---

Latex:
(Intros
  THEN  (InstLemma  `mod2-cases`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RepUR  ``is\_power``  0
  THEN  HypSubst'  (-1)  0
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  (RWW  "assert-is-power"  0  THENA  Auto)
  THEN  (All  (RWO  "mod2-is-zero  mod2-is-one")  THENA  Auto)
  THEN  ExRepD
  THEN  Eliminate  \mkleeneopen{}n\mkleeneclose{}\mcdot{}
  THEN  (Assert  0  \mleq{}  n1  BY
                          Auto)
  THEN  ThinVar  `n'
  THEN  Auto
  THEN  Try  (Complete  (ParallelLast)))

---

Home Index