Theorem atansssdm

Description: The domain of continuity of the arctangent is a subset of the actual domain of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015)

	Ref	Expression
Hypotheses	atansopn.d	|- D = ( CC \ ( -oo (,] 0 ) )
	atansopn.s	|- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }
Assertion	atansssdm	|- S C_ dom arctan

Proof

Step	Hyp	Ref	Expression
1		atansopn.d	|- D = ( CC \ ( -oo (,] 0 ) )
2		atansopn.s	|- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }
3		rabss	|- ( { y e. CC | ( 1 + ( y ^ 2 ) ) e. D } C_ dom arctan <-> A. y e. CC ( ( 1 + ( y ^ 2 ) ) e. D -> y e. dom arctan ) )
4		simpl	|- ( ( y e. CC /\ ( 1 + ( y ^ 2 ) ) e. D ) -> y e. CC )
5	1	logdmn0	|- ( ( 1 + ( y ^ 2 ) ) e. D -> ( 1 + ( y ^ 2 ) ) =/= 0 )
6	5	adantl	|- ( ( y e. CC /\ ( 1 + ( y ^ 2 ) ) e. D ) -> ( 1 + ( y ^ 2 ) ) =/= 0 )
7		atandm4	|- ( y e. dom arctan <-> ( y e. CC /\ ( 1 + ( y ^ 2 ) ) =/= 0 ) )
8	4 6 7	sylanbrc	|- ( ( y e. CC /\ ( 1 + ( y ^ 2 ) ) e. D ) -> y e. dom arctan )
9	8	ex	|- ( y e. CC -> ( ( 1 + ( y ^ 2 ) ) e. D -> y e. dom arctan ) )
10	3 9	mprgbir	|- { y e. CC | ( 1 + ( y ^ 2 ) ) e. D } C_ dom arctan
11	2 10	eqsstri	|- S C_ dom arctan