### Nuprl Lemma : Riemann-sum-constant

`∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[c:ℝ]. ∀[k:ℕ+].  (Riemann-sum(λx.c;a;b;k) = (c * (b - a)))`

Proof

Definitions occuring in Statement :  Riemann-sum: `Riemann-sum(f;a;b;k)` rleq: `x ≤ y` rsub: `x - y` req: `x = y` rmul: `a * b` real: `ℝ` nat_plus: `ℕ+` uall: `∀[x:A]. B[x]` set: `{x:A| B[x]} ` lambda: `λx.A[x]`
Definitions unfolded in proof :  squash: `↓T` implies: `P `` Q` sq_stable: `SqStable(P)` uimplies: `b supposing a` and: `P ∧ Q` so_apply: `x[s]` so_lambda: `λ2x.t[x]` top: `Top` all: `∀x:A. B[x]` rfun: `I ⟶ℝ` subtype_rel: `A ⊆r B` prop: `ℙ` member: `t ∈ T` uall: `∀[x:A]. B[x]` nat_plus: `ℕ+` has-value: `(a)↓` Riemann-sum: `Riemann-sum(f;a;b;k)` iff: `P `⇐⇒` Q` has-valueall: `has-valueall(a)` callbyvalueall: callbyvalueall partition-sum: `partition-sum(f;x;p)` default-partition-choice: `default-partition-choice(p)` rev_uimplies: `rev_uimplies(P;Q)` le: `A ≤ B` uiff: `uiff(P;Q)` less_than: `a < b` not: `¬A` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` or: `P ∨ Q` decidable: `Dec(P)` lelt: `i ≤ j < k` guard: `{T}` int_seg: `{i..j-}` cons: `[a / b]` select: `L[n]` rev_implies: `P `` Q` int_upper: `{i...}` true: `True` less_than': `less_than'(a;b)` ge: `i ≥ j ` partition: `partition(I)` nat: `ℕ` full-partition: `full-partition(I;p)` sq_type: `SQType(T)`
Lemmas referenced :  subtype_base_sq int_subtype_base decidable__equal_int select_append_back squash_wf true_wf lelt_wf select-cons-tl rsum-telescopes length_of_cons_lemma right_endpoint_rccint_lemma add_nat_wf append_wf cons_wf nil_wf length_nil non_neg_length length_cons partition_wf length_append subtype_rel_set partitions_wf subtype_rel_list length-append length_of_nil_lemma nat_wf nat_properties intformeq_wf int_formula_prop_eq_lemma add_nat_plus length_wf_nat add_functionality_wrt_eq iff_weakening_equal length-singleton member_wf req_weakening left_endpoint_rccint_lemma req_wf req_functionality rsum_wf subtract_wf length_wf select_wf int_seg_properties nat_plus_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_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_add_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt add-is-int-iff subtract-is-int-iff intformless_wf itermSubtract_wf int_formula_prop_less_lemma int_term_value_subtract_lemma false_wf int_seg_wf rsum_functionality2 rmul-rsub-distrib le_wf full-partition_wf rccint_wf uniform-partition_wf list_wf valueall-type-has-valueall list-valueall-type real-valueall-type evalall-reduce valueall-type-real-list rccint-icompact value-type-has-value set-value-type less_than_wf int-value-type sq_stable__req Riemann-sum_wf rleq_wf top_wf member_rccint_lemma subtype_rel_dep_function real_wf and_wf subtype_rel_self set_wf rmul_wf rsub_wf req_witness nat_plus_wf
Rules used in proof :  imageElimination baseClosed imageMemberEquality independent_functionElimination lambdaFormation because_Cache independent_isectElimination setEquality voidEquality voidElimination isect_memberEquality dependent_functionElimination sqequalRule applyEquality lambdaEquality hypothesis dependent_set_memberEquality hypothesisEquality isectElimination sqequalHypSubstitution lemma_by_obid rename thin setElimination cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution natural_numberEquality intEquality callbyvalueReduce productElimination equalitySymmetry equalityTransitivity equalityEquality closedConclusion baseApply promote_hyp pointwiseFunctionality computeAll independent_pairFormation int_eqEquality dependent_pairFormation unionElimination addEquality substitution universeEquality instantiate

Latex:
\mforall{}[a:\mBbbR{}].  \mforall{}[b:\{b:\mBbbR{}|  a  \mleq{}  b\}  ].  \mforall{}[c:\mBbbR{}].  \mforall{}[k:\mBbbN{}\msupplus{}].    (Riemann-sum(\mlambda{}x.c;a;b;k)  =  (c  *  (b  -  a)))

Date html generated: 2016_05_18-AM-10_39_54
Last ObjectModification: 2016_01_17-AM-00_24_47

Theory : reals

Home Index