Theorem fourierdlem92 31822

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

Hypotheses

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

Assertion

Ref	Expression
fourierdlem92	|- ( 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, L   i, M, x   m, M, p   Q, i, x   Q, p   x, R   S, i, x   S, p   T, i, x   T, m, p   ph, i, x

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

Proof of Theorem fourierdlem92

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

Step	Hyp	Ref	Expression
1		fourierdlem92.a	. . . 4 |- ( ph -> A e. RR )
2	1	adantr 465	. . 3 |- ( ( ph /\ 0 < T ) -> A e. RR )
3		fourierdlem92.b	. . . 4 |- ( ph -> B e. RR )
4	3	adantr 465	. . 3 |- ( ( ph /\ 0 < T ) -> B e. RR )
5		fourierdlem92.p	. . 3 |- 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 ) ) ) } )
6		fourierdlem92.m	. . . 4 |- ( ph -> M e. NN )
7	6	adantr 465	. . 3 |- ( ( ph /\ 0 < T ) -> M e. NN )
8		fourierdlem92.t	. . . . 5 |- ( ph -> T e. RR )
9	8	adantr 465	. . . 4 |- ( ( ph /\ 0 < T ) -> T e. RR )
10		simpr 461	. . . 4 |- ( ( ph /\ 0 < T ) -> 0 < T )
11	9, 10	elrpd 11266	. . 3 |- ( ( ph /\ 0 < T ) -> T e. RR+ )
12		fourierdlem92.q	. . . 4 |- ( ph -> Q e. ( P ` M ) )
13	12	adantr 465	. . 3 |- ( ( ph /\ 0 < T ) -> Q e. ( P ` M ) )
14		fourierdlem92.fper	. . . 4 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
15	14	adantlr 714	. . 3 |- ( ( ( ph /\ 0 < T ) /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
16		nfcv 2629	. . . 4 |- F/_ i ( ( Q ` j ) + T )
17		nfcv 2629	. . . 4 |- F/_ j ( ( Q ` i ) + T )
18		fveq2 5872	. . . . 5 |- ( j = i -> ( Q ` j ) = ( Q ` i ) )
19	18	oveq1d 6310	. . . 4 |- ( j = i -> ( ( Q ` j ) + T ) = ( ( Q ` i ) + T ) )
20	16, 17, 19	cbvmpt 4543	. . 3 |- ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) )
21		fourierdlem92.f	. . . 4 |- ( ph -> F : RR --> CC )
22	21	adantr 465	. . 3 |- ( ( ph /\ 0 < T ) -> F : RR --> CC )
23		fourierdlem92.cncf	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
24	23	adantlr 714	. . 3 |- ( ( ( ph /\ 0 < T ) /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
25		fourierdlem92.r	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
26	25	adantlr 714	. . 3 |- ( ( ( ph /\ 0 < T ) /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
27		fourierdlem92.l	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
28	27	adantlr 714	. . 3 |- ( ( ( ph /\ 0 < T ) /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
29		nfcv 2629	. . . 4 |- F/_ x if ( y = ( Q ` i ) , R , if ( y = ( Q ` ( i + 1 ) ) , L , ( F ` y ) ) )
30		nfcv 2629	. . . 4 |- F/_ y if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) )
31		eqeq1 2471	. . . . 5 |- ( y = x -> ( y = ( Q ` i ) <-> x = ( Q ` i ) ) )
32		eqidd 2468	. . . . 5 |- ( y = x -> R = R )
33		eqeq1 2471	. . . . . 6 |- ( y = x -> ( y = ( Q ` ( i + 1 ) ) <-> x = ( Q ` ( i + 1 ) ) ) )
34		eqidd 2468	. . . . . 6 |- ( y = x -> L = L )
35		fveq2 5872	. . . . . 6 |- ( y = x -> ( F ` y ) = ( F ` x ) )
36	33, 34, 35	ifeq123d 31337	. . . . 5 |- ( y = x -> if ( y = ( Q ` ( i + 1 ) ) , L , ( F ` y ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) )
37	31, 32, 36	ifeq123d 31337	. . . 4 |- ( y = x -> if ( y = ( Q ` i ) , R , if ( y = ( Q ` ( i + 1 ) ) , L , ( F ` y ) ) ) = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) )
38	29, 30, 37	cbvmpt 4543	. . 3 |- ( y e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( y = ( Q ` i ) , R , if ( y = ( Q ` ( i + 1 ) ) , L , ( F ` y ) ) ) ) = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) )
39		eqid 2467	. . 3 |- ( x e. ( ( ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) ` i ) [,] ( ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) ` ( i + 1 ) ) ) |-> ( ( y e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( y = ( Q ` i ) , R , if ( y = ( Q ` ( i + 1 ) ) , L , ( F ` y ) ) ) ) ` ( x - T ) ) ) = ( x e. ( ( ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) ` i ) [,] ( ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) ` ( i + 1 ) ) ) |-> ( ( y e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( y = ( Q ` i ) , R , if ( y = ( Q ` ( i + 1 ) ) , L , ( F ` y ) ) ) ) ` ( x - T ) ) )
40	2, 4, 5, 7, 11, 13, 15, 20, 22, 24, 26, 28, 38, 39	fourierdlem81 31811	. 2 |- ( ( ph /\ 0 < T ) -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
41		simpr 461	. . . . . . . 8 |- ( ( ph /\ T = 0 ) -> T = 0 )
42	41	oveq2d 6311	. . . . . . 7 |- ( ( ph /\ T = 0 ) -> ( A + T ) = ( A + 0 ) )
43	1	recnd 9634	. . . . . . . . 9 |- ( ph -> A e. CC )
44	43	adantr 465	. . . . . . . 8 |- ( ( ph /\ T = 0 ) -> A e. CC )
45	44	addid1d 9791	. . . . . . 7 |- ( ( ph /\ T = 0 ) -> ( A + 0 ) = A )
46	42, 45	eqtrd 2508	. . . . . 6 |- ( ( ph /\ T = 0 ) -> ( A + T ) = A )
47	41	oveq2d 6311	. . . . . . 7 |- ( ( ph /\ T = 0 ) -> ( B + T ) = ( B + 0 ) )
48	3	recnd 9634	. . . . . . . . 9 |- ( ph -> B e. CC )
49	48	adantr 465	. . . . . . . 8 |- ( ( ph /\ T = 0 ) -> B e. CC )
50	49	addid1d 9791	. . . . . . 7 |- ( ( ph /\ T = 0 ) -> ( B + 0 ) = B )
51	47, 50	eqtrd 2508	. . . . . 6 |- ( ( ph /\ T = 0 ) -> ( B + T ) = B )
52	46, 51	oveq12d 6313	. . . . 5 |- ( ( ph /\ T = 0 ) -> ( ( A + T ) [,] ( B + T ) ) = ( A [,] B ) )
53		itgeq1 22047	. . . . 5 |- ( ( ( A + T ) [,] ( B + T ) ) = ( A [,] B ) -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
54	52, 53	syl 16	. . . 4 |- ( ( ph /\ T = 0 ) -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
55	54	adantlr 714	. . 3 |- ( ( ( ph /\ -. 0 < T ) /\ T = 0 ) -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
56		simpll 753	. . . 4 |- ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> ph )
57		simpr 461	. . . . . . . 8 |- ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> -. T = 0 )
58		simplr 754	. . . . . . . 8 |- ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> -. 0 < T )
59	57, 58	jca 532	. . . . . . 7 |- ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> ( -. T = 0 /\ -. 0 < T ) )
60		ioran 490	. . . . . . 7 |- ( -. ( T = 0 \/ 0 < T ) <-> ( -. T = 0 /\ -. 0 < T ) )
61	59, 60	sylibr 212	. . . . . 6 |- ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> -. ( T = 0 \/ 0 < T ) )
62	56, 8	syl 16	. . . . . . 7 |- ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> T e. RR )
63		0re 9608	. . . . . . . 8 |- 0 e. RR
64	63	a1i 11	. . . . . . 7 |- ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> 0 e. RR )
65		axlttri 9668	. . . . . . 7 |- ( ( T e. RR /\ 0 e. RR ) -> ( T < 0 <-> -. ( T = 0 \/ 0 < T ) ) )
66	62, 64, 65	syl2anc 661	. . . . . 6 |- ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> ( T < 0 <-> -. ( T = 0 \/ 0 < T ) ) )
67	61, 66	mpbird 232	. . . . 5 |- ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> T < 0 )
68	62	lt0neg1d 10134	. . . . 5 |- ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> ( T < 0 <-> 0 < -u T ) )
69	67, 68	mpbid 210	. . . 4 |- ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> 0 < -u T )
70		ax-resscn 9561	. . . . . . . . . . . . 13 |- RR C_ CC
71	1, 8	readdcld 9635	. . . . . . . . . . . . 13 |- ( ph -> ( A + T ) e. RR )
72	70, 71	sseldi 3507	. . . . . . . . . . . 12 |- ( ph -> ( A + T ) e. CC )
73	70, 8	sseldi 3507	. . . . . . . . . . . 12 |- ( ph -> T e. CC )
74	72, 73	negsubd 9948	. . . . . . . . . . 11 |- ( ph -> ( ( A + T ) + -u T ) = ( ( A + T ) - T ) )
75	43, 73	pncand 9943	. . . . . . . . . . 11 |- ( ph -> ( ( A + T ) - T ) = A )
76	74, 75	eqtr2d 2509	. . . . . . . . . 10 |- ( ph -> A = ( ( A + T ) + -u T ) )
77	76	eqcomd 2475	. . . . . . . . 9 |- ( ph -> ( ( A + T ) + -u T ) = A )
78	3, 8	readdcld 9635	. . . . . . . . . . . 12 |- ( ph -> ( B + T ) e. RR )
79	70, 78	sseldi 3507	. . . . . . . . . . 11 |- ( ph -> ( B + T ) e. CC )
80	79, 73	negsubd 9948	. . . . . . . . . 10 |- ( ph -> ( ( B + T ) + -u T ) = ( ( B + T ) - T ) )
81	48, 73	pncand 9943	. . . . . . . . . 10 |- ( ph -> ( ( B + T ) - T ) = B )
82	80, 81	eqtrd 2508	. . . . . . . . 9 |- ( ph -> ( ( B + T ) + -u T ) = B )
83	77, 82	oveq12d 6313	. . . . . . . 8 |- ( ph -> ( ( ( A + T ) + -u T ) [,] ( ( B + T ) + -u T ) ) = ( A [,] B ) )
84		eqidd 2468	. . . . . . . 8 |- ( ph -> ( A [,] B ) = ( A [,] B ) )
85	83, 84	eqtr2d 2509	. . . . . . 7 |- ( ph -> ( A [,] B ) = ( ( ( A + T ) + -u T ) [,] ( ( B + T ) + -u T ) ) )
86		itgeq1 22047	. . . . . . 7 |- ( ( A [,] B ) = ( ( ( A + T ) + -u T ) [,] ( ( B + T ) + -u T ) ) -> S. ( A [,] B ) ( F ` x ) _d x = S. ( ( ( A + T ) + -u T ) [,] ( ( B + T ) + -u T ) ) ( F ` x ) _d x )
87	85, 86	syl 16	. . . . . 6 |- ( ph -> S. ( A [,] B ) ( F ` x ) _d x = S. ( ( ( A + T ) + -u T ) [,] ( ( B + T ) + -u T ) ) ( F ` x ) _d x )
88	87	adantr 465	. . . . 5 |- ( ( ph /\ 0 < -u T ) -> S. ( A [,] B ) ( F ` x ) _d x = S. ( ( ( A + T ) + -u T ) [,] ( ( B + T ) + -u T ) ) ( F ` x ) _d x )
89	1	adantr 465	. . . . . . 7 |- ( ( ph /\ 0 < -u T ) -> A e. RR )
90	8	adantr 465	. . . . . . 7 |- ( ( ph /\ 0 < -u T ) -> T e. RR )
91	89, 90	readdcld 9635	. . . . . 6 |- ( ( ph /\ 0 < -u T ) -> ( A + T ) e. RR )
92	3	adantr 465	. . . . . . 7 |- ( ( ph /\ 0 < -u T ) -> B e. RR )
93	92, 90	readdcld 9635	. . . . . 6 |- ( ( ph /\ 0 < -u T ) -> ( B + T ) e. RR )
94		eqid 2467	. . . . . 6 |- ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
95	6	adantr 465	. . . . . 6 |- ( ( ph /\ 0 < -u T ) -> M e. NN )
96	90	renegcld 9998	. . . . . . 7 |- ( ( ph /\ 0 < -u T ) -> -u T e. RR )
97		simpr 461	. . . . . . 7 |- ( ( ph /\ 0 < -u T ) -> 0 < -u T )
98	96, 97	elrpd 11266	. . . . . 6 |- ( ( ph /\ 0 < -u T ) -> -u T e. RR+ )
99	5	fourierdlem2 31732	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) ) ) ) )
100	6, 99	syl 16	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) ) ) ) )
101	12, 100	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
102	101	simpld 459	. . . . . . . . . . . . . . 15 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
103		elmapi 7452	. . . . . . . . . . . . . . 15 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
104	102, 103	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> Q : ( 0 ... M ) --> RR )
105	104	ffvelrnda 6032	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
106	8	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... M ) ) -> T e. RR )
107	105, 106	readdcld 9635	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( Q ` i ) + T ) e. RR )
108		fourierdlem92.s	. . . . . . . . . . . 12 |- S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) )
109	107, 108	fmptd 6056	. . . . . . . . . . 11 |- ( ph -> S : ( 0 ... M ) --> RR )
110		reex 9595	. . . . . . . . . . . . 13 |- RR e. _V
111	110	a1i 11	. . . . . . . . . . . 12 |- ( ph -> RR e. _V )
112		ovex 6320	. . . . . . . . . . . . 13 |- ( 0 ... M ) e. _V
113	112	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( 0 ... M ) e. _V )
114		elmapg 7445	. . . . . . . . . . . 12 |- ( ( RR e. _V /\ ( 0 ... M ) e. _V ) -> ( S e. ( RR ^m ( 0 ... M ) ) <-> S : ( 0 ... M ) --> RR ) )
115	111, 113, 114	syl2anc 661	. . . . . . . . . . 11 |- ( ph -> ( S e. ( RR ^m ( 0 ... M ) ) <-> S : ( 0 ... M ) --> RR ) )
116	109, 115	mpbird 232	. . . . . . . . . 10 |- ( ph -> S e. ( RR ^m ( 0 ... M ) ) )
117	108	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) ) )
118		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
119	118	oveq1d 6310	. . . . . . . . . . . . . . 15 |- ( i = 0 -> ( ( Q ` i ) + T ) = ( ( Q ` 0 ) + T ) )
120	119	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ i = 0 ) -> ( ( Q ` i ) + T ) = ( ( Q ` 0 ) + T ) )
121		0z 10887	. . . . . . . . . . . . . . . . . 18 |- 0 e. ZZ
122	121	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> 0 e. ZZ )
123	6	nnzd 10977	. . . . . . . . . . . . . . . . 17 |- ( ph -> M e. ZZ )
124	122, 123, 122	3jca 1176	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) )
125	63	leidi 10099	. . . . . . . . . . . . . . . . 17 |- 0 <_ 0
126	125	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 <_ 0 )
127		nnnn0 10814	. . . . . . . . . . . . . . . . . 18 |- ( M e. NN -> M e. NN0 )
128		nn0ge0 10833	. . . . . . . . . . . . . . . . . 18 |- ( M e. NN0 -> 0 <_ M )
129	127, 128	syl 16	. . . . . . . . . . . . . . . . 17 |- ( M e. NN -> 0 <_ M )
130	6, 129	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 <_ M )
131	124, 126, 130	jca32 535	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) /\ ( 0 <_ 0 /\ 0 <_ M ) ) )
132		elfz2 11691	. . . . . . . . . . . . . . 15 |- ( 0 e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) /\ ( 0 <_ 0 /\ 0 <_ M ) ) )
133	131, 132	sylibr 212	. . . . . . . . . . . . . 14 |- ( ph -> 0 e. ( 0 ... M ) )
134	104, 133	ffvelrnd 6033	. . . . . . . . . . . . . . 15 |- ( ph -> ( Q ` 0 ) e. RR )
135	134, 8	readdcld 9635	. . . . . . . . . . . . . 14 |- ( ph -> ( ( Q ` 0 ) + T ) e. RR )
136	117, 120, 133, 135	fvmptd 5962	. . . . . . . . . . . . 13 |- ( ph -> ( S ` 0 ) = ( ( Q ` 0 ) + T ) )
137		simprll 761	. . . . . . . . . . . . . . 15 |- ( ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) -> ( Q ` 0 ) = A )
138	101, 137	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( Q ` 0 ) = A )
139	138	oveq1d 6310	. . . . . . . . . . . . 13 |- ( ph -> ( ( Q ` 0 ) + T ) = ( A + T ) )
140	136, 139	eqtrd 2508	. . . . . . . . . . . 12 |- ( ph -> ( S ` 0 ) = ( A + T ) )
141		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( i = M -> ( Q ` i ) = ( Q ` M ) )
142	141	oveq1d 6310	. . . . . . . . . . . . . . 15 |- ( i = M -> ( ( Q ` i ) + T ) = ( ( Q ` M ) + T ) )
143	142	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ i = M ) -> ( ( Q ` i ) + T ) = ( ( Q ` M ) + T ) )
144	6, 127	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> M e. NN0 )
145		nn0uz 11128	. . . . . . . . . . . . . . . 16 |- NN0 = ( ZZ>= ` 0 )
146	144, 145	syl6eleq 2565	. . . . . . . . . . . . . . 15 |- ( ph -> M e. ( ZZ>= ` 0 ) )
147		eluzfz2 11706	. . . . . . . . . . . . . . 15 |- ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
148	146, 147	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> M e. ( 0 ... M ) )
149	104, 148	ffvelrnd 6033	. . . . . . . . . . . . . . 15 |- ( ph -> ( Q ` M ) e. RR )
150	149, 8	readdcld 9635	. . . . . . . . . . . . . 14 |- ( ph -> ( ( Q ` M ) + T ) e. RR )
151	117, 143, 148, 150	fvmptd 5962	. . . . . . . . . . . . 13 |- ( ph -> ( S ` M ) = ( ( Q ` M ) + T ) )
152		simprlr 762	. . . . . . . . . . . . . . 15 |- ( ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) -> ( Q ` M ) = B )
153	101, 152	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( Q ` M ) = B )
154	153	oveq1d 6310	. . . . . . . . . . . . 13 |- ( ph -> ( ( Q ` M ) + T ) = ( B + T ) )
155	151, 154	eqtrd 2508	. . . . . . . . . . . 12 |- ( ph -> ( S ` M ) = ( B + T ) )
156	140, 155	jca 532	. . . . . . . . . . 11 |- ( ph -> ( ( S ` 0 ) = ( A + T ) /\ ( S ` M ) = ( B + T ) ) )
157	104	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
158		simpr 461	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0..^ M ) )
159		elfzofz 11823	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
160	158, 159	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
161	157, 160	ffvelrnd 6033	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
162		fzofzp1 11889	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
163	158, 162	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
164	157, 163	ffvelrnd 6033	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
165	8	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> T e. RR )
166	101	simprd 463	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
167	166	simprd 463	. . . . . . . . . . . . . . 15 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
168	167	r19.21bi 2836	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
169	161, 164, 165, 168	ltadd1dd 10175	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + T ) < ( ( Q ` ( i + 1 ) ) + T ) )
170	161, 165	readdcld 9635	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + T ) e. RR )
171	160, 170	jca 532	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i e. ( 0 ... M ) /\ ( ( Q ` i ) + T ) e. RR ) )
172	108	fvmpt2 5964	. . . . . . . . . . . . . . 15 |- ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) + T ) e. RR ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
173	171, 172	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
174	108, 20	eqtr4i 2499	. . . . . . . . . . . . . . . 16 |- S = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) )
175	174	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> S = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) )
176		fveq2 5872	. . . . . . . . . . . . . . . . 17 |- ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
177	176	oveq1d 6310	. . . . . . . . . . . . . . . 16 |- ( j = ( i + 1 ) -> ( ( Q ` j ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
178	177	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
179	164, 165	readdcld 9635	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR )
180	175, 178, 163, 179	fvmptd 5962	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) + T ) )
181	173, 180	breq12d 4466	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` i ) < ( S ` ( i + 1 ) ) <-> ( ( Q ` i ) + T ) < ( ( Q ` ( i + 1 ) ) + T ) ) )
182	169, 181	mpbird 232	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( S ` i ) < ( S ` ( i + 1 ) ) )
183	182	ralrimiva 2881	. . . . . . . . . . 11 |- ( ph -> A. i e. ( 0..^ M ) ( S ` i ) < ( S ` ( i + 1 ) ) )
184	156, 183	jca 532	. . . . . . . . . 10 |- ( ph -> ( ( ( S ` 0 ) = ( A + T ) /\ ( S ` M ) = ( B + T ) ) /\ A. i e. ( 0..^ M ) ( S ` i ) < ( S ` ( i + 1 ) ) ) )
185	116, 184	jca 532	. . . . . . . . 9 |- ( ph -> ( S e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( S ` 0 ) = ( A + T ) /\ ( S ` M ) = ( B + T ) ) /\ A. i e. ( 0..^ M ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) )
186		fourierdlem92.h	. . . . . . . . . . 11 |- H = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
187	186	fourierdlem2 31732	. . . . . . . . . 10 |- ( M e. NN -> ( S e. ( H ` M ) <-> ( S e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( S ` 0 ) = ( A + T ) /\ ( S ` M ) = ( B + T ) ) /\ A. i e. ( 0..^ M ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) )
188	6, 187	syl 16	. . . . . . . . 9 |- ( ph -> ( S e. ( H ` M ) <-> ( S e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( S ` 0 ) = ( A + T ) /\ ( S ` M ) = ( B + T ) ) /\ A. i e. ( 0..^ M ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) )
189	185, 188	mpbird 232	. . . . . . . 8 |- ( ph -> S e. ( H ` M ) )
190	186	fveq1i 5873	. . . . . . . . 9 |- ( H ` M ) = ( ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` M )
191	190	a1i 11	. . . . . . . 8 |- ( ph -> ( H ` M ) = ( ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` M ) )
192	189, 191	eleqtrd 2557	. . . . . . 7 |- ( ph -> S e. ( ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` M ) )
193	192	adantr 465	. . . . . 6 |- ( ( ph /\ 0 < -u T ) -> S e. ( ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` M ) )
194	71	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) e. RR )
195	78	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( B + T ) e. RR )
196		simpr 461	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
197		eliccre 31427	. . . . . . . . . . . 12 |- ( ( ( A + T ) e. RR /\ ( B + T ) e. RR /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. RR )
198	194, 195, 196, 197	syl3anc 1228	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. RR )
199	70, 198	sseldi 3507	. . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. CC )
200	73	negcld 9929	. . . . . . . . . . 11 |- ( ph -> -u T e. CC )
201	200	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> -u T e. CC )
202	199, 201	addcld 9627	. . . . . . . . 9 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) e. CC )
203		simpl 457	. . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ph )
204	8	renegcld 9998	. . . . . . . . . . . . . 14 |- ( ph -> -u T e. RR )
205	204	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> -u T e. RR )
206	198, 205	readdcld 9635	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) e. RR )
207	76	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A = ( ( A + T ) + -u T ) )
208	194	rexrd 9655	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) e. RR* )
209	195	rexrd 9655	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( B + T ) e. RR* )
210		iccgelb 11593	. . . . . . . . . . . . . . 15 |- ( ( ( A + T ) e. RR* /\ ( B + T ) e. RR* /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) <_ x )
211	208, 209, 196, 210	syl3anc 1228	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) <_ x )
212	194, 198, 205	leadd1d 10158	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( A + T ) <_ x <-> ( ( A + T ) + -u T ) <_ ( x + -u T ) ) )
213	211, 212	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( A + T ) + -u T ) <_ ( x + -u T ) )
214	207, 213	eqbrtrd 4473	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A <_ ( x + -u T ) )
215		iccleub 11592	. . . . . . . . . . . . . . 15 |- ( ( ( A + T ) e. RR* /\ ( B + T ) e. RR* /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x <_ ( B + T ) )
216	208, 209, 196, 215	syl3anc 1228	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x <_ ( B + T ) )
217	198, 195, 205	leadd1d 10158	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x <_ ( B + T ) <-> ( x + -u T ) <_ ( ( B + T ) + -u T ) ) )
218	216, 217	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) <_ ( ( B + T ) + -u T ) )
219	70, 195	sseldi 3507	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( B + T ) e. CC )
220	203, 73	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> T e. CC )
221	219, 220	negsubd 9948	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( B + T ) + -u T ) = ( ( B + T ) - T ) )
222	81	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( B + T ) - T ) = B )
223	221, 222	eqtrd 2508	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( B + T ) + -u T ) = B )
224	218, 223	breqtrd 4477	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) <_ B )
225	206, 214, 224	3jca 1176	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x + -u T ) e. RR /\ A <_ ( x + -u T ) /\ ( x + -u T ) <_ B ) )
226	203, 1	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A e. RR )
227	203, 3	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> B e. RR )
228		elicc2 11601	. . . . . . . . . . . 12 |- ( ( A e. RR /\ B e. RR ) -> ( ( x + -u T ) e. ( A [,] B ) <-> ( ( x + -u T ) e. RR /\ A <_ ( x + -u T ) /\ ( x + -u T ) <_ B ) ) )
229	226, 227, 228	syl2anc 661	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x + -u T ) e. ( A [,] B ) <-> ( ( x + -u T ) e. RR /\ A <_ ( x + -u T ) /\ ( x + -u T ) <_ B ) ) )
230	225, 229	mpbird 232	. . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) e. ( A [,] B ) )
231	203, 230	jca 532	. . . . . . . . 9 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ph /\ ( x + -u T ) e. ( A [,] B ) ) )
232		eleq1 2539	. . . . . . . . . . . 12 |- ( y = ( x + -u T ) -> ( y e. ( A [,] B ) <-> ( x + -u T ) e. ( A [,] B ) ) )
233	232	anbi2d 703	. . . . . . . . . . 11 |- ( y = ( x + -u T ) -> ( ( ph /\ y e. ( A [,] B ) ) <-> ( ph /\ ( x + -u T ) e. ( A [,] B ) ) ) )
234		oveq1 6302	. . . . . . . . . . . . 13 |- ( y = ( x + -u T ) -> ( y + T ) = ( ( x + -u T ) + T ) )
235	234	fveq2d 5876	. . . . . . . . . . . 12 |- ( y = ( x + -u T ) -> ( F ` ( y + T ) ) = ( F ` ( ( x + -u T ) + T ) ) )
236		fveq2 5872	. . . . . . . . . . . 12 |- ( y = ( x + -u T ) -> ( F ` y ) = ( F ` ( x + -u T ) ) )
237	235, 236	eqeq12d 2489	. . . . . . . . . . 11 |- ( y = ( x + -u T ) -> ( ( F ` ( y + T ) ) = ( F ` y ) <-> ( F ` ( ( x + -u T ) + T ) ) = ( F ` ( x + -u T ) ) ) )
238	233, 237	imbi12d 320	. . . . . . . . . 10 |- ( y = ( x + -u T ) -> ( ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) ) <-> ( ( ph /\ ( x + -u T ) e. ( A [,] B ) ) -> ( F ` ( ( x + -u T ) + T ) ) = ( F ` ( x + -u T ) ) ) ) )
239		nfv 1683	. . . . . . . . . . . 12 |- F/ x ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) )
240		eleq1 2539	. . . . . . . . . . . . . 14 |- ( x = y -> ( x e. ( A [,] B ) <-> y e. ( A [,] B ) ) )
241	240	anbi2d 703	. . . . . . . . . . . . 13 |- ( x = y -> ( ( ph /\ x e. ( A [,] B ) ) <-> ( ph /\ y e. ( A [,] B ) ) ) )
242		oveq1 6302	. . . . . . . . . . . . . . 15 |- ( x = y -> ( x + T ) = ( y + T ) )
243	242	fveq2d 5876	. . . . . . . . . . . . . 14 |- ( x = y -> ( F ` ( x + T ) ) = ( F ` ( y + T ) ) )
244		fveq2 5872	. . . . . . . . . . . . . 14 |- ( x = y -> ( F ` x ) = ( F ` y ) )
245	243, 244	eqeq12d 2489	. . . . . . . . . . . . 13 |- ( x = y -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( y + T ) ) = ( F ` y ) ) )
246	241, 245	imbi12d 320	. . . . . . . . . . . 12 |- ( x = y -> ( ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) ) ) )
247	239, 246, 14	chvar 1982	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) )
248	247	a1i 11	. . . . . . . . . 10 |- ( y e. CC -> ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) ) )
249	238, 248	vtoclga 3182	. . . . . . . . 9 |- ( ( x + -u T ) e. CC -> ( ( ph /\ ( x + -u T ) e. ( A [,] B ) ) -> ( F ` ( ( x + -u T ) + T ) ) = ( F ` ( x + -u T ) ) ) )
250	202, 231, 249	sylc 60	. . . . . . . 8 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( F ` ( ( x + -u T ) + T ) ) = ( F ` ( x + -u T ) ) )
251	199, 220	negsubd 9948	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) = ( x - T ) )
252	251	oveq1d 6310	. . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x + -u T ) + T ) = ( ( x - T ) + T ) )
253	199, 220	npcand 9946	. . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x - T ) + T ) = x )
254		eqidd 2468	. . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x = x )
255	252, 253, 254	3eqtrd 2512	. . . . . . . . 9 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x + -u T ) + T ) = x )
256	255	fveq2d 5876	. . . . . . . 8 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( F ` ( ( x + -u T ) + T ) ) = ( F ` x ) )
257	250, 256	eqtr3d 2510	. . . . . . 7 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( F ` ( x + -u T ) ) = ( F ` x ) )
258	257	adantlr 714	. . . . . 6 |- ( ( ( ph /\ 0 < -u T ) /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( F ` ( x + -u T ) ) = ( F ` x ) )
259		nfcv 2629	. . . . . . 7 |- F/_ i ( ( S ` j ) + -u T )
260		nfcv 2629	. . . . . . 7 |- F/_ j ( ( S ` i ) + -u T )
261		fveq2 5872	. . . . . . . 8 |- ( j = i -> ( S ` j ) = ( S ` i ) )
262	261	oveq1d 6310	. . . . . . 7 |- ( j = i -> ( ( S ` j ) + -u T ) = ( ( S ` i ) + -u T ) )
263	259, 260, 262	cbvmpt 4543	. . . . . 6 |- ( j e. ( 0 ... M ) |-> ( ( S ` j ) + -u T ) ) = ( i e. ( 0 ... M ) |-> ( ( S ` i ) + -u T ) )
264	21	adantr 465	. . . . . 6 |- ( ( ph /\ 0 < -u T ) -> F : RR --> CC )
265	21	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F : RR --> CC )
266		ioossre 11598	. . . . . . . . . . 11 |- ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) C_ RR
267	266	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) C_ RR )
268	265, 267	feqresmpt 5928	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) = ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
269	173, 180	oveq12d 6313	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) = ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) )
270	161, 164, 165	iooshift 31449	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) = { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } )
271	269, 270	eqtrd 2508	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) = { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } )
272		mpteq1 4533	. . . . . . . . . 10 |- ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) = { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) = ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( F ` x ) ) )
273	271, 272	syl 16	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) = ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( F ` x ) ) )
274		simpll 753	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ph )
275	158	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> i e. ( 0..^ M ) )
276	270	eleq2d 2537	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) <-> x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) )
277	276	biimpar 485	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) )
278		elioore 11571	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) -> x e. RR )
279	278	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x e. RR )
280	8	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> T e. RR )
281	279, 280	resubcld 9999	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) e. RR )
282	281	3adant2 1015	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) e. RR )
283	70, 161	sseldi 3507	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. CC )
284	73	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> T e. CC )
285	283, 284	pncand 9943	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) + T ) - T ) = ( Q ` i ) )
286	285	eqcomd 2475	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( ( ( Q ` i ) + T ) - T ) )
287	286	3adant3 1016	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` i ) = ( ( ( Q ` i ) + T ) - T ) )
288	170	rexrd 9655	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + T ) e. RR* )
289	288	3adant3 1016	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) e. RR* )
290	179	rexrd 9655	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR* )
291	290	3adant3 1016	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR* )
292		simp3 998	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) )
293		ioogtlb 31415	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( Q ` i ) + T ) e. RR* /\ ( ( Q ` ( i + 1 ) ) + T ) e. RR* /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) < x )
294	289, 291, 292, 293	syl3anc 1228	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) < x )
295	170	3adant3 1016	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) e. RR )
296	279	3adant2 1015	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x e. RR )
297	280	3adant2 1015	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> T e. RR )
298	295, 296, 297	ltsub1d 10173	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( ( Q ` i ) + T ) < x <-> ( ( ( Q ` i ) + T ) - T ) < ( x - T ) ) )
299	294, 298	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( ( Q ` i ) + T ) - T ) < ( x - T ) )
300	287, 299	eqbrtrd 4473	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` i ) < ( x - T ) )
301		iooltub 31435	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( Q ` i ) + T ) e. RR* /\ ( ( Q ` ( i + 1 ) ) + T ) e. RR* /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x < ( ( Q ` ( i + 1 ) ) + T ) )
302	289, 291, 292, 301	syl3anc 1228	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x < ( ( Q ` ( i + 1 ) ) + T ) )
303	179	3adant3 1016	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR )
304	296, 303, 297	ltsub1d 10173	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x < ( ( Q ` ( i + 1 ) ) + T ) <-> ( x - T ) < ( ( ( Q ` ( i + 1 ) ) + T ) - T ) ) )
305	302, 304	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) < ( ( ( Q ` ( i + 1 ) ) + T ) - T ) )
306	70, 164	sseldi 3507	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
307	306, 284	pncand 9943	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` ( i + 1 ) ) + T ) - T ) = ( Q ` ( i + 1 ) ) )
308	307	3adant3 1016	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( ( Q ` ( i + 1 ) ) + T ) - T ) = ( Q ` ( i + 1 ) ) )
309	305, 308	breqtrd 4477	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) < ( Q ` ( i + 1 ) ) )
310	282, 300, 309	3jca 1176	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( x - T ) e. RR /\ ( Q ` i ) < ( x - T ) /\ ( x - T ) < ( Q ` ( i + 1 ) ) ) )
311	161	rexrd 9655	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
312	311	3adant3 1016	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` i ) e. RR* )
313	164	rexrd 9655	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
314	313	3adant3 1016	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
315		elioo2 11582	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) ) ) )
316	312, 314, 315	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( ( x - T ) e. RR /\ ( Q ` i ) < ( x - T ) /\ ( x - T ) < ( Q ` ( i + 1 ) ) ) ) )
317	310, 316	mpbird 232	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
318	274, 275, 277, 317	syl3anc 1228	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
319		fvres 5886	. . . . . . . . . . . 12 |- ( ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) = ( F ` ( x - T ) ) )
320	318, 319	syl 16	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) = ( F ` ( x - T ) ) )
321	274, 277, 281	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( x - T ) e. RR )
322	1	3ad2ant1 1017	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> A e. RR )
323	75	eqcomd 2475	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A = ( ( A + T ) - T ) )
324	323	3ad2ant1 1017	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> A = ( ( A + T ) - T ) )
325	71	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( A + T ) e. RR )
326	1	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> A e. RR* )
327	326	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A e. RR* )
328	3	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> B e. RR* )
329	328	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ i e. ( 0..^ M ) ) -> B e. RR* )
330	5, 6, 12	fourierdlem15 31745	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
331	330	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
332	161, 164, 168	ltled 9744	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) <_ ( Q ` ( i + 1 ) ) )
333		lbicc2 11648	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( Q ` i ) <_ ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
334	311, 313, 332, 333	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
335	327, 329, 331, 158, 334	fourierdlem1 31731	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. ( A [,] B ) )
336		iccgelb 11593	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A e. RR* /\ B e. RR* /\ ( Q ` i ) e. ( A [,] B ) ) -> A <_ ( Q ` i ) )
337	327, 329, 335, 336	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A <_ ( Q ` i ) )
338	1	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A e. RR )
339	338, 161, 165	leadd1d 10158	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( A <_ ( Q ` i ) <-> ( A + T ) <_ ( ( Q ` i ) + T ) ) )
340	337, 339	mpbid 210	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( A + T ) <_ ( ( Q ` i ) + T ) )
341	340	3adant3 1016	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( A + T ) <_ ( ( Q ` i ) + T ) )
342	325, 295, 296, 341, 294	lelttrd 9751	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( A + T ) < x )
343	325, 296, 297	ltsub1d 10173	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( A + T ) < x <-> ( ( A + T ) - T ) < ( x - T ) ) )
344	342, 343	mpbid 210	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( A + T ) - T ) < ( x - T ) )
345	324, 344	eqbrtrd 4473	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> A < ( x - T ) )
346	322, 282, 345	ltled 9744	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> A <_ ( x - T ) )
347	3	3ad2ant1 1017	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> B e. RR )
348	164	3adant3 1016	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
349	331, 163	ffvelrnd 6033	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( A [,] B ) )
350		iccleub 11592	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. RR* /\ B e. RR* /\ ( Q ` ( i + 1 ) ) e. ( A [,] B ) ) -> ( Q ` ( i + 1 ) ) <_ B )
351	327, 329, 349, 350	syl3anc 1228	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) <_ B )
352	351	3adant3 1016	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` ( i + 1 ) ) <_ B )
353	282, 348, 347, 309, 352	ltletrd 9753	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) < B )
354	282, 347, 353	ltled 9744	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) <_ B )
355	282, 346, 354	3jca 1176	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( x - T ) e. RR /\ A <_ ( x - T ) /\ ( x - T ) <_ B ) )
356		elicc2 11601	. . . . . . . . . . . . . . . 16 |- ( ( A e. RR /\ B e. RR ) -> ( ( x - T ) e. ( A [,] B ) <-> ( ( x - T ) e. RR /\ A <_ ( x - T ) /\ ( x - T ) <_ B ) ) )
357	322, 347, 356	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( x - T ) e. ( A [,] B ) <-> ( ( x - T ) e. RR /\ A <_ ( x - T ) /\ ( x - T ) <_ B ) ) )
358	355, 357	mpbird 232	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) e. ( A [,] B ) )
359	274, 275, 277, 358	syl3anc 1228	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( x - T ) e. ( A [,] B ) )
360	274, 359	jca 532	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( ph /\ ( x - T ) e. ( A [,] B ) ) )
361		eleq1 2539	. . . . . . . . . . . . . . 15 |- ( y = ( x - T ) -> ( y e. ( A [,] B ) <-> ( x - T ) e. ( A [,] B ) ) )
362	361	anbi2d 703	. . . . . . . . . . . . . 14 |- ( y = ( x - T ) -> ( ( ph /\ y e. ( A [,] B ) ) <-> ( ph /\ ( x - T ) e. ( A [,] B ) ) ) )
363		oveq1 6302	. . . . . . . . . . . . . . . 16 |- ( y = ( x - T ) -> ( y + T ) = ( ( x - T ) + T ) )
364	363	fveq2d 5876	. . . . . . . . . . . . . . 15 |- ( y = ( x - T ) -> ( F ` ( y + T ) ) = ( F ` ( ( x - T ) + T ) ) )
365		fveq2 5872	. . . . . . . . . . . . . . 15 |- ( y = ( x - T ) -> ( F ` y ) = ( F ` ( x - T ) ) )
366	364, 365	eqeq12d 2489	. . . . . . . . . . . . . 14 |- ( y = ( x - T ) -> ( ( F ` ( y + T ) ) = ( F ` y ) <-> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) ) )
367	362, 366	imbi12d 320	. . . . . . . . . . . . 13 |- ( y = ( x - T ) -> ( ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) ) <-> ( ( ph /\ ( x - T ) e. ( A [,] B ) ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) ) ) )
368	247	a1i 11	. . . . . . . . . . . . 13 |- ( y e. RR -> ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) ) )
369	367, 368	vtoclga 3182	. . . . . . . . . . . 12 |- ( ( x - T ) e. RR -> ( ( ph /\ ( x - T ) e. ( A [,] B ) ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) ) )
370	321, 360, 369	sylc 60	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) )
371	277, 278	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> x e. RR )
372	70	sseli 3505	. . . . . . . . . . . . . . 15 |- ( x e. RR -> x e. CC )
373	372	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> x e. CC )
374	73	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> T e. CC )
375	373, 374	npcand 9946	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> ( ( x - T ) + T ) = x )
376	375	fveq2d 5876	. . . . . . . . . . . 12 |- ( ( ph /\ x e. RR ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` x ) )
377	274, 371, 376	syl2anc 661	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` x ) )
378	320, 370, 377	3eqtr2rd 2515	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( F ` x ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) )
379	378	mpteq2dva 4539	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( F ` x ) ) = ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) )
380	268, 273, 379	3eqtrd 2512	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) = ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) )
381		ioosscn 31414	. . . . . . . . . . 11 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
382	381	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
383		nfcv 2629	. . . . . . . . . . 11 |- F/_ w CC
384		nfcv 2629	. . . . . . . . . . 11 |- F/_ x CC
385		nfv 1683	. . . . . . . . . . 11 |- F/ x E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T )
386		nfv 1683	. . . . . . . . . . 11 |- F/ w E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T )
387		eqeq1 2471	. . . . . . . . . . . . 13 |- ( w = x -> ( w = ( z + T ) <-> x = ( z + T ) ) )
388	387	rexbidv 2978	. . . . . . . . . . . 12 |- ( w = x -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) <-> E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) )
389		nfv 1683	. . . . . . . . . . . . . 14 |- F/ y x = ( z + T )
390		nfv 1683	. . . . . . . . . . . . . 14 |- F/ z x = ( y + T )
391		oveq1 6302	. . . . . . . . . . . . . . 15 |- ( z = y -> ( z + T ) = ( y + T ) )
392	391	eqeq2d 2481	. . . . . . . . . . . . . 14 |- ( z = y -> ( x = ( z + T ) <-> x = ( y + T ) ) )
393	389, 390, 392	cbvrex 3090	. . . . . . . . . . . . 13 |- ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) <-> E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) )
394	393	a1i 11	. . . . . . . . . . . 12 |- ( w = x -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) <-> E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) ) )
395	388, 394	bitrd 253	. . . . . . . . . . 11 |- ( w = x -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) <-> E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) ) )
396	383, 384, 385, 386, 395	cbvrab 3116	. . . . . . . . . 10 |- { 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 ) }
397		eqid 2467	. . . . . . . . . 10 |- ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) = ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) )
398	382, 284, 396, 23, 397	cncfshift 31535	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) e. ( { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } -cn-> CC ) )
399	397	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) = ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) )
400	271	eqcomd 2475	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } = ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
401	400	oveq1d 6310	. . . . . . . . . 10 |- ( ( 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 ) )
402	399, 401	eleq12d 2549	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) e. ( { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } -cn-> CC ) <-> ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) e. ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -cn-> CC ) ) )
403	398, 402	mpbid 210	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) e. ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -cn-> CC ) )
404	380, 403	eqeltrd 2555	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )