Theorem dvdivbd 37069

Description: A sufficient condition for the derivative to be bounded, for the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
dvdivbd.s	|- ( ph -> S e. { RR , CC } )
dvdivbd.a	|- ( ( ph /\ x e. X ) -> A e. CC )
dvdivbd.adv	|- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> C ) )
dvdivbd.c	|- ( ( ph /\ x e. X ) -> C e. CC )
dvdivbd.b	|- ( ( ph /\ x e. X ) -> B e. CC )
dvdivbd.u	|- ( ph -> U e. RR )
dvdivbd.r	|- ( ph -> R e. RR )
dvdivbd.t	|- ( ph -> T e. RR )
dvdivbd.q	|- ( ph -> Q e. RR )
dvdivbd.cbd	|- ( ( ph /\ x e. X ) -> ( abs ` C ) <_ U )
dvdivbd.bbd	|- ( ( ph /\ x e. X ) -> ( abs ` B ) <_ R )
dvdivbd.dbd	|- ( ( ph /\ x e. X ) -> ( abs ` D ) <_ T )
dvdivbd.abd	|- ( ( ph /\ x e. X ) -> ( abs ` A ) <_ Q )
dvdivbd.bdv	|- ( ph -> ( S _D ( x e. X |-> B ) ) = ( x e. X |-> D ) )
dvdivbd.d	|- ( ( ph /\ x e. X ) -> D e. CC )
dvdivbd.e	|- ( ph -> E e. RR+ )
dvdivbd.ele	|- ( ph -> A. x e. X E <_ ( abs ` B ) )
dvdivbd.f	|- F = ( S _D ( x e. X |-> ( A / B ) ) )

Assertion

Ref	Expression
dvdivbd	|- ( ph -> E. b e. RR A. x e. X ( abs ` ( F ` x ) ) <_ b )

Distinct variable groups:   E, b, x   F, b   Q, b, x   R, b, x   x, S   T, b, x   U, b, x   X, b, x   ph, x

Allowed substitution hints:   ph( b)   A( x, b)   B( x, b)   C( x, b)   D( x, b)   S( b)   F( x)

Proof of Theorem dvdivbd

Step	Hyp	Ref	Expression
1		dvdivbd.u	. . . . 5 |- ( ph -> U e. RR )
2		dvdivbd.r	. . . . 5 |- ( ph -> R e. RR )
3	1, 2	remulcld 9653	. . . 4 |- ( ph -> ( U x. R ) e. RR )
4		dvdivbd.t	. . . . 5 |- ( ph -> T e. RR )
5		dvdivbd.q	. . . . 5 |- ( ph -> Q e. RR )
6	4, 5	remulcld 9653	. . . 4 |- ( ph -> ( T x. Q ) e. RR )
7	3, 6	readdcld 9652	. . 3 |- ( ph -> ( ( U x. R ) + ( T x. Q ) ) e. RR )
8		dvdivbd.e	. . . . 5 |- ( ph -> E e. RR+ )
9	8	rpred 11303	. . . 4 |- ( ph -> E e. RR )
10	9	resqcld 12378	. . 3 |- ( ph -> ( E ^ 2 ) e. RR )
11	8	rpcnd 11305	. . . 4 |- ( ph -> E e. CC )
12	8	rpgt0d 11306	. . . . 5 |- ( ph -> 0 < E )
13	12	gt0ne0d 10156	. . . 4 |- ( ph -> E =/= 0 )
14		2z 10936	. . . . 5 |- 2 e. ZZ
15	14	a1i 11	. . . 4 |- ( ph -> 2 e. ZZ )
16	11, 13, 15	expne0d 12358	. . 3 |- ( ph -> ( E ^ 2 ) =/= 0 )
17	7, 10, 16	redivcld 10412	. 2 |- ( ph -> ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) e. RR )
18		dvdivbd.f	. . . . . . 7 |- F = ( S _D ( x e. X |-> ( A / B ) ) )
19		dvdivbd.s	. . . . . . . 8 |- ( ph -> S e. { RR , CC } )
20		dvdivbd.a	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> A e. CC )
21		dvdivbd.c	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> C e. CC )
22		dvdivbd.adv	. . . . . . . 8 |- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> C ) )
23		dvdivbd.b	. . . . . . . . 9 |- ( ( ph /\ x e. X ) -> B e. CC )
24		simpr 459	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. X ) /\ B = 0 ) -> B = 0 )
25	24	abs00bd 13271	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. X ) /\ B = 0 ) -> ( abs ` B ) = 0 )
26		0red 9626	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. X ) -> 0 e. RR )
27	9	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. X ) -> E e. RR )
28	23	abscld 13414	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. X ) -> ( abs ` B ) e. RR )
29	12	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. X ) -> 0 < E )
30		dvdivbd.ele	. . . . . . . . . . . . . . . 16 |- ( ph -> A. x e. X E <_ ( abs ` B ) )
31	30	r19.21bi 2772	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. X ) -> E <_ ( abs ` B ) )
32	26, 27, 28, 29, 31	ltletrd 9775	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. X ) -> 0 < ( abs ` B ) )
33	32	gt0ne0d 10156	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. X ) -> ( abs ` B ) =/= 0 )
34	33	adantr 463	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. X ) /\ B = 0 ) -> ( abs ` B ) =/= 0 )
35	34	neneqd 2605	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. X ) /\ B = 0 ) -> -. ( abs ` B ) = 0 )
36	25, 35	pm2.65da 574	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> -. B = 0 )
37	36	neqned 2606	. . . . . . . . 9 |- ( ( ph /\ x e. X ) -> B =/= 0 )
38		eldifsn 4096	. . . . . . . . 9 |- ( B e. ( CC \ { 0 } ) <-> ( B e. CC /\ B =/= 0 ) )
39	23, 37, 38	sylanbrc 662	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> B e. ( CC \ { 0 } ) )
40		dvdivbd.d	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> D e. CC )
41		dvdivbd.bdv	. . . . . . . 8 |- ( ph -> ( S _D ( x e. X |-> B ) ) = ( x e. X |-> D ) )
42	19, 20, 21, 22, 39, 40, 41	dvmptdiv 37063	. . . . . . 7 |- ( ph -> ( S _D ( x e. X |-> ( A / B ) ) ) = ( x e. X |-> ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) )
43	18, 42	syl5eq 2455	. . . . . 6 |- ( ph -> F = ( x e. X |-> ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) )
44	21, 23	mulcld 9645	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> ( C x. B ) e. CC )
45	40, 20	mulcld 9645	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> ( D x. A ) e. CC )
46	44, 45	subcld 9966	. . . . . . 7 |- ( ( ph /\ x e. X ) -> ( ( C x. B ) - ( D x. A ) ) e. CC )
47	23	sqcld 12350	. . . . . . 7 |- ( ( ph /\ x e. X ) -> ( B ^ 2 ) e. CC )
48		sqne0 12277	. . . . . . . . 9 |- ( B e. CC -> ( ( B ^ 2 ) =/= 0 <-> B =/= 0 ) )
49	23, 48	syl 17	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> ( ( B ^ 2 ) =/= 0 <-> B =/= 0 ) )
50	37, 49	mpbird 232	. . . . . . 7 |- ( ( ph /\ x e. X ) -> ( B ^ 2 ) =/= 0 )
51	46, 47, 50	divcld 10360	. . . . . 6 |- ( ( ph /\ x e. X ) -> ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) e. CC )
52	43, 51	fvmpt2d 5942	. . . . 5 |- ( ( ph /\ x e. X ) -> ( F ` x ) = ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) )
53	52	fveq2d 5852	. . . 4 |- ( ( ph /\ x e. X ) -> ( abs ` ( F ` x ) ) = ( abs ` ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) )
54	46, 47, 50	absdivd 13433	. . . . 5 |- ( ( ph /\ x e. X ) -> ( abs ` ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) = ( ( abs ` ( ( C x. B ) - ( D x. A ) ) ) / ( abs ` ( B ^ 2 ) ) ) )
55	46	abscld 13414	. . . . . 6 |- ( ( ph /\ x e. X ) -> ( abs ` ( ( C x. B ) - ( D x. A ) ) ) e. RR )
56	7	adantr 463	. . . . . 6 |- ( ( ph /\ x e. X ) -> ( ( U x. R ) + ( T x. Q ) ) e. RR )
57	8	adantr 463	. . . . . . 7 |- ( ( ph /\ x e. X ) -> E e. RR+ )
58	14	a1i 11	. . . . . . 7 |- ( ( ph /\ x e. X ) -> 2 e. ZZ )
59	57, 58	rpexpcld 12375	. . . . . 6 |- ( ( ph /\ x e. X ) -> ( E ^ 2 ) e. RR+ )
60	47	abscld 13414	. . . . . 6 |- ( ( ph /\ x e. X ) -> ( abs ` ( B ^ 2 ) ) e. RR )
61	46	absge0d 13422	. . . . . 6 |- ( ( ph /\ x e. X ) -> 0 <_ ( abs ` ( ( C x. B ) - ( D x. A ) ) ) )
62	44	abscld 13414	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> ( abs ` ( C x. B ) ) e. RR )
63	45	abscld 13414	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> ( abs ` ( D x. A ) ) e. RR )
64	62, 63	readdcld 9652	. . . . . . 7 |- ( ( ph /\ x e. X ) -> ( ( abs ` ( C x. B ) ) + ( abs ` ( D x. A ) ) ) e. RR )
65	44, 45	abs2dif2d 13436	. . . . . . 7 |- ( ( ph /\ x e. X ) -> ( abs ` ( ( C x. B ) - ( D x. A ) ) ) <_ ( ( abs ` ( C x. B ) ) + ( abs ` ( D x. A ) ) ) )
66	3	adantr 463	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> ( U x. R ) e. RR )
67	6	adantr 463	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> ( T x. Q ) e. RR )
68	21, 23	absmuld 13432	. . . . . . . . 9 |- ( ( ph /\ x e. X ) -> ( abs ` ( C x. B ) ) = ( ( abs ` C ) x. ( abs ` B ) ) )
69	21	abscld 13414	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> ( abs ` C ) e. RR )
70	1	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> U e. RR )
71	2	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> R e. RR )
72	21	absge0d 13422	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> 0 <_ ( abs ` C ) )
73	23	absge0d 13422	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> 0 <_ ( abs ` B ) )
74		dvdivbd.cbd	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> ( abs ` C ) <_ U )
75		dvdivbd.bbd	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> ( abs ` B ) <_ R )
76	69, 70, 28, 71, 72, 73, 74, 75	lemul12ad 10527	. . . . . . . . 9 |- ( ( ph /\ x e. X ) -> ( ( abs ` C ) x. ( abs ` B ) ) <_ ( U x. R ) )
77	68, 76	eqbrtrd 4414	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> ( abs ` ( C x. B ) ) <_ ( U x. R ) )
78	40, 20	absmuld 13432	. . . . . . . . 9 |- ( ( ph /\ x e. X ) -> ( abs ` ( D x. A ) ) = ( ( abs ` D ) x. ( abs ` A ) ) )
79	40	abscld 13414	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> ( abs ` D ) e. RR )
80	4	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> T e. RR )
81	20	abscld 13414	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> ( abs ` A ) e. RR )
82	5	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> Q e. RR )
83	40	absge0d 13422	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> 0 <_ ( abs ` D ) )
84	20	absge0d 13422	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> 0 <_ ( abs ` A ) )
85		dvdivbd.dbd	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> ( abs ` D ) <_ T )
86		dvdivbd.abd	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> ( abs ` A ) <_ Q )
87	79, 80, 81, 82, 83, 84, 85, 86	lemul12ad 10527	. . . . . . . . 9 |- ( ( ph /\ x e. X ) -> ( ( abs ` D ) x. ( abs ` A ) ) <_ ( T x. Q ) )
88	78, 87	eqbrtrd 4414	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> ( abs ` ( D x. A ) ) <_ ( T x. Q ) )
89	62, 63, 66, 67, 77, 88	le2addd 10209	. . . . . . 7 |- ( ( ph /\ x e. X ) -> ( ( abs ` ( C x. B ) ) + ( abs ` ( D x. A ) ) ) <_ ( ( U x. R ) + ( T x. Q ) ) )
90	55, 64, 56, 65, 89	letrd 9772	. . . . . 6 |- ( ( ph /\ x e. X ) -> ( abs ` ( ( C x. B ) - ( D x. A ) ) ) <_ ( ( U x. R ) + ( T x. Q ) ) )
91		2nn0 10852	. . . . . . . . 9 |- 2 e. NN0
92	91	a1i 11	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> 2 e. NN0 )
93	26, 27, 29	ltled 9764	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> 0 <_ E )
94		leexp1a 12267	. . . . . . . 8 |- ( ( ( E e. RR /\ ( abs ` B ) e. RR /\ 2 e. NN0 ) /\ ( 0 <_ E /\ E <_ ( abs ` B ) ) ) -> ( E ^ 2 ) <_ ( ( abs ` B ) ^ 2 ) )
95	27, 28, 92, 93, 31, 94	syl32anc 1238	. . . . . . 7 |- ( ( ph /\ x e. X ) -> ( E ^ 2 ) <_ ( ( abs ` B ) ^ 2 ) )
96	23, 92	absexpd 13430	. . . . . . 7 |- ( ( ph /\ x e. X ) -> ( abs ` ( B ^ 2 ) ) = ( ( abs ` B ) ^ 2 ) )
97	95, 96	breqtrrd 4420	. . . . . 6 |- ( ( ph /\ x e. X ) -> ( E ^ 2 ) <_ ( abs ` ( B ^ 2 ) ) )
98	55, 56, 59, 60, 61, 90, 97	lediv12ad 11358	. . . . 5 |- ( ( ph /\ x e. X ) -> ( ( abs ` ( ( C x. B ) - ( D x. A ) ) ) / ( abs ` ( B ^ 2 ) ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) )
99	54, 98	eqbrtrd 4414	. . . 4 |- ( ( ph /\ x e. X ) -> ( abs ` ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) )
100	53, 99	eqbrtrd 4414	. . 3 |- ( ( ph /\ x e. X ) -> ( abs ` ( F ` x ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) )
101	100	ralrimiva 2817	. 2 |- ( ph -> A. x e. X ( abs ` ( F ` x ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) )
102		breq2 4398	. . . 4 |- ( b = ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) -> ( ( abs ` ( F ` x ) ) <_ b <-> ( abs ` ( F ` x ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) ) )
103	102	ralbidv 2842	. . 3 |- ( b = ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) -> ( A. x e. X ( abs ` ( F ` x ) ) <_ b <-> A. x e. X ( abs ` ( F ` x ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) ) )
104	103	rspcev 3159	. 2 |- ( ( ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) e. RR /\ A. x e. X ( abs ` ( F ` x ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) ) -> E. b e. RR A. x e. X ( abs ` ( F ` x ) ) <_ b )
105	17, 101, 104	syl2anc 659	1 |- ( ph -> E. b e. RR A. x e. X ( abs ` ( F ` x ) ) <_ b )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1405   e. wcel 1842   =/= wne 2598   A.wral 2753   E.wrex 2754   \ cdif 3410   {csn 3971   {cpr 3973   class class class wbr 4394   |-> cmpt 4452   ` cfv 5568  (class class class)co 6277   CCcc 9519   RRcr 9520   0cc0 9521   + caddc 9524   x. cmul 9526   < clt 9657   <_ cle 9658   - cmin 9840   / cdiv 10246   2c2 10625   NN0cn0 10835   ZZcz 10904   RR+crp 11264   ^cexp 12208   abscabs 13214   _D cdv 22557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573  ax-inf2 8090  ax-cnex 9577  ax-resscn 9578  ax-1cn 9579  ax-icn 9580  ax-addcl 9581  ax-addrcl 9582  ax-mulcl 9583  ax-mulrcl 9584  ax-mulcom 9585  ax-addass 9586  ax-mulass 9587  ax-distr 9588  ax-i2m1 9589  ax-1ne0 9590  ax-1rid 9591  ax-rnegex 9592  ax-rrecex 9593  ax-cnre 9594  ax-pre-lttri 9595  ax-pre-lttrn 9596  ax-pre-ltadd 9597  ax-pre-mulgt0 9598  ax-pre-sup 9599  ax-addf 9600  ax-mulf 9601

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-int 4227  df-iun 4272  df-iin 4273  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-se 4782  df-we 4783  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-pred 5366  df-ord 5412  df-on 5413  df-lim 5414  df-suc 5415  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-isom 5577  df-riota 6239  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-of 6520  df-om 6683  df-1st 6783  df-2nd 6784  df-supp 6902  df-wrecs 7012  df-recs 7074  df-rdg 7112  df-1o 7166  df-2o 7167  df-oadd 7170  df-er 7347  df-map 7458  df-pm 7459  df-ixp 7507  df-en 7554  df-dom 7555  df-sdom 7556  df-fin 7557  df-fsupp 7863  df-fi 7904  df-sup 7934  df-oi 7968  df-card 8351  df-cda 8579  df-pnf 9659  df-mnf 9660  df-xr 9661  df-ltxr 9662  df-le 9663  df-sub 9842  df-neg 9843  df-div 10247  df-nn 10576  df-2 10634  df-3 10635  df-4 10636  df-5 10637  df-6 10638  df-7 10639  df-8 10640  df-9 10641  df-10 10642  df-n0 10836  df-z 10905  df-dec 11019  df-uz 11127  df-q 11227  df-rp 11265  df-xneg 11370  df-xadd 11371  df-xmul 11372  df-icc 11588  df-fz 11725  df-fzo 11853  df-seq 12150  df-exp 12209  df-hash 12451  df-cj 13079  df-re 13080  df-im 13081  df-sqrt 13215  df-abs 13216  df-struct 14841  df-ndx 14842  df-slot 14843  df-base 14844  df-sets 14845  df-ress 14846  df-plusg 14920  df-mulr 14921  df-starv 14922  df-sca 14923  df-vsca 14924  df-ip 14925  df-tset 14926  df-ple 14927  df-ds 14929  df-unif 14930  df-hom 14931  df-cco 14932  df-rest 15035  df-topn 15036  df-0g 15054  df-gsum 15055  df-topgen 15056  df-pt 15057  df-prds 15060  df-xrs 15114  df-qtop 15119  df-imas 15120  df-xps 15122  df-mre 15198  df-mrc 15199  df-acs 15201  df-mgm 16194  df-sgrp 16233  df-mnd 16243  df-submnd 16289  df-mulg 16382  df-cntz 16677  df-cmn 17122  df-psmet 18729  df-xmet 18730  df-met 18731  df-bl 18732  df-mopn 18733  df-fbas 18734  df-fg 18735  df-cnfld 18739  df-top 19689  df-bases 19691  df-topon 19692  df-topsp 19693  df-cld 19810  df-ntr 19811  df-cls 19812  df-nei 19890  df-lp 19928  df-perf 19929  df-cn 20019  df-cnp 20020  df-t1 20106  df-haus 20107  df-tx 20353  df-hmeo 20546  df-fil 20637  df-fm 20729  df-flim 20730  df-flf 20731  df-xms 21113  df-ms 21114  df-tms 21115  df-cncf 21672  df-limc 22560  df-dv 22561

This theorem is referenced by:  fourierdlem68  37306