### Nuprl Lemma : member-int_seg

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

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` less_than: `a < b` uimplies: `b 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: `b 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

Latex:
\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