Metamath Proof Explorer

Theorem atandmcj

Description: The arctangent function distributes under conjugation. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion atandmcj 
|- ( A e. dom arctan -> ( * ` A ) e. dom arctan )

Proof

Step Hyp Ref Expression
1 atandm3 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) )
2 1 simplbi 
 |-  ( A e. dom arctan -> A e. CC )
3 2 cjcld 
 |-  ( A e. dom arctan -> ( * ` A ) e. CC )
4 2nn0 
 |-  2 e. NN0
5 cjexp 
 |-  ( ( A e. CC /\ 2 e. NN0 ) -> ( * ` ( A ^ 2 ) ) = ( ( * ` A ) ^ 2 ) )
6 2 4 5 sylancl 
 |-  ( A e. dom arctan -> ( * ` ( A ^ 2 ) ) = ( ( * ` A ) ^ 2 ) )
7 2 sqcld 
 |-  ( A e. dom arctan -> ( A ^ 2 ) e. CC )
8 7 cjcjd 
 |-  ( A e. dom arctan -> ( * ` ( * ` ( A ^ 2 ) ) ) = ( A ^ 2 ) )
9 1 simprbi 
 |-  ( A e. dom arctan -> ( A ^ 2 ) =/= -u 1 )
10 8 9 eqnetrd 
 |-  ( A e. dom arctan -> ( * ` ( * ` ( A ^ 2 ) ) ) =/= -u 1 )
11 fveq2 
 |-  ( ( * ` ( A ^ 2 ) ) = -u 1 -> ( * ` ( * ` ( A ^ 2 ) ) ) = ( * ` -u 1 ) )
12 neg1rr 
 |-  -u 1 e. RR
13 cjre 
 |-  ( -u 1 e. RR -> ( * ` -u 1 ) = -u 1 )
14 12 13 ax-mp 
 |-  ( * ` -u 1 ) = -u 1
15 11 14 eqtrdi 
 |-  ( ( * ` ( A ^ 2 ) ) = -u 1 -> ( * ` ( * ` ( A ^ 2 ) ) ) = -u 1 )
16 15 necon3i 
 |-  ( ( * ` ( * ` ( A ^ 2 ) ) ) =/= -u 1 -> ( * ` ( A ^ 2 ) ) =/= -u 1 )
17 10 16 syl 
 |-  ( A e. dom arctan -> ( * ` ( A ^ 2 ) ) =/= -u 1 )
18 6 17 eqnetrrd 
 |-  ( A e. dom arctan -> ( ( * ` A ) ^ 2 ) =/= -u 1 )
19 atandm3 
 |-  ( ( * ` A ) e. dom arctan <-> ( ( * ` A ) e. CC /\ ( ( * ` A ) ^ 2 ) =/= -u 1 ) )
20 3 18 19 sylanbrc 
 |-  ( A e. dom arctan -> ( * ` A ) e. dom arctan )