Metamath Proof Explorer

Theorem absefib

Description: A complex number is real iff the exponential of its product with _i has absolute value one. (Contributed by NM, 21-Aug-2008)

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

Proof

Step Hyp Ref Expression
1 ef0 
 |-  ( exp ` 0 ) = 1
2 1 eqeq2i 
 |-  ( ( exp ` -u ( Im ` A ) ) = ( exp ` 0 ) <-> ( exp ` -u ( Im ` A ) ) = 1 )
3 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
4 3 renegcld 
 |-  ( A e. CC -> -u ( Im ` A ) e. RR )
5 0re 
 |-  0 e. RR
6 reef11 
 |-  ( ( -u ( Im ` A ) e. RR /\ 0 e. RR ) -> ( ( exp ` -u ( Im ` A ) ) = ( exp ` 0 ) <-> -u ( Im ` A ) = 0 ) )
7 4 5 6 sylancl 
 |-  ( A e. CC -> ( ( exp ` -u ( Im ` A ) ) = ( exp ` 0 ) <-> -u ( Im ` A ) = 0 ) )
8 2 7 bitr3id 
 |-  ( A e. CC -> ( ( exp ` -u ( Im ` A ) ) = 1 <-> -u ( Im ` A ) = 0 ) )
9 3 recnd 
 |-  ( A e. CC -> ( Im ` A ) e. CC )
10 9 negeq0d 
 |-  ( A e. CC -> ( ( Im ` A ) = 0 <-> -u ( Im ` A ) = 0 ) )
11 8 10 bitr4d 
 |-  ( A e. CC -> ( ( exp ` -u ( Im ` A ) ) = 1 <-> ( Im ` A ) = 0 ) )
12 ax-icn 
 |-  _i e. CC
13 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
14 12 13 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
15 absef 
 |-  ( ( _i x. A ) e. CC -> ( abs ` ( exp ` ( _i x. A ) ) ) = ( exp ` ( Re ` ( _i x. A ) ) ) )
16 14 15 syl 
 |-  ( A e. CC -> ( abs ` ( exp ` ( _i x. A ) ) ) = ( exp ` ( Re ` ( _i x. A ) ) ) )
17 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
18 17 recnd 
 |-  ( A e. CC -> ( Re ` A ) e. CC )
19 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` A ) e. CC ) -> ( _i x. ( Im ` A ) ) e. CC )
20 12 9 19 sylancr 
 |-  ( A e. CC -> ( _i x. ( Im ` A ) ) e. CC )
21 replim 
 |-  ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
22 18 20 21 comraddd 
 |-  ( A e. CC -> A = ( ( _i x. ( Im ` A ) ) + ( Re ` A ) ) )
23 22 oveq2d 
 |-  ( A e. CC -> ( _i x. A ) = ( _i x. ( ( _i x. ( Im ` A ) ) + ( Re ` A ) ) ) )
24 adddi 
 |-  ( ( _i e. CC /\ ( _i x. ( Im ` A ) ) e. CC /\ ( Re ` A ) e. CC ) -> ( _i x. ( ( _i x. ( Im ` A ) ) + ( Re ` A ) ) ) = ( ( _i x. ( _i x. ( Im ` A ) ) ) + ( _i x. ( Re ` A ) ) ) )
25 12 20 18 24 mp3an2i 
 |-  ( A e. CC -> ( _i x. ( ( _i x. ( Im ` A ) ) + ( Re ` A ) ) ) = ( ( _i x. ( _i x. ( Im ` A ) ) ) + ( _i x. ( Re ` A ) ) ) )
26 ixi 
 |-  ( _i x. _i ) = -u 1
27 26 oveq1i 
 |-  ( ( _i x. _i ) x. ( Im ` A ) ) = ( -u 1 x. ( Im ` A ) )
28 mulass 
 |-  ( ( _i e. CC /\ _i e. CC /\ ( Im ` A ) e. CC ) -> ( ( _i x. _i ) x. ( Im ` A ) ) = ( _i x. ( _i x. ( Im ` A ) ) ) )
29 12 12 9 28 mp3an12i 
 |-  ( A e. CC -> ( ( _i x. _i ) x. ( Im ` A ) ) = ( _i x. ( _i x. ( Im ` A ) ) ) )
30 9 mulm1d 
 |-  ( A e. CC -> ( -u 1 x. ( Im ` A ) ) = -u ( Im ` A ) )
31 27 29 30 3eqtr3a 
 |-  ( A e. CC -> ( _i x. ( _i x. ( Im ` A ) ) ) = -u ( Im ` A ) )
32 31 oveq1d 
 |-  ( A e. CC -> ( ( _i x. ( _i x. ( Im ` A ) ) ) + ( _i x. ( Re ` A ) ) ) = ( -u ( Im ` A ) + ( _i x. ( Re ` A ) ) ) )
33 25 32 eqtrd 
 |-  ( A e. CC -> ( _i x. ( ( _i x. ( Im ` A ) ) + ( Re ` A ) ) ) = ( -u ( Im ` A ) + ( _i x. ( Re ` A ) ) ) )
34 23 33 eqtrd 
 |-  ( A e. CC -> ( _i x. A ) = ( -u ( Im ` A ) + ( _i x. ( Re ` A ) ) ) )
35 34 fveq2d 
 |-  ( A e. CC -> ( Re ` ( _i x. A ) ) = ( Re ` ( -u ( Im ` A ) + ( _i x. ( Re ` A ) ) ) ) )
36 4 17 crred 
 |-  ( A e. CC -> ( Re ` ( -u ( Im ` A ) + ( _i x. ( Re ` A ) ) ) ) = -u ( Im ` A ) )
37 35 36 eqtrd 
 |-  ( A e. CC -> ( Re ` ( _i x. A ) ) = -u ( Im ` A ) )
38 37 fveq2d 
 |-  ( A e. CC -> ( exp ` ( Re ` ( _i x. A ) ) ) = ( exp ` -u ( Im ` A ) ) )
39 16 38 eqtrd 
 |-  ( A e. CC -> ( abs ` ( exp ` ( _i x. A ) ) ) = ( exp ` -u ( Im ` A ) ) )
40 39 eqeq1d 
 |-  ( A e. CC -> ( ( abs ` ( exp ` ( _i x. A ) ) ) = 1 <-> ( exp ` -u ( Im ` A ) ) = 1 ) )
41 reim0b 
 |-  ( A e. CC -> ( A e. RR <-> ( Im ` A ) = 0 ) )
42 11 40 41 3bitr4rd 
 |-  ( A e. CC -> ( A e. RR <-> ( abs ` ( exp ` ( _i x. A ) ) ) = 1 ) )