Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( A e. RR /\ A = 0 ) -> A = 0 ) |
2 |
1
|
fveq2d |
|- ( ( A e. RR /\ A = 0 ) -> ( arctan ` A ) = ( arctan ` 0 ) ) |
3 |
|
atan0 |
|- ( arctan ` 0 ) = 0 |
4 |
|
0re |
|- 0 e. RR |
5 |
3 4
|
eqeltri |
|- ( arctan ` 0 ) e. RR |
6 |
2 5
|
eqeltrdi |
|- ( ( A e. RR /\ A = 0 ) -> ( arctan ` A ) e. RR ) |
7 |
|
atanre |
|- ( A e. RR -> A e. dom arctan ) |
8 |
7
|
adantr |
|- ( ( A e. RR /\ A =/= 0 ) -> A e. dom arctan ) |
9 |
|
atancl |
|- ( A e. dom arctan -> ( arctan ` A ) e. CC ) |
10 |
8 9
|
syl |
|- ( ( A e. RR /\ A =/= 0 ) -> ( arctan ` A ) e. CC ) |
11 |
|
simpl |
|- ( ( A e. RR /\ A =/= 0 ) -> A e. RR ) |
12 |
11
|
recnd |
|- ( ( A e. RR /\ A =/= 0 ) -> A e. CC ) |
13 |
|
rere |
|- ( A e. RR -> ( Re ` A ) = A ) |
14 |
13
|
adantr |
|- ( ( A e. RR /\ A =/= 0 ) -> ( Re ` A ) = A ) |
15 |
|
simpr |
|- ( ( A e. RR /\ A =/= 0 ) -> A =/= 0 ) |
16 |
14 15
|
eqnetrd |
|- ( ( A e. RR /\ A =/= 0 ) -> ( Re ` A ) =/= 0 ) |
17 |
|
atancj |
|- ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( A e. dom arctan /\ ( * ` ( arctan ` A ) ) = ( arctan ` ( * ` A ) ) ) ) |
18 |
12 16 17
|
syl2anc |
|- ( ( A e. RR /\ A =/= 0 ) -> ( A e. dom arctan /\ ( * ` ( arctan ` A ) ) = ( arctan ` ( * ` A ) ) ) ) |
19 |
18
|
simprd |
|- ( ( A e. RR /\ A =/= 0 ) -> ( * ` ( arctan ` A ) ) = ( arctan ` ( * ` A ) ) ) |
20 |
|
cjre |
|- ( A e. RR -> ( * ` A ) = A ) |
21 |
20
|
adantr |
|- ( ( A e. RR /\ A =/= 0 ) -> ( * ` A ) = A ) |
22 |
21
|
fveq2d |
|- ( ( A e. RR /\ A =/= 0 ) -> ( arctan ` ( * ` A ) ) = ( arctan ` A ) ) |
23 |
19 22
|
eqtrd |
|- ( ( A e. RR /\ A =/= 0 ) -> ( * ` ( arctan ` A ) ) = ( arctan ` A ) ) |
24 |
10 23
|
cjrebd |
|- ( ( A e. RR /\ A =/= 0 ) -> ( arctan ` A ) e. RR ) |
25 |
6 24
|
pm2.61dane |
|- ( A e. RR -> ( arctan ` A ) e. RR ) |