proposition: Lemma PI_tg_cv : Un_cv PI_tg 0.
proof: Proof. unfold Un_cv; unfold Rdist; intros. assert (0 < 2 * eps) by lra. assert (H1 := archimed (/ (2 * eps))). assert (0 <= up (/ (2 * eps)))%Z. { apply le_IZR. left; apply Rlt_trans with (/ (2 * eps)). - apply Rinv_0_lt_compat; assumption. - elim H1; intros; assumption. } assert (H3 := IZN (up (/ (2 * eps))) H2). elim H3; intros N H4. assert (0 < N)%nat. { elim H1; intros H5 _. destruct (lt_eq_lt_dec 0 N) as [[| <- ]|H6]. - assumption. - rewrite H4 in H5. simpl in H5. cut (0 < / (2 * eps)); [ intro | apply Rinv_0_lt_compat; assumption ]. elim (Rlt_irrefl _ (Rlt_trans _ _ _ H6 H5)). - elim (Nat.nlt_0_r _ H6). } exists N; intros. assert (0 < n)%nat by (apply Nat.lt_le_trans with N; assumption). unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_right. 2:{ apply Rle_ge; apply PI_tg_pos. } unfold PI_tg; apply Rlt_trans with (/ INR (2 * n)). - apply Rmult_lt_reg_l with (INR (2 * n)). { apply lt_INR_0. auto with zarith. } rewrite Rinv_r. 2:{ replace n with (S (pred n)). - apply not_O_INR; discriminate. - apply Nat.lt_succ_pred with 0%nat. assumption. } apply Rmult_lt_reg_l with (INR (2 * n + 1)). { apply lt_INR_0. replace (2 * n + 1)%nat with (S (2 * n)) by ring; apply Nat.lt_0_succ. } rewrite (Rmult_comm (INR (2 * n + 1))). rewrite Rmult_assoc; rewrite Rinv_l. 2:{ apply not_O_INR; replace (2 * n + 1)%nat with (S (2 * n)); [ discriminate | ring ]. } do 2 rewrite Rmult_1_r; apply lt_INR. replace (2 * n + 1)%nat with (S (2 * n)) by ring; apply Nat.lt_succ_diag_r. - apply Rle_lt_trans with (/ INR (2 * N)). + apply Rinv_le_contravar. * rewrite mult_INR; apply Rmult_lt_0_compat; [ simpl; prove_sup0 | apply lt_INR_0; assumption ]. * apply le_INR. now apply Nat.mul_le_mono_nonneg_l; [ apply Nat.le_0_l | ]. + rewrite mult_INR. apply Rmult_lt_reg_l with (INR N / eps). * apply Rdiv_lt_0_compat with (2 := H). now apply (lt_INR 0). * replace (_ */ _) with (/(2 * eps)). -- replace (_ / _ * _) with (INR N). ++ rewrite INR_IZR_INZ. now rewrite <- H4. ++ field. now apply Rgt_not_eq. -- simpl (INR 2); field; split. ++ now apply Rgt_not_eq, (lt_INR 0). ++ now apply Rgt_not_eq. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra