src/HOL/NthRoot.thy
 changeset 59741 5b762cd73a8e parent 58889 5b7a9633cfa8 child 60141 833adf7db7d8
```     1.1 --- a/src/HOL/NthRoot.thy	Tue Mar 17 17:45:03 2015 +0000
1.2 +++ b/src/HOL/NthRoot.thy	Wed Mar 18 14:13:27 2015 +0000
1.3 @@ -626,19 +626,24 @@
1.5  done
1.6
1.7 +lemma sqrt2_less_2: "sqrt 2 < (2::real)"
1.8 +  by (metis not_less not_less_iff_gr_or_eq numeral_less_iff real_sqrt_four real_sqrt_le_iff semiring_norm(75) semiring_norm(78) semiring_norm(85))
1.9 +
1.10 +
1.11  text{*Needed for the infinitely close relation over the nonstandard
1.12      complex numbers*}
1.13  lemma lemma_sqrt_hcomplex_capprox:
1.14       "[| 0 < u; x < u/2; y < u/2; 0 \<le> x; 0 \<le> y |] ==> sqrt (x\<^sup>2 + y\<^sup>2) < u"
1.15 -apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
1.16 -apply (erule_tac [2] lemma_real_divide_sqrt_less)
1.17 -apply (rule power2_le_imp_le)
1.18 -apply (auto simp add: zero_le_divide_iff power_divide)
1.19 -apply (rule_tac t = "u\<^sup>2" in real_sum_of_halves [THEN subst])
1.21 -apply (auto simp add: four_x_squared intro: power_mono)
1.22 -done
1.23 -
1.24 +  apply (rule real_sqrt_sum_squares_less)
1.25 +  apply (auto simp add: abs_if field_simps)
1.26 +  apply (rule le_less_trans [where y = "x*2"])
1.27 +  using less_eq_real_def sqrt2_less_2 apply force
1.28 +  apply assumption
1.29 +  apply (rule le_less_trans [where y = "y*2"])
1.30 +  using less_eq_real_def sqrt2_less_2 mult_le_cancel_left
1.31 +  apply auto
1.32 +  done
1.33 +
1.34  text "Legacy theorem names:"
1.35  lemmas real_root_pos2 = real_root_power_cancel
1.36  lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le]
```