equal
deleted
inserted
replaced
213 lemma hrabs_hyperpow_two [simp]: "abs(x pow (1 + 1)) = x pow (1 + 1)" |
213 lemma hrabs_hyperpow_two [simp]: "abs(x pow (1 + 1)) = x pow (1 + 1)" |
214 by (simp add: abs_if hyperpow_two_le linorder_not_less) |
214 by (simp add: abs_if hyperpow_two_le linorder_not_less) |
215 |
215 |
216 lemma hyperpow_two_hrabs [simp]: "abs(x) pow (1 + 1) = x pow (1 + 1)" |
216 lemma hyperpow_two_hrabs [simp]: "abs(x) pow (1 + 1) = x pow (1 + 1)" |
217 by (simp add: hyperpow_hrabs) |
217 by (simp add: hyperpow_hrabs) |
|
218 |
|
219 text{*The precondition could be weakened to @{term "0\<le>x"}*} |
|
220 lemma hypreal_mult_less_mono: |
|
221 "[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y" |
|
222 by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) |
218 |
223 |
219 lemma hyperpow_two_gt_one: "1 < r ==> 1 < r pow (1 + 1)" |
224 lemma hyperpow_two_gt_one: "1 < r ==> 1 < r pow (1 + 1)" |
220 apply (auto simp add: hyperpow_two) |
225 apply (auto simp add: hyperpow_two) |
221 apply (rule_tac y = "1*1" in order_le_less_trans) |
226 apply (rule_tac y = "1*1" in order_le_less_trans) |
222 apply (rule_tac [2] hypreal_mult_less_mono, auto) |
227 apply (rule_tac [2] hypreal_mult_less_mono, auto) |