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 )