Nuprl Lemma : minus_mono_wrt_lt

[i,j:ℤ].  uiff(i > j;-i < -j)


Proof




Definitions occuring in Statement :  less_than: a < b uiff: uiff(P;Q) uall: [x:A]. B[x] gt: i > j minus: -n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a prop: gt: i > j all: x:A. B[x] subtype_rel: A ⊆B top: Top subtract: m nat_plus: + less_than: a < b squash: T less_than': less_than'(a;b) true: True implies:  Q le: A ≤ B not: ¬A false: False decidable: Dec(P) or: P ∨ Q
Lemmas referenced :  minus-one-mul gt_wf member-less_than less_than_wf less-iff-le add_functionality_wrt_le subtract_wf le_reflexive minus-one-mul-top add-associates one-mul add-swap add-commutes add-mul-special two-mul mul-distributes-right zero-mul zero-add not-lt-2 mul-associates add-zero omega-shadow mul-distributes le-add-cancel decidable__lt
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination minusEquality productElimination independent_pairEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry intEquality dependent_functionElimination addEquality natural_numberEquality multiplyEquality applyEquality lambdaEquality voidElimination voidEquality dependent_set_memberEquality imageMemberEquality baseClosed independent_functionElimination unionElimination

Latex:
\mforall{}[i,j:\mBbbZ{}].    uiff(i  >  j;-i  <  -j)



Date html generated: 2018_05_21-PM-00_02_08
Last ObjectModification: 2018_05_19-AM-07_13_14

Theory : arithmetic


Home Index