fundamental_theorem[T: TYPE+ FROM real]: THEORY
%------------------------------------------------------------------------------
%
%  Theory and proofs taken from Introduction to Analysis (Maxwell Rosenlight)
%
%  Author:  Rick Butler               NASA Langley
%
%  Note: some material moved to theory indefinite_integral on 7/20/07
%
%------------------------------------------------------------------------------

BEGIN

   ASSUMING
      IMPORTING deriv_domain_def[T]

      connected_domain : ASSUMPTION connected?[T]


      not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING

   IMPORTING deriv_domain_def
   deriv_domain: LEMMA deriv_domain?[T]
   IMPORTING integral, derivative_props[T] %, derivatives_more[T]

   a,b,c,x: VAR T
   f,F,G: VAR [T -> real]

%  NOTE: LEMMA "continuous_Integrable?[T]" implicitly used throughout

   fundamental: THEOREM continuous?(f) AND
                        (FORALL x: F(x) = Integral(a,x,f)) 
                   IMPLIES derivable?(F) AND deriv(F) = f

   fundamental2: THEOREM continuous?(f) 
                              IMPLIES (EXISTS F: derivable?(F) AND deriv(F) = f)

   fundamental3: THEOREM derivable?(F) AND deriv(F) = f AND continuous?(f) 
                            IMPLIES Integrable?(a,b,f) AND
                                    Integral(a,b,f) = F(b) - F(a)
                                      
   derivable_Integrable?: COROLLARY derivable?(f)
                                    IMPLIES Integrable?(a,b,f)

   fundamental3b: COROLLARY derivable?(F) AND continuous?(deriv(F))
                            IMPLIES Integrable?(a,b,deriv(F)) AND
                                    Integral(a,b,deriv(F)) = F(b) - F(a)

END fundamental_theorem