Metamath Proof Explorer


Theorem atanrecl

Description: The arctangent function is real for all real inputs. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion atanrecl
|- ( A e. RR -> ( arctan ` A ) e. RR )

Proof

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 )