Theorem fourierdlem81 37319

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 37240	. . . . . . . . . 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 210	. . . . . . . 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 461	. . . . . . 7 |- ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
8	7	simpld 457	. . . . . 6 |- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
9	8	simpld 457	. . . . 5 |- ( ph -> ( Q ` 0 ) = A )
10	9	eqcomd 2410	. . . 4 |- ( ph -> A = ( Q ` 0 ) )
11	8	simprd 461	. . . . 5 |- ( ph -> ( Q ` M ) = B )
12	11	eqcomd 2410	. . . 4 |- ( ph -> B = ( Q ` M ) )
13	10, 12	oveq12d 6295	. . 3 |- ( ph -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
14	13	itgeq1d 37104	. 2 |- ( ph -> S. ( A [,] B ) ( F ` x ) _d x = S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( F ` x ) _d x )
15		0zd 10916	. . 3 |- ( ph -> 0 e. ZZ )
16		nnuz 11161	. . . . 5 |- NN = ( ZZ>= ` 1 )
17		0p1e1 10687	. . . . . 6 |- ( 0 + 1 ) = 1
18	17	fveq2i 5851	. . . . 5 |- ( ZZ>= ` ( 0 + 1 ) ) = ( ZZ>= ` 1 )
19	16, 18	eqtr4i 2434	. . . 4 |- NN = ( ZZ>= ` ( 0 + 1 ) )
20	2, 19	syl6eleq 2500	. . 3 |- ( ph -> M e. ( ZZ>= ` ( 0 + 1 ) ) )
21	6	simpld 457	. . . 4 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
22		reex 9612	. . . . . 6 |- RR e. _V
23	22	a1i 11	. . . . 5 |- ( ph -> RR e. _V )
24		ovex 6305	. . . . . 6 |- ( 0 ... M ) e. _V
25	24	a1i 11	. . . . 5 |- ( ph -> ( 0 ... M ) e. _V )
26	23, 25	elmapd 7470	. . . 4 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) <-> Q : ( 0 ... M ) --> RR ) )
27	21, 26	mpbid 210	. . 3 |- ( ph -> Q : ( 0 ... M ) --> RR )
28	7	simprd 461	. . . 4 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
29	28	r19.21bi 2772	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
30		fourierdlem81.f	. . . . 5 |- ( ph -> F : RR --> CC )
31	30	adantr 463	. . . 4 |- ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> F : RR --> CC )
32		fourierdlem81.a	. . . . . . 7 |- ( ph -> A e. RR )
33	9, 32	eqeltrd 2490	. . . . . 6 |- ( ph -> ( Q ` 0 ) e. RR )
34		fourierdlem81.b	. . . . . . 7 |- ( ph -> B e. RR )
35	11, 34	eqeltrd 2490	. . . . . 6 |- ( ph -> ( Q ` M ) e. RR )
36	33, 35	iccssred 36888	. . . . 5 |- ( ph -> ( ( Q ` 0 ) [,] ( Q ` M ) ) C_ RR )
37	36	sselda 3441	. . . 4 |- ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> x e. RR )
38	31, 37	ffvelrnd 6009	. . 3 |- ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( F ` x ) e. CC )
39	27	adantr 463	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
40		elfzofz 11872	. . . . . 6 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
41	40	adantl 464	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
42	39, 41	ffvelrnd 6009	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
43		fzofzp1 11944	. . . . . 6 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
44	43	adantl 464	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
45	39, 44	ffvelrnd 6009	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
46	30	feqmptd 5901	. . . . . . . 8 |- ( ph -> F = ( x e. RR |-> ( F ` x ) ) )
47	46	reseq1d 5092	. . . . . . 7 |- ( ph -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( x e. RR |-> ( F ` x ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
48	47	adantr 463	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( x e. RR |-> ( F ` x ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
49		ioossre 11638	. . . . . . . 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 5144	. . . . . 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 2444	. . . . 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 37126	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. L^1 )
57	52, 56	eqeltrd 2490	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
58	30	ad2antrr 724	. . . . 5 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> F : RR --> CC )
59	42, 45	iccssred 36888	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ RR )
60	59	sselda 3441	. . . . 5 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. RR )
61	58, 60	ffvelrnd 6009	. . . 4 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
62	42, 45, 57, 61	ibliooicc 37119	. . 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 37127	. 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 5848	. . . . . . . . 9 |- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
67	66	oveq1d 6292	. . . . . . . 8 |- ( i = 0 -> ( ( Q ` i ) + T ) = ( ( Q ` 0 ) + T ) )
68	67	adantl 464	. . . . . . 7 |- ( ( ph /\ i = 0 ) -> ( ( Q ` i ) + T ) = ( ( Q ` 0 ) + T ) )
69	2	nnnn0d 10892	. . . . . . . . 9 |- ( ph -> M e. NN0 )
70		nn0uz 11160	. . . . . . . . 9 |- NN0 = ( ZZ>= ` 0 )
71	69, 70	syl6eleq 2500	. . . . . . . 8 |- ( ph -> M e. ( ZZ>= ` 0 ) )
72		eluzfz1 11745	. . . . . . . 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 11303	. . . . . . . 8 |- ( ph -> T e. RR )
76	33, 75	readdcld 9652	. . . . . . 7 |- ( ph -> ( ( Q ` 0 ) + T ) e. RR )
77	65, 68, 73, 76	fvmptd 5937	. . . . . 6 |- ( ph -> ( S ` 0 ) = ( ( Q ` 0 ) + T ) )
78	9	oveq1d 6292	. . . . . 6 |- ( ph -> ( ( Q ` 0 ) + T ) = ( A + T ) )
79	77, 78	eqtr2d 2444	. . . . 5 |- ( ph -> ( A + T ) = ( S ` 0 ) )
80		fveq2 5848	. . . . . . . . 9 |- ( i = M -> ( Q ` i ) = ( Q ` M ) )
81	80	oveq1d 6292	. . . . . . . 8 |- ( i = M -> ( ( Q ` i ) + T ) = ( ( Q ` M ) + T ) )
82	81	adantl 464	. . . . . . 7 |- ( ( ph /\ i = M ) -> ( ( Q ` i ) + T ) = ( ( Q ` M ) + T ) )
83		eluzfz2 11746	. . . . . . . 8 |- ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
84	71, 83	syl 17	. . . . . . 7 |- ( ph -> M e. ( 0 ... M ) )
85	35, 75	readdcld 9652	. . . . . . 7 |- ( ph -> ( ( Q ` M ) + T ) e. RR )
86	65, 82, 84, 85	fvmptd 5937	. . . . . 6 |- ( ph -> ( S ` M ) = ( ( Q ` M ) + T ) )
87	11	oveq1d 6292	. . . . . 6 |- ( ph -> ( ( Q ` M ) + T ) = ( B + T ) )
88	86, 87	eqtr2d 2444	. . . . 5 |- ( ph -> ( B + T ) = ( S ` M ) )
89	79, 88	oveq12d 6295	. . . 4 |- ( ph -> ( ( A + T ) [,] ( B + T ) ) = ( ( S ` 0 ) [,] ( S ` M ) ) )
90	89	itgeq1d 37104	. . 3 |- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( ( S ` 0 ) [,] ( S ` M ) ) ( F ` x ) _d x )
91	27	ffvelrnda 6008	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
92	75	adantr 463	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... M ) ) -> T e. RR )
93	91, 92	readdcld 9652	. . . . 5 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( Q ` i ) + T ) e. RR )
94	93, 64	fmptd 6032	. . . 4 |- ( ph -> S : ( 0 ... M ) --> RR )
95	75	adantr 463	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> T e. RR )
96	42, 45, 95, 29	ltadd1dd 10202	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + T ) < ( ( Q ` ( i + 1 ) ) + T ) )
97	40, 93	sylan2 472	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + T ) e. RR )
98	64	fvmpt2 5940	. . . . . 6 |- ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) + T ) e. RR ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
99	41, 97, 98	syl2anc 659	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
100		fveq2 5848	. . . . . . . . . 10 |- ( i = j -> ( Q ` i ) = ( Q ` j ) )
101	100	oveq1d 6292	. . . . . . . . 9 |- ( i = j -> ( ( Q ` i ) + T ) = ( ( Q ` j ) + T ) )
102	101	cbvmptv 4486	. . . . . . . 8 |- ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) ) = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) )
103	64, 102	eqtri 2431	. . . . . . 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 5848	. . . . . . . 8 |- ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
106	105	oveq1d 6292	. . . . . . 7 |- ( j = ( i + 1 ) -> ( ( Q ` j ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
107	106	adantl 464	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
108	45, 95	readdcld 9652	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR )
109	104, 107, 44, 108	fvmptd 5937	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) + T ) )
110	96, 99, 109	3brtr4d 4424	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` i ) < ( S ` ( i + 1 ) ) )
111	30	adantr 463	. . . . 5 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> F : RR --> CC )
112	77, 76	eqeltrd 2490	. . . . . . . 8 |- ( ph -> ( S ` 0 ) e. RR )
113	112	adantr 463	. . . . . . 7 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( S ` 0 ) e. RR )
114	86, 85	eqeltrd 2490	. . . . . . . 8 |- ( ph -> ( S ` M ) e. RR )
115	114	adantr 463	. . . . . . 7 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( S ` M ) e. RR )
116	113, 115	iccssred 36888	. . . . . 6 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( ( S ` 0 ) [,] ( S ` M ) ) C_ RR )
117		simpr 459	. . . . . 6 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> x e. ( ( S ` 0 ) [,] ( S ` M ) ) )
118	116, 117	sseldd 3442	. . . . 5 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> x e. RR )
119	111, 118	ffvelrnd 6009	. . . 4 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( F ` x ) e. CC )
120	99, 97	eqeltrd 2490	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` i ) e. RR )
121	109, 108	eqeltrd 2490	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` ( i + 1 ) ) e. RR )
122		ioosscn 36876	. . . . . . . . 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 2406	. . . . . . . . . . 11 |- ( w = x -> ( w = ( z + T ) <-> x = ( z + T ) ) )
125	124	rexbidv 2917	. . . . . . . . . 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 6284	. . . . . . . . . . . 12 |- ( z = y -> ( z + T ) = ( y + T ) )
127	126	eqeq2d 2416	. . . . . . . . . . 11 |- ( z = y -> ( x = ( z + T ) <-> x = ( y + T ) ) )
128	127	cbvrexv 3034	. . . . . . . . . 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 261	. . . . . . . . 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 3057	. . . . . . . 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 5717	. . . . . . . . . . . 12 |- ( F : RR --> CC -> dom F = RR )
132	30, 131	syl 17	. . . . . . . . . . 11 |- ( ph -> dom F = RR )
133	132	feq2d 5700	. . . . . . . . . 10 |- ( ph -> ( F : dom F --> CC <-> F : RR --> CC ) )
134	30, 133	mpbird 232	. . . . . . . . 9 |- ( ph -> F : dom F --> CC )
135	134	adantr 463	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F : dom F --> CC )
136		elioore 11611	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> z e. RR )
137	136	adantl 464	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. RR )
138	75	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> T e. RR )
139	137, 138	readdcld 9652	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z + T ) e. RR )
140	139	adantlr 713	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z + T ) e. RR )
141	140	3adant3 1017	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> ( z + T ) e. RR )
142		simp3 999	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> w = ( z + T ) )
143	132	3ad2ant1 1018	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> dom F = RR )
144	143	3adant1r 1223	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> dom F = RR )
145	141, 142, 144	3eltr4d 2505	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> w e. dom F )
146	145	3exp 1196	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( w = ( z + T ) -> w e. dom F ) ) )
147	146	adantr 463	. . . . . . . . . . 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 2893	. . . . . . . . . 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 2817	. . . . . . . . 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 3515	. . . . . . . . 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 212	. . . . . . . 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 752	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
153	32	rexrd 9672	. . . . . . . . . . 11 |- ( ph -> A e. RR* )
154	153	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A e. RR* )
155	34	rexrd 9672	. . . . . . . . . . 11 |- ( ph -> B e. RR* )
156	155	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> B e. RR* )
157	3, 2, 1	fourierdlem15 37253	. . . . . . . . . . 11 |- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
158	157	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
159		simplr 754	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0..^ M ) )
160		ioossicc 11662	. . . . . . . . . . . 12 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
161	160	sseli 3437	. . . . . . . . . . 11 |- ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
162	161	adantl 464	. . . . . . . . . 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 37239	. . . . . . . . 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 659	. . . . . . . 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 37030	. . . . . . 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 3206	. . . . . . . . . . . . 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 462	. . . . . . . . . . . 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 459	. . . . . . . . . . . . . 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 1728	. . . . . . . . . . . . . . . 16 |- F/ z ( ph /\ i e. ( 0..^ M ) )
171		nfre1 2864	. . . . . . . . . . . . . . . 16 |- F/ z E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T )
172	170, 171	nfan 1956	. . . . . . . . . . . . . . 15 |- F/ z ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) )
173		nfv 1728	. . . . . . . . . . . . . . 15 |- F/ z ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) )
174		simp3 999	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x = ( z + T ) )
175	139	3adant3 1017	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( z + T ) e. RR )
176	174, 175	eqeltrd 2490	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x e. RR )
177	176	3adant1r 1223	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x e. RR )
178	42	adantr 463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
179	136	adantl 464	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. RR )
180	75	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> T e. RR )
181		simpr 459	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
182	42	rexrd 9672	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
183	182	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
184	45	rexrd 9672	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
185	184	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
186		elioo2 11622	. . . . . . . . . . . . . . . . . . . . . . . 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 659	. . . . . . . . . . . . . . . . . . . . . . 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 210	. . . . . . . . . . . . . . . . . . . . . 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 1010	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < z )
190	178, 179, 180, 189	ltadd1dd 10202	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) + T ) < ( z + T ) )
191	190	3adant3 1017	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( ( Q ` i ) + T ) < ( z + T ) )
192	99	3ad2ant1 1018	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
193		simp3 999	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x = ( z + T ) )
194	191, 192, 193	3brtr4d 4424	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( S ` i ) < x )
195	45	adantr 463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
196	188	simp3d 1011	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z < ( Q ` ( i + 1 ) ) )
197	179, 195, 180, 196	ltadd1dd 10202	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z + T ) < ( ( Q ` ( i + 1 ) ) + T ) )
198	197	3adant3 1017	. . . . . . . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . . . . . . . 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 4424	. . . . . . . . . . . . . . . . . 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 1177	. . . . . . . . . . . . . . . . 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 1196	. . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . 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 2887	. . . . . . . . . . . . . 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 9672	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` i ) e. RR* )
207	206	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( S ` i ) e. RR* )
208	121	rexrd 9672	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` ( i + 1 ) ) e. RR* )
209	208	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( S ` ( i + 1 ) ) e. RR* )
210		elioo2 11622	. . . . . . . . . . . . . 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 659	. . . . . . . . . . . . 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 232	. . . . . . . . . . . 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 472	. . . . . . . . . . 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 11611	. . . . . . . . . . . . . 14 |- ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -> x e. RR )
215	214	recnd 9651	. . . . . . . . . . . . 13 |- ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -> x e. CC )
216	215	adantl 464	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. CC )
217	182	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
218	184	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
219	214	adantl 464	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. RR )
220	75	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> T e. RR )
221	219, 220	resubcld 10027	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. RR )
222	221	adantlr 713	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. RR )
223	99	oveq1d 6292	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` i ) - T ) = ( ( ( Q ` i ) + T ) - T ) )
224	42	recnd 9651	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. CC )
225	95	recnd 9651	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> T e. CC )
226	224, 225	pncand 9967	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) + T ) - T ) = ( Q ` i ) )
227	223, 226	eqtr2d 2444	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( ( S ` i ) - T ) )
228	227	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) = ( ( S ` i ) - T ) )
229	120	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) e. RR )
230	214	adantl 464	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. RR )
231	75	ad2antrr 724	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> T e. RR )
232		simpr 459	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
233	206	adantr 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) e. RR* )
234	208	adantr 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` ( i + 1 ) ) e. RR* )
235	233, 234, 210	syl2anc 659	. . . . . . . . . . . . . . . . . 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 210	. . . . . . . . . . . . . . . . 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 1010	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) < x )
238	229, 230, 231, 237	ltsub1dd 10203	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( S ` i ) - T ) < ( x - T ) )
239	228, 238	eqbrtrd 4414	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( x - T ) )
240	121	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` ( i + 1 ) ) e. RR )
241	236	simp3d 1011	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x < ( S ` ( i + 1 ) ) )
242	230, 240, 231, 241	ltsub1dd 10203	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) < ( ( S ` ( i + 1 ) ) - T ) )
243	109	oveq1d 6292	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` ( i + 1 ) ) - T ) = ( ( ( Q ` ( i + 1 ) ) + T ) - T ) )
244	45	recnd 9651	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
245	244, 225	pncand 9967	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` ( i + 1 ) ) + T ) - T ) = ( Q ` ( i + 1 ) ) )
246	243, 245	eqtrd 2443	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) )
247	246	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) )
248	242, 247	breqtrd 4418	. . . . . . . . . . . . . 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 36880	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
250	219	recnd 9651	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. CC )
251	220	recnd 9651	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> T e. CC )
252	250, 251	npcand 9970	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( x - T ) + T ) = x )
253	252	eqcomd 2410	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x = ( ( x - T ) + T ) )
254	253	adantlr 713	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x = ( ( x - T ) + T ) )
255		oveq1 6284	. . . . . . . . . . . . . . 15 |- ( z = ( x - T ) -> ( z + T ) = ( ( x - T ) + T ) )
256	255	eqeq2d 2416	. . . . . . . . . . . . . 14 |- ( z = ( x - T ) -> ( x = ( z + T ) <-> x = ( ( x - T ) + T ) ) )
257	256	rspcev 3159	. . . . . . . . . . . . 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 659	. . . . . . . . . . . 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 662	. . . . . . . . . . 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 833	. . . . . . . . . 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 2399	. . . . . . . . 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 5093	. . . . . . . 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 463	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F : RR --> CC )
264		ioossre 11638	. . . . . . . . . 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 5902	. . . . . . . 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 2443	. . . . . . 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 6292	. . . . . . 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 2504	. . . . . 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 3490	. . . . . . . . 9 |- ( ph -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
271	270	adantr 463	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
272		eqid 2402	. . . . . . . 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 752	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
274	153	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A e. RR* )
275	155	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> B e. RR* )
276	157	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
277		simplr 754	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0..^ M ) )
278	160, 181	sseldi 3439	. . . . . . . . . 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 37239	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( A [,] B ) )
280		eleq1 2474	. . . . . . . . . . . 12 |- ( x = z -> ( x e. ( A [,] B ) <-> z e. ( A [,] B ) ) )
281	280	anbi2d 702	. . . . . . . . . . 11 |- ( x = z -> ( ( ph /\ x e. ( A [,] B ) ) <-> ( ph /\ z e. ( A [,] B ) ) ) )
282		oveq1 6284	. . . . . . . . . . . . 13 |- ( x = z -> ( x + T ) = ( z + T ) )
283	282	fveq2d 5852	. . . . . . . . . . . 12 |- ( x = z -> ( F ` ( x + T ) ) = ( F ` ( z + T ) ) )
284		fveq2 5848	. . . . . . . . . . . 12 |- ( x = z -> ( F ` x ) = ( F ` z ) )
285	283, 284	eqeq12d 2424	. . . . . . . . . . 11 |- ( x = z -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( z + T ) ) = ( F ` z ) ) )
286	281, 285	imbi12d 318	. . . . . . . . . 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 2041	. . . . . . . . 9 |- ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` ( z + T ) ) = ( F ` z ) )
288	273, 279, 287	syl2anc 659	. . . . . . . 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 36983	. . . . . . 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 2410	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) = ( S ` ( i + 1 ) ) )
291	267, 290	oveq12d 6295	. . . . . . 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 2492	. . . . . 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 36983	. . . . . . 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 2410	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + T ) = ( S ` i ) )
295	267, 294	oveq12d 6295	. . . . . . 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 2492	. . . . . 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 37126	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
298	30	ad2antrr 724	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> F : RR --> CC )
299	120	adantr 463	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) e. RR )
300	121	adantr 463	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( S ` ( i + 1 ) ) e. RR )
301		simpr 459	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) )
302		eliccre 36889	. . . . . . 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 1230	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x e. RR )
304	298, 303	ffvelrnd 6009	. . . . 5 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
305	120, 121, 297, 304	ibliooicc 37119	. . . 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 37127	. . 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 3890	. . . . . . . . . . . 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 464	. . . . . . . . . . 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 3890	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = R )
311		iftrue 3890	. . . . . . . . . . . . . . . . . . 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 2446	. . . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . 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 3893	. . . . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . . 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 3890	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = L )
317	316	adantl 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = L )
318		iffalse 3893	. . . . . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . . . 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 3890	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = L )
321	320	adantl 464	. . . . . . . . . . . . . . . . . . . . 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 2444	. . . . . . . . . . . . . . . . . . . 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 2447	. . . . . . . . . . . . . . . . . . 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 712	. . . . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . . . . 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 3893	. . . . . . . . . . . . . . . . . . . 20 |- ( -. x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = ( F ` x ) )
327	326	adantl 464	. . . . . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . . . . . 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 3893	. . . . . . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) e. RR )
335	60	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> x e. RR )
336	182	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) e. RR* )
337	184	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
338		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . 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 11633	. . . . . . . . . . . . . . . . . . . . . . . . 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 1230	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) <_ x )
341		neqne 36790	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -. x = ( Q ` i ) -> x =/= ( Q ` i ) )
342	341	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . 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 36844	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) < x )
344	343	adantr 463	. . . . . . . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
347	184	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
348		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
349		iccleub 11632	. . . . . . . . . . . . . . . . . . . . . . . . 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 1230	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x <_ ( Q ` ( i + 1 ) ) )
351	350	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 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 36790	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -. x = ( Q ` ( i + 1 ) ) -> x =/= ( Q ` ( i + 1 ) ) )
353	352	necomd 2674	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( -. x = ( Q ` ( i + 1 ) ) -> ( Q ` ( i + 1 ) ) =/= x )
354	353	adantl 464	. . . . . . . . . . . . . . . . . . . . . . 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 36844	. . . . . . . . . . . . . . . . . . . . . 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 36880	. . . . . . . . . . . . . . . . . . . . 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 5862	. . . . . . . . . . . . . . . . . . . . 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 2448	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) ->