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

Metamath Proof Explorer

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