---

Step * of Lemma assert-is-power

No Annotations
∀n:ℕ+. ∀x:ℕ.  (↑is-power(n;x) ⇐⇒ ∃r:ℕ. (x = r^n ∈ ℤ))
BY
{ (Intros
   THEN Unfold `is-power` 0
   THEN (InstLemma `iroot-property` [⌜n⌝;⌜x⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜iroot(n;x)⌝⋅ THENA Auto)
   THEN All Thin
   THEN (CallByValueReduce 0 THENA Auto)
   THEN RW assert_pushdownC 0
   THEN Auto) }

1
1. n : ℕ+
2. x : ℕ
3. v : ℕ
4. v^n ≤ x
5. x < (v + 1)^n
6. v^n = x ∈ ℤ
⊢ ∃r:ℕ. (x = r^n ∈ ℤ)

2
1. n : ℕ+
2. x : ℕ
3. v : ℕ
4. v^n ≤ x
5. x < (v + 1)^n
6. ∃r:ℕ. (x = r^n ∈ ℤ)
⊢ v^n = x ∈ ℤ

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbN{}.    (\muparrow{}is-power(n;x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}r:\mBbbN{}.  (x  =  r\^{}n))


By

---

Latex:
(Intros
  THEN  Unfold  `is-power`  0
  THEN  (InstLemma  `iroot-property`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}iroot(n;x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  RW  assert\_pushdownC  0
  THEN  Auto)

---

Home Index