Theorem efiarg

Description: The exponential of the "arg" function Im o. log . (Contributed by Mario Carneiro, 25-Feb-2015)

	Ref	Expression
Assertion	efiarg	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}=\frac{A}{\left|A\right|}$$

Proof

Step	Hyp	Ref	Expression
1		logcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in ℂ$$
2	1	recld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Re \left(\log A\right)\in ℝ$$
3	2	recnd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Re \left(\log A\right)\in ℂ$$
4		efsub	$$⊢\left(\log A\in ℂ\wedge \Re \left(\log A\right)\in ℂ\right)\to {\mathrm{e}}^{\log A-\Re \left(\log A\right)}=\frac{{\mathrm{e}}^{\log A}}{{\mathrm{e}}^{\Re \left(\log A\right)}}$$
5	1 3 4	syl2anc	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\log A-\Re \left(\log A\right)}=\frac{{\mathrm{e}}^{\log A}}{{\mathrm{e}}^{\Re \left(\log A\right)}}$$
6		ax-icn	$$⊢\mathrm{i}\in ℂ$$
7	1	imcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Im \left(\log A\right)\in ℝ$$
8	7	recnd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Im \left(\log A\right)\in ℂ$$
9		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge \Im \left(\log A\right)\in ℂ\right)\to \mathrm{i}\Im \left(\log A\right)\in ℂ$$
10	6 8 9	sylancr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \mathrm{i}\Im \left(\log A\right)\in ℂ$$
11	1	replimd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A=\Re \left(\log A\right)+\mathrm{i}\Im \left(\log A\right)$$
12	3 10 11	mvrladdd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A-\Re \left(\log A\right)=\mathrm{i}\Im \left(\log A\right)$$
13	12	fveq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\log A-\Re \left(\log A\right)}={\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}$$
14		eflog	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\log A}=A$$
15		relog	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Re \left(\log A\right)=\log \left|A\right|$$
16	15	fveq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\Re \left(\log A\right)}={\mathrm{e}}^{\log \left|A\right|}$$
17		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
18	17	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\in ℝ$$
19	18	recnd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\in ℂ$$
20		absrpcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\in {ℝ}^{+}$$
21	20	rpne0d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\ne 0$$
22		eflog	$$⊢\left(\left|A\right|\in ℂ\wedge \left|A\right|\ne 0\right)\to {\mathrm{e}}^{\log \left|A\right|}=\left|A\right|$$
23	19 21 22	syl2anc	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\log \left|A\right|}=\left|A\right|$$
24	16 23	eqtrd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\Re \left(\log A\right)}=\left|A\right|$$
25	14 24	oveq12d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{{\mathrm{e}}^{\log A}}{{\mathrm{e}}^{\Re \left(\log A\right)}}=\frac{A}{\left|A\right|}$$
26	5 13 25	3eqtr3d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}=\frac{A}{\left|A\right|}$$