Nuprl Lemma : satisfies-integer-inequality_wf

[xs,as:ℤ List].  (xs ⋅ as ≥0 ∈ ℙ)


Proof




Definitions occuring in Statement :  satisfies-integer-inequality: xs ⋅ as ≥0 list: List uall: [x:A]. B[x] prop: member: t ∈ T int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T satisfies-integer-inequality: xs ⋅ as ≥0 prop: and: P ∧ Q subtype_rel: A ⊆B uimplies: supposing a ge: i ≥ 
Lemmas referenced :  list_wf integer-dot-product_wf ge_wf less_than_wf int_subtype_base list_subtype_base equal-wf-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule productEquality lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality baseApply closedConclusion baseClosed hypothesisEquality applyEquality independent_isectElimination hypothesis because_Cache natural_numberEquality equalityTransitivity equalitySymmetry axiomEquality isect_memberEquality

Latex:
\mforall{}[xs,as:\mBbbZ{}  List].    (xs  \mcdot{}  as  \mgeq{}0  \mmember{}  \mBbbP{})



Date html generated: 2016_05_14-AM-06_56_17
Last ObjectModification: 2016_01_14-PM-08_44_37

Theory : omega


Home Index