Nuprl Lemma : int_iseg_properties

`∀[i,j:ℤ]. ∀[y:{i...j}].  ((i ≤ y) ∧ (y ≤ j))`

Proof

Definitions occuring in Statement :  int_iseg: `{i...j}` uall: `∀[x:A]. B[x]` le: `A ≤ B` and: `P ∧ Q` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` int_iseg: `{i...j}` prop: `ℙ` implies: `P `` Q` sq_stable: `SqStable(P)` le: `A ≤ B` and: `P ∧ Q` not: `¬A` false: `False` squash: `↓T`
Lemmas referenced :  int_iseg_wf squash_wf less_than'_wf sq_stable__le le_wf sq_stable__and
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename lemma_by_obid isectElimination hypothesisEquality hypothesis isect_memberEquality independent_functionElimination lambdaFormation because_Cache sqequalRule lambdaEquality dependent_functionElimination productElimination independent_pairEquality voidElimination axiomEquality imageMemberEquality baseClosed imageElimination equalityTransitivity equalitySymmetry intEquality

Latex:
\mforall{}[i,j:\mBbbZ{}].  \mforall{}[y:\{i...j\}].    ((i  \mleq{}  y)  \mwedge{}  (y  \mleq{}  j))

Date html generated: 2016_05_13-PM-04_02_08
Last ObjectModification: 2016_01_14-PM-07_24_35

Theory : int_1

Home Index