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