Nuprl Lemma : ring_term_value_wf
∀[r:Rng]. ∀[f:ℤ ⟶ |r|]. ∀[t:int_term()]. (ring_term_value(f;t) ∈ |r|)
Proof
Definitions occuring in Statement :
ring_term_value: ring_term_value(f;t),
rng: Rng,
rng_car: |r|,
int_term: int_term(),
uall: ∀[x:A]. B[x],
member: t ∈ T,
function: x:A ⟶ B[x],
int: ℤ
Definitions unfolded in proof :
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2;s3;s4],
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_apply: x[s],
so_lambda: λ2x.t[x],
rng: Rng,
ring_term_value: ring_term_value(f;t),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
rng_wf,
rng_times_wf,
rng_minus_wf,
int_term_wf,
rng_plus_wf,
infix_ap_wf,
int-to-ring_wf,
rng_car_wf,
int_term_ind_wf_simple
Rules used in proof :
functionEquality,
isect_memberEquality,
equalitySymmetry,
equalityTransitivity,
axiomEquality,
functionExtensionality,
applyEquality,
intEquality,
lambdaEquality,
hypothesisEquality,
hypothesis,
because_Cache,
rename,
setElimination,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
sqequalRule,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[r:Rng]. \mforall{}[f:\mBbbZ{} {}\mrightarrow{} |r|]. \mforall{}[t:int\_term()]. (ring\_term\_value(f;t) \mmember{} |r|)
Date html generated:
2018_05_21-PM-03_15_25
Last ObjectModification:
2018_01_25-PM-02_16_33
Theory : rings_1
Home
Index