Theorem fourierdlem75

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

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

Proof

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