equal
deleted
inserted
replaced
3305 have "C > 0" |
3305 have "C > 0" |
3306 using \<open>0 < B\<close> zna by (simp add: C_def divide_simps add_strict_increasing) |
3306 using \<open>0 < B\<close> zna by (simp add: C_def divide_simps add_strict_increasing) |
3307 have "\<bar>norm (z + C *\<^sub>R (z-a)) - norm (C *\<^sub>R (z-a))\<bar> \<le> norm z" |
3307 have "\<bar>norm (z + C *\<^sub>R (z-a)) - norm (C *\<^sub>R (z-a))\<bar> \<le> norm z" |
3308 by (metis add_diff_cancel norm_triangle_ineq3) |
3308 by (metis add_diff_cancel norm_triangle_ineq3) |
3309 moreover have "norm (C *\<^sub>R (z-a)) > norm z + B" |
3309 moreover have "norm (C *\<^sub>R (z-a)) > norm z + B" |
3310 using zna \<open>B>0\<close> by (simp add: C_def le_max_iff_disj field_simps) |
3310 using zna \<open>B>0\<close> by (simp add: C_def le_max_iff_disj) |
3311 ultimately have C: "norm (z + C *\<^sub>R (z-a)) > B" by linarith |
3311 ultimately have C: "norm (z + C *\<^sub>R (z-a)) > B" by linarith |
3312 { fix u::real |
3312 { fix u::real |
3313 assume u: "0\<le>u" "u\<le>1" and ins: "(1 - u) *\<^sub>R z + u *\<^sub>R (z + C *\<^sub>R (z - a)) \<in> s" |
3313 assume u: "0\<le>u" "u\<le>1" and ins: "(1 - u) *\<^sub>R z + u *\<^sub>R (z + C *\<^sub>R (z - a)) \<in> s" |
3314 then have Cpos: "1 + u * C > 0" |
3314 then have Cpos: "1 + u * C > 0" |
3315 by (meson \<open>0 < C\<close> add_pos_nonneg less_eq_real_def zero_le_mult_iff zero_less_one) |
3315 by (meson \<open>0 < C\<close> add_pos_nonneg less_eq_real_def zero_le_mult_iff zero_less_one) |