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