proposition: Theorem Barrow : forall J F (contF : Continuous J F) (pJ:proper J) G0 (derG0 : Derivative J pJ G0 F) a b (H : Continuous_I (Min_leEq_Max a b) F) Ha Hb, let Ha' := Derivative_imp_inc _ _ _ _ derG0 a Ha in let Hb' := Derivative_imp_inc _ _ _ _ derG0 b Hb in Integral H [=] G0 b Hb'[-]G0 a Ha'.
proof: Proof. intros J F contF pJ G0 derG0 a b H1 Ha Hb; intros. pose (x0:=a). pose (Hx0:=Ha). set (G := ( [-S-]contF) x0 Hx0). elim (@FTC2 J F contF x0 Hx0 pJ G0 derG0); intros c Hc. elim Hc; intros H2 H. elim H; clear H Hc; intros H3 H0. set (G0a := G0 a Ha') in *. set (G0b := G0 b Hb') in *. rstepr (G0b[+]c[-] (G0a[+]c)). set (Ga := G a Ha) in *. set (Gb := G b Hb) in *. apply eq_transitive_unfolded with (Gb[-]Ga). unfold Ga, Gb, G in |- *; simpl in |- *. cut (forall x y z : IR, z [=] x[+]y -> y [=] z[-]x). intro H5. apply H5. apply Integral_plus_Integral with (Min3_leEq_Max3 x0 b a). apply included_imp_Continuous with J. auto. apply included3_interval; auto. intros; apply eq_symmetric_unfolded. rstepr (x[+]y[-]x); algebra. cut (forall x y z : IR, x[-]y [=] z -> x [=] y[+]z); intros. fold G in H0. apply cg_minus_wd; unfold Ga, Gb, G0a, G0b in |- *; apply H; auto. simpl in H0. apply eq_transitive_unfolded with ((G{-}G0) b (Hb, Hb')). 2: apply H0 with (Hx := (Hb, Hb')). simpl. apply cg_minus_wd. apply Integral_wd. apply Feq_reflexive. destruct H1 as [H1 _]. apply H1. algebra. auto. auto. change c with ([-C-]c a I). apply eq_transitive_unfolded with ((G{-}G0) a (Ha, Ha')). 2: apply H0 with (Hx := (Ha, Ha')). simpl. apply cg_minus_wd. apply Integral_wd. apply Feq_reflexive. destruct H1 as [H1 _]. intros y Hy. apply H1. apply (compact_wd _ _ (Min_leEq_Max a b) a). apply compact_Min_lft. unfold compact, x0 in Hy. destruct Hy. apply leEq_imp_eq. astepl (Min a a). assumption. apply Min_id. stepr(Max a a). assumption. apply Max_id. algebra. auto. rstepl (y[+] (x[-]y)). algebra. Qed.
imports: CoRN.ftc.MoreIntegrals CoRN.ftc.CalculusTheorems