Nuprl Lemma : log-from_wf
∀a:{a:ℝ| r0 < a} . ∀b:{b:ℝ| |b - rlog(a)| ≤ (r1/r(10))} . (log-from(a;b) ∈ {x:ℝ| x = rlog(a)} )
Proof
Definitions occuring in Statement :
log-from: log-from(a;b),
rlog: rlog(x),
rdiv: (x/y),
rleq: x ≤ y,
rless: x < y,
rabs: |x|,
rsub: x - y,
req: x = y,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
member: t ∈ T,
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
prop: ℙ,
so_apply: x[s],
subtype_rel: A ⊆r B,
uimplies: b supposing a,
rneq: x ≠ y,
guard: {T},
or: P ∨ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
true: True,
logseq-converges-ext,
cauchy-limit: cauchy-limit(n.x[n];c),
log-from: log-from(a;b),
accelerate: accelerate(k;f),
nat_plus: ℕ+,
has-value: (a)↓,
nat: ℕ,
le: A ≤ B,
false: False,
not: ¬A,
int_upper: {i...},
decidable: Dec(P),
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
top: Top,
real: ℝ,
nequal: a ≠ b ∈ T ,
sq_type: SQType(T)
Lemmas referenced :
req-from-converges,
logseq_wf,
rless_wf,
int-to-real_wf,
nat_wf,
rlog_wf,
logseq-converges-ext,
all_wf,
real_wf,
rleq_wf,
rabs_wf,
rsub_wf,
rdiv_wf,
rless-int,
converges-to_wf,
set_wf,
nat_plus_wf,
value-type-has-value,
int-value-type,
le_wf,
exp_wf2,
exp_wf4,
false_wf,
set-value-type,
cubic_converge_wf,
nat_plus_properties,
decidable__le,
satisfiable-full-omega-tt,
intformand_wf,
intformnot_wf,
intformle_wf,
itermConstant_wf,
itermMultiply_wf,
itermVar_wf,
intformless_wf,
int_formula_prop_and_lemma,
int_formula_prop_not_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_term_value_mul_lemma,
int_term_value_var_lemma,
int_formula_prop_less_lemma,
int_formula_prop_wf,
decidable__equal_int,
intformeq_wf,
int_formula_prop_eq_lemma,
decidable__lt,
less_than_wf,
subtype_base_sq,
int_subtype_base,
equal-wf-base,
true_wf,
cauchy-limit_wf,
converges-cauchy-witness,
regular-int-seq_wf,
req_inversion,
req_transitivity,
req_weakening,
req_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
sqequalRule,
lambdaEquality,
setElimination,
rename,
dependent_set_memberEquality,
because_Cache,
hypothesis,
natural_numberEquality,
hypothesisEquality,
applyEquality,
instantiate,
setEquality,
independent_isectElimination,
inrFormation,
dependent_functionElimination,
productElimination,
independent_functionElimination,
independent_pairFormation,
imageMemberEquality,
baseClosed,
functionExtensionality,
callbyvalueReduce,
sqleReflexivity,
intEquality,
multiplyEquality,
unionElimination,
dependent_pairFormation,
int_eqEquality,
isect_memberEquality,
voidElimination,
voidEquality,
computeAll,
divideEquality,
equalityTransitivity,
equalitySymmetry,
addLevel,
cumulativity,
Error :applyLambdaEquality,
imageElimination
Latex:
\mforall{}a:\{a:\mBbbR{}| r0 < a\} . \mforall{}b:\{b:\mBbbR{}| |b - rlog(a)| \mleq{} (r1/r(10))\} . (log-from(a;b) \mmember{} \{x:\mBbbR{}| x = rlog(a)\} )
Date html generated:
2016_10_26-PM-00_37_38
Last ObjectModification:
2016_09_18-PM-10_10_20
Theory : reals_2
Home
Index