Nuprl Lemma : add_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] le: A ≤ B add: m int:
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a rev_uimplies: rev_uimplies(P;Q) or: P ∨ Q implies:  Q guard: {T} prop: uall: [x:A]. B[x] subtype_rel: A ⊆B le: A ≤ B not: ¬A false: False top: Top
Lemmas referenced :  le-iff-less-or-equal add-monotonic equal-wf-base int_subtype_base less_than_wf less_than'_wf le_wf add-commutes
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_functionElimination thin hypothesisEquality hypothesis productElimination independent_isectElimination addEquality unionElimination inlFormation independent_functionElimination sqequalRule inrFormation isectElimination because_Cache applyEquality intEquality baseApply closedConclusion baseClosed isect_memberFormation independent_pairEquality lambdaEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality voidElimination voidEquality

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

Date html generated: 2019_06_20-AM-11_22_52
Last ObjectModification: 2018_08_17-AM-11_59_31

Theory : arithmetic

Home Index