Theorem fourierdlem81 31811

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 31732	. . . . . . . . . 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 16	. . . . . . . . 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 463	. . . . . . 7 |- ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
8	7	simpld 459	. . . . . 6 |- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
9	8	simpld 459	. . . . 5 |- ( ph -> ( Q ` 0 ) = A )
10	9	eqcomd 2475	. . . 4 |- ( ph -> A = ( Q ` 0 ) )
11	8	simprd 463	. . . . 5 |- ( ph -> ( Q ` M ) = B )
12	11	eqcomd 2475	. . . 4 |- ( ph -> B = ( Q ` M ) )
13	10, 12	oveq12d 6313	. . 3 |- ( ph -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
14		itgeq1 22047	. . 3 |- ( ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) -> S. ( A [,] B ) ( F ` x ) _d x = S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( F ` x ) _d x )
15	13, 14	syl 16	. 2 |- ( ph -> S. ( A [,] B ) ( F ` x ) _d x = S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( F ` x ) _d x )
16		0z 10887	. . . 4 |- 0 e. ZZ
17	16	a1i 11	. . 3 |- ( ph -> 0 e. ZZ )
18		0p1e1 10659	. . . . . . 7 |- ( 0 + 1 ) = 1
19	18	fveq2i 5875	. . . . . 6 |- ( ZZ>= ` ( 0 + 1 ) ) = ( ZZ>= ` 1 )
20		nnuz 11129	. . . . . . 7 |- NN = ( ZZ>= ` 1 )
21	20	eqcomi 2480	. . . . . 6 |- ( ZZ>= ` 1 ) = NN
22	19, 21	eqtr2i 2497	. . . . 5 |- NN = ( ZZ>= ` ( 0 + 1 ) )
23	22	a1i 11	. . . 4 |- ( ph -> NN = ( ZZ>= ` ( 0 + 1 ) ) )
24	2, 23	eleqtrd 2557	. . 3 |- ( ph -> M e. ( ZZ>= ` ( 0 + 1 ) ) )
25	6	simpld 459	. . . 4 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
26		reex 9595	. . . . . 6 |- RR e. _V
27	26	a1i 11	. . . . 5 |- ( ph -> RR e. _V )
28		ovex 6320	. . . . . 6 |- ( 0 ... M ) e. _V
29	28	a1i 11	. . . . 5 |- ( ph -> ( 0 ... M ) e. _V )
30		elmapg 7445	. . . . 5 |- ( ( RR e. _V /\ ( 0 ... M ) e. _V ) -> ( Q e. ( RR ^m ( 0 ... M ) ) <-> Q : ( 0 ... M ) --> RR ) )
31	27, 29, 30	syl2anc 661	. . . 4 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) <-> Q : ( 0 ... M ) --> RR ) )
32	25, 31	mpbid 210	. . 3 |- ( ph -> Q : ( 0 ... M ) --> RR )
33	7	simprd 463	. . . 4 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
34	33	r19.21bi 2836	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
35		fourierdlem81.f	. . . . 5 |- ( ph -> F : RR --> CC )
36	35	adantr 465	. . . 4 |- ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> F : RR --> CC )
37		fourierdlem81.a	. . . . . . . 8 |- ( ph -> A e. RR )
38	9, 37	eqeltrd 2555	. . . . . . 7 |- ( ph -> ( Q ` 0 ) e. RR )
39		fourierdlem81.b	. . . . . . . 8 |- ( ph -> B e. RR )
40	11, 39	eqeltrd 2555	. . . . . . 7 |- ( ph -> ( Q ` M ) e. RR )
41		iccssre 11618	. . . . . . 7 |- ( ( ( Q ` 0 ) e. RR /\ ( Q ` M ) e. RR ) -> ( ( Q ` 0 ) [,] ( Q ` M ) ) C_ RR )
42	38, 40, 41	syl2anc 661	. . . . . 6 |- ( ph -> ( ( Q ` 0 ) [,] ( Q ` M ) ) C_ RR )
43	42	adantr 465	. . . . 5 |- ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( ( Q ` 0 ) [,] ( Q ` M ) ) C_ RR )
44		simpr 461	. . . . 5 |- ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
45	43, 44	sseldd 3510	. . . 4 |- ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> x e. RR )
46	36, 45	ffvelrnd 6033	. . 3 |- ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( F ` x ) e. CC )
47	32	adantr 465	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
48		elfzofz 11823	. . . . . 6 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
49	48	adantl 466	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
50	47, 49	ffvelrnd 6033	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
51		fzofzp1 11889	. . . . . 6 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
52	51	adantl 466	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
53	47, 52	ffvelrnd 6033	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
54	35	feqmptd 5927	. . . . . . . 8 |- ( ph -> F = ( x e. RR |-> ( F ` x ) ) )
55	54	reseq1d 5278	. . . . . . 7 |- ( ph -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( x e. RR |-> ( F ` x ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
56	55	adantr 465	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( x e. RR |-> ( F ` x ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
57		ioossre 11598	. . . . . . . 8 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
58	57	a1i 11	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
59		resmpt 5329	. . . . . . 7 |- ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR -> ( ( x e. RR |-> ( F ` x ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
60	58, 59	syl 16	. . . . . 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 ) ) )
61		eqidd 2468	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
62	56, 60, 61	3eqtrrd 2513	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
63		fourierdlem81.cncf	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
64		fourierdlem81.l	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
65		fourierdlem81.r	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
66	50, 53, 63, 64, 65	iblcncfioo 31619	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. L^1 )
67	62, 66	eqeltrd 2555	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
68	35	ad2antrr 725	. . . . 5 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> F : RR --> CC )
69		iccssre 11618	. . . . . . 7 |- ( ( ( Q ` i ) e. RR /\ ( Q ` ( i + 1 ) ) e. RR ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ RR )
70	50, 53, 69	syl2anc 661	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ RR )
71	70	sselda 3509	. . . . 5 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. RR )
72	68, 71	ffvelrnd 6033	. . . 4 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
73	50, 53, 67, 72	ibliooicc 31612	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
74	17, 24, 32, 34, 46, 73	itgspltprt 31620	. 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 )
75		fourierdlem81.s	. . . . . . . 8 |- S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) )
76	75	a1i 11	. . . . . . 7 |- ( ph -> S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) ) )
77		fveq2 5872	. . . . . . . . 9 |- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
78	77	oveq1d 6310	. . . . . . . 8 |- ( i = 0 -> ( ( Q ` i ) + T ) = ( ( Q ` 0 ) + T ) )
79	78	adantl 466	. . . . . . 7 |- ( ( ph /\ i = 0 ) -> ( ( Q ` i ) + T ) = ( ( Q ` 0 ) + T ) )
80	2	nnnn0d 10864	. . . . . . . . 9 |- ( ph -> M e. NN0 )
81		nn0uz 11128	. . . . . . . . . 10 |- NN0 = ( ZZ>= ` 0 )
82	81	a1i 11	. . . . . . . . 9 |- ( ph -> NN0 = ( ZZ>= ` 0 ) )
83	80, 82	eleqtrd 2557	. . . . . . . 8 |- ( ph -> M e. ( ZZ>= ` 0 ) )
84		eluzfz1 11705	. . . . . . . 8 |- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
85	83, 84	syl 16	. . . . . . 7 |- ( ph -> 0 e. ( 0 ... M ) )
86		fourierdlem81.t	. . . . . . . . 9 |- ( ph -> T e. RR+ )
87	86	rpred 11268	. . . . . . . 8 |- ( ph -> T e. RR )
88	38, 87	readdcld 9635	. . . . . . 7 |- ( ph -> ( ( Q ` 0 ) + T ) e. RR )
89	76, 79, 85, 88	fvmptd 5962	. . . . . 6 |- ( ph -> ( S ` 0 ) = ( ( Q ` 0 ) + T ) )
90	9	oveq1d 6310	. . . . . 6 |- ( ph -> ( ( Q ` 0 ) + T ) = ( A + T ) )
91	89, 90	eqtr2d 2509	. . . . 5 |- ( ph -> ( A + T ) = ( S ` 0 ) )
92		fveq2 5872	. . . . . . . . 9 |- ( i = M -> ( Q ` i ) = ( Q ` M ) )
93		eqidd 2468	. . . . . . . . 9 |- ( i = M -> T = T )
94	92, 93	oveq12d 6313	. . . . . . . 8 |- ( i = M -> ( ( Q ` i ) + T ) = ( ( Q ` M ) + T ) )
95	94	adantl 466	. . . . . . 7 |- ( ( ph /\ i = M ) -> ( ( Q ` i ) + T ) = ( ( Q ` M ) + T ) )
96		eluzfz2 11706	. . . . . . . 8 |- ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
97	83, 96	syl 16	. . . . . . 7 |- ( ph -> M e. ( 0 ... M ) )
98	40, 87	readdcld 9635	. . . . . . 7 |- ( ph -> ( ( Q ` M ) + T ) e. RR )
99	76, 95, 97, 98	fvmptd 5962	. . . . . 6 |- ( ph -> ( S ` M ) = ( ( Q ` M ) + T ) )
100	11	oveq1d 6310	. . . . . 6 |- ( ph -> ( ( Q ` M ) + T ) = ( B + T ) )
101	99, 100	eqtr2d 2509	. . . . 5 |- ( ph -> ( B + T ) = ( S ` M ) )
102	91, 101	oveq12d 6313	. . . 4 |- ( ph -> ( ( A + T ) [,] ( B + T ) ) = ( ( S ` 0 ) [,] ( S ` M ) ) )
103		itgeq1 22047	. . . 4 |- ( ( ( A + T ) [,] ( B + T ) ) = ( ( S ` 0 ) [,] ( S ` M ) ) -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( ( S ` 0 ) [,] ( S ` M ) ) ( F ` x ) _d x )
104	102, 103	syl 16	. . 3 |- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( ( S ` 0 ) [,] ( S ` M ) ) ( F ` x ) _d x )
105	32	ffvelrnda 6032	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
106	87	adantr 465	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... M ) ) -> T e. RR )
107	105, 106	readdcld 9635	. . . . 5 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( Q ` i ) + T ) e. RR )
108	107, 75	fmptd 6056	. . . 4 |- ( ph -> S : ( 0 ... M ) --> RR )
109	87	adantr 465	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> T e. RR )
110	50, 53, 109	ltadd1d 10157	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( ( Q ` i ) + T ) < ( ( Q ` ( i + 1 ) ) + T ) ) )
111	34, 110	mpbid 210	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + T ) < ( ( Q ` ( i + 1 ) ) + T ) )
112	49, 107	syldan 470	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + T ) e. RR )
113	75	fvmpt2 5964	. . . . . . 7 |- ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) + T ) e. RR ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
114	49, 112, 113	syl2anc 661	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
115		nfcv 2629	. . . . . . . . . 10 |- F/_ j ( ( Q ` i ) + T )
116		nfcv 2629	. . . . . . . . . 10 |- F/_ i ( ( Q ` j ) + T )
117		fveq2 5872	. . . . . . . . . . 11 |- ( i = j -> ( Q ` i ) = ( Q ` j ) )
118	117	oveq1d 6310	. . . . . . . . . 10 |- ( i = j -> ( ( Q ` i ) + T ) = ( ( Q ` j ) + T ) )
119	115, 116, 118	cbvmpt 4543	. . . . . . . . 9 |- ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) ) = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) )
120	75, 119	eqtri 2496	. . . . . . . 8 |- S = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) )
121	120	a1i 11	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> S = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) )
122		fveq2 5872	. . . . . . . . 9 |- ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
123	122	oveq1d 6310	. . . . . . . 8 |- ( j = ( i + 1 ) -> ( ( Q ` j ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
124	123	adantl 466	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
125	53, 109	readdcld 9635	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR )
126	121, 124, 52, 125	fvmptd 5962	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) + T ) )
127	114, 126	breq12d 4466	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` i ) < ( S ` ( i + 1 ) ) <-> ( ( Q ` i ) + T ) < ( ( Q ` ( i + 1 ) ) + T ) ) )
128	111, 127	mpbird 232	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` i ) < ( S ` ( i + 1 ) ) )
129	35	adantr 465	. . . . 5 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> F : RR --> CC )
130	89, 88	eqeltrd 2555	. . . . . . . 8 |- ( ph -> ( S ` 0 ) e. RR )
131	130	adantr 465	. . . . . . 7 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( S ` 0 ) e. RR )
132	99, 98	eqeltrd 2555	. . . . . . . 8 |- ( ph -> ( S ` M ) e. RR )
133	132	adantr 465	. . . . . . 7 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( S ` M ) e. RR )
134		iccssre 11618	. . . . . . 7 |- ( ( ( S ` 0 ) e. RR /\ ( S ` M ) e. RR ) -> ( ( S ` 0 ) [,] ( S ` M ) ) C_ RR )
135	131, 133, 134	syl2anc 661	. . . . . 6 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( ( S ` 0 ) [,] ( S ` M ) ) C_ RR )
136		simpr 461	. . . . . 6 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> x e. ( ( S ` 0 ) [,] ( S ` M ) ) )
137	135, 136	sseldd 3510	. . . . 5 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> x e. RR )
138	129, 137	ffvelrnd 6033	. . . 4 |- ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( F ` x ) e. CC )
139	114, 112	eqeltrd 2555	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` i ) e. RR )
140	126, 125	eqeltrd 2555	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` ( i + 1 ) ) e. RR )
141		ioosscn 31414	. . . . . . . . 9 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
142	141	a1i 11	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
143		nfcv 2629	. . . . . . . . 9 |- F/_ w CC
144		nfcv 2629	. . . . . . . . 9 |- F/_ x CC
145		nfv 1683	. . . . . . . . 9 |- F/ x E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T )
146		nfv 1683	. . . . . . . . 9 |- F/ w E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T )
147		eqeq1 2471	. . . . . . . . . . 11 |- ( w = x -> ( w = ( z + T ) <-> x = ( z + T ) ) )
148	147	rexbidv 2978	. . . . . . . . . 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 ) ) )
149		nfv 1683	. . . . . . . . . . . 12 |- F/ y x = ( z + T )
150		nfv 1683	. . . . . . . . . . . 12 |- F/ z x = ( y + T )
151		oveq1 6302	. . . . . . . . . . . . 13 |- ( z = y -> ( z + T ) = ( y + T ) )
152	151	eqeq2d 2481	. . . . . . . . . . . 12 |- ( z = y -> ( x = ( z + T ) <-> x = ( y + T ) ) )
153	149, 150, 152	cbvrex 3090	. . . . . . . . . . 11 |- ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) <-> E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) )
154	153	a1i 11	. . . . . . . . . 10 |- ( w = x -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) <-> E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) ) )
155	148, 154	bitrd 253	. . . . . . . . 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 ) ) )
156	143, 144, 145, 146, 155	cbvrab 3116	. . . . . . . 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 ) }
157		fdm 5741	. . . . . . . . . . . 12 |- ( F : RR --> CC -> dom F = RR )
158	35, 157	syl 16	. . . . . . . . . . 11 |- ( ph -> dom F = RR )
159		feq2 5720	. . . . . . . . . . 11 |- ( dom F = RR -> ( F : dom F --> CC <-> F : RR --> CC ) )
160	158, 159	syl 16	. . . . . . . . . 10 |- ( ph -> ( F : dom F --> CC <-> F : RR --> CC ) )
161	35, 160	mpbird 232	. . . . . . . . 9 |- ( ph -> F : dom F --> CC )
162	161	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F : dom F --> CC )
163	57	sseli 3505	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> z e. RR )
164	163	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. RR )
165	87	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> T e. RR )
166	164, 165	readdcld 9635	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z + T ) e. RR )
167	166	adantlr 714	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z + T ) e. RR )
168	167	3adant3 1016	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> ( z + T ) e. RR )
169		simp3 998	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> w = ( z + T ) )
170	158	3ad2ant1 1017	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> dom F = RR )
171	170	3adant1r 1221	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> dom F = RR )
172	169, 171	eleq12d 2549	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> ( w e. dom F <-> ( z + T ) e. RR ) )
173	168, 172	mpbird 232	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> w e. dom F )
174	173	3exp 1195	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( w = ( z + T ) -> w e. dom F ) ) )
175	174	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ w e. CC ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( w = ( z + T ) -> w e. dom F ) ) )
176	175	rexlimdv 2957	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ w e. CC ) -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) -> w e. dom F ) )
177	176	ralrimiva 2881	. . . . . . . . 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 ) )
178		rabss 3582	. . . . . . . . 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 ) )
179	177, 178	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 )
180		simpl 457	. . . . . . . . . 10 |- ( ( ph /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
181	180	adantlr 714	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
182	37	rexrd 9655	. . . . . . . . . . 11 |- ( ph -> A e. RR* )
183	181, 182	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A e. RR* )
184	39	rexrd 9655	. . . . . . . . . . 11 |- ( ph -> B e. RR* )
185	181, 184	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> B e. RR* )
186	3, 2, 1	fourierdlem15 31745	. . . . . . . . . . 11 |- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
187	181, 186	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
188		simpr 461	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0..^ M ) )
189	188	adantr 465	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0..^ M ) )
190		ioossicc 11622	. . . . . . . . . . . 12 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
191	190	sseli 3505	. . . . . . . . . . 11 |- ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
192	191	adantl 466	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
193	183, 185, 187, 189, 192	fourierdlem1 31731	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. ( A [,] B ) )
194		fourierdlem81.fper	. . . . . . . . 9 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
195	181, 193, 194	syl2anc 661	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
196	142, 109, 156, 162, 179, 195, 63	cncfperiod 31540	. . . . . . 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 ) )
197		nfv 1683	. . . . . . . . . . . 12 |- F/ x ( ph /\ i e. ( 0..^ M ) )
198		simpl 457	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( ph /\ i e. ( 0..^ M ) ) )
199	148	elrab 3266	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) )
200	199	simprbi 464	. . . . . . . . . . . . . . . . 17 |- ( 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 ) )
201	200	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ 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 ) )
202	198, 201	jca 532	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) )
203		simpr 461	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) )
204		nfv 1683	. . . . . . . . . . . . . . . . . . 19 |- F/ z ( ph /\ i e. ( 0..^ M ) )
205		nfre1 2928	. . . . . . . . . . . . . . . . . . 19 |- F/ z E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T )
206	204, 205	nfan 1875	. . . . . . . . . . . . . . . . . 18 |- F/ z ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) )
207		nfv 1683	. . . . . . . . . . . . . . . . . 18 |- F/ z ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) )
208		simp3 998	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x = ( z + T ) )
209	166	3adant3 1016	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( z + T ) e. RR )
210	208, 209	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x e. RR )
211	210	3adant1r 1221	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x e. RR )
212		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
213	50	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
214	213	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
215	53	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
216	215	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
217		elioo2 11582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( 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 ) ) ) ) )
218	214, 216, 217	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( 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 ) ) ) ) )
219	212, 218	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z e. RR /\ ( Q ` i ) < z /\ z < ( Q ` ( i + 1 ) ) ) )
220	219	simp2d 1009	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < z )
221	50	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
222	163	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. RR )
223	109	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> T e. RR )
224	221, 222, 223	ltadd1d 10157	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) < z <-> ( ( Q ` i ) + T ) < ( z + T ) ) )
225	220, 224	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) + T ) < ( z + T ) )
226	225	3adant3 1016	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( ( Q ` i ) + T ) < ( z + T ) )
227	114	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
228		simp3 998	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x = ( z + T ) )
229	227, 228	breq12d 4466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( ( S ` i ) < x <-> ( ( Q ` i ) + T ) < ( z + T ) ) )
230	226, 229	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( S ` i ) < x )
231	219	simp3d 1010	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z < ( Q ` ( i + 1 ) ) )
232	53	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
233	222, 232, 223	ltadd1d 10157	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z < ( Q ` ( i + 1 ) ) <-> ( z + T ) < ( ( Q ` ( i + 1 ) ) + T ) ) )
234	231, 233	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z + T ) < ( ( Q ` ( i + 1 ) ) + T ) )
235	234	3adant3 1016	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( z + T ) < ( ( Q ` ( i + 1 ) ) + T ) )
236	126	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( S ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) + T ) )
237	228, 236	breq12d 4466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( x < ( S ` ( i + 1 ) ) <-> ( z + T ) < ( ( Q ` ( i + 1 ) ) + T ) ) )
238	235, 237	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x < ( S ` ( i + 1 ) ) )
239	211, 230, 238	3jca 1176	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) ) ) )
240	239	3exp 1195	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) ) ) ) )
241	240	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) ) ) )
242	206, 207, 241	rexlimd 2951	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) ) ) )
243	203, 242	mpd 15	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) ) ) )
244	139	rexrd 9655	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` i ) e. RR* )
245	244	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( S ` i ) e. RR* )
246	140	rexrd 9655	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` ( i + 1 ) ) e. RR* )
247	246	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( S ` ( i + 1 ) ) e. RR* )
248		elioo2 11582	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) ) ) )
249	245, 247, 248	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) ) ) ) )
250	243, 249	mpbird 232	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
251	202, 250	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) ) )
252	251	ex 434	. . . . . . . . . . . . 13 |- ( ( 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 ) ) ) ) )
253		elioore 11571	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -> x e. RR )
254		ax-resscn 9561	. . . . . . . . . . . . . . . . . . 19 |- RR C_ CC
255	254	sseli 3505	. . . . . . . . . . . . . . . . . 18 |- ( x e. RR -> x e. CC )
256	253, 255	syl 16	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -> x e. CC )
257	256	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. CC )
258	253	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. RR )
259	87	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> T e. RR )
260	258, 259	resubcld 9999	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. RR )
261	260	adantlr 714	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. RR )
262	114	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` i ) - T ) = ( ( ( Q ` i ) + T ) - T ) )
263	254, 50	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. CC )
264	254, 109	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ i e. ( 0..^ M ) ) -> T e. CC )
265	263, 264	pncand 9943	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) + T ) - T ) = ( Q ` i ) )
266	262, 265	eqtr2d 2509	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( ( S ` i ) - T ) )
267	266	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) = ( ( S ` i ) - T ) )
268		simpr 461	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
269	244	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) e. RR* )
270	246	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` ( i + 1 ) ) e. RR* )
271	269, 270, 248	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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 ) ) ) ) )
272	268, 271	mpbid 210	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) )
273	272	simp2d 1009	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) < x )
274	139	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) e. RR )
275	253	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. RR )
276	109	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> T e. RR )
277	274, 275, 276	ltsub1d 10173	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( S ` i ) < x <-> ( ( S ` i ) - T ) < ( x - T ) ) )
278	273, 277	mpbid 210	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( S ` i ) - T ) < ( x - T ) )
279	267, 278	eqbrtrd 4473	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( x - T ) )
280	272	simp3d 1010	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x < ( S ` ( i + 1 ) ) )
281	140	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` ( i + 1 ) ) e. RR )
282	275, 281, 276	ltsub1d 10173	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x < ( S ` ( i + 1 ) ) <-> ( x - T ) < ( ( S ` ( i + 1 ) ) - T ) ) )
283	280, 282	mpbid 210	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) < ( ( S ` ( i + 1 ) ) - T ) )
284	126	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` ( i + 1 ) ) - T ) = ( ( ( Q ` ( i + 1 ) ) + T ) - T ) )
285	254, 53	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
286	285, 264	pncand 9943	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` ( i + 1 ) ) + T ) - T ) = ( Q ` ( i + 1 ) ) )
287	284, 286	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) )
288	287	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) )
289	283, 288	breqtrd 4477	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) < ( Q ` ( i + 1 ) ) )
290	261, 279, 289	3jca 1176	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( x - T ) e. RR /\ ( Q ` i ) < ( x - T ) /\ ( x - T ) < ( Q ` ( i + 1 ) ) ) )
291	213	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
292	215	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
293		elioo2 11582	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* ) -> ( ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( ( x - T ) e. RR /\ ( Q ` i ) < ( x - T ) /\ ( x - T ) < ( Q ` ( i + 1 ) ) ) ) )
294	291, 292, 293	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( ( x - T ) e. RR /\ ( Q ` i ) < ( x - T ) /\ ( x - T ) < ( Q ` ( i + 1 ) ) ) ) )
295	290, 294	mpbird 232	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
296	258, 255	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. CC )
297	254, 259	sseldi 3507	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> T e. CC )
298	296, 297	npcand 9946	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( x - T ) + T ) = x )
299	298	eqcomd 2475	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x = ( ( x - T ) + T ) )
300	299	adantlr 714	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x = ( ( x - T ) + T ) )
301		oveq1 6302	. . . . . . . . . . . . . . . . . . 19 |- ( z = ( x - T ) -> ( z + T ) = ( ( x - T ) + T ) )
302	301	eqeq2d 2481	. . . . . . . . . . . . . . . . . 18 |- ( z = ( x - T ) -> ( x = ( z + T ) <-> x = ( ( x - T ) + T ) ) )
303	302	rspcev 3219	. . . . . . . . . . . . . . . . 17 |- ( ( ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( ( x - T ) + T ) ) -> E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) )
304	295, 300, 303	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) )
305	257, 304	jca 532	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x e. CC /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) )
306	305, 199	sylibr 212	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) } )
307	306	ex 434	. . . . . . . . . . . . 13 |- ( ( 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 ) } ) )
308	252, 307	impbid 191	. . . . . . . . . . . 12 |- ( ( 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 ) ) ) ) )
309	197, 308	alrimi 1825	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A. x ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } <-> x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) )
310		dfcleq 2460	. . . . . . . . . . 11 |- ( { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } = ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) <-> A. x ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } <-> x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) )
311	309, 310	sylibr 212	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } = ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
312	311	reseq2d 5279	. . . . . . . . 9 |- ( ( 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 ) ) ) ) )
313	35	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F : RR --> CC )
314		ioossre 11598	. . . . . . . . . . 11 |- ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) C_ RR
315	314	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) C_ RR )
316	313, 315	feqresmpt 5928	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) = ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
317	312, 316	eqtrd 2508	. . . . . . . 8 |- ( ( 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 ) ) )
318	311	oveq1d 6310	. . . . . . . 8 |- ( ( 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 ) )
319	317, 318	eleq12d 2549	. . . . . . 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 ) <-> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -cn-> CC ) ) )
320	196, 319	mpbid 210	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -cn-> CC ) )
321	57, 158	syl5sseqr 3558	. . . . . . . . 9 |- ( ph -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
322	321	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
323		eqid 2467	. . . . . . . 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 ) }
324		simpll 753	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
325	324, 182	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A e. RR* )
326	324, 184	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> B e. RR* )
327	324, 186	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
328	188	adantr 465	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0..^ M ) )
329	190, 212	sseldi 3507	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
330	325, 326, 327, 328, 329	fourierdlem1 31731	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( A [,] B ) )
331		nfv 1683	. . . . . . . . . 10 |- F/ x ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` ( z + T ) ) = ( F ` z ) )
332		eleq1 2539	. . . . . . . . . . . 12 |- ( x = z -> ( x e. ( A [,] B ) <-> z e. ( A [,] B ) ) )
333	332	anbi2d 703	. . . . . . . . . . 11 |- ( x = z -> ( ( ph /\ x e. ( A [,] B ) ) <-> ( ph /\ z e. ( A [,] B ) ) ) )
334		oveq1 6302	. . . . . . . . . . . . 13 |- ( x = z -> ( x + T ) = ( z + T ) )
335	334	fveq2d 5876	. . . . . . . . . . . 12 |- ( x = z -> ( F ` ( x + T ) ) = ( F ` ( z + T ) ) )
336		fveq2 5872	. . . . . . . . . . . 12 |- ( x = z -> ( F ` x ) = ( F ` z ) )
337	335, 336	eqeq12d 2489	. . . . . . . . . . 11 |- ( x = z -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( z + T ) ) = ( F ` z ) ) )
338	333, 337	imbi12d 320	. . . . . . . . . 10 |- ( x = z -> ( ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` ( z + T ) ) = ( F ` z ) ) ) )
339	331, 338, 194	chvar 1982	. . . . . . . . 9 |- ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` ( z + T ) ) = ( F ` z ) )
340	324, 330, 339	syl2anc 661	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( z + T ) ) = ( F ` z ) )
341	162, 142, 322, 264, 323, 179, 340, 64	limcperiod 31493	. . . . . . 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 ) ) )
342	126	eqcomd 2475	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) = ( S ` ( i + 1 ) ) )
343	317, 342	oveq12d 6313	. . . . . . 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 ) ) ) )
344	341, 343	eleqtrd 2557	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) lim CC ( S ` ( i + 1 ) ) ) )
345	162, 142, 322, 264, 323, 179, 340, 65	limcperiod 31493	. . . . . . 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 ) ) )
346	114	eqcomd 2475	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + T ) = ( S ` i ) )
347	317, 346	oveq12d 6313	. . . . . . 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 ) ) )
348	345, 347	eleqtrd 2557	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) lim CC ( S ` i ) ) )
349	139, 140, 320, 344, 348	iblcncfioo 31619	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
350	313	adantr 465	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> F : RR --> CC )
351	139	adantr 465	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) e. RR )
352	140	adantr 465	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( S ` ( i + 1 ) ) e. RR )
353		simpr 461	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) )
354		eliccre 31427	. . . . . . 7 |- ( ( ( S ` i ) e. RR /\ ( S ` ( i + 1 ) ) e. RR /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x e. RR )
355	351, 352, 353, 354	syl3anc 1228	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x e. RR )
356	350, 355	ffvelrnd 6033	. . . . 5 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
357	139, 140, 349, 356	ibliooicc 31612	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
358	17, 24, 108, 128, 138, 357	itgspltprt 31620	. . 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 )
359		fourierdlem81.g	. . . . . . . . . . . . . . 15 |- G = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) )
360	359	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> G = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) ) )
361		iftrue 3951	. . . . . . . . . . . . . . . . . 18 |- ( x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = R )
362		iftrue 3951	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) = R )
363	362	eqcomd 2475	. . . . . . . . . . . . . . . . . 18 |- ( x = ( Q ` i ) -> R = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
364	361, 363	eqtrd 2508	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) ) )
365	364	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) ) )
366		iffalse 3954	. . . . . . . . . . . . . . . . . . . 20 |- ( -. x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) )
367	366	adantr 465	. . . . . . . . . . . . . . . . . . 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 + 1 ) ) , L , ( F ` x ) ) )
368		iftrue 3951	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = L )
369	368	adantl 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = L )
370		iffalse 3954	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. 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 ) ) )
371	370	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( -. 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 ) ) )
372		iftrue 3951	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = L )
373	372	adantl 466	. . . . . . . . . . . . . . . . . . . 20 |- ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = L )
374	371, 373	eqtr2d 2509	. . . . . . . . . . . . . . . . . . 19 |- ( ( -. 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 ) ) ) )
375	367, 369, 374