### Nuprl Lemma : from-upto-member-nat

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

Proof

Definitions occuring in Statement :  from-upto: `[n, m)` l_member: `(x ∈ l)` nat: `ℕ` less_than: `a < b` uiff: `uiff(P;Q)` le: `A ≤ B` all: `∀x:A. B[x]` and: `P ∧ Q`
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]` nat: `ℕ` prop: `ℙ` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` cand: `A c∧ B` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` l_member: `(x ∈ l)` 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` int_seg: `{i..j-}` lelt: `i ≤ j < k` bool: `𝔹` unit: `Unit` it: `⋅` bnot: `¬bb` assert: `↑b` squash: `↓T` sq_stable: `SqStable(P)`
Lemmas referenced :  less_than'_wf member-less_than l_member_wf nat_wf from-upto_wf subtype_rel_list le_wf less_than_wf subtype_rel_sets nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_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 intformeq_wf itermAdd_wf int_formula_prop_eq_lemma int_term_value_add_lemma 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 select_wf sq_stable__and sq_stable__le sq_stable__less_than squash_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 setElimination rename hypothesis axiomEquality equalityTransitivity equalitySymmetry independent_isectElimination applyEquality setEquality intEquality productEquality because_Cache natural_numberEquality unionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidEquality computeAll instantiate cumulativity independent_functionElimination impliesFunctionality dependent_set_memberEquality applyLambdaEquality equalityElimination promote_hyp addEquality imageMemberEquality baseClosed imageElimination

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

Date html generated: 2017_04_17-AM-07_55_39
Last ObjectModification: 2017_02_27-PM-04_28_41

Theory : list_1

Home Index