Theorem fourierdlem61 31791

Description: Given a differentiable function F, with finite limit of the derivative at A the derived function H has a limit at 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem61.a	|- ( ph -> A e. RR )
fourierdlem61.b	|- ( ph -> B e. RR )
fourierdlem61.altb	|- ( ph -> A < B )
fourierdlem61.f	|- ( ph -> F : ( A (,) B ) --> RR )
fourierdlem61.y	|- ( ph -> Y e. ( F lim CC A ) )
fourierdlem61.g	|- G = ( RR _D F )
fourierdlem61.domg	|- ( ph -> dom G = ( A (,) B ) )
fourierdlem61.e	|- ( ph -> E e. ( G lim CC A ) )
fourierdlem61.h	|- H = ( s e. ( 0 (,) ( B - A ) ) |-> ( ( ( F ` ( A + s ) ) - Y ) / s ) )
fourierdlem61.n	|- N = ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) )
fourierdlem61.d	|- D = ( s e. ( 0 (,) ( B - A ) ) |-> s )

Assertion

Ref	Expression
fourierdlem61	|- ( ph -> E e. ( H lim CC 0 ) )

Distinct variable groups:   A, s   B, s   D, s   E, s   F, s   G, s   N, s   Y, s   ph, s

Allowed substitution hint:   H( s)

Proof of Theorem fourierdlem61

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		0re 9608	. . . 4 |- 0 e. RR
2	1	a1i 11	. . 3 |- ( ph -> 0 e. RR )
3		fourierdlem61.b	. . . . 5 |- ( ph -> B e. RR )
4		fourierdlem61.a	. . . . 5 |- ( ph -> A e. RR )
5	3, 4	resubcld 9999	. . . 4 |- ( ph -> ( B - A ) e. RR )
6	5	rexrd 9655	. . 3 |- ( ph -> ( B - A ) e. RR* )
7		fourierdlem61.altb	. . . 4 |- ( ph -> A < B )
8	4, 3	posdifd 10151	. . . 4 |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
9	7, 8	mpbid 210	. . 3 |- ( ph -> 0 < ( B - A ) )
10		fourierdlem61.f	. . . . . . 7 |- ( ph -> F : ( A (,) B ) --> RR )
11	10	adantr 465	. . . . . 6 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> F : ( A (,) B ) --> RR )
12	4	rexrd 9655	. . . . . . . 8 |- ( ph -> A e. RR* )
13	12	adantr 465	. . . . . . 7 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> A e. RR* )
14	3	rexrd 9655	. . . . . . . 8 |- ( ph -> B e. RR* )
15	14	adantr 465	. . . . . . 7 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> B e. RR* )
16	4	adantr 465	. . . . . . . 8 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> A e. RR )
17		elioore 11571	. . . . . . . . 9 |- ( s e. ( 0 (,) ( B - A ) ) -> s e. RR )
18	17	adantl 466	. . . . . . . 8 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> s e. RR )
19	16, 18	readdcld 9635	. . . . . . 7 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( A + s ) e. RR )
20	4	recnd 9634	. . . . . . . . . . 11 |- ( ph -> A e. CC )
21	20	addid1d 9791	. . . . . . . . . 10 |- ( ph -> ( A + 0 ) = A )
22	21	eqcomd 2475	. . . . . . . . 9 |- ( ph -> A = ( A + 0 ) )
23	22	adantr 465	. . . . . . . 8 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> A = ( A + 0 ) )
24		0xr 9652	. . . . . . . . . . 11 |- 0 e. RR*
25	24	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> 0 e. RR* )
26	6	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( B - A ) e. RR* )
27		simpr 461	. . . . . . . . . 10 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> s e. ( 0 (,) ( B - A ) ) )
28		ioogtlb 31415	. . . . . . . . . 10 |- ( ( 0 e. RR* /\ ( B - A ) e. RR* /\ s e. ( 0 (,) ( B - A ) ) ) -> 0 < s )
29	25, 26, 27, 28	syl3anc 1228	. . . . . . . . 9 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> 0 < s )
30	1	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> 0 e. RR )
31	30, 18, 16	ltadd2d 9749	. . . . . . . . 9 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( 0 < s <-> ( A + 0 ) < ( A + s ) ) )
32	29, 31	mpbid 210	. . . . . . . 8 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( A + 0 ) < ( A + s ) )
33	23, 32	eqbrtrd 4473	. . . . . . 7 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> A < ( A + s ) )
34		iooltub 31435	. . . . . . . . . 10 |- ( ( 0 e. RR* /\ ( B - A ) e. RR* /\ s e. ( 0 (,) ( B - A ) ) ) -> s < ( B - A ) )
35	25, 26, 27, 34	syl3anc 1228	. . . . . . . . 9 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> s < ( B - A ) )
36	5	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( B - A ) e. RR )
37	18, 36, 16	ltadd2d 9749	. . . . . . . . 9 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( s < ( B - A ) <-> ( A + s ) < ( A + ( B - A ) ) ) )
38	35, 37	mpbid 210	. . . . . . . 8 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( A + s ) < ( A + ( B - A ) ) )
39	3	recnd 9634	. . . . . . . . . 10 |- ( ph -> B e. CC )
40	20, 39	pncan3d 9945	. . . . . . . . 9 |- ( ph -> ( A + ( B - A ) ) = B )
41	40	adantr 465	. . . . . . . 8 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( A + ( B - A ) ) = B )
42	38, 41	breqtrd 4477	. . . . . . 7 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( A + s ) < B )
43	13, 15, 19, 33, 42	eliood 31418	. . . . . 6 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( A + s ) e. ( A (,) B ) )
44	11, 43	ffvelrnd 6033	. . . . 5 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( F ` ( A + s ) ) e. RR )
45		ioossre 11598	. . . . . . . . 9 |- ( A (,) B ) C_ RR
46	45	a1i 11	. . . . . . . 8 |- ( ph -> ( A (,) B ) C_ RR )
47		ax-resscn 9561	. . . . . . . 8 |- RR C_ CC
48	46, 47	syl6ss 3521	. . . . . . 7 |- ( ph -> ( A (,) B ) C_ CC )
49		eqid 2467	. . . . . . . 8 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
50	49, 14, 4, 7	lptioo1cn 31511	. . . . . . 7 |- ( ph -> A e. ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( A (,) B ) ) )
51		fourierdlem61.y	. . . . . . 7 |- ( ph -> Y e. ( F lim CC A ) )
52	10, 48, 50, 51	limcrecl 31494	. . . . . 6 |- ( ph -> Y e. RR )
53	52	adantr 465	. . . . 5 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> Y e. RR )
54	44, 53	resubcld 9999	. . . 4 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( ( F ` ( A + s ) ) - Y ) e. RR )
55		fourierdlem61.n	. . . 4 |- N = ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) )
56	54, 55	fmptd 6056	. . 3 |- ( ph -> N : ( 0 (,) ( B - A ) ) --> RR )
57		fourierdlem61.d	. . . 4 |- D = ( s e. ( 0 (,) ( B - A ) ) |-> s )
58	18, 57	fmptd 6056	. . 3 |- ( ph -> D : ( 0 (,) ( B - A ) ) --> RR )
59	55	oveq2i 6306	. . . . . 6 |- ( RR _D N ) = ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) ) )
60	59	a1i 11	. . . . 5 |- ( ph -> ( RR _D N ) = ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) ) ) )
61	60	dmeqd 5211	. . . 4 |- ( ph -> dom ( RR _D N ) = dom ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) ) ) )
62		reex 9595	. . . . . . . . 9 |- RR e. _V
63	62	prid1 4141	. . . . . . . 8 |- RR e. { RR , CC }
64	63	a1i 11	. . . . . . 7 |- ( ph -> RR e. { RR , CC } )
65	44	recnd 9634	. . . . . . 7 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( F ` ( A + s ) ) e. CC )
66		dvfre 22222	. . . . . . . . . . 11 |- ( ( F : ( A (,) B ) --> RR /\ ( A (,) B ) C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
67	10, 46, 66	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
68		fourierdlem61.g	. . . . . . . . . . . 12 |- G = ( RR _D F )
69	68	a1i 11	. . . . . . . . . . 11 |- ( ph -> G = ( RR _D F ) )
70		feq1 5719	. . . . . . . . . . 11 |- ( G = ( RR _D F ) -> ( G : dom ( RR _D F ) --> RR <-> ( RR _D F ) : dom ( RR _D F ) --> RR ) )
71	69, 70	syl 16	. . . . . . . . . 10 |- ( ph -> ( G : dom ( RR _D F ) --> RR <-> ( RR _D F ) : dom ( RR _D F ) --> RR ) )
72	67, 71	mpbird 232	. . . . . . . . 9 |- ( ph -> G : dom ( RR _D F ) --> RR )
73	72	adantr 465	. . . . . . . 8 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> G : dom ( RR _D F ) --> RR )
74	69	eqcomd 2475	. . . . . . . . . . . 12 |- ( ph -> ( RR _D F ) = G )
75		dmeq 5209	. . . . . . . . . . . 12 |- ( ( RR _D F ) = G -> dom ( RR _D F ) = dom G )
76	74, 75	syl 16	. . . . . . . . . . 11 |- ( ph -> dom ( RR _D F ) = dom G )
77		fourierdlem61.domg	. . . . . . . . . . 11 |- ( ph -> dom G = ( A (,) B ) )
78	76, 77	eqtr2d 2509	. . . . . . . . . 10 |- ( ph -> ( A (,) B ) = dom ( RR _D F ) )
79	78	adantr 465	. . . . . . . . 9 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( A (,) B ) = dom ( RR _D F ) )
80	43, 79	eleqtrd 2557	. . . . . . . 8 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( A + s ) e. dom ( RR _D F ) )
81	73, 80	ffvelrnd 6033	. . . . . . 7 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( G ` ( A + s ) ) e. RR )
82		1re 9607	. . . . . . . . . 10 |- 1 e. RR
83	82	a1i 11	. . . . . . . . 9 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> 1 e. RR )
84	47	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ x e. ( A (,) B ) ) -> RR C_ CC )
85	10	ffvelrnda 6032	. . . . . . . . . 10 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. RR )
86	84, 85	sseldd 3510	. . . . . . . . 9 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
87		feq2 5720	. . . . . . . . . . . 12 |- ( ( A (,) B ) = dom ( RR _D F ) -> ( G : ( A (,) B ) --> RR <-> G : dom ( RR _D F ) --> RR ) )
88	78, 87	syl 16	. . . . . . . . . . 11 |- ( ph -> ( G : ( A (,) B ) --> RR <-> G : dom ( RR _D F ) --> RR ) )
89	72, 88	mpbird 232	. . . . . . . . . 10 |- ( ph -> G : ( A (,) B ) --> RR )
90	89	ffvelrnda 6032	. . . . . . . . 9 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( G ` x ) e. RR )
91	20	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> A e. CC )
92	20	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ s e. RR ) -> A e. CC )
93	1	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ s e. RR ) -> 0 e. RR )
94	64, 20	dvmptc 22229	. . . . . . . . . . . 12 |- ( ph -> ( RR _D ( s e. RR |-> A ) ) = ( s e. RR |-> 0 ) )
95		ioossre 11598	. . . . . . . . . . . . 13 |- ( 0 (,) ( B - A ) ) C_ RR
96	95	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( 0 (,) ( B - A ) ) C_ RR )
97	49	tgioo2 21176	. . . . . . . . . . . 12 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
98		iooretop 21141	. . . . . . . . . . . . 13 |- ( 0 (,) ( B - A ) ) e. ( topGen ` ran (,) )
99	98	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( 0 (,) ( B - A ) ) e. ( topGen ` ran (,) ) )
100	64, 92, 93, 94, 96, 97, 49, 99	dvmptres 22234	. . . . . . . . . . 11 |- ( ph -> ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> A ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> 0 ) )
101	47, 18	sseldi 3507	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> s e. CC )
102	47	sseli 3505	. . . . . . . . . . . . 13 |- ( s e. RR -> s e. CC )
103	102	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ s e. RR ) -> s e. CC )
104	82	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ s e. RR ) -> 1 e. RR )
105	64	dvmptid 22228	. . . . . . . . . . . 12 |- ( ph -> ( RR _D ( s e. RR |-> s ) ) = ( s e. RR |-> 1 ) )
106	64, 103, 104, 105, 96, 97, 49, 99	dvmptres 22234	. . . . . . . . . . 11 |- ( ph -> ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> s ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> 1 ) )
107	64, 91, 30, 100, 101, 83, 106	dvmptadd 22231	. . . . . . . . . 10 |- ( ph -> ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> ( A + s ) ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( 0 + 1 ) ) )
108		0p1e1 10659	. . . . . . . . . . . . 13 |- ( 0 + 1 ) = 1
109	108	a1i 11	. . . . . . . . . . . 12 |- ( s e. ( 0 (,) ( B - A ) ) -> ( 0 + 1 ) = 1 )
110	109	mpteq2ia 4535	. . . . . . . . . . 11 |- ( s e. ( 0 (,) ( B - A ) ) |-> ( 0 + 1 ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> 1 )
111	110	a1i 11	. . . . . . . . . 10 |- ( ph -> ( s e. ( 0 (,) ( B - A ) ) |-> ( 0 + 1 ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> 1 ) )
112	107, 111	eqtrd 2508	. . . . . . . . 9 |- ( ph -> ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> ( A + s ) ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> 1 ) )
113	10	feqmptd 5927	. . . . . . . . . . . 12 |- ( ph -> F = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
114	113	eqcomd 2475	. . . . . . . . . . 11 |- ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) = F )
115	114	oveq2d 6311	. . . . . . . . . 10 |- ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( F ` x ) ) ) = ( RR _D F ) )
116	89	feqmptd 5927	. . . . . . . . . 10 |- ( ph -> G = ( x e. ( A (,) B ) |-> ( G ` x ) ) )
117	115, 74, 116	3eqtrd 2512	. . . . . . . . 9 |- ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( F ` x ) ) ) = ( x e. ( A (,) B ) |-> ( G ` x ) ) )
118		fveq2 5872	. . . . . . . . 9 |- ( x = ( A + s ) -> ( F ` x ) = ( F ` ( A + s ) ) )
119		fveq2 5872	. . . . . . . . 9 |- ( x = ( A + s ) -> ( G ` x ) = ( G ` ( A + s ) ) )
120	64, 64, 43, 83, 86, 90, 112, 117, 118, 119	dvmptco 22243	. . . . . . . 8 |- ( ph -> ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> ( F ` ( A + s ) ) ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( ( G ` ( A + s ) ) x. 1 ) ) )
121	47, 81	sseldi 3507	. . . . . . . . . 10 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( G ` ( A + s ) ) e. CC )
122	121	mulid1d 9625	. . . . . . . . 9 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( ( G ` ( A + s ) ) x. 1 ) = ( G ` ( A + s ) ) )
123	122	mpteq2dva 4539	. . . . . . . 8 |- ( ph -> ( s e. ( 0 (,) ( B - A ) ) |-> ( ( G ` ( A + s ) ) x. 1 ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) )
124	120, 123	eqtrd 2508	. . . . . . 7 |- ( ph -> ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> ( F ` ( A + s ) ) ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) )
125		limccl 22147	. . . . . . . . 9 |- ( F lim CC A ) C_ CC
126	125, 51	sseldi 3507	. . . . . . . 8 |- ( ph -> Y e. CC )
127	126	adantr 465	. . . . . . 7 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> Y e. CC )
128		eqidd 2468	. . . . . . . 8 |- ( ph -> ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> Y ) ) = ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> Y ) ) )
129	126	adantr 465	. . . . . . . . 9 |- ( ( ph /\ s e. RR ) -> Y e. CC )
130	64, 126	dvmptc 22229	. . . . . . . . 9 |- ( ph -> ( RR _D ( s e. RR |-> Y ) ) = ( s e. RR |-> 0 ) )
131	64, 129, 93, 130, 96, 97, 49, 99	dvmptres 22234	. . . . . . . 8 |- ( ph -> ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> Y ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> 0 ) )
132	128, 131	eqtrd 2508	. . . . . . 7 |- ( ph -> ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> Y ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> 0 ) )
133	64, 65, 81, 124, 127, 30, 132	dvmptsub 22238	. . . . . 6 |- ( ph -> ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( ( G ` ( A + s ) ) - 0 ) ) )
134	121	subid1d 9931	. . . . . . 7 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( ( G ` ( A + s ) ) - 0 ) = ( G ` ( A + s ) ) )
135	134	mpteq2dva 4539	. . . . . 6 |- ( ph -> ( s e. ( 0 (,) ( B - A ) ) |-> ( ( G ` ( A + s ) ) - 0 ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) )
136	133, 135	eqtrd 2508	. . . . 5 |- ( ph -> ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) )
137	136	dmeqd 5211	. . . 4 |- ( ph -> dom ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) ) ) = dom ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) )
138	81	ralrimiva 2881	. . . . 5 |- ( ph -> A. s e. ( 0 (,) ( B - A ) ) ( G ` ( A + s ) ) e. RR )
139		dmmptg 5510	. . . . 5 |- ( A. s e. ( 0 (,) ( B - A ) ) ( G ` ( A + s ) ) e. RR -> dom ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) = ( 0 (,) ( B - A ) ) )
140	138, 139	syl 16	. . . 4 |- ( ph -> dom ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) = ( 0 (,) ( B - A ) ) )
141	61, 137, 140	3eqtrd 2512	. . 3 |- ( ph -> dom ( RR _D N ) = ( 0 (,) ( B - A ) ) )
142	57	a1i 11	. . . . . . 7 |- ( ph -> D = ( s e. ( 0 (,) ( B - A ) ) |-> s ) )
143	142	oveq2d 6311	. . . . . 6 |- ( ph -> ( RR _D D ) = ( RR _D ( s e. ( 0 (,) ( B - A ) ) |-> s ) ) )
144	143, 106	eqtrd 2508	. . . . 5 |- ( ph -> ( RR _D D ) = ( s e. ( 0 (,) ( B - A ) ) |-> 1 ) )
145	144	dmeqd 5211	. . . 4 |- ( ph -> dom ( RR _D D ) = dom ( s e. ( 0 (,) ( B - A ) ) |-> 1 ) )
146	83	ralrimiva 2881	. . . . 5 |- ( ph -> A. s e. ( 0 (,) ( B - A ) ) 1 e. RR )
147		dmmptg 5510	. . . . 5 |- ( A. s e. ( 0 (,) ( B - A ) ) 1 e. RR -> dom ( s e. ( 0 (,) ( B - A ) ) |-> 1 ) = ( 0 (,) ( B - A ) ) )
148	146, 147	syl 16	. . . 4 |- ( ph -> dom ( s e. ( 0 (,) ( B - A ) ) |-> 1 ) = ( 0 (,) ( B - A ) ) )
149	145, 148	eqtrd 2508	. . 3 |- ( ph -> dom ( RR _D D ) = ( 0 (,) ( B - A ) ) )
150	126	subidd 9930	. . . . . 6 |- ( ph -> ( Y - Y ) = 0 )
151	150	eqcomd 2475	. . . . 5 |- ( ph -> 0 = ( Y - Y ) )
152		eqid 2467	. . . . . 6 |- ( s e. ( 0 (,) ( B - A ) ) |-> ( F ` ( A + s ) ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( F ` ( A + s ) ) )
153		eqid 2467	. . . . . 6 |- ( s e. ( 0 (,) ( B - A ) ) |-> Y ) = ( s e. ( 0 (,) ( B - A ) ) |-> Y )
154		eqid 2467	. . . . . 6 |- ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) )
155	43	adantrr 716	. . . . . . 7 |- ( ( ph /\ ( s e. ( 0 (,) ( B - A ) ) /\ ( A + s ) =/= A ) ) -> ( A + s ) e. ( A (,) B ) )
156		eqid 2467	. . . . . . . . 9 |- ( s e. ( 0 (,) ( B - A ) ) |-> A ) = ( s e. ( 0 (,) ( B - A ) ) |-> A )
157		eqid 2467	. . . . . . . . 9 |- ( s e. ( 0 (,) ( B - A ) ) |-> s ) = ( s e. ( 0 (,) ( B - A ) ) |-> s )
158		eqid 2467	. . . . . . . . 9 |- ( s e. ( 0 (,) ( B - A ) ) |-> ( A + s ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( A + s ) )
159	96, 47	syl6ss 3521	. . . . . . . . . 10 |- ( ph -> ( 0 (,) ( B - A ) ) C_ CC )
160	47, 2	sseldi 3507	. . . . . . . . . 10 |- ( ph -> 0 e. CC )
161	156, 159, 20, 160	constlimc 31489	. . . . . . . . 9 |- ( ph -> A e. ( ( s e. ( 0 (,) ( B - A ) ) |-> A ) lim CC 0 ) )
162	159, 157, 160	idlimc 31491	. . . . . . . . 9 |- ( ph -> 0 e. ( ( s e. ( 0 (,) ( B - A ) ) |-> s ) lim CC 0 ) )
163	156, 157, 158, 91, 101, 161, 162	addlimc 31513	. . . . . . . 8 |- ( ph -> ( A + 0 ) e. ( ( s e. ( 0 (,) ( B - A ) ) |-> ( A + s ) ) lim CC 0 ) )
164	22, 163	eqeltrd 2555	. . . . . . 7 |- ( ph -> A e. ( ( s e. ( 0 (,) ( B - A ) ) |-> ( A + s ) ) lim CC 0 ) )
165	113	oveq1d 6310	. . . . . . . 8 |- ( ph -> ( F lim CC A ) = ( ( x e. ( A (,) B ) |-> ( F ` x ) ) lim CC A ) )
166	51, 165	eleqtrd 2557	. . . . . . 7 |- ( ph -> Y e. ( ( x e. ( A (,) B ) |-> ( F ` x ) ) lim CC A ) )
167		simplrr 760	. . . . . . . 8 |- ( ( ( ph /\ ( s e. ( 0 (,) ( B - A ) ) /\ ( A + s ) = A ) ) /\ -. ( F ` ( A + s ) ) = Y ) -> ( A + s ) = A )
168	16, 33	gtned 9731	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( A + s ) =/= A )
169	168	neneqd 2669	. . . . . . . . . 10 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> -. ( A + s ) = A )
170	169	adantrr 716	. . . . . . . . 9 |- ( ( ph /\ ( s e. ( 0 (,) ( B - A ) ) /\ ( A + s ) = A ) ) -> -. ( A + s ) = A )
171	170	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ ( s e. ( 0 (,) ( B - A ) ) /\ ( A + s ) = A ) ) /\ -. ( F ` ( A + s ) ) = Y ) -> -. ( A + s ) = A )
172	167, 171	condan 792	. . . . . . 7 |- ( ( ph /\ ( s e. ( 0 (,) ( B - A ) ) /\ ( A + s ) = A ) ) -> ( F ` ( A + s ) ) = Y )
173	155, 86, 164, 166, 118, 172	limcco 22165	. . . . . 6 |- ( ph -> Y e. ( ( s e. ( 0 (,) ( B - A ) ) |-> ( F ` ( A + s ) ) ) lim CC 0 ) )
174	153, 159, 126, 160	constlimc 31489	. . . . . 6 |- ( ph -> Y e. ( ( s e. ( 0 (,) ( B - A ) ) |-> Y ) lim CC 0 ) )
175	152, 153, 154, 65, 127, 173, 174	sublimc 31517	. . . . 5 |- ( ph -> ( Y - Y ) e. ( ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) ) lim CC 0 ) )
176	151, 175	eqeltrd 2555	. . . 4 |- ( ph -> 0 e. ( ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) ) lim CC 0 ) )
177	55	eqcomi 2480	. . . . . 6 |- ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) ) = N
178	177	oveq1i 6305	. . . . 5 |- ( ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) ) lim CC 0 ) = ( N lim CC 0 )
179	178	a1i 11	. . . 4 |- ( ph -> ( ( s e. ( 0 (,) ( B - A ) ) |-> ( ( F ` ( A + s ) ) - Y ) ) lim CC 0 ) = ( N lim CC 0 ) )
180	176, 179	eleqtrd 2557	. . 3 |- ( ph -> 0 e. ( N lim CC 0 ) )
181	159, 57, 160	idlimc 31491	. . 3 |- ( ph -> 0 e. ( D lim CC 0 ) )
182		lbioo 11572	. . . . 5 |- -. 0 e. ( 0 (,) ( B - A ) )
183	182	a1i 11	. . . 4 |- ( ph -> -. 0 e. ( 0 (,) ( B - A ) ) )
184		mptresid 5334	. . . . . . . . 9 |- ( s e. ( 0 (,) ( B - A ) ) |-> s ) = ( _I |` ( 0 (,) ( B - A ) ) )
185	184	a1i 11	. . . . . . . 8 |- ( ph -> ( s e. ( 0 (,) ( B - A ) ) |-> s ) = ( _I |` ( 0 (,) ( B - A ) ) ) )
186	142, 185	eqtrd 2508	. . . . . . 7 |- ( ph -> D = ( _I |` ( 0 (,) ( B - A ) ) ) )
187	186	rneqd 5236	. . . . . 6 |- ( ph -> ran D = ran ( _I |` ( 0 (,) ( B - A ) ) ) )
188		rnresi 5356	. . . . . . 7 |- ran ( _I |` ( 0 (,) ( B - A ) ) ) = ( 0 (,) ( B - A ) )
189	188	a1i 11	. . . . . 6 |- ( ph -> ran ( _I |` ( 0 (,) ( B - A ) ) ) = ( 0 (,) ( B - A ) ) )
190	187, 189	eqtrd 2508	. . . . 5 |- ( ph -> ran D = ( 0 (,) ( B - A ) ) )
191	190	eqcomd 2475	. . . 4 |- ( ph -> ( 0 (,) ( B - A ) ) = ran D )
192	183, 191	neleqtrd 2579	. . 3 |- ( ph -> -. 0 e. ran D )
193		ax-1ne0 9573	. . . . . . . 8 |- 1 =/= 0
194	193	necomi 2737	. . . . . . 7 |- 0 =/= 1
195		neneq 31334	. . . . . . 7 |- ( 0 =/= 1 -> -. 0 = 1 )
196	194, 195	ax-mp 5	. . . . . 6 |- -. 0 = 1
197	196	a1i 11	. . . . 5 |- ( ph -> -. 0 = 1 )
198		elsncg 4056	. . . . . 6 |- ( 0 e. RR -> ( 0 e. { 1 } <-> 0 = 1 ) )
199	2, 198	syl 16	. . . . 5 |- ( ph -> ( 0 e. { 1 } <-> 0 = 1 ) )
200	197, 199	mtbird 301	. . . 4 |- ( ph -> -. 0 e. { 1 } )
201	144	rneqd 5236	. . . . 5 |- ( ph -> ran ( RR _D D ) = ran ( s e. ( 0 (,) ( B - A ) ) |-> 1 ) )
202		eqid 2467	. . . . . 6 |- ( s e. ( 0 (,) ( B - A ) ) |-> 1 ) = ( s e. ( 0 (,) ( B - A ) ) |-> 1 )
203	24	a1i 11	. . . . . . . 8 |- ( ph -> 0 e. RR* )
204		ioon0 11567	. . . . . . . 8 |- ( ( 0 e. RR* /\ ( B - A ) e. RR* ) -> ( ( 0 (,) ( B - A ) ) =/= (/) <-> 0 < ( B - A ) ) )
205	203, 6, 204	syl2anc 661	. . . . . . 7 |- ( ph -> ( ( 0 (,) ( B - A ) ) =/= (/) <-> 0 < ( B - A ) ) )
206	9, 205	mpbird 232	. . . . . 6 |- ( ph -> ( 0 (,) ( B - A ) ) =/= (/) )
207	202, 83, 206	rnmptc 31350	. . . . 5 |- ( ph -> ran ( s e. ( 0 (,) ( B - A ) ) |-> 1 ) = { 1 } )
208	201, 207	eqtr2d 2509	. . . 4 |- ( ph -> { 1 } = ran ( RR _D D ) )
209	200, 208	neleqtrd 2579	. . 3 |- ( ph -> -. 0 e. ran ( RR _D D ) )
210	47, 90	sseldi 3507	. . . . 5 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( G ` x ) e. CC )
211		fourierdlem61.e	. . . . . 6 |- ( ph -> E e. ( G lim CC A ) )
212	116	oveq1d 6310	. . . . . 6 |- ( ph -> ( G lim CC A ) = ( ( x e. ( A (,) B ) |-> ( G ` x ) ) lim CC A ) )
213	211, 212	eleqtrd 2557	. . . . 5 |- ( ph -> E e. ( ( x e. ( A (,) B ) |-> ( G ` x ) ) lim CC A ) )
214		simplrr 760	. . . . . 6 |- ( ( ( ph /\ ( s e. ( 0 (,) ( B - A ) ) /\ ( A + s ) = A ) ) /\ -. ( G ` ( A + s ) ) = E ) -> ( A + s ) = A )
215	170	adantr 465	. . . . . 6 |- ( ( ( ph /\ ( s e. ( 0 (,) ( B - A ) ) /\ ( A + s ) = A ) ) /\ -. ( G ` ( A + s ) ) = E ) -> -. ( A + s ) = A )
216	214, 215	condan 792	. . . . 5 |- ( ( ph /\ ( s e. ( 0 (,) ( B - A ) ) /\ ( A + s ) = A ) ) -> ( G ` ( A + s ) ) = E )
217	155, 210, 164, 213, 119, 216	limcco 22165	. . . 4 |- ( ph -> E e. ( ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) lim CC 0 ) )
218	121	div1d 10324	. . . . . . . 8 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( ( G ` ( A + s ) ) / 1 ) = ( G ` ( A + s ) ) )
219	218	eqcomd 2475	. . . . . . 7 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( G ` ( A + s ) ) = ( ( G ` ( A + s ) ) / 1 ) )
220		eqid 2467	. . . . . . . . . . . 12 |- ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) )
221	220	fvmpt2 5964	. . . . . . . . . . 11 |- ( ( s e. ( 0 (,) ( B - A ) ) /\ ( G ` ( A + s ) ) e. RR ) -> ( ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) ` s ) = ( G ` ( A + s ) ) )
222	27, 81, 221	syl2anc 661	. . . . . . . . . 10 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) ` s ) = ( G ` ( A + s ) ) )
223	222	eqcomd 2475	. . . . . . . . 9 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( G ` ( A + s ) ) = ( ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) ` s ) )
224	60, 136	eqtr2d 2509	. . . . . . . . . . . . 13 |- ( ph -> ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) = ( RR _D N ) )
225	224	eqcomd 2475	. . . . . . . . . . . 12 |- ( ph -> ( RR _D N ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) )
226	225	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( RR _D N ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) )
227	226	fveq1d 5874	. . . . . . . . . 10 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( ( RR _D N ) ` s ) = ( ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) ` s ) )
228	227, 222, 223	3eqtrrd 2513	. . . . . . . . 9 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) ` s ) = ( ( RR _D N ) ` s ) )
229	223, 228	eqtrd 2508	. . . . . . . 8 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( G ` ( A + s ) ) = ( ( RR _D N ) ` s ) )
230	144	fveq1d 5874	. . . . . . . . . 10 |- ( ph -> ( ( RR _D D ) ` s ) = ( ( s e. ( 0 (,) ( B - A ) ) |-> 1 ) ` s ) )
231	230	adantr 465	. . . . . . . . 9 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( ( RR _D D ) ` s ) = ( ( s e. ( 0 (,) ( B - A ) ) |-> 1 ) ` s ) )
232	202	fvmpt2 5964	. . . . . . . . . 10 |- ( ( s e. ( 0 (,) ( B - A ) ) /\ 1 e. RR ) -> ( ( s e. ( 0 (,) ( B - A ) ) |-> 1 ) ` s ) = 1 )
233	27, 83, 232	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( ( s e. ( 0 (,) ( B - A ) ) |-> 1 ) ` s ) = 1 )
234	231, 233	eqtr2d 2509	. . . . . . . 8 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> 1 = ( ( RR _D D ) ` s ) )
235	229, 234	oveq12d 6313	. . . . . . 7 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( ( G ` ( A + s ) ) / 1 ) = ( ( ( RR _D N ) ` s ) / ( ( RR _D D ) ` s ) ) )
236		eqidd 2468	. . . . . . 7 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( ( ( RR _D N ) ` s ) / ( ( RR _D D ) ` s ) ) = ( ( ( RR _D N ) ` s ) / ( ( RR _D D ) ` s ) ) )
237	219, 235, 236	3eqtrd 2512	. . . . . 6 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( G ` ( A + s ) ) = ( ( ( RR _D N ) ` s ) / ( ( RR _D D ) ` s ) ) )
238	237	mpteq2dva 4539	. . . . 5 |- ( ph -> ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( ( ( RR _D N ) ` s ) / ( ( RR _D D ) ` s ) ) ) )
239	238	oveq1d 6310	. . . 4 |- ( ph -> ( ( s e. ( 0 (,) ( B - A ) ) |-> ( G ` ( A + s ) ) ) lim CC 0 ) = ( ( s e. ( 0 (,) ( B - A ) ) |-> ( ( ( RR _D N ) ` s ) / ( ( RR _D D ) ` s ) ) ) lim CC 0 ) )
240	217, 239	eleqtrd 2557	. . 3 |- ( ph -> E e. ( ( s e. ( 0 (,) ( B - A ) ) |-> ( ( ( RR _D N ) ` s ) / ( ( RR _D D ) ` s ) ) ) lim CC 0 ) )
241	2, 6, 9, 56, 58, 141, 149, 180, 181, 192, 209, 240	lhop1 22283	. 2 |- ( ph -> E e. ( ( s e. ( 0 (,) ( B - A ) ) |-> ( ( N ` s ) / ( D ` s ) ) ) lim CC 0 ) )
242		fourierdlem61.h	. . . . 5 |- H = ( s e. ( 0 (,) ( B - A ) ) |-> ( ( ( F ` ( A + s ) ) - Y ) / s ) )
243	242	a1i 11	. . . 4 |- ( ph -> H = ( s e. ( 0 (,) ( B - A ) ) |-> ( ( ( F ` ( A + s ) ) - Y ) / s ) ) )
244		eqidd 2468	. . . 4 |- ( ph -> ( s e. ( 0 (,) ( B - A ) ) |-> ( ( ( F ` ( A + s ) ) - Y ) / s ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( ( ( F ` ( A + s ) ) - Y ) / s ) ) )
245	55	fvmpt2 5964	. . . . . . . 8 |- ( ( s e. ( 0 (,) ( B - A ) ) /\ ( ( F ` ( A + s ) ) - Y ) e. RR ) -> ( N ` s ) = ( ( F ` ( A + s ) ) - Y ) )
246	27, 54, 245	syl2anc 661	. . . . . . 7 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( N ` s ) = ( ( F ` ( A + s ) ) - Y ) )
247	57	fvmpt2 5964	. . . . . . . 8 |- ( ( s e. ( 0 (,) ( B - A ) ) /\ s e. ( 0 (,) ( B - A ) ) ) -> ( D ` s ) = s )
248	27, 27, 247	syl2anc 661	. . . . . . 7 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( D ` s ) = s )
249	246, 248	oveq12d 6313	. . . . . 6 |- ( ( ph /\ s e. ( 0 (,) ( B - A ) ) ) -> ( ( N ` s ) / ( D ` s ) ) = ( ( ( F ` ( A + s ) ) - Y ) / s ) )
250	249	mpteq2dva 4539	. . . . 5 |- ( ph -> ( s e. ( 0 (,) ( B - A ) ) |-> ( ( N ` s ) / ( D ` s ) ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( ( ( F ` ( A + s ) ) - Y ) / s ) ) )
251	250	eqcomd 2475	. . . 4 |- ( ph -> ( s e. ( 0 (,) ( B - A ) ) |-> ( ( ( F ` ( A + s ) ) - Y ) / s ) ) = ( s e. ( 0 (,) ( B - A ) ) |-> ( ( N ` s ) / ( D ` s ) ) ) )
252	243, 244, 251	3eqtrrd 2513	. . 3 |- ( ph -> ( s e. ( 0 (,) ( B - A ) ) |-> ( ( N ` s ) / ( D ` s ) ) ) = H )
253	252	oveq1d 6310	. 2 |- ( ph -> ( ( s e. ( 0 (,) ( B - A ) ) |-> ( ( N ` s ) / ( D ` s ) ) ) lim CC 0 ) = ( H lim CC 0 ) )
254	241, 253	eleqtrd 2557	1 |- ( ph -> E e. ( H lim CC 0 ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2817   C_ wss 3481   (/)c0 3790   {csn 4033   {cpr 4035   class class class wbr 4453   |-> cmpt 4511   _I cid 4796   dom cdm 5005   ran crn 5006   |` cres 5007   -->wf 5590   ` cfv 5594  (class class class)co 6295   CCcc 9502   RRcr 9503   0cc0 9504   1c1 9505   + caddc 9507   x. cmul 9509   RR*cxr 9639   < clt 9640   - cmin 9817   / cdiv 10218   (,)cioo 11541   TopOpenctopn 14694   topGenctg 14710  ℂ_fldccnfld 18290   lim CC climc 22134   _D cdv 22135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581  ax-pre-sup 9582  ax-addf 9583  ax-mulf 9584

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-iin 4334  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  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-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-of 6535  df-om 6696  df-1st 6795  df-2nd 6796  df-supp 6914  df-recs 7054  df-rdg 7088  df-1o 7142  df-2o 7143  df-oadd 7146  df-er 7323  df-map 7434  df-pm 7435  df-ixp 7482  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-fsupp 7842  df-fi 7883  df-sup 7913  df-oi 7947  df-card 8332  df-cda 8560  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-div 10219  df-nn 10549  df-2 10606  df-3 10607  df-4 10608  df-5 10609  df-6 10610  df-7 10611  df-8 10612  df-9 10613  df-10 10614  df-n0 10808  df-z 10877  df-dec 10989  df-uz 11095  df-q 11195  df-rp 11233  df-xneg 11330  df-xadd 11331  df-xmul 11332  df-ioo 11545  df-ioc 11546  df-ico 11547  df-icc 11548  df-fz 11685  df-fzo 11805  df-seq 12088  df-exp 12147  df-hash 12386  df-cj 12912  df-re 12913  df-im 12914  df-sqrt 13048  df-abs 13049  df-struct 14509  df-ndx 14510  df-slot 14511  df-base 14512  df-sets 14513  df-ress 14514  df-plusg 14585  df-mulr 14586  df-starv 14587  df-sca 14588  df-vsca 14589  df-ip 14590  df-tset 14591  df-ple 14592  df-ds 14594  df-unif 14595  df-hom 14596  df-cco 14597  df-rest 14695  df-topn 14696  df-0g 14714  df-gsum 14715  df-topgen 14716  df-pt 14717  df-prds 14720  df-xrs 14774  df-qtop 14779  df-imas 14780  df-xps 14782  df-mre 14858  df-mrc 14859  df-acs 14861  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-submnd 15840  df-mulg 15932  df-cntz 16227  df-cmn 16673  df-psmet 18281  df-xmet 18282  df-met 18283  df-bl 18284  df-mopn 18285  df-fbas 18286  df-fg 18287  df-cnfld 18291  df-top 19268  df-bases 19270  df-topon 19271  df-topsp 19272  df-cld 19388  df-ntr 19389  df-cls 19390  df-nei 19467  df-lp 19505  df-perf 19506  df-cn 19596  df-cnp 19597  df-haus 19684  df-cmp 19755  df-tx 19931  df-hmeo 20124  df-fil 20215  df-fm 20307  df-flim 20308  df-flf 20309  df-xms 20691  df-ms 20692  df-tms 20693  df-cncf 21250  df-limc 22138  df-dv 22139

This theorem is referenced by:  fourierdlem75  31805