### Nuprl Lemma : condition-implies-le

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

Proof

Definitions occuring in Statement :  uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` subtract: `n - m` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` rev_uimplies: `rev_uimplies(P;Q)` le: `A ≤ B` guard: `{T}` all: `∀x:A. B[x]` prop: `ℙ` not: `¬A` implies: `P `` 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

Latex:
\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