### Nuprl Lemma : sum-has-value

`∀[n,f:Base].  {(n ∈ ℤ) ∧ (f ∈ ℕn ⟶ ℤ)} supposing (Σ(f[x] | x < n))↓`

Proof

Definitions occuring in Statement :  sum: `Σ(f[x] | x < k)` int_seg: `{i..j-}` has-value: `(a)↓` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` guard: `{T}` so_apply: `x[s]` and: `P ∧ Q` member: `t ∈ T` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` base: `Base`
Definitions unfolded in proof :  prop: `ℙ` cand: `A c∧ B` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` guard: `{T}` has-value: `(a)↓` sum_aux: `sum_aux(k;v;i;x.f[x])` sum: `Σ(f[x] | x < k)` or: `P ∨ Q` decidable: `Dec(P)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` top: `Top` not: `¬A` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` ge: `i ≥ j ` false: `False` implies: `P `` Q` nat: `ℕ` all: `∀x:A. B[x]` lelt: `i ≤ j < k` int_seg: `{i..j-}` less_than: `a < b` less_than': `less_than'(a;b)` true: `True` squash: `↓T` sq_type: `SQType(T)` le: `A ≤ B`
Lemmas referenced :  istype-top istype-void int_subtype_base value-type-has-value int-value-type int_seg_properties nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf istype-le subtract_wf itermSubtract_wf int_term_value_subtract_lemma decidable__equal_int subtype_base_sq intformeq_wf int_formula_prop_eq_lemma decidable__lt intformless_wf int_formula_prop_less_lemma istype-less_than false_wf void_wf int_seg_wf satisfiable-full-omega-tt ge_wf less_than_wf less_than_transitivity1 less_than_irreflexivity le_wf set_subtype_base nat_wf has-value_wf_base base_wf
Rules used in proof :  because_Cache isect_memberEquality hypothesisEquality baseClosed closedConclusion baseApply isectElimination lemma_by_obid equalitySymmetry equalityTransitivity axiomEquality independent_pairEquality thin productElimination sqequalHypSubstitution hypothesis independent_pairFormation cut introduction isect_memberFormation computationStep sqequalTransitivity sqequalReflexivity sqequalRule sqequalSubstitution callbyvalueLess unionElimination applyEquality independent_functionElimination computeAll voidEquality voidElimination dependent_functionElimination intEquality int_eqEquality lambdaEquality dependent_pairFormation independent_isectElimination natural_numberEquality intWeakElimination rename setElimination lambdaFormation instantiate functionExtensionality lessCases Error :isect_memberFormation_alt,  axiomSqEquality Error :inhabitedIsType,  Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  extract_by_obid imageMemberEquality Error :lambdaFormation_alt,  imageElimination callbyvalueCallbyvalue callbyvalueReduce callbyvalueAdd Error :dependent_set_memberEquality_alt,  addEquality approximateComputation Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  Error :universeIsType,  cumulativity Error :productIsType,  dependent_set_memberEquality

Latex:
\mforall{}[n,f:Base].    \{(n  \mmember{}  \mBbbZ{})  \mwedge{}  (f  \mmember{}  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{})\}  supposing  (\mSigma{}(f[x]  |  x  <  n))\mdownarrow{}

Date html generated: 2019_06_20-PM-01_17_53
Last ObjectModification: 2019_03_28-PM-00_07_18

Theory : int_2

Home Index