equal
deleted
inserted
replaced
86 by (simp add: nx ny) |
86 by (simp add: nx ny) |
87 qed |
87 qed |
88 then show ?thesis |
88 then show ?thesis |
89 by (rule_tac x="2*pi" in exI) auto |
89 by (rule_tac x="2*pi" in exI) auto |
90 qed |
90 qed |
91 ultimately obtain z where z: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = z" |
91 ultimately have "(\<lambda>x. g x - h x) constant_on S \<inter> T" |
92 using continuous_discrete_range_constant [OF conST contgh] by blast |
92 using continuous_discrete_range_constant [OF conST contgh] by blast |
|
93 then obtain z where z: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = z" |
|
94 by (auto simp: constant_on_def) |
93 obtain w where "exp(\<i> * of_real(h w)) = exp (\<i> * of_real(z + h w))" |
95 obtain w where "exp(\<i> * of_real(h w)) = exp (\<i> * of_real(z + h w))" |
94 using disc z False |
96 using disc z False |
95 by auto (metis diff_add_cancel g h of_real_add) |
97 by auto (metis diff_add_cancel g h of_real_add) |
96 then have [simp]: "exp (\<i>* of_real z) = 1" |
98 then have [simp]: "exp (\<i>* of_real z) = 1" |
97 by (metis cis_conv_exp cis_mult exp_not_eq_zero mult_cancel_right1) |
99 by (metis cis_conv_exp cis_mult exp_not_eq_zero mult_cancel_right1) |