### Nuprl Lemma : int_seg_equality

`∀[m,n:ℤ]. ∀[x:{m..n-}].  ∀y:ℤ. x = y ∈ {m..n-} supposing x = y ∈ ℤ`

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` uimplies: `b supposing a` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` prop: `ℙ`
Lemmas referenced :  and_wf le_wf less_than_wf equal_wf int_seg_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalHypSubstitution setElimination thin rename dependent_set_memberEquality productElimination hypothesis lemma_by_obid isectElimination hypothesisEquality intEquality sqequalRule lambdaEquality dependent_functionElimination isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry

Latex:
\mforall{}[m,n:\mBbbZ{}].  \mforall{}[x:\{m..n\msupminus{}\}].    \mforall{}y:\mBbbZ{}.  x  =  y  supposing  x  =  y

Date html generated: 2016_05_13-PM-03_32_50
Last ObjectModification: 2015_12_26-AM-09_45_05

Theory : arithmetic

Home Index