Nuprl Lemma : less_than_transitivity2

[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] 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 less_than_wf member-less_than le_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  <  z  and  (x  \mleq{}  y))

Date html generated: 2019_06_20-AM-11_22_50
Last ObjectModification: 2018_09_10-PM-01_15_08

Theory : arithmetic

Home Index