Theorem dvaddbr 23701

Description: The sum rule for derivatives at a point. For the (simpler but more limited) function version, see dvadd 23703. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)

Hypotheses

Ref	Expression
dvadd.f	|- ( ph -> F : X --> CC )
dvadd.x	|- ( ph -> X C_ S )
dvadd.g	|- ( ph -> G : Y --> CC )
dvadd.y	|- ( ph -> Y C_ S )
dvaddbr.s	|- ( ph -> S C_ CC )
dvadd.k	|- ( ph -> K e. V )
dvadd.l	|- ( ph -> L e. V )
dvadd.bf	|- ( ph -> C ( S _D F ) K )
dvadd.bg	|- ( ph -> C ( S _D G ) L )
dvadd.j	|- J = ( TopOpen ` ℂfld )

Assertion

Ref	Expression
dvaddbr	|- ( ph -> C ( S _D ( F oF + G ) ) ( K + L ) )

Proof of Theorem dvaddbr

Dummy variables y z x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvadd.bf	. . . . . 6 |- ( ph -> C ( S _D F ) K )
2		eqid 2622	. . . . . . 7 |- ( J ↾t S ) = ( J ↾t S )
3		dvadd.j	. . . . . . 7 |- J = ( TopOpen ` ℂfld )
4		eqid 2622	. . . . . . 7 |- ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) = ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) )
5		dvaddbr.s	. . . . . . 7 |- ( ph -> S C_ CC )
6		dvadd.f	. . . . . . 7 |- ( ph -> F : X --> CC )
7		dvadd.x	. . . . . . 7 |- ( ph -> X C_ S )
8	2, 3, 4, 5, 6, 7	eldv 23662	. . . . . 6 |- ( ph -> ( C ( S _D F ) K <-> ( C e. ( ( int ` ( J ↾t S ) ) ` X ) /\ K e. ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) lim CC C ) ) ) )
9	1, 8	mpbid 222	. . . . 5 |- ( ph -> ( C e. ( ( int ` ( J ↾t S ) ) ` X ) /\ K e. ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) lim CC C ) ) )
10	9	simpld 475	. . . 4 |- ( ph -> C e. ( ( int ` ( J ↾t S ) ) ` X ) )
11		dvadd.bg	. . . . . 6 |- ( ph -> C ( S _D G ) L )
12		eqid 2622	. . . . . . 7 |- ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) )
13		dvadd.g	. . . . . . 7 |- ( ph -> G : Y --> CC )
14		dvadd.y	. . . . . . 7 |- ( ph -> Y C_ S )
15	2, 3, 12, 5, 13, 14	eldv 23662	. . . . . 6 |- ( ph -> ( C ( S _D G ) L <-> ( C e. ( ( int ` ( J ↾t S ) ) ` Y ) /\ L e. ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) lim CC C ) ) ) )
16	11, 15	mpbid 222	. . . . 5 |- ( ph -> ( C e. ( ( int ` ( J ↾t S ) ) ` Y ) /\ L e. ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) lim CC C ) ) )
17	16	simpld 475	. . . 4 |- ( ph -> C e. ( ( int ` ( J ↾t S ) ) ` Y ) )
18	10, 17	elind 3798	. . 3 |- ( ph -> C e. ( ( ( int ` ( J ↾t S ) ) ` X ) i^i ( ( int ` ( J ↾t S ) ) ` Y ) ) )
19	3	cnfldtopon 22586	. . . . . 6 |- J e. (TopOn ` CC )
20		resttopon 20965	. . . . . 6 |- ( ( J e. (TopOn ` CC ) /\ S C_ CC ) -> ( J ↾t S ) e. (TopOn ` S ) )
21	19, 5, 20	sylancr 695	. . . . 5 |- ( ph -> ( J ↾t S ) e. (TopOn ` S ) )
22		topontop 20718	. . . . 5 |- ( ( J ↾t S ) e. (TopOn ` S ) -> ( J ↾t S ) e. Top )
23	21, 22	syl 17	. . . 4 |- ( ph -> ( J ↾t S ) e. Top )
24		toponuni 20719	. . . . . 6 |- ( ( J ↾t S ) e. (TopOn ` S ) -> S = U. ( J ↾t S ) )
25	21, 24	syl 17	. . . . 5 |- ( ph -> S = U. ( J ↾t S ) )
26	7, 25	sseqtrd 3641	. . . 4 |- ( ph -> X C_ U. ( J ↾t S ) )
27	14, 25	sseqtrd 3641	. . . 4 |- ( ph -> Y C_ U. ( J ↾t S ) )
28		eqid 2622	. . . . 5 |- U. ( J ↾t S ) = U. ( J ↾t S )
29	28	ntrin 20865	. . . 4 |- ( ( ( J ↾t S ) e. Top /\ X C_ U. ( J ↾t S ) /\ Y C_ U. ( J ↾t S ) ) -> ( ( int ` ( J ↾t S ) ) ` ( X i^i Y ) ) = ( ( ( int ` ( J ↾t S ) ) ` X ) i^i ( ( int ` ( J ↾t S ) ) ` Y ) ) )
30	23, 26, 27, 29	syl3anc 1326	. . 3 |- ( ph -> ( ( int ` ( J ↾t S ) ) ` ( X i^i Y ) ) = ( ( ( int ` ( J ↾t S ) ) ` X ) i^i ( ( int ` ( J ↾t S ) ) ` Y ) ) )
31	18, 30	eleqtrrd 2704	. 2 |- ( ph -> C e. ( ( int ` ( J ↾t S ) ) ` ( X i^i Y ) ) )
32		inss1 3833	. . . . . . 7 |- ( X i^i Y ) C_ X
33		ssdif 3745	. . . . . . 7 |- ( ( X i^i Y ) C_ X -> ( ( X i^i Y ) \ { C } ) C_ ( X \ { C } ) )
34	32, 33	mp1i 13	. . . . . 6 |- ( ph -> ( ( X i^i Y ) \ { C } ) C_ ( X \ { C } ) )
35	34	sselda 3603	. . . . 5 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> z e. ( X \ { C } ) )
36	7, 5	sstrd 3613	. . . . . 6 |- ( ph -> X C_ CC )
37	28	ntrss2 20861	. . . . . . . 8 |- ( ( ( J ↾t S ) e. Top /\ X C_ U. ( J ↾t S ) ) -> ( ( int ` ( J ↾t S ) ) ` X ) C_ X )
38	23, 26, 37	syl2anc 693	. . . . . . 7 |- ( ph -> ( ( int ` ( J ↾t S ) ) ` X ) C_ X )
39	38, 10	sseldd 3604	. . . . . 6 |- ( ph -> C e. X )
40	6, 36, 39	dvlem 23660	. . . . 5 |- ( ( ph /\ z e. ( X \ { C } ) ) -> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) e. CC )
41	35, 40	syldan 487	. . . 4 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) e. CC )
42		inss2 3834	. . . . . . 7 |- ( X i^i Y ) C_ Y
43		ssdif 3745	. . . . . . 7 |- ( ( X i^i Y ) C_ Y -> ( ( X i^i Y ) \ { C } ) C_ ( Y \ { C } ) )
44	42, 43	mp1i 13	. . . . . 6 |- ( ph -> ( ( X i^i Y ) \ { C } ) C_ ( Y \ { C } ) )
45	44	sselda 3603	. . . . 5 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> z e. ( Y \ { C } ) )
46	14, 5	sstrd 3613	. . . . . 6 |- ( ph -> Y C_ CC )
47	28	ntrss2 20861	. . . . . . . 8 |- ( ( ( J ↾t S ) e. Top /\ Y C_ U. ( J ↾t S ) ) -> ( ( int ` ( J ↾t S ) ) ` Y ) C_ Y )
48	23, 27, 47	syl2anc 693	. . . . . . 7 |- ( ph -> ( ( int ` ( J ↾t S ) ) ` Y ) C_ Y )
49	48, 17	sseldd 3604	. . . . . 6 |- ( ph -> C e. Y )
50	13, 46, 49	dvlem 23660	. . . . 5 |- ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) e. CC )
51	45, 50	syldan 487	. . . 4 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) e. CC )
52		ssid 3624	. . . . 5 |- CC C_ CC
53	52	a1i 11	. . . 4 |- ( ph -> CC C_ CC )
54		txtopon 21394	. . . . . . 7 |- ( ( J e. (TopOn ` CC ) /\ J e. (TopOn ` CC ) ) -> ( J tX J ) e. (TopOn ` ( CC X. CC ) ) )
55	19, 19, 54	mp2an 708	. . . . . 6 |- ( J tX J ) e. (TopOn ` ( CC X. CC ) )
56	55	toponunii 20721	. . . . . . 7 |- ( CC X. CC ) = U. ( J tX J )
57	56	restid 16094	. . . . . 6 |- ( ( J tX J ) e. (TopOn ` ( CC X. CC ) ) -> ( ( J tX J ) ↾t ( CC X. CC ) ) = ( J tX J ) )
58	55, 57	ax-mp 5	. . . . 5 |- ( ( J tX J ) ↾t ( CC X. CC ) ) = ( J tX J )
59	58	eqcomi 2631	. . . 4 |- ( J tX J ) = ( ( J tX J ) ↾t ( CC X. CC ) )
60	9	simprd 479	. . . . 5 |- ( ph -> K e. ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) lim CC C ) )
61	40, 4	fmptd 6385	. . . . . . 7 |- ( ph -> ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) : ( X \ { C } ) --> CC )
62	36	ssdifssd 3748	. . . . . . 7 |- ( ph -> ( X \ { C } ) C_ CC )
63		eqid 2622	. . . . . . 7 |- ( J ↾t ( ( X \ { C } ) u. { C } ) ) = ( J ↾t ( ( X \ { C } ) u. { C } ) )
64	32, 7	syl5ss 3614	. . . . . . . . . . . . . 14 |- ( ph -> ( X i^i Y ) C_ S )
65	64, 25	sseqtrd 3641	. . . . . . . . . . . . 13 |- ( ph -> ( X i^i Y ) C_ U. ( J ↾t S ) )
66		difssd 3738	. . . . . . . . . . . . 13 |- ( ph -> ( U. ( J ↾t S ) \ X ) C_ U. ( J ↾t S ) )
67	65, 66	unssd 3789	. . . . . . . . . . . 12 |- ( ph -> ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ X ) ) C_ U. ( J ↾t S ) )
68		ssun1 3776	. . . . . . . . . . . . 13 |- ( X i^i Y ) C_ ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ X ) )
69	68	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( X i^i Y ) C_ ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ X ) ) )
70	28	ntrss 20859	. . . . . . . . . . . 12 |- ( ( ( J ↾t S ) e. Top /\ ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ X ) ) C_ U. ( J ↾t S ) /\ ( X i^i Y ) C_ ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ X ) ) ) -> ( ( int ` ( J ↾t S ) ) ` ( X i^i Y ) ) C_ ( ( int ` ( J ↾t S ) ) ` ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ X ) ) ) )
71	23, 67, 69, 70	syl3anc 1326	. . . . . . . . . . 11 |- ( ph -> ( ( int ` ( J ↾t S ) ) ` ( X i^i Y ) ) C_ ( ( int ` ( J ↾t S ) ) ` ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ X ) ) ) )
72	71, 31	sseldd 3604	. . . . . . . . . 10 |- ( ph -> C e. ( ( int ` ( J ↾t S ) ) ` ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ X ) ) ) )
73	72, 39	elind 3798	. . . . . . . . 9 |- ( ph -> C e. ( ( ( int ` ( J ↾t S ) ) ` ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ X ) ) ) i^i X ) )
74	32	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( X i^i Y ) C_ X )
75		eqid 2622	. . . . . . . . . . . 12 |- ( ( J ↾t S ) ↾t X ) = ( ( J ↾t S ) ↾t X )
76	28, 75	restntr 20986	. . . . . . . . . . 11 |- ( ( ( J ↾t S ) e. Top /\ X C_ U. ( J ↾t S ) /\ ( X i^i Y ) C_ X ) -> ( ( int ` ( ( J ↾t S ) ↾t X ) ) ` ( X i^i Y ) ) = ( ( ( int ` ( J ↾t S ) ) ` ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ X ) ) ) i^i X ) )
77	23, 26, 74, 76	syl3anc 1326	. . . . . . . . . 10 |- ( ph -> ( ( int ` ( ( J ↾t S ) ↾t X ) ) ` ( X i^i Y ) ) = ( ( ( int ` ( J ↾t S ) ) ` ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ X ) ) ) i^i X ) )
78	3	cnfldtop 22587	. . . . . . . . . . . . . 14 |- J e. Top
79	78	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> J e. Top )
80		cnex 10017	. . . . . . . . . . . . . 14 |- CC e. _V
81		ssexg 4804	. . . . . . . . . . . . . 14 |- ( ( S C_ CC /\ CC e. _V ) -> S e. _V )
82	5, 80, 81	sylancl 694	. . . . . . . . . . . . 13 |- ( ph -> S e. _V )
83		restabs 20969	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ X C_ S /\ S e. _V ) -> ( ( J ↾t S ) ↾t X ) = ( J ↾t X ) )
84	79, 7, 82, 83	syl3anc 1326	. . . . . . . . . . . 12 |- ( ph -> ( ( J ↾t S ) ↾t X ) = ( J ↾t X ) )
85	84	fveq2d 6195	. . . . . . . . . . 11 |- ( ph -> ( int ` ( ( J ↾t S ) ↾t X ) ) = ( int ` ( J ↾t X ) ) )
86	85	fveq1d 6193	. . . . . . . . . 10 |- ( ph -> ( ( int ` ( ( J ↾t S ) ↾t X ) ) ` ( X i^i Y ) ) = ( ( int ` ( J ↾t X ) ) ` ( X i^i Y ) ) )
87	77, 86	eqtr3d 2658	. . . . . . . . 9 |- ( ph -> ( ( ( int ` ( J ↾t S ) ) ` ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ X ) ) ) i^i X ) = ( ( int ` ( J ↾t X ) ) ` ( X i^i Y ) ) )
88	73, 87	eleqtrd 2703	. . . . . . . 8 |- ( ph -> C e. ( ( int ` ( J ↾t X ) ) ` ( X i^i Y ) ) )
89		undif1 4043	. . . . . . . . . . . 12 |- ( ( X \ { C } ) u. { C } ) = ( X u. { C } )
90	39	snssd 4340	. . . . . . . . . . . . 13 |- ( ph -> { C } C_ X )
91		ssequn2 3786	. . . . . . . . . . . . 13 |- ( { C } C_ X <-> ( X u. { C } ) = X )
92	90, 91	sylib 208	. . . . . . . . . . . 12 |- ( ph -> ( X u. { C } ) = X )
93	89, 92	syl5eq 2668	. . . . . . . . . . 11 |- ( ph -> ( ( X \ { C } ) u. { C } ) = X )
94	93	oveq2d 6666	. . . . . . . . . 10 |- ( ph -> ( J ↾t ( ( X \ { C } ) u. { C } ) ) = ( J ↾t X ) )
95	94	fveq2d 6195	. . . . . . . . 9 |- ( ph -> ( int ` ( J ↾t ( ( X \ { C } ) u. { C } ) ) ) = ( int ` ( J ↾t X ) ) )
96		undif1 4043	. . . . . . . . . 10 |- ( ( ( X i^i Y ) \ { C } ) u. { C } ) = ( ( X i^i Y ) u. { C } )
97	39, 49	elind 3798	. . . . . . . . . . . 12 |- ( ph -> C e. ( X i^i Y ) )
98	97	snssd 4340	. . . . . . . . . . 11 |- ( ph -> { C } C_ ( X i^i Y ) )
99		ssequn2 3786	. . . . . . . . . . 11 |- ( { C } C_ ( X i^i Y ) <-> ( ( X i^i Y ) u. { C } ) = ( X i^i Y ) )
100	98, 99	sylib 208	. . . . . . . . . 10 |- ( ph -> ( ( X i^i Y ) u. { C } ) = ( X i^i Y ) )
101	96, 100	syl5eq 2668	. . . . . . . . 9 |- ( ph -> ( ( ( X i^i Y ) \ { C } ) u. { C } ) = ( X i^i Y ) )
102	95, 101	fveq12d 6197	. . . . . . . 8 |- ( ph -> ( ( int ` ( J ↾t ( ( X \ { C } ) u. { C } ) ) ) ` ( ( ( X i^i Y ) \ { C } ) u. { C } ) ) = ( ( int ` ( J ↾t X ) ) ` ( X i^i Y ) ) )
103	88, 102	eleqtrrd 2704	. . . . . . 7 |- ( ph -> C e. ( ( int ` ( J ↾t ( ( X \ { C } ) u. { C } ) ) ) ` ( ( ( X i^i Y ) \ { C } ) u. { C } ) ) )
104	61, 34, 62, 3, 63, 103	limcres 23650	. . . . . 6 |- ( ph -> ( ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) |` ( ( X i^i Y ) \ { C } ) ) lim CC C ) = ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) lim CC C ) )
105	34	resmptd 5452	. . . . . . 7 |- ( ph -> ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) |` ( ( X i^i Y ) \ { C } ) ) = ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) )
106	105	oveq1d 6665	. . . . . 6 |- ( ph -> ( ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) |` ( ( X i^i Y ) \ { C } ) ) lim CC C ) = ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) lim CC C ) )
107	104, 106	eqtr3d 2658	. . . . 5 |- ( ph -> ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) lim CC C ) = ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) lim CC C ) )
108	60, 107	eleqtrd 2703	. . . 4 |- ( ph -> K e. ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) lim CC C ) )
109	16	simprd 479	. . . . 5 |- ( ph -> L e. ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) lim CC C ) )
110	50, 12	fmptd 6385	. . . . . . 7 |- ( ph -> ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) : ( Y \ { C } ) --> CC )
111	46	ssdifssd 3748	. . . . . . 7 |- ( ph -> ( Y \ { C } ) C_ CC )
112		eqid 2622	. . . . . . 7 |- ( J ↾t ( ( Y \ { C } ) u. { C } ) ) = ( J ↾t ( ( Y \ { C } ) u. { C } ) )
113		difssd 3738	. . . . . . . . . . . . 13 |- ( ph -> ( U. ( J ↾t S ) \ Y ) C_ U. ( J ↾t S ) )
114	65, 113	unssd 3789	. . . . . . . . . . . 12 |- ( ph -> ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ Y ) ) C_ U. ( J ↾t S ) )
115		ssun1 3776	. . . . . . . . . . . . 13 |- ( X i^i Y ) C_ ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ Y ) )
116	115	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( X i^i Y ) C_ ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ Y ) ) )
117	28	ntrss 20859	. . . . . . . . . . . 12 |- ( ( ( J ↾t S ) e. Top /\ ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ Y ) ) C_ U. ( J ↾t S ) /\ ( X i^i Y ) C_ ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ Y ) ) ) -> ( ( int ` ( J ↾t S ) ) ` ( X i^i Y ) ) C_ ( ( int ` ( J ↾t S ) ) ` ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ Y ) ) ) )
118	23, 114, 116, 117	syl3anc 1326	. . . . . . . . . . 11 |- ( ph -> ( ( int ` ( J ↾t S ) ) ` ( X i^i Y ) ) C_ ( ( int ` ( J ↾t S ) ) ` ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ Y ) ) ) )
119	118, 31	sseldd 3604	. . . . . . . . . 10 |- ( ph -> C e. ( ( int ` ( J ↾t S ) ) ` ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ Y ) ) ) )
120	119, 49	elind 3798	. . . . . . . . 9 |- ( ph -> C e. ( ( ( int ` ( J ↾t S ) ) ` ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ Y ) ) ) i^i Y ) )
121	42	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( X i^i Y ) C_ Y )
122		eqid 2622	. . . . . . . . . . . 12 |- ( ( J ↾t S ) ↾t Y ) = ( ( J ↾t S ) ↾t Y )
123	28, 122	restntr 20986	. . . . . . . . . . 11 |- ( ( ( J ↾t S ) e. Top /\ Y C_ U. ( J ↾t S ) /\ ( X i^i Y ) C_ Y ) -> ( ( int ` ( ( J ↾t S ) ↾t Y ) ) ` ( X i^i Y ) ) = ( ( ( int ` ( J ↾t S ) ) ` ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ Y ) ) ) i^i Y ) )
124	23, 27, 121, 123	syl3anc 1326	. . . . . . . . . 10 |- ( ph -> ( ( int ` ( ( J ↾t S ) ↾t Y ) ) ` ( X i^i Y ) ) = ( ( ( int ` ( J ↾t S ) ) ` ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ Y ) ) ) i^i Y ) )
125		restabs 20969	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ Y C_ S /\ S e. _V ) -> ( ( J ↾t S ) ↾t Y ) = ( J ↾t Y ) )
126	79, 14, 82, 125	syl3anc 1326	. . . . . . . . . . . 12 |- ( ph -> ( ( J ↾t S ) ↾t Y ) = ( J ↾t Y ) )
127	126	fveq2d 6195	. . . . . . . . . . 11 |- ( ph -> ( int ` ( ( J ↾t S ) ↾t Y ) ) = ( int ` ( J ↾t Y ) ) )
128	127	fveq1d 6193	. . . . . . . . . 10 |- ( ph -> ( ( int ` ( ( J ↾t S ) ↾t Y ) ) ` ( X i^i Y ) ) = ( ( int ` ( J ↾t Y ) ) ` ( X i^i Y ) ) )
129	124, 128	eqtr3d 2658	. . . . . . . . 9 |- ( ph -> ( ( ( int ` ( J ↾t S ) ) ` ( ( X i^i Y ) u. ( U. ( J ↾t S ) \ Y ) ) ) i^i Y ) = ( ( int ` ( J ↾t Y ) ) ` ( X i^i Y ) ) )
130	120, 129	eleqtrd 2703	. . . . . . . 8 |- ( ph -> C e. ( ( int ` ( J ↾t Y ) ) ` ( X i^i Y ) ) )
131		undif1 4043	. . . . . . . . . . . 12 |- ( ( Y \ { C } ) u. { C } ) = ( Y u. { C } )
132	49	snssd 4340	. . . . . . . . . . . . 13 |- ( ph -> { C } C_ Y )
133		ssequn2 3786	. . . . . . . . . . . . 13 |- ( { C } C_ Y <-> ( Y u. { C } ) = Y )
134	132, 133	sylib 208	. . . . . . . . . . . 12 |- ( ph -> ( Y u. { C } ) = Y )
135	131, 134	syl5eq 2668	. . . . . . . . . . 11 |- ( ph -> ( ( Y \ { C } ) u. { C } ) = Y )
136	135	oveq2d 6666	. . . . . . . . . 10 |- ( ph -> ( J ↾t ( ( Y \ { C } ) u. { C } ) ) = ( J ↾t Y ) )
137	136	fveq2d 6195	. . . . . . . . 9 |- ( ph -> ( int ` ( J ↾t ( ( Y \ { C } ) u. { C } ) ) ) = ( int ` ( J ↾t Y ) ) )
138	137, 101	fveq12d 6197	. . . . . . . 8 |- ( ph -> ( ( int ` ( J ↾t ( ( Y \ { C } ) u. { C } ) ) ) ` ( ( ( X i^i Y ) \ { C } ) u. { C } ) ) = ( ( int ` ( J ↾t Y ) ) ` ( X i^i Y ) ) )
139	130, 138	eleqtrrd 2704	. . . . . . 7 |- ( ph -> C e. ( ( int ` ( J ↾t ( ( Y \ { C } ) u. { C } ) ) ) ` ( ( ( X i^i Y ) \ { C } ) u. { C } ) ) )
140	110, 44, 111, 3, 112, 139	limcres 23650	. . . . . 6 |- ( ph -> ( ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) |` ( ( X i^i Y ) \ { C } ) ) lim CC C ) = ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) lim CC C ) )
141	44	resmptd 5452	. . . . . . 7 |- ( ph -> ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) |` ( ( X i^i Y ) \ { C } ) ) = ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) )
142	141	oveq1d 6665	. . . . . 6 |- ( ph -> ( ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) |` ( ( X i^i Y ) \ { C } ) ) lim CC C ) = ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) lim CC C ) )
143	140, 142	eqtr3d 2658	. . . . 5 |- ( ph -> ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) lim CC C ) = ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) lim CC C ) )
144	109, 143	eleqtrd 2703	. . . 4 |- ( ph -> L e. ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) lim CC C ) )
145	3	addcn 22668	. . . . 5 |- + e. ( ( J tX J ) Cn J )
146	5, 6, 7	dvcl 23663	. . . . . . 7 |- ( ( ph /\ C ( S _D F ) K ) -> K e. CC )
147	1, 146	mpdan 702	. . . . . 6 |- ( ph -> K e. CC )
148	5, 13, 14	dvcl 23663	. . . . . . 7 |- ( ( ph /\ C ( S _D G ) L ) -> L e. CC )
149	11, 148	mpdan 702	. . . . . 6 |- ( ph -> L e. CC )
150		opelxpi 5148	. . . . . 6 |- ( ( K e. CC /\ L e. CC ) -> <. K , L >. e. ( CC X. CC ) )
151	147, 149, 150	syl2anc 693	. . . . 5 |- ( ph -> <. K , L >. e. ( CC X. CC ) )
152	56	cncnpi 21082	. . . . 5 |- ( ( + e. ( ( J tX J ) Cn J ) /\ <. K , L >. e. ( CC X. CC ) ) -> + e. ( ( ( J tX J ) CnP J ) ` <. K , L >. ) )
153	145, 151, 152	sylancr 695	. . . 4 |- ( ph -> + e. ( ( ( J tX J ) CnP J ) ` <. K , L >. ) )
154	41, 51, 53, 53, 3, 59, 108, 144, 153	limccnp2 23656	. . 3 |- ( ph -> ( K + L ) e. ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) + ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) ) lim CC C ) )
155		eldifi 3732	. . . . . . . . . . 11 |- ( z e. ( ( X i^i Y ) \ { C } ) -> z e. ( X i^i Y ) )
156	155	adantl 482	. . . . . . . . . 10 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> z e. ( X i^i Y ) )
157		ffn 6045	. . . . . . . . . . . . 13 |- ( F : X --> CC -> F Fn X )
158	6, 157	syl 17	. . . . . . . . . . . 12 |- ( ph -> F Fn X )
159	158	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> F Fn X )
160		ffn 6045	. . . . . . . . . . . . 13 |- ( G : Y --> CC -> G Fn Y )
161	13, 160	syl 17	. . . . . . . . . . . 12 |- ( ph -> G Fn Y )
162	161	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> G Fn Y )
163		ssexg 4804	. . . . . . . . . . . . 13 |- ( ( X C_ CC /\ CC e. _V ) -> X e. _V )
164	36, 80, 163	sylancl 694	. . . . . . . . . . . 12 |- ( ph -> X e. _V )
165	164	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> X e. _V )
166		ssexg 4804	. . . . . . . . . . . . 13 |- ( ( Y C_ CC /\ CC e. _V ) -> Y e. _V )
167	46, 80, 166	sylancl 694	. . . . . . . . . . . 12 |- ( ph -> Y e. _V )
168	167	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> Y e. _V )
169		eqid 2622	. . . . . . . . . . 11 |- ( X i^i Y ) = ( X i^i Y )
170		eqidd 2623	. . . . . . . . . . 11 |- ( ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) /\ z e. X ) -> ( F ` z ) = ( F ` z ) )
171		eqidd 2623	. . . . . . . . . . 11 |- ( ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) /\ z e. Y ) -> ( G ` z ) = ( G ` z ) )
172	159, 162, 165, 168, 169, 170, 171	ofval 6906	. . . . . . . . . 10 |- ( ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) /\ z e. ( X i^i Y ) ) -> ( ( F oF + G ) ` z ) = ( ( F ` z ) + ( G ` z ) ) )
173	156, 172	mpdan 702	. . . . . . . . 9 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( F oF + G ) ` z ) = ( ( F ` z ) + ( G ` z ) ) )
174		eqidd 2623	. . . . . . . . . . 11 |- ( ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) /\ C e. X ) -> ( F ` C ) = ( F ` C ) )
175		eqidd 2623	. . . . . . . . . . 11 |- ( ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) /\ C e. Y ) -> ( G ` C ) = ( G ` C ) )
176	159, 162, 165, 168, 169, 174, 175	ofval 6906	. . . . . . . . . 10 |- ( ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) /\ C e. ( X i^i Y ) ) -> ( ( F oF + G ) ` C ) = ( ( F ` C ) + ( G ` C ) ) )
177	97, 176	mpidan 704	. . . . . . . . 9 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( F oF + G ) ` C ) = ( ( F ` C ) + ( G ` C ) ) )
178	173, 177	oveq12d 6668	. . . . . . . 8 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( F oF + G ) ` z ) - ( ( F oF + G ) ` C ) ) = ( ( ( F ` z ) + ( G ` z ) ) - ( ( F ` C ) + ( G ` C ) ) ) )
179		difss 3737	. . . . . . . . . . . 12 |- ( ( X i^i Y ) \ { C } ) C_ ( X i^i Y )
180	179, 32	sstri 3612	. . . . . . . . . . 11 |- ( ( X i^i Y ) \ { C } ) C_ X
181	180	sseli 3599	. . . . . . . . . 10 |- ( z e. ( ( X i^i Y ) \ { C } ) -> z e. X )
182		ffvelrn 6357	. . . . . . . . . 10 |- ( ( F : X --> CC /\ z e. X ) -> ( F ` z ) e. CC )
183	6, 181, 182	syl2an 494	. . . . . . . . 9 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( F ` z ) e. CC )
184	179, 42	sstri 3612	. . . . . . . . . . 11 |- ( ( X i^i Y ) \ { C } ) C_ Y
185	184	sseli 3599	. . . . . . . . . 10 |- ( z e. ( ( X i^i Y ) \ { C } ) -> z e. Y )
186		ffvelrn 6357	. . . . . . . . . 10 |- ( ( G : Y --> CC /\ z e. Y ) -> ( G ` z ) e. CC )
187	13, 185, 186	syl2an 494	. . . . . . . . 9 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( G ` z ) e. CC )
188	6, 39	ffvelrnd 6360	. . . . . . . . . 10 |- ( ph -> ( F ` C ) e. CC )
189	188	adantr 481	. . . . . . . . 9 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( F ` C ) e. CC )
190	13, 49	ffvelrnd 6360	. . . . . . . . . 10 |- ( ph -> ( G ` C ) e. CC )
191	190	adantr 481	. . . . . . . . 9 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( G ` C ) e. CC )
192	183, 187, 189, 191	addsub4d 10439	. . . . . . . 8 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( F ` z ) + ( G ` z ) ) - ( ( F ` C ) + ( G ` C ) ) ) = ( ( ( F ` z ) - ( F ` C ) ) + ( ( G ` z ) - ( G ` C ) ) ) )
193	178, 192	eqtrd 2656	. . . . . . 7 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( F oF + G ) ` z ) - ( ( F oF + G ) ` C ) ) = ( ( ( F ` z ) - ( F ` C ) ) + ( ( G ` z ) - ( G ` C ) ) ) )
194	193	oveq1d 6665	. . . . . 6 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( ( F oF + G ) ` z ) - ( ( F oF + G ) ` C ) ) / ( z - C ) ) = ( ( ( ( F ` z ) - ( F ` C ) ) + ( ( G ` z ) - ( G ` C ) ) ) / ( z - C ) ) )
195	183, 189	subcld 10392	. . . . . . 7 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( F ` z ) - ( F ` C ) ) e. CC )
196	187, 191	subcld 10392	. . . . . . 7 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( G ` z ) - ( G ` C ) ) e. CC )
197	180, 36	syl5ss 3614	. . . . . . . . 9 |- ( ph -> ( ( X i^i Y ) \ { C } ) C_ CC )
198	197	sselda 3603	. . . . . . . 8 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> z e. CC )
199	36, 39	sseldd 3604	. . . . . . . . 9 |- ( ph -> C e. CC )
200	199	adantr 481	. . . . . . . 8 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> C e. CC )
201	198, 200	subcld 10392	. . . . . . 7 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( z - C ) e. CC )
202		eldifsni 4320	. . . . . . . . 9 |- ( z e. ( ( X i^i Y ) \ { C } ) -> z =/= C )
203	202	adantl 482	. . . . . . . 8 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> z =/= C )
204	198, 200, 203	subne0d 10401	. . . . . . 7 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( z - C ) =/= 0 )
205	195, 196, 201, 204	divdird 10839	. . . . . 6 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( ( F ` z ) - ( F ` C ) ) + ( ( G ` z ) - ( G ` C ) ) ) / ( z - C ) ) = ( ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) + ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) )
206	194, 205	eqtrd 2656	. . . . 5 |- ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( ( F oF + G ) ` z ) - ( ( F oF + G ) ` C ) ) / ( z - C ) ) = ( ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) + ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) )
207	206	mpteq2dva 4744	. . . 4 |- ( ph -> ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F oF + G ) ` z ) - ( ( F oF + G ) ` C ) ) / ( z - C ) ) ) = ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) + ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) ) )
208	207	oveq1d 6665	. . 3 |- ( ph -> ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F oF + G ) ` z ) - ( ( F oF + G ) ` C ) ) / ( z - C ) ) ) lim CC C ) = ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) + ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) ) lim CC C ) )
209	154, 208	eleqtrrd 2704	. 2 |- ( ph -> ( K + L ) e. ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F oF + G ) ` z ) - ( ( F oF + G ) ` C ) ) / ( z - C ) ) ) lim CC C ) )
210		eqid 2622	. . 3 |- ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F oF + G ) ` z ) - ( ( F oF + G ) ` C ) ) / ( z - C ) ) ) = ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F oF + G ) ` z ) - ( ( F oF + G ) ` C ) ) / ( z - C ) ) )
211		addcl 10018	. . . . 5 |- ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
212	211	adantl 482	. . . 4 |- ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x + y ) e. CC )
213	212, 6, 13, 164, 167, 169	off 6912	. . 3 |- ( ph -> ( F oF + G ) : ( X i^i Y ) --> CC )
214	2, 3, 210, 5, 213, 64	eldv 23662	. 2 |- ( ph -> ( C ( S _D ( F oF + G ) ) ( K + L ) <-> ( C e. ( ( int ` ( J ↾t S ) ) ` ( X i^i Y ) ) /\ ( K + L ) e. ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F oF + G ) ` z ) - ( ( F oF + G ) ` C ) ) / ( z - C ) ) ) lim CC C ) ) ) )
215	31, 209, 214	mpbir2and 957	1 |- ( ph -> C ( S _D ( F oF + G ) ) ( K + L ) )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   {csn 4177   <.cop 4183   U.cuni 4436   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   |` cres 5116   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   oFcof 6895   CCcc 9934   + caddc 9939   - cmin 10266   / cdiv 10684   ↾_t crest 16081   TopOpenctopn 16082  ℂ_fldccnfld 19746   Topctop 20698  TopOnctopon 20715   intcnt 20821   Cn ccn 21028   CnP ccnp 21029   tX ctx 21363   lim CC climc 23626   _D cdv 23627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-icc 12182  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-xrs 16162  df-qtop 16167  df-imas 16168  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-submnd 17336  df-mulg 17541  df-cntz 17750  df-cmn 18195  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-cn 21031  df-cnp 21032  df-tx 21365  df-hmeo 21558  df-xms 22125  df-ms 22126  df-tms 22127  df-limc 23630  df-dv 23631

This theorem is referenced by:  dvadd  23703  dvaddf  23705