Nuprl Lemma : add_functionality_wrt_lt

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


Definitions occuring in Statement :  less_than: a < b uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B add: m int:
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T implies:  Q uall: [x:A]. B[x] uimplies: supposing a prop: and: P ∧ Q uiff: uiff(P;Q) or: P ∨ Q guard: {T}
Lemmas referenced :  add-monotonic le_wf less_than_wf member-less_than equal_wf le-iff-less-or-equal
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_functionElimination thin hypothesisEquality independent_functionElimination hypothesis isectElimination addEquality because_Cache intEquality isect_memberFormation sqequalRule isect_memberEquality independent_isectElimination equalityTransitivity equalitySymmetry productElimination lemma_by_obid unionElimination inrFormation inlFormation

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

Date html generated: 2019_06_20-AM-11_22_54
Last ObjectModification: 2018_08_17-PM-00_00_07

Theory : arithmetic

Home Index