### Nuprl Lemma : not-lt-2

`∀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: `b supposing a` member: `t ∈ T` le: `A ≤ B` not: `¬A` implies: `P `` Q` false: `False` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` less_than: `a < b` cand: `A c∧ B` squash: `↓T`
Lemmas referenced :  le_wf less_than_irreflexivity less_than_transitivity1 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_isectElimination independent_functionElimination intEquality imageMemberEquality baseClosed

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

Date html generated: 2016_05_13-PM-03_31_01
Last ObjectModification: 2016_01_14-PM-06_41_07

Theory : arithmetic

Home Index