mullimcf - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mullimcf		Structured version Unicode version

Theorem mullimcf 31875

Description: Limit of the multiplication of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
mullimcf.f
mullimcf.g
mullimcf.h
mullimcf.b	lim
mullimcf.c	lim

**Assertion**
Ref	Expression
mullimcf	lim

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem mullimcf Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		limccl 22496	. . . 4 lim
2		mullimcf.b	. . . 4 lim
3	1, 2	sseldi 3497	. . 3
4		limccl 22496	. . . 4 lim
5		mullimcf.c	. . . 4 lim
6	4, 5	sseldi 3497	. . 3
7	3, 6	mulcld 9633	. 2
8		simpr 461	. . . . 5 $/\$
9	3	adantr 465	. . . . 5 $/\$
10	6	adantr 465	. . . . 5 $/\$
11		mulcn2 13521	. . . . 5 $/\$ $/\$ $/\$
12	8, 9, 10, 11	syl3anc 1228	. . . 4 $/\$ $/\$
13		mullimcf.f	. . . . . . . . . . . . . . . 16
14		fdm 5741	. . . . . . . . . . . . . . . . . 18
15	13, 14	syl 16	. . . . . . . . . . . . . . . . 17
16		limcrcl 22495	. . . . . . . . . . . . . . . . . . 19 lim $/\$ $/\$
17	2, 16	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
18	17	simp2d 1009	. . . . . . . . . . . . . . . . 17
19	15, 18	eqsstr3d 3534	. . . . . . . . . . . . . . . 16
20	17	simp3d 1010	. . . . . . . . . . . . . . . 16
21	13, 19, 20	ellimc3 22500	. . . . . . . . . . . . . . 15 lim $/\$ $/\$
22	2, 21	mpbid 210	. . . . . . . . . . . . . 14 $/\$ $/\$
23	22	simprd 463	. . . . . . . . . . . . 13 $/\$
24	23	r19.21bi 2826	. . . . . . . . . . . 12 $/\$ $/\$
25	24	adantrr 716	. . . . . . . . . . 11 $/\$ $/\$ $/\$
26		mullimcf.g	. . . . . . . . . . . . . . . 16
27	26, 19, 20	ellimc3 22500	. . . . . . . . . . . . . . 15 lim $/\$ $/\$
28	5, 27	mpbid 210	. . . . . . . . . . . . . 14 $/\$ $/\$
29	28	simprd 463	. . . . . . . . . . . . 13 $/\$
30	29	r19.21bi 2826	. . . . . . . . . . . 12 $/\$ $/\$
31	30	adantrl 715	. . . . . . . . . . 11 $/\$ $/\$ $/\$
32		reeanv 3025	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	25, 31, 32	sylanbrc 664	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
34		ifcl 3986	. . . . . . . . . . . . . 14 $/\$
35	34	3ad2ant2 1018	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		nfv 1708	. . . . . . . . . . . . . . 15 $/\$ $/\$
37		nfv 1708	. . . . . . . . . . . . . . 15 $/\$
38		nfra1 2838	. . . . . . . . . . . . . . . 16 $/\$
39		nfra1 2838	. . . . . . . . . . . . . . . 16 $/\$
40	38, 39	nfan 1929	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
41	36, 37, 40	nf3an 1931	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simp11l 1107	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43		simp1rl 1061	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	43	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	42, 44	jca 532	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46		simp12 1027	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47		simp13l 1111	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	45, 46, 47	jca31 534	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		simp1r 1021	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50		simp2 997	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51		simp3l 1024	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52		simplll 759	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
53	52	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54		simp1lr 1060	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		simp3r 1025	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		simp1l 1020	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
57		simp2 997	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
58	19	sselda 3499	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
59	56, 57, 58	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
60	56, 20	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
61	59, 60	subcld 9950	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
62	61	abscld 13370	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
63		rpre 11251	. . . . . . . . . . . . . . . . . . . . . . . 24
64	63	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
65	64	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
66		rpre 11251	. . . . . . . . . . . . . . . . . . . . . . . 24
67	66	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
68	67	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
69	65, 68	ifcld 3987	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
70		simp3 998	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
71		min1 11414	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
72	65, 68, 71	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
73	62, 69, 65, 70, 72	ltletrd 9759	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
74	53, 54, 50, 55, 73	syl211anc 1234	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	51, 74	jca 532	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
76		rsp 2823	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
77	49, 50, 75, 76	syl3c 61	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	48, 77	syld3an1 1274	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
79		simp1l 1020	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	79, 43	jca 532	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81		simp2 997	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
82		simp3r 1025	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83	80, 81, 82	jca31 534	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84		simp1r 1021	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85		simp2 997	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		simp3l 1024	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87		simplll 759	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
88	87	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		simp1lr 1060	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		simp3r 1025	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91		min2 11415	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
92	65, 68, 91	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
93	62, 69, 68, 70, 92	ltletrd 9759	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
94	88, 89, 85, 90, 93	syl211anc 1234	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95	86, 94	jca 532	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		rsp 2823	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
97	84, 85, 95, 96	syl3c 61	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	83, 97	syl3an1 1261	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99	78, 98	jca 532	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	99	3exp 1195	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	41, 100	ralrimi 2857	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		breq2 4460	. . . . . . . . . . . . . . . . 17
103	102	anbi2d 703	. . . . . . . . . . . . . . . 16 $/\$ $/\$
104	103	imbi1d 317	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
105	104	ralbidv 2896	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
106	105	rspcev 3210	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
107	35, 101, 106	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108	107	3exp 1195	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109	108	rexlimdvv 2955	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110	33, 109	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
111	110	adantlr 714	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
112	111	3adant3 1016	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113		nfv 1708	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114		nfra1 2838	. . . . . . . . . . 11 $/\$ $/\$
115	113, 114	nfan 1929	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		simp1l 1020	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
117	116	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118	117	3ad2ant1 1017	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
119		simp2 997	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
120		mullimcf.h	. . . . . . . . . . . . . . . . 17
121	120	a1i 11	. . . . . . . . . . . . . . . 16 $/\$
122		fveq2 5872	. . . . . . . . . . . . . . . . . 18
123		fveq2 5872	. . . . . . . . . . . . . . . . . 18
124	122, 123	oveq12d 6314	. . . . . . . . . . . . . . . . 17
125	124	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$
126		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
127	13	ffvelrnda 6032	. . . . . . . . . . . . . . . . 17 $/\$
128	26	ffvelrnda 6032	. . . . . . . . . . . . . . . . 17 $/\$
129	127, 128	mulcld 9633	. . . . . . . . . . . . . . . 16 $/\$
130	121, 125, 126, 129	fvmptd 5961	. . . . . . . . . . . . . . 15 $/\$
131	130	oveq1d 6311	. . . . . . . . . . . . . 14 $/\$
132	131	fveq2d 5876	. . . . . . . . . . . . 13 $/\$
133	118, 119, 132	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	127, 128	jca 532	. . . . . . . . . . . . . 14 $/\$ $/\$
135	118, 119, 134	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136		simpll3 1037	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
137	136	3ad2ant1 1017	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
138		rsp 2823	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
139	138	3imp 1190	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140	139	3adant1l 1220	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
141		oveq1 6303	. . . . . . . . . . . . . . . . . 18
142	141	fveq2d 5876	. . . . . . . . . . . . . . . . 17
143	142	breq1d 4466	. . . . . . . . . . . . . . . 16
144	143	anbi1d 704	. . . . . . . . . . . . . . 15 $/\$ $/\$
145		oveq1 6303	. . . . . . . . . . . . . . . . . 18
146	145	oveq1d 6311	. . . . . . . . . . . . . . . . 17
147	146	fveq2d 5876	. . . . . . . . . . . . . . . 16
148	147	breq1d 4466	. . . . . . . . . . . . . . 15
149	144, 148	imbi12d 320	. . . . . . . . . . . . . 14 $/\$ $/\$
150		oveq1 6303	. . . . . . . . . . . . . . . . . 18
151	150	fveq2d 5876	. . . . . . . . . . . . . . . . 17
152	151	breq1d 4466	. . . . . . . . . . . . . . . 16
153	152	anbi2d 703	. . . . . . . . . . . . . . 15 $/\$ $/\$
154		oveq2 6304	. . . . . . . . . . . . . . . . . 18
155	154	oveq1d 6311	. . . . . . . . . . . . . . . . 17
156	155	fveq2d 5876	. . . . . . . . . . . . . . . 16
157	156	breq1d 4466	. . . . . . . . . . . . . . 15
158	153, 157	imbi12d 320	. . . . . . . . . . . . . 14 $/\$ $/\$
159	149, 158	rspc2v 3219	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
160	135, 137, 140, 159	syl3c 61	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
161	133, 160	eqbrtrd 4476	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	161	3exp 1195	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	115, 162	ralrimi 2857	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
164	163	ex 434	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
165	164	reximdva 2932	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
166	112, 165	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167	166	3exp 1195	. . . . 5 $/\$ $/\$ $/\$ $/\$
168	167	rexlimdvv 2955	. . . 4 $/\$ $/\$ $/\$
169	12, 168	mpd 15	. . 3 $/\$ $/\$
170	169	ralrimiva 2871	. 2 $/\$
171	13	ffvelrnda 6032	. . . . 5 $/\$
172	26	ffvelrnda 6032	. . . . 5 $/\$
173	171, 172	mulcld 9633	. . . 4 $/\$
174	173, 120	fmptd 6056	. . 3
175	174, 19, 20	ellimc3 22500	. 2 lim $/\$ $/\$
176	7, 170, 175	mpbir2and 922	1 lim

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369 $/\$ w3a 973

wceq 1395

wcel 1819

wne 2652

wral 2807

wrex 2808

wss 3471

cif 3944 class class class wbr 4456

cmpt 4515

cdm 5008

wf 5590

cfv 5594 (class class class)co 6296

cc 9507

cr 9508

cmul 9514

clt 9645

cle 9646

cmin 9824

crp 11245

cabs 13170 lim

climc 22483

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-oadd 7152 df-er 7329 df-map 7440 df-pm 7441 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-fi 7889 df-sup 7919 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-5 10618 df-6 10619 df-7 10620 df-8 10621 df-9 10622 df-10 10623 df-n0 10817 df-z 10886 df-dec 11001 df-uz 11107 df-q 11208 df-rp 11246 df-xneg 11343 df-xadd 11344 df-xmul 11345 df-fz 11698 df-seq 12111 df-exp 12170 df-cj 13035 df-re 13036 df-im 13037 df-sqrt 13171 df-abs 13172 df-struct 14737 df-ndx 14738 df-slot 14739 df-base 14740 df-plusg 14816 df-mulr 14817 df-starv 14818 df-tset 14822 df-ple 14823 df-ds 14825 df-unif 14826 df-rest 14931 df-topn 14932 df-topgen 14952 df-psmet 18629 df-xmet 18630 df-met 18631 df-bl 18632 df-mopn 18633 df-cnfld 18639 df-top 19617 df-bases 19619 df-topon 19620 df-topsp 19621 df-cnp 19947 df-xms 21040 df-ms 21041 df-limc 22487

This theorem is referenced by: fourierdlem101 32236 fourierdlem111 32246

W3C validator