### Nuprl Lemma : poly-coeff-of_wf

`∀[vs:ℤ List]. ∀[p:iPolynomial()].  (poly-coeff-of(vs;p) ∈ ℤ)`

Proof

Definitions occuring in Statement :  poly-coeff-of: `poly-coeff-of(vs;p)` iPolynomial: `iPolynomial()` list: `T List` uall: `∀[x:A]. B[x]` member: `t ∈ T` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` poly-coeff-of: `poly-coeff-of(vs;p)` so_lambda: `so_lambda(x,y,z.t[x; y; z])` iMonomial: `iMonomial()` int_nzero: `ℤ-o` so_apply: `x[s1;s2;s3]` iPolynomial: `iPolynomial()`
Lemmas referenced :  list_ind_wf iMonomial_wf ifthenelse_wf intlex_wf list_wf iPolynomial_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis intEquality natural_numberEquality lambdaEquality spreadEquality hypothesisEquality setElimination rename axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[vs:\mBbbZ{}  List].  \mforall{}[p:iPolynomial()].    (poly-coeff-of(vs;p)  \mmember{}  \mBbbZ{})

Date html generated: 2016_05_14-AM-07_10_38
Last ObjectModification: 2015_12_26-PM-01_07_00

Theory : omega

Home Index