Nuprl Lemma : add-positive

[x,y:ℤ].  (0 < y) supposing (0 < and 0 < y)


Definitions occuring in Statement :  less_than: a < b uimplies: supposing a uall: [x:A]. B[x] add: m natural_number: $n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: guard: {T} or: P ∨ Q subtype_rel: A ⊆B all: x:A. B[x] implies:  Q
Lemmas referenced :  less_than_wf member-less_than equal-wf-base int_subtype_base add-monotonic
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality hypothesisEquality sqequalRule isect_memberEquality addEquality independent_isectElimination because_Cache equalityTransitivity equalitySymmetry intEquality inrFormation baseClosed applyEquality dependent_functionElimination independent_functionElimination

\mforall{}[x,y:\mBbbZ{}].    (0  <  x  +  y)  supposing  (0  <  x  and  0  <  y)

Date html generated: 2019_06_20-AM-11_22_36
Last ObjectModification: 2018_08_17-AM-11_56_34

Theory : arithmetic

Home Index