Theorem dvatan 20728

Description: The derivative of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)

Hypotheses

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

Assertion

Ref	Expression
dvatan	|- ( CC _D (arctan |` S ) ) = ( x e. S |-> ( 1 / ( 1 + ( x ^ 2 ) ) ) )

Distinct variable groups:   x, y, D   x, S

Allowed substitution hint:   S( y)

Proof of Theorem dvatan

Step	Hyp	Ref	Expression
1		cnex 9027	. . . . . 6 |- CC e. _V
2	1	prid2 3873	. . . . 5 |- CC e. { RR , CC }
3	2	a1i 11	. . . 4 |- ( T. -> CC e. { RR , CC } )
4		ax-1cn 9004	. . . . . . 7 |- 1 e. CC
5		ax-icn 9005	. . . . . . . 8 |- _i e. CC
6		atansopn.d	. . . . . . . . . . . 12 |- D = ( CC \ ( -oo (,] 0 ) )
7		atansopn.s	. . . . . . . . . . . 12 |- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }
8	6, 7	atansssdm 20726	. . . . . . . . . . 11 |- S C_ dom arctan
9		simpr 448	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> x e. S )
10	8, 9	sseldi 3306	. . . . . . . . . 10 |- ( ( T. /\ x e. S ) -> x e. dom arctan )
11		atandm2 20670	. . . . . . . . . 10 |- ( x e. dom arctan <-> ( x e. CC /\ ( 1 - ( _i x. x ) ) =/= 0 /\ ( 1 + ( _i x. x ) ) =/= 0 ) )
12	10, 11	sylib 189	. . . . . . . . 9 |- ( ( T. /\ x e. S ) -> ( x e. CC /\ ( 1 - ( _i x. x ) ) =/= 0 /\ ( 1 + ( _i x. x ) ) =/= 0 ) )
13	12	simp1d 969	. . . . . . . 8 |- ( ( T. /\ x e. S ) -> x e. CC )
14		mulcl 9030	. . . . . . . 8 |- ( ( _i e. CC /\ x e. CC ) -> ( _i x. x ) e. CC )
15	5, 13, 14	sylancr 645	. . . . . . 7 |- ( ( T. /\ x e. S ) -> ( _i x. x ) e. CC )
16		subcl 9261	. . . . . . 7 |- ( ( 1 e. CC /\ ( _i x. x ) e. CC ) -> ( 1 - ( _i x. x ) ) e. CC )
17	4, 15, 16	sylancr 645	. . . . . 6 |- ( ( T. /\ x e. S ) -> ( 1 - ( _i x. x ) ) e. CC )
18	12	simp2d 970	. . . . . 6 |- ( ( T. /\ x e. S ) -> ( 1 - ( _i x. x ) ) =/= 0 )
19	17, 18	logcld 20421	. . . . 5 |- ( ( T. /\ x e. S ) -> ( log ` ( 1 - ( _i x. x ) ) ) e. CC )
20		addcl 9028	. . . . . . 7 |- ( ( 1 e. CC /\ ( _i x. x ) e. CC ) -> ( 1 + ( _i x. x ) ) e. CC )
21	4, 15, 20	sylancr 645	. . . . . 6 |- ( ( T. /\ x e. S ) -> ( 1 + ( _i x. x ) ) e. CC )
22	12	simp3d 971	. . . . . 6 |- ( ( T. /\ x e. S ) -> ( 1 + ( _i x. x ) ) =/= 0 )
23	21, 22	logcld 20421	. . . . 5 |- ( ( T. /\ x e. S ) -> ( log ` ( 1 + ( _i x. x ) ) ) e. CC )
24	19, 23	subcld 9367	. . . 4 |- ( ( T. /\ x e. S ) -> ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) e. CC )
25		ovex 6065	. . . . 5 |- ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) e. _V
26	25	a1i 11	. . . 4 |- ( ( T. /\ x e. S ) -> ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) e. _V )
27		ovex 6065	. . . . . . 7 |- ( 1 / ( x + _i ) ) e. _V
28	27	a1i 11	. . . . . 6 |- ( ( T. /\ x e. S ) -> ( 1 / ( x + _i ) ) e. _V )
29	6, 7	atans2 20724	. . . . . . . . . 10 |- ( x e. S <-> ( x e. CC /\ ( 1 - ( _i x. x ) ) e. D /\ ( 1 + ( _i x. x ) ) e. D ) )
30	29	simp2bi 973	. . . . . . . . 9 |- ( x e. S -> ( 1 - ( _i x. x ) ) e. D )
31	30	adantl 453	. . . . . . . 8 |- ( ( T. /\ x e. S ) -> ( 1 - ( _i x. x ) ) e. D )
32		negex 9260	. . . . . . . . 9 |- -u _i e. _V
33	32	a1i 11	. . . . . . . 8 |- ( ( T. /\ x e. S ) -> -u _i e. _V )
34	6	logdmss 20486	. . . . . . . . . 10 |- D C_ ( CC \ { 0 } )
35		simpr 448	. . . . . . . . . 10 |- ( ( T. /\ y e. D ) -> y e. D )
36	34, 35	sseldi 3306	. . . . . . . . 9 |- ( ( T. /\ y e. D ) -> y e. ( CC \ { 0 } ) )
37		logf1o 20415	. . . . . . . . . . 11 |- log : ( CC \ { 0 } ) -1-1-onto-> ran log
38		f1of 5633	. . . . . . . . . . 11 |- ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
39	37, 38	ax-mp 8	. . . . . . . . . 10 |- log : ( CC \ { 0 } ) --> ran log
40	39	ffvelrni 5828	. . . . . . . . 9 |- ( y e. ( CC \ { 0 } ) -> ( log ` y ) e. ran log )
41		logrncn 20413	. . . . . . . . 9 |- ( ( log ` y ) e. ran log -> ( log ` y ) e. CC )
42	36, 40, 41	3syl 19	. . . . . . . 8 |- ( ( T. /\ y e. D ) -> ( log ` y ) e. CC )
43		ovex 6065	. . . . . . . . 9 |- ( 1 / y ) e. _V
44	43	a1i 11	. . . . . . . 8 |- ( ( T. /\ y e. D ) -> ( 1 / y ) e. _V )
45	5	a1i 11	. . . . . . . . . . 11 |- ( T. -> _i e. CC )
46	45, 14	sylan 458	. . . . . . . . . 10 |- ( ( T. /\ x e. CC ) -> ( _i x. x ) e. CC )
47	4, 46, 16	sylancr 645	. . . . . . . . 9 |- ( ( T. /\ x e. CC ) -> ( 1 - ( _i x. x ) ) e. CC )
48	32	a1i 11	. . . . . . . . 9 |- ( ( T. /\ x e. CC ) -> -u _i e. _V )
49	4	a1i 11	. . . . . . . . . . 11 |- ( ( T. /\ x e. CC ) -> 1 e. CC )
50		0cn 9040	. . . . . . . . . . . 12 |- 0 e. CC
51	50	a1i 11	. . . . . . . . . . 11 |- ( ( T. /\ x e. CC ) -> 0 e. CC )
52	4	a1i 11	. . . . . . . . . . . 12 |- ( T. -> 1 e. CC )
53	3, 52	dvmptc 19797	. . . . . . . . . . 11 |- ( T. -> ( CC _D ( x e. CC |-> 1 ) ) = ( x e. CC |-> 0 ) )
54	5	a1i 11	. . . . . . . . . . 11 |- ( ( T. /\ x e. CC ) -> _i e. CC )
55		simpr 448	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. CC ) -> x e. CC )
56	3	dvmptid 19796	. . . . . . . . . . . . 13 |- ( T. -> ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 ) )
57	3, 55, 49, 56, 45	dvmptcmul 19803	. . . . . . . . . . . 12 |- ( T. -> ( CC _D ( x e. CC |-> ( _i x. x ) ) ) = ( x e. CC |-> ( _i x. 1 ) ) )
58	5	mulid1i 9048	. . . . . . . . . . . . 13 |- ( _i x. 1 ) = _i
59	58	mpteq2i 4252	. . . . . . . . . . . 12 |- ( x e. CC |-> ( _i x. 1 ) ) = ( x e. CC |-> _i )
60	57, 59	syl6eq 2452	. . . . . . . . . . 11 |- ( T. -> ( CC _D ( x e. CC |-> ( _i x. x ) ) ) = ( x e. CC |-> _i ) )
61	3, 49, 51, 53, 46, 54, 60	dvmptsub 19806	. . . . . . . . . 10 |- ( T. -> ( CC _D ( x e. CC |-> ( 1 - ( _i x. x ) ) ) ) = ( x e. CC |-> ( 0 - _i ) ) )
62		df-neg 9250	. . . . . . . . . . 11 |- -u _i = ( 0 - _i )
63	62	mpteq2i 4252	. . . . . . . . . 10 |- ( x e. CC |-> -u _i ) = ( x e. CC |-> ( 0 - _i ) )
64	61, 63	syl6eqr 2454	. . . . . . . . 9 |- ( T. -> ( CC _D ( x e. CC |-> ( 1 - ( _i x. x ) ) ) ) = ( x e. CC |-> -u _i ) )
65		eqid 2404	. . . . . . . . . . . 12 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
66	65	cnfldtopon 18770	. . . . . . . . . . 11 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
67	6, 7	atansopn 20725	. . . . . . . . . . 11 |- S e. ( TopOpen ` ℂfld )
68		toponss 16949	. . . . . . . . . . 11 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ S e. ( TopOpen ` ℂfld ) ) -> S C_ CC )
69	66, 67, 68	mp2an 654	. . . . . . . . . 10 |- S C_ CC
70	69	a1i 11	. . . . . . . . 9 |- ( T. -> S C_ CC )
71	65	cnfldtop 18771	. . . . . . . . . . 11 |- ( TopOpen ` ℂfld ) e. Top
72	66	toponunii 16952	. . . . . . . . . . . 12 |- CC = U. ( TopOpen ` ℂfld )
73	72	restid 13616	. . . . . . . . . . 11 |- ( ( TopOpen ` ℂfld ) e. Top -> ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld ) )
74	71, 73	ax-mp 8	. . . . . . . . . 10 |- ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld )
75	74	eqcomi 2408	. . . . . . . . 9 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
76	67	a1i 11	. . . . . . . . 9 |- ( T. -> S e. ( TopOpen ` ℂfld ) )
77	3, 47, 48, 64, 70, 75, 65, 76	dvmptres 19802	. . . . . . . 8 |- ( T. -> ( CC _D ( x e. S |-> ( 1 - ( _i x. x ) ) ) ) = ( x e. S |-> -u _i ) )
78		fssres 5569	. . . . . . . . . . . . . 14 |- ( ( log : ( CC \ { 0 } ) --> ran log /\ D C_ ( CC \ { 0 } ) ) -> ( log |` D ) : D --> ran log )
79	39, 34, 78	mp2an 654	. . . . . . . . . . . . 13 |- ( log |` D ) : D --> ran log
80	79	a1i 11	. . . . . . . . . . . 12 |- ( T. -> ( log |` D ) : D --> ran log )
81	80	feqmptd 5738	. . . . . . . . . . 11 |- ( T. -> ( log |` D ) = ( y e. D |-> ( ( log |` D ) ` y ) ) )
82		fvres 5704	. . . . . . . . . . . 12 |- ( y e. D -> ( ( log |` D ) ` y ) = ( log ` y ) )
83	82	mpteq2ia 4251	. . . . . . . . . . 11 |- ( y e. D |-> ( ( log |` D ) ` y ) ) = ( y e. D |-> ( log ` y ) )
84	81, 83	syl6req 2453	. . . . . . . . . 10 |- ( T. -> ( y e. D |-> ( log ` y ) ) = ( log |` D ) )
85	84	oveq2d 6056	. . . . . . . . 9 |- ( T. -> ( CC _D ( y e. D |-> ( log ` y ) ) ) = ( CC _D ( log |` D ) ) )
86	6	dvlog 20495	. . . . . . . . 9 |- ( CC _D ( log |` D ) ) = ( y e. D |-> ( 1 / y ) )
87	85, 86	syl6eq 2452	. . . . . . . 8 |- ( T. -> ( CC _D ( y e. D |-> ( log ` y ) ) ) = ( y e. D |-> ( 1 / y ) ) )
88		fveq2 5687	. . . . . . . 8 |- ( y = ( 1 - ( _i x. x ) ) -> ( log ` y ) = ( log ` ( 1 - ( _i x. x ) ) ) )
89		oveq2 6048	. . . . . . . 8 |- ( y = ( 1 - ( _i x. x ) ) -> ( 1 / y ) = ( 1 / ( 1 - ( _i x. x ) ) ) )
90	3, 3, 31, 33, 42, 44, 77, 87, 88, 89	dvmptco 19811	. . . . . . 7 |- ( T. -> ( CC _D ( x e. S |-> ( log ` ( 1 - ( _i x. x ) ) ) ) ) = ( x e. S |-> ( ( 1 / ( 1 - ( _i x. x ) ) ) x. -u _i ) ) )
91		irec 11435	. . . . . . . . . 10 |- ( 1 / _i ) = -u _i
92	91	oveq2i 6051	. . . . . . . . 9 |- ( ( 1 / ( 1 - ( _i x. x ) ) ) x. ( 1 / _i ) ) = ( ( 1 / ( 1 - ( _i x. x ) ) ) x. -u _i )
93	5	a1i 11	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> _i e. CC )
94		ine0 9425	. . . . . . . . . . . 12 |- _i =/= 0
95	94	a1i 11	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> _i =/= 0 )
96	17, 93, 18, 95	recdiv2d 9764	. . . . . . . . . 10 |- ( ( T. /\ x e. S ) -> ( ( 1 / ( 1 - ( _i x. x ) ) ) / _i ) = ( 1 / ( ( 1 - ( _i x. x ) ) x. _i ) ) )
97	17, 18	reccld 9739	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> ( 1 / ( 1 - ( _i x. x ) ) ) e. CC )
98	97, 93, 95	divrecd 9749	. . . . . . . . . 10 |- ( ( T. /\ x e. S ) -> ( ( 1 / ( 1 - ( _i x. x ) ) ) / _i ) = ( ( 1 / ( 1 - ( _i x. x ) ) ) x. ( 1 / _i ) ) )
99	4	a1i 11	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. S ) -> 1 e. CC )
100	99, 15, 93	subdird 9446	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. S ) -> ( ( 1 - ( _i x. x ) ) x. _i ) = ( ( 1 x. _i ) - ( ( _i x. x ) x. _i ) ) )
101	5	mulid2i 9049	. . . . . . . . . . . . . . 15 |- ( 1 x. _i ) = _i
102	101	a1i 11	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. S ) -> ( 1 x. _i ) = _i )
103	93, 13, 93	mul32d 9232	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. S ) -> ( ( _i x. x ) x. _i ) = ( ( _i x. _i ) x. x ) )
104		ixi 9607	. . . . . . . . . . . . . . . . 17 |- ( _i x. _i ) = -u 1
105	104	oveq1i 6050	. . . . . . . . . . . . . . . 16 |- ( ( _i x. _i ) x. x ) = ( -u 1 x. x )
106	13	mulm1d 9441	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. S ) -> ( -u 1 x. x ) = -u x )
107	105, 106	syl5eq 2448	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. S ) -> ( ( _i x. _i ) x. x ) = -u x )
108	103, 107	eqtrd 2436	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. S ) -> ( ( _i x. x ) x. _i ) = -u x )
109	102, 108	oveq12d 6058	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. S ) -> ( ( 1 x. _i ) - ( ( _i x. x ) x. _i ) ) = ( _i - -u x ) )
110		subneg 9306	. . . . . . . . . . . . . 14 |- ( ( _i e. CC /\ x e. CC ) -> ( _i - -u x ) = ( _i + x ) )
111	5, 13, 110	sylancr 645	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. S ) -> ( _i - -u x ) = ( _i + x ) )
112	100, 109, 111	3eqtrd 2440	. . . . . . . . . . . 12 |- ( ( T. /\ x e. S ) -> ( ( 1 - ( _i x. x ) ) x. _i ) = ( _i + x ) )
113		addcom 9208	. . . . . . . . . . . . 13 |- ( ( _i e. CC /\ x e. CC ) -> ( _i + x ) = ( x + _i ) )
114	5, 13, 113	sylancr 645	. . . . . . . . . . . 12 |- ( ( T. /\ x e. S ) -> ( _i + x ) = ( x + _i ) )
115	112, 114	eqtrd 2436	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> ( ( 1 - ( _i x. x ) ) x. _i ) = ( x + _i ) )
116	115	oveq2d 6056	. . . . . . . . . 10 |- ( ( T. /\ x e. S ) -> ( 1 / ( ( 1 - ( _i x. x ) ) x. _i ) ) = ( 1 / ( x + _i ) ) )
117	96, 98, 116	3eqtr3d 2444	. . . . . . . . 9 |- ( ( T. /\ x e. S ) -> ( ( 1 / ( 1 - ( _i x. x ) ) ) x. ( 1 / _i ) ) = ( 1 / ( x + _i ) ) )
118	92, 117	syl5eqr 2450	. . . . . . . 8 |- ( ( T. /\ x e. S ) -> ( ( 1 / ( 1 - ( _i x. x ) ) ) x. -u _i ) = ( 1 / ( x + _i ) ) )
119	118	mpteq2dva 4255	. . . . . . 7 |- ( T. -> ( x e. S |-> ( ( 1 / ( 1 - ( _i x. x ) ) ) x. -u _i ) ) = ( x e. S |-> ( 1 / ( x + _i ) ) ) )
120	90, 119	eqtrd 2436	. . . . . 6 |- ( T. -> ( CC _D ( x e. S |-> ( log ` ( 1 - ( _i x. x ) ) ) ) ) = ( x e. S |-> ( 1 / ( x + _i ) ) ) )
121		ovex 6065	. . . . . . 7 |- ( 1 / ( x - _i ) ) e. _V
122	121	a1i 11	. . . . . 6 |- ( ( T. /\ x e. S ) -> ( 1 / ( x - _i ) ) e. _V )
123	29	simp3bi 974	. . . . . . . . 9 |- ( x e. S -> ( 1 + ( _i x. x ) ) e. D )
124	123	adantl 453	. . . . . . . 8 |- ( ( T. /\ x e. S ) -> ( 1 + ( _i x. x ) ) e. D )
125	4, 46, 20	sylancr 645	. . . . . . . . 9 |- ( ( T. /\ x e. CC ) -> ( 1 + ( _i x. x ) ) e. CC )
126	3, 49, 51, 53, 46, 54, 60	dvmptadd 19799	. . . . . . . . . 10 |- ( T. -> ( CC _D ( x e. CC |-> ( 1 + ( _i x. x ) ) ) ) = ( x e. CC |-> ( 0 + _i ) ) )
127	5	addid2i 9210	. . . . . . . . . . 11 |- ( 0 + _i ) = _i
128	127	mpteq2i 4252	. . . . . . . . . 10 |- ( x e. CC |-> ( 0 + _i ) ) = ( x e. CC |-> _i )
129	126, 128	syl6eq 2452	. . . . . . . . 9 |- ( T. -> ( CC _D ( x e. CC |-> ( 1 + ( _i x. x ) ) ) ) = ( x e. CC |-> _i ) )
130	3, 125, 54, 129, 70, 75, 65, 76	dvmptres 19802	. . . . . . . 8 |- ( T. -> ( CC _D ( x e. S |-> ( 1 + ( _i x. x ) ) ) ) = ( x e. S |-> _i ) )
131		fveq2 5687	. . . . . . . 8 |- ( y = ( 1 + ( _i x. x ) ) -> ( log ` y ) = ( log ` ( 1 + ( _i x. x ) ) ) )
132		oveq2 6048	. . . . . . . 8 |- ( y = ( 1 + ( _i x. x ) ) -> ( 1 / y ) = ( 1 / ( 1 + ( _i x. x ) ) ) )
133	3, 3, 124, 93, 42, 44, 130, 87, 131, 132	dvmptco 19811	. . . . . . 7 |- ( T. -> ( CC _D ( x e. S |-> ( log ` ( 1 + ( _i x. x ) ) ) ) ) = ( x e. S |-> ( ( 1 / ( 1 + ( _i x. x ) ) ) x. _i ) ) )
134	99, 21, 93, 22, 95	divdiv2d 9778	. . . . . . . . 9 |- ( ( T. /\ x e. S ) -> ( 1 / ( ( 1 + ( _i x. x ) ) / _i ) ) = ( ( 1 x. _i ) / ( 1 + ( _i x. x ) ) ) )
135	99, 15, 93, 95	divdird 9784	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> ( ( 1 + ( _i x. x ) ) / _i ) = ( ( 1 / _i ) + ( ( _i x. x ) / _i ) ) )
136	91	a1i 11	. . . . . . . . . . . 12 |- ( ( T. /\ x e. S ) -> ( 1 / _i ) = -u _i )
137	13, 93, 95	divcan3d 9751	. . . . . . . . . . . 12 |- ( ( T. /\ x e. S ) -> ( ( _i x. x ) / _i ) = x )
138	136, 137	oveq12d 6058	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> ( ( 1 / _i ) + ( ( _i x. x ) / _i ) ) = ( -u _i + x ) )
139	5	negcli 9324	. . . . . . . . . . . . 13 |- -u _i e. CC
140		addcom 9208	. . . . . . . . . . . . 13 |- ( ( -u _i e. CC /\ x e. CC ) -> ( -u _i + x ) = ( x + -u _i ) )
141	139, 13, 140	sylancr 645	. . . . . . . . . . . 12 |- ( ( T. /\ x e. S ) -> ( -u _i + x ) = ( x + -u _i ) )
142		negsub 9305	. . . . . . . . . . . . 13 |- ( ( x e. CC /\ _i e. CC ) -> ( x + -u _i ) = ( x - _i ) )
143	13, 5, 142	sylancl 644	. . . . . . . . . . . 12 |- ( ( T. /\ x e. S ) -> ( x + -u _i ) = ( x - _i ) )
144	141, 143	eqtrd 2436	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> ( -u _i + x ) = ( x - _i ) )
145	135, 138, 144	3eqtrd 2440	. . . . . . . . . 10 |- ( ( T. /\ x e. S ) -> ( ( 1 + ( _i x. x ) ) / _i ) = ( x - _i ) )
146	145	oveq2d 6056	. . . . . . . . 9 |- ( ( T. /\ x e. S ) -> ( 1 / ( ( 1 + ( _i x. x ) ) / _i ) ) = ( 1 / ( x - _i ) ) )
147	99, 93, 21, 22	div23d 9783	. . . . . . . . 9 |- ( ( T. /\ x e. S ) -> ( ( 1 x. _i ) / ( 1 + ( _i x. x ) ) ) = ( ( 1 / ( 1 + ( _i x. x ) ) ) x. _i ) )
148	134, 146, 147	3eqtr3rd 2445	. . . . . . . 8 |- ( ( T. /\ x e. S ) -> ( ( 1 / ( 1 + ( _i x. x ) ) ) x. _i ) = ( 1 / ( x - _i ) ) )
149	148	mpteq2dva 4255	. . . . . . 7 |- ( T. -> ( x e. S |-> ( ( 1 / ( 1 + ( _i x. x ) ) ) x. _i ) ) = ( x e. S |-> ( 1 / ( x - _i ) ) ) )
150	133, 149	eqtrd 2436	. . . . . 6 |- ( T. -> ( CC _D ( x e. S |-> ( log ` ( 1 + ( _i x. x ) ) ) ) ) = ( x e. S |-> ( 1 / ( x - _i ) ) ) )
151	3, 19, 28, 120, 23, 122, 150	dvmptsub 19806	. . . . 5 |- ( T. -> ( CC _D ( x e. S |-> ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) = ( x e. S |-> ( ( 1 / ( x + _i ) ) - ( 1 / ( x - _i ) ) ) ) )
152		subcl 9261	. . . . . . . . 9 |- ( ( x e. CC /\ _i e. CC ) -> ( x - _i ) e. CC )
153	13, 5, 152	sylancl 644	. . . . . . . 8 |- ( ( T. /\ x e. S ) -> ( x - _i ) e. CC )
154		addcl 9028	. . . . . . . . 9 |- ( ( x e. CC /\ _i e. CC ) -> ( x + _i ) e. CC )
155	13, 5, 154	sylancl 644	. . . . . . . 8 |- ( ( T. /\ x e. S ) -> ( x + _i ) e. CC )
156	13	sqcld 11476	. . . . . . . . 9 |- ( ( T. /\ x e. S ) -> ( x ^ 2 ) e. CC )
157		addcl 9028	. . . . . . . . 9 |- ( ( 1 e. CC /\ ( x ^ 2 ) e. CC ) -> ( 1 + ( x ^ 2 ) ) e. CC )
158	4, 156, 157	sylancr 645	. . . . . . . 8 |- ( ( T. /\ x e. S ) -> ( 1 + ( x ^ 2 ) ) e. CC )
159		atandm4 20672	. . . . . . . . . 10 |- ( x e. dom arctan <-> ( x e. CC /\ ( 1 + ( x ^ 2 ) ) =/= 0 ) )
160	159	simprbi 451	. . . . . . . . 9 |- ( x e. dom arctan -> ( 1 + ( x ^ 2 ) ) =/= 0 )
161	10, 160	syl 16	. . . . . . . 8 |- ( ( T. /\ x e. S ) -> ( 1 + ( x ^ 2 ) ) =/= 0 )
162	153, 155, 158, 161	divsubdird 9785	. . . . . . 7 |- ( ( T. /\ x e. S ) -> ( ( ( x - _i ) - ( x + _i ) ) / ( 1 + ( x ^ 2 ) ) ) = ( ( ( x - _i ) / ( 1 + ( x ^ 2 ) ) ) - ( ( x + _i ) / ( 1 + ( x ^ 2 ) ) ) ) )
163	143	oveq1d 6055	. . . . . . . . . 10 |- ( ( T. /\ x e. S ) -> ( ( x + -u _i ) - ( x + _i ) ) = ( ( x - _i ) - ( x + _i ) ) )
164	139	a1i 11	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> -u _i e. CC )
165	13, 164, 93	pnpcand 9404	. . . . . . . . . 10 |- ( ( T. /\ x e. S ) -> ( ( x + -u _i ) - ( x + _i ) ) = ( -u _i - _i ) )
166	163, 165	eqtr3d 2438	. . . . . . . . 9 |- ( ( T. /\ x e. S ) -> ( ( x - _i ) - ( x + _i ) ) = ( -u _i - _i ) )
167		2cn 10026	. . . . . . . . . . . 12 |- 2 e. CC
168	167, 5, 94	divreci 9715	. . . . . . . . . . 11 |- ( 2 / _i ) = ( 2 x. ( 1 / _i ) )
169	91	oveq2i 6051	. . . . . . . . . . 11 |- ( 2 x. ( 1 / _i ) ) = ( 2 x. -u _i )
170	168, 169	eqtri 2424	. . . . . . . . . 10 |- ( 2 / _i ) = ( 2 x. -u _i )
171	139	2timesi 10057	. . . . . . . . . 10 |- ( 2 x. -u _i ) = ( -u _i + -u _i )
172	139, 5	negsubi 9334	. . . . . . . . . 10 |- ( -u _i + -u _i ) = ( -u _i - _i )
173	170, 171, 172	3eqtri 2428	. . . . . . . . 9 |- ( 2 / _i ) = ( -u _i - _i )
174	166, 173	syl6eqr 2454	. . . . . . . 8 |- ( ( T. /\ x e. S ) -> ( ( x - _i ) - ( x + _i ) ) = ( 2 / _i ) )
175	174	oveq1d 6055	. . . . . . 7 |- ( ( T. /\ x e. S ) -> ( ( ( x - _i ) - ( x + _i ) ) / ( 1 + ( x ^ 2 ) ) ) = ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) )
176	153	mulid1d 9061	. . . . . . . . . 10 |- ( ( T. /\ x e. S ) -> ( ( x - _i ) x. 1 ) = ( x - _i ) )
177	153, 155	mulcomd 9065	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> ( ( x - _i ) x. ( x + _i ) ) = ( ( x + _i ) x. ( x - _i ) ) )
178		i2 11436	. . . . . . . . . . . . . 14 |- ( _i ^ 2 ) = -u 1
179	178	oveq2i 6051	. . . . . . . . . . . . 13 |- ( ( x ^ 2 ) - ( _i ^ 2 ) ) = ( ( x ^ 2 ) - -u 1 )
180		subneg 9306	. . . . . . . . . . . . . 14 |- ( ( ( x ^ 2 ) e. CC /\ 1 e. CC ) -> ( ( x ^ 2 ) - -u 1 ) = ( ( x ^ 2 ) + 1 ) )
181	156, 4, 180	sylancl 644	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. S ) -> ( ( x ^ 2 ) - -u 1 ) = ( ( x ^ 2 ) + 1 ) )
182	179, 181	syl5eq 2448	. . . . . . . . . . . 12 |- ( ( T. /\ x e. S ) -> ( ( x ^ 2 ) - ( _i ^ 2 ) ) = ( ( x ^ 2 ) + 1 ) )
183		subsq 11443	. . . . . . . . . . . . 13 |- ( ( x e. CC /\ _i e. CC ) -> ( ( x ^ 2 ) - ( _i ^ 2 ) ) = ( ( x + _i ) x. ( x - _i ) ) )
184	13, 5, 183	sylancl 644	. . . . . . . . . . . 12 |- ( ( T. /\ x e. S ) -> ( ( x ^ 2 ) - ( _i ^ 2 ) ) = ( ( x + _i ) x. ( x - _i ) ) )
185		addcom 9208	. . . . . . . . . . . . 13 |- ( ( ( x ^ 2 ) e. CC /\ 1 e. CC ) -> ( ( x ^ 2 ) + 1 ) = ( 1 + ( x ^ 2 ) ) )
186	156, 4, 185	sylancl 644	. . . . . . . . . . . 12 |- ( ( T. /\ x e. S ) -> ( ( x ^ 2 ) + 1 ) = ( 1 + ( x ^ 2 ) ) )
187	182, 184, 186	3eqtr3d 2444	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> ( ( x + _i ) x. ( x - _i ) ) = ( 1 + ( x ^ 2 ) ) )
188	177, 187	eqtrd 2436	. . . . . . . . . 10 |- ( ( T. /\ x e. S ) -> ( ( x - _i ) x. ( x + _i ) ) = ( 1 + ( x ^ 2 ) ) )
189	176, 188	oveq12d 6058	. . . . . . . . 9 |- ( ( T. /\ x e. S ) -> ( ( ( x - _i ) x. 1 ) / ( ( x - _i ) x. ( x + _i ) ) ) = ( ( x - _i ) / ( 1 + ( x ^ 2 ) ) ) )
190		subneg 9306	. . . . . . . . . . . 12 |- ( ( x e. CC /\ _i e. CC ) -> ( x - -u _i ) = ( x + _i ) )
191	13, 5, 190	sylancl 644	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> ( x - -u _i ) = ( x + _i ) )
192		atandm 20669	. . . . . . . . . . . . . 14 |- ( x e. dom arctan <-> ( x e. CC /\ x =/= -u _i /\ x =/= _i ) )
193	10, 192	sylib 189	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. S ) -> ( x e. CC /\ x =/= -u _i /\ x =/= _i ) )
194	193	simp2d 970	. . . . . . . . . . . 12 |- ( ( T. /\ x e. S ) -> x =/= -u _i )
195		subeq0 9283	. . . . . . . . . . . . . 14 |- ( ( x e. CC /\ -u _i e. CC ) -> ( ( x - -u _i ) = 0 <-> x = -u _i ) )
196	195	necon3bid 2602	. . . . . . . . . . . . 13 |- ( ( x e. CC /\ -u _i e. CC ) -> ( ( x - -u _i ) =/= 0 <-> x =/= -u _i ) )
197	13, 139, 196	sylancl 644	. . . . . . . . . . . 12 |- ( ( T. /\ x e. S ) -> ( ( x - -u _i ) =/= 0 <-> x =/= -u _i ) )
198	194, 197	mpbird 224	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> ( x - -u _i ) =/= 0 )
199	191, 198	eqnetrrd 2587	. . . . . . . . . 10 |- ( ( T. /\ x e. S ) -> ( x + _i ) =/= 0 )
200	193	simp3d 971	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> x =/= _i )
201		subeq0 9283	. . . . . . . . . . . . 13 |- ( ( x e. CC /\ _i e. CC ) -> ( ( x - _i ) = 0 <-> x = _i ) )
202	201	necon3bid 2602	. . . . . . . . . . . 12 |- ( ( x e. CC /\ _i e. CC ) -> ( ( x - _i ) =/= 0 <-> x =/= _i ) )
203	13, 5, 202	sylancl 644	. . . . . . . . . . 11 |- ( ( T. /\ x e. S ) -> ( ( x - _i ) =/= 0 <-> x =/= _i ) )
204	200, 203	mpbird 224	. . . . . . . . . 10 |- ( ( T. /\ x e. S ) -> ( x - _i ) =/= 0 )
205	99, 155, 153, 199, 204	divcan5d 9772	. . . . . . . . 9 |- ( ( T. /\ x e. S ) -> ( ( ( x - _i ) x. 1 ) / ( ( x - _i ) x. ( x + _i ) ) ) = ( 1 / ( x + _i ) ) )
206	189, 205	eqtr3d 2438	. . . . . . . 8 |- ( ( T. /\ x e. S ) -> ( ( x - _i ) / ( 1 + ( x ^ 2 ) ) ) = ( 1 / ( x + _i ) ) )
207	155	mulid1d 9061	. . . . . . . . . 10 |- ( ( T. /\ x e. S ) -> ( ( x + _i ) x. 1 ) = ( x + _i ) )
208	207, 187	oveq12d 6058	. . . . . . . . 9 |- ( ( T. /\ x e. S ) -> ( ( ( x + _i ) x. 1 ) / ( ( x + _i ) x. ( x - _i ) ) ) = ( ( x + _i ) / ( 1 + ( x ^ 2 ) ) ) )
209	99, 153, 155, 204, 199	divcan5d 9772	. . . . . . . . 9 |- ( ( T. /\ x e. S ) -> ( ( ( x + _i ) x. 1 ) / ( ( x + _i ) x. ( x - _i ) ) ) = ( 1 / ( x - _i ) ) )
210	208, 209	eqtr3d 2438	. . . . . . . 8 |- ( ( T. /\ x e. S ) -> ( ( x + _i ) / ( 1 + ( x ^ 2 ) ) ) = ( 1 / ( x - _i ) ) )
211	206, 210	oveq12d 6058	. . . . . . 7 |- ( ( T. /\ x e. S ) -> ( ( ( x - _i ) / ( 1 + ( x ^ 2 ) ) ) - ( ( x + _i ) / ( 1 + ( x ^ 2 ) ) ) ) = ( ( 1 / ( x + _i ) ) - ( 1 / ( x - _i ) ) ) )
212	162, 175, 211	3eqtr3rd 2445	. . . . . 6 |- ( ( T. /\ x e. S ) -> ( ( 1 / ( x + _i ) ) - ( 1 / ( x - _i ) ) ) = ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) )
213	212	mpteq2dva 4255	. . . . 5 |- ( T. -> ( x e. S |-> ( ( 1 / ( x + _i ) ) - ( 1 / ( x - _i ) ) ) ) = ( x e. S |-> ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) ) )
214	151, 213	eqtrd 2436	. . . 4 |- ( T. -> ( CC _D ( x e. S |-> ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) = ( x e. S |-> ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) ) )
215		halfcl 10149	. . . . 5 |- ( _i e. CC -> ( _i / 2 ) e. CC )
216	5, 215	mp1i 12	. . . 4 |- ( T. -> ( _i / 2 ) e. CC )
217	3, 24, 26, 214, 216	dvmptcmul 19803	. . 3 |- ( T. -> ( CC _D ( x e. S |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) ) = ( x e. S |-> ( ( _i / 2 ) x. ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) ) ) )
218		df-atan 20660	. . . . . . 7 |- arctan = ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) )
219	218	reseq1i 5101	. . . . . 6 |- (arctan |` S ) = ( ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) |` S )
220		atanf 20673	. . . . . . . . 9 |- arctan : ( CC \ { -u _i , _i } ) --> CC
221	220	fdmi 5555	. . . . . . . 8 |- dom arctan = ( CC \ { -u _i , _i } )
222	8, 221	sseqtri 3340	. . . . . . 7 |- S C_ ( CC \ { -u _i , _i } )
223		resmpt 5150	. . . . . . 7 |- ( S C_ ( CC \ { -u _i , _i } ) -> ( ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) |` S ) = ( x e. S |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) )
224	222, 223	ax-mp 8	. . . . . 6 |- ( ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) |` S ) = ( x e. S |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) )
225	219, 224	eqtri 2424	. . . . 5 |- (arctan |` S ) = ( x e. S |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) )
226	225	a1i 11	. . . 4 |- ( T. -> (arctan |` S ) = ( x e. S |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) )
227	226	oveq2d 6056	. . 3 |- ( T. -> ( CC _D (arctan |` S ) ) = ( CC _D ( x e. S |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) ) )
228		2ne0 10039	. . . . . . 7 |- 2 =/= 0
229		divcan6 9677	. . . . . . 7 |- ( ( ( _i e. CC /\ _i =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( _i / 2 ) x. ( 2 / _i ) ) = 1 )
230	5, 94, 167, 228, 229	mp4an 655	. . . . . 6 |- ( ( _i / 2 ) x. ( 2 / _i ) ) = 1
231	230	oveq1i 6050	. . . . 5 |- ( ( ( _i / 2 ) x. ( 2 / _i ) ) / ( 1 + ( x ^ 2 ) ) ) = ( 1 / ( 1 + ( x ^ 2 ) ) )
232	5, 215	mp1i 12	. . . . . 6 |- ( ( T. /\ x e. S ) -> ( _i / 2 ) e. CC )
233	167, 5, 94	divcli 9712	. . . . . . 7 |- ( 2 / _i ) e. CC
234	233	a1i 11	. . . . . 6 |- ( ( T. /\ x e. S ) -> ( 2 / _i ) e. CC )
235	232, 234, 158, 161	divassd 9781	. . . . 5 |- ( ( T. /\ x e. S ) -> ( ( ( _i / 2 ) x. ( 2 / _i ) ) / ( 1 + ( x ^ 2 ) ) ) = ( ( _i / 2 ) x. ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) ) )
236	231, 235	syl5eqr 2450	. . . 4 |- ( ( T. /\ x e. S ) -> ( 1 / ( 1 + ( x ^ 2 ) ) ) = ( ( _i / 2 ) x. ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) ) )
237	236	mpteq2dva 4255	. . 3 |- ( T. -> ( x e. S |-> ( 1 / ( 1 + ( x ^ 2 ) ) ) ) = ( x e. S |-> ( ( _i / 2 ) x. ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) ) ) )
238	217, 227, 237	3eqtr4d 2446	. 2 |- ( T. -> ( CC _D (arctan |` S ) ) = ( x e. S |-> ( 1 / ( 1 + ( x ^ 2 ) ) ) ) )
239	238	trud 1329	1 |- ( CC _D (arctan |` S ) ) = ( x e. S |-> ( 1 / ( 1 + ( x ^ 2 ) ) ) )

Syntax hints:   <-> wb 177   /\ wa 359   /\ w3a 936   T. wtru 1322   = wceq 1649   e. wcel 1721   =/= wne 2567   {crab 2670   _Vcvv 2916   \ cdif 3277   C_ wss 3280   {csn 3774   {cpr 3775   e. cmpt 4226   dom cdm 4837   ran crn 4838   |` cres 4839   -->wf 5409   -1-1-onto->wf1o 5412   ` cfv 5413  (class class class)co 6040   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   _ici 8948   + caddc 8949   x. cmul 8951   -oocmnf 9074   - cmin 9247   -ucneg 9248   / cdiv 9633   2c2 10005   (,]cioc 10873   ^cexp 11337   ↾_t crest 13603   TopOpenctopn 13604  ℂ_fldccnfld 16658   Topctop 16913  TopOnctopon 16914   _D cdv 19703   logclog 20405  arctancatan 20657

This theorem is referenced by:  atancn  20729

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025  ax-mulf 9026

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-fi 7374  df-sup 7404  df-oi 7435  df-card 7782  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-q 10531  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-ioo 10876  df-ioc 10877  df-ico 10878  df-icc 10879  df-fz 11000  df-fzo 11091  df-fl 11157  df-mod 11206  df-seq 11279  df-exp 11338  df-fac 11522  df-bc 11549  df-hash 11574  df-shft 11837  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-limsup 12220  df-clim 12237  df-rlim 12238  df-sum 12435  df-ef 12625  df-sin 12627  df-cos 12628  df-tan 12629  df-pi 12630  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-starv 13499  df-sca 13500  df-vsca 13501  df-tset 13503  df-ple 13504  df-ds 13506  df-unif 13507  df-hom 13508  df-cco 13509  df-rest 13605  df-topn 13606  df-topgen 13622  df-pt 13623  df-prds 13626  df-xrs 13681  df-0g 13682  df-gsum 13683  df-qtop 13688  df-imas 13689  df-xps 13691  df-mre 13766  df-mrc 13767  df-acs 13769  df-mnd 14645  df-submnd 14694  df-mulg 14770  df-cntz 15071  df-cmn 15369  df-psmet 16649  df-xmet 16650  df-met 16651  df-bl 16652  df-mopn 16653  df-fbas 16654  df-fg 16655  df-cnfld 16659  df-top 16918  df-bases 16920  df-topon 16921  df-topsp 16922  df-cld 17038  df-ntr 17039  df-cls 17040  df-nei 17117  df-lp 17155  df-perf 17156  df-cn 17245  df-cnp 17246  df-haus 17333  df-cmp 17404  df-tx 17547  df-hmeo 17740  df-fil 17831  df-fm 17923  df-flim 17924  df-flf 17925  df-xms 18303  df-ms 18304  df-tms 18305  df-cncf 18861  df-limc 19706  df-dv 19707  df-log 20407  df-atan 20660