src/HOL/Hyperreal/NthRoot.thy
changeset 25602 137ebc0603f4
parent 23477 f4b83f03cac9
child 25766 6960410f134d
equal deleted inserted replaced
25601:24567e50ebcc 25602:137ebc0603f4
     5 *)
     5 *)
     6 
     6 
     7 header {* Nth Roots of Real Numbers *}
     7 header {* Nth Roots of Real Numbers *}
     8 
     8 
     9 theory NthRoot
     9 theory NthRoot
    10 imports SEQ Parity Deriv
    10 imports Parity "../Hyperreal/Deriv"
    11 begin
    11 begin
    12 
    12 
    13 subsection {* Existence of Nth Root *}
    13 subsection {* Existence of Nth Root *}
    14 
    14 
    15 text {* Existence follows from the Intermediate Value Theorem *}
    15 text {* Existence follows from the Intermediate Value Theorem *}
    80 done
    80 done
    81 
    81 
    82 lemma real_root_pow_pos2 [simp]: (* TODO: rename *)
    82 lemma real_root_pow_pos2 [simp]: (* TODO: rename *)
    83   "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n x ^ n = x"
    83   "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n x ^ n = x"
    84 by (auto simp add: order_le_less real_root_pow_pos)
    84 by (auto simp add: order_le_less real_root_pow_pos)
    85 
       
    86 lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n"
       
    87 by (cases n, simp_all)
       
    88 
    85 
    89 lemma odd_real_root_pow: "odd n \<Longrightarrow> root n x ^ n = x"
    86 lemma odd_real_root_pow: "odd n \<Longrightarrow> root n x ^ n = x"
    90 apply (rule_tac x=0 and y=x in linorder_le_cases)
    87 apply (rule_tac x=0 and y=x in linorder_le_cases)
    91 apply (erule (1) real_root_pow_pos2 [OF odd_pos])
    88 apply (erule (1) real_root_pow_pos2 [OF odd_pos])
    92 apply (subgoal_tac "root n (- x) ^ n = - x")
    89 apply (subgoal_tac "root n (- x) ^ n = - x")