Nuprl Lemma : member-int_seg

[i,j,x:ℤ].  (x ∈ {i..j-}) supposing ((i ≤ x) and x < j)


Definitions occuring in Statement :  int_seg: {i..j-} less_than: a < b uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B member: t ∈ T int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q
Lemmas referenced :  istype-le istype-less_than istype-int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut Error :dependent_set_memberEquality_alt,  hypothesisEquality independent_pairFormation hypothesis sqequalRule Error :productIsType,  extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache axiomEquality equalityTransitivity equalitySymmetry Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  Error :inhabitedIsType

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

Date html generated: 2019_06_20-AM-11_23_46
Last ObjectModification: 2018_10_25-PM-00_59_43

Theory : arithmetic

Home Index