# HG changeset patch
# User paulson
# Date 1752651624 -3600
# Node ID 42595eaf29da064870f61a50a40698d320ea95a4
# Parent  e70239b753a006b300a342b6bbfe026f35a2d9b9# Parent  253db0f4c540f3f63ea00edf102b4914186c8c8f
merged

diff -r e70239b753a0 -r 42595eaf29da src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jul 15 23:13:12 2025 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Jul 16 08:40:24 2025 +0100
@@ -2033,6 +2033,9 @@
 lemma Arg_eq_pi_iff: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
   using Arg_eq_pi complex_is_Real_iff by blast
 
+lemma Arg_eq_0_iff: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> Re z \<ge> 0"
+  using Arg_eq_0 complex_is_Real_iff by blast
+
 lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
   using Arg_eq_pi_iff Arg_eq_0 by force
 
@@ -2399,10 +2402,17 @@
 
 lemma powr_nat': "(z :: complex) \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> z powr of_nat n = z ^ n"
   by (cases "z = 0") (auto simp: powr_nat)
-    
+
+lemma norm_powr_complex: "norm (x powr y) = norm x powr Re y * exp (-Im y * Arg x)"
+  by (simp add: powr_def Arg_eq_Im_Ln norm_divide exp_diff exp_minus field_simps)
+
 lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
   using Ln_Reals_eq norm_exp_eq_Re by (auto simp: Im_Ln_eq_0 powr_def norm_complex_def)
 
+lemma norm_powr_real_powr:
+  "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
+  by (metis dual_order.order_iff_strict norm_powr_real norm_zero of_real_0 of_real_Re powr_def)
+
 lemma norm_powr_real_powr': "w \<in> \<real> \<Longrightarrow> norm (z powr w) = norm z powr Re w"
   by (auto simp: powr_def Reals_def)
 
@@ -2604,10 +2614,6 @@
   shows "(\<lambda>z. f z / g z) holomorphic_on S"
   by (metis (no_types, lifting) assms division_ring_divide_zero holomorphic_on_divide holomorphic_transform)
 
-lemma norm_powr_real_powr:
-  "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
-  by (metis dual_order.order_iff_strict norm_powr_real norm_zero of_real_0 of_real_Re powr_def)
-
 lemma tendsto_powr_complex:
   fixes f g :: "_ \<Rightarrow> complex"
   assumes a: "a \<notin> \<real>\<^sub>\<le>\<^sub>0"