Theorem fourierdlem97 31827

Description: F is continuous on the intervals induced by the moved partition V (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem97.f	|- ( ph -> F : RR --> RR )
fourierdlem97.g	|- G = ( RR _D F )
fourierdlem97.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 ) ) ) } )
fourierdlem97.a	|- ( ph -> B e. RR )
fourierdlem97.b	|- ( ph -> A e. RR )
fourierdlem97.t	|- T = ( B - A )
fourierdlem97.m	|- ( ph -> M e. NN )
fourierdlem97.q	|- ( ph -> Q e. ( P ` M ) )
fourierdlem97.fper	|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem97.qcn	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem97.c	|- ( ph -> C e. RR )
fourierdlem97.d	|- ( ph -> D e. ( C (,) +oo ) )
fourierdlem97.j	|- ( ph -> J e. ( 0..^ ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) )
fourierdlem97.v	|- V = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
fourierdlem97.h	|- H = ( s e. RR |-> if ( s e. dom G , ( G ` s ) , 0 ) )

Assertion

Ref	Expression
fourierdlem97	|- ( ph -> ( G |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) e. ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) -cn-> CC ) )

Distinct variable groups:   A, i, x   A, m, p, i   B, i, x   B, m, p   y, C, g   C, i, x, y   C, m, p, y   y, D, g   D, i, x   D, m, p   F, s, x   y, F   i, G, s   y, G   i, H, s, x   h, J, k, i, x   J, s   h, M, i, x   m, M, p   M, s   Q, h, k, g, y   Q, i, x   Q, m, p, k   Q, s   T, h, k, g, y   T, i, x   T, m, p   T, s   h, V, k, g   i, V, x   V, p   V, s   ph, h, y, g   ph, i, s, x

Allowed substitution hints:   ph( k, m, p)   A( y, g, h, k, s)   B( y, g, h, k, s)   C( h, k, s)   D( h, k, s)   P( x, y, g, h, i, k, m, s, p)   F( g, h, i, k, m, p)   G( x, g, h, k, m, p)   H( y, g, h, k, m, p)   J( y, g, m, p)   M( y, g, k)   V( y, m)

Proof of Theorem fourierdlem97

Dummy variables f l t u w z v e j are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem97.f	. . . . . . 7 |- ( ph -> F : RR --> RR )
2		ssid 3528	. . . . . . 7 |- RR C_ RR
3		dvfre 22222	. . . . . . 7 |- ( ( F : RR --> RR /\ RR C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
4	1, 2, 3	sylancl 662	. . . . . 6 |- ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
5		fourierdlem97.g	. . . . . . . 8 |- G = ( RR _D F )
6	5	feq1i 5729	. . . . . . 7 |- ( G : dom ( RR _D F ) --> RR <-> ( RR _D F ) : dom ( RR _D F ) --> RR )
7	6	a1i 11	. . . . . 6 |- ( ph -> ( G : dom ( RR _D F ) --> RR <-> ( RR _D F ) : dom ( RR _D F ) --> RR ) )
8	4, 7	mpbird 232	. . . . 5 |- ( ph -> G : dom ( RR _D F ) --> RR )
9	5	dmeqi 5210	. . . . . . 7 |- dom G = dom ( RR _D F )
10	9	a1i 11	. . . . . 6 |- ( ph -> dom G = dom ( RR _D F ) )
11	10	feq2d 5724	. . . . 5 |- ( ph -> ( G : dom G --> RR <-> G : dom ( RR _D F ) --> RR ) )
12	8, 11	mpbird 232	. . . 4 |- ( ph -> G : dom G --> RR )
13		fourierdlem97.t	. . . . . . 7 |- T = ( B - A )
14		fourierdlem97.p	. . . . . . 7 |- 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 ) ) ) } )
15		fourierdlem97.m	. . . . . . 7 |- ( ph -> M e. NN )
16		fourierdlem97.q	. . . . . . 7 |- ( ph -> Q e. ( P ` M ) )
17		fourierdlem97.c	. . . . . . 7 |- ( ph -> C e. RR )
18		fourierdlem97.d	. . . . . . . 8 |- ( ph -> D e. ( C (,) +oo ) )
19		elioore 11571	. . . . . . . 8 |- ( D e. ( C (,) +oo ) -> D e. RR )
20	18, 19	syl 16	. . . . . . 7 |- ( ph -> D e. RR )
21	17	rexrd 9655	. . . . . . . 8 |- ( ph -> C e. RR* )
22		pnfxr 11333	. . . . . . . . 9 |- +oo e. RR*
23	22	a1i 11	. . . . . . . 8 |- ( ph -> +oo e. RR* )
24		ioogtlb 31415	. . . . . . . 8 |- ( ( C e. RR* /\ +oo e. RR* /\ D e. ( C (,) +oo ) ) -> C < D )
25	21, 23, 18, 24	syl3anc 1228	. . . . . . 7 |- ( ph -> C < D )
26		oveq1 6302	. . . . . . . . . . 11 |- ( y = x -> ( y + ( h x. T ) ) = ( x + ( h x. T ) ) )
27	26	eleq1d 2536	. . . . . . . . . 10 |- ( y = x -> ( ( y + ( h x. T ) ) e. ran Q <-> ( x + ( h x. T ) ) e. ran Q ) )
28	27	rexbidv 2978	. . . . . . . . 9 |- ( y = x -> ( E. h e. ZZ ( y + ( h x. T ) ) e. ran Q <-> E. h e. ZZ ( x + ( h x. T ) ) e. ran Q ) )
29	28	cbvrabv 3117	. . . . . . . 8 |- { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } = { x e. ( C [,] D ) | E. h e. ZZ ( x + ( h x. T ) ) e. ran Q }
30	29	uneq2i 3660	. . . . . . 7 |- ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) = ( { C , D } u. { x e. ( C [,] D ) | E. h e. ZZ ( x + ( h x. T ) ) e. ran Q } )
31		oveq1 6302	. . . . . . . . . . . . . . . 16 |- ( k = l -> ( k x. T ) = ( l x. T ) )
32	31	oveq2d 6311	. . . . . . . . . . . . . . 15 |- ( k = l -> ( y + ( k x. T ) ) = ( y + ( l x. T ) ) )
33	32	eleq1d 2536	. . . . . . . . . . . . . 14 |- ( k = l -> ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( l x. T ) ) e. ran Q ) )
34	33	cbvrexv 3094	. . . . . . . . . . . . 13 |- ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. l e. ZZ ( y + ( l x. T ) ) e. ran Q )
35	34	a1i 11	. . . . . . . . . . . 12 |- ( y e. ( C [,] D ) -> ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. l e. ZZ ( y + ( l x. T ) ) e. ran Q ) )
36	35	rabbiia 3107	. . . . . . . . . . 11 |- { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q }
37	36	uneq2i 3660	. . . . . . . . . 10 |- ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } )
38		oveq1 6302	. . . . . . . . . . . . . . . 16 |- ( l = h -> ( l x. T ) = ( h x. T ) )
39	38	oveq2d 6311	. . . . . . . . . . . . . . 15 |- ( l = h -> ( y + ( l x. T ) ) = ( y + ( h x. T ) ) )
40	39	eleq1d 2536	. . . . . . . . . . . . . 14 |- ( l = h -> ( ( y + ( l x. T ) ) e. ran Q <-> ( y + ( h x. T ) ) e. ran Q ) )
41	40	cbvrexv 3094	. . . . . . . . . . . . 13 |- ( E. l e. ZZ ( y + ( l x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q )
42	41	a1i 11	. . . . . . . . . . . 12 |- ( y e. ( C [,] D ) -> ( E. l e. ZZ ( y + ( l x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q ) )
43	42	rabbiia 3107	. . . . . . . . . . 11 |- { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q }
44	43	uneq2i 3660	. . . . . . . . . 10 |- ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } )
45	37, 44	eqtri 2496	. . . . . . . . 9 |- ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } )
46	45	fveq2i 5875	. . . . . . . 8 |- ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) = ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) )
47	46	oveq1i 6305	. . . . . . 7 |- ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) - 1 )
48		fourierdlem97.v	. . . . . . 7 |- V = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
49		fourierdlem97.j	. . . . . . 7 |- ( ph -> J e. ( 0..^ ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) )
50		oveq1 6302	. . . . . . . . . . 11 |- ( k = h -> ( k x. T ) = ( h x. T ) )
51	50	oveq2d 6311	. . . . . . . . . 10 |- ( k = h -> ( ( Q ` 0 ) + ( k x. T ) ) = ( ( Q ` 0 ) + ( h x. T ) ) )
52	51	breq1d 4463	. . . . . . . . 9 |- ( k = h -> ( ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) <-> ( ( Q ` 0 ) + ( h x. T ) ) <_ ( V ` J ) ) )
53	52	cbvrabv 3117	. . . . . . . 8 |- { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } = { h e. ZZ | ( ( Q ` 0 ) + ( h x. T ) ) <_ ( V ` J ) }
54	53	supeq1i 7919	. . . . . . 7 |- sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) = sup ( { h e. ZZ | ( ( Q ` 0 ) + ( h x. T ) ) <_ ( V ` J ) } , RR , < )
55		fveq2 5872	. . . . . . . . . . 11 |- ( j = e -> ( Q ` j ) = ( Q ` e ) )
56	55	oveq1d 6310	. . . . . . . . . 10 |- ( j = e -> ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) = ( ( Q ` e ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) )
57	56	breq1d 4463	. . . . . . . . 9 |- ( j = e -> ( ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) <-> ( ( Q ` e ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) ) )
58	57	cbvrabv 3117	. . . . . . . 8 |- { j e. ( 0..^ M ) | ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) } = { e e. ( 0..^ M ) | ( ( Q ` e ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) }
59	58	supeq1i 7919	. . . . . . 7 |- sup ( { j e. ( 0..^ M ) | ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) } , RR , < ) = sup ( { e e. ( 0..^ M ) | ( ( Q ` e ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) } , RR , < )
60	13, 14, 15, 16, 17, 20, 25, 30, 47, 48, 49, 54, 59	fourierdlem64 31794	. . . . . 6 |- ( ph -> ( ( sup ( { j e. ( 0..^ M ) | ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) } , RR , < ) e. ( 0..^ M ) /\ sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) e. ZZ ) /\ E. i e. ( 0..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) )
61	60	simprd 463	. . . . 5 |- ( ph -> E. i e. ( 0..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
62		simpl1 999	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ph )
63		simpl2l 1049	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> i e. ( 0..^ M ) )
64		fourierdlem97.qcn	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
65		cncff 21265	. . . . . . . . . . . . . . . . . . . 20 |- ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
66	64, 65	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
67		ffun 5739	. . . . . . . . . . . . . . . . . . . . . 22 |- ( G : dom ( RR _D F ) --> RR -> Fun G )
68	8, 67	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> Fun G )
69	68	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Fun G )
70		ffvresb 6063	. . . . . . . . . . . . . . . . . . . 20 |- ( Fun G -> ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC <-> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( s e. dom G /\ ( G ` s ) e. CC ) ) )
71	69, 70	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC <-> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( s e. dom G /\ ( G ` s ) e. CC ) ) )
72	66, 71	mpbid 210	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( s e. dom G /\ ( G ` s ) e. CC ) )
73	72	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( s e. dom G /\ ( G ` s ) e. CC ) )
74		simpr 461	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
75		rspa 2834	. . . . . . . . . . . . . . . . 17 |- ( ( A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( s e. dom G /\ ( G ` s ) e. CC ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( s e. dom G /\ ( G ` s ) e. CC ) )
76	73, 74, 75	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( s e. dom G /\ ( G ` s ) e. CC ) )
77	76	simpld 459	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. dom G )
78	77	ralrimiva 2881	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) s e. dom G )
79		dfss3 3499	. . . . . . . . . . . . . 14 |- ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom G <-> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) s e. dom G )
80	78, 79	sylibr 212	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom G )
81	80	idi 2	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom G )
82	62, 63, 81	syl2anc 661	. . . . . . . . . . 11 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom G )
83		simpl2 1000	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( i e. ( 0..^ M ) /\ l e. ZZ ) )
84	62, 83	jca 532	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) )
85		simpr 461	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) )
86		simpl3 1001	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
87		simpr 461	. . . . . . . . . . . . . 14 |- ( ( t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
88		simpl 457	. . . . . . . . . . . . . 14 |- ( ( t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) )
89	87, 88	sseldd 3510	. . . . . . . . . . . . 13 |- ( ( t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
90	85, 86, 89	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
91	14	fourierdlem2 31732	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 ) ) ) ) ) )
92	15, 91	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) ) ) ) ) )
93	16, 92	mpbid 210	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
94	93	simpld 459	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
95		elmapi 7452	. . . . . . . . . . . . . . . . . . 19 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
96	94, 95	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> Q : ( 0 ... M ) --> RR )
97	96	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
98		elfzofz 11823	. . . . . . . . . . . . . . . . . 18 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
99	98	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
100	97, 99	ffvelrnd 6033	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
101	100	rexrd 9655	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
102	101	adantrr 716	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) -> ( Q ` i ) e. RR* )
103	102	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` i ) e. RR* )
104		fzofzp1 11889	. . . . . . . . . . . . . . . . . 18 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
105	104	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
106	97, 105	ffvelrnd 6033	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
107	106	adantrr 716	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) -> ( Q ` ( i + 1 ) ) e. RR )
108	107	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
109	108	rexrd 9655	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
110		elioore 11571	. . . . . . . . . . . . . . 15 |- ( t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) -> t e. RR )
111	110	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> t e. RR )
112		zre 10880	. . . . . . . . . . . . . . . . 17 |- ( l e. ZZ -> l e. RR )
113	112	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( i e. ( 0..^ M ) /\ l e. ZZ ) -> l e. RR )
114	113	ad2antlr 726	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> l e. RR )
115	13	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> T = ( B - A ) )
116		fourierdlem97.a	. . . . . . . . . . . . . . . . . 18 |- ( ph -> B e. RR )
117		fourierdlem97.b	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A e. RR )
118	116, 117	resubcld 9999	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( B - A ) e. RR )
119	115, 118	eqeltrd 2555	. . . . . . . . . . . . . . . 16 |- ( ph -> T e. RR )
120	119	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> T e. RR )
121	114, 120	remulcld 9636	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( l x. T ) e. RR )
122	111, 121	resubcld 9999	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( t - ( l x. T ) ) e. RR )
123	100	adantrr 716	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) -> ( Q ` i ) e. RR )
124	112	ad2antll 728	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) -> l e. RR )
125	119	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) -> T e. RR )
126	124, 125	remulcld 9636	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) -> ( l x. T ) e. RR )
127	123, 126	readdcld 9635	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) -> ( ( Q ` i ) + ( l x. T ) ) e. RR )
128	127	rexrd 9655	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) -> ( ( Q ` i ) + ( l x. T ) ) e. RR* )
129	128	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( Q ` i ) + ( l x. T ) ) e. RR* )
130	107, 126	readdcld 9635	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) -> ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR )
131	130	rexrd 9655	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) -> ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR* )
132	131	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR* )
133		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
134		ioogtlb 31415	. . . . . . . . . . . . . . 15 |- ( ( ( ( Q ` i ) + ( l x. T ) ) e. RR* /\ ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR* /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( Q ` i ) + ( l x. T ) ) < t )
135	129, 132, 133, 134	syl3anc 1228	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( Q ` i ) + ( l x. T ) ) < t )
136	123	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` i ) e. RR )
137	136, 121, 111	ltaddsubd 10164	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( ( Q ` i ) + ( l x. T ) ) < t <-> ( Q ` i ) < ( t - ( l x. T ) ) ) )
138	135, 137	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` i ) < ( t - ( l x. T ) ) )
139		iooltub 31435	. . . . . . . . . . . . . . 15 |- ( ( ( ( Q ` i ) + ( l x. T ) ) e. RR* /\ ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR* /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> t < ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) )
140	129, 132, 133, 139	syl3anc 1228	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> t < ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) )
141	111, 121, 108	ltsubaddd 10160	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( t - ( l x. T ) ) < ( Q ` ( i + 1 ) ) <-> t < ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
142	140, 141	mpbird 232	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( t - ( l x. T ) ) < ( Q ` ( i + 1 ) ) )
143	103, 109, 122, 138, 142	eliood 31418	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( t - ( l x. T ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
144	84, 90, 143	syl2anc 661	. . . . . . . . . . 11 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( t - ( l x. T ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
145	82, 144	sseldd 3510	. . . . . . . . . 10 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( t - ( l x. T ) ) e. dom G )
146		simpl 457	. . . . . . . . . . . . 13 |- ( ( ( ph /\ l e. ZZ ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ph /\ l e. ZZ ) )
147		ioossre 11598	. . . . . . . . . . . . . . 15 |- ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ RR
148	147	sseli 3505	. . . . . . . . . . . . . 14 |- ( t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) -> t e. RR )
149	148	adantl 466	. . . . . . . . . . . . 13 |- ( ( ( ph /\ l e. ZZ ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> t e. RR )
150		ax-resscn 9561	. . . . . . . . . . . . . . . . . . . 20 |- RR C_ CC
151	150	sseli 3505	. . . . . . . . . . . . . . . . . . 19 |- ( t e. RR -> t e. CC )
152	151	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> t e. CC )
153	150, 112	sseldi 3507	. . . . . . . . . . . . . . . . . . . 20 |- ( l e. ZZ -> l e. CC )
154	153	ad2antlr 726	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> l e. CC )
155	119	recnd 9634	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> T e. CC )
156	155	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> T e. CC )
157	154, 156	mulcld 9628	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> ( l x. T ) e. CC )
158	152, 157	npcand 9946	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> ( ( t - ( l x. T ) ) + ( l x. T ) ) = t )
159	158	eqcomd 2475	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> t = ( ( t - ( l x. T ) ) + ( l x. T ) ) )
160	159	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) /\ ( t - ( l x. T ) ) e. dom G ) -> t = ( ( t - ( l x. T ) ) + ( l x. T ) ) )
161		ovex 6320	. . . . . . . . . . . . . . . . . 18 |- ( t - ( l x. T ) ) e. _V
162		eleq1 2539	. . . . . . . . . . . . . . . . . . . . 21 |- ( s = ( t - ( l x. T ) ) -> ( s e. dom G <-> ( t - ( l x. T ) ) e. dom G ) )
163	162	anbi2d 703	. . . . . . . . . . . . . . . . . . . 20 |- ( s = ( t - ( l x. T ) ) -> ( ( ( ph /\ l e. ZZ ) /\ s e. dom G ) <-> ( ( ph /\ l e. ZZ ) /\ ( t - ( l x. T ) ) e. dom G ) ) )
164		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . 22 |- ( s = ( t - ( l x. T ) ) -> ( s + ( l x. T ) ) = ( ( t - ( l x. T ) ) + ( l x. T ) ) )
165	164	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . 21 |- ( s = ( t - ( l x. T ) ) -> ( ( s + ( l x. T ) ) e. dom G <-> ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G ) )
166	164	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . 22 |- ( s = ( t - ( l x. T ) ) -> ( G ` ( s + ( l x. T ) ) ) = ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) )
167		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . 22 |- ( s = ( t - ( l x. T ) ) -> ( G ` s ) = ( G ` ( t - ( l x. T ) ) ) )
168	166, 167	eqeq12d 2489	. . . . . . . . . . . . . . . . . . . . 21 |- ( s = ( t - ( l x. T ) ) -> ( ( G ` ( s + ( l x. T ) ) ) = ( G ` s ) <-> ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) = ( G ` ( t - ( l x. T ) ) ) ) )
169	165, 168	anbi12d 710	. . . . . . . . . . . . . . . . . . . 20 |- ( s = ( t - ( l x. T ) ) -> ( ( ( s + ( l x. T ) ) e. dom G /\ ( G ` ( s + ( l x. T ) ) ) = ( G ` s ) ) <-> ( ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G /\ ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) = ( G ` ( t - ( l x. T ) ) ) ) ) )
170	163, 169	imbi12d 320	. . . . . . . . . . . . . . . . . . 19 |- ( s = ( t - ( l x. T ) ) -> ( ( ( ( ph /\ l e. ZZ ) /\ s e. dom G ) -> ( ( s + ( l x. T ) ) e. dom G /\ ( G ` ( s + ( l x. T ) ) ) = ( G ` s ) ) ) <-> ( ( ( ph /\ l e. ZZ ) /\ ( t - ( l x. T ) ) e. dom G ) -> ( ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G /\ ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) = ( G ` ( t - ( l x. T ) ) ) ) ) ) )
171	150	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> RR C_ CC )
172	1, 171	fssd 5746	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> F : RR --> CC )
173	172	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ l e. ZZ ) -> F : RR --> CC )
174	112	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ l e. ZZ ) -> l e. RR )
175	119	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ l e. ZZ ) -> T e. RR )
176	174, 175	remulcld 9636	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ l e. ZZ ) -> ( l x. T ) e. RR )
177	173	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> F : RR --> CC )
178	175	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> T e. RR )
179		simplr 754	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> l e. ZZ )
180		simpr 461	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> s e. RR )
181		fourierdlem97.fper	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
182	181	adant423 31330	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
183	177, 178, 179, 180, 182	fperiodmul 31404	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> ( F ` ( s + ( l x. T ) ) ) = ( F ` s ) )
184	173, 176, 183, 5	fperdvper 31571	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ l e. ZZ ) /\ s e. dom G ) -> ( ( s + ( l x. T ) ) e. dom G /\ ( G ` ( s + ( l x. T ) ) ) = ( G ` s ) ) )
185	170, 184	vtoclg 3176	. . . . . . . . . . . . . . . . . 18 |- ( ( t - ( l x. T ) ) e. _V -> ( ( ( ph /\ l e. ZZ ) /\ ( t - ( l x. T ) ) e. dom G ) -> ( ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G /\ ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) = ( G ` ( t - ( l x. T ) ) ) ) ) )
186	161, 185	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ l e. ZZ ) /\ ( t - ( l x. T ) ) e. dom G ) -> ( ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G /\ ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) = ( G ` ( t - ( l x. T ) ) ) ) )
187	186	simpld 459	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ l e. ZZ ) /\ ( t - ( l x. T ) ) e. dom G ) -> ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G )
188	187	adantlr 714	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) /\ ( t - ( l x. T ) ) e. dom G ) -> ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G )
189	160, 188	eqeltrd 2555	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) /\ ( t - ( l x. T ) ) e. dom G ) -> t e. dom G )
190	189	ex 434	. . . . . . . . . . . . 13 |- ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> ( ( t - ( l x. T ) ) e. dom G -> t e. dom G ) )
191	146, 149, 190	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( ph /\ l e. ZZ ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( t - ( l x. T ) ) e. dom G -> t e. dom G ) )
192	191	adantlrl 719	. . . . . . . . . . 11 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( t - ( l x. T ) ) e. dom G -> t e. dom G ) )
193	192	3adantl3 1154	. . . . . . . . . 10 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( t - ( l x. T ) ) e. dom G -> t e. dom G ) )
194	145, 193	mpd 15	. . . . . . . . 9 |- ( ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> t e. dom G )
195	194	ralrimiva 2881	. . . . . . . 8 |- ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> A. t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) t e. dom G )
196		dfss3 3499	. . . . . . . 8 |- ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G <-> A. t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) t e. dom G )
197	195, 196	sylibr 212	. . . . . . 7 |- ( ( ph /\ ( i e. ( 0..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G )
198	197	3exp 1195	. . . . . 6 |- ( ph -> ( ( i e. ( 0..^ M ) /\ l e. ZZ ) -> ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G ) ) )
199	198	rexlimdvv 2965	. . . . 5 |- ( ph -> ( E. i e. ( 0..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G ) )
200	61, 199	mpd 15	. . . 4 |- ( ph -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G )
201	12, 200	feqresmpt 5928	. . 3 |- ( ph -> ( G |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) = ( s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) |-> ( G ` s ) ) )
202	147	a1i 11	. . . . . . 7 |- ( ph -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ RR )
203	202	sselda 3509	. . . . . 6 |- ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> s e. RR )
204		iftrue 3951	. . . . . . . . . . 11 |- ( s e. dom G -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` s ) )
205	204	adantl 466	. . . . . . . . . 10 |- ( ( ph /\ s e. dom G ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` s ) )
206	8	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ s e. dom G ) -> G : dom ( RR _D F ) --> RR )
207		id 22	. . . . . . . . . . . . 13 |- ( s e. dom G -> s e. dom G )
208	9	a1i 11	. . . . . . . . . . . . 13 |- ( s e. dom G -> dom G = dom ( RR _D F ) )
209	207, 208	eleqtrd 2557	. . . . . . . . . . . 12 |- ( s e. dom G -> s e. dom ( RR _D F ) )
210	209	adantl 466	. . . . . . . . . . 11 |- ( ( ph /\ s e. dom G ) -> s e. dom ( RR _D F ) )
211	206, 210	ffvelrnd 6033	. . . . . . . . . 10 |- ( ( ph /\ s e. dom G ) -> ( G ` s ) e. RR )
212	205, 211	eqeltrd 2555	. . . . . . . . 9 |- ( ( ph /\ s e. dom G ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
213	212	adantlr 714	. . . . . . . 8 |- ( ( ( ph /\ s e. RR ) /\ s e. dom G ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
214		iffalse 3954	. . . . . . . . . 10 |- ( -. s e. dom G -> if ( s e. dom G , ( G ` s ) , 0 ) = 0 )
215		0re 9608	. . . . . . . . . . 11 |- 0 e. RR
216	215	a1i 11	. . . . . . . . . 10 |- ( -. s e. dom G -> 0 e. RR )
217	214, 216	eqeltrd 2555	. . . . . . . . 9 |- ( -. s e. dom G -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
218	217	adantl 466	. . . . . . . 8 |- ( ( ( ph /\ s e. RR ) /\ -. s e. dom G ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
219	213, 218	pm2.61dan 789	. . . . . . 7 |- ( ( ph /\ s e. RR ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
220	203, 219	syldan 470	. . . . . 6 |- ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
221		fourierdlem97.h	. . . . . . 7 |- H = ( s e. RR |-> if ( s e. dom G , ( G ` s ) , 0 ) )
222	221	fvmpt2 5964	. . . . . 6 |- ( ( s e. RR /\ if ( s e. dom G , ( G ` s ) , 0 ) e. RR ) -> ( H ` s ) = if ( s e. dom G , ( G ` s ) , 0 ) )
223	203, 220, 222	syl2anc 661	. . . . 5 |- ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( H ` s ) = if ( s e. dom G , ( G ` s ) , 0 ) )
224	200	sselda 3509	. . . . . 6 |- ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> s e. dom G )
225	224	iftrued 3953	. . . . 5 |- ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` s ) )
226		eqidd 2468	. . . . 5 |- ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( G ` s ) = ( G ` s ) )
227	223, 225, 226	3eqtrrd 2513	. . . 4 |- ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( G ` s ) = ( H ` s ) )
228	227	mpteq2dva 4539	. . 3 |- ( ph -> ( s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) |-> ( G ` s ) ) = ( s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) |-> ( H ` s ) ) )
229	219, 221	fmptd 6056	. . . . 5 |- ( ph -> H : RR --> RR )
230	229, 202	feqresmpt 5928	. . . 4 |- ( ph -> ( H |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) = ( s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) |-> ( H ` s ) ) )
231	230	eqcomd 2475	. . 3 |- ( ph -> ( s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) |-> ( H ` s ) ) = ( H |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) )
232	201, 228, 231	3eqtrd 2512	. 2 |- ( ph -> ( G |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) = ( H |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) )
233	229, 171	fssd 5746	. . 3 |- ( ph -> H : RR --> CC )
234	221	a1i 11	. . . . . 6 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> H = ( s e. RR |-> if ( s e. dom G , ( G ` s ) , 0 ) ) )
235		eleq1 2539	. . . . . . . . . 10 |- ( s = ( x + T ) -> ( s e. dom G <-> ( x + T ) e. dom G ) )
236		fveq2 5872	. . . . . . . . . 10 |- ( s = ( x + T ) -> ( G ` s ) = ( G ` ( x + T ) ) )
237		eqidd 2468	. . . . . . . . . 10 |- ( s = ( x + T ) -> 0 = 0 )
238	235, 236, 237	ifeq123d 31337	. . . . . . . . 9 |- ( s = ( x + T ) -> if ( s e. dom G , ( G ` s ) , 0 ) = if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) )
239	238	adantl 466	. . . . . . . 8 |- ( ( ( ph /\ x e. dom G ) /\ s = ( x + T ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) )
240	172, 119, 181, 5	fperdvper 31571	. . . . . . . . . . 11 |- ( ( ph /\ x e. dom G ) -> ( ( x + T ) e. dom G /\ ( G ` ( x + T ) ) = ( G ` x ) ) )
241	240	simpld 459	. . . . . . . . . 10 |- ( ( ph /\ x e. dom G ) -> ( x + T ) e. dom G )
242	241	iftrued 3953	. . . . . . . . 9 |- ( ( ph /\ x e. dom G ) -> if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) = ( G ` ( x + T ) ) )
243	242	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ x e. dom G ) /\ s = ( x + T ) ) -> if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) = ( G ` ( x + T ) ) )
244	239, 243	eqtrd 2508	. . . . . . 7 |- ( ( ( ph /\ x e. dom G ) /\ s = ( x + T ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` ( x + T ) ) )
245	244	adantllr 718	. . . . . 6 |- ( ( ( ( ph /\ x e. RR ) /\ x e. dom G ) /\ s = ( x + T ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` ( x + T ) ) )
246		simpr 461	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> x e. RR )
247	119	adantr 465	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> T e. RR )
248	246, 247	readdcld 9635	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> ( x + T ) e. RR )
249	248	adantr 465	. . . . . 6 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( x + T ) e. RR )
250	12	ad2antrr 725	. . . . . . 7 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> G : dom G --> RR )
251	241	adantlr 714	. . . . . . 7 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( x + T ) e. dom G )
252	250, 251	ffvelrnd 6033	. . . . . 6 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( G ` ( x + T ) ) e. RR )
253	234, 245, 249, 252	fvmptd 5962	. . . . 5 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( H ` ( x + T ) ) = ( G ` ( x + T ) ) )
254	240	simprd 463	. . . . . 6 |- ( ( ph /\ x e. dom G ) -> ( G ` ( x + T ) ) = ( G ` x ) )
255	254	adantlr 714	. . . . 5 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( G ` ( x + T ) ) = ( G ` x ) )
256		eleq1 2539	. . . . . . . . 9 |- ( s = x -> ( s e. dom G <-> x e. dom G ) )
257		fveq2 5872	. . . . . . . . 9 |- ( s = x -> ( G ` s ) = ( G ` x ) )
258		eqidd 2468	. . . . . . . . 9 |- ( s = x -> 0 = 0 )
259	256, 257, 258	ifeq123d 31337	. . . . . . . 8 |- ( s = x -> if ( s e. dom G , ( G ` s ) , 0 ) = if ( x e. dom G , ( G ` x ) , 0 ) )
260	259	adantl 466	. . . . . . 7 |- ( ( ( ( ph /\ x e. RR ) /\ x e. dom G ) /\ s = x ) -> if ( s e. dom G , ( G ` s ) , 0 ) = if ( x e. dom G , ( G ` x ) , 0 ) )
261	246	adantr 465	. . . . . . 7 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> x e. RR )
262		simpr 461	. . . . . . . . . 10 |- ( ( ph /\ x e. dom G ) -> x e. dom G )
263	262	iftrued 3953	. . . . . . . . 9 |- ( ( ph /\ x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) = ( G ` x ) )
264	12	ffvelrnda 6032	. . . . . . . . 9 |- ( ( ph /\ x e. dom G ) -> ( G ` x ) e. RR )
265	263, 264	eqeltrd 2555	. . . . . . . 8 |- ( ( ph /\ x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) e. RR )
266	265	adantlr 714	. . . . . . 7 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) e. RR )
267	234, 260, 261, 266	fvmptd 5962	. . . . . 6 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( H ` x ) = if ( x e. dom G , ( G ` x ) , 0 ) )
268		simpr 461	. . . . . . 7 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> x e. dom G )
269	268	iftrued 3953	. . . . . 6 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) = ( G ` x ) )
270		eqidd 2468	. . . . . 6 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( G ` x ) = ( G ` x ) )
271	267, 269, 270	3eqtrrd 2513	. . . . 5 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( G ` x ) = ( H ` x ) )
272	253, 255, 271	3eqtrd 2512	. . . 4 |- ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( H ` ( x + T ) ) = ( H ` x ) )
273	221	a1i 11	. . . . . 6 |- ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> H = ( s e. RR |-> if ( s e. dom G , ( G ` s ) , 0 ) ) )
274	238	adantl 466	. . . . . 6 |- ( ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) /\ s = ( x + T ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) )
275	248	adantr 465	. . . . . 6 |- ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> ( x + T ) e. RR )
276	150, 248	sseldi 3507	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> ( x + T ) e. CC )
277	150, 247	sseldi 3507	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> T e. CC )
278	276, 277	negsubd 9948	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> ( ( x + T ) + -u T ) = ( ( x + T ) - T ) )
279	150, 246	sseldi 3507	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> x e. CC )
280	279, 277	pncand 9943	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> ( ( x + T ) - T ) = x )
281	278, 280	eqtr2d 2509	. . . . . . . . . . . 12 |- ( ( ph /\ x e. RR ) -> x = ( ( x + T ) + -u T ) )
282	281	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> x = ( ( x + T ) + -u T ) )
283		simpr 461	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ( x + T ) e. dom G )
284		simpll 753	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ph )
285	284, 283	jca 532	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ( ph /\ ( x + T ) e. dom G ) )
286		eleq1 2539	. . . . . . . . . . . . . . . 16 |- ( y = ( x + T ) -> ( y e. dom G <-> ( x + T ) e. dom G ) )
287	286	anbi2d 703	. . . . . . . . . . . . . . 15 |- ( y = ( x + T ) -> ( ( ph /\ y e. dom G ) <-> ( ph /\ ( x + T ) e. dom G ) ) )
288		oveq1 6302	. . . . . . . . . . . . . . . . 17 |- ( y = ( x + T ) -> ( y + -u T ) = ( ( x + T ) + -u T ) )
289	288	eleq1d 2536	. . . . . . . . . . . . . . . 16 |- ( y = ( x + T ) -> ( ( y + -u T ) e. dom G <-> ( ( x + T ) + -u T ) e. dom G ) )
290	288	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( y = ( x + T ) -> ( G ` ( y + -u T ) ) = ( G ` ( ( x + T ) + -u T ) ) )
291		fveq2 5872	. . . . . . . . . . . . . . . . 17 |- ( y = ( x + T ) -> ( G ` y ) = ( G ` ( x + T ) ) )
292	290, 291	eqeq12d 2489	. . . . . . . . . . . . . . . 16 |- ( y = ( x + T ) -> ( ( G ` ( y + -u T ) ) = ( G ` y ) <-> ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) )
293	289, 292	anbi12d 710	. . . . . . . . . . . . . . 15 |- ( y = ( x + T ) -> ( ( ( y + -u T ) e. dom G /\ ( G ` ( y + -u T ) ) = ( G ` y ) ) <-> ( ( ( x + T ) + -u T ) e. dom G /\ ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) ) )
294	287, 293	imbi12d 320	. . . . . . . . . . . . . 14 |- ( y = ( x + T ) -> ( ( ( ph /\ y e. dom G ) -> ( ( y + -u T ) e. dom G /\ ( G ` ( y + -u T ) ) = ( G ` y ) ) ) <-> ( ( ph /\ ( x + T ) e. dom G ) -> ( ( ( x + T ) + -u T ) e. dom G /\ ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) ) ) )
295	119	renegcld 9998	. . . . . . . . . . . . . . 15 |- ( ph -> -u T e. RR )
296	155	mulm1d 10020	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( -u 1 x. T ) = -u T )
297	296	eqcomd 2475	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> -u T = ( -u 1 x. T ) )
298	297	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. RR ) -> -u T = ( -u 1 x. T ) )
299	298	oveq2d 6311	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. RR ) -> ( y + -u T ) = ( y + ( -u 1 x. T ) ) )
300	299	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + -u T ) ) = ( F ` ( y + ( -u 1 x. T ) ) ) )
301	172	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. RR ) -> F : RR --> CC )
302	119	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. RR ) -> T e. RR )
303		1z 10906	. . . . . . . . . . . . . . . . . . 19 |- 1 e. ZZ
304	303	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. RR ) -> 1 e. ZZ )
305	304	znegcld 10980	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. RR ) -> -u 1 e. ZZ )
306		simpr 461	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. RR ) -> y e. RR )
307	181	adantlr 714	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ y e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
308	301, 302, 305, 306, 307	fperiodmul 31404	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + ( -u 1 x. T ) ) ) = ( F ` y ) )
309	300, 308	eqtrd 2508	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + -u T ) ) = ( F ` y ) )
310	172, 295, 309, 5	fperdvper 31571	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. dom G ) -> ( ( y + -u T ) e. dom G /\ ( G ` ( y + -u T ) ) = ( G ` y ) ) )
311	294, 310	vtoclg 3176	. . . . . . . . . . . . 13 |- ( ( x + T ) e. dom G -> ( ( ph /\ ( x + T ) e. dom G ) -> ( ( ( x + T ) + -u T ) e. dom G /\ ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) ) )
312	283, 285, 311	sylc 60	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ( ( ( x + T ) + -u T ) e. dom G /\ ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) )
313	312	simpld 459	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ( ( x + T ) + -u T ) e. dom G )
314	282, 313	eqeltrd 2555	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> x e. dom G )
315	314	ex 434	. . . . . . . . 9 |- ( ( ph /\ x e. RR ) -> ( ( x + T ) e. dom G -> x e. dom G ) )
316	315	con3dimp 441	. . . . . . . 8 |- ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> -. ( x + T ) e. dom G )
317	316	iffalsed 3956	. . . . . . 7 |- ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) = 0 )
318	215	a1i 11	. . . . . . 7 |- ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> 0 e. RR )
319	317, 318	eqeltrd 2555	. . . . . 6 |- ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) e. RR )
320	273, 274, 275, 319	fvmptd 5962	. . . . 5 |- ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> ( H ` ( x + T ) ) = if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) )
321	259	adantl 466	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) /\ s = x ) -> if ( s e. dom G , ( G ` s ) , 0 ) = if ( x e. dom G , ( G ` x ) , 0 ) )
322		simpr 461	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> -. x e. dom G )
323	322	iffalsed 3956	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) = 0 )
324	323	adantr 465	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) /\ s = x ) -> if ( x e. dom G , ( G ` x ) , 0 ) = 0 )
325	321, 324	eqtrd 2508	. . . . . . 7 |- ( ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) /\ s = x ) -> if ( s e. dom G , ( G ` s ) , 0 ) = 0 )
326	246	adantr 465	. . . . . . 7 |- ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> x e. RR )
327	273, 325, 326, 318	fvmptd 5962	. . . . . 6 |- ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> ( H ` x ) = 0 )
328	327	eqcomd 2475	. . . . 5 |- ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> 0 = ( H ` x ) )
329	320, 317, 328	3eqtrd 2512	. . . 4 |- ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> ( H ` ( x + T ) ) = ( H ` x ) )
330	272, 329	pm2.61dan 789	. . 3 |- ( ( ph /\ x e. RR ) -> ( H ` ( x + T ) ) = ( H ` x ) )
331	229	adantr 465	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> H : RR --> RR )
332		ioossre 11598	. . . . . . 7 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
333	332	a1i 11	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
334	331, 333	feqresmpt 5928	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( H ` s ) ) )
335	332	sseli 3505	. . . . . . . . . 10 |- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. RR )
336	335	adantl 466	. . . . . . . . 9 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
337	336, 219	syldan 470	. . . . . . . . 9 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
338	336, 337, 222	syl2anc 661	. . . . . . . 8 |- ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( H ` s ) = if ( s e. dom G , ( G ` s ) , 0 ) )
339	338	adantlr 714	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( H ` s ) = if ( s e. dom G , ( G ` s ) , 0 ) )
340	77	iftrued 3953	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` s ) )
341		eqidd 2468	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( G ` s ) = ( G ` s ) )
342	339, 340, 341	3eqtrd 2512	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( H ` s ) = ( G ` s ) )
343	342	mpteq2dva 4539	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( H ` s ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( G ` s ) ) )
344	12	adantr 465	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> G : dom G --> RR )
345	344, 80	feqresmpt 5928	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( G ` s ) ) )
346	345	eqcomd 2475	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( G ` s ) ) = ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
347	334, 343, 346	3eqtrd 2512	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
348	347, 64	eqeltrd 2555	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
349		eqid 2467	. . 3 |- ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
350		oveq1 6302	. . . . . . . 8 |- ( z = y -> ( z + ( l x. T ) ) = ( y + ( l x. T ) ) )
351	350	eleq1d 2536	. . . . . . 7 |- ( z = y -> ( ( z + ( l x. T ) ) e. ran Q <-> ( y + ( l x. T ) ) e. ran Q ) )
352	351	rexbidv 2978	. . . . . 6 |- ( z = y -> ( E. l e. ZZ ( z + ( l x. T ) ) e. ran Q <-> E. l e. ZZ ( y + ( l x. T ) ) e. ran Q ) )
353	352	cbvrabv 3117	. . . . 5 |- { z e. ( C [,] D ) | E. l e. ZZ ( z + ( l x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q }
354	353	uneq2i 3660	. . . 4 |- ( { C , D } u. { z e. ( C [,] D ) | E. l e. ZZ ( z + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } )
355	354	eqcomi 2480	. . 3 |- ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { z e. ( C [,] D ) | E. l e. ZZ ( z + ( l x. T ) ) e. ran Q } )
356	37	fveq2i 5875	. . . 4 |- ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) = ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) )
357	356	oveq1i 6305	. . 3 |- ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 )
358		isoeq1 6214	. . . . 5 |- ( f = g -> ( f Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ (