### Nuprl Lemma : not-le

`∀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]` member: `t ∈ T` decidable: `Dec(P)` or: `P ∨ Q` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` prop: `ℙ` uall: `∀[x:A]. B[x]` not: `¬A` implies: `P `` Q` false: `False` less_than: `a < b` squash: `↓T` le: `A ≤ B` cand: `A c∧ B`
Lemmas referenced :  less_than'_wf less_than_wf le_wf not_wf decidable__lt
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis unionElimination independent_pairFormation isect_memberFormation isectElimination introduction independent_functionElimination voidElimination sqequalRule lambdaEquality intEquality imageElimination productElimination imageMemberEquality baseClosed

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

Date html generated: 2016_05_13-PM-03_29_44
Last ObjectModification: 2016_01_14-PM-06_41_57

Theory : arithmetic

Home Index