proposition: Lemma Dirichlet_crit : fun_series_abs_convergent_IR (olor (x0[-]r) (x0[+]r)) FPowerSeries.
proof: Proof. fold r in (value of Hr). red in |- *; intros. red in |- *; intros. apply fun_ratio_test_conv. intro. unfold FPowerSeries in |- *; Contin. elim (ProjT2 (ProjT2 Ha)); intros N HN. exists N. cut {z : IR | [0] [<] z and z [<] r | forall x : IR, Compact Hab x -> AbsIR (x[-]x0) [<=] z}. intro H. elim H; intros z Hz. elim Hz; clear Hz; intros H0z Hzr Hz. clear H. exists (([1][/] r[//]pos_ap_zero _ _ Hr) [*]z). apply shift_mult_less with (pos_ap_zero _ _ H0z). assumption. apply recip_resp_less; assumption. split. apply less_leEq; apply mult_resp_pos. apply recip_resp_pos; assumption. assumption. intros. astepl (AbsIR (FPowerSeries (S n) x (ProjIR1 Hx'))). apply leEq_wdl with (AbsIR (a (S n)) [*]AbsIR (x[-]x0) [*]AbsIR ((x[-]x0) [^]n)). apply leEq_wdr with (([1][/] r[//]pos_ap_zero _ _ Hr) [*]z[*]AbsIR (a n) [*] AbsIR ((x[-]x0) [^]n)). apply mult_resp_leEq_rht. 2: apply AbsIR_nonneg. rstepr (([1][/] r[//]pos_ap_zero _ _ Hr) [*]AbsIR (a n) [*]z). apply mult_resp_leEq_both; try apply AbsIR_nonneg. apply HN; assumption. apply Hz; auto. rstepl (([1][/] r[//]pos_ap_zero _ _ Hr) [*]z[*](AbsIR (a n) [*]AbsIR ((x[-]x0) [^]n))). apply mult_wdr. astepr (AbsIR (FPowerSeries n x (ProjIR1 Hx))). simpl in |- *; apply eq_symmetric_unfolded; apply AbsIR_resp_mult. simpl in |- *. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. apply AbsIR_resp_mult. apply eq_transitive_unfolded with (AbsIR (a (S n)) [*](AbsIR ((x[-]x0) [^]n) [*]AbsIR (x[-]x0))). apply mult_wdr; apply AbsIR_resp_mult. simpl in |- *; rational. clear HN. cut ((forall x : IR, Compact Hab x -> a0 [<=] x) /\ (forall x : IR, Compact Hab x -> x [<=] b)); intros. inversion_clear H. exists (Max (Max (b[-]x0) (x0[-]a0)) (r [/]TwoNZ)). repeat split. eapply less_leEq_trans. 2: apply rht_leEq_Max. apply pos_div_two; auto. repeat apply Max_less. apply shift_minus_less'. elim (Hinc _ (compact_inc_rht _ _ Hab)); auto. apply shift_minus_less; apply shift_less_plus'; elim (Hinc _ (compact_inc_lft _ _ Hab)); auto. apply pos_div_two'; auto. intros. simpl in |- *; unfold ABSIR in |- *; apply Max_leEq. apply leEq_transitive with (b[-]x0). apply minus_resp_leEq; apply H1; auto. eapply leEq_transitive. 2: apply lft_leEq_Max. apply lft_leEq_Max. apply leEq_transitive with (x0[-]a0). rstepr ([--](a0[-]x0)); apply inv_resp_leEq. apply minus_resp_leEq; apply H0; auto. eapply leEq_transitive. 2: apply lft_leEq_Max. apply rht_leEq_Max. split; intros x H; elim H; auto. Qed.
imports: CoRN.ftc.FTC