Nuprl Lemma : mul-monomials_wf
∀[m1,m2:iMonomial()]. (mul-monomials(m1;m2) ∈ iMonomial())
Proof
Definitions occuring in Statement :
mul-monomials: mul-monomials(m1;m2),
iMonomial: iMonomial(),
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
iMonomial: iMonomial(),
mul-monomials: mul-monomials(m1;m2),
has-value: (a)↓,
uimplies: b supposing a,
int_nzero: ℤ-o,
nequal: a ≠ b ∈ T ,
not: ¬A,
implies: P ⇒ Q,
false: False,
prop: ℙ
Lemmas referenced :
value-type-has-value,
int-value-type,
list_wf,
list-value-type,
merge-int-accum_wf,
merge-int-accum-sq,
iMonomial_wf,
int_entire_a,
equal_wf,
nequal_wf,
merge-int_wf,
subtype_rel_self,
sorted_wf,
merge-int-sorted
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalHypSubstitution,
productElimination,
thin,
sqequalRule,
callbyvalueReduce,
extract_by_obid,
isectElimination,
intEquality,
independent_isectElimination,
hypothesis,
multiplyEquality,
setElimination,
rename,
hypothesisEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality,
because_Cache,
independent_pairEquality,
dependent_set_memberEquality,
lambdaFormation,
independent_functionElimination,
voidElimination,
natural_numberEquality
Latex:
\mforall{}[m1,m2:iMonomial()]. (mul-monomials(m1;m2) \mmember{} iMonomial())
Date html generated:
2017_09_29-PM-05_53_13
Last ObjectModification:
2017_07_26-PM-01_42_44
Theory : omega
Home
Index