### 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:  Q false: False add: m minus: -n natural_number: \$n int:
Definitions unfolded in proof :  member: t ∈ T uall: [x:A]. B[x] prop: implies:  Q false: False uimplies: supposing a subtract: 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