proposition: Lemma IVT_interv : forall (f : R -> R) (x y : R), (forall a, x <= a <= y -> continuity_pt f a) -> x < y -> f x < 0 -> 0 < f y -> {z : R | x <= z <= y /\ f z = 0}.
proof: Proof. intros. assert (x <= y) by (left;assumption). generalize (dicho_lb_cv x y (fun z:R => cond_positivity (f z)) H3). generalize (dicho_up_cv x y (fun z:R => cond_positivity (f z)) H3). intros X X0. elim X; intros x0 p. elim X0; intros x1 p0. assert (H4 := cv_dicho _ _ _ _ _ H3 p0 p). rewrite H4 in p0. exists x0. split. 1:split. { apply Rle_trans with (dicho_lb x y (fun z:R => cond_positivity (f z)) 0). { simpl in |- *. right; reflexivity. } apply growing_ineq. { apply dicho_lb_growing; assumption. } assumption. } { apply Rle_trans with (dicho_up x y (fun z:R => cond_positivity (f z)) 0). { apply decreasing_ineq. { apply dicho_up_decreasing; assumption. } assumption. } right; reflexivity. } set (Vn := fun n:nat => dicho_lb x y (fun z:R => cond_positivity (f z)) n). set (Wn := fun n:nat => dicho_up x y (fun z:R => cond_positivity (f z)) n). cut ((forall n:nat, f (Vn n) <= 0) -> f x0 <= 0). { cut ((forall n:nat, 0 <= f (Wn n)) -> 0 <= f x0). { intros. cut (forall n:nat, f (Vn n) <= 0). { cut (forall n:nat, 0 <= f (Wn n)). { intros. assert (H9 := H6 H8). assert (H10 := H5 H7). apply Rle_antisym; assumption. } intro. unfold Wn in |- *. cut (forall z:R, cond_positivity z = true <-> 0 <= z). { intro. assert (H8 := dicho_up_car x y (fun z:R => cond_positivity (f z)) n). elim (H7 (f (dicho_up x y (fun z:R => cond_positivity (f z)) n))); intros. apply H9. apply H8. elim (H7 (f y)); intros. apply H12. left; assumption. } intro. unfold cond_positivity in |- *. destruct (Rle_dec 0 z) as [|Hnotle]. { split. { intro; assumption. } intro; reflexivity. } split. { intro feqt;discriminate feqt. } intro. elim Hnotle; assumption. } unfold Vn in |- *. cut (forall z:R, cond_positivity z = false <-> z < 0). { intros. assert (H8 := dicho_lb_car x y (fun z:R => cond_positivity (f z)) n). left. elim (H7 (f (dicho_lb x y (fun z:R => cond_positivity (f z)) n))); intros. apply H9. apply H8. elim (H7 (f x)); intros. apply H12. assumption. } intro. unfold cond_positivity in |- *. destruct (Rle_dec 0 z) as [Hle|]. { split. { intro feqt; discriminate feqt. } intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle H7)). } split. { intro; auto with real. } intro; reflexivity. } cut (Un_cv Wn x0). { intros. assert (Temp : x <= x0 <= y). { apply IVT_interv_prelim1 with (D:=(fun z : R => cond_positivity (f z))) ; assumption. } assert (H7 := continuity_seq f Wn x0 (H x0 Temp) H5). destruct (total_order_T 0 (f x0)) as [[Hlt|<-]|Hgt]. - left; assumption. - right; reflexivity. - unfold Un_cv in H7; unfold Rdist in H7. cut (0 < - f x0). { intro. elim (H7 (- f x0) H8); intros. cut (x2 >= x2)%nat; [ intro | unfold ge in |- *; apply le_n ]. assert (H11 := H9 x2 H10). rewrite Rabs_right in H11. { pattern (- f x0) at 1 in H11; rewrite <- Rplus_0_r in H11. unfold Rminus in H11; rewrite (Rplus_comm (f (Wn x2))) in H11. assert (H12 := Rplus_lt_reg_l _ _ _ H11). assert (H13 := H6 x2). elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H13 H12)). } apply Rle_ge; left; unfold Rminus in |- *; apply Rplus_le_lt_0_compat. { apply H6. } exact H8. } apply Ropp_0_gt_lt_contravar; assumption. } unfold Wn in |- *; assumption. } assert (Un_cv Vn x0) by (unfold Vn; assumption). intros. assert (Temp : x <= x0 <= y). { apply IVT_interv_prelim1 with (D:=(fun z : R => cond_positivity (f z))) ; assumption. } assert (H7 := continuity_seq f Vn x0 (H x0 Temp) H5). destruct (total_order_T 0 (f x0)) as [[Hlt|Heq]|]. - unfold Un_cv in H7; unfold Rdist in H7. elim (H7 (f x0) Hlt); intros. cut (x2 >= x2)%nat; [ intro | unfold ge; apply le_n ]. assert (H10 := H8 x2 H9). rewrite Rabs_left in H10. { pattern (f x0) at 2 in H10; rewrite <- Rplus_0_r in H10. rewrite Ropp_minus_distr in H10. unfold Rminus in H10. assert (H11 := Rplus_lt_reg_l _ _ _ H10). assert (H12 := H6 x2). cut (0 < f (Vn x2)). { intro. elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H13 H12)). } rewrite <- (Ropp_involutive (f (Vn x2))). apply Ropp_0_gt_lt_contravar; assumption. } apply Rplus_lt_reg_l with (f x0 - f (Vn x2)). rewrite Rplus_0_r; replace (f x0 - f (Vn x2) + (f (Vn x2) - f x0)) with 0; [ unfold Rminus in |- *; apply Rplus_lt_le_0_compat | ring ]. { assumption. } apply Ropp_0_ge_le_contravar; apply Rle_ge; apply H6. - right; rewrite <- Heq; reflexivity. - left; assumption. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra