Nuprl Lemma : sub_functionality_wrt_le

[i1,i2,j1,j2:ℤ].  ((i1 i2) ≤ (j1 j2)) supposing ((i2 ≥ j2 and (i1 ≤ j1))


Definitions occuring in Statement :  uimplies: supposing a uall: [x:A]. B[x] ge: i ≥  le: A ≤ B subtract: m int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a le: A ≤ B and: P ∧ Q subtract: m not: ¬A implies:  Q false: False prop: ge: i ≥  all: x:A. B[x] subtype_rel: A ⊆B top: Top uiff: uiff(P;Q) nat_plus: + less_than: a < b squash: T less_than': less_than'(a;b) true: True decidable: Dec(P) or: P ∨ Q
Lemmas referenced :  decidable__le le-add-cancel-alt mul-commutes mul-swap mul-distributes less_than_wf omega-shadow add-zero mul-associates minus-add not-le-2 zero-add zero-mul mul-distributes-right two-mul add-mul-special add-associates add-commutes add-swap one-mul minus-one-mul-top le_reflexive add_functionality_wrt_le le_wf ge_wf subtract_wf less_than'_wf minus-one-mul
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin hypothesis sqequalRule lemma_by_obid isectElimination hypothesisEquality independent_pairEquality lambdaEquality dependent_functionElimination because_Cache axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality intEquality voidElimination multiplyEquality natural_numberEquality independent_isectElimination applyEquality voidEquality addEquality minusEquality dependent_set_memberEquality independent_pairFormation imageMemberEquality baseClosed independent_functionElimination unionElimination

\mforall{}[i1,i2,j1,j2:\mBbbZ{}].    ((i1  -  i2)  \mleq{}  (j1  -  j2))  supposing  ((i2  \mgeq{}  j2  )  and  (i1  \mleq{}  j1))

Date html generated: 2016_05_13-PM-03_40_37
Last ObjectModification: 2016_01_14-PM-06_39_05

Theory : arithmetic

Home Index