Nuprl Lemma : not-lt

x,y:ℤ.  uiff(¬x < y;y ≤ x)


Proof




Definitions occuring in Statement :  less_than: a < b uiff: uiff(P;Q) le: A ≤ B all: x:A. B[x] not: ¬A int:
Definitions unfolded in proof :  all: x:A. B[x] uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a member: t ∈ T le: A ≤ B not: ¬A implies:  Q false: False uall: [x:A]. B[x] prop: less_than: a < b cand: c∧ B squash: T
Lemmas referenced :  le_wf less_than_wf not_wf less_than'_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality lambdaEquality dependent_functionElimination hypothesisEquality voidElimination lemma_by_obid isectElimination hypothesis axiomEquality independent_functionElimination intEquality imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}x,y:\mBbbZ{}.    uiff(\mneg{}x  <  y;y  \mleq{}  x)



Date html generated: 2016_05_13-PM-03_29_42
Last ObjectModification: 2016_01_14-PM-06_41_42

Theory : arithmetic


Home Index