### Nuprl Lemma : not-gt

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

Proof

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

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

Date html generated: 2016_05_13-PM-03_29_47
Last ObjectModification: 2016_01_14-PM-06_41_44

Theory : arithmetic

Home Index