Theorem efiargd

Description: The exponential of the "arg" function Im o. log , deduction version. (Contributed by Thierry Arnoux, 5-Nov-2025)

	Ref	Expression
Hypotheses	efiargd.1	$$⊢\phi \to A\in ℂ$$
	efiargd.2	$$⊢\phi \to A\ne 0$$
Assertion	efiargd	$$⊢\phi \to {\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}=\frac{A}{\left|A\right|}$$

Proof

Step	Hyp	Ref	Expression
1		efiargd.1	$$⊢\phi \to A\in ℂ$$
2		efiargd.2	$$⊢\phi \to A\ne 0$$
3		efiarg	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}=\frac{A}{\left|A\right|}$$
4	1 2 3	syl2anc	$$⊢\phi \to {\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}=\frac{A}{\left|A\right|}$$