Nuprl Lemma : condition-implies-le

[a,b,c,d:ℤ].  (a ≤ b) supposing ((c ≤ d) and ((b a) (d c) ∈ ℤ))


Definitions occuring in Statement :  uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B subtract: m int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a rev_uimplies: rev_uimplies(P;Q) le: A ≤ B guard: {T} all: x:A. B[x] prop: not: ¬A implies:  Q false: False
Lemmas referenced :  le-iff-nonneg le_transitivity subtract_wf le_weakening less_than'_wf le_wf equal_wf
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesisEquality hypothesis productElimination independent_isectElimination equalitySymmetry natural_numberEquality dependent_functionElimination because_Cache intEquality isect_memberFormation introduction sqequalRule independent_pairEquality lambdaEquality axiomEquality isect_memberEquality equalityTransitivity voidElimination

\mforall{}[a,b,c,d:\mBbbZ{}].    (a  \mleq{}  b)  supposing  ((c  \mleq{}  d)  and  ((b  -  a)  =  (d  -  c)))

Date html generated: 2016_05_13-PM-03_31_28
Last ObjectModification: 2015_12_26-AM-09_45_56

Theory : arithmetic

Home Index