equal
deleted
inserted
replaced
2114 by (blast intro: isCont_o2 [OF _ isCont_Arcsin]) |
2114 by (blast intro: isCont_o2 [OF _ isCont_Arcsin]) |
2115 |
2115 |
2116 lemma sin_Arcsin [simp]: "sin(Arcsin z) = z" |
2116 lemma sin_Arcsin [simp]: "sin(Arcsin z) = z" |
2117 proof - |
2117 proof - |
2118 have "\<i>*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \<longleftrightarrow> (\<i>*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0" |
2118 have "\<i>*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \<longleftrightarrow> (\<i>*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0" |
2119 by (simp add: algebra_simps) --\<open>Cancelling a factor of 2\<close> |
2119 by (simp add: algebra_simps) \<comment>\<open>Cancelling a factor of 2\<close> |
2120 moreover have "... \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0" |
2120 moreover have "... \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0" |
2121 by (metis Arcsin_body_lemma distrib_right no_zero_divisors zero_neq_numeral) |
2121 by (metis Arcsin_body_lemma distrib_right no_zero_divisors zero_neq_numeral) |
2122 ultimately show ?thesis |
2122 ultimately show ?thesis |
2123 apply (simp add: sin_exp_eq Arcsin_def Arcsin_body_lemma exp_minus divide_simps) |
2123 apply (simp add: sin_exp_eq Arcsin_def Arcsin_body_lemma exp_minus divide_simps) |
2124 apply (simp add: algebra_simps) |
2124 apply (simp add: algebra_simps) |
2292 by (blast intro: isCont_o2 [OF _ isCont_Arccos]) |
2292 by (blast intro: isCont_o2 [OF _ isCont_Arccos]) |
2293 |
2293 |
2294 lemma cos_Arccos [simp]: "cos(Arccos z) = z" |
2294 lemma cos_Arccos [simp]: "cos(Arccos z) = z" |
2295 proof - |
2295 proof - |
2296 have "z*2 + \<i> * (2 * csqrt (1 - z\<^sup>2)) = 0 \<longleftrightarrow> z*2 + \<i> * csqrt (1 - z\<^sup>2)*2 = 0" |
2296 have "z*2 + \<i> * (2 * csqrt (1 - z\<^sup>2)) = 0 \<longleftrightarrow> z*2 + \<i> * csqrt (1 - z\<^sup>2)*2 = 0" |
2297 by (simp add: algebra_simps) --\<open>Cancelling a factor of 2\<close> |
2297 by (simp add: algebra_simps) \<comment>\<open>Cancelling a factor of 2\<close> |
2298 moreover have "... \<longleftrightarrow> z + \<i> * csqrt (1 - z\<^sup>2) = 0" |
2298 moreover have "... \<longleftrightarrow> z + \<i> * csqrt (1 - z\<^sup>2) = 0" |
2299 by (metis distrib_right mult_eq_0_iff zero_neq_numeral) |
2299 by (metis distrib_right mult_eq_0_iff zero_neq_numeral) |
2300 ultimately show ?thesis |
2300 ultimately show ?thesis |
2301 apply (simp add: cos_exp_eq Arccos_def Arccos_body_lemma exp_minus field_simps) |
2301 apply (simp add: cos_exp_eq Arccos_def Arccos_body_lemma exp_minus field_simps) |
2302 apply (simp add: power2_eq_square [symmetric]) |
2302 apply (simp add: power2_eq_square [symmetric]) |