src/HOL/Hyperreal/NthRoot.thy
changeset 22443 346729a55460
parent 21865 55cc354fd2d9
child 22630 2a9b64b26612
     1.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Wed Mar 14 21:40:28 2007 +0100
     1.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Wed Mar 14 21:52:26 2007 +0100
     1.3 @@ -386,4 +386,21 @@
     1.4              del: realpow_Suc)
     1.5  done
     1.6  
     1.7 +lemma sqrt_divide_self_eq:
     1.8 +  assumes nneg: "0 \<le> x"
     1.9 +  shows "sqrt x / x = inverse (sqrt x)"
    1.10 +proof cases
    1.11 +  assume "x=0" thus ?thesis by simp
    1.12 +next
    1.13 +  assume nz: "x\<noteq>0" 
    1.14 +  hence pos: "0<x" using nneg by arith
    1.15 +  show ?thesis
    1.16 +  proof (rule right_inverse_eq [THEN iffD1, THEN sym]) 
    1.17 +    show "sqrt x / x \<noteq> 0" by (simp add: divide_inverse nneg nz) 
    1.18 +    show "inverse (sqrt x) / (sqrt x / x) = 1"
    1.19 +      by (simp add: divide_inverse mult_assoc [symmetric] 
    1.20 +                  power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz) 
    1.21 +  qed
    1.22 +qed
    1.23 +
    1.24  end