Nuprl Lemma : less-iff-positive

`∀[x,y:ℤ].  uiff(x < y;0 < y - x)`

Proof

Definitions occuring in Statement :  less_than: `a < b` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` subtract: `n - m` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` or: `P ∨ Q` all: `∀x:A. B[x]` implies: `P `` Q` subtract: `n - m` top: `Top`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis natural_numberEquality because_Cache intEquality sqequalRule productElimination independent_pairEquality isect_memberEquality independent_isectElimination equalityTransitivity equalitySymmetry minusEquality inlFormation dependent_functionElimination independent_functionElimination voidElimination voidEquality multiplyEquality

Latex:
\mforall{}[x,y:\mBbbZ{}].    uiff(x  <  y;0  <  y  -  x)

Date html generated: 2019_06_20-AM-11_22_32
Last ObjectModification: 2018_08_17-PM-00_02_42

Theory : arithmetic

Home Index