Theorem dvef 22874

Description: Derivative of the exponential function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.)

Assertion

Ref	Expression
dvef	|- ( CC _D exp ) = exp

Proof of Theorem dvef

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

Step	Hyp	Ref	Expression
1		dvfcn 22805	. . . . . . 7 |- ( CC _D exp ) : dom ( CC _D exp ) --> CC
2		dvbsss 22799	. . . . . . . . 9 |- dom ( CC _D exp ) C_ CC
3		efcl 14080	. . . . . . . . . . . . . . . 16 |- ( x e. CC -> ( exp ` x ) e. CC )
4		fconstg 5730	. . . . . . . . . . . . . . . 16 |- ( ( exp ` x ) e. CC -> ( CC X. { ( exp ` x ) } ) : CC --> { ( exp ` x ) } )
5	3, 4	syl 17	. . . . . . . . . . . . . . 15 |- ( x e. CC -> ( CC X. { ( exp ` x ) } ) : CC --> { ( exp ` x ) } )
6	3	snssd 4088	. . . . . . . . . . . . . . 15 |- ( x e. CC -> { ( exp ` x ) } C_ CC )
7	5, 6	fssd 5698	. . . . . . . . . . . . . 14 |- ( x e. CC -> ( CC X. { ( exp ` x ) } ) : CC --> CC )
8		ssid 3426	. . . . . . . . . . . . . . 15 |- CC C_ CC
9	8	a1i 11	. . . . . . . . . . . . . 14 |- ( x e. CC -> CC C_ CC )
10		subcl 9825	. . . . . . . . . . . . . . . . 17 |- ( ( z e. CC /\ x e. CC ) -> ( z - x ) e. CC )
11	10	ancoms 454	. . . . . . . . . . . . . . . 16 |- ( ( x e. CC /\ z e. CC ) -> ( z - x ) e. CC )
12		efcl 14080	. . . . . . . . . . . . . . . 16 |- ( ( z - x ) e. CC -> ( exp ` ( z - x ) ) e. CC )
13	11, 12	syl 17	. . . . . . . . . . . . . . 15 |- ( ( x e. CC /\ z e. CC ) -> ( exp ` ( z - x ) ) e. CC )
14		eqid 2428	. . . . . . . . . . . . . . 15 |- ( z e. CC |-> ( exp ` ( z - x ) ) ) = ( z e. CC |-> ( exp ` ( z - x ) ) )
15	13, 14	fmptd 6005	. . . . . . . . . . . . . 14 |- ( x e. CC -> ( z e. CC |-> ( exp ` ( z - x ) ) ) : CC --> CC )
16		0cn 9586	. . . . . . . . . . . . . . 15 |- 0 e. CC
17	16	a1i 11	. . . . . . . . . . . . . 14 |- ( x e. CC -> 0 e. CC )
18		ax-1cn 9548	. . . . . . . . . . . . . . 15 |- 1 e. CC
19	18	a1i 11	. . . . . . . . . . . . . 14 |- ( x e. CC -> 1 e. CC )
20	16	elexi 3032	. . . . . . . . . . . . . . . . . 18 |- 0 e. _V
21	20	snid 3969	. . . . . . . . . . . . . . . . 17 |- 0 e. { 0 }
22		opelxpi 4828	. . . . . . . . . . . . . . . . 17 |- ( ( x e. CC /\ 0 e. { 0 } ) -> <. x , 0 >. e. ( CC X. { 0 } ) )
23	21, 22	mpan2 675	. . . . . . . . . . . . . . . 16 |- ( x e. CC -> <. x , 0 >. e. ( CC X. { 0 } ) )
24		dvconst 22813	. . . . . . . . . . . . . . . . 17 |- ( ( exp ` x ) e. CC -> ( CC _D ( CC X. { ( exp ` x ) } ) ) = ( CC X. { 0 } ) )
25	3, 24	syl 17	. . . . . . . . . . . . . . . 16 |- ( x e. CC -> ( CC _D ( CC X. { ( exp ` x ) } ) ) = ( CC X. { 0 } ) )
26	23, 25	eleqtrrd 2509	. . . . . . . . . . . . . . 15 |- ( x e. CC -> <. x , 0 >. e. ( CC _D ( CC X. { ( exp ` x ) } ) ) )
27		df-br 4367	. . . . . . . . . . . . . . 15 |- ( x ( CC _D ( CC X. { ( exp ` x ) } ) ) 0 <-> <. x , 0 >. e. ( CC _D ( CC X. { ( exp ` x ) } ) ) )
28	26, 27	sylibr 215	. . . . . . . . . . . . . 14 |- ( x e. CC -> x ( CC _D ( CC X. { ( exp ` x ) } ) ) 0 )
29		eff 14079	. . . . . . . . . . . . . . . . . 18 |- exp : CC --> CC
30	29	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( x e. CC -> exp : CC --> CC )
31		eqid 2428	. . . . . . . . . . . . . . . . . 18 |- ( z e. CC |-> ( z - x ) ) = ( z e. CC |-> ( z - x ) )
32	11, 31	fmptd 6005	. . . . . . . . . . . . . . . . 17 |- ( x e. CC -> ( z e. CC |-> ( z - x ) ) : CC --> CC )
33		oveq1 6256	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( z - x ) = ( x - x ) )
34		ovex 6277	. . . . . . . . . . . . . . . . . . . 20 |- ( x - x ) e. _V
35	33, 31, 34	fvmpt 5908	. . . . . . . . . . . . . . . . . . 19 |- ( x e. CC -> ( ( z e. CC |-> ( z - x ) ) ` x ) = ( x - x ) )
36		subid 9844	. . . . . . . . . . . . . . . . . . 19 |- ( x e. CC -> ( x - x ) = 0 )
37	35, 36	eqtrd 2462	. . . . . . . . . . . . . . . . . 18 |- ( x e. CC -> ( ( z e. CC |-> ( z - x ) ) ` x ) = 0 )
38		dveflem 22873	. . . . . . . . . . . . . . . . . 18 |- 0 ( CC _D exp ) 1
39	37, 38	syl6eqbr 4404	. . . . . . . . . . . . . . . . 17 |- ( x e. CC -> ( ( z e. CC |-> ( z - x ) ) ` x ) ( CC _D exp ) 1 )
40	18	elexi 3032	. . . . . . . . . . . . . . . . . . . . 21 |- 1 e. _V
41	40	snid 3969	. . . . . . . . . . . . . . . . . . . 20 |- 1 e. { 1 }
42		opelxpi 4828	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x e. CC /\ 1 e. { 1 } ) -> <. x , 1 >. e. ( CC X. { 1 } ) )
43	41, 42	mpan2 675	. . . . . . . . . . . . . . . . . . 19 |- ( x e. CC -> <. x , 1 >. e. ( CC X. { 1 } ) )
44		cnelprrecn 9583	. . . . . . . . . . . . . . . . . . . . . 22 |- CC e. { RR , CC }
45	44	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. CC -> CC e. { RR , CC } )
46		simpr 462	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. CC /\ z e. CC ) -> z e. CC )
47	18	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. CC /\ z e. CC ) -> 1 e. CC )
48	45	dvmptid 22853	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. CC -> ( CC _D ( z e. CC |-> z ) ) = ( z e. CC |-> 1 ) )
49		simpl 458	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. CC /\ z e. CC ) -> x e. CC )
50	16	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. CC /\ z e. CC ) -> 0 e. CC )
51		id 22	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. CC -> x e. CC )
52	45, 51	dvmptc 22854	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. CC -> ( CC _D ( z e. CC |-> x ) ) = ( z e. CC |-> 0 ) )
53	45, 46, 47, 48, 49, 50, 52	dvmptsub 22863	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. CC -> ( CC _D ( z e. CC |-> ( z - x ) ) ) = ( z e. CC |-> ( 1 - 0 ) ) )
54		1m0e1 10671	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 1 - 0 ) = 1
55	54	mpteq2i 4450	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. CC |-> ( 1 - 0 ) ) = ( z e. CC |-> 1 )
56		fconstmpt 4840	. . . . . . . . . . . . . . . . . . . . 21 |- ( CC X. { 1 } ) = ( z e. CC |-> 1 )
57	55, 56	eqtr4i 2453	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. CC |-> ( 1 - 0 ) ) = ( CC X. { 1 } )
58	53, 57	syl6eq 2478	. . . . . . . . . . . . . . . . . . 19 |- ( x e. CC -> ( CC _D ( z e. CC |-> ( z - x ) ) ) = ( CC X. { 1 } ) )
59	43, 58	eleqtrrd 2509	. . . . . . . . . . . . . . . . . 18 |- ( x e. CC -> <. x , 1 >. e. ( CC _D ( z e. CC |-> ( z - x ) ) ) )
60		df-br 4367	. . . . . . . . . . . . . . . . . 18 |- ( x ( CC _D ( z e. CC |-> ( z - x ) ) ) 1 <-> <. x , 1 >. e. ( CC _D ( z e. CC |-> ( z - x ) ) ) )
61	59, 60	sylibr 215	. . . . . . . . . . . . . . . . 17 |- ( x e. CC -> x ( CC _D ( z e. CC |-> ( z - x ) ) ) 1 )
62		eqid 2428	. . . . . . . . . . . . . . . . 17 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
63	30, 9, 32, 9, 9, 9, 19, 19, 39, 61, 62	dvcobr 22842	. . . . . . . . . . . . . . . 16 |- ( x e. CC -> x ( CC _D ( exp o. ( z e. CC |-> ( z - x ) ) ) ) ( 1 x. 1 ) )
64		1t1e1 10708	. . . . . . . . . . . . . . . 16 |- ( 1 x. 1 ) = 1
65	63, 64	syl6breq 4406	. . . . . . . . . . . . . . 15 |- ( x e. CC -> x ( CC _D ( exp o. ( z e. CC |-> ( z - x ) ) ) ) 1 )
66		eqidd 2429	. . . . . . . . . . . . . . . . . 18 |- ( x e. CC -> ( z e. CC |-> ( z - x ) ) = ( z e. CC |-> ( z - x ) ) )
67	30	feqmptd 5878	. . . . . . . . . . . . . . . . . 18 |- ( x e. CC -> exp = ( y e. CC |-> ( exp ` y ) ) )
68		fveq2 5825	. . . . . . . . . . . . . . . . . 18 |- ( y = ( z - x ) -> ( exp ` y ) = ( exp ` ( z - x ) ) )
69	11, 66, 67, 68	fmptco 6015	. . . . . . . . . . . . . . . . 17 |- ( x e. CC -> ( exp o. ( z e. CC |-> ( z - x ) ) ) = ( z e. CC |-> ( exp ` ( z - x ) ) ) )
70	69	oveq2d 6265	. . . . . . . . . . . . . . . 16 |- ( x e. CC -> ( CC _D ( exp o. ( z e. CC |-> ( z - x ) ) ) ) = ( CC _D ( z e. CC |-> ( exp ` ( z - x ) ) ) ) )
71	70	breqd 4377	. . . . . . . . . . . . . . 15 |- ( x e. CC -> ( x ( CC _D ( exp o. ( z e. CC |-> ( z - x ) ) ) ) 1 <-> x ( CC _D ( z e. CC |-> ( exp ` ( z - x ) ) ) ) 1 ) )
72	65, 71	mpbid 213	. . . . . . . . . . . . . 14 |- ( x e. CC -> x ( CC _D ( z e. CC |-> ( exp ` ( z - x ) ) ) ) 1 )
73	7, 9, 15, 9, 9, 17, 19, 28, 72, 62	dvmulbr 22835	. . . . . . . . . . . . 13 |- ( x e. CC -> x ( CC _D ( ( CC X. { ( exp ` x ) } ) oF x. ( z e. CC |-> ( exp ` ( z - x ) ) ) ) ) ( ( 0 x. ( ( z e. CC |-> ( exp ` ( z - x ) ) ) ` x ) ) + ( 1 x. ( ( CC X. { ( exp ` x ) } ) ` x ) ) ) )
74	15, 51	ffvelrnd 5982	. . . . . . . . . . . . . . . 16 |- ( x e. CC -> ( ( z e. CC |-> ( exp ` ( z - x ) ) ) ` x ) e. CC )
75	74	mul02d 9782	. . . . . . . . . . . . . . 15 |- ( x e. CC -> ( 0 x. ( ( z e. CC |-> ( exp ` ( z - x ) ) ) ` x ) ) = 0 )
76		fvex 5835	. . . . . . . . . . . . . . . . . 18 |- ( exp ` x ) e. _V
77	76	fvconst2 6079	. . . . . . . . . . . . . . . . 17 |- ( x e. CC -> ( ( CC X. { ( exp ` x ) } ) ` x ) = ( exp ` x ) )
78	77	oveq2d 6265	. . . . . . . . . . . . . . . 16 |- ( x e. CC -> ( 1 x. ( ( CC X. { ( exp ` x ) } ) ` x ) ) = ( 1 x. ( exp ` x ) ) )
79	3	mulid2d 9612	. . . . . . . . . . . . . . . 16 |- ( x e. CC -> ( 1 x. ( exp ` x ) ) = ( exp ` x ) )
80	78, 79	eqtrd 2462	. . . . . . . . . . . . . . 15 |- ( x e. CC -> ( 1 x. ( ( CC X. { ( exp ` x ) } ) ` x ) ) = ( exp ` x ) )
81	75, 80	oveq12d 6267	. . . . . . . . . . . . . 14 |- ( x e. CC -> ( ( 0 x. ( ( z e. CC |-> ( exp ` ( z - x ) ) ) ` x ) ) + ( 1 x. ( ( CC X. { ( exp ` x ) } ) ` x ) ) ) = ( 0 + ( exp ` x ) ) )
82	3	addid2d 9785	. . . . . . . . . . . . . 14 |- ( x e. CC -> ( 0 + ( exp ` x ) ) = ( exp ` x ) )
83	81, 82	eqtrd 2462	. . . . . . . . . . . . 13 |- ( x e. CC -> ( ( 0 x. ( ( z e. CC |-> ( exp ` ( z - x ) ) ) ` x ) ) + ( 1 x. ( ( CC X. { ( exp ` x ) } ) ` x ) ) ) = ( exp ` x ) )
84	73, 83	breqtrd 4391	. . . . . . . . . . . 12 |- ( x e. CC -> x ( CC _D ( ( CC X. { ( exp ` x ) } ) oF x. ( z e. CC |-> ( exp ` ( z - x ) ) ) ) ) ( exp ` x ) )
85		cnex 9571	. . . . . . . . . . . . . . . . 17 |- CC e. _V
86	85	a1i 11	. . . . . . . . . . . . . . . 16 |- ( x e. CC -> CC e. _V )
87	76	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( x e. CC /\ z e. CC ) -> ( exp ` x ) e. _V )
88		fvex 5835	. . . . . . . . . . . . . . . . 17 |- ( exp ` ( z - x ) ) e. _V
89	88	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( x e. CC /\ z e. CC ) -> ( exp ` ( z - x ) ) e. _V )
90		fconstmpt 4840	. . . . . . . . . . . . . . . . 17 |- ( CC X. { ( exp ` x ) } ) = ( z e. CC |-> ( exp ` x ) )
91	90	a1i 11	. . . . . . . . . . . . . . . 16 |- ( x e. CC -> ( CC X. { ( exp ` x ) } ) = ( z e. CC |-> ( exp ` x ) ) )
92		eqidd 2429	. . . . . . . . . . . . . . . 16 |- ( x e. CC -> ( z e. CC |-> ( exp ` ( z - x ) ) ) = ( z e. CC |-> ( exp ` ( z - x ) ) ) )
93	86, 87, 89, 91, 92	offval2 6506	. . . . . . . . . . . . . . 15 |- ( x e. CC -> ( ( CC X. { ( exp ` x ) } ) oF x. ( z e. CC |-> ( exp ` ( z - x ) ) ) ) = ( z e. CC |-> ( ( exp ` x ) x. ( exp ` ( z - x ) ) ) ) )
94	30	feqmptd 5878	. . . . . . . . . . . . . . . 16 |- ( x e. CC -> exp = ( z e. CC |-> ( exp ` z ) ) )
95		efadd 14091	. . . . . . . . . . . . . . . . . . 19 |- ( ( x e. CC /\ ( z - x ) e. CC ) -> ( exp ` ( x + ( z - x ) ) ) = ( ( exp ` x ) x. ( exp ` ( z - x ) ) ) )
96	11, 95	syldan 472	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. CC /\ z e. CC ) -> ( exp ` ( x + ( z - x ) ) ) = ( ( exp ` x ) x. ( exp ` ( z - x ) ) ) )
97		pncan3 9834	. . . . . . . . . . . . . . . . . . 19 |- ( ( x e. CC /\ z e. CC ) -> ( x + ( z - x ) ) = z )
98	97	fveq2d 5829	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. CC /\ z e. CC ) -> ( exp ` ( x + ( z - x ) ) ) = ( exp ` z ) )
99	96, 98	eqtr3d 2464	. . . . . . . . . . . . . . . . 17 |- ( ( x e. CC /\ z e. CC ) -> ( ( exp ` x ) x. ( exp ` ( z - x ) ) ) = ( exp ` z ) )
100	99	mpteq2dva 4453	. . . . . . . . . . . . . . . 16 |- ( x e. CC -> ( z e. CC |-> ( ( exp ` x ) x. ( exp ` ( z - x ) ) ) ) = ( z e. CC |-> ( exp ` z ) ) )
101	94, 100	eqtr4d 2465	. . . . . . . . . . . . . . 15 |- ( x e. CC -> exp = ( z e. CC |-> ( ( exp ` x ) x. ( exp ` ( z - x ) ) ) ) )
102	93, 101	eqtr4d 2465	. . . . . . . . . . . . . 14 |- ( x e. CC -> ( ( CC X. { ( exp ` x ) } ) oF x. ( z e. CC |-> ( exp ` ( z - x ) ) ) ) = exp )
103	102	oveq2d 6265	. . . . . . . . . . . . 13 |- ( x e. CC -> ( CC _D ( ( CC X. { ( exp ` x ) } ) oF x. ( z e. CC |-> ( exp ` ( z - x ) ) ) ) ) = ( CC _D exp ) )
104	103	breqd 4377	. . . . . . . . . . . 12 |- ( x e. CC -> ( x ( CC _D ( ( CC X. { ( exp ` x ) } ) oF x. ( z e. CC |-> ( exp ` ( z - x ) ) ) ) ) ( exp ` x ) <-> x ( CC _D exp ) ( exp ` x ) ) )
105	84, 104	mpbid 213	. . . . . . . . . . 11 |- ( x e. CC -> x ( CC _D exp ) ( exp ` x ) )
106		vex 3025	. . . . . . . . . . . 12 |- x e. _V
107	106, 76	breldm 5001	. . . . . . . . . . 11 |- ( x ( CC _D exp ) ( exp ` x ) -> x e. dom ( CC _D exp ) )
108	105, 107	syl 17	. . . . . . . . . 10 |- ( x e. CC -> x e. dom ( CC _D exp ) )
109	108	ssriv 3411	. . . . . . . . 9 |- CC C_ dom ( CC _D exp )
110	2, 109	eqssi 3423	. . . . . . . 8 |- dom ( CC _D exp ) = CC
111	110	feq2i 5682	. . . . . . 7 |- ( ( CC _D exp ) : dom ( CC _D exp ) --> CC <-> ( CC _D exp ) : CC --> CC )
112	1, 111	mpbi 211	. . . . . 6 |- ( CC _D exp ) : CC --> CC
113	112	a1i 11	. . . . 5 |- ( T. -> ( CC _D exp ) : CC --> CC )
114	113	feqmptd 5878	. . . 4 |- ( T. -> ( CC _D exp ) = ( x e. CC |-> ( ( CC _D exp ) ` x ) ) )
115		ffun 5691	. . . . . . 7 |- ( ( CC _D exp ) : dom ( CC _D exp ) --> CC -> Fun ( CC _D exp ) )
116	1, 115	ax-mp 5	. . . . . 6 |- Fun ( CC _D exp )
117		funbrfv 5863	. . . . . 6 |- ( Fun ( CC _D exp ) -> ( x ( CC _D exp ) ( exp ` x ) -> ( ( CC _D exp ) ` x ) = ( exp ` x ) ) )
118	116, 105, 117	mpsyl 65	. . . . 5 |- ( x e. CC -> ( ( CC _D exp ) ` x ) = ( exp ` x ) )
119	118	mpteq2ia 4449	. . . 4 |- ( x e. CC |-> ( ( CC _D exp ) ` x ) ) = ( x e. CC |-> ( exp ` x ) )
120	114, 119	syl6eq 2478	. . 3 |- ( T. -> ( CC _D exp ) = ( x e. CC |-> ( exp ` x ) ) )
121	29	a1i 11	. . . 4 |- ( T. -> exp : CC --> CC )
122	121	feqmptd 5878	. . 3 |- ( T. -> exp = ( x e. CC |-> ( exp ` x ) ) )
123	120, 122	eqtr4d 2465	. 2 |- ( T. -> ( CC _D exp ) = exp )
124	123	trud 1446	1 |- ( CC _D exp ) = exp

Syntax hints:   /\ wa 370   = wceq 1437   T. wtru 1438   e. wcel 1872   _Vcvv 3022   C_ wss 3379   {csn 3941   {cpr 3943   <.cop 3947   class class class wbr 4366   |-> cmpt 4425   X. cxp 4794   dom cdm 4796   o. ccom 4800   Fun wfun 5538   -->wf 5540   ` cfv 5544  (class class class)co 6249   oFcof 6487   CCcc 9488   RRcr 9489   0cc0 9490   1c1 9491   + caddc 9493   x. cmul 9495   - cmin 9811   expce 14057   TopOpenctopn 15263  ℂ_fldccnfld 18913   _D cdv 22760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-inf2 8099  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567  ax-pre-sup 9568  ax-addf 9569  ax-mulf 9570

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-int 4199  df-iun 4244  df-iin 4245  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-se 4756  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-isom 5553  df-riota 6211  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-of 6489  df-om 6651  df-1st 6751  df-2nd 6752  df-supp 6870  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-1o 7137  df-2o 7138  df-oadd 7141  df-er 7318  df-map 7429  df-pm 7430  df-ixp 7478  df-en 7525  df-dom 7526  df-sdom 7527  df-fin 7528  df-fsupp 7837  df-fi 7878  df-sup 7909  df-inf 7910  df-oi 7978  df-card 8325  df-cda 8549  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9813  df-neg 9814  df-div 10221  df-nn 10561  df-2 10619  df-3 10620  df-4 10621  df-5 10622  df-6 10623  df-7 10624  df-8 10625  df-9 10626  df-10 10627  df-n0 10821  df-z 10889  df-dec 11003  df-uz 11111  df-q 11216  df-rp 11254  df-xneg 11360  df-xadd 11361  df-xmul 11362  df-ico 11592  df-icc 11593  df-fz 11736  df-fzo 11867  df-fl 11978  df-seq 12164  df-exp 12223  df-fac 12410  df-bc 12438  df-hash 12466  df-shft 13074  df-cj 13106  df-re 13107  df-im 13108  df-sqrt 13242  df-abs 13243  df-limsup 13469  df-clim 13495  df-rlim 13496  df-sum 13696  df-ef 14064  df-struct 15066  df-ndx 15067  df-slot 15068  df-base 15069  df-sets 15070  df-ress 15071  df-plusg 15146  df-mulr 15147  df-starv 15148  df-sca 15149  df-vsca 15150  df-ip 15151  df-tset 15152  df-ple 15153  df-ds 15155  df-unif 15156  df-hom 15157  df-cco 15158  df-rest 15264  df-topn 15265  df-0g 15283  df-gsum 15284  df-topgen 15285  df-pt 15286  df-prds 15289  df-xrs 15343  df-qtop 15349  df-imas 15350  df-xps 15353  df-mre 15435  df-mrc 15436  df-acs 15438  df-mgm 16431  df-sgrp 16470  df-mnd 16480  df-submnd 16526  df-mulg 16619  df-cntz 16914  df-cmn 17375  df-psmet 18905  df-xmet 18906  df-met 18907  df-bl 18908  df-mopn 18909  df-fbas 18910  df-fg 18911  df-cnfld 18914  df-top 19863  df-bases 19864  df-topon 19865  df-topsp 19866  df-cld 19976  df-ntr 19977  df-cls 19978  df-nei 20056  df-lp 20094  df-perf 20095  df-cn 20185  df-cnp 20186  df-haus 20273  df-tx 20519  df-hmeo 20712  df-fil 20803  df-fm 20895  df-flim 20896  df-flf 20897  df-xms 21277  df-ms 21278  df-tms 21279  df-cncf 21852  df-limc 22763  df-dv 22764

This theorem is referenced by:  dvsincos  22875  efcn  23340  efcvx  23346  pige3  23414  dvrelog  23524  dvlog  23538  dvcxp1  23622  dvcxp2  23623  dvcncxp1  23625  dvsef  36594  expgrowthi  36595  expgrowth  36597