proposition: Theorem FTC1 : Derivative J pJ G F.
proof: Proof. split; Included. split; Included. intros; apply Derivative_I_char. Included. inversion_clear contF. Included. intros. red in contF. inversion_clear contF. elim (contin_prop _ _ _ _ (X2 _ _ _ X) e X0); intros d H3 H4. exists d. assumption. intros x y X3 X4 Hx Hy Hx' H. simpl in |- *. rename Hab into Hab'. set (Hab := less_leEq _ _ _ Hab') in *. cut (included (Compact (Min_leEq_Max x y)) (Compact Hab)). intro Hinc. cut (Continuous_I (Min_leEq_Max x y) F). 2: apply included_imp_Continuous with J; auto. intro H8. apply leEq_wdl with (AbsIR (Integral H8[-] Integral (Continuous_I_const _ _ (Min_leEq_Max x y) (F x Hx')))). apply leEq_wdl with (AbsIR (Integral (Continuous_I_minus _ _ _ _ _ H8 (Continuous_I_const _ _ _ (F x Hx'))))). eapply leEq_transitive. apply Integral_leEq_norm. apply mult_resp_leEq_rht. 2: apply AbsIR_nonneg. apply leEq_Norm_Funct. intros z Hz Hz1. simpl in |- *. apply leEq_wdl with (AbsIR (F z (X1 z (X z (Hinc z Hz))) [-]F x Hx')). 2: apply AbsIR_wd; algebra. apply H4; auto. eapply leEq_transitive. 2: apply H. eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply Abs_Max. eapply leEq_wdr. 2: apply AbsIR_eq_x; apply shift_leEq_minus. 2: astepl (Min x y); apply Min_leEq_Max. apply compact_elements with (Min_leEq_Max x y); auto. apply compact_Min_lft. apply AbsIR_wd; apply Integral_minus. apply AbsIR_wd; apply cg_minus_wd. rstepl (Integral (prim_lemma _ _ contF x0 Hx0 _ Hx) [+]Integral H8[-] Integral (prim_lemma _ _ contF x0 Hx0 _ Hx)). apply cg_minus_wd. apply eq_symmetric_unfolded; apply Integral_plus_Integral with (Min3_leEq_Max3 x0 y x). apply included_imp_Continuous with J; auto. apply included3_interval; auto. apply Integral_wd. apply Feq_reflexive. apply (included_trans _ (Compact (Min_leEq_Max x0 x)) J); try apply included_interval; auto. apply Integral_const. Included. Included. Qed.
imports: CoRN.ftc.MoreIntegrals CoRN.ftc.CalculusTheorems