Nuprl Lemma : imonomial-cons-req
∀v:ℤ List. ∀u,a:ℤ. ∀f:ℤ ⟶ ℝ. (real_term_value(f;imonomial-term(<a, [u / v]>)) = ((f u) * real_term_value(f;imonomial-t\000Cerm(<a, v>))))
Proof
Definitions occuring in Statement :
real_term_value: real_term_value(f;t),
req: x = y,
rmul: a * b,
real: ℝ,
imonomial-term: imonomial-term(m),
cons: [a / b],
list: T List,
all: ∀x:A. B[x],
apply: f a,
function: x:A ⟶ B[x],
pair: <a, b>,
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
uiff: uiff(P;Q),
and: P ∧ Q,
rev_uimplies: rev_uimplies(P;Q),
imonomial-term: imonomial-term(m),
top: Top,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
real_term_value: real_term_value(f;t),
itermMultiply: left (*) right,
int_term_ind: int_term_ind,
itermConstant: "const",
itermVar: vvar,
implies: P ⇒ Q
Lemmas referenced :
real_wf,
list_wf,
real_term_value_wf,
imonomial-term_wf,
cons_wf,
rmul_wf,
int-to-real_wf,
rmul-ac,
req_functionality,
imonomial-term-linear-req,
rmul_functionality,
req_weakening,
list_accum_cons_lemma,
list_accum_wf,
int_term_wf,
itermMultiply_wf,
itermConstant_wf,
itermVar_wf,
req_wf,
imonomial-req-lemma,
uiff_transitivity,
req_inversion,
rmul-assoc,
rmul-one-both
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
functionEquality,
intEquality,
cut,
introduction,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
functionExtensionality,
applyEquality,
hypothesisEquality,
independent_pairEquality,
natural_numberEquality,
because_Cache,
independent_isectElimination,
dependent_functionElimination,
productElimination,
sqequalRule,
isect_memberEquality,
voidElimination,
voidEquality,
lambdaEquality,
independent_functionElimination
Latex:
\mforall{}v:\mBbbZ{} List. \mforall{}u,a:\mBbbZ{}. \mforall{}f:\mBbbZ{} {}\mrightarrow{} \mBbbR{}. (real\_term\_value(f;imonomial-term(<a, [u / v]>)) = ((f u) * real\_term\000C\_value(f;imonomial-term(<a, v>))))
Date html generated:
2017_10_02-PM-07_19_48
Last ObjectModification:
2017_07_28-AM-07_21_27
Theory : reals
Home
Index