kill(all)$

math:calculus :Second Fundamental Theorem of Calculus(proof),part 2,version 1.0
peter.vlasschaert@gmail.com,12/08/2019

see:website
math:calculus :First Fundamental Theorem of Calculus(proof),part 1,version 1.0

load : packages

load(lrats)$

How to proof this:  

p1:'integrate(f(t),t,a,b)  = F(b) -F(a);

 Let F be any antiderivative of f on an interval  'l' , that is, `F'`(x) = f(x)  for all x  in 'I '.  
l : a ≤ x ≤ b  ( 'domain')

How to proof this:  

1e)  definition : G(x)
===============

p1a:G(x)='integrate(f(t),t,a,x);

p1b:G(x):='integrate(f(t),t,a,x);

By the First Fundamental Theorem of Calculus, G is an antiderivative of f. 
Since F is also an antiderivative of f, it must be that F and G differ by a constant:

before show : see part 1
===================
F'(x) = f(x)

intermezzo: differential equation, from part 1

p2:'diff(F,x) =f(x);

p2a:ode2(p2,F,x);

end intermezzo

why constant : C
============

reason : for C,intermezzo
reason : differential of C always zero.

How to find  C : ?
=============
answer : x=a

1e) subst : x=a
---------------------

p3:G(x) =F(x) +C;

p3a:lratsubst([x=a],p3);

p3b:solve(p3a,C);

p3c:lratsubst(p3b,p3);

final result
========
answer : x =b

p3d:subst([x=b],p3c);