kill(all)$

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

load : packages

load(lrats);

How to proof this:  

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

definition : Maxima for F(x)

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

Then i) F is differentiable on I  and ii) `F'`(x) = f(x)  for all x  in I

proof :

1e)  step : definition derivative
-----------------------------------------

rhs : use definition : Figure 1, 'p1a'

p2:'diff(F(x),x) =limit((F(x+h)-F(x))/h,h,0);

2e) step : rhs 'p2'
------------------------

a) rule 1 :applied for integration : p2 & figure 2

p2a:-'integrate(f(t),t,a,x) = 'integrate(f(t),t,x,a);

p2b:lhs(p2)=lratsubst([p2a],rhs(p2));

b) rule 2: integration 

p2c:'integrate(f(t),t,g(x),a)+'integrate(f(t),t,a,h(x)) = 'integrate(f(t),t,g(x),h(x)) ;

use : subst , use 'p2b'

p2d:[h(x)=x+h,g(x)=x];

p2e:lratsubst(p2d,p2c);

use : 'p2e' ,rhs of p2b,rule 2

p2f:lhs(p2b) =lratsubst([p2e],rhs(p2b));

rem : analysis 'rhs(p2f)'

p2f1:args(rhs(p2f));

3e) mean value theorema
------------------------------------

p2g:lhs(p2f) =ev(rhs(p2f),nouns);

4e) approximation rhs
-------------------------------

small h:That is, Integrate(f(t),t = x .. x+h)   is approximately   h*f(x)

by definition
==========

p2h1:lhs(p2g) = "F'(x)";

p2h2:integrate(f(t),t,x,x+h) =(x+h-x)*f(x);

we have proof:
===========

'First Fundamental Theorem of Calculus'
===============================

5e) final result
-------------------

p2i:rhs(p2h1) =lratsubst([p2h2],rhs(p2g));

we start from here
==============

p2i1:p1;

 two rules, 'integration'
-------------------------------------

first rule :
------------

p2ir1:p2a;

second rule :
------------------

p2ir2:p2c;