Nuprl Lemma : easy-member-int_seg

[i,j,a:ℤ].  (j a ∈ {i..j-}) supposing (((i a) ≤ j) and 0 < a)


Definitions occuring in Statement :  int_seg: {i..j-} less_than: a < b uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B member: t ∈ T subtract: m add: m natural_number: $n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q le: A ≤ B cand: c∧ B less_than: a < b squash: T top: Top subtract: m all: x:A. B[x] uiff: uiff(P;Q) nat_plus: + less_than': less_than'(a;b) true: True implies:  Q not: ¬A false: False decidable: Dec(P) or: P ∨ Q
Lemmas referenced :  subtract_wf add-commutes istype-void minus-one-mul istype-le istype-less_than istype-int not-le-2 add_functionality_wrt_le le_reflexive minus-one-mul-top add-associates one-mul add-swap add-mul-special zero-mul zero-add add-zero two-mul mul-distributes-right omega-shadow mul-distributes mul-swap mul-associates le-add-cancel less-iff-le not-lt-2 minus-add decidable__le decidable__lt
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut dependent_set_memberEquality_alt extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_pairFormation productElimination imageElimination sqequalRule because_Cache isect_memberEquality_alt voidElimination productIsType axiomEquality equalityTransitivity equalitySymmetry addEquality isectIsTypeImplies inhabitedIsType natural_numberEquality dependent_functionElimination independent_isectElimination multiplyEquality minusEquality imageMemberEquality baseClosed independent_functionElimination unionElimination

\mforall{}[i,j,a:\mBbbZ{}].    (j  -  a  \mmember{}  \{i..j\msupminus{}\})  supposing  (((i  +  a)  \mleq{}  j)  and  0  <  a)

Date html generated: 2020_05_19-PM-09_35_43
Last ObjectModification: 2019_12_08-PM-06_18_58

Theory : arithmetic

Home Index