Nuprl Lemma : add-nonneg

x,y:ℤ.  (0 ≤ (x y)) supposing ((0 ≤ x) and (0 ≤ y))


Proof




Definitions occuring in Statement :  uimplies: supposing a le: A ≤ B all: x:A. B[x] add: m natural_number: $n int:
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a member: t ∈ T decidable: Dec(P) or: P ∨ Q uall: [x:A]. B[x] sq_type: SQType(T) implies:  Q guard: {T} prop: not: ¬A false: False iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q le: A ≤ B
Lemmas referenced :  decidable__int_equal subtype_base_sq int_subtype_base less_than_wf add-zero equal_wf zero-add or_wf iff_weakening_uiff le_wf le-iff-less-or-equal less_than'_wf add-positive
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut isect_memberFormation lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin because_Cache hypothesis unionElimination instantiate isectElimination cumulativity intEquality independent_isectElimination independent_functionElimination hypothesisEquality sqequalRule inrFormation natural_numberEquality addEquality inlFormation voidElimination addLevel introduction productElimination independent_pairEquality lambdaEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality isectEquality

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



Date html generated: 2016_05_13-PM-03_30_32
Last ObjectModification: 2015_12_26-AM-09_46_51

Theory : arithmetic


Home Index