proposition: Lemma cos_eq_0_2PI_0 (x:R) : 0 <= x -> x <= 2 * PI -> cos x = 0 -> x = PI / 2 \/ x = 3 * (PI / 2).
proof: Proof. intros Lo Hi Hx. destruct (Rtotal_order x (3 * (PI / 2))) as [LT|[EQ|GT]]. - rewrite cos_sin in Hx. assert (Lo' : 0 <= PI / 2 + x). { apply Rplus_le_le_0_compat. - apply Rlt_le, PI2_RGT_0. - trivial. } assert (Hi' : PI / 2 + x <= 2 * PI). { apply Rlt_le. replace (2 * PI) with (PI / 2 + 3 * (PI / 2)) by field. now apply Rplus_lt_compat_l. } destruct (sin_eq_O_2PI_0 (PI / 2 + x) Lo' Hi' Hx) as [H|[H|H]]. + exfalso. apply (Rplus_le_compat_l (PI/2)) in Lo. rewrite Rplus_0_r, H in Lo. apply (Rlt_irrefl 0 (Rlt_le_trans 0 (PI / 2) 0 PI2_RGT_0 Lo)). + left. apply (Rplus_eq_compat_l (-(PI/2))) in H. ring_simplify in H. rewrite H. field. + right. apply (Rplus_eq_compat_l (-(PI/2))) in H. ring_simplify in H. rewrite H. field. - now right. - exfalso. destruct (cos_eq_0_0 x Hx) as (k,Hk). clear Hx Lo. subst. assert (LT : (k < 2)%Z). { apply lt_IZR. simpl. apply (Rmult_lt_reg_r PI); [apply PI_RGT_0|]. apply Rlt_le_trans with (IZR k * PI + PI/2); trivial. rewrite <- (Rplus_0_r (IZR k * PI)) at 1. apply Rplus_lt_compat_l. apply PI2_RGT_0. } assert (GT' : (1 < k)%Z). { apply lt_IZR. simpl. apply (Rmult_lt_reg_r PI); [apply PI_RGT_0|rewrite Rmult_1_l]. replace (3*(PI/2)) with (PI/2 + PI) in GT by field. rewrite Rplus_comm in GT. now apply Rplus_lt_reg_l in GT. } lia. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Rtrigo_def Rtrigo_alt Cos_rel Cos_plus ZArith_base Zcomplements Lia Lra Ranalysis1 Rsqrt_def PSeries_reg