### Nuprl Lemma : test-arith

`∀[x,y,z:ℤ].  (((y + 1) ≤ x) `` ((z + 1) ≤ y) `` ((x + (-1)) ≤ z) `` False)`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` le: `A ≤ B` implies: `P `` Q` false: `False` add: `n + m` minus: `-n` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` implies: `P `` Q` false: `False` uimplies: `b supposing a` subtract: `n - m` top: `Top` uiff: `uiff(P;Q)` and: `P ∧ Q` le: `A ≤ B` not: `¬A` less_than': `less_than'(a;b)` true: `True`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut lemma_by_obid sqequalHypSubstitution isectElimination thin addEquality hypothesisEquality minusEquality natural_numberEquality hypothesis intEquality because_Cache isect_memberFormation introduction lambdaFormation sqequalRule lambdaEquality dependent_functionElimination isect_memberEquality voidElimination independent_isectElimination voidEquality multiplyEquality productElimination independent_functionElimination

Latex:
\mforall{}[x,y,z:\mBbbZ{}].    (((y  +  1)  \mleq{}  x)  {}\mRightarrow{}  ((z  +  1)  \mleq{}  y)  {}\mRightarrow{}  ((x  +  (-1))  \mleq{}  z)  {}\mRightarrow{}  False)

Date html generated: 2016_05_13-PM-03_31_52
Last ObjectModification: 2015_12_26-AM-09_45_59

Theory : arithmetic

Home Index