Theorem fourierdlem101 32172

Description: Integral by substitution for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem101.d	|- D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
fourierdlem101.p	|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` m ) = pi ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem101.g	|- G = ( t e. ( -u pi [,] pi ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) )
fourierdlem101.q	|- ( ph -> Q e. ( P ` M ) )
fourierdlem101.6	|- ( ph -> M e. NN )
fourierdlem101.n	|- ( ph -> N e. NN )
fourierdlem101.x	|- ( ph -> X e. RR )
fourierdlem101.f	|- ( ph -> F : ( -u pi [,] pi ) --> CC )
fourierdlem101.fcn	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem101.r	|- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
fourierdlem101.l	|- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )

Assertion

Ref	Expression
fourierdlem101	|- ( ph -> S. ( -u pi [,] pi ) ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) _d t = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` N ) ` s ) ) _d s )

Distinct variable groups:   D, s, t   t, F   i, G, s, t   t, L   i, M, s, t   m, M, p, i   n, N, s   t, N   Q, i, s, t   Q, p   t, R   i, X, s, t   ph, i, s, t   ph, n

Allowed substitution hints:   ph( m, p)   D( i, m, n, p)   P( t, i, m, n, s, p)   Q( m, n)   R( i, m, n, s, p)   F( i, m, n, s, p)   G( m, n, p)   L( i, m, n, s, p)   M( n)   N( i, m, p)   X( m, n, p)

Proof of Theorem fourierdlem101

Dummy variables r j are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 461	. . . . 5 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> t e. ( -u pi [,] pi ) )
2		fourierdlem101.f	. . . . . . 7 |- ( ph -> F : ( -u pi [,] pi ) --> CC )
3	2	ffvelrnda 6032	. . . . . 6 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( F ` t ) e. CC )
4		fourierdlem101.n	. . . . . . . . 9 |- ( ph -> N e. NN )
5	4	adantr 465	. . . . . . . 8 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> N e. NN )
6		pire 22977	. . . . . . . . . . . 12 |- pi e. RR
7	6	renegcli 9899	. . . . . . . . . . 11 |- -u pi e. RR
8		eliccre 31722	. . . . . . . . . . 11 |- ( ( -u pi e. RR /\ pi e. RR /\ t e. ( -u pi [,] pi ) ) -> t e. RR )
9	7, 6, 8	mp3an12 1314	. . . . . . . . . 10 |- ( t e. ( -u pi [,] pi ) -> t e. RR )
10	9	adantl 466	. . . . . . . . 9 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> t e. RR )
11		fourierdlem101.x	. . . . . . . . . 10 |- ( ph -> X e. RR )
12	11	adantr 465	. . . . . . . . 9 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> X e. RR )
13	10, 12	resubcld 10008	. . . . . . . 8 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( t - X ) e. RR )
14		fourierdlem101.d	. . . . . . . . 9 |- D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
15	14	dirkerre 32059	. . . . . . . 8 |- ( ( N e. NN /\ ( t - X ) e. RR ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
16	5, 13, 15	syl2anc 661	. . . . . . 7 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
17	16	recnd 9639	. . . . . 6 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( ( D ` N ) ` ( t - X ) ) e. CC )
18	3, 17	mulcld 9633	. . . . 5 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) e. CC )
19		fourierdlem101.g	. . . . . 6 |- G = ( t e. ( -u pi [,] pi ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) )
20	19	fvmpt2 5964	. . . . 5 |- ( ( t e. ( -u pi [,] pi ) /\ ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) e. CC ) -> ( G ` t ) = ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) )
21	1, 18, 20	syl2anc 661	. . . 4 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( G ` t ) = ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) )
22	21	eqcomd 2465	. . 3 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) = ( G ` t ) )
23	22	itgeq2dv 22314	. 2 |- ( ph -> S. ( -u pi [,] pi ) ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) _d t = S. ( -u pi [,] pi ) ( G ` t ) _d t )
24		fourierdlem101.p	. . 3 |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` m ) = pi ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
25		fveq2 5872	. . . . 5 |- ( j = i -> ( Q ` j ) = ( Q ` i ) )
26	25	oveq1d 6311	. . . 4 |- ( j = i -> ( ( Q ` j ) - X ) = ( ( Q ` i ) - X ) )
27	26	cbvmptv 4548	. . 3 |- ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) ) = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )
28		fourierdlem101.6	. . 3 |- ( ph -> M e. NN )
29		fourierdlem101.q	. . 3 |- ( ph -> Q e. ( P ` M ) )
30	18, 19	fmptd 6056	. . 3 |- ( ph -> G : ( -u pi [,] pi ) --> CC )
31	19	reseq1i 5279	. . . . 5 |- ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( t e. ( -u pi [,] pi ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
32		ioossicc 11635	. . . . . . 7 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
33	7	a1i 11	. . . . . . . . . 10 |- ( ph -> -u pi e. RR )
34	33	rexrd 9660	. . . . . . . . 9 |- ( ph -> -u pi e. RR* )
35	34	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -u pi e. RR* )
36	6	a1i 11	. . . . . . . . . 10 |- ( ph -> pi e. RR )
37	36	rexrd 9660	. . . . . . . . 9 |- ( ph -> pi e. RR* )
38	37	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> pi e. RR* )
39	24, 28, 29	fourierdlem15 32086	. . . . . . . . 9 |- ( ph -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
40	39	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
41		simpr 461	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0..^ M ) )
42	35, 38, 40, 41	fourierdlem8 32079	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) )
43	32, 42	syl5ss 3510	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) )
44	43	resmptd 5335	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( t e. ( -u pi [,] pi ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) )
45	31, 44	syl5eq 2510	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) )
46	2	adantr 465	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F : ( -u pi [,] pi ) --> CC )
47	46, 43	feqresmpt 5927	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) )
48		fourierdlem101.fcn	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
49	47, 48	eqeltrrd 2546	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
50		eqidd 2458	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( s e. RR |-> ( ( D ` N ) ` s ) ) = ( s e. RR |-> ( ( D ` N ) ` s ) ) )
51		simpr 461	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) -> s = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) )
52		eqidd 2458	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) )
53		oveq1 6303	. . . . . . . . . . . . . . 15 |- ( t = r -> ( t - X ) = ( r - X ) )
54	53	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ t = r ) -> ( t - X ) = ( r - X ) )
55		simpr 461	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
56		elioore 11584	. . . . . . . . . . . . . . . . 17 |- ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> r e. RR )
57	56	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> r e. RR )
58	11	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
59	57, 58	resubcld 10008	. . . . . . . . . . . . . . 15 |- ( ( ph /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r - X ) e. RR )
60	59	adantlr 714	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r - X ) e. RR )
61	52, 54, 55, 60	fvmptd 5961	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) = ( r - X ) )
62	61	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) = ( r - X ) )
63	51, 62	eqtrd 2498	. . . . . . . . . . 11 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) -> s = ( r - X ) )
64	63	fveq2d 5876	. . . . . . . . . 10 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) -> ( ( D ` N ) ` s ) = ( ( D ` N ) ` ( r - X ) ) )
65		elioore 11584	. . . . . . . . . . . . . . 15 |- ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> t e. RR )
66	65	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> t e. RR )
67	11	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
68	66, 67	resubcld 10008	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( t - X ) e. RR )
69	68	adantlr 714	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( t - X ) e. RR )
70		eqid 2457	. . . . . . . . . . . 12 |- ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) )
71	69, 70	fmptd 6056	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> RR )
72	71	ffvelrnda 6032	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) e. RR )
73	4	ad2antrr 725	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> N e. NN )
74	14	dirkerre 32059	. . . . . . . . . . 11 |- ( ( N e. NN /\ ( r - X ) e. RR ) -> ( ( D ` N ) ` ( r - X ) ) e. RR )
75	73, 60, 74	syl2anc 661	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` N ) ` ( r - X ) ) e. RR )
76	50, 64, 72, 75	fvmptd 5961	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) ` ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) = ( ( D ` N ) ` ( r - X ) ) )
77	76	eqcomd 2465	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` N ) ` ( r - X ) ) = ( ( s e. RR |-> ( ( D ` N ) ` s ) ) ` ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) )
78	77	mpteq2dva 4543	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( r - X ) ) ) = ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) ` ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) ) )
79	53	fveq2d 5876	. . . . . . . . 9 |- ( t = r -> ( ( D ` N ) ` ( t - X ) ) = ( ( D ` N ) ` ( r - X ) ) )
80	79	cbvmptv 4548	. . . . . . . 8 |- ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( t - X ) ) ) = ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( r - X ) ) )
81	80	a1i 11	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( t - X ) ) ) = ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( r - X ) ) ) )
82	14	dirkerre 32059	. . . . . . . . . . 11 |- ( ( N e. NN /\ s e. RR ) -> ( ( D ` N ) ` s ) e. RR )
83	4, 82	sylan 471	. . . . . . . . . 10 |- ( ( ph /\ s e. RR ) -> ( ( D ` N ) ` s ) e. RR )
84		eqid 2457	. . . . . . . . . 10 |- ( s e. RR |-> ( ( D ` N ) ` s ) ) = ( s e. RR |-> ( ( D ` N ) ` s ) )
85	83, 84	fmptd 6056	. . . . . . . . 9 |- ( ph -> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> RR )
86	85	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> RR )
87		fcompt 6068	. . . . . . . 8 |- ( ( ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> RR /\ ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> RR ) -> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) o. ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ) = ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) ` ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) ) )
88	86, 71, 87	syl2anc 661	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) o. ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ) = ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) ` ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) ) )
89	78, 81, 88	3eqtr4d 2508	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( t - X ) ) ) = ( ( s e. RR |-> ( ( D ` N ) ` s ) ) o. ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ) )
90		eqid 2457	. . . . . . . 8 |- ( t e. CC |-> ( t - X ) ) = ( t e. CC |-> ( t - X ) )
91		simpr 461	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. CC ) -> t e. CC )
92	11	recnd 9639	. . . . . . . . . . . . . 14 |- ( ph -> X e. CC )
93	92	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. CC ) -> X e. CC )
94	91, 93	negsubd 9956	. . . . . . . . . . . 12 |- ( ( ph /\ t e. CC ) -> ( t + -u X ) = ( t - X ) )
95	94	eqcomd 2465	. . . . . . . . . . 11 |- ( ( ph /\ t e. CC ) -> ( t - X ) = ( t + -u X ) )
96	95	mpteq2dva 4543	. . . . . . . . . 10 |- ( ph -> ( t e. CC |-> ( t - X ) ) = ( t e. CC |-> ( t + -u X ) ) )
97	92	negcld 9937	. . . . . . . . . . 11 |- ( ph -> -u X e. CC )
98		eqid 2457	. . . . . . . . . . . 12 |- ( t e. CC |-> ( t + -u X ) ) = ( t e. CC |-> ( t + -u X ) )
99	98	addccncf 21546	. . . . . . . . . . 11 |- ( -u X e. CC -> ( t e. CC |-> ( t + -u X ) ) e. ( CC -cn-> CC ) )
100	97, 99	syl 16	. . . . . . . . . 10 |- ( ph -> ( t e. CC |-> ( t + -u X ) ) e. ( CC -cn-> CC ) )
101	96, 100	eqeltrd 2545	. . . . . . . . 9 |- ( ph -> ( t e. CC |-> ( t - X ) ) e. ( CC -cn-> CC ) )
102	101	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. CC |-> ( t - X ) ) e. ( CC -cn-> CC ) )
103		ioossre 11611	. . . . . . . . . 10 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
104		ax-resscn 9566	. . . . . . . . . 10 |- RR C_ CC
105	103, 104	sstri 3508	. . . . . . . . 9 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
106	105	a1i 11	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
107	104	a1i 11	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> RR C_ CC )
108	90, 102, 106, 107, 69	cncfmptssg 31854	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> RR ) )
109	83	recnd 9639	. . . . . . . . . 10 |- ( ( ph /\ s e. RR ) -> ( ( D ` N ) ` s ) e. CC )
110	109, 84	fmptd 6056	. . . . . . . . 9 |- ( ph -> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> CC )
111		ssid 3518	. . . . . . . . . 10 |- CC C_ CC
112	14	dirkerf 32061	. . . . . . . . . . . . 13 |- ( N e. NN -> ( D ` N ) : RR --> RR )
113	4, 112	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( D ` N ) : RR --> RR )
114	113	feqmptd 5926	. . . . . . . . . . 11 |- ( ph -> ( D ` N ) = ( s e. RR |-> ( ( D ` N ) ` s ) ) )
115	14	dirkercncf 32071	. . . . . . . . . . . 12 |- ( N e. NN -> ( D ` N ) e. ( RR -cn-> RR ) )
116	4, 115	syl 16	. . . . . . . . . . 11 |- ( ph -> ( D ` N ) e. ( RR -cn-> RR ) )
117	114, 116	eqeltrrd 2546	. . . . . . . . . 10 |- ( ph -> ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> RR ) )
118		cncffvrn 21528	. . . . . . . . . 10 |- ( ( CC C_ CC /\ ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> RR ) ) -> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> CC ) <-> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> CC ) )
119	111, 117, 118	sylancr 663	. . . . . . . . 9 |- ( ph -> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> CC ) <-> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> CC ) )
120	110, 119	mpbird 232	. . . . . . . 8 |- ( ph -> ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> CC ) )
121	120	adantr 465	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> CC ) )
122	108, 121	cncfco 21537	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) o. ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
123	89, 122	eqeltrd 2545	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
124	49, 123	mulcncf 21985	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
125	45, 124	eqeltrd 2545	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
126		cncff 21523	. . . . . . . 8 |- ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
127	48, 126	syl 16	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
128	113	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( D ` N ) : RR --> RR )
129		elioore 11584	. . . . . . . . . . . . 13 |- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. RR )
130	129	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
131	11	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
132	130, 131	resubcld 10008	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( s - X ) e. RR )
133	128, 132	ffvelrnd 6033	. . . . . . . . . 10 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` N ) ` ( s - X ) ) e. RR )
134	133	recnd 9639	. . . . . . . . 9 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` N ) ` ( s - X ) ) e. CC )
135		eqid 2457	. . . . . . . . 9 |- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) )
136	134, 135	fmptd 6056	. . . . . . . 8 |- ( ph -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
137	136	adantr 465	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
138		eqid 2457	. . . . . . 7 |- ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) )
139		fourierdlem101.r	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
140		oveq1 6303	. . . . . . . . . . . . . 14 |- ( t = ( Q ` i ) -> ( t - X ) = ( ( Q ` i ) - X ) )
141	140	fveq2d 5876	. . . . . . . . . . . . 13 |- ( t = ( Q ` i ) -> ( ( D ` N ) ` ( t - X ) ) = ( ( D ` N ) ` ( ( Q ` i ) - X ) ) )
142	141	eqcomd 2465	. . . . . . . . . . . 12 |- ( t = ( Q ` i ) -> ( ( D ` N ) ` ( ( Q ` i ) - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
143	142	adantl 466	. . . . . . . . . . 11 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ t = ( Q ` i ) ) -> ( ( D ` N ) ` ( ( Q ` i ) - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
144		eqidd 2458	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) )
145		oveq1 6303	. . . . . . . . . . . . . 14 |- ( s = t -> ( s - X ) = ( t - X ) )
146	145	fveq2d 5876	. . . . . . . . . . . . 13 |- ( s = t -> ( ( D ` N ) ` ( s - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
147	146	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) /\ s = t ) -> ( ( D ` N ) ` ( s - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
148		elsn 4046	. . . . . . . . . . . . . . 15 |- ( t e. { ( Q ` i ) } <-> t = ( Q ` i ) )
149	148	notbii 296	. . . . . . . . . . . . . 14 |- ( -. t e. { ( Q ` i ) } <-> -. t = ( Q ` i ) )
150		elunnel2 31597	. . . . . . . . . . . . . 14 |- ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) /\ -. t e. { ( Q ` i ) } ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
151	149, 150	sylan2br 476	. . . . . . . . . . . . 13 |- ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) /\ -. t = ( Q ` i ) ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
152	151	adantll 713	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
153	113	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( D ` N ) : RR --> RR )
154		simpr 461	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t = ( Q ` i ) ) -> t = ( Q ` i ) )
155	9	ssriv 3503	. . . . . . . . . . . . . . . . . . . 20 |- ( -u pi [,] pi ) C_ RR
156		fzossfz 11844	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 0..^ M ) C_ ( 0 ... M )
157	156, 41	sseldi 3497	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
158	40, 157	ffvelrnd 6033	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. ( -u pi [,] pi ) )
159	155, 158	sseldi 3497	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
160	159	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t = ( Q ` i ) ) -> ( Q ` i ) e. RR )
161	154, 160	eqeltrd 2545	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t = ( Q ` i ) ) -> t e. RR )
162	161	adantlr 714	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ t = ( Q ` i ) ) -> t e. RR )
163	152, 65	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) -> t e. RR )
164	162, 163	pm2.61dan 791	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> t e. RR )
165	11	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> X e. RR )
166	164, 165	resubcld 10008	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( t - X ) e. RR )
167	153, 166	ffvelrnd 6033	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
168	167	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
169	144, 147, 152, 168	fvmptd 5961	. . . . . . . . . . 11 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) = ( ( D ` N ) ` ( t - X ) ) )
170	143, 169	ifeqda 3977	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> if ( t = ( Q ` i ) , ( ( D ` N ) ` ( ( Q ` i ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( D ` N ) ` ( t - X ) ) )
171	170	mpteq2dva 4543	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> if ( t = ( Q ` i ) , ( ( D ` N ) ` ( ( Q ` i ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) = ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) )
172	113	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( D ` N ) : RR --> RR )
173		simpr 461	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) )
174		elun 3641	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) <-> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ s e. { ( Q ` i ) } ) )
175	173, 174	sylib 196	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ s e. { ( Q ` i ) } ) )
176	175	adantlr 714	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ s e. { ( Q ` i ) } ) )
177		elsni 4057	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( s e. { ( Q ` i ) } -> s = ( Q ` i ) )
178	177	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. { ( Q ` i ) } ) -> s = ( Q ` i ) )
179	159	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. { ( Q ` i ) } ) -> ( Q ` i ) e. RR )
180	178, 179	eqeltrd 2545	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. { ( Q ` i ) } ) -> s e. RR )
181	180	ex 434	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. { ( Q ` i ) } -> s e. RR ) )
182	181	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( s e. { ( Q ` i ) } -> s e. RR ) )
183		pm3.44 511	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. RR ) /\ ( s e. { ( Q ` i ) } -> s e. RR ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ s e. { ( Q ` i ) } ) -> s e. RR ) )
184	129, 182, 183	sylancr 663	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ s e. { ( Q ` i ) } ) -> s e. RR ) )
185	176, 184	mpd 15	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> s e. RR )
186	11	ad2antrr 725	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> X e. RR )
187	185, 186	resubcld 10008	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( s - X ) e. RR )
188		eqid 2457	. . . . . . . . . . . . . . . 16 |- ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) = ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) )
189	187, 188	fmptd 6056	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) : ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) --> RR )
190		fcompt 6068	. . . . . . . . . . . . . . 15 |- ( ( ( D ` N ) : RR --> RR /\ ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) : ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) --> RR ) -> ( ( D ` N ) o. ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ) = ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ` t ) ) ) )
191	172, 189, 190	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( D ` N ) o. ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ) = ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ` t ) ) ) )
192		eqidd 2458	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) = ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) )
193	145	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ s = t ) -> ( s - X ) = ( t - X ) )
194		simpr 461	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) )
195	192, 193, 194, 166	fvmptd 5961	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ` t ) = ( t - X ) )
196	195	fveq2d 5876	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( ( D ` N ) ` ( ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ` t ) ) = ( ( D ` N ) ` ( t - X ) ) )
197	196	mpteq2dva 4543	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ` t ) ) ) = ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) )
198	191, 197	eqtr2d 2499	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) = ( ( D ` N ) o. ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ) )
199		eqid 2457	. . . . . . . . . . . . . . . 16 |- ( s e. CC |-> ( s - X ) ) = ( s e. CC |-> ( s - X ) )
200		simpr 461	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ s e. CC ) -> s e. CC )
201	92	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ s e. CC ) -> X e. CC )
202	200, 201	negsubd 9956	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ s e. CC ) -> ( s + -u X ) = ( s - X ) )
203	202	eqcomd 2465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ s e. CC ) -> ( s - X ) = ( s + -u X ) )
204	203	mpteq2dva 4543	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( s e. CC |-> ( s - X ) ) = ( s e. CC |-> ( s + -u X ) ) )
205		eqid 2457	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. CC |-> ( s + -u X ) ) = ( s e. CC |-> ( s + -u X ) )
206	205	addccncf 21546	. . . . . . . . . . . . . . . . . . 19 |- ( -u X e. CC -> ( s e. CC |-> ( s + -u X ) ) e. ( CC -cn-> CC ) )
207	97, 206	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( s e. CC |-> ( s + -u X ) ) e. ( CC -cn-> CC ) )
208	204, 207	eqeltrd 2545	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( s e. CC |-> ( s - X ) ) e. ( CC -cn-> CC ) )
209	208	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. CC |-> ( s - X ) ) e. ( CC -cn-> CC ) )
210	159	recnd 9639	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. CC )
211	210	snssd 4177	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> { ( Q ` i ) } C_ CC )
212	106, 211	unssd 3676	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) C_ CC )
213	199, 209, 212, 107, 187	cncfmptssg 31854	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) e. ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) -cn-> RR ) )
214	114, 120	eqeltrd 2545	. . . . . . . . . . . . . . . 16 |- ( ph -> ( D ` N ) e. ( RR -cn-> CC ) )
215	214	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( D ` N ) e. ( RR -cn-> CC ) )
216	213, 215	cncfco 21537	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( D ` N ) o. ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ) e. ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) -cn-> CC ) )
217		eqid 2457	. . . . . . . . . . . . . . . 16 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
218		eqid 2457	. . . . . . . . . . . . . . . 16 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) )
219	217	cnfldtop 21417	. . . . . . . . . . . . . . . . . 18 |- ( TopOpen ` ℂfld ) e. Top
220		unicntop 31613	. . . . . . . . . . . . . . . . . . 19 |- CC = U. ( TopOpen ` ℂfld )
221	220	restid 14851	. . . . . . . . . . . . . . . . . 18 |- ( ( TopOpen ` ℂfld ) e. Top -> ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld ) )
222	219, 221	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld )
223	222	eqcomi 2470	. . . . . . . . . . . . . . . 16 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
224	217, 218, 223	cncfcn 21539	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) C_ CC /\ CC C_ CC ) -> ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) Cn ( TopOpen ` ℂfld ) ) )
225	212, 111, 224	sylancl 662	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) Cn ( TopOpen ` ℂfld ) ) )
226	216, 225	eleqtrd 2547	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( D ` N ) o. ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) Cn ( TopOpen ` ℂfld ) ) )
227	198, 226	eqeltrd 2545	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) Cn ( TopOpen ` ℂfld ) ) )
228	217	cnfldtopon 21416	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
229		resttopon 19789	. . . . . . . . . . . . . 14 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) e. (TopOn ` ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) )
230	228, 212, 229	sylancr 663	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) e. (TopOn ` ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) )
231		cncnp 19908	. . . . . . . . . . . . 13 |- ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) e. (TopOn ` ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ ( TopOpen ` ℂfld ) e. (TopOn ` CC ) ) -> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) Cn ( TopOpen ` ℂfld ) ) <-> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) : ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) --> CC /\ A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` s ) ) ) )
232	230, 228, 231	sylancl 662	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) Cn ( TopOpen ` ℂfld ) ) <-> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) : ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) --> CC /\ A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` s ) ) ) )
233	227, 232	mpbid 210	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) : ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) --> CC /\ A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` s ) ) )
234	233	simprd 463	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` s ) )
235		eqidd 2458	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( Q ` i ) )
236		elsncg 4055	. . . . . . . . . . . . . 14 |- ( ( Q ` i ) e. RR -> ( ( Q ` i ) e. { ( Q ` i ) } <-> ( Q ` i ) = ( Q ` i ) ) )
237	159, 236	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) e. { ( Q ` i ) } <-> ( Q ` i ) = ( Q ` i ) ) )
238	235, 237	mpbird 232	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. { ( Q ` i ) } )
239	238	olcd 393	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ ( Q ` i ) e. { ( Q ` i ) } ) )
240		elun 3641	. . . . . . . . . . 11 |- ( ( Q ` i ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) <-> ( ( Q ` i ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ ( Q ` i ) e. { ( Q ` i ) } ) )
241	239, 240	sylibr 212	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) )
242		fveq2 5872	. . . . . . . . . . . 12 |- ( s = ( Q ` i ) -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` s ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` ( Q ` i ) ) )
243	242	eleq2d 2527	. . . . . . . . . . 11 |- ( s = ( Q ` i ) -> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` s ) <-> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` ( Q ` i ) ) ) )
244	243	rspccva 3209	. . . . . . . . . 10 |- ( ( A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` s ) /\ ( Q ` i ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` ( Q ` i ) ) )
245	234, 241, 244	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` ( Q ` i ) ) )
246	171, 245	eqeltrd 2545	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> if ( t = ( Q ` i ) , ( ( D ` N ) ` ( ( Q ` i ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` ( Q ` i ) ) )
247		eqid 2457	. . . . . . . . 9 |- ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> if ( t = ( Q ` i ) , ( ( D ` N ) ` ( ( Q ` i ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) = ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> if ( t = ( Q ` i ) , ( ( D ` N ) ` ( ( Q ` i ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) )
248	218, 217, 247, 137, 106, 210	ellimc 22403	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( D ` N ) ` ( ( Q ` i ) - X ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) lim CC ( Q ` i ) ) <-> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> if ( t = ( Q ` i ) , ( ( D ` N ) ` ( ( Q ` i ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` ( Q ` i ) ) ) )
249	246, 248	mpbird 232	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( D ` N ) ` ( ( Q ` i ) - X ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) lim CC ( Q ` i ) ) )
250	127, 137, 138, 139, 249	mullimcf 31811	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( R x. ( ( D ` N ) ` ( ( Q ` i ) - X ) ) ) e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) lim CC ( Q ` i ) ) )
251		fvres 5886	. . . . . . . . . 10 |- ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) = ( F ` t ) )
252	251	adantl 466	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) = ( F ` t ) )
253	252	oveq1d 6311	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) )
254	253	mpteq2dva 4543	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) )
255	254	oveq1d 6311	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) lim CC ( Q ` i ) ) = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) lim CC ( Q ` i ) ) )
256	250, 255	eleqtrd 2547	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( R x. ( ( D ` N ) ` ( ( Q ` i ) - X ) ) ) e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) lim CC ( Q ` i ) ) )
257		eqidd 2458	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) )
258		simpr 461	. . . . . . . . . . 11 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = t ) -> s = t )
259	258	oveq1d 6311	. . . . . . . . . 10 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = t ) -> ( s - X ) = ( t - X ) )
260	259	fveq2d 5876	. . . . . . . . 9 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = t ) -> ( ( D ` N ) ` ( s - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
261		simpr 461	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
262	113	ad2antrr 725	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( D ` N ) : RR --> RR )
263	262, 69	ffvelrnd 6033	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
264	257, 260, 261, 263	fvmptd 5961	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) = ( ( D ` N ) ` ( t - X ) ) )
265	264	oveq2d 6312	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) )
266	265	mpteq2dva 4543	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) )
267	266	oveq1d 6311	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) lim CC ( Q ` i ) ) = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) lim CC ( Q ` i ) ) )
268	256, 267	eleqtrd 2547	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( R x. ( ( D ` N ) ` ( ( Q ` i ) - X ) ) ) e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) lim CC ( Q ` i ) ) )
269	45	eqcomd 2465	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) = ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
270	269	oveq1d 6311	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) lim CC ( Q ` i ) ) = ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
271	268, 270	eleqtrd 2547	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( R x. ( ( D ` N ) ` ( ( Q ` i ) - X ) ) ) e. ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
272		fourierdlem101.l	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
273		iftrue 3950	. . . . . . . . . . 11 |- ( t = ( Q ` ( i + 1 ) ) -> if ( t = ( Q ` ( i + 1 ) ) , ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) )
274		oveq1 6303	. . . . . . . . . . . . 13 |- ( t = ( Q ` ( i + 1 ) ) -> ( t - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
275	274	eqcomd 2465	. . . . . . . . . . . 12 |- ( t = ( Q ` ( i + 1 ) ) -> ( ( Q ` ( i + 1 ) ) - X ) = ( t - X ) )
276	275	fveq2d 5876	. . . . . . . . . . 11 |- ( t = ( Q ` ( i + 1 ) ) -> ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
277	273, 276