Metamath Proof Explorer


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 )