Theorem efiarg

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

	Ref	Expression
Assertion	efiarg	|- ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) = ( A / ( abs ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		logcl	|- ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
2	1	recld	|- ( ( A e. CC /\ A =/= 0 ) -> ( Re ` ( log ` A ) ) e. RR )
3	2	recnd	|- ( ( A e. CC /\ A =/= 0 ) -> ( Re ` ( log ` A ) ) e. CC )
4		efsub	|- ( ( ( log ` A ) e. CC /\ ( Re ` ( log ` A ) ) e. CC ) -> ( exp ` ( ( log ` A ) - ( Re ` ( log ` A ) ) ) ) = ( ( exp ` ( log ` A ) ) / ( exp ` ( Re ` ( log ` A ) ) ) ) )
5	1 3 4	syl2anc	|- ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( ( log ` A ) - ( Re ` ( log ` A ) ) ) ) = ( ( exp ` ( log ` A ) ) / ( exp ` ( Re ` ( log ` A ) ) ) ) )
6		ax-icn	|- _i e. CC
7	1	imcld	|- ( ( A e. CC /\ A =/= 0 ) -> ( Im ` ( log ` A ) ) e. RR )
8	7	recnd	|- ( ( A e. CC /\ A =/= 0 ) -> ( Im ` ( log ` A ) ) e. CC )
9		mulcl	|- ( ( _i e. CC /\ ( Im ` ( log ` A ) ) e. CC ) -> ( _i x. ( Im ` ( log ` A ) ) ) e. CC )
10	6 8 9	sylancr	|- ( ( A e. CC /\ A =/= 0 ) -> ( _i x. ( Im ` ( log ` A ) ) ) e. CC )
11	1	replimd	|- ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) = ( ( Re ` ( log ` A ) ) + ( _i x. ( Im ` ( log ` A ) ) ) ) )
12	3 10 11	mvrladdd	|- ( ( A e. CC /\ A =/= 0 ) -> ( ( log ` A ) - ( Re ` ( log ` A ) ) ) = ( _i x. ( Im ` ( log ` A ) ) ) )
13	12	fveq2d	|- ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( ( log ` A ) - ( Re ` ( log ` A ) ) ) ) = ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) )
14		eflog	|- ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
15		relog	|- ( ( A e. CC /\ A =/= 0 ) -> ( Re ` ( log ` A ) ) = ( log ` ( abs ` A ) ) )
16	15	fveq2d	|- ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( Re ` ( log ` A ) ) ) = ( exp ` ( log ` ( abs ` A ) ) ) )
17		abscl	|- ( A e. CC -> ( abs ` A ) e. RR )
18	17	adantr	|- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR )
19	18	recnd	|- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. CC )
20		absrpcl	|- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )
21	20	rpne0d	|- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) =/= 0 )
22		eflog	|- ( ( ( abs ` A ) e. CC /\ ( abs ` A ) =/= 0 ) -> ( exp ` ( log ` ( abs ` A ) ) ) = ( abs ` A ) )
23	19 21 22	syl2anc	|- ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` ( abs ` A ) ) ) = ( abs ` A ) )
24	16 23	eqtrd	|- ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( Re ` ( log ` A ) ) ) = ( abs ` A ) )
25	14 24	oveq12d	|- ( ( A e. CC /\ A =/= 0 ) -> ( ( exp ` ( log ` A ) ) / ( exp ` ( Re ` ( log ` A ) ) ) ) = ( A / ( abs ` A ) ) )
26	5 13 25	3eqtr3d	|- ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) = ( A / ( abs ` A ) ) )