Theorem efiarg

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

	Ref	Expression
Assertion	efiarg	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		logcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
2	1	recld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
3	2	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
4		efsub	⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( ℜ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐴 ) − ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) / ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) )
5	1 3 4	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( log ‘ 𝐴 ) − ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) / ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) )
6		ax-icn	⊢ i ∈ ℂ
7	1	imcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
8	7	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
9		mulcl	⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ ) → ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℂ )
10	6 8 9	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℂ )
11	1	replimd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) = ( ( ℜ ‘ ( log ‘ 𝐴 ) ) + ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
12	3 10 11	mvrladdd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( log ‘ 𝐴 ) − ( ℜ ‘ ( log ‘ 𝐴 ) ) ) = ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
13	12	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( log ‘ 𝐴 ) − ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) = ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
14		eflog	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
15		relog	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) = ( log ‘ ( abs ‘ 𝐴 ) ) )
16	15	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) = ( exp ‘ ( log ‘ ( abs ‘ 𝐴 ) ) ) )
17		abscl	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
18	17	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
19	18	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
20		absrpcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
21	20	rpne0d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ≠ 0 )
22		eflog	⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℂ ∧ ( abs ‘ 𝐴 ) ≠ 0 ) → ( exp ‘ ( log ‘ ( abs ‘ 𝐴 ) ) ) = ( abs ‘ 𝐴 ) )
23	19 21 22	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ ( abs ‘ 𝐴 ) ) ) = ( abs ‘ 𝐴 ) )
24	16 23	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) = ( abs ‘ 𝐴 ) )
25	14 24	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( exp ‘ ( log ‘ 𝐴 ) ) / ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )
26	5 13 25	3eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )