Nuprl Lemma : nequal-le-implies

[x,y:ℤ].  ((x 1) ≤ y) supposing ((x ≤ y) and y ≠ x)


Definitions occuring in Statement :  uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B nequal: a ≠ b ∈  add: m natural_number: $n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a le: A ≤ B and: P ∧ Q nequal: a ≠ b ∈  all: x:A. B[x] decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q not: ¬A rev_implies:  Q implies:  Q false: False prop: uiff: uiff(P;Q) subtype_rel: A ⊆B top: Top less_than': less_than'(a;b) true: True subtract: m
Lemmas referenced :  decidable__le false_wf not-le-2 not-equal-2 add_functionality_wrt_le add-swap add-commutes le-add-cancel condition-implies-le add-associates minus-add minus-one-mul minus-one-mul-top zero-add le-add-cancel2 less_than'_wf le_wf nequal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin hypothesis lemma_by_obid dependent_functionElimination addEquality hypothesisEquality natural_numberEquality unionElimination independent_pairFormation lambdaFormation voidElimination independent_functionElimination independent_isectElimination isectElimination sqequalRule applyEquality lambdaEquality isect_memberEquality voidEquality intEquality because_Cache minusEquality independent_pairEquality axiomEquality equalityTransitivity equalitySymmetry

\mforall{}[x,y:\mBbbZ{}].    ((x  +  1)  \mleq{}  y)  supposing  ((x  \mleq{}  y)  and  y  \mneq{}  x)

Date html generated: 2016_05_13-PM-03_31_41
Last ObjectModification: 2015_12_26-AM-09_46_05

Theory : arithmetic

Home Index