### Nuprl Lemma : rsum-one

`∀[n,m:ℤ].  (Σ{r1 | n≤k≤m} = if m <z n then r0 else r((m - n) + 1) fi )`

Proof

Definitions occuring in Statement :  rsum: `Σ{x[k] | n≤k≤m}` req: `x = y` int-to-real: `r(n)` ifthenelse: `if b then t else f fi ` lt_int: `i <z j` uall: `∀[x:A]. B[x]` subtract: `n - m` add: `n + m` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` all: `∀x:A. B[x]` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` prop: `ℙ` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  req_witness rsum_wf int-to-real_wf int_seg_wf ifthenelse_wf lt_int_wf real_wf subtract_wf rmul_wf eqtt_to_assert assert_of_lt_int rmul-zero eqff_to_assert equal_wf bool_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot rmul-identity1 req_functionality rsum-constant2 req_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality natural_numberEquality hypothesis addEquality independent_functionElimination intEquality isect_memberEquality because_Cache lambdaFormation unionElimination equalityElimination productElimination independent_isectElimination dependent_pairFormation equalityTransitivity equalitySymmetry promote_hyp dependent_functionElimination instantiate voidElimination

Latex:
\mforall{}[n,m:\mBbbZ{}].    (\mSigma{}\{r1  |  n\mleq{}k\mleq{}m\}  =  if  m  <z  n  then  r0  else  r((m  -  n)  +  1)  fi  )

Date html generated: 2017_10_03-AM-08_59_53
Last ObjectModification: 2017_07_28-AM-07_39_15

Theory : reals

Home Index