Theorem fourierdlem81 38152

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by its period T. In this lemma, T is assumed to be strictly positive. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem81.a	|- ( ph -> A e. RR )
fourierdlem81.b	|- ( ph -> B e. RR )
fourierdlem81.p	|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem81.m	|- ( ph -> M e. NN )
fourierdlem81.t	|- ( ph -> T e. RR+ )
fourierdlem81.q	|- ( ph -> Q e. ( P ` M ) )
fourierdlem81.fper	|- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem81.s	|- S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) )
fourierdlem81.f	|- ( ph -> F : RR --> CC )
fourierdlem81.cncf	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem81.r	|- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
fourierdlem81.l	|- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
fourierdlem81.g	|- G = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) )
fourierdlem81.h	|- H = ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> ( G ` ( x - T ) ) )

Assertion

Ref	Expression
fourierdlem81	|- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )

Distinct variable groups:   A, i, m, p   x, A, i   B, i, m, p   x, B   i, F, x   x, G   x, L   i, M, m, p   x, M   Q, i, p   x, Q   x, R   S, i, x   T, i, x   ph, i, x

Allowed substitution hints:   ph( m, p)   P( x, i, m, p)   Q( m)   R( i, m, p)   S( m, p)   T( m, p)   F( m, p)   G( i, m, p)   H( x, i, m, p)   L( i, m, p)

Proof of Theorem fourierdlem81

Dummy variables y w z j are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem81.q	. . . . . . . . 9 |- ( ph -> Q e. ( P ` M ) )
2		fourierdlem81.m	. . . . . . . . . 10 |- ( ph -> M e. NN )
3		fourierdlem81.p	. . . . . . . . . . 11 |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
4	3	fourierdlem2 38072	. . . . . . . . . 10 |- ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
5	2, 4	syl 17	. . . . . . . . 9 |- ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
6	1, 5	mpbid 215	. . . . . . . 8 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
7	6	simprd 469	. . . . . . 7 |- ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
8	7	simpld 465	. . . . . 6 |- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
9	8	simpld 465	. . . . 5 |- ( ph -> ( Q ` 0 ) = A )
10	9	eqcomd 2468	. . . 4 |- ( ph -> A = ( Q ` 0 ) )
11	8	simprd 469	. . . . 5 |- ( ph -> ( Q ` M ) = B )
12	11	eqcomd 2468	. . . 4 |- ( ph -> B = ( Q ` M ) )
13	10, 12	oveq12d 6338	. . 3 |- ( ph -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
14	13	itgeq1d 37919	. 2 |- ( ph -> S. ( A [,] B ) ( F ` x ) _d x = S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( F ` x ) _d x )
15		0zd 10983	. . 3 |- ( ph -> 0 e. ZZ )
16		nnuz 11228	. . . . 5 |- NN = ( ZZ>= ` 1 )
17		0p1e1 10754	. . . . . 6 |- ( 0 + 1 ) = 1
18	17	fveq2i 5895	. . . . 5 |- ( ZZ>= ` ( 0 + 1 ) ) = ( ZZ>= ` 1 )
19	16, 18	eqtr4i 2487	. . . 4 |- NN = ( ZZ>= ` ( 0 + 1 ) )
20	2, 19	syl6eleq 2550	. . 3 |- ( ph -> M e. ( ZZ>= ` ( 0 + 1 ) ) )
21	6	simpld 465	. . . 4 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
22		reex 9661	. . . . . 6 |- RR e. _V
23	22	a1i 11	. . . . 5 |- ( ph -> RR e. _V )
24		ovex 6348	. . . . . 6 |- ( 0 ... M ) e. _V
25	24	a1i 11	. . . . 5 |- ( ph -> ( 0 ... M ) e. _V )
26	23, 25	elmapd 7517	. . . 4 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) <-> Q : ( 0 ... M ) --> RR ) )
27	21, 26	mpbid 215	. . 3 |- ( ph -> Q : ( 0 ... M ) --> RR )
28	7	simprd 469	. . . 4 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
29	28	r19.21bi 2769	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
30		fourierdlem81.f	. . . . 5 |- ( ph -> F : RR --> CC )
31	30	adantr 471	. . . 4 |- ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> F : RR --> CC )
32		fourierdlem81.a	. . . . . . 7 |- ( ph -> A e. RR )
33	9, 32	eqeltrd 2540	. . . . . 6 |- ( ph -> ( Q ` 0 ) e. RR )
34		fourierdlem81.b	. . . . . . 7 |- ( ph -> B e. RR )
35	11, 34	eqeltrd 2540	. . . . . 6 |- ( ph -> ( Q ` M ) e. RR )
36	33, 35	iccssred 37687	. . . . 5 |- ( ph -> ( ( Q ` 0 ) [,] ( Q ` M ) ) C_ RR )
37	36	sselda 3444	. . . 4 |- ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> x e. RR )
38	31, 37	ffvelrnd 6051	. . 3 |- ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( F ` x ) e. CC )
39	27	adantr 471	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
40		elfzofz 11972	. . . . . 6 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
41	40	adantl 472	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
42	39, 41	ffvelrnd 6051	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
43		fzofzp1 12045	. . . . . 6 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
44	43	adantl 472	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
45	39, 44	ffvelrnd 6051	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
46	30	feqmptd 5945	. . . . . . . 8 |- ( ph -> F = ( x e. RR |-> ( F ` x ) ) )
47	46	reseq1d 5126	. . . . . . 7 |- ( ph -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( x e. RR |-> ( F ` x ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
48	47	adantr 471	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( x e. RR |-> ( F ` x ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
49		ioossre 11730	. . . . . . . 8 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
50	49	a1i 11	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
51	50	resmptd 5178	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( x e. RR |-> ( F ` x ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
52	48, 51	eqtr2d 2497	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
53		fourierdlem81.cncf	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
54		fourierdlem81.l	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
55		fourierdlem81.r	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
56	42, 45, 53, 54, 55	iblcncfioo 37941	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. L^1 )
57	52, 56	eqeltrd 2540	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
58	30	ad2antrr 737	. . . . 5 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> F : RR --> CC )
59	42, 45	iccssred 37687	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ RR )
60	59	sselda 3444	. . . . 5 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. RR )
61	58, 60	ffvelrnd 6051	. . . 4 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
62	42, 45, 57, 61	ibliooicc 37934	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
63	15, 20, 27, 29, 38, 62	itgspltprt 37942	. 2 |- ( ph -> S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( F ` x ) _d x = sum_ i e. ( 0..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` x ) _d x )
64		fourierdlem81.s	. . . . . . . 8 |- S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) )
65	64	a1i 11	. . . . . . 7 |- ( ph -> S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) ) )
66		fveq2 5892	. . . . . . . . 9 |- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
67	66	oveq1d 6335	. . . . . . . 8 |- ( i = 0 -> ( ( Q ` i ) + T ) = ( ( Q ` 0 ) + T ) )
68	67	adantl 472	. . . . . . 7 |- ( ( ph /\ i = 0 ) -> ( ( Q ` i ) + T ) = ( ( Q ` 0 ) + T ) )
69	2	nnnn0d 10959	. . . . . . . . 9 |- ( ph -> M e. NN0 )
70		nn0uz 11227	. . . . . . . . 9 |- NN0 = ( ZZ>= ` 0 )
71	69, 70	syl6eleq 2550	. . . . . . . 8 |- ( ph -> M e. ( ZZ>= ` 0 ) )
72		eluzfz1 11841	. . . . . . . 8 |- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
73	71, 72	syl 17	. . . . . . 7 |- ( ph -> 0 e. ( 0 ... M ) )
74		fourierdlem81.t	. . . . . . . . 9 |- ( ph -> T e. RR+ )
75	74	rpred 11375	. . . . . . . 8 |- ( ph -> T e. RR )
76	33, 75	readdcld 9701	. . . . . . 7 |- ( ph -> ( ( Q ` 0 ) + T ) e. RR )
77	65, 68, 73, 76	fvmptd 5982	. . . . . 6 |- ( ph -> ( S ` 0 ) = ( ( Q ` 0 ) + T ) )
78	9	oveq1d 6335	. . . . . 6 |- ( ph -> ( ( Q ` 0 ) + T ) = ( A + T ) )
79	77, 78	eqtr2d 2497	. . . . 5 |- ( ph -> ( A + T ) = ( S ` 0 ) )
80		fveq2 5892	. . . . . . . . 9 |- ( i = M -> ( Q ` i ) = ( Q ` M ) )
81	80	oveq1d 6335	. . . . . . . 8 |- ( i = M -> ( ( Q ` i ) + T ) = ( ( Q ` M ) + T ) )
82	81	adantl 472	. . . . . . 7 |- ( ( ph /\ i = M ) -> ( ( Q ` i ) + T ) = ( ( Q ` M ) + T ) )
83		eluzfz2 11842	. . . . . . . 8 |- ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
84	71, 83	syl 17	. . . . . . 7 |- ( ph -> M e. ( 0 ... M ) )
85	35, 75	readdcld 9701	. . . . . . 7 |- ( ph -> ( ( Q ` M ) + T ) e. RR )
86	65, 82, 84, 85	fvmptd 5982	. . . . . 6 |- ( ph -> ( S ` M ) = ( ( Q ` M ) + T ) )
87	11	oveq1d 6335	. . . . . 6 |- ( ph -> ( ( Q ` M ) + T ) = ( B + T ) )
88	86, 87	eqtr2d 2497	. . . . 5 |- ( ph -> ( B + T ) = ( S ` M ) )
89	79, 88	oveq12d 6338	. . . 4 |- ( ph -> ( ( A + T ) [,] ( B + T ) ) = ( ( S ` 0 ) [,] ( S ` M ) ) )
90	89	itgeq1d 37919	. . 3 |- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( ( S ` 0 ) [,] ( S ` M ) ) ( F ` x ) _d x )
91	27	ffvelrnda 6050	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
92	75	adantr 471	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... M ) ) -> T e. RR )
93	91, 92	readdcld 9701	. . . . 5 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( Q ` i ) + T ) e. RR )
94	93, 64	fmptd 6074	. . . 4 |- ( ph -> S : ( 0 ... M ) --> RR )
95	75	adantr 471	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> T e. RR )
96	42, 45, 95, 29	ltadd1dd 10257	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + T ) < ( ( Q ` ( i + 1 ) ) + T ) )
97	40, 93	sylan2 481	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + T ) e. RR )
98	64	fvmpt2 5985	. . . . . 6 |- ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) + T ) e. RR ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
99	41, 97, 98	syl2anc 671	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
100		fveq2 5892	. . . . . . . . . 10 |- ( i = j -> ( Q ` i ) = ( Q ` j ) )
101	100	oveq1d 6335	. . . . . . . . 9 |- ( i = j -> ( ( Q ` i ) + T ) = ( ( Q ` j ) + T ) )
102	101	cbvmptv 4511	. . . . . . . 8 |- ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) ) = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) )
103	64, 102	eqtri 2484	. . . . . . 7 |- S = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) )
104	103	a1i 11	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> S = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) )
105		fveq2 5892	. . . . . . . 8 |- ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
106	105	oveq1d 6335	. . . . . . 7 |- ( j = ( i + 1 ) -> ( ( Q ` j ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
107	106	adantl 472	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
108	45, 95	readdcld 9701	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR )
109	104, 107, 44, 108	fvmptd 5982	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) + T ) )
110	96, 99, 109	3brtr4d 4449	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` i ) < ( S ` ( i + 1 ) ) )
111	30	adantr 471	. . . . 5 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> F : RR --> CC )
112	77, 76	eqeltrd 2540	. . . . . . . 8 |- ( ph -> ( S ` 0 ) e. RR )
113	112	adantr 471	. . . . . . 7 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( S ` 0 ) e. RR )
114	86, 85	eqeltrd 2540	. . . . . . . 8 |- ( ph -> ( S ` M ) e. RR )
115	114	adantr 471	. . . . . . 7 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( S ` M ) e. RR )
116	113, 115	iccssred 37687	. . . . . 6 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( ( S ` 0 ) [,] ( S ` M ) ) C_ RR )
117		simpr 467	. . . . . 6 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> x e. ( ( S ` 0 ) [,] ( S ` M ) ) )
118	116, 117	sseldd 3445	. . . . 5 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> x e. RR )
119	111, 118	ffvelrnd 6051	. . . 4 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( F ` x ) e. CC )
120	99, 97	eqeltrd 2540	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` i ) e. RR )
121	109, 108	eqeltrd 2540	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` ( i + 1 ) ) e. RR )
122		ioosscn 37676	. . . . . . . . 9 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
123	122	a1i 11	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
124		eqeq1 2466	. . . . . . . . . . 11 |- ( w = x -> ( w = ( z + T ) <-> x = ( z + T ) ) )
125	124	rexbidv 2913	. . . . . . . . . 10 |- ( w = x -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) <-> E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) )
126		oveq1 6327	. . . . . . . . . . . 12 |- ( z = y -> ( z + T ) = ( y + T ) )
127	126	eqeq2d 2472	. . . . . . . . . . 11 |- ( z = y -> ( x = ( z + T ) <-> x = ( y + T ) ) )
128	127	cbvrexv 3032	. . . . . . . . . 10 |- ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) <-> E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) )
129	125, 128	syl6bb 269	. . . . . . . . 9 |- ( w = x -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) <-> E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) ) )
130	129	cbvrabv 3056	. . . . . . . 8 |- { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } = { x e. CC | E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) }
131		fdm 5760	. . . . . . . . . . . 12 |- ( F : RR --> CC -> dom F = RR )
132	30, 131	syl 17	. . . . . . . . . . 11 |- ( ph -> dom F = RR )
133	132	feq2d 5741	. . . . . . . . . 10 |- ( ph -> ( F : dom F --> CC <-> F : RR --> CC ) )
134	30, 133	mpbird 240	. . . . . . . . 9 |- ( ph -> F : dom F --> CC )
135	134	adantr 471	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F : dom F --> CC )
136		elioore 11700	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> z e. RR )
137	136	adantl 472	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. RR )
138	75	adantr 471	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> T e. RR )
139	137, 138	readdcld 9701	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z + T ) e. RR )
140	139	adantlr 726	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z + T ) e. RR )
141	140	3adant3 1034	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> ( z + T ) e. RR )
142		simp3 1016	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> w = ( z + T ) )
143	132	3ad2ant1 1035	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> dom F = RR )
144	143	3adant1r 1269	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> dom F = RR )
145	141, 142, 144	3eltr4d 2555	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> w e. dom F )
146	145	3exp 1214	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( w = ( z + T ) -> w e. dom F ) ) )
147	146	adantr 471	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ w e. CC ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( w = ( z + T ) -> w e. dom F ) ) )
148	147	rexlimdv 2889	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ w e. CC ) -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) -> w e. dom F ) )
149	148	ralrimiva 2814	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A. w e. CC ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) -> w e. dom F ) )
150		rabss 3518	. . . . . . . . 9 |- ( { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } C_ dom F <-> A. w e. CC ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) -> w e. dom F ) )
151	149, 150	sylibr 217	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } C_ dom F )
152		simpll 765	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
153	32	rexrd 9721	. . . . . . . . . . 11 |- ( ph -> A e. RR* )
154	153	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A e. RR* )
155	34	rexrd 9721	. . . . . . . . . . 11 |- ( ph -> B e. RR* )
156	155	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> B e. RR* )
157	3, 2, 1	fourierdlem15 38085	. . . . . . . . . . 11 |- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
158	157	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
159		simplr 767	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0..^ M ) )
160		ioossicc 11754	. . . . . . . . . . . 12 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
161	160	sseli 3440	. . . . . . . . . . 11 |- ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
162	161	adantl 472	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
163	154, 156, 158, 159, 162	fourierdlem1 38071	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. ( A [,] B ) )
164		fourierdlem81.fper	. . . . . . . . 9 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
165	152, 163, 164	syl2anc 671	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
166	123, 95, 130, 135, 151, 165, 53	cncfperiod 37842	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) e. ( { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } -cn-> CC ) )
167	125	elrab 3208	. . . . . . . . . . . . 13 |- ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } <-> ( x e. CC /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) )
168	167	simprbi 470	. . . . . . . . . . . 12 |- ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } -> E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) )
169		simpr 467	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) )
170		nfv 1772	. . . . . . . . . . . . . . . 16 |- F/ z ( ph /\ i e. ( 0..^ M ) )
171		nfre1 2860	. . . . . . . . . . . . . . . 16 |- F/ z E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T )
172	170, 171	nfan 2022	. . . . . . . . . . . . . . 15 |- F/ z ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) )
173		nfv 1772	. . . . . . . . . . . . . . 15 |- F/ z ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) )
174		simp3 1016	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x = ( z + T ) )
175	139	3adant3 1034	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( z + T ) e. RR )
176	174, 175	eqeltrd 2540	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x e. RR )
177	176	3adant1r 1269	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x e. RR )
178	42	adantr 471	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
179	136	adantl 472	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. RR )
180	75	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> T e. RR )
181		simpr 467	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
182	42	rexrd 9721	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
183	182	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
184	45	rexrd 9721	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
185	184	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
186		elioo2 11711	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( z e. RR /\ ( Q ` i ) < z /\ z < ( Q ` ( i + 1 ) ) ) ) )
187	183, 185, 186	syl2anc 671	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( z e. RR /\ ( Q ` i ) < z /\ z < ( Q ` ( i + 1 ) ) ) ) )
188	181, 187	mpbid 215	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z e. RR /\ ( Q ` i ) < z /\ z < ( Q ` ( i + 1 ) ) ) )
189	188	simp2d 1027	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < z )
190	178, 179, 180, 189	ltadd1dd 10257	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) + T ) < ( z + T ) )
191	190	3adant3 1034	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( ( Q ` i ) + T ) < ( z + T ) )
192	99	3ad2ant1 1035	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
193		simp3 1016	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x = ( z + T ) )
194	191, 192, 193	3brtr4d 4449	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( S ` i ) < x )
195	45	adantr 471	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
196	188	simp3d 1028	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z < ( Q ` ( i + 1 ) ) )
197	179, 195, 180, 196	ltadd1dd 10257	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z + T ) < ( ( Q ` ( i + 1 ) ) + T ) )
198	197	3adant3 1034	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( z + T ) < ( ( Q ` ( i + 1 ) ) + T ) )
199	109	3ad2ant1 1035	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( S ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) + T ) )
200	198, 193, 199	3brtr4d 4449	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x < ( S ` ( i + 1 ) ) )
201	177, 194, 200	3jca 1194	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) )
202	201	3exp 1214	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( x = ( z + T ) -> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) ) ) )
203	202	adantr 471	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( x = ( z + T ) -> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) ) ) )
204	172, 173, 203	rexlimd 2883	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) -> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) ) )
205	169, 204	mpd 15	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) )
206	120	rexrd 9721	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` i ) e. RR* )
207	206	adantr 471	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( S ` i ) e. RR* )
208	121	rexrd 9721	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` ( i + 1 ) ) e. RR* )
209	208	adantr 471	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( S ` ( i + 1 ) ) e. RR* )
210		elioo2 11711	. . . . . . . . . . . . . 14 |- ( ( ( S ` i ) e. RR* /\ ( S ` ( i + 1 ) ) e. RR* ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) <-> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) ) )
211	207, 209, 210	syl2anc 671	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) <-> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) ) )
212	205, 211	mpbird 240	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
213	168, 212	sylan2 481	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
214		elioore 11700	. . . . . . . . . . . . . 14 |- ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -> x e. RR )
215	214	recnd 9700	. . . . . . . . . . . . 13 |- ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -> x e. CC )
216	215	adantl 472	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. CC )
217	182	adantr 471	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
218	184	adantr 471	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
219	214	adantl 472	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. RR )
220	75	adantr 471	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> T e. RR )
221	219, 220	resubcld 10080	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. RR )
222	221	adantlr 726	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. RR )
223	99	oveq1d 6335	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` i ) - T ) = ( ( ( Q ` i ) + T ) - T ) )
224	42	recnd 9700	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. CC )
225	95	recnd 9700	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> T e. CC )
226	224, 225	pncand 10018	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) + T ) - T ) = ( Q ` i ) )
227	223, 226	eqtr2d 2497	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( ( S ` i ) - T ) )
228	227	adantr 471	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) = ( ( S ` i ) - T ) )
229	120	adantr 471	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) e. RR )
230	214	adantl 472	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. RR )
231	75	ad2antrr 737	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> T e. RR )
232		simpr 467	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
233	206	adantr 471	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) e. RR* )
234	208	adantr 471	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` ( i + 1 ) ) e. RR* )
235	233, 234, 210	syl2anc 671	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) <-> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) ) )
236	232, 235	mpbid 215	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) )
237	236	simp2d 1027	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) < x )
238	229, 230, 231, 237	ltsub1dd 10258	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( S ` i ) - T ) < ( x - T ) )
239	228, 238	eqbrtrd 4439	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( x - T ) )
240	121	adantr 471	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` ( i + 1 ) ) e. RR )
241	236	simp3d 1028	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x < ( S ` ( i + 1 ) ) )
242	230, 240, 231, 241	ltsub1dd 10258	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) < ( ( S ` ( i + 1 ) ) - T ) )
243	109	oveq1d 6335	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` ( i + 1 ) ) - T ) = ( ( ( Q ` ( i + 1 ) ) + T ) - T ) )
244	45	recnd 9700	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
245	244, 225	pncand 10018	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` ( i + 1 ) ) + T ) - T ) = ( Q ` ( i + 1 ) ) )
246	243, 245	eqtrd 2496	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) )
247	246	adantr 471	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) )
248	242, 247	breqtrd 4443	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) < ( Q ` ( i + 1 ) ) )
249	217, 218, 222, 239, 248	eliood 37680	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
250	219	recnd 9700	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. CC )
251	220	recnd 9700	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> T e. CC )
252	250, 251	npcand 10021	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( x - T ) + T ) = x )
253	252	eqcomd 2468	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x = ( ( x - T ) + T ) )
254	253	adantlr 726	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x = ( ( x - T ) + T ) )
255		oveq1 6327	. . . . . . . . . . . . . . 15 |- ( z = ( x - T ) -> ( z + T ) = ( ( x - T ) + T ) )
256	255	eqeq2d 2472	. . . . . . . . . . . . . 14 |- ( z = ( x - T ) -> ( x = ( z + T ) <-> x = ( ( x - T ) + T ) ) )
257	256	rspcev 3162	. . . . . . . . . . . . 13 |- ( ( ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( ( x - T ) + T ) ) -> E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) )
258	249, 254, 257	syl2anc 671	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) )
259	216, 258, 167	sylanbrc 675	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } )
260	213, 259	impbida 848	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } <-> x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) )
261	260	eqrdv 2460	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } = ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
262	261	reseq2d 5127	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) = ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) )
263	30	adantr 471	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F : RR --> CC )
264		ioossre 11730	. . . . . . . . . 10 |- ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) C_ RR
265	264	a1i 11	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) C_ RR )
266	263, 265	feqresmpt 5946	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) = ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
267	262, 266	eqtrd 2496	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) = ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
268	261	oveq1d 6335	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } -cn-> CC ) = ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -cn-> CC ) )
269	166, 267, 268	3eltr3d 2554	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -cn-> CC ) )
270	49, 132	syl5sseqr 3493	. . . . . . . . 9 |- ( ph -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
271	270	adantr 471	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
272		eqid 2462	. . . . . . . 8 |- { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } = { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) }
273		simpll 765	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
274	153	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A e. RR* )
275	155	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> B e. RR* )
276	157	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
277		simplr 767	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0..^ M ) )
278	160, 181	sseldi 3442	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
279	274, 275, 276, 277, 278	fourierdlem1 38071	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( A [,] B ) )
280		eleq1 2528	. . . . . . . . . . . 12 |- ( x = z -> ( x e. ( A [,] B ) <-> z e. ( A [,] B ) ) )
281	280	anbi2d 715	. . . . . . . . . . 11 |- ( x = z -> ( ( ph /\ x e. ( A [,] B ) ) <-> ( ph /\ z e. ( A [,] B ) ) ) )
282		oveq1 6327	. . . . . . . . . . . . 13 |- ( x = z -> ( x + T ) = ( z + T ) )
283	282	fveq2d 5896	. . . . . . . . . . . 12 |- ( x = z -> ( F ` ( x + T ) ) = ( F ` ( z + T ) ) )
284		fveq2 5892	. . . . . . . . . . . 12 |- ( x = z -> ( F ` x ) = ( F ` z ) )
285	283, 284	eqeq12d 2477	. . . . . . . . . . 11 |- ( x = z -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( z + T ) ) = ( F ` z ) ) )
286	281, 285	imbi12d 326	. . . . . . . . . 10 |- ( x = z -> ( ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` ( z + T ) ) = ( F ` z ) ) ) )
287	286, 164	chvarv 2118	. . . . . . . . 9 |- ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` ( z + T ) ) = ( F ` z ) )
288	273, 279, 287	syl2anc 671	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( z + T ) ) = ( F ` z ) )
289	135, 123, 271, 225, 272, 151, 288, 54	limcperiod 37794	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) lim CC ( ( Q ` ( i + 1 ) ) + T ) ) )
290	109	eqcomd 2468	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) = ( S ` ( i + 1 ) ) )
291	267, 290	oveq12d 6338	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) lim CC ( ( Q ` ( i + 1 ) ) + T ) ) = ( ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) lim CC ( S ` ( i + 1 ) ) ) )
292	289, 291	eleqtrd 2542	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) lim CC ( S ` ( i + 1 ) ) ) )
293	135, 123, 271, 225, 272, 151, 288, 55	limcperiod 37794	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) lim CC ( ( Q ` i ) + T ) ) )
294	99	eqcomd 2468	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + T ) = ( S ` i ) )
295	267, 294	oveq12d 6338	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) lim CC ( ( Q ` i ) + T ) ) = ( ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) lim CC ( S ` i ) ) )
296	293, 295	eleqtrd 2542	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) lim CC ( S ` i ) ) )
297	120, 121, 269, 292, 296	iblcncfioo 37941	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
298	30	ad2antrr 737	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> F : RR --> CC )
299	120	adantr 471	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) e. RR )
300	121	adantr 471	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( S ` ( i + 1 ) ) e. RR )
301		simpr 467	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) )
302		eliccre 37688	. . . . . . 7 |- ( ( ( S ` i ) e. RR /\ ( S ` ( i + 1 ) ) e. RR /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x e. RR )
303	299, 300, 301, 302	syl3anc 1276	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x e. RR )
304	298, 303	ffvelrnd 6051	. . . . 5 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
305	120, 121, 297, 304	ibliooicc 37934	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
306	15, 20, 94, 110, 119, 305	itgspltprt 37942	. . 3 |- ( ph -> S. ( ( S ` 0 ) [,] ( S ` M ) ) ( F ` x ) _d x = sum_ i e. ( 0..^ M ) S. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ( F ` x ) _d x )
307		iftrue 3899	. . . . . . . . . . . 12 |- ( x = ( S ` i ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) = R )
308	307	adantl 472	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x = ( S ` i ) ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) = R )
309		fourierdlem81.g	. . . . . . . . . . . . . . 15 |- G = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) )
310		iftrue 3899	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = R )
311		iftrue 3899	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) = R )
312	310, 311	eqtr4d 2499	. . . . . . . . . . . . . . . . . 18 |- ( x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
313	312	adantl 472	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ x = ( Q ` i ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
314		iffalse 3902	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) )
315	314	adantr 471	. . . . . . . . . . . . . . . . . . . 20 |- ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) )
316		iftrue 3899	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = L )
317	316	adantl 472	. . . . . . . . . . . . . . . . . . . 20 |- ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = L )
318		iffalse 3902	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) )
319	318	adantr 471	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) )
320		iftrue 3899	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = L )
321	320	adantl 472	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = L )
322	319, 321	eqtr2d 2497	. . . . . . . . . . . . . . . . . . . 20 |- ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> L = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
323	315, 317, 322	3eqtrd 2500	. . . . . . . . . . . . . . . . . . 19 |- ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
324	323	adantll 725	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
325	314	ad2antlr 738	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) )
326		iffalse 3902	. . . . . . . . . . . . . . . . . . . 20 |- ( -. x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = ( F ` x ) )
327	326	adantl 472	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = ( F ` x ) )
328	318	ad2antlr 738	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) )
329		iffalse 3902	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) )
330	329	adantl 472	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) )
331	182	ad3antrrr 741	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) e. RR* )
332	184	ad3antrrr 741	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
333	60	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x e. RR )
334	42	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) e. RR )
335	60	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> x e. RR )
336	182	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) e. RR* )
337	184	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
338		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
339		iccgelb 11725	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) <_ x )
340	336, 337, 338, 339	syl3anc 1276	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) <_ x )
341		neqne 2643	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -. x = ( Q ` i ) -> x =/= ( Q ` i ) )
342	341	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> x =/= ( Q ` i ) )
343	334, 335, 340, 342	leneltd 9820	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) < x )
344	343	adantr 471	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) < x )
345	45	ad3antrrr 741	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
346	182	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
347	184	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
348		simpr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
349		iccleub 11724	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x <_ ( Q ` ( i + 1 ) ) )
350	346, 347, 348, 349	syl3anc 1276	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x <_ ( Q ` ( i + 1 ) ) )
351	350	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x <_ ( Q ` ( i + 1 ) ) )
352		neqne 2643	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -. x = ( Q ` ( i + 1 ) ) -> x =/= ( Q ` ( i + 1 ) ) )
353	352	necomd 2691	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( -. x = ( Q ` ( i + 1 ) ) -> ( Q ` ( i + 1 ) ) =/= x )
354	353	adantl 472	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) =/= x )
355	333, 345, 351, 354	leneltd 9820	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x < ( Q ` ( i + 1 ) ) )
356	331, 332, 333, 344, 355	eliood 37680	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
357		fvres 5906	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) = ( F ` x ) )
358	356, 357	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) = ( F ` x ) )
359	328, 330, 358	3eqtrrd 2501	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) )