Nuprl Lemma : add-positive-nonneg

[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] le: A ≤ B add: m natural_number: $n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: all: x:A. B[x] implies:  Q or: P ∨ Q guard: {T} subtype_rel: A ⊆B false: False less_than: a < b squash: T le: A ≤ B and: P ∧ Q not: ¬A
Lemmas referenced :  less_than_wf member-less_than le_wf add-monotonic less-trichotomy equal-wf-base int_subtype_base
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 dependent_functionElimination independent_functionElimination unionElimination inrFormation baseClosed applyEquality inlFormation voidElimination imageElimination productElimination

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

Date html generated: 2019_06_20-AM-11_22_38
Last ObjectModification: 2018_08_17-AM-11_57_33

Theory : arithmetic

Home Index