Nuprl Lemma : ftc-example2

∀a,b:ℝ.
  (a_∫^-b t^3 * cosine(t) dt
  = ((((b^3 - r(6) * b) * sine(b)) - (a^3 - r(6) * a) * sine(a))
    + ((((r(3) * b^2) - r(6)) * cosine(b)) - ((r(3) * a^2) - r(6)) * cosine(a))))

Proof

Definitions occuring in Statement : integral: a_∫^-b f[x] dx, cosine: cosine(x), sine: sine(x), rnexp: x^k1, rsub: x - y, req: x = y, rmul: a * b, radd: a + b, int-to-real: r(n), real: ℝ, all: ∀x:A. B[x], natural_number: $n
Definitions unfolded in proof : all: ∀x:A. B[x], member: t ∈ T, rfun: I ⟶ℝ, uall: ∀[x:A]. B[x], nat: ℕ, le: A ≤ B, and: P ∧ Q, less_than': less_than'(a;b), false: False, not: ¬A, implies: P ⇒ Q, prop: ℙ, ifun: ifun(f;I), top: Top, real-fun: real-fun(f;a;b), uimplies: b supposing a, uiff: uiff(P;Q), rev_uimplies: rev_uimplies(P;Q), iff: P ⇐⇒ Q, so_lambda: λ₂x.t[x], so_apply: x[s], decidable: Dec(P), or: P ∨ Q, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], subtract: n - m, sq_type: SQType(T), guard: {T}, nat_plus: ℕ⁺, less_than: a < b, squash: ↓T, true: True, bool: 𝔹, unit: Unit, it: ⋅, btrue: tt, ifthenelse: if b then t else f fi , subtype_rel: A ⊆r B, real: ℝ, bfalse: ff, bnot: ¬_bb, assert: ↑b, eq_int: (i =_z j), int-to-real: r(n), rnexp: x^k1, rfun-eq: rfun-eq(I;f;g), r-ap: f(x), req_int_terms: t1 ≡ t2
Lemmas referenced : real_wf, rmul_wf, rnexp_wf, istype-false, istype-le, cosine_wf, i-member_wf, rccint_wf, rmin_wf, rmax_wf, left_endpoint_rccint_lemma, istype-void, right_endpoint_rccint_lemma, req_functionality, rmul_functionality, rnexp_functionality, cosine_functionality, req_weakening, req_wf, ifun_wf, rccint-icompact, rmin-rleq-rmax, integral_wf, rsub_wf, sine_wf, int-to-real_wf, rminus_wf, radd_wf, riiint_wf, true_wf, member_riiint_lemma, subtype_base_sq, int_subtype_base, decidable__equal_int, full-omega-unsat, intformnot_wf, intformeq_wf, itermConstant_wf, itermSubtract_wf, istype-int, int_formula_prop_not_lemma, int_formula_prop_eq_lemma, int_term_value_constant_lemma, int_term_value_subtract_lemma, int_formula_prop_wf, istype-less_than, sine_functionality, eq_int_wf, eqtt_to_assert, assert_of_eq_int, eqff_to_assert, bool_subtype_base, bool_cases_sqequal, bool_wf, assert-bnot, neg_assert_of_eq_int, ftc-total-integral, integration-by-parts, derivative-rnexp, derivative-sine, derivative-const-mul, derivative-minus-minus, derivative-cosine, rnexp_zero_lemma, rminus_functionality, derivative-minus, derivative-const, derivative_functionality, rmul-zero-both, uiff_transitivity, rsub_functionality, req_transitivity, req_inversion, rmul_assoc, rmul-int, rnexp1, rmul-zero, itermMultiply_wf, itermVar_wf, itermMinus_wf, itermAdd_wf, req-iff-rsub-is-0, real_polynomial_null, real_term_value_sub_lemma, real_term_value_mul_lemma, real_term_value_var_lemma, real_term_value_const_lemma, real_term_value_minus_lemma, real_term_value_add_lemma
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, lambdaFormation_alt, inhabitedIsType, hypothesisEquality, universeIsType, cut, introduction, extract_by_obid, hypothesis, dependent_set_memberEquality_alt, sqequalRule, lambdaEquality_alt, sqequalHypSubstitution, isectElimination, thin, natural_numberEquality, independent_pairFormation, setElimination, rename, because_Cache, setIsType, dependent_functionElimination, isect_memberEquality_alt, voidElimination, independent_isectElimination, productElimination, independent_functionElimination, equalityTransitivity, equalitySymmetry, closedConclusion, functionIsType, applyEquality, instantiate, cumulativity, intEquality, unionElimination, approximateComputation, dependent_pairFormation_alt, imageMemberEquality, baseClosed, equalityElimination, equalityIsType4, promote_hyp, equalityIsType1, multiplyEquality, int_eqEquality

Latex:
\mforall{}a,b:\mBbbR{}. (a\_\mint{}\msupminus{}b t\^{}3 * cosine(t) dt = ((((b\^{}3 - r(6) * b) * sine(b)) - (a\^{}3 - r(6) * a) * sine(a)) + ((((r(3) * b\^{}2) - r(6)) * cosine(b)) - ((r(3) * a\^{}2) - r(6)) * cosine(a)))) Date html generated: 2019_10_31-AM-06_17_29 Last ObjectModification: 2018_11_08-PM-05_57_17 Theory : reals_2 Home Index