proposition: Lemma NewtonInt_P5 : forall (f g:R -> R) (l a b:R), Newton_integrable f a b -> Newton_integrable g a b -> Newton_integrable (fun x:R => l * f x + g x) a b.
proof: Proof. unfold Newton_integrable; intros f g l a b X X0; elim X; intros x p; elim X0; intros x0 p0; exists (fun y:R => l * x y + x0 y). elim p; intro; elim p0; intro. - left; unfold antiderivative; unfold antiderivative in H, H0; elim H; clear H; intros; elim H0; clear H0; intros H0 _. split. 2:assumption. intros; elim (H _ H2); elim (H0 _ H2); intros. assert (H5 : derivable_pt (fun y:R => l * x y + x0 y) x1). { reg. } exists H5; symmetry ; reg; rewrite <- H3; rewrite <- H4; reflexivity. - unfold antiderivative in H, H0; elim H; elim H0; intros; elim H4; intro. { elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H5 H2)). } left; rewrite <- H5; unfold antiderivative; split. 2:right;reflexivity. intros; elim H6; intros; assert (H9 : x1 = a). { apply Rle_antisym; assumption. } assert (H10 : a <= x1 <= b). { split; right; [ symmetry ; assumption | rewrite <- H5; assumption ]. } assert (H11 : b <= x1 <= a). { split; right; [ rewrite <- H5; symmetry ; assumption | assumption ]. } assert (H12 : derivable_pt x x1). { unfold derivable_pt; exists (f x1); elim (H3 _ H10); intros; eapply derive_pt_eq_1; symmetry ; apply H12. } assert (H13 : derivable_pt x0 x1). { unfold derivable_pt; exists (g x1); elim (H1 _ H11); intros; eapply derive_pt_eq_1; symmetry ; apply H13. } assert (H14 : derivable_pt (fun y:R => l * x y + x0 y) x1). { reg. } exists H14; symmetry ; reg. assert (H15 : derive_pt x0 x1 H13 = g x1). { elim (H1 _ H11); intros; rewrite H15; apply pr_nu. } assert (H16 : derive_pt x x1 H12 = f x1). { elim (H3 _ H10); intros; rewrite H16; apply pr_nu. } rewrite H15; rewrite H16; ring. - unfold antiderivative in H, H0; elim H; elim H0; intros; elim H4; intro. { elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H5 H2)). } left; rewrite H5; unfold antiderivative; split. 2:{ right;reflexivity. } intros; elim H6; intros; assert (H9 : x1 = a). { apply Rle_antisym; assumption. } assert (H10 : a <= x1 <= b). { split; right; [ symmetry ; assumption | rewrite H5; assumption ]. } assert (H11 : b <= x1 <= a). { split; right; [ rewrite H5; symmetry ; assumption | assumption ]. } assert (H12 : derivable_pt x x1). { unfold derivable_pt; exists (f x1); elim (H3 _ H11); intros; eapply derive_pt_eq_1; symmetry ; apply H12. } assert (H13 : derivable_pt x0 x1). { unfold derivable_pt; exists (g x1); elim (H1 _ H10); intros; eapply derive_pt_eq_1; symmetry ; apply H13. } assert (H14 : derivable_pt (fun y:R => l * x y + x0 y) x1). { reg. } exists H14; symmetry ; reg. assert (H15 : derive_pt x0 x1 H13 = g x1). { elim (H1 _ H10); intros; rewrite H15; apply pr_nu. } assert (H16 : derive_pt x x1 H12 = f x1). { elim (H3 _ H11); intros; rewrite H16; apply pr_nu. } rewrite H15; rewrite H16; ring. - right; unfold antiderivative; unfold antiderivative in H, H0; elim H; clear H; intros; elim H0; clear H0; intros H0 _; split. 2:assumption. intros; elim (H _ H2); elim (H0 _ H2); intros. assert (H5 : derivable_pt (fun y:R => l * x y + x0 y) x1). { reg. } exists H5; symmetry ; reg; rewrite <- H3; rewrite <- H4; reflexivity. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis