### Nuprl Lemma : add-wf-bar-int

`∀[x,y:bar(ℤ)].  (x + y ∈ bar(ℤ))`

Proof

Definitions occuring in Statement :  bar: `bar(T)` uall: `∀[x:A]. B[x]` member: `t ∈ T` add: `n + m` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` cand: `A c∧ B` guard: `{T}` or: `P ∨ Q` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` implies: `P `` Q`
Lemmas referenced :  subtype_bar2 base_wf int_subtype_base value-type_wf subtype_rel_self bar-base add-wf-bar subtype_barSqtype_base int-value-type
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesis independent_isectElimination independent_pairFormation sqequalRule inrFormation because_Cache hypothesisEquality applyEquality dependent_functionElimination independent_functionElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[x,y:bar(\mBbbZ{})].    (x  +  y  \mmember{}  bar(\mBbbZ{}))

Date html generated: 2016_07_08-PM-05_18_51
Last ObjectModification: 2015_12_27-PM-05_17_13

Theory : bar!type

Home Index