proposition: Lemma FPowerSeries'_conv' : fun_series_abs_convergent_IR realline FPowerSeries'.
proof: Proof. clear Hr r Ha. red in |- *; intros. red in |- *; intros. apply fun_ratio_test_conv. intro. unfold FPowerSeries' in |- *; Contin. elim Ha'; intros N HN. elim HN; intros c H H0. clear HN Ha'. elim (Archimedes (Max (Max b x0[-]Min a0 x0) [1][*]Two[*]c)); intros y Hy. exists (Nat.max N y); exists (Half:IR); repeat split. unfold Half in |- *. apply pos_div_two'; apply pos_one. apply less_leEq; apply pos_half. intros x H1; intros. astepl (AbsIR (FPowerSeries' (S n) x (ProjIR1 Hx'))). astepr (Half[*]AbsIR (FPowerSeries' n x (ProjIR1 Hx))). simpl in |- *. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply leEq_wdl with ((AbsIR (a (S n)) [/] _[//]nring_fac_ap_zero _ (S n)) [*] (AbsIR ((x[-]x0) [^]n) [*]AbsIR (x[-]x0))). 2: apply mult_wd. 2: apply eq_transitive_unfolded with (AbsIR (a (S n)) [/] _[//] AbsIR_resp_ap_zero _ (nring_fac_ap_zero _ (S n))). 3: apply eq_symmetric_unfolded; apply AbsIR_division. 2: apply div_wd; algebra. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x; apply nring_nonneg. 2: apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. 2: apply AbsIR_resp_mult. 2: apply mult_wd; apply AbsIR_wd; simpl in |- *; algebra. apply leEq_wdr with ([1] [/]TwoNZ[*](AbsIR (a n) [/] _[//]nring_fac_ap_zero _ n) [*] AbsIR ((x[-]x0) [^]n)). 2: apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. 3: apply mult_assoc_unfolded. 2: apply mult_wdr. 2: eapply eq_transitive_unfolded. 2: apply AbsIR_resp_mult. 2: apply mult_wdl; simpl in |- *; algebra. 2: apply eq_transitive_unfolded with (AbsIR (a n) [/] _[//]AbsIR_resp_ap_zero _ (nring_fac_ap_zero _ n)). 2: apply AbsIR_division. 2: apply div_wd; algebra. 2: apply AbsIR_eq_x; apply nring_nonneg. rstepl (AbsIR (a (S n)) [*]AbsIR (x[-]x0) [*]AbsIR ((x[-]x0) [^]n) [/] _[//] nring_fac_ap_zero _ (S n)). apply shift_div_leEq. apply pos_nring_fac. rstepr ([1] [/]TwoNZ[*] (AbsIR (a n) [*]nring (fact (S n)) [/] _[//]nring_fac_ap_zero _ n) [*] AbsIR ((x[-]x0) [^]n)). apply leEq_wdr with ([1] [/]TwoNZ[*](AbsIR (a n) [*]nring (S n)) [*]AbsIR ((x[-]x0) [^]n)). 2: apply mult_wdl; apply mult_wdr. 2: rstepr (AbsIR (a n) [*](nring (fact (S n)) [/] _[//]nring_fac_ap_zero _ n)). 2: apply mult_wdr. 2: astepr (nring (S n * fact n) [/] _[//]nring_fac_ap_zero IR n). 2: astepr (nring (S n) [*]nring (fact n) [/] _[//]nring_fac_ap_zero IR n); rational. rstepr ([1] [/]TwoNZ[*]nring (S n) [*]AbsIR (a n) [*]AbsIR ((x[-]x0) [^]n)). apply mult_resp_leEq_rht. 2: apply AbsIR_nonneg. apply leEq_transitive with (AbsIR (a (S n)) [*]AbsIR (Max b x0[-]Min a0 x0)). apply mult_resp_leEq_lft. cut (Min a0 x0 [<=] Max b x0). intro H3. apply compact_elements with H3. inversion_clear H1; split. apply leEq_transitive with a0; auto; apply Min_leEq_lft. apply leEq_transitive with b; auto; apply lft_leEq_Max. split. apply Min_leEq_rht. apply rht_leEq_Max. apply leEq_transitive with x0. apply Min_leEq_rht. apply rht_leEq_Max. apply AbsIR_nonneg. apply leEq_transitive with (AbsIR (a (S n)) [*]Max (Max b x0[-]Min a0 x0) [1]). apply mult_resp_leEq_lft. 2: apply AbsIR_nonneg. eapply leEq_wdl. apply lft_leEq_Max. apply eq_symmetric_unfolded; apply AbsIR_eq_x. apply shift_leEq_minus; astepl (Min a0 x0). apply leEq_transitive with x0. apply Min_leEq_rht. apply rht_leEq_Max. apply shift_mult_leEq with (max_one_ap_zero (Max b x0[-]Min a0 x0)). apply pos_max_one. apply leEq_transitive with (c[*]AbsIR (a n)). apply H0. apply Nat.le_trans with (Nat.max N y); auto; apply Nat.le_max_l. apply shift_leEq_div. apply pos_max_one. rstepl (c[*]Max (Max b x0[-]Min a0 x0) [1][*]AbsIR (a n)). apply mult_resp_leEq_rht. 2: apply AbsIR_nonneg. rstepr (nring (R:=IR) (S n) [/]TwoNZ); apply shift_leEq_div. apply pos_two. apply less_leEq; apply leEq_less_trans with (nring (R:=IR) y). eapply leEq_wdl. apply Hy. rational. apply nring_less. red in |- *. cut (y <= n); intros; auto with arith. apply Nat.le_trans with (Nat.max N y); auto with arith. Qed.
imports: CoRN.ftc.FTC