Nuprl Lemma : lt_transitivity_2

[i,j,k:ℤ].  (i < k) supposing (j < and (i ≤ j))


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 le: A ≤ B and: P ∧ Q guard: {T} prop:
Lemmas referenced :  less_than_transitivity2 less_than_wf member-less_than le_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 because_Cache equalityTransitivity equalitySymmetry intEquality

\mforall{}[i,j,k:\mBbbZ{}].    (i  <  k)  supposing  (j  <  k  and  (i  \mleq{}  j))

Date html generated: 2016_05_13-PM-03_30_45
Last ObjectModification: 2015_12_26-AM-09_46_28

Theory : arithmetic

Home Index