Nuprl Lemma : less_than_transitivity1

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


Definitions occuring in Statement :  less_than: a < b uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] uiff: uiff(P;Q) and: P ∧ Q or: P ∨ Q prop: squash: T true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q
Lemmas referenced :  le-iff-less-or-equal le_wf member-less_than less_than_wf less_than_transitivity squash_wf true_wf subtype_rel_self iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis productElimination independent_isectElimination unionElimination isectElimination sqequalRule isect_memberEquality because_Cache equalityTransitivity equalitySymmetry intEquality applyEquality lambdaEquality imageElimination natural_numberEquality imageMemberEquality baseClosed instantiate universeEquality independent_functionElimination

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

Date html generated: 2019_06_20-AM-11_22_48
Last ObjectModification: 2018_09_10-PM-01_14_11

Theory : arithmetic

Home Index