equal
deleted
inserted
replaced
129 using False apply (auto simp: le_diff_eq pos_le_divideRI) |
129 using False apply (auto simp: le_diff_eq pos_le_divideRI) |
130 using diff_le_eq pos_le_divideR_eq by force |
130 using diff_le_eq pos_le_divideR_eq by force |
131 show "\<lbrakk>\<not> 0 \<le> m; a \<le> b; x \<in> {m *\<^sub>R b + c..m *\<^sub>R a + c}\<rbrakk> |
131 show "\<lbrakk>\<not> 0 \<le> m; a \<le> b; x \<in> {m *\<^sub>R b + c..m *\<^sub>R a + c}\<rbrakk> |
132 \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x |
132 \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x |
133 apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI) |
133 apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI) |
134 apply (auto simp: diff_le_eq neg_le_divideR_eq) |
134 apply (auto simp add: neg_le_divideR_eq not_le) |
135 using diff_eq_diff_less_eq linordered_field_class.sign_simps(11) minus_diff_eq not_less scaleR_le_cancel_left_neg by fastforce |
135 apply (auto simp: field_simps) |
|
136 apply (metis (no_types, lifting) add_diff_cancel_left' add_le_imp_le_right diff_add_cancel inverse_eq_divide neg_le_divideR_eq neg_le_iff_le scale_minus_right) |
|
137 done |
136 qed |
138 qed |
137 qed |
139 qed |
138 qed |
140 qed |
139 |
141 |
140 subsection \<open>Limit Points\<close> |
142 subsection \<open>Limit Points\<close> |