Nuprl Lemma : add-member-int_seg2

[k,m,n,x:ℤ].  uiff(x k ∈ {m..n-};x ∈ {m k..n k-})


Proof




Definitions occuring in Statement :  int_seg: {i..j-} uiff: uiff(P;Q) uall: [x:A]. B[x] member: t ∈ T subtract: m add: m int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a int_seg: {i..j-} lelt: i ≤ j < k squash: T prop: implies:  Q all: x:A. B[x] sq_stable: SqStable(P) top: Top subtract: m le: A ≤ B subtype_rel: A ⊆B nat_plus: + less_than: a < b less_than': less_than'(a;b) true: True not: ¬A false: False decidable: Dec(P) or: P ∨ Q
Lemmas referenced :  decidable__lt less-iff-le not-lt-2 le-add-cancel-alt mul-commutes mul-swap mul-distributes omega-shadow mul-distributes-right two-mul mul-associates not-le-2 add-zero zero-add zero-mul add-mul-special add-swap one-mul add-associates minus-add minus-one-mul-top le_reflexive add_functionality_wrt_le add-is-int-iff int_subtype_base int_seg_wf equal-wf-base subtract_wf minus-one-mul add-commutes squash_wf member-less_than sq_stable__less_than decidable__le sq_stable_from_decidable sq_stable__and less_than_wf le_wf and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation dependent_set_memberEquality hypothesisEquality sqequalHypSubstitution applyEquality lambdaEquality setElimination thin rename hypothesis sqequalRule imageMemberEquality baseClosed setEquality intEquality lemma_by_obid isectElimination because_Cache imageElimination isect_memberEquality independent_functionElimination dependent_functionElimination equalityTransitivity equalitySymmetry lambdaFormation independent_isectElimination productElimination voidElimination voidEquality axiomEquality baseApply closedConclusion addEquality independent_pairEquality multiplyEquality natural_numberEquality minusEquality unionElimination

Latex:
\mforall{}[k,m,n,x:\mBbbZ{}].    uiff(x  +  k  \mmember{}  \{m..n\msupminus{}\};x  \mmember{}  \{m  -  k..n  -  k\msupminus{}\})



Date html generated: 2016_05_13-PM-03_38_58
Last ObjectModification: 2016_01_14-PM-06_39_13

Theory : arithmetic


Home Index