### Nuprl Lemma : from-upto-member

`∀n,m,k:ℤ.  uiff((k ∈ [n, m));(n ≤ k) ∧ k < m)`

Proof

Definitions occuring in Statement :  from-upto: `[n, m)` l_member: `(x ∈ l)` less_than: `a < b` uiff: `uiff(P;Q)` le: `A ≤ B` all: `∀x:A. B[x]` and: `P ∧ Q` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` le: `A ≤ B` not: `¬A` implies: `P `` Q` false: `False` uall: `∀[x:A]. B[x]` prop: `ℙ` subtype_rel: `A ⊆r B` l_member: `(x ∈ l)` exists: `∃x:A. B[x]` cand: `A c∧ B` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` ifthenelse: `if b then t else f fi ` btrue: `tt` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` bfalse: `ff` nat: `ℕ` int_seg: `{i..j-}` lelt: `i ≤ j < k` ge: `i ≥ j ` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` bool: `𝔹` unit: `Unit` it: `⋅` bnot: `¬bb` assert: `↑b`
Lemmas referenced :  less_than'_wf member-less_than l_member_wf from-upto_wf subtype_rel_list le_wf less_than_wf length-from-upto lt_int_wf assert_wf bnot_wf not_wf bool_cases subtype_base_sq bool_wf bool_subtype_base eqtt_to_assert assert_of_lt_int eqff_to_assert iff_transitivity iff_weakening_uiff assert_of_bnot select-from-upto lelt_wf subtract_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermVar_wf intformeq_wf itermAdd_wf itermConstant_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_wf decidable__lt intformless_wf itermSubtract_wf int_formula_prop_less_lemma int_term_value_subtract_lemma equal_wf bool_cases_sqequal assert-bnot decidable__equal_int length_wf equal-wf-base-T select_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 extract_by_obid isectElimination hypothesis axiomEquality independent_isectElimination intEquality applyEquality setEquality productEquality because_Cache setElimination rename equalityTransitivity equalitySymmetry unionElimination instantiate cumulativity independent_functionElimination impliesFunctionality dependent_set_memberEquality natural_numberEquality dependent_pairFormation int_eqEquality isect_memberEquality voidEquality computeAll equalityElimination promote_hyp

Latex:
\mforall{}n,m,k:\mBbbZ{}.    uiff((k  \mmember{}  [n,  m));(n  \mleq{}  k)  \mwedge{}  k  <  m)

Date html generated: 2017_04_17-AM-07_55_28
Last ObjectModification: 2017_02_27-PM-04_26_57

Theory : list_1

Home Index