Theorem fourierdlem101 31831

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 22718	. . . . . . . . . . . . 13 |- pi e. RR
7	6	renegcli 9892	. . . . . . . . . . . 12 |- -u pi e. RR
8	7	a1i 11	. . . . . . . . . . 11 |- ( t e. ( -u pi [,] pi ) -> -u pi e. RR )
9	6	a1i 11	. . . . . . . . . . 11 |- ( t e. ( -u pi [,] pi ) -> pi e. RR )
10		id 22	. . . . . . . . . . 11 |- ( t e. ( -u pi [,] pi ) -> t e. ( -u pi [,] pi ) )
11		eliccre 31427	. . . . . . . . . . 11 |- ( ( -u pi e. RR /\ pi e. RR /\ t e. ( -u pi [,] pi ) ) -> t e. RR )
12	8, 9, 10, 11	syl3anc 1228	. . . . . . . . . 10 |- ( t e. ( -u pi [,] pi ) -> t e. RR )
13	12	adantl 466	. . . . . . . . 9 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> t e. RR )
14		fourierdlem101.x	. . . . . . . . . 10 |- ( ph -> X e. RR )
15	14	adantr 465	. . . . . . . . 9 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> X e. RR )
16	13, 15	resubcld 9999	. . . . . . . 8 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( t - X ) e. RR )
17		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 ) ) ) ) ) ) )
18	17	dirkerre 31718	. . . . . . . 8 |- ( ( N e. NN /\ ( t - X ) e. RR ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
19	5, 16, 18	syl2anc 661	. . . . . . 7 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
20	19	recnd 9634	. . . . . 6 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( ( D ` N ) ` ( t - X ) ) e. CC )
21	3, 20	mulcld 9628	. . . . 5 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) e. CC )
22		fourierdlem101.g	. . . . . 6 |- G = ( t e. ( -u pi [,] pi ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) )
23	22	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 ) ) ) )
24	1, 21, 23	syl2anc 661	. . . 4 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( G ` t ) = ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) )
25	24	eqcomd 2475	. . 3 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) = ( G ` t ) )
26	25	itgeq2dv 22056	. 2 |- ( ph -> S. ( -u pi [,] pi ) ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) _d t = S. ( -u pi [,] pi ) ( G ` t ) _d t )
27		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 ) ) ) } )
28		nfcv 2629	. . . 4 |- F/_ i ( ( Q ` j ) - X )
29		nfcv 2629	. . . 4 |- F/_ j ( ( Q ` i ) - X )
30		fveq2 5872	. . . . 5 |- ( j = i -> ( Q ` j ) = ( Q ` i ) )
31	30	oveq1d 6310	. . . 4 |- ( j = i -> ( ( Q ` j ) - X ) = ( ( Q ` i ) - X ) )
32	28, 29, 31	cbvmpt 4543	. . 3 |- ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) ) = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )
33		fourierdlem101.6	. . 3 |- ( ph -> M e. NN )
34		fourierdlem101.q	. . 3 |- ( ph -> Q e. ( P ` M ) )
35	21	ralrimiva 2881	. . . 4 |- ( ph -> A. t e. ( -u pi [,] pi ) ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) e. CC )
36	22	fmpt 6053	. . . 4 |- ( A. t e. ( -u pi [,] pi ) ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) e. CC <-> G : ( -u pi [,] pi ) --> CC )
37	35, 36	sylib 196	. . 3 |- ( ph -> G : ( -u pi [,] pi ) --> CC )
38	22	reseq1i 5275	. . . . . 6 |- ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( t e. ( -u pi [,] pi ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
39	38	a1i 11	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( t e. ( -u pi [,] pi ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
40		ioossicc 11622	. . . . . . 7 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
41	7	a1i 11	. . . . . . . . . 10 |- ( ph -> -u pi e. RR )
42	41	rexrd 9655	. . . . . . . . 9 |- ( ph -> -u pi e. RR* )
43	42	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -u pi e. RR* )
44	6	a1i 11	. . . . . . . . . 10 |- ( ph -> pi e. RR )
45	44	rexrd 9655	. . . . . . . . 9 |- ( ph -> pi e. RR* )
46	45	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> pi e. RR* )
47	27, 33, 34	fourierdlem15 31745	. . . . . . . . 9 |- ( ph -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
48	47	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
49		simpr 461	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0..^ M ) )
50	43, 46, 48, 49	fourierdlem8 31738	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) )
51	40, 50	syl5ss 3520	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) )
52		resmpt 5329	. . . . . 6 |- ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) -> ( ( 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 ) ) ) ) )
53	51, 52	syl 16	. . . . 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 ) ) ) ) )
54		eqidd 2468	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) )
55	39, 53, 54	3eqtrd 2512	. . . 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 ) ) ) ) )
56	2	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F : ( -u pi [,] pi ) --> CC )
57	56, 51	feqresmpt 5928	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) )
58	57	eqcomd 2475	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
59		fourierdlem101.fcn	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
60	58, 59	eqeltrd 2555	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
61	4	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ s e. RR ) -> N e. NN )
62		simpr 461	. . . . . . . . . . . 12 |- ( ( ph /\ s e. RR ) -> s e. RR )
63	17	dirkerre 31718	. . . . . . . . . . . 12 |- ( ( N e. NN /\ s e. RR ) -> ( ( D ` N ) ` s ) e. RR )
64	61, 62, 63	syl2anc 661	. . . . . . . . . . 11 |- ( ( ph /\ s e. RR ) -> ( ( D ` N ) ` s ) e. RR )
65	64	ralrimiva 2881	. . . . . . . . . 10 |- ( ph -> A. s e. RR ( ( D ` N ) ` s ) e. RR )
66		eqid 2467	. . . . . . . . . . 11 |- ( s e. RR |-> ( ( D ` N ) ` s ) ) = ( s e. RR |-> ( ( D ` N ) ` s ) )
67	66	fmpt 6053	. . . . . . . . . 10 |- ( A. s e. RR ( ( D ` N ) ` s ) e. RR <-> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> RR )
68	65, 67	sylib 196	. . . . . . . . 9 |- ( ph -> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> RR )
69	68	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> RR )
70		elioore 11571	. . . . . . . . . . . . 13 |- ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> t e. RR )
71	70	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> t e. RR )
72	14	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
73	71, 72	resubcld 9999	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( t - X ) e. RR )
74	73	adantlr 714	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( t - X ) e. RR )
75	74	ralrimiva 2881	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A. t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( t - X ) e. RR )
76		eqid 2467	. . . . . . . . . 10 |- ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) )
77	76	fmpt 6053	. . . . . . . . 9 |- ( A. t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( t - X ) e. RR <-> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> RR )
78	75, 77	sylib 196	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> RR )
79		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 ) ) ) )
80	69, 78, 79	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 ) ) ) )
81		nfcv 2629	. . . . . . . . . 10 |- F/_ r ( ( D ` N ) ` ( t - X ) )
82		nfcv 2629	. . . . . . . . . 10 |- F/_ t ( ( D ` N ) ` ( r - X ) )
83		oveq1 6302	. . . . . . . . . . 11 |- ( t = r -> ( t - X ) = ( r - X ) )
84	83	fveq2d 5876	. . . . . . . . . 10 |- ( t = r -> ( ( D ` N ) ` ( t - X ) ) = ( ( D ` N ) ` ( r - X ) ) )
85	81, 82, 84	cbvmpt 4543	. . . . . . . . 9 |- ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( t - X ) ) ) = ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( r - X ) ) )
86	85	a1i 11	. . . . . . . 8 |- ( ( 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 ) ) ) )
87		eqidd 2468	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( s e. RR |-> ( ( D ` N ) ` s ) ) = ( s e. RR |-> ( ( D ` N ) ` s ) ) )
88		simpr 461	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
89		eqidd 2468	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) )
90	83	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ t = r ) -> ( t - X ) = ( r - X ) )
91		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
92		elioore 11571	. . . . . . . . . . . . . . . . . 18 |- ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> r e. RR )
93	92	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> r e. RR )
94	14	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
95	93, 94	resubcld 9999	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r - X ) e. RR )
96	95	adantlr 714	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r - X ) e. RR )
97	89, 90, 91, 96	fvmptd 5962	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) = ( r - X ) )
98	97	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
99	88, 98	eqtrd 2508	. . . . . . . . . . . 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 = ( r - X ) )
100	99	fveq2d 5876	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
101	78	ffvelrnda 6032	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) e. RR )
102	4	ad2antrr 725	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> N e. NN )
103	17	dirkerre 31718	. . . . . . . . . . . 12 |- ( ( N e. NN /\ ( r - X ) e. RR ) -> ( ( D ` N ) ` ( r - X ) ) e. RR )
104	102, 96, 103	syl2anc 661	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` N ) ` ( r - X ) ) e. RR )
105	87, 100, 101, 104	fvmptd 5962	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
106	105	eqcomd 2475	. . . . . . . . 9 |- ( ( ( 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 ) ) )
107	106	mpteq2dva 4539	. . . . . . . 8 |- ( ( 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 ) ) ) )
108	86, 107	eqtr2d 2509	. . . . . . 7 |- ( ( 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 ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( t - X ) ) ) )
109	80, 108	eqtr2d 2509	. . . . . 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 ) ) ) )
110		eqid 2467	. . . . . . . 8 |- ( t e. CC |-> ( t - X ) ) = ( t e. CC |-> ( t - X ) )
111		simpr 461	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. CC ) -> t e. CC )
112		ax-resscn 9561	. . . . . . . . . . . . . . 15 |- RR C_ CC
113	112, 14	sseldi 3507	. . . . . . . . . . . . . 14 |- ( ph -> X e. CC )
114	113	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. CC ) -> X e. CC )
115	111, 114	negsubd 9948	. . . . . . . . . . . 12 |- ( ( ph /\ t e. CC ) -> ( t + -u X ) = ( t - X ) )
116	115	eqcomd 2475	. . . . . . . . . . 11 |- ( ( ph /\ t e. CC ) -> ( t - X ) = ( t + -u X ) )
117	116	mpteq2dva 4539	. . . . . . . . . 10 |- ( ph -> ( t e. CC |-> ( t - X ) ) = ( t e. CC |-> ( t + -u X ) ) )
118	113	negcld 9929	. . . . . . . . . . 11 |- ( ph -> -u X e. CC )
119		eqid 2467	. . . . . . . . . . . 12 |- ( t e. CC |-> ( t + -u X ) ) = ( t e. CC |-> ( t + -u X ) )
120	119	addccncf 21288	. . . . . . . . . . 11 |- ( -u X e. CC -> ( t e. CC |-> ( t + -u X ) ) e. ( CC -cn-> CC ) )
121	118, 120	syl 16	. . . . . . . . . 10 |- ( ph -> ( t e. CC |-> ( t + -u X ) ) e. ( CC -cn-> CC ) )
122	117, 121	eqeltrd 2555	. . . . . . . . 9 |- ( ph -> ( t e. CC |-> ( t - X ) ) e. ( CC -cn-> CC ) )
123	122	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. CC |-> ( t - X ) ) e. ( CC -cn-> CC ) )
124		ioossre 11598	. . . . . . . . . 10 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
125	124, 112	sstri 3518	. . . . . . . . 9 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
126	125	a1i 11	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
127	112	a1i 11	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> RR C_ CC )
128	110, 123, 126, 127, 74	cncfmptssg 31531	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> RR ) )
129	112, 64	sseldi 3507	. . . . . . . . . 10 |- ( ( ph /\ s e. RR ) -> ( ( D ` N ) ` s ) e. CC )
130	129, 66	fmptd 6056	. . . . . . . . 9 |- ( ph -> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> CC )
131		ssid 3528	. . . . . . . . . . 11 |- CC C_ CC
132	131	a1i 11	. . . . . . . . . 10 |- ( ph -> CC C_ CC )
133	17	dirkerf 31720	. . . . . . . . . . . . . 14 |- ( N e. NN -> ( D ` N ) : RR --> RR )
134	4, 133	syl 16	. . . . . . . . . . . . 13 |- ( ph -> ( D ` N ) : RR --> RR )
135	134	feqmptd 5927	. . . . . . . . . . . 12 |- ( ph -> ( D ` N ) = ( s e. RR |-> ( ( D ` N ) ` s ) ) )
136	135	eqcomd 2475	. . . . . . . . . . 11 |- ( ph -> ( s e. RR |-> ( ( D ` N ) ` s ) ) = ( D ` N ) )
137	17	dirkercncf 31730	. . . . . . . . . . . 12 |- ( N e. NN -> ( D ` N ) e. ( RR -cn-> RR ) )
138	4, 137	syl 16	. . . . . . . . . . 11 |- ( ph -> ( D ` N ) e. ( RR -cn-> RR ) )
139	136, 138	eqeltrd 2555	. . . . . . . . . 10 |- ( ph -> ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> RR ) )
140		cncffvrn 21270	. . . . . . . . . 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 ) )
141	132, 139, 140	syl2anc 661	. . . . . . . . 9 |- ( ph -> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> CC ) <-> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> CC ) )
142	130, 141	mpbird 232	. . . . . . . 8 |- ( ph -> ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> CC ) )
143	142	adantr 465	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> CC ) )
144	128, 143	cncfco 21279	. . . . . 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 ) )
145	109, 144	eqeltrd 2555	. . . . 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 ) )
146	60, 145	mulcncf 21727	. . . 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 ) )
147	55, 146	eqeltrd 2555	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
148		cncff 21265	. . . . . . . 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 )
149	59, 148	syl 16	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
150	134	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( D ` N ) : RR --> RR )
151	124	sseli 3505	. . . . . . . . . . . . 13 |- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. RR )
152	151	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
153	14	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
154	152, 153	resubcld 9999	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( s - X ) e. RR )
155		ffvelrn 6030	. . . . . . . . . . 11 |- ( ( ( D ` N ) : RR --> RR /\ ( s - X ) e. RR ) -> ( ( D ` N ) ` ( s - X ) ) e. RR )
156	150, 154, 155	syl2anc 661	. . . . . . . . . 10 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` N ) ` ( s - X ) ) e. RR )
157	112, 156	sseldi 3507	. . . . . . . . 9 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` N ) ` ( s - X ) ) e. CC )
158		eqid 2467	. . . . . . . . 9 |- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) )
159	157, 158	fmptd 6056	. . . . . . . 8 |- ( ph -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
160	159	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 )
161		eqid 2467	. . . . . . 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 ) ) )
162		fourierdlem101.r	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
163		iftrue 3951	. . . . . . . . . . . . 13 |- ( t = ( 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 ) ` ( ( Q ` i ) - X ) ) )
164	163	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ t = ( 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 ) ` ( ( Q ` i ) - X ) ) )
165		oveq1 6302	. . . . . . . . . . . . . . 15 |- ( t = ( Q ` i ) -> ( t - X ) = ( ( Q ` i ) - X ) )
166	165	fveq2d 5876	. . . . . . . . . . . . . 14 |- ( t = ( Q ` i ) -> ( ( D ` N ) ` ( t - X ) ) = ( ( D ` N ) ` ( ( Q ` i ) - X ) ) )
167	166	eqcomd 2475	. . . . . . . . . . . . 13 |- ( t = ( Q ` i ) -> ( ( D ` N ) ` ( ( Q ` i ) - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
168	167	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
169		eqidd 2468	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ t = ( Q ` i ) ) -> ( ( D ` N ) ` ( t - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
170	164, 168, 169	3eqtrd 2512	. . . . . . . . . . 11 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ t = ( 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		iffalse 3954	. . . . . . . . . . . . 13 |- ( -. t = ( Q ` i ) -> if ( t = ( Q ` i ) , ( ( D ` N ) ` ( ( Q ` i ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) )
172	171	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) -> if ( t = ( Q ` i ) , ( ( D ` N ) ` ( ( Q ` i ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) )
173		eqidd 2468	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) ) )
174		oveq1 6302	. . . . . . . . . . . . . . 15 |- ( s = t -> ( s - X ) = ( t - X ) )
175	174	fveq2d 5876	. . . . . . . . . . . . . 14 |- ( s = t -> ( ( D ` N ) ` ( s - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
176	175	adantl 466	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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 ) ) )
177		simpl 457	. . . . . . . . . . . . . . 15 |- ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) /\ -. t = ( Q ` i ) ) -> t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) )
178		vex 3121	. . . . . . . . . . . . . . . . . . 19 |- t e. _V
179		elsncg 4056	. . . . . . . . . . . . . . . . . . 19 |- ( t e. _V -> ( t e. { ( Q ` i ) } <-> t = ( Q ` i ) ) )
180	178, 179	ax-mp 5	. . . . . . . . . . . . . . . . . 18 |- ( t e. { ( Q ` i ) } <-> t = ( Q ` i ) )
181	180	notbii 296	. . . . . . . . . . . . . . . . 17 |- ( -. t e. { ( Q ` i ) } <-> -. t = ( Q ` i ) )
182	181	biimpri 206	. . . . . . . . . . . . . . . 16 |- ( -. t = ( Q ` i ) -> -. t e. { ( Q ` i ) } )
183	182	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) /\ -. t = ( Q ` i ) ) -> -. t e. { ( Q ` i ) } )
184		elun 3650	. . . . . . . . . . . . . . . . . . 19 |- ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) <-> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ t e. { ( Q ` i ) } ) )
185	184	biimpi 194	. . . . . . . . . . . . . . . . . 18 |- ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ t e. { ( Q ` i ) } ) )
186	185	orcomd 388	. . . . . . . . . . . . . . . . 17 |- ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) -> ( t e. { ( Q ` i ) } \/ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
187	186	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) /\ -. t e. { ( Q ` i ) } ) -> ( t e. { ( Q ` i ) } \/ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
188		simpr 461	. . . . . . . . . . . . . . . 16 |- ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) /\ -. t e. { ( Q ` i ) } ) -> -. t e. { ( Q ` i ) } )
189		pm2.53 373	. . . . . . . . . . . . . . . 16 |- ( ( t e. { ( Q ` i ) } \/ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( -. t e. { ( Q ` i ) } -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
190	187, 188, 189	sylc 60	. . . . . . . . . . . . . . 15 |- ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) /\ -. t e. { ( Q ` i ) } ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
191	177, 183, 190	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) /\ -. t = ( Q ` i ) ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
192	191	adantll 713	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) ) )
193	134	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( D ` N ) : RR --> RR )
194		simpr 461	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t = ( Q ` i ) ) -> t = ( Q ` i ) )
195	12	ssriv 3513	. . . . . . . . . . . . . . . . . . . . 21 |- ( -u pi [,] pi ) C_ RR
196		fzossfz 11826	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0..^ M ) C_ ( 0 ... M )
197	196, 49	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
198		ffvelrn 6030	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( Q : ( 0 ... M ) --> ( -u pi [,] pi ) /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. ( -u pi [,] pi ) )
199	48, 197, 198	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. ( -u pi [,] pi ) )
200	195, 199	sseldi 3507	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
201	200	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t = ( Q ` i ) ) -> ( Q ` i ) e. RR )
202	194, 201	eqeltrd 2555	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t = ( Q ` i ) ) -> t e. RR )
203	202	adantlr 714	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ t = ( Q ` i ) ) -> t e. RR )
204	192, 70	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) -> t e. RR )
205	203, 204	pm2.61dan 789	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> t e. RR )
206	14	ad2antrr 725	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> X e. RR )
207	205, 206	resubcld 9999	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( t - X ) e. RR )
208		ffvelrn 6030	. . . . . . . . . . . . . . 15 |- ( ( ( D ` N ) : RR --> RR /\ ( t - X ) e. RR ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
209	193, 207, 208	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
210	209	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
211	173, 176, 192, 210	fvmptd 5962	. . . . . . . . . . . 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 ) ) ) ` t ) = ( ( D ` N ) ` ( t - X ) ) )
212		eqidd 2468	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) -> ( ( D ` N ) ` ( t - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
213	172, 211, 212	3eqtrd 2512	. . . . . . . . . . 11 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( 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 ) ) )
214	170, 213	pm2.61dan 789	. . . . . . . . . 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 ) ) )
215	214	mpteq2dva 4539	. . . . . . . . 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 ) ) ) )
216	134	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( D ` N ) : RR --> RR )
217		simpr 461	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) )
218		elun 3650	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) <-> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ s e. { ( Q ` i ) } ) )
219	217, 218	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 ) } ) )
220	219	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 ) } ) )
221	151	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. RR ) )
222		elsni 4058	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( s e. { ( Q ` i ) } -> s = ( Q ` i ) )
223	222	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. { ( Q ` i ) } ) -> s = ( Q ` i ) )
224	200	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. { ( Q ` i ) } ) -> ( Q ` i ) e. RR )
225	223, 224	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. { ( Q ` i ) } ) -> s e. RR )
226	225	ex 434	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. { ( Q ` i ) } -> s e. RR ) )
227	226	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 ) )
228		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 ) )
229	221, 227, 228	syl2anc 661	. . . . . . . . . . . . . . . . . 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 ) )
230	220, 229	mpd 15	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> s e. RR )
231	14	ad2antrr 725	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> X e. RR )
232	230, 231	resubcld 9999	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( s - X ) e. RR )
233		eqid 2467	. . . . . . . . . . . . . . . 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 ) )
234	232, 233	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 )
235		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 ) ) ) )
236	216, 234, 235	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 ) ) ) )
237		eqidd 2468	. . . . . . . . . . . . . . . . 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 ) ) )
238	174	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ s = t ) -> ( s - X ) = ( t - X ) )
239		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 ) } ) )
240	237, 238, 239, 207	fvmptd 5962	. . . . . . . . . . . . . . . 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 ) )
241	240	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 ) ) )
242	241	mpteq2dva 4539	. . . . . . . . . . . . . 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 ) ) ) )
243	236, 242	eqtr2d 2509	. . . . . . . . . . . . 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 ) ) ) )
244		eqid 2467	. . . . . . . . . . . . . . . 16 |- ( s e. CC |-> ( s - X ) ) = ( s e. CC |-> ( s - X ) )
245		simpr 461	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ s e. CC ) -> s e. CC )
246	113	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ s e. CC ) -> X e. CC )
247		negsub 9879	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( s e. CC /\ X e. CC ) -> ( s + -u X ) = ( s - X ) )
248	245, 246, 247	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ s e. CC ) -> ( s + -u X ) = ( s - X ) )
249	248	eqcomd 2475	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ s e. CC ) -> ( s - X ) = ( s + -u X ) )
250	249	mpteq2dva 4539	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( s e. CC |-> ( s - X ) ) = ( s e. CC |-> ( s + -u X ) ) )
251		eqid 2467	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. CC |-> ( s + -u X ) ) = ( s e. CC |-> ( s + -u X ) )
252	251	addccncf 21288	. . . . . . . . . . . . . . . . . . 19 |- ( -u X e. CC -> ( s e. CC |-> ( s + -u X ) ) e. ( CC -cn-> CC ) )
253	118, 252	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( s e. CC |-> ( s + -u X ) ) e. ( CC -cn-> CC ) )
254	250, 253	eqeltrd 2555	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( s e. CC |-> ( s - X ) ) e. ( CC -cn-> CC ) )
255	254	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. CC |-> ( s - X ) ) e. ( CC -cn-> CC ) )
256	112, 200	sseldi 3507	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. CC )
257	256	snssd 4178	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> { ( Q ` i ) } C_ CC )
258	126, 257	jca 532	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC /\ { ( Q ` i ) } C_ CC ) )
259		unss 3683	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC /\ { ( Q ` i ) } C_ CC ) <-> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) C_ CC )
260	258, 259	sylib 196	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) C_ CC )
261	244, 255, 260, 127, 232	cncfmptssg 31531	. . . . . . . . . . . . . . 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 ) )
262	135, 142	eqeltrd 2555	. . . . . . . . . . . . . . . 16 |- ( ph -> ( D ` N ) e. ( RR -cn-> CC ) )
263	262	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( D ` N ) e. ( RR -cn-> CC ) )
264	261, 263	cncfco 21279	. . . . . . . . . . . . . 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 ) )
265	131	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> CC C_ CC )
266		eqid 2467	. . . . . . . . . . . . . . . 16 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
267		eqid 2467	. . . . . . . . . . . . . . . 16 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) )
268	266	cnfldtop 21159	. . . . . . . . . . . . . . . . . 18 |- ( TopOpen ` ℂfld ) e. Top
269		unicntop 31336	. . . . . . . . . . . . . . . . . . 19 |- CC = U. ( TopOpen ` ℂfld )
270	269	restid 14706	. . . . . . . . . . . . . . . . . 18 |- ( ( TopOpen ` ℂfld ) e. Top -> ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld ) )
271	268, 270	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld )
272	271	eqcomi 2480	. . . . . . . . . . . . . . . 16 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
273	266, 267, 272	cncfcn 21281	. . . . . . . . . . . . . . 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 ) ) )
274	260, 265, 273	syl2anc 661	. . . . . . . . . . . . . 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 ) ) )
275	264, 274	eleqtrd 2557	. . . . . . . . . . . . 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 ) ) )
276	243, 275	eqeltrd 2555	. . . . . . . . . . . 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 ) ) )
277	266	cnfldtopon 21158	. . . . . . . . . . . . . . 15 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
278	277	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( TopOpen ` ℂfld ) e. (TopOn ` CC ) )
279		resttopon 19530	. . . . . . . . . . . . . 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 ) } ) ) )
280	278, 260, 279	syl2anc 661	. . . . . . . . . . . . 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 ) } ) ) )
281		cncnp 19649	. . . . . . . . . . . . 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 ) ) ) )
282	280, 278, 281	syl2anc 661	. . . . . . . . . . . 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 ) ) ) )
283	276, 282	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 ) ) )
284	283	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 ) )
285		eqidd 2468	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( Q ` i ) )
286		elsncg 4056	. . . . . . . . . . . . . 14 |- ( ( Q ` i ) e. RR -> ( ( Q ` i ) e. { ( Q ` i ) } <-> ( Q ` i ) = ( Q ` i ) ) )
287	200, 286	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) e. { ( Q ` i ) } <-> ( Q ` i ) = ( Q ` i ) ) )
288	285, 287	mpbird 232	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. { ( Q ` i ) } )
289	288	olcd 393	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ ( Q ` i ) e. { ( Q ` i ) } ) )
290		elun 3650	. . . . . . . . . . 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 ) } ) )
291	289, 290	sylibr 212	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) )
292		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 ) ) )
293	292	eleq2d 2537	. . . . . . . . . . 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 ) ) ) )
294	293	rspccva 3218	. . . . . . . . . 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 ) ) )
295	284, 291, 294	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 ) ) )
296	215, 295	eqeltrd 2555	. . . . . . . 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