Theorem fourierdlem113 38195

Description: Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem113.f	|- ( ph -> F : RR --> RR )
fourierdlem113.t	|- T = ( 2 x. pi )
fourierdlem113.per	|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem113.x	|- ( ph -> X e. RR )
fourierdlem113.l	|- ( ph -> L e. ( ( F |` ( -oo (,) X ) ) lim CC X ) )
fourierdlem113.r	|- ( ph -> R e. ( ( F |` ( X (,) +oo ) ) lim CC X ) )
fourierdlem113.p	|- P = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` n ) = pi ) /\ A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem113.m	|- ( ph -> M e. NN )
fourierdlem113.q	|- ( ph -> Q e. ( P ` M ) )
fourierdlem113.dvcn	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem113.dvlb	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) =/= (/) )
fourierdlem113.dvub	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) =/= (/) )
fourierdlem113.a	|- A = ( n e. NN0 |-> ( S. ( -u pi (,) pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / pi ) )
fourierdlem113.b	|- B = ( n e. NN |-> ( S. ( -u pi (,) pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / pi ) )
fourierdlem113.15	|- S = ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
fourierdlem113.e	|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( pi - x ) / T ) ) x. T ) ) )
fourierdlem113.exq	|- ( ph -> ( E ` X ) e. ran Q )

Assertion

Ref	Expression
fourierdlem113	|- ( ph -> ( seq 1 ( + , S ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) /\ ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( L + R ) / 2 ) ) )

Distinct variable groups:   A, n   B, n   x, E   i, F, n, x   i, L, n   i, M, x, n   M, p, i, n   Q, i, x, n   Q, p   R, i, n   T, i, x, n   T, p   i, X, x, n   X, p   ph, i, x, n

Allowed substitution hints:   ph( p)   A( x, i, p)   B( x, i, p)   P( x, i, n, p)   R( x, p)   S( x, i, n, p)   E( i, n, p)   F( p)   L( x, p)

Proof of Theorem fourierdlem113

Dummy variables j k m w y t u z f g are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem113.f	. 2 |- ( ph -> F : RR --> RR )
2		oveq1 6315	. . . . . . 7 |- ( w = y -> ( w mod ( 2 x. pi ) ) = ( y mod ( 2 x. pi ) ) )
3	2	eqeq1d 2473	. . . . . 6 |- ( w = y -> ( ( w mod ( 2 x. pi ) ) = 0 <-> ( y mod ( 2 x. pi ) ) = 0 ) )
4		oveq2 6316	. . . . . . . 8 |- ( w = y -> ( ( k + ( 1 / 2 ) ) x. w ) = ( ( k + ( 1 / 2 ) ) x. y ) )
5	4	fveq2d 5883	. . . . . . 7 |- ( w = y -> ( sin ` ( ( k + ( 1 / 2 ) ) x. w ) ) = ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) )
6		oveq1 6315	. . . . . . . . 9 |- ( w = y -> ( w / 2 ) = ( y / 2 ) )
7	6	fveq2d 5883	. . . . . . . 8 |- ( w = y -> ( sin ` ( w / 2 ) ) = ( sin ` ( y / 2 ) ) )
8	7	oveq2d 6324	. . . . . . 7 |- ( w = y -> ( ( 2 x. pi ) x. ( sin ` ( w / 2 ) ) ) = ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) )
9	5, 8	oveq12d 6326	. . . . . 6 |- ( w = y -> ( ( sin ` ( ( k + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. pi ) x. ( sin ` ( w / 2 ) ) ) ) = ( ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) )
10	3, 9	ifbieq2d 3897	. . . . 5 |- ( w = y -> if ( ( w mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. pi ) x. ( sin ` ( w / 2 ) ) ) ) ) = if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
11	10	cbvmptv 4488	. . . 4 |- ( w e. RR |-> if ( ( w mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. pi ) x. ( sin ` ( w / 2 ) ) ) ) ) ) = ( y e. RR |-> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
12		oveq2 6316	. . . . . . . 8 |- ( k = m -> ( 2 x. k ) = ( 2 x. m ) )
13	12	oveq1d 6323	. . . . . . 7 |- ( k = m -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. m ) + 1 ) )
14	13	oveq1d 6323	. . . . . 6 |- ( k = m -> ( ( ( 2 x. k ) + 1 ) / ( 2 x. pi ) ) = ( ( ( 2 x. m ) + 1 ) / ( 2 x. pi ) ) )
15		oveq1 6315	. . . . . . . . 9 |- ( k = m -> ( k + ( 1 / 2 ) ) = ( m + ( 1 / 2 ) ) )
16	15	oveq1d 6323	. . . . . . . 8 |- ( k = m -> ( ( k + ( 1 / 2 ) ) x. y ) = ( ( m + ( 1 / 2 ) ) x. y ) )
17	16	fveq2d 5883	. . . . . . 7 |- ( k = m -> ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) = ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) )
18	17	oveq1d 6323	. . . . . 6 |- ( k = m -> ( ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) )
19	14, 18	ifeq12d 3892	. . . . 5 |- ( k = m -> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
20	19	mpteq2dv 4483	. . . 4 |- ( k = m -> ( y e. RR |-> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) = ( y e. RR |-> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
21	11, 20	syl5eq 2517	. . 3 |- ( k = m -> ( w e. RR |-> if ( ( w mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. pi ) x. ( sin ` ( w / 2 ) ) ) ) ) ) = ( y e. RR |-> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
22	21	cbvmptv 4488	. 2 |- ( k e. NN |-> ( w e. RR |-> if ( ( w mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. pi ) x. ( sin ` ( w / 2 ) ) ) ) ) ) ) = ( m e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
23		fourierdlem113.p	. 2 |- P = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` n ) = pi ) /\ A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
24		fourierdlem113.m	. 2 |- ( ph -> M e. NN )
25		fourierdlem113.q	. 2 |- ( ph -> Q e. ( P ` M ) )
26		oveq1 6315	. . . . . . . 8 |- ( w = y -> ( w + ( j x. T ) ) = ( y + ( j x. T ) ) )
27	26	eleq1d 2533	. . . . . . 7 |- ( w = y -> ( ( w + ( j x. T ) ) e. ran Q <-> ( y + ( j x. T ) ) e. ran Q ) )
28	27	rexbidv 2892	. . . . . 6 |- ( w = y -> ( E. j e. ZZ ( w + ( j x. T ) ) e. ran Q <-> E. j e. ZZ ( y + ( j x. T ) ) e. ran Q ) )
29	28	cbvrabv 3030	. . . . 5 |- { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } = { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q }
30	29	uneq2i 3576	. . . 4 |- ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) = ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } )
31	30	fveq2i 5882	. . 3 |- ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) = ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) )
32	31	oveq1i 6318	. 2 |- ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) = ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) - 1 )
33		oveq1 6315	. . . . . . . . . . . 12 |- ( k = j -> ( k x. T ) = ( j x. T ) )
34	33	oveq2d 6324	. . . . . . . . . . 11 |- ( k = j -> ( y + ( k x. T ) ) = ( y + ( j x. T ) ) )
35	34	eleq1d 2533	. . . . . . . . . 10 |- ( k = j -> ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( j x. T ) ) e. ran Q ) )
36	35	cbvrexv 3006	. . . . . . . . 9 |- ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. j e. ZZ ( y + ( j x. T ) ) e. ran Q )
37	36	a1i 11	. . . . . . . 8 |- ( y e. ( ( -u pi + X ) [,] ( pi + X ) ) -> ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. j e. ZZ ( y + ( j x. T ) ) e. ran Q ) )
38	37	rabbiia 3019	. . . . . . 7 |- { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q }
39	38	uneq2i 3576	. . . . . 6 |- ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } )
40		isoeq5 6232	. . . . . 6 |- ( ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) ) )
41	39, 40	ax-mp 5	. . . . 5 |- ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) )
42	41	a1i 11	. . . 4 |- ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) ) )
43	33	oveq2d 6324	. . . . . . . . . . . . . 14 |- ( k = j -> ( w + ( k x. T ) ) = ( w + ( j x. T ) ) )
44	43	eleq1d 2533	. . . . . . . . . . . . 13 |- ( k = j -> ( ( w + ( k x. T ) ) e. ran Q <-> ( w + ( j x. T ) ) e. ran Q ) )
45	44	cbvrexv 3006	. . . . . . . . . . . 12 |- ( E. k e. ZZ ( w + ( k x. T ) ) e. ran Q <-> E. j e. ZZ ( w + ( j x. T ) ) e. ran Q )
46	45	a1i 11	. . . . . . . . . . 11 |- ( w e. ( ( -u pi + X ) [,] ( pi + X ) ) -> ( E. k e. ZZ ( w + ( k x. T ) ) e. ran Q <-> E. j e. ZZ ( w + ( j x. T ) ) e. ran Q ) )
47	46	rabbiia 3019	. . . . . . . . . 10 |- { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } = { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q }
48	47	uneq2i 3576	. . . . . . . . 9 |- ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) = ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } )
49	48	fveq2i 5882	. . . . . . . 8 |- ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) = ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) )
50	49	oveq1i 6318	. . . . . . 7 |- ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) = ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 )
51	50	oveq2i 6319	. . . . . 6 |- ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) = ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) )
52		isoeq4 6231	. . . . . 6 |- ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) = ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) ) )
53	51, 52	ax-mp 5	. . . . 5 |- ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) )
54	53	a1i 11	. . . 4 |- ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) ) )
55		isoeq1 6228	. . . 4 |- ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) ) )
56	42, 54, 55	3bitrd 287	. . 3 |- ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) ) )
57	56	cbviotav 5559	. 2 |- ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) )
58		fourierdlem113.x	. 2 |- ( ph -> X e. RR )
59		pire 23492	. . . . 5 |- pi e. RR
60	59	renegcli 9955	. . . 4 |- -u pi e. RR
61	60	a1i 11	. . 3 |- ( ph -> -u pi e. RR )
62	59	a1i 11	. . 3 |- ( ph -> pi e. RR )
63		negpilt0 37580	. . . 4 |- -u pi < 0
64	63	a1i 11	. . 3 |- ( ph -> -u pi < 0 )
65		pipos 23494	. . . 4 |- 0 < pi
66	65	a1i 11	. . 3 |- ( ph -> 0 < pi )
67		picn 23493	. . . . 5 |- pi e. CC
68	67	2timesi 10753	. . . 4 |- ( 2 x. pi ) = ( pi + pi )
69		fourierdlem113.t	. . . 4 |- T = ( 2 x. pi )
70	67, 67	subnegi 9973	. . . 4 |- ( pi - -u pi ) = ( pi + pi )
71	68, 69, 70	3eqtr4i 2503	. . 3 |- T = ( pi - -u pi )
72	23	fourierdlem2 38083	. . . . . . . 8 |- ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
73	24, 72	syl 17	. . . . . . 7 |- ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
74	25, 73	mpbid 215	. . . . . 6 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
75	74	simpld 466	. . . . 5 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
76		elmapi 7511	. . . . 5 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
77	75, 76	syl 17	. . . 4 |- ( ph -> Q : ( 0 ... M ) --> RR )
78		fzfid 12224	. . . 4 |- ( ph -> ( 0 ... M ) e. Fin )
79		rnffi 37513	. . . 4 |- ( ( Q : ( 0 ... M ) --> RR /\ ( 0 ... M ) e. Fin ) -> ran Q e. Fin )
80	77, 78, 79	syl2anc 673	. . 3 |- ( ph -> ran Q e. Fin )
81	23, 24, 25	fourierdlem15 38096	. . . 4 |- ( ph -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
82		frn 5747	. . . 4 |- ( Q : ( 0 ... M ) --> ( -u pi [,] pi ) -> ran Q C_ ( -u pi [,] pi ) )
83	81, 82	syl 17	. . 3 |- ( ph -> ran Q C_ ( -u pi [,] pi ) )
84	74	simprd 470	. . . . 5 |- ( ph -> ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
85	84	simplrd 771	. . . 4 |- ( ph -> ( Q ` M ) = pi )
86		ffun 5742	. . . . . 6 |- ( Q : ( 0 ... M ) --> ( -u pi [,] pi ) -> Fun Q )
87	81, 86	syl 17	. . . . 5 |- ( ph -> Fun Q )
88	24	nnnn0d 10949	. . . . . . . 8 |- ( ph -> M e. NN0 )
89		nn0uz 11217	. . . . . . . 8 |- NN0 = ( ZZ>= ` 0 )
90	88, 89	syl6eleq 2559	. . . . . . 7 |- ( ph -> M e. ( ZZ>= ` 0 ) )
91		eluzfz2 11833	. . . . . . 7 |- ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
92	90, 91	syl 17	. . . . . 6 |- ( ph -> M e. ( 0 ... M ) )
93		fdm 5745	. . . . . . . 8 |- ( Q : ( 0 ... M ) --> ( -u pi [,] pi ) -> dom Q = ( 0 ... M ) )
94	81, 93	syl 17	. . . . . . 7 |- ( ph -> dom Q = ( 0 ... M ) )
95	94	eqcomd 2477	. . . . . 6 |- ( ph -> ( 0 ... M ) = dom Q )
96	92, 95	eleqtrd 2551	. . . . 5 |- ( ph -> M e. dom Q )
97		fvelrn 6030	. . . . 5 |- ( ( Fun Q /\ M e. dom Q ) -> ( Q ` M ) e. ran Q )
98	87, 96, 97	syl2anc 673	. . . 4 |- ( ph -> ( Q ` M ) e. ran Q )
99	85, 98	eqeltrrd 2550	. . 3 |- ( ph -> pi e. ran Q )
100		fourierdlem113.e	. . 3 |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( pi - x ) / T ) ) x. T ) ) )
101		fourierdlem113.exq	. . 3 |- ( ph -> ( E ` X ) e. ran Q )
102		eqid 2471	. . 3 |- ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) = ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } )
103		isoeq1 6228	. . . . 5 |- ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) )
104	30, 48, 39	3eqtr4ri 2504	. . . . . 6 |- ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } )
105		isoeq5 6232	. . . . . 6 |- ( ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) -> ( f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) ) )
106	104, 105	ax-mp 5	. . . . 5 |- ( f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) )
107	103, 106	syl6bb 269	. . . 4 |- ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) ) )
108	107	cbviotav 5559	. . 3 |- ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) )
109		eqid 2471	. . 3 |- { w e. ( ( -u pi + X ) (,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } = { w e. ( ( -u pi + X ) (,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q }
110	61, 62, 64, 66, 71, 80, 83, 99, 100, 58, 101, 102, 108, 109	fourierdlem51 38133	. 2 |- ( ph -> X e. ran ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { w e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) )
111		fourierdlem113.per	. 2 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
112		ax-resscn 9614	. . . 4 |- RR C_ CC
113	112	a1i 11	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> RR C_ CC )
114		ioossre 11721	. . . . . . 7 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
115	114	a1i 11	. . . . . 6 |- ( ph -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
116	1, 115	fssresd 5762	. . . . 5 |- ( ph -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> RR )
117	112	a1i 11	. . . . 5 |- ( ph -> RR C_ CC )
118	116, 117	fssd 5750	. . . 4 |- ( ph -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
119	118	adantr 472	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
120	114	a1i 11	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
121	1, 117	fssd 5750	. . . . . . 7 |- ( ph -> F : RR --> CC )
122	121	adantr 472	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F : RR --> CC )
123		ssid 3437	. . . . . . 7 |- RR C_ RR
124	123	a1i 11	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> RR C_ RR )
125		eqid 2471	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
126	125	tgioo2 21899	. . . . . . 7 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
127	125, 126	dvres 22945	. . . . . 6 |- ( ( ( RR C_ CC /\ F : RR --> CC ) /\ ( RR C_ RR /\ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR ) ) -> ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) )
128	113, 122, 124, 120, 127	syl22anc 1293	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) )
129	128	dmeqd 5042	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> dom ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = dom ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) )
130		ioontr 37707	. . . . . . 7 |- ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) )
131	130	reseq2i 5108	. . . . . 6 |- ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
132	131	dmeqi 5041	. . . . 5 |- dom ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
133	132	a1i 11	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> dom ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
134		fourierdlem113.dvcn	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
135		cncff 22003	. . . . 5 |- ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
136		fdm 5745	. . . . 5 |- ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC -> dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
137	134, 135, 136	3syl 18	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
138	129, 133, 137	3eqtrd 2509	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> dom ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
139		dvcn 22954	. . 3 |- ( ( ( RR C_ CC /\ ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC /\ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR ) /\ dom ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
140	113, 119, 120, 138, 139	syl31anc 1295	. 2 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
141	120, 113	sstrd 3428	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
142	77	adantr 472	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
143		fzofzp1 12037	. . . . . . 7 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
144	143	adantl 473	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
145	142, 144	ffvelrnd 6038	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
146	145	rexrd 9708	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
147		elfzofz 11962	. . . . . 6 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
148	147	adantl 473	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
149	142, 148	ffvelrnd 6038	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
150	74	simprrd 775	. . . . 5 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
151	150	r19.21bi 2776	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
152	125, 146, 149, 151	lptioo1cn 37824	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
153	116	adantr 472	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> RR )
154	123	a1i 11	. . . . . . . 8 |- ( ph -> RR C_ RR )
155	117, 121, 154	dvbss 22935	. . . . . . 7 |- ( ph -> dom ( RR _D F ) C_ RR )
156		dvfre 22984	. . . . . . . 8 |- ( ( F : RR --> RR /\ RR C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
157	1, 154, 156	syl2anc 673	. . . . . . 7 |- ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
158		0re 9661	. . . . . . . . . 10 |- 0 e. RR
159	60, 158, 59	lttri 9778	. . . . . . . . 9 |- ( ( -u pi < 0 /\ 0 < pi ) -> -u pi < pi )
160	63, 65, 159	mp2an 686	. . . . . . . 8 |- -u pi < pi
161	160	a1i 11	. . . . . . 7 |- ( ph -> -u pi < pi )
162	84	simplld 769	. . . . . . 7 |- ( ph -> ( Q ` 0 ) = -u pi )
163	134, 135	syl 17	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
164		fourierdlem113.dvlb	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) =/= (/) )
165	163, 141, 152, 164, 125	ellimciota 37791	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( iota x x e. ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) ) e. ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
166	149	rexrd 9708	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
167	125, 166, 145, 151	lptioo2cn 37823	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
168		fourierdlem113.dvub	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) =/= (/) )
169	163, 141, 167, 168, 125	ellimciota 37791	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( iota x x e. ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) e. ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
170	121	adantr 472	. . . . . . . . . 10 |- ( ( ph /\ k e. ZZ ) -> F : RR --> CC )
171		zre 10965	. . . . . . . . . . . 12 |- ( k e. ZZ -> k e. RR )
172	171	adantl 473	. . . . . . . . . . 11 |- ( ( ph /\ k e. ZZ ) -> k e. RR )
173		2re 10701	. . . . . . . . . . . . . . 15 |- 2 e. RR
174	173, 59	remulcli 9675	. . . . . . . . . . . . . 14 |- ( 2 x. pi ) e. RR
175	174	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( 2 x. pi ) e. RR )
176	69, 175	syl5eqel 2553	. . . . . . . . . . . 12 |- ( ph -> T e. RR )
177	176	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ k e. ZZ ) -> T e. RR )
178	172, 177	remulcld 9689	. . . . . . . . . 10 |- ( ( ph /\ k e. ZZ ) -> ( k x. T ) e. RR )
179	170	adantr 472	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> F : RR --> CC )
180	177	adantr 472	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> T e. RR )
181		simplr 770	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> k e. ZZ )
182		simpr 468	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> t e. RR )
183	111	adant423 37430	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
184	179, 180, 181, 182, 183	fperiodmul 37610	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> ( F ` ( t + ( k x. T ) ) ) = ( F ` t ) )
185		eqid 2471	. . . . . . . . . 10 |- ( RR _D F ) = ( RR _D F )
186	170, 178, 184, 185	fperdvper 37887	. . . . . . . . 9 |- ( ( ( ph /\ k e. ZZ ) /\ t e. dom ( RR _D F ) ) -> ( ( t + ( k x. T ) ) e. dom ( RR _D F ) /\ ( ( RR _D F ) ` ( t + ( k x. T ) ) ) = ( ( RR _D F ) ` t ) ) )
187	186	an32s 821	. . . . . . . 8 |- ( ( ( ph /\ t e. dom ( RR _D F ) ) /\ k e. ZZ ) -> ( ( t + ( k x. T ) ) e. dom ( RR _D F ) /\ ( ( RR _D F ) ` ( t + ( k x. T ) ) ) = ( ( RR _D F ) ` t ) ) )
188	187	simpld 466	. . . . . . 7 |- ( ( ( ph /\ t e. dom ( RR _D F ) ) /\ k e. ZZ ) -> ( t + ( k x. T ) ) e. dom ( RR _D F ) )
189	187	simprd 470	. . . . . . 7 |- ( ( ( ph /\ t e. dom ( RR _D F ) ) /\ k e. ZZ ) -> ( ( RR _D F ) ` ( t + ( k x. T ) ) ) = ( ( RR _D F ) ` t ) )
190		fveq2 5879	. . . . . . . . 9 |- ( j = i -> ( Q ` j ) = ( Q ` i ) )
191		oveq1 6315	. . . . . . . . . 10 |- ( j = i -> ( j + 1 ) = ( i + 1 ) )
192	191	fveq2d 5883	. . . . . . . . 9 |- ( j = i -> ( Q ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) )
193	190, 192	oveq12d 6326	. . . . . . . 8 |- ( j = i -> ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
194	193	cbvmptv 4488	. . . . . . 7 |- ( j e. ( 0..^ M ) |-> ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) = ( i e. ( 0..^ M ) |-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
195		eqid 2471	. . . . . . 7 |- ( t e. RR |-> ( t + ( ( |_ ` ( ( pi - t ) / T ) ) x. T ) ) ) = ( t e. RR |-> ( t + ( ( |_ ` ( ( pi - t ) / T ) ) x. T ) ) )
196	155, 157, 61, 62, 161, 71, 24, 77, 162, 85, 134, 165, 169, 188, 189, 194, 195	fourierdlem71 38153	. . . . . 6 |- ( ph -> E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
197	196	adantr 472	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
198		nfv 1769	. . . . . . . . 9 |- F/ t ( ph /\ i e. ( 0..^ M ) )
199		nfra1 2785	. . . . . . . . 9 |- F/ t A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z
200	198, 199	nfan 2031	. . . . . . . 8 |- F/ t ( ( ph /\ i e. ( 0..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
201	128, 131	syl6eq 2521	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
202	201	fveq1d 5881	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) = ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) )
203		fvres 5893	. . . . . . . . . . . . 13 |- ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
204	202, 203	sylan9eq 2525	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
205	204	fveq2d 5883	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) = ( abs ` ( ( RR _D F ) ` t ) ) )
206	205	adantlr 729	. . . . . . . . . 10 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) = ( abs ` ( ( RR _D F ) ` t ) ) )
207		simplr 770	. . . . . . . . . . 11 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
208		ssdmres 5132	. . . . . . . . . . . . . 14 |- ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom ( RR _D F ) <-> dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
209	137, 208	sylibr 217	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom ( RR _D F ) )
210	209	ad2antrr 740	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom ( RR _D F ) )
211		simpr 468	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
212	210, 211	sseldd 3419	. . . . . . . . . . 11 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> t e. dom ( RR _D F ) )
213		rspa 2774	. . . . . . . . . . 11 |- ( ( A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z /\ t e. dom ( RR _D F ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
214	207, 212, 213	syl2anc 673	. . . . . . . . . 10 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
215	206, 214	eqbrtrd 4416	. . . . . . . . 9 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z )
216	215	ex 441	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z ) )
217	200, 216	ralrimi 2800	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) -> A. t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z )
218	217	ex 441	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z -> A. t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z ) )
219	218	reximdv 2857	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z -> E. z e. RR A. t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z ) )
220	197, 219	mpd 15	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> E. z e. RR A. t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z )
221	149, 145, 153, 138, 220	ioodvbdlimc1 37904	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) =/= (/) )
222	119, 141, 152, 221, 125	ellimciota 37791	. 2 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( iota y y e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) ) e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
223	149, 145, 153, 138, 220	ioodvbdlimc2 37907	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) =/= (/) )
224	119, 141, 167, 223, 125	ellimciota 37791	. 2 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( iota y y e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
225		frel 5744	. . . . . . 7 |- ( ( RR _D F ) : dom ( RR _D F ) --> RR -> Rel ( RR _D F ) )
226	157, 225	syl 17	. . . . . 6 |- ( ph -> Rel ( RR _D F ) )
227		resindm 5155	. . . . . 6 |- ( Rel ( RR _D F ) -> ( ( RR _D F ) |` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) = ( ( RR _D F ) |` ( -oo (,) X ) ) )
228	226, 227	syl 17	. . . . 5 |- ( ph -> ( ( RR _D F ) |` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) = ( ( RR _D F ) |` ( -oo (,) X ) ) )
229		inss2 3644	. . . . . . 7 |- ( ( -oo (,) X ) i^i dom ( RR _D F ) ) C_ dom ( RR _D F )
230	229	a1i 11	. . . . . 6 |- ( ph -> ( ( -oo (,) X ) i^i dom ( RR _D F ) ) C_ dom ( RR _D F ) )
231	157, 230	fssresd 5762	. . . . 5 |- ( ph -> ( ( RR _D F ) |` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) : ( ( -oo (,) X ) i^i dom ( RR _D F ) ) --> RR )
232	228, 231	feq1dd 37503	. . . 4 |- ( ph -> ( ( RR _D F ) |` ( -oo (,) X ) ) : ( ( -oo (,) X ) i^i dom ( RR _D F ) ) --> RR )
233	232, 117	fssd 5750	. . 3 |- ( ph -> ( ( RR _D F ) |` ( -oo (,) X ) ) : ( ( -oo (,) X ) i^i dom ( RR _D F ) ) --> CC )
234		ioosscn 37687	. . . . 5 |- ( -oo (,) X ) C_ CC
235		ssinss1 3651	. . . . 5 |- ( ( -oo (,) X ) C_ CC -> ( ( -oo (,) X ) i^i dom ( RR _D F ) ) C_ CC )
236	234, 235	ax-mp 5	. . . 4 |- ( ( -oo (,) X ) i^i dom ( RR _D F ) ) C_ CC
237	236	a1i 11	. . 3 |- ( ph -> ( ( -oo (,) X ) i^i dom ( RR _D F ) ) C_ CC )
238		3simpb 1028	. . . . . . . 8 |- ( ( ph /\ x e. dom ( RR _D F ) /\ k e. ZZ ) -> ( ph /\ k e. ZZ ) )
239		simp2 1031	. . . . . . . 8 |- ( ( ph /\ x e. dom ( RR _D F ) /\ k e. ZZ ) -> x e. dom ( RR _D F ) )
240	170	adantr 472	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> F : RR --> CC )
241	177	adantr 472	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> T e. RR )
242		simplr 770	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> k e. ZZ )
243		simpr 468	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> x e. RR )
244		eleq1 2537	. . . . . . . . . . . . . 14 |- ( x = y -> ( x e. RR <-> y e. RR ) )
245	244	anbi2d 718	. . . . . . . . . . . . 13 |- ( x = y -> ( ( ph /\ x e. RR ) <-> ( ph /\ y e. RR ) ) )
246		oveq1 6315	. . . . . . . . . . . . . . 15 |- ( x = y -> ( x + T ) = ( y + T ) )
247	246	fveq2d 5883	. . . . . . . . . . . . . 14 |- ( x = y -> ( F ` ( x + T ) ) = ( F ` ( y + T ) ) )
248		fveq2 5879	. . . . . . . . . . . . . 14 |- ( x = y -> ( F ` x ) = ( F ` y ) )
249	247, 248	eqeq12d 2486	. . . . . . . . . . . . 13 |- ( x = y -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( y + T ) ) = ( F ` y ) ) )
250	245, 249	imbi12d 327	. . . . . . . . . . . 12 |- ( x = y -> ( ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ y e. RR ) -> ( F ` ( y + T ) ) = ( F ` y ) ) ) )
251	250, 111	chvarv 2120	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + T ) ) = ( F ` y ) )
252	251	adant423 37430	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) /\ y e. RR ) -> ( F ` ( y + T ) ) = ( F ` y ) )
253	240, 241, 242, 243, 252	fperiodmul 37610	. . . . . . . . 9 |- ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
254	170, 178, 253, 185	fperdvper 37887	. . . . . . . 8 |- ( ( ( ph /\ k e. ZZ ) /\ x e. dom ( RR _D F ) ) -> ( ( x + ( k x. T ) ) e. dom ( RR _D F ) /\ ( ( RR _D F ) ` ( x + ( k x. T ) ) ) = ( ( RR _D F ) ` x ) ) )
255	238, 239, 254	syl2anc 673	. . . . . . 7 |- ( ( ph /\ x e. dom ( RR _D F ) /\ k e. ZZ ) -> ( ( x + ( k x. T ) ) e. dom ( RR _D F ) /\ ( ( RR _D F ) ` ( x + ( k x. T ) ) ) = ( ( RR _D F ) ` x ) ) )
256	255	simpld 466	. . . . . 6 |- ( ( ph /\ x e. dom ( RR _D F ) /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. dom ( RR _D F ) )
257		oveq2 6316	. . . . . . . . . 10 |- ( w = x -> ( pi - w ) = ( pi - x ) )
258	257	oveq1d 6323	. . . . . . . . 9 |- ( w = x -> ( ( pi - w ) / T ) = ( ( pi - x ) / T ) )
259	258	fveq2d 5883	. . . . . . . 8 |- ( w = x -> ( |_ ` ( ( pi - w ) / T ) ) = ( |_ ` ( ( pi - x ) / T ) ) )
260	259	oveq1d 6323	. . . . . . 7 |- ( w = x -> ( ( |_ ` ( ( pi - w ) / T ) ) x. T ) = ( ( |_ ` ( ( pi - x ) / T ) ) x. T ) )
261	260	cbvmptv 4488	. . . . . 6 |- ( w e. RR |-> ( ( |_ ` ( ( pi - w ) / T ) ) x. T ) ) = ( x e. RR |-> ( ( |_ ` ( ( pi - x ) / T ) ) x. T ) )
262		eqid 2471	. . . . . 6 |- ( x e. RR |-> ( x + ( ( w e. RR |-> ( ( |_ ` ( ( pi - w ) / T ) ) x. T ) ) ` x ) ) ) = ( x e. RR |-> ( x + ( ( w e. RR |-> ( ( |_ ` ( ( pi - w ) / T ) ) x. T ) ) ` x ) ) )
263	61, 62, 161, 71, 256, 58, 261, 262, 23, 24, 25, 209	fourierdlem41 38123	. . . . 5 |- ( ph -> ( E. y e. RR ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) /\ E. y e. RR ( X < y /\ ( X (,) y ) C_ dom ( RR _D F ) ) ) )
264	263	simpld 466	. . . 4 |- ( ph -> E. y e. RR ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) )
265	125	cnfldtop 21882	. . . . . . . . 9 |- ( TopOpen ` ℂfld ) e. Top
266	265	a1i 11	. . . . . . . 8 |- ( ( ph /\ y e. RR /\ ( y (,) X ) C_ dom ( RR _D F ) ) -> ( TopOpen ` ℂfld ) e. Top )
267	236	a1i 11	. . . . . . . 8 |- ( ( ph /\ y e. RR /\ ( y (,) X ) C_ dom ( RR _D F ) ) -> ( ( -oo (,) X ) i^i dom ( RR _D F ) ) C_ CC )
268		mnfxr 11437	. . . . . . . . . . . 12 |- -oo e. RR*
269	268	a1i 11	. . . . . . . . . . 11 |- ( y e. RR -> -oo e. RR* )
270		rexr 9704	. . . . . . . . . . . 12 |- ( y e. RR -> y e. RR* )
271		mnflt 11448	. . . . . . . . . . . 12 |- ( y e. RR -> -oo < y )
272	269, 270, 271	xrltled 37574	. . . . . . . . . . 11 |- ( y e. RR -> -oo <_ y )
273		iooss1 11696	. . . . . . . . . . 11 |- ( ( -oo e. RR* /\ -oo <_ y ) -> ( y (,) X ) C_ ( -oo (,) X ) )
274	269, 272, 273	syl2anc 673	. . . . . . . . . 10 |- ( y e. RR -> ( y (,) X ) C_ ( -oo (,) X ) )
275	274	3ad2ant2 1052	. . . . . . . . 9 |- ( ( ph /\ y e. RR /\ ( y (,) X ) C_ dom ( RR _D F ) ) -> ( y (,) X ) C_ ( -oo (,) X ) )
276		simp3 1032	. . . . . . . . 9 |- ( ( ph /\ y e. RR /\ ( y (,) X ) C_ dom ( RR _D F ) ) -> ( y (,) X ) C_ dom ( RR _D F ) )
277	275, 276	ssind 3647	. . . . . . . 8 |- ( ( ph /\ y e. RR /\ ( y (,) X ) C_ dom ( RR _D F ) ) -> ( y (,) X ) C_ ( ( -oo (,) X ) i^i dom ( RR _D F ) ) )
278		unicntop 37433	. . . . . . . . 9 |- CC = U. ( TopOpen ` ℂfld )
279	278	lpss3 20237	. . . . . . . 8 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( ( -oo (,) X ) i^i dom ( RR _D F ) ) C_ CC /\ ( y (,) X ) C_ ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) -> ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( y (,) X ) ) C_ ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) )
280	266, 267, 277, 279	syl3anc 1292	. . . . . . 7 |- ( ( ph /\ y e. RR /\ ( y (,) X ) C_ dom ( RR _D F ) ) -> ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( y (,) X ) ) C_ ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) )
281	280	3adant3l 1288	. . . . . 6 |- ( ( ph /\ y e. RR /\ ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) ) -> ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( y (,) X ) ) C_ ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) )
282	270	3ad2ant2 1052	. . . . . . 7 |- ( ( ph /\ y e. RR /\ ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) ) -> y e. RR* )
283	58	3ad2ant1 1051	. . . . . . 7 |- ( ( ph /\ y e. RR /\ ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) ) -> X e. RR )
284		simp3l 1058	. . . . . . 7 |- ( ( ph /\ y e. RR /\ ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) ) -> y < X )
285	125, 282, 283, 284	lptioo2cn 37823	. . . . . 6 |- ( ( ph /\ y e. RR /\ ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) ) -> X e. ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( y (,) X ) ) )
286	281, 285	sseldd 3419	. . . . 5 |- ( ( ph /\ y e. RR /\ ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) ) -> X e. ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) )
287	286	rexlimdv3a 2873	. . . 4 |- ( ph -> ( E. y e. RR ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) -> X e. ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) ) )
288	264, 287	mpd 15	. . 3 |- ( ph -> X e. ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) )
289	255	simprd 470	. . . 4 |- ( ( ph /\ x e. dom ( RR _D F ) /\ k e. ZZ ) -> ( ( RR _D F ) ` ( x + ( k x. T ) ) ) = ( ( RR _D F ) ` x ) )
290		oveq2 6316	. . . . . . . 8 |- ( y = x -> ( pi - y ) = ( pi - x ) )
291	290	oveq1d 6323	. . . . . . 7 |- ( y = x -> ( ( pi - y ) / T ) = ( ( pi - x ) / T ) )
292	291	fveq2d 5883	. . . . . 6 |- ( y = x -> ( |_ ` ( ( pi - y ) / T ) ) = ( |_ ` ( ( pi - x ) / T ) ) )
293	292	oveq1d 6323	. . . . 5 |- ( y = x -> ( ( |_ ` ( ( pi - y ) / T ) ) x. T ) = ( ( |_ ` ( ( pi - x ) / T ) ) x. T ) )
294	293	cbvmptv 4488	. . . 4 |- ( y e. RR |-> ( ( |_ ` ( ( pi - y ) / T ) ) x. T ) ) = ( x e. RR |-> ( ( |_ ` ( ( pi - x ) / T ) ) x. T ) )
295		id 22	. . . . . 6 |- ( z = x -> z = x )
296		fveq2 5879	. . . . . 6 |- ( z = x -> ( ( y e. RR |-> ( ( |_ ` ( ( pi - y ) /