Step
*
of Lemma
integer-nth-root2
∀n:{n:ℕ+| (n mod 2) = 1 ∈ ℤ} . ∀x:{...0}. (∃r:{{...0}| (r - 1^n < x ∧ (x ≤ r^n))})
BY
{ (Auto
THEN (InstLemma `integer-nth-root-ext` [⌜n⌝;⌜-x⌝]⋅ THENA Auto)
THEN skip{(D -1
THEN With ⌜-r⌝ (D 0)⋅
THEN Auto
THEN (Subst' (-r) - 1 ~ -(r + 1) 0 THENA Auto)
THEN (RWO "exp-minus" 0 THENA Auto)
THEN (Subst' n mod 2 ~ 1 0 THENA Auto)
THEN Reduce 0
THEN Auto')}) }
1
1. n : {n:ℕ+| (n mod 2) = 1 ∈ ℤ} @i
2. x : {...0}@i
3. ∃r:{ℕ| ((r^n ≤ (-x)) ∧ -x < r + 1^n)}
⊢ ∃r:{{...0}| (r - 1^n < x ∧ (x ≤ r^n))}
Latex:
Latex:
\mforall{}n:\{n:\mBbbN{}\msupplus{}| (n mod 2) = 1\} . \mforall{}x:\{...0\}. (\mexists{}r:\{\{...0\}| (r - 1\^{}n < x \mwedge{} (x \mleq{} r\^{}n))\})
By
Latex:
(Auto
THEN (InstLemma `integer-nth-root-ext` [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}-x\mkleeneclose{}]\mcdot{} THENA Auto)
THEN skip\{(D -1
THEN With \mkleeneopen{}-r\mkleeneclose{} (D 0)\mcdot{}
THEN Auto
THEN (Subst' (-r) - 1 \msim{} -(r + 1) 0 THENA Auto)
THEN (RWO "exp-minus" 0 THENA Auto)
THEN (Subst' n mod 2 \msim{} 1 0 THENA Auto)
THEN Reduce 0
THEN Auto')\})
Home
Index