Nuprl Lemma : lt_transitivity_1

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


Proof




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_transitivity1 le_wf member-less_than less_than_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

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



Date html generated: 2016_05_13-PM-03_30_43
Last ObjectModification: 2015_12_26-AM-09_46_33

Theory : arithmetic


Home Index