Nuprl Lemma : near-root_wf
∀k:{2...}. ∀p:{p:ℤ| (0 ≤ p) ∨ (↑isOdd(k))} . ∀q,n:ℕ+.
(near-root(k;p;q;n) ∈ {r:ℤ × ℕ+| let a,b = r in (0 ≤ p ⇐⇒ 0 ≤ a) ∧ (|(r(a))/b^k - (r(p)/r(q))| < (r1/r(n)))} )
Proof
Definitions occuring in Statement :
near-root: near-root(k;p;q;n),
rdiv: (x/y),
rless: x < y,
rabs: |x|,
rnexp: x^k1,
int-rdiv: (a)/k1,
rsub: x - y,
int-to-real: r(n),
isOdd: isOdd(n),
int_upper: {i...},
nat_plus: ℕ+,
assert: ↑b,
le: A ≤ B,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
spread: spread def,
product: x:A × B[x],
natural_number: $n,
int: ℤ
Definitions unfolded in proof :
near-root-rational-ext,
sq_exists: ∃x:A [B[x]],
decidable: Dec(P),
rneq: x ≠ y,
top: Top,
exists: ∃x:A. B[x],
satisfiable_int_formula: satisfiable_int_formula(fmla),
guard: {T},
nequal: a ≠ b ∈ T ,
so_apply: x[s],
int_nzero: ℤ-o,
nat_plus: ℕ+,
not: ¬A,
false: False,
less_than': less_than'(a;b),
le: A ≤ B,
uimplies: b supposing a,
implies: P ⇒ Q,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
so_lambda: λ2x.t[x],
prop: ℙ,
or: P ∨ Q,
int_upper: {i...},
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
member: t ∈ T,
all: ∀x:A. B[x]
Lemmas referenced :
set_wf,
false_wf,
int_formula_prop_not_lemma,
intformnot_wf,
decidable__lt,
rless-int,
rdiv_wf,
int-to-real_wf,
int_subtype_base,
equal-wf-base,
int_formula_prop_wf,
int_formula_prop_less_lemma,
int_term_value_constant_lemma,
int_term_value_var_lemma,
int_formula_prop_eq_lemma,
int_formula_prop_and_lemma,
intformless_wf,
itermConstant_wf,
itermVar_wf,
intformeq_wf,
intformand_wf,
full-omega-unsat,
int_upper_properties,
nat_plus_properties,
nequal_wf,
less_than_wf,
subtype_rel_sets,
int-rdiv_wf,
upper_subtype_nat,
rnexp_wf,
rsub_wf,
rabs_wf,
rless_wf,
iff_wf,
sq_exists_wf,
nat_plus_wf,
isOdd_wf,
assert_wf,
le_wf,
or_wf,
all_wf,
int_upper_wf,
subtype_rel_self,
near-root-rational-ext
Rules used in proof :
dependent_set_memberEquality,
unionElimination,
inrFormation,
baseClosed,
voidEquality,
voidElimination,
isect_memberEquality,
dependent_functionElimination,
int_eqEquality,
dependent_pairFormation,
independent_functionElimination,
approximateComputation,
independent_pairFormation,
independent_isectElimination,
productElimination,
productEquality,
lambdaEquality,
because_Cache,
rename,
setElimination,
hypothesisEquality,
intEquality,
setEquality,
natural_numberEquality,
functionEquality,
isectElimination,
sqequalHypSubstitution,
introduction,
sqequalRule,
hypothesis,
extract_by_obid,
instantiate,
thin,
applyEquality,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}k:\{2...\}. \mforall{}p:\{p:\mBbbZ{}| (0 \mleq{} p) \mvee{} (\muparrow{}isOdd(k))\} . \mforall{}q,n:\mBbbN{}\msupplus{}.
(near-root(k;p;q;n) \mmember{} \{r:\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}|
let a,b = r
in (0 \mleq{} p \mLeftarrow{}{}\mRightarrow{} 0 \mleq{} a) \mwedge{} (|(r(a))/b\^{}k - (r(p)/r(q))| < (r1/r(n)))\} )
Date html generated:
2018_05_22-PM-02_22_09
Last ObjectModification:
2018_05_21-AM-00_42_42
Theory : reals
Home
Index