Nuprl Lemma : not-less-implies-equal

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


Definitions occuring in Statement :  less_than: a < b uimplies: supposing a all: x:A. B[x] not: ¬A int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a member: t ∈ T decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q not: ¬A rev_implies:  Q implies:  Q false: False prop: uiff: uiff(P;Q) uall: [x:A]. B[x] subtype_rel: A ⊆B top: Top le: A ≤ B less_than': less_than'(a;b) true: True
Lemmas referenced :  decidable__int_equal false_wf not-equal-2 not-lt-2 add_functionality_wrt_le add-swap add-commutes le-add-cancel add-associates not_wf less_than_wf
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

\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