equal
deleted
inserted
replaced
5632 { fix e::real assume "e>0" |
5632 { fix e::real assume "e>0" |
5633 hence "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (z m) (z n) < e" |
5633 hence "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (z m) (z n) < e" |
5634 proof(cases "d = 0") |
5634 proof(cases "d = 0") |
5635 case True |
5635 case True |
5636 have *: "\<And>x. ((1 - c) * x \<le> 0) = (x \<le> 0)" using `1 - c > 0` |
5636 have *: "\<And>x. ((1 - c) * x \<le> 0) = (x \<le> 0)" using `1 - c > 0` |
5637 by (metis mult_zero_left real_mult_commute real_mult_le_cancel_iff1) |
5637 by (metis mult_zero_left mult_commute real_mult_le_cancel_iff1) |
5638 from True have "\<And>n. z n = z0" using cf_z2[of 0] and c unfolding z_def |
5638 from True have "\<And>n. z n = z0" using cf_z2[of 0] and c unfolding z_def |
5639 by (simp add: *) |
5639 by (simp add: *) |
5640 thus ?thesis using `e>0` by auto |
5640 thus ?thesis using `e>0` by auto |
5641 next |
5641 next |
5642 case False hence "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"] |
5642 case False hence "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"] |