Nuprl Lemma : le_functionality

[a,b,c,d:ℤ].  ({a ≤ supposing b ≤ c}) supposing ((c ≤ d) and (b ≥ ))


Definitions occuring in Statement :  uimplies: supposing a uall: [x:A]. B[x] guard: {T} ge: i ≥  le: A ≤ B int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a guard: {T} le: A ≤ B and: P ∧ Q ge: i ≥  not: ¬A implies:  Q false: False prop:
Lemmas referenced :  le_transitivity le_wf less_than'_wf ge_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin hypothesis lemma_by_obid isectElimination hypothesisEquality independent_isectElimination sqequalRule independent_pairEquality lambdaEquality dependent_functionElimination because_Cache axiomEquality isect_memberEquality equalityTransitivity equalitySymmetry intEquality voidElimination

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

Date html generated: 2016_05_13-PM-03_30_49
Last ObjectModification: 2015_12_26-AM-09_46_27

Theory : arithmetic

Home Index