src/HOL/Hyperreal/NthRoot.thy
changeset 22961 e499ded5d0fc
parent 22956 617140080e6a
child 22968 7134874437ac
equal deleted inserted replaced
22960:114cf1906681 22961:e499ded5d0fc
   472 apply (auto simp add: mult_ac)
   472 apply (auto simp add: mult_ac)
   473 done
   473 done
   474 
   474 
   475 subsection {* Square Root of Sum of Squares *}
   475 subsection {* Square Root of Sum of Squares *}
   476 
   476 
   477 lemma "(sqrt (x\<twosuperior> + y\<twosuperior>))\<twosuperior> = x\<twosuperior> + y\<twosuperior>"
   477 lemma real_sqrt_mult_self_sum_ge_zero [simp]: "0 \<le> sqrt(x*x + y*y)"
       
   478 by (rule real_sqrt_ge_zero [OF real_mult_self_sum_ge_zero])
       
   479 
       
   480 lemma real_sqrt_sum_squares_ge_zero [simp]: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
   478 by simp
   481 by simp
   479 
       
   480 lemma real_sqrt_mult_self_sum_ge_zero [simp]: "0 \<le> sqrt(x*x + y*y)"
       
   481 by (rule real_sqrt_ge_zero [OF real_mult_self_sum_ge_zero]) 
       
   482 
       
   483 lemma real_sqrt_sum_squares_ge_zero [simp]: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
       
   484 by (auto intro!: real_sqrt_ge_zero)
       
   485 
   482 
   486 lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
   483 lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
   487      "0 \<le> sqrt ((x\<twosuperior> + y\<twosuperior>)*(xa\<twosuperior> + ya\<twosuperior>))"
   484      "0 \<le> sqrt ((x\<twosuperior> + y\<twosuperior>)*(xa\<twosuperior> + ya\<twosuperior>))"
   488 by (auto intro!: real_sqrt_ge_zero simp add: zero_le_mult_iff)
   485 by (auto intro!: real_sqrt_ge_zero simp add: zero_le_mult_iff)
   489 
   486 
   494 lemma real_sqrt_sum_squares_ge1 [simp]: "x \<le> sqrt(x\<twosuperior> + y\<twosuperior>)"
   491 lemma real_sqrt_sum_squares_ge1 [simp]: "x \<le> sqrt(x\<twosuperior> + y\<twosuperior>)"
   495 by (rule power2_le_imp_le, simp_all)
   492 by (rule power2_le_imp_le, simp_all)
   496 
   493 
   497 lemma real_sqrt_sum_squares_ge2 [simp]: "y \<le> sqrt(x\<twosuperior> + y\<twosuperior>)"
   494 lemma real_sqrt_sum_squares_ge2 [simp]: "y \<le> sqrt(x\<twosuperior> + y\<twosuperior>)"
   498 by (rule power2_le_imp_le, simp_all)
   495 by (rule power2_le_imp_le, simp_all)
   499 
       
   500 lemma real_sqrt_sos_less_one_iff: "(sqrt (x\<twosuperior> + y\<twosuperior>) < 1) = (x\<twosuperior> + y\<twosuperior> < 1)"
       
   501 by (rule real_sqrt_lt_1_iff)
       
   502 
       
   503 lemma real_sqrt_sos_eq_one_iff: "(sqrt (x\<twosuperior> + y\<twosuperior>) = 1) = (x\<twosuperior> + y\<twosuperior> = 1)"
       
   504 by (rule real_sqrt_eq_1_iff)
       
   505 
   496 
   506 lemma power2_sum:
   497 lemma power2_sum:
   507   fixes x y :: "'a::{number_ring,recpower}"
   498   fixes x y :: "'a::{number_ring,recpower}"
   508   shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
   499   shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
   509 by (simp add: left_distrib right_distrib power2_eq_square)
   500 by (simp add: left_distrib right_distrib power2_eq_square)