fourierdlem74

Description: Given a piecewise smooth function F , the derived function H has a limit at the upper bound of each interval of the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem74.xre	\|- ( ph -> X e. RR )
	fourierdlem74.p	\|- P = ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` m ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
	fourierdlem74.f	\|- ( ph -> F : RR --> RR )
	fourierdlem74.x	\|- ( ph -> X e. ran V )
	fourierdlem74.y	\|- ( ph -> Y e. RR )
	fourierdlem74.w	\|- ( ph -> W e. ( ( F \|` ( -oo (,) X ) ) limCC X ) )
	fourierdlem74.h	\|- H = ( s e. ( -u _pi [,] _pi ) \|-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
	fourierdlem74.m	\|- ( ph -> M e. NN )
	fourierdlem74.v	\|- ( ph -> V e. ( P ` M ) )
	fourierdlem74.r	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
	fourierdlem74.q	\|- Q = ( i e. ( 0 ... M ) \|-> ( ( V ` i ) - X ) )
	fourierdlem74.o	\|- O = ( 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 ) ) ) } )
	fourierdlem74.g	\|- G = ( RR _D F )
	fourierdlem74.gcn	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
	fourierdlem74.e	\|- ( ph -> E e. ( ( G \|` ( -oo (,) X ) ) limCC X ) )
	fourierdlem74.a	\|- A = if ( ( V ` ( i + 1 ) ) = X , E , ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) )
Assertion	fourierdlem74	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. ( ( H \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem74.xre	\|- ( ph -> X e. RR )
2		fourierdlem74.p	\|- P = ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` m ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
3		fourierdlem74.f	\|- ( ph -> F : RR --> RR )
4		fourierdlem74.x	\|- ( ph -> X e. ran V )
5		fourierdlem74.y	\|- ( ph -> Y e. RR )
6		fourierdlem74.w	\|- ( ph -> W e. ( ( F \|` ( -oo (,) X ) ) limCC X ) )
7		fourierdlem74.h	\|- H = ( s e. ( -u _pi [,] _pi ) \|-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
8		fourierdlem74.m	\|- ( ph -> M e. NN )
9		fourierdlem74.v	\|- ( ph -> V e. ( P ` M ) )
10		fourierdlem74.r	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
11		fourierdlem74.q	\|- Q = ( i e. ( 0 ... M ) \|-> ( ( V ` i ) - X ) )
12		fourierdlem74.o	\|- O = ( 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 ) ) ) } )
13		fourierdlem74.g	\|- G = ( RR _D F )
14		fourierdlem74.gcn	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
15		fourierdlem74.e	\|- ( ph -> E e. ( ( G \|` ( -oo (,) X ) ) limCC X ) )
16		fourierdlem74.a	\|- A = if ( ( V ` ( i + 1 ) ) = X , E , ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) )
17		elfzofz	\|- ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
18		pire	\|- _pi e. RR
19	18	renegcli	\|- -u _pi e. RR
20	19	a1i	\|- ( ph -> -u _pi e. RR )
21	20 1	readdcld	\|- ( ph -> ( -u _pi + X ) e. RR )
22	18	a1i	\|- ( ph -> _pi e. RR )
23	22 1	readdcld	\|- ( ph -> ( _pi + X ) e. RR )
24	21 23	iccssred	\|- ( ph -> ( ( -u _pi + X ) [,] ( _pi + X ) ) C_ RR )
25	24	adantr	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( -u _pi + X ) [,] ( _pi + X ) ) C_ RR )
26	2 8 9	fourierdlem15	\|- ( ph -> V : ( 0 ... M ) --> ( ( -u _pi + X ) [,] ( _pi + X ) ) )
27	26	ffvelcdmda	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( V ` i ) e. ( ( -u _pi + X ) [,] ( _pi + X ) ) )
28	25 27	sseldd	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( V ` i ) e. RR )
29	17 28	sylan2	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) e. RR )
30	29	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( V ` i ) e. RR )
31	1	ad2antrr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> X e. RR )
32	2	fourierdlem2	\|- ( M e. NN -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
33	8 32	syl	\|- ( ph -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
34	9 33	mpbid	\|- ( ph -> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) )
35	34	simprrd	\|- ( ph -> A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) )
36	35	r19.21bi	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) < ( V ` ( i + 1 ) ) )
37	36	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( V ` i ) < ( V ` ( i + 1 ) ) )
38		eqcom	\|- ( ( V ` ( i + 1 ) ) = X <-> X = ( V ` ( i + 1 ) ) )
39	38	bilani	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> X = ( V ` ( i + 1 ) ) )
40	37 39	breqtrrd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( V ` i ) < X )
41		ioossre	\|- ( ( V ` i ) (,) X ) C_ RR
42	41	a1i	\|- ( ph -> ( ( V ` i ) (,) X ) C_ RR )
43	3 42	fssresd	\|- ( ph -> ( F \|` ( ( V ` i ) (,) X ) ) : ( ( V ` i ) (,) X ) --> RR )
44	43	ad2antrr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( F \|` ( ( V ` i ) (,) X ) ) : ( ( V ` i ) (,) X ) --> RR )
45		limcresi	\|- ( ( F \|` ( -oo (,) X ) ) limCC X ) C_ ( ( ( F \|` ( -oo (,) X ) ) \|` ( ( V ` i ) (,) X ) ) limCC X )
46	45 6	sselid	\|- ( ph -> W e. ( ( ( F \|` ( -oo (,) X ) ) \|` ( ( V ` i ) (,) X ) ) limCC X ) )
47	46	adantr	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> W e. ( ( ( F \|` ( -oo (,) X ) ) \|` ( ( V ` i ) (,) X ) ) limCC X ) )
48		mnfxr	\|- -oo e. RR*
49	48	a1i	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> -oo e. RR* )
50	29	rexrd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) e. RR* )
51	29	mnfltd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> -oo < ( V ` i ) )
52	49 50 51	xrltled	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> -oo <_ ( V ` i ) )
53		iooss1	\|- ( ( -oo e. RR* /\ -oo <_ ( V ` i ) ) -> ( ( V ` i ) (,) X ) C_ ( -oo (,) X ) )
54	49 52 53	syl2anc	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` i ) (,) X ) C_ ( -oo (,) X ) )
55	54	resabs1d	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F \|` ( -oo (,) X ) ) \|` ( ( V ` i ) (,) X ) ) = ( F \|` ( ( V ` i ) (,) X ) ) )
56	55	oveq1d	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( F \|` ( -oo (,) X ) ) \|` ( ( V ` i ) (,) X ) ) limCC X ) = ( ( F \|` ( ( V ` i ) (,) X ) ) limCC X ) )
57	47 56	eleqtrd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> W e. ( ( F \|` ( ( V ` i ) (,) X ) ) limCC X ) )
58	57	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> W e. ( ( F \|` ( ( V ` i ) (,) X ) ) limCC X ) )
59		eqid	\|- ( RR _D ( F \|` ( ( V ` i ) (,) X ) ) ) = ( RR _D ( F \|` ( ( V ` i ) (,) X ) ) )
60		ax-resscn	\|- RR C_ CC
61	60	a1i	\|- ( ph -> RR C_ CC )
62	3 61	fssd	\|- ( ph -> F : RR --> CC )
63		ssid	\|- RR C_ RR
64	63	a1i	\|- ( ph -> RR C_ RR )
65		eqid	\|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
66		tgioo4	\|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) \|`t RR )
67	65 66	dvres	\|- ( ( ( RR C_ CC /\ F : RR --> CC ) /\ ( RR C_ RR /\ ( ( V ` i ) (,) X ) C_ RR ) ) -> ( RR _D ( F \|` ( ( V ` i ) (,) X ) ) ) = ( ( RR _D F ) \|` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( V ` i ) (,) X ) ) ) )
68	61 62 64 42 67	syl22anc	\|- ( ph -> ( RR _D ( F \|` ( ( V ` i ) (,) X ) ) ) = ( ( RR _D F ) \|` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( V ` i ) (,) X ) ) ) )
69	13	eqcomi	\|- ( RR _D F ) = G
70		ioontr	\|- ( ( int ` ( topGen ` ran (,) ) ) ` ( ( V ` i ) (,) X ) ) = ( ( V ` i ) (,) X )
71	69 70	reseq12i	\|- ( ( RR _D F ) \|` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( V ` i ) (,) X ) ) ) = ( G \|` ( ( V ` i ) (,) X ) )
72	71	a1i	\|- ( ph -> ( ( RR _D F ) \|` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( V ` i ) (,) X ) ) ) = ( G \|` ( ( V ` i ) (,) X ) ) )
73	68 72	eqtrd	\|- ( ph -> ( RR _D ( F \|` ( ( V ` i ) (,) X ) ) ) = ( G \|` ( ( V ` i ) (,) X ) ) )
74	73	dmeqd	\|- ( ph -> dom ( RR _D ( F \|` ( ( V ` i ) (,) X ) ) ) = dom ( G \|` ( ( V ` i ) (,) X ) ) )
75	74	ad2antrr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> dom ( RR _D ( F \|` ( ( V ` i ) (,) X ) ) ) = dom ( G \|` ( ( V ` i ) (,) X ) ) )
76	14	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( G \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
77		oveq2	\|- ( ( V ` ( i + 1 ) ) = X -> ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) = ( ( V ` i ) (,) X ) )
78	77	reseq2d	\|- ( ( V ` ( i + 1 ) ) = X -> ( G \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) = ( G \|` ( ( V ` i ) (,) X ) ) )
79	78 77	feq12d	\|- ( ( V ` ( i + 1 ) ) = X -> ( ( G \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR <-> ( G \|` ( ( V ` i ) (,) X ) ) : ( ( V ` i ) (,) X ) --> RR ) )
80	79	adantl	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( ( G \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR <-> ( G \|` ( ( V ` i ) (,) X ) ) : ( ( V ` i ) (,) X ) --> RR ) )
81	76 80	mpbid	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( G \|` ( ( V ` i ) (,) X ) ) : ( ( V ` i ) (,) X ) --> RR )
82		fdm	\|- ( ( G \|` ( ( V ` i ) (,) X ) ) : ( ( V ` i ) (,) X ) --> RR -> dom ( G \|` ( ( V ` i ) (,) X ) ) = ( ( V ` i ) (,) X ) )
83	81 82	syl	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> dom ( G \|` ( ( V ` i ) (,) X ) ) = ( ( V ` i ) (,) X ) )
84	75 83	eqtrd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> dom ( RR _D ( F \|` ( ( V ` i ) (,) X ) ) ) = ( ( V ` i ) (,) X ) )
85		limcresi	\|- ( ( G \|` ( -oo (,) X ) ) limCC X ) C_ ( ( ( G \|` ( -oo (,) X ) ) \|` ( ( V ` i ) (,) X ) ) limCC X )
86	54	resabs1d	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( G \|` ( -oo (,) X ) ) \|` ( ( V ` i ) (,) X ) ) = ( G \|` ( ( V ` i ) (,) X ) ) )
87	86	oveq1d	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( G \|` ( -oo (,) X ) ) \|` ( ( V ` i ) (,) X ) ) limCC X ) = ( ( G \|` ( ( V ` i ) (,) X ) ) limCC X ) )
88	85 87	sseqtrid	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( G \|` ( -oo (,) X ) ) limCC X ) C_ ( ( G \|` ( ( V ` i ) (,) X ) ) limCC X ) )
89	15	adantr	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> E e. ( ( G \|` ( -oo (,) X ) ) limCC X ) )
90	88 89	sseldd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> E e. ( ( G \|` ( ( V ` i ) (,) X ) ) limCC X ) )
91	68 72	eqtr2d	\|- ( ph -> ( G \|` ( ( V ` i ) (,) X ) ) = ( RR _D ( F \|` ( ( V ` i ) (,) X ) ) ) )
92	91	oveq1d	\|- ( ph -> ( ( G \|` ( ( V ` i ) (,) X ) ) limCC X ) = ( ( RR _D ( F \|` ( ( V ` i ) (,) X ) ) ) limCC X ) )
93	92	adantr	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( G \|` ( ( V ` i ) (,) X ) ) limCC X ) = ( ( RR _D ( F \|` ( ( V ` i ) (,) X ) ) ) limCC X ) )
94	90 93	eleqtrd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> E e. ( ( RR _D ( F \|` ( ( V ` i ) (,) X ) ) ) limCC X ) )
95	94	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> E e. ( ( RR _D ( F \|` ( ( V ` i ) (,) X ) ) ) limCC X ) )
96		eqid	\|- ( s e. ( ( ( V ` i ) - X ) (,) 0 ) \|-> ( ( ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) ) = ( s e. ( ( ( V ` i ) - X ) (,) 0 ) \|-> ( ( ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) )
97		oveq2	\|- ( x = s -> ( X + x ) = ( X + s ) )
98	97	fveq2d	\|- ( x = s -> ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + x ) ) = ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) )
99	98	oveq1d	\|- ( x = s -> ( ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + x ) ) - W ) = ( ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) )
100	99	cbvmptv	\|- ( x e. ( ( ( V ` i ) - X ) (,) 0 ) \|-> ( ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + x ) ) - W ) ) = ( s e. ( ( ( V ` i ) - X ) (,) 0 ) \|-> ( ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) )
101		id	\|- ( x = s -> x = s )
102	101	cbvmptv	\|- ( x e. ( ( ( V ` i ) - X ) (,) 0 ) \|-> x ) = ( s e. ( ( ( V ` i ) - X ) (,) 0 ) \|-> s )
103	30 31 40 44 58 59 84 95 96 100 102	fourierdlem60	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> E e. ( ( s e. ( ( ( V ` i ) - X ) (,) 0 ) \|-> ( ( ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) ) limCC 0 ) )
104		iftrue	\|- ( ( V ` ( i + 1 ) ) = X -> if ( ( V ` ( i + 1 ) ) = X , E , ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) ) = E )
105	16 104	eqtrid	\|- ( ( V ` ( i + 1 ) ) = X -> A = E )
106	105	adantl	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> A = E )
107	7	reseq1i	\|- ( H \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( s e. ( -u _pi [,] _pi ) \|-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
108	107	a1i	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( H \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( s e. ( -u _pi [,] _pi ) \|-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
109		ioossicc	\|- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
110	19	rexri	\|- -u _pi e. RR*
111	110	a1i	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> -u _pi e. RR* )
112	18	rexri	\|- _pi e. RR*
113	112	a1i	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> _pi e. RR* )
114	19	a1i	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> -u _pi e. RR )
115	18	a1i	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> _pi e. RR )
116	1	adantr	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> X e. RR )
117	28 116	resubcld	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) - X ) e. RR )
118	20	recnd	\|- ( ph -> -u _pi e. CC )
119	1	recnd	\|- ( ph -> X e. CC )
120	118 119	pncand	\|- ( ph -> ( ( -u _pi + X ) - X ) = -u _pi )
121	120	eqcomd	\|- ( ph -> -u _pi = ( ( -u _pi + X ) - X ) )
122	121	adantr	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> -u _pi = ( ( -u _pi + X ) - X ) )
123	21	adantr	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( -u _pi + X ) e. RR )
124	23	adantr	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( _pi + X ) e. RR )
125		elicc2	\|- ( ( ( -u _pi + X ) e. RR /\ ( _pi + X ) e. RR ) -> ( ( V ` i ) e. ( ( -u _pi + X ) [,] ( _pi + X ) ) <-> ( ( V ` i ) e. RR /\ ( -u _pi + X ) <_ ( V ` i ) /\ ( V ` i ) <_ ( _pi + X ) ) ) )
126	123 124 125	syl2anc	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) e. ( ( -u _pi + X ) [,] ( _pi + X ) ) <-> ( ( V ` i ) e. RR /\ ( -u _pi + X ) <_ ( V ` i ) /\ ( V ` i ) <_ ( _pi + X ) ) ) )
127	27 126	mpbid	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) e. RR /\ ( -u _pi + X ) <_ ( V ` i ) /\ ( V ` i ) <_ ( _pi + X ) ) )
128	127	simp2d	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( -u _pi + X ) <_ ( V ` i ) )
129	123 28 116 128	lesub1dd	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( -u _pi + X ) - X ) <_ ( ( V ` i ) - X ) )
130	122 129	eqbrtrd	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> -u _pi <_ ( ( V ` i ) - X ) )
131	127	simp3d	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( V ` i ) <_ ( _pi + X ) )
132	28 124 116 131	lesub1dd	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) - X ) <_ ( ( _pi + X ) - X ) )
133	115	recnd	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> _pi e. CC )
134	119	adantr	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> X e. CC )
135	133 134	pncand	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( _pi + X ) - X ) = _pi )
136	132 135	breqtrd	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) - X ) <_ _pi )
137	114 115 117 130 136	eliccd	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) - X ) e. ( -u _pi [,] _pi ) )
138	137 11	fmptd	\|- ( ph -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
139	138	adantr	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
140		simpr	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
141	111 113 139 140	fourierdlem8	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
142	109 141	sstrid	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
143	142	resmptd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( s e. ( -u _pi [,] _pi ) \|-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) )
144	143	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( ( s e. ( -u _pi [,] _pi ) \|-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) )
145	17	adantl	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
146	17 117	sylan2	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` i ) - X ) e. RR )
147	11	fvmpt2	\|- ( ( i e. ( 0 ... M ) /\ ( ( V ` i ) - X ) e. RR ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
148	145 146 147	syl2anc	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
149	148	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
150		fveq2	\|- ( i = j -> ( V ` i ) = ( V ` j ) )
151	150	oveq1d	\|- ( i = j -> ( ( V ` i ) - X ) = ( ( V ` j ) - X ) )
152	151	cbvmptv	\|- ( i e. ( 0 ... M ) \|-> ( ( V ` i ) - X ) ) = ( j e. ( 0 ... M ) \|-> ( ( V ` j ) - X ) )
153	11 152	eqtri	\|- Q = ( j e. ( 0 ... M ) \|-> ( ( V ` j ) - X ) )
154	153	a1i	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q = ( j e. ( 0 ... M ) \|-> ( ( V ` j ) - X ) ) )
155		fveq2	\|- ( j = ( i + 1 ) -> ( V ` j ) = ( V ` ( i + 1 ) ) )
156	155	oveq1d	\|- ( j = ( i + 1 ) -> ( ( V ` j ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
157	156	adantl	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( V ` j ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
158		fzofzp1	\|- ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
159	158	adantl	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
160	34	simpld	\|- ( ph -> V e. ( RR ^m ( 0 ... M ) ) )
161		elmapi	\|- ( V e. ( RR ^m ( 0 ... M ) ) -> V : ( 0 ... M ) --> RR )
162	160 161	syl	\|- ( ph -> V : ( 0 ... M ) --> RR )
163	162	adantr	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> V : ( 0 ... M ) --> RR )
164	163 159	ffvelcdmd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` ( i + 1 ) ) e. RR )
165	1	adantr	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. RR )
166	164 165	resubcld	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` ( i + 1 ) ) - X ) e. RR )
167	154 157 159 166	fvmptd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
168	167	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
169		oveq1	\|- ( ( V ` ( i + 1 ) ) = X -> ( ( V ` ( i + 1 ) ) - X ) = ( X - X ) )
170	169	adantl	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( ( V ` ( i + 1 ) ) - X ) = ( X - X ) )
171	119	ad2antrr	\|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> X e. CC )
172	171	subidd	\|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( X - X ) = 0 )
173	17 172	sylanl2	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( X - X ) = 0 )
174	168 170 173	3eqtrd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( Q ` ( i + 1 ) ) = 0 )
175	149 174	oveq12d	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( ( V ` i ) - X ) (,) 0 ) )
176		simplr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = 0 ) -> s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
177	8	adantr	\|- ( ( ph /\ s = 0 ) -> M e. NN )
178	20 22 1 2 12 8 9 11	fourierdlem14	\|- ( ph -> Q e. ( O ` M ) )
179	178	adantr	\|- ( ( ph /\ s = 0 ) -> Q e. ( O ` M ) )
180		simpr	\|- ( ( ph /\ s = 0 ) -> s = 0 )
181		ffn	\|- ( V : ( 0 ... M ) --> ( ( -u _pi + X ) [,] ( _pi + X ) ) -> V Fn ( 0 ... M ) )
182		fvelrnb	\|- ( V Fn ( 0 ... M ) -> ( X e. ran V <-> E. i e. ( 0 ... M ) ( V ` i ) = X ) )
183	26 181 182	3syl	\|- ( ph -> ( X e. ran V <-> E. i e. ( 0 ... M ) ( V ` i ) = X ) )
184	4 183	mpbid	\|- ( ph -> E. i e. ( 0 ... M ) ( V ` i ) = X )
185		simpr	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> i e. ( 0 ... M ) )
186	11	fvmpt2	\|- ( ( i e. ( 0 ... M ) /\ ( ( V ` i ) - X ) e. ( -u _pi [,] _pi ) ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
187	185 137 186	syl2anc	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
188	187	adantr	\|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` i ) = X ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
189		oveq1	\|- ( ( V ` i ) = X -> ( ( V ` i ) - X ) = ( X - X ) )
190	189	adantl	\|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` i ) = X ) -> ( ( V ` i ) - X ) = ( X - X ) )
191	119	subidd	\|- ( ph -> ( X - X ) = 0 )
192	191	ad2antrr	\|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` i ) = X ) -> ( X - X ) = 0 )
193	188 190 192	3eqtrd	\|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` i ) = X ) -> ( Q ` i ) = 0 )
194	193	ex	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) = X -> ( Q ` i ) = 0 ) )
195	194	reximdva	\|- ( ph -> ( E. i e. ( 0 ... M ) ( V ` i ) = X -> E. i e. ( 0 ... M ) ( Q ` i ) = 0 ) )
196	184 195	mpd	\|- ( ph -> E. i e. ( 0 ... M ) ( Q ` i ) = 0 )
197	117 11	fmptd	\|- ( ph -> Q : ( 0 ... M ) --> RR )
198		ffn	\|- ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
199		fvelrnb	\|- ( Q Fn ( 0 ... M ) -> ( 0 e. ran Q <-> E. i e. ( 0 ... M ) ( Q ` i ) = 0 ) )
200	197 198 199	3syl	\|- ( ph -> ( 0 e. ran Q <-> E. i e. ( 0 ... M ) ( Q ` i ) = 0 ) )
201	196 200	mpbird	\|- ( ph -> 0 e. ran Q )
202	201	adantr	\|- ( ( ph /\ s = 0 ) -> 0 e. ran Q )
203	180 202	eqeltrd	\|- ( ( ph /\ s = 0 ) -> s e. ran Q )
204	12 177 179 203	fourierdlem12	\|- ( ( ( ph /\ s = 0 ) /\ i e. ( 0 ..^ M ) ) -> -. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
205	204	an32s	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s = 0 ) -> -. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
206	205	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = 0 ) -> -. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
207	176 206	pm2.65da	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. s = 0 )
208	207	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. s = 0 )
209	208	iffalsed	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) )
210		elioore	\|- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. RR )
211	210	adantl	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
212		0red	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> 0 e. RR )
213		elioo3g	\|- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ s e. RR* ) /\ ( ( Q ` i ) < s /\ s < ( Q ` ( i + 1 ) ) ) ) )
214	213	biimpi	\|- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ s e. RR* ) /\ ( ( Q ` i ) < s /\ s < ( Q ` ( i + 1 ) ) ) ) )
215	214	simprrd	\|- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s < ( Q ` ( i + 1 ) ) )
216	215	adantl	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s < ( Q ` ( i + 1 ) ) )
217	174	adantr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) = 0 )
218	216 217	breqtrd	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s < 0 )
219	211 212 218	ltnsymd	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. 0 < s )
220	219	iffalsed	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( 0 < s , Y , W ) = W )
221	220	oveq2d	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) = ( ( F ` ( X + s ) ) - W ) )
222	221	oveq1d	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) = ( ( ( F ` ( X + s ) ) - W ) / s ) )
223	50	ad2antrr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) e. RR* )
224	1	rexrd	\|- ( ph -> X e. RR* )
225	224	ad3antrrr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR* )
226	165	ad2antrr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
227	226 211	readdcld	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) e. RR )
228	119	adantr	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. CC )
229		iccssre	\|- ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR )
230	19 18 229	mp2an	\|- ( -u _pi [,] _pi ) C_ RR
231	230 60	sstri	\|- ( -u _pi [,] _pi ) C_ CC
232	187 137	eqeltrd	\|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. ( -u _pi [,] _pi ) )
233	17 232	sylan2	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( -u _pi [,] _pi ) )
234	231 233	sselid	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
235	228 234	addcomd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( Q ` i ) ) = ( ( Q ` i ) + X ) )
236	148	oveq1d	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + X ) = ( ( ( V ` i ) - X ) + X ) )
237	29	recnd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) e. CC )
238	237 228	npcand	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( V ` i ) - X ) + X ) = ( V ` i ) )
239	235 236 238	3eqtrrd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) = ( X + ( Q ` i ) ) )
240	239	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) = ( X + ( Q ` i ) ) )
241	148 146	eqeltrd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
242	241	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
243	210	adantl	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
244	1	ad2antrr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
245	214	simprld	\|- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) < s )
246	245	adantl	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < s )
247	242 243 244 246	ltadd2dd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + ( Q ` i ) ) < ( X + s ) )
248	240 247	eqbrtrd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) < ( X + s ) )
249	248	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) < ( X + s ) )
250		ltaddneg	\|- ( ( s e. RR /\ X e. RR ) -> ( s < 0 <-> ( X + s ) < X ) )
251	211 226 250	syl2anc	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( s < 0 <-> ( X + s ) < X ) )
252	218 251	mpbid	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) < X )
253	223 225 227 249 252	eliood	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) e. ( ( V ` i ) (,) X ) )
254		fvres	\|- ( ( X + s ) e. ( ( V ` i ) (,) X ) -> ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) = ( F ` ( X + s ) ) )
255	254	eqcomd	\|- ( ( X + s ) e. ( ( V ` i ) (,) X ) -> ( F ` ( X + s ) ) = ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) )
256	253 255	syl	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) = ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) )
257	256	oveq1d	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` ( X + s ) ) - W ) = ( ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) )
258	257	oveq1d	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F ` ( X + s ) ) - W ) / s ) = ( ( ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) )
259	209 222 258	3eqtrd	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) = ( ( ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) )
260	175 259	mpteq12dva	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) = ( s e. ( ( ( V ` i ) - X ) (,) 0 ) \|-> ( ( ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) ) )
261	108 144 260	3eqtrd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( H \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( ( V ` i ) - X ) (,) 0 ) \|-> ( ( ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) ) )
262	261 174	oveq12d	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( ( H \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( s e. ( ( ( V ` i ) - X ) (,) 0 ) \|-> ( ( ( ( F \|` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) ) limCC 0 ) )
263	103 106 262	3eltr4d	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> A e. ( ( H \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
264		eqid	\|- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) )
265		eqid	\|- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> s ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> s )
266		eqid	\|- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) )
267	3	adantr	\|- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> F : RR --> RR )
268	1	adantr	\|- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
269	210	adantl	\|- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
270	268 269	readdcld	\|- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) e. RR )
271	267 270	ffvelcdmd	\|- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. RR )
272	271	recnd	\|- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. CC )
273	272	adantlr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. CC )
274	273	3adantl3	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. CC )
275	5	recnd	\|- ( ph -> Y e. CC )
276		limccl	\|- ( ( F \|` ( -oo (,) X ) ) limCC X ) C_ CC
277	276 6	sselid	\|- ( ph -> W e. CC )
278	275 277	ifcld	\|- ( ph -> if ( 0 < s , Y , W ) e. CC )
279	278	adantr	\|- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( 0 < s , Y , W ) e. CC )
280	279	3ad2antl1	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( 0 < s , Y , W ) e. CC )
281	274 280	subcld	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) e. CC )
282	210	recnd	\|- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. CC )
283	282	adantl	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. CC )
284		velsn	\|- ( s e. { 0 } <-> s = 0 )
285	207 284	sylnibr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. s e. { 0 } )
286	285	3adantl3	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. s e. { 0 } )
287	283 286	eldifd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. ( CC \ { 0 } ) )
288		eqid	\|- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( F ` ( X + s ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( F ` ( X + s ) ) )
289		eqid	\|- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> W ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> W )
290		eqid	\|- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - W ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - W ) )
291	277	ad2antrr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> W e. CC )
292	3	adantr	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> F : RR --> RR )
293		ioossre	\|- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
294	293	a1i	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
295	50	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) e. RR* )
296	164	rexrd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` ( i + 1 ) ) e. RR* )
297	296	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` ( i + 1 ) ) e. RR* )
298	270	adantlr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) e. RR )
299	197	adantr	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
300	299 159	ffvelcdmd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
301	300	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
302	215	adantl	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s < ( Q ` ( i + 1 ) ) )
303	243 301 244 302	ltadd2dd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) < ( X + ( Q ` ( i + 1 ) ) ) )
304	167	oveq2d	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( Q ` ( i + 1 ) ) ) = ( X + ( ( V ` ( i + 1 ) ) - X ) ) )
305	164	recnd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` ( i + 1 ) ) e. CC )
306	228 305	pncan3d	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( ( V ` ( i + 1 ) ) - X ) ) = ( V ` ( i + 1 ) ) )
307	304 306	eqtrd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( Q ` ( i + 1 ) ) ) = ( V ` ( i + 1 ) ) )
308	307	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + ( Q ` ( i + 1 ) ) ) = ( V ` ( i + 1 ) ) )
309	303 308	breqtrd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) < ( V ` ( i + 1 ) ) )
310	295 297 298 248 309	eliood	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
311		ioossre	\|- ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ RR
312	311	a1i	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ RR )
313	243 302	ltned	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s =/= ( Q ` ( i + 1 ) ) )
314	307	eqcomd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` ( i + 1 ) ) = ( X + ( Q ` ( i + 1 ) ) ) )
315	314	oveq2d	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) = ( ( F \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( X + ( Q ` ( i + 1 ) ) ) ) )
316	10 315	eleqtrd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( X + ( Q ` ( i + 1 ) ) ) ) )
317	300	recnd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
318	292 165 294 288 310 312 313 316 317	fourierdlem53	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( F ` ( X + s ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
319		ioosscn	\|- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
320	319	a1i	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
321	277	adantr	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> W e. CC )
322	289 320 321 317	constlimc	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> W e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> W ) limCC ( Q ` ( i + 1 ) ) ) )
323	288 289 290 273 291 318 322	sublimc	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( R - W ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - W ) ) limCC ( Q ` ( i + 1 ) ) ) )
324	323	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( R - W ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - W ) ) limCC ( Q ` ( i + 1 ) ) ) )
325		iftrue	\|- ( ( V ` ( i + 1 ) ) < X -> if ( ( V ` ( i + 1 ) ) < X , W , Y ) = W )
326	325	oveq2d	\|- ( ( V ` ( i + 1 ) ) < X -> ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) = ( R - W ) )
327	326	adantl	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) = ( R - W ) )
328	210	adantl	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
329		0red	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> 0 e. RR )
330	300	ad2antrr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
331	215	adantl	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s < ( Q ` ( i + 1 ) ) )
332	167	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
333	164	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( V ` ( i + 1 ) ) e. RR )
334	1	ad2antrr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> X e. RR )
335		simpr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( V ` ( i + 1 ) ) < X )
336	333 334 335	ltled	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( V ` ( i + 1 ) ) <_ X )
337	333 334	suble0d	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( ( ( V ` ( i + 1 ) ) - X ) <_ 0 <-> ( V ` ( i + 1 ) ) <_ X ) )
338	336 337	mpbird	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( ( V ` ( i + 1 ) ) - X ) <_ 0 )
339	332 338	eqbrtrd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( Q ` ( i + 1 ) ) <_ 0 )
340	339	adantr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) <_ 0 )
341	328 330 329 331 340	ltletrd	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s < 0 )
342	328 329 341	ltnsymd	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. 0 < s )
343	342	iffalsed	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( 0 < s , Y , W ) = W )
344	343	oveq2d	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) = ( ( F ` ( X + s ) ) - W ) )
345	344	mpteq2dva	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - W ) ) )
346	345	oveq1d	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - W ) ) limCC ( Q ` ( i + 1 ) ) ) )
347	324 327 346	3eltr4d	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
348	347	3adantl3	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ ( V ` ( i + 1 ) ) < X ) -> ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
349		simpl1	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> ph )
350		simpl2	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> i e. ( 0 ..^ M ) )
351	1	ad2antrr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. ( V ` ( i + 1 ) ) < X ) -> X e. RR )
352	351	3adantl3	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> X e. RR )
353	164	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. ( V ` ( i + 1 ) ) < X ) -> ( V ` ( i + 1 ) ) e. RR )
354	353	3adantl3	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> ( V ` ( i + 1 ) ) e. RR )
355		neqne	\|- ( -. ( V ` ( i + 1 ) ) = X -> ( V ` ( i + 1 ) ) =/= X )
356	355	necomd	\|- ( -. ( V ` ( i + 1 ) ) = X -> X =/= ( V ` ( i + 1 ) ) )
357	356	adantr	\|- ( ( -. ( V ` ( i + 1 ) ) = X /\ -. ( V ` ( i + 1 ) ) < X ) -> X =/= ( V ` ( i + 1 ) ) )
358	357	3ad2antl3	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> X =/= ( V ` ( i + 1 ) ) )
359		simpr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> -. ( V ` ( i + 1 ) ) < X )
360	352 354 358 359	lttri5d	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> X < ( V ` ( i + 1 ) ) )
361		eqid	\|- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> if ( 0 < s , Y , W ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> if ( 0 < s , Y , W ) )
362	273	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. CC )
363	278	ad3antrrr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( 0 < s , Y , W ) e. CC )
364	318	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> R e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( F ` ( X + s ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
365		eqid	\|- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> Y ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> Y )
366	275	adantr	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> Y e. CC )
367	365 320 366 317	constlimc	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> Y e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> Y ) limCC ( Q ` ( i + 1 ) ) ) )
368	367	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> Y e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> Y ) limCC ( Q ` ( i + 1 ) ) ) )
369	1	ad2antrr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> X e. RR )
370	164	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> ( V ` ( i + 1 ) ) e. RR )
371		simpr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> X < ( V ` ( i + 1 ) ) )
372	369 370 371	ltnsymd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> -. ( V ` ( i + 1 ) ) < X )
373	372	iffalsed	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> if ( ( V ` ( i + 1 ) ) < X , W , Y ) = Y )
374		0red	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> 0 e. RR )
375	241	ad2antrr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
376	210	adantl	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
377	191	eqcomd	\|- ( ph -> 0 = ( X - X ) )
378	377	ad2antrr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> 0 = ( X - X ) )
379	29	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> ( V ` i ) e. RR )
380	50	ad2antrr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ -. X <_ ( V ` i ) ) -> ( V ` i ) e. RR* )
381	296	ad2antrr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ -. X <_ ( V ` i ) ) -> ( V ` ( i + 1 ) ) e. RR* )
382	165	ad2antrr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ -. X <_ ( V ` i ) ) -> X e. RR )
383		simpr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. X <_ ( V ` i ) ) -> -. X <_ ( V ` i ) )
384	29	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. X <_ ( V ` i ) ) -> ( V ` i ) e. RR )
385	1	ad2antrr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. X <_ ( V ` i ) ) -> X e. RR )
386	384 385	ltnled	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. X <_ ( V ` i ) ) -> ( ( V ` i ) < X <-> -. X <_ ( V ` i ) ) )
387	383 386	mpbird	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. X <_ ( V ` i ) ) -> ( V ` i ) < X )
388	387	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ -. X <_ ( V ` i ) ) -> ( V ` i ) < X )
389		simplr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ -. X <_ ( V ` i ) ) -> X < ( V ` ( i + 1 ) ) )
390	380 381 382 388 389	eliood	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ -. X <_ ( V ` i ) ) -> X e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
391	2 8 9 4	fourierdlem12	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> -. X e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
392	391	ad2antrr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ -. X <_ ( V ` i ) ) -> -. X e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
393	390 392	condan	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> X <_ ( V ` i ) )
394	369 379 369 393	lesub1dd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> ( X - X ) <_ ( ( V ` i ) - X ) )
395	378 394	eqbrtrd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> 0 <_ ( ( V ` i ) - X ) )
396	148	eqcomd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` i ) - X ) = ( Q ` i ) )
397	396	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> ( ( V ` i ) - X ) = ( Q ` i ) )
398	395 397	breqtrd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> 0 <_ ( Q ` i ) )
399	398	adantr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> 0 <_ ( Q ` i ) )
400	245	adantl	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < s )
401	374 375 376 399 400	lelttrd	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> 0 < s )
402	401	iftrued	\|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( 0 < s , Y , W ) = Y )
403	402	mpteq2dva	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> if ( 0 < s , Y , W ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> Y ) )
404	403	oveq1d	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> if ( 0 < s , Y , W ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> Y ) limCC ( Q ` ( i + 1 ) ) ) )
405	368 373 404	3eltr4d	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> if ( ( V ` ( i + 1 ) ) < X , W , Y ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> if ( 0 < s , Y , W ) ) limCC ( Q ` ( i + 1 ) ) ) )
406	288 361 264 362 363 364 405	sublimc	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
407	349 350 360 406	syl21anc	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
408	348 407	pm2.61dan	\|- ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
409	320 265 317	idlimc	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> s ) limCC ( Q ` ( i + 1 ) ) ) )
410	409	3adant3	\|- ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( Q ` ( i + 1 ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> s ) limCC ( Q ` ( i + 1 ) ) ) )
411	167	3adant3	\|- ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
412	305	3adant3	\|- ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( V ` ( i + 1 ) ) e. CC )
413	228	3adant3	\|- ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> X e. CC )
414	355	3ad2ant3	\|- ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( V ` ( i + 1 ) ) =/= X )
415	412 413 414	subne0d	\|- ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( ( V ` ( i + 1 ) ) - X ) =/= 0 )
416	411 415	eqnetrd	\|- ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( Q ` ( i + 1 ) ) =/= 0 )
417	207	3adantl3	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. s = 0 )
418	417	neqned	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s =/= 0 )
419	264 265 266 281 287 408 410 416 418	divlimc	\|- ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) limCC ( Q ` ( i + 1 ) ) ) )
420		iffalse	\|- ( -. ( V ` ( i + 1 ) ) = X -> if ( ( V ` ( i + 1 ) ) = X , E , ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) ) = ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) )
421	16 420	eqtrid	\|- ( -. ( V ` ( i + 1 ) ) = X -> A = ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) )
422	421	3ad2ant3	\|- ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> A = ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) )
423		ioossre	\|- ( -oo (,) X ) C_ RR
424	423	a1i	\|- ( ph -> ( -oo (,) X ) C_ RR )
425	3 424	fssresd	\|- ( ph -> ( F \|` ( -oo (,) X ) ) : ( -oo (,) X ) --> RR )
426	423 61	sstrid	\|- ( ph -> ( -oo (,) X ) C_ CC )
427	48	a1i	\|- ( ph -> -oo e. RR* )
428	1	mnfltd	\|- ( ph -> -oo < X )
429	65 427 1 428	lptioo2cn	\|- ( ph -> X e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( -oo (,) X ) ) )
430	425 426 429 6	limcrecl	\|- ( ph -> W e. RR )
431	3 1 5 430 7	fourierdlem9	\|- ( ph -> H : ( -u _pi [,] _pi ) --> RR )
432	431	adantr	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> H : ( -u _pi [,] _pi ) --> RR )
433	432 142	feqresmpt	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( H ` s ) ) )
434	142	sselda	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. ( -u _pi [,] _pi ) )
435		0cnd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> 0 e. CC )
436	278	ad2antrr	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( 0 < s , Y , W ) e. CC )
437	273 436	subcld	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) e. CC )
438	282	adantl	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. CC )
439	207	neqned	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s =/= 0 )
440	437 438 439	divcld	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) e. CC )
441	435 440	ifcld	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) e. CC )
442	7	fvmpt2	\|- ( ( s e. ( -u _pi [,] _pi ) /\ if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) e. CC ) -> ( H ` s ) = if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
443	434 441 442	syl2anc	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( H ` s ) = if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
444	207	iffalsed	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) )
445	443 444	eqtrd	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( H ` s ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) )
446	445	mpteq2dva	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( H ` s ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
447	433 446	eqtrd	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
448	447	3adant3	\|- ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( H \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
449	448	oveq1d	\|- ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( ( H \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \|-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) limCC ( Q ` ( i + 1 ) ) ) )
450	419 422 449	3eltr4d	\|- ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> A e. ( ( H \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
451	450	3expa	\|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. ( V ` ( i + 1 ) ) = X ) -> A e. ( ( H \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
452	263 451	pm2.61dan	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. ( ( H \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )

Metamath Proof Explorer

Theorem fourierdlem74

Proof