Nuprl Lemma : imonomial-term-add-req
∀vs:ℤ List. ∀a,b:ℤ-o. ∀f:ℤ ⟶ ℝ. ((real_term_value(f;imonomial-term(<a, vs>)) + real_term_value(f;imonomial-term(<b, vs\000C>))) = real_term_value(f;imonomial-term(<a + b, vs>)))
Proof
Definitions occuring in Statement :
real_term_value: real_term_value(f;t),
req: x = y,
radd: a + b,
real: ℝ,
imonomial-term: imonomial-term(m),
list: T List,
int_nzero: ℤ-o,
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
pair: <a, b>,
add: n + m,
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
int_nzero: ℤ-o,
uimplies: b supposing a,
uiff: uiff(P;Q),
and: P ∧ Q,
rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :
real_wf,
int_nzero_wf,
list_wf,
radd_wf,
real_term_value_wf,
imonomial-term_wf,
rmul_wf,
int-to-real_wf,
req_weakening,
req_functionality,
radd_functionality,
imonomial-term-linear-req,
req_transitivity,
req_inversion,
rmul-distrib,
rmul_functionality,
radd-int
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,
setElimination,
rename,
because_Cache,
natural_numberEquality,
addEquality,
independent_isectElimination,
dependent_functionElimination,
productElimination
Latex:
\mforall{}vs:\mBbbZ{} List. \mforall{}a,b:\mBbbZ{}\msupminus{}\msupzero{}. \mforall{}f:\mBbbZ{} {}\mrightarrow{} \mBbbR{}.
((real\_term\_value(f;imonomial-term(<a, vs>)) + real\_term\_value(f;imonomial-term(<b, vs>))) = real\_\000Cterm\_value(f;imonomial-term(<a + b, vs>)))
Date html generated:
2017_10_02-PM-07_19_08
Last ObjectModification:
2017_04_03-AM-00_43_06
Theory : reals
Home
Index