Nuprl Lemma : less_than_transitivity

[x,y,z:ℤ].  (x < z) supposing (y < and x < y)


Definitions occuring in Statement :  less_than: a < b uimplies: supposing a uall: [x:A]. B[x] int:
Definitions unfolded in proof :  prop: uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T cand: c∧ B and: P ∧ Q squash: T less_than: a < b less_than': less_than'(a;b)
Lemmas referenced :  member-less_than less_than_wf
Rules used in proof :  equalitySymmetry equalityTransitivity independent_isectElimination isect_memberEquality isect_memberFormation intEquality because_Cache isectElimination extract_by_obid baseClosed imageMemberEquality sqequalRule hypothesisEquality hypothesis independent_pairFormation thin productElimination cut introduction imageElimination sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution sqequalHypSubstitution Error :lessTransitive

\mforall{}[x,y,z:\mBbbZ{}].    (x  <  z)  supposing  (y  <  z  and  x  <  y)

Date html generated: 2019_06_20-AM-11_22_43
Last ObjectModification: 2018_10_11-PM-03_46_40

Theory : arithmetic

Home Index