### Nuprl Lemma : not-less-implies-equal

`∀x,y:ℤ.  (x = y ∈ ℤ) supposing ((¬x < y) and (¬y < x))`

Proof

Definitions occuring in Statement :  less_than: `a < b` uimplies: `b supposing a` all: `∀x:A. B[x]` not: `¬A` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` not: `¬A` rev_implies: `P `` Q` implies: `P `` Q` false: `False` prop: `ℙ` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` top: `Top` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis unionElimination independent_pairFormation voidElimination productElimination independent_functionElimination independent_isectElimination isectElimination addEquality natural_numberEquality sqequalRule applyEquality lambdaEquality isect_memberEquality voidEquality intEquality because_Cache axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}x,y:\mBbbZ{}.    (x  =  y)  supposing  ((\mneg{}x  <  y)  and  (\mneg{}y  <  x))

Date html generated: 2016_05_13-PM-03_32_27
Last ObjectModification: 2015_12_26-AM-09_45_20

Theory : arithmetic

Home Index