Theorem absefi

Description: The absolute value of the exponential of an imaginary number is one. Equation 48 of Rudin p. 167. (Contributed by Jason Orendorff, 9-Feb-2007)

	Ref	Expression
Assertion	absefi	|- ( A e. RR -> ( abs ` ( exp ` ( _i x. A ) ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		recn	|- ( A e. RR -> A e. CC )
2		efival	|- ( A e. CC -> ( exp ` ( _i x. A ) ) = ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) )
3	1 2	syl	|- ( A e. RR -> ( exp ` ( _i x. A ) ) = ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) )
4	3	fveq2d	|- ( A e. RR -> ( abs ` ( exp ` ( _i x. A ) ) ) = ( abs ` ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ) )
5		recoscl	|- ( A e. RR -> ( cos ` A ) e. RR )
6		resincl	|- ( A e. RR -> ( sin ` A ) e. RR )
7		absreim	|- ( ( ( cos ` A ) e. RR /\ ( sin ` A ) e. RR ) -> ( abs ` ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ) = ( sqrt ` ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) ) )
8	5 6 7	syl2anc	|- ( A e. RR -> ( abs ` ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ) = ( sqrt ` ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) ) )
9	5	resqcld	|- ( A e. RR -> ( ( cos ` A ) ^ 2 ) e. RR )
10	9	recnd	|- ( A e. RR -> ( ( cos ` A ) ^ 2 ) e. CC )
11	6	resqcld	|- ( A e. RR -> ( ( sin ` A ) ^ 2 ) e. RR )
12	11	recnd	|- ( A e. RR -> ( ( sin ` A ) ^ 2 ) e. CC )
13	10 12	addcomd	|- ( A e. RR -> ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) = ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) )
14		sincossq	|- ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
15	1 14	syl	|- ( A e. RR -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
16	13 15	eqtrd	|- ( A e. RR -> ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) = 1 )
17	16	fveq2d	|- ( A e. RR -> ( sqrt ` ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) ) = ( sqrt ` 1 ) )
18		sqrt1	|- ( sqrt ` 1 ) = 1
19	17 18	eqtrdi	|- ( A e. RR -> ( sqrt ` ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) ) = 1 )
20	8 19	eqtrd	|- ( A e. RR -> ( abs ` ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ) = 1 )
21	4 20	eqtrd	|- ( A e. RR -> ( abs ` ( exp ` ( _i x. A ) ) ) = 1 )