Nuprl Lemma : less_than_functionality

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

Proof

Definitions occuring in Statement :  less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` guard: `{T}` ge: `i ≥ j ` le: `A ≤ B` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` guard: `{T}` le: `A ≤ B` and: `P ∧ Q` ge: `i ≥ j ` 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

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