Nuprl Lemma : less-iff-le

x,y:ℤ.  uiff(x < y;(1 x) ≤ y)


Proof




Definitions occuring in Statement :  less_than: a < b uiff: uiff(P;Q) le: A ≤ B all: x:A. B[x] add: m natural_number: $n int:
Definitions unfolded in proof :  all: x:A. B[x] uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a member: t ∈ T le: A ≤ B not: ¬A implies:  Q false: False uall: [x:A]. B[x] prop: rev_uimplies: rev_uimplies(P;Q) less_than: a < b squash: T less_than': less_than'(a;b) true: True guard: {T}
Lemmas referenced :  less_than_transitivity1 zero-add le_reflexive add_functionality_wrt_lt le-iff-less-or-equal le_wf less_than_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 addEquality natural_numberEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry intEquality independent_isectElimination lessDiscrete imageMemberEquality baseClosed because_Cache

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



Date html generated: 2016_05_13-PM-03_30_56
Last ObjectModification: 2016_01_14-PM-06_41_18

Theory : arithmetic


Home Index