Nuprl Lemma : less_than_functionality

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


Definitions occuring in Statement :  less_than: a < b 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 ≥  prop:
Lemmas referenced :  less_than_transitivity2 less_than_transitivity1 less_than_wf member-less_than le_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 isect_memberEquality equalityTransitivity equalitySymmetry because_Cache intEquality

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

Date html generated: 2016_05_13-PM-03_30_51
Last ObjectModification: 2015_12_26-AM-09_46_30

Theory : arithmetic

Home Index