This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )