Nuprl Lemma : add_functionality_wrt_le

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


Proof




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 prop: uall: [x:A]. B[x] guard: {T} le: A ≤ B not: ¬A implies:  Q false: False top: Top
Lemmas referenced :  le-iff-less-or-equal equal_wf less_than_wf less_than'_wf le_wf add-commutes
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_functionElimination thin hypothesisEquality hypothesis productElimination independent_isectElimination addEquality unionElimination inlFormation isectElimination intEquality sqequalRule inrFormation because_Cache isect_memberFormation introduction independent_pairEquality lambdaEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality voidElimination addMonotonic voidEquality

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



Date html generated: 2016_05_13-PM-03_30_20
Last ObjectModification: 2015_12_26-AM-09_47_06

Theory : arithmetic


Home Index