Nuprl Lemma : not-ge

x,y:ℤ.  uiff(¬(x ≥ );y > x)


Proof




Definitions occuring in Statement :  uiff: uiff(P;Q) gt: i > j ge: i ≥  all: x:A. B[x] not: ¬A int:
Definitions unfolded in proof :  all: x:A. B[x] gt: i > j ge: i ≥  member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a prop: uall: [x:A]. B[x] implies:  Q iff: ⇐⇒ Q rev_implies:  Q not: ¬A false: False
Lemmas referenced :  less_than_wf iff_weakening_uiff not_wf le_wf not-le uiff_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation intEquality cut independent_pairFormation isect_memberFormation hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality because_Cache addLevel productElimination independent_isectElimination independent_functionElimination dependent_functionElimination cumulativity introduction sqequalRule lambdaEquality voidElimination

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



Date html generated: 2016_05_13-PM-03_29_46
Last ObjectModification: 2015_12_26-AM-09_47_27

Theory : arithmetic


Home Index