Theorem fourierdlem109 38191

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by any value X. This lemma generalizes fourierdlem92 38174 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem109.a	|- ( ph -> A e. RR )
fourierdlem109.b	|- ( ph -> B e. RR )
fourierdlem109.t	|- T = ( B - A )
fourierdlem109.x	|- ( ph -> X e. RR )
fourierdlem109.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 ) ) ) } )
fourierdlem109.m	|- ( ph -> M e. NN )
fourierdlem109.q	|- ( ph -> Q e. ( P ` M ) )
fourierdlem109.f	|- ( ph -> F : RR --> CC )
fourierdlem109.fper	|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem109.fcn	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem109.r	|- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
fourierdlem109.l	|- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
fourierdlem109.o	|- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem109.h	|- H = ( { ( A - X ) , ( B - X ) } u. { x e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
fourierdlem109.n	|- N = ( ( # ` H ) - 1 )
fourierdlem109.16	|- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
fourierdlem109.17	|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
fourierdlem109.18	|- J = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
fourierdlem109.19	|- I = ( x e. RR |-> sup ( { j e. ( 0..^ M ) | ( Q ` j ) <_ ( J ` ( E ` x ) ) } , RR , < ) )

Assertion

Ref	Expression
fourierdlem109	|- ( ph -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )

Distinct variable groups:   A, f, j, k, y   A, i, x, j, k, y   A, m, p, i, j   B, f, j, k, y   B, i, x   B, m, p   f, E, j, k, y   i, E, x   i, F, j, x, y   f, H, y   x, H   f, I, k, y   i, I, x   i, J, j, x, y   x, L, y   i, M, x, y, j   m, M, p   f, N, j, k, y   i, N, x   m, N, p   Q, f, j, k, y   Q, i, x   Q, m, p   x, R, y   S, f, j, k, y   S, i, x   S, m, p   T, f, j, k, y   T, i, x   T, m, p   f, X, j, y   i, X, m, p   x, X   ph, f, j, k, y   ph, i, x

Allowed substitution hints:   ph( m, p)   P( x, y, f, i, j, k, m, p)   R( f, i, j, k, m, p)   E( m, p)   F( f, k, m, p)   H( i, j, k, m, p)   I( j, m, p)   J( f, k, m, p)   L( f, i, j, k, m, p)   M( f, k)   O( x, y, f, i, j, k, m, p)   X( k)

Proof of Theorem fourierdlem109

Step	Hyp	Ref	Expression
1		fourierdlem109.a	. . . 4 |- ( ph -> A e. RR )
2	1	adantr 472	. . 3 |- ( ( ph /\ 0 < X ) -> A e. RR )
3		fourierdlem109.b	. . . 4 |- ( ph -> B e. RR )
4	3	adantr 472	. . 3 |- ( ( ph /\ 0 < X ) -> B e. RR )
5		fourierdlem109.t	. . 3 |- T = ( B - A )
6		fourierdlem109.x	. . . . 5 |- ( ph -> X e. RR )
7	6	adantr 472	. . . 4 |- ( ( ph /\ 0 < X ) -> X e. RR )
8		simpr 468	. . . 4 |- ( ( ph /\ 0 < X ) -> 0 < X )
9	7, 8	elrpd 11361	. . 3 |- ( ( ph /\ 0 < X ) -> X e. RR+ )
10		fourierdlem109.p	. . 3 |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
11		fourierdlem109.m	. . . 4 |- ( ph -> M e. NN )
12	11	adantr 472	. . 3 |- ( ( ph /\ 0 < X ) -> M e. NN )
13		fourierdlem109.q	. . . 4 |- ( ph -> Q e. ( P ` M ) )
14	13	adantr 472	. . 3 |- ( ( ph /\ 0 < X ) -> Q e. ( P ` M ) )
15		fourierdlem109.f	. . . 4 |- ( ph -> F : RR --> CC )
16	15	adantr 472	. . 3 |- ( ( ph /\ 0 < X ) -> F : RR --> CC )
17		fourierdlem109.fper	. . . 4 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
18	17	adantlr 729	. . 3 |- ( ( ( ph /\ 0 < X ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
19		fourierdlem109.fcn	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
20	19	adantlr 729	. . 3 |- ( ( ( ph /\ 0 < X ) /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
21		fourierdlem109.r	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
22	21	adantlr 729	. . 3 |- ( ( ( ph /\ 0 < X ) /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
23		fourierdlem109.l	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
24	23	adantlr 729	. . 3 |- ( ( ( ph /\ 0 < X ) /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
25	2, 4, 5, 9, 10, 12, 14, 16, 18, 20, 22, 24	fourierdlem108 38190	. 2 |- ( ( ph /\ 0 < X ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
26		oveq2 6316	. . . . . . 7 |- ( X = 0 -> ( A - X ) = ( A - 0 ) )
27	1	recnd 9687	. . . . . . . 8 |- ( ph -> A e. CC )
28	27	subid1d 9994	. . . . . . 7 |- ( ph -> ( A - 0 ) = A )
29	26, 28	sylan9eqr 2527	. . . . . 6 |- ( ( ph /\ X = 0 ) -> ( A - X ) = A )
30		oveq2 6316	. . . . . . 7 |- ( X = 0 -> ( B - X ) = ( B - 0 ) )
31	3	recnd 9687	. . . . . . . 8 |- ( ph -> B e. CC )
32	31	subid1d 9994	. . . . . . 7 |- ( ph -> ( B - 0 ) = B )
33	30, 32	sylan9eqr 2527	. . . . . 6 |- ( ( ph /\ X = 0 ) -> ( B - X ) = B )
34	29, 33	oveq12d 6326	. . . . 5 |- ( ( ph /\ X = 0 ) -> ( ( A - X ) [,] ( B - X ) ) = ( A [,] B ) )
35	34	itgeq1d 37930	. . . 4 |- ( ( ph /\ X = 0 ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
36	35	adantlr 729	. . 3 |- ( ( ( ph /\ -. 0 < X ) /\ X = 0 ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
37		simpll 768	. . . 4 |- ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> ph )
38	37, 6	syl 17	. . . . 5 |- ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> X e. RR )
39		0red 9662	. . . . 5 |- ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> 0 e. RR )
40		simpr 468	. . . . . 6 |- ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> -. X = 0 )
41	40	neqned 2650	. . . . 5 |- ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> X =/= 0 )
42		simplr 770	. . . . 5 |- ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> -. 0 < X )
43	38, 39, 41, 42	lttri5d 37605	. . . 4 |- ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> X < 0 )
44	6	recnd 9687	. . . . . . . . . . . 12 |- ( ph -> X e. CC )
45	27, 44	subcld 10005	. . . . . . . . . . 11 |- ( ph -> ( A - X ) e. CC )
46	45, 44	subnegd 10012	. . . . . . . . . 10 |- ( ph -> ( ( A - X ) - -u X ) = ( ( A - X ) + X ) )
47	27, 44	npcand 10009	. . . . . . . . . 10 |- ( ph -> ( ( A - X ) + X ) = A )
48	46, 47	eqtrd 2505	. . . . . . . . 9 |- ( ph -> ( ( A - X ) - -u X ) = A )
49	31, 44	subcld 10005	. . . . . . . . . . 11 |- ( ph -> ( B - X ) e. CC )
50	49, 44	subnegd 10012	. . . . . . . . . 10 |- ( ph -> ( ( B - X ) - -u X ) = ( ( B - X ) + X ) )
51	31, 44	npcand 10009	. . . . . . . . . 10 |- ( ph -> ( ( B - X ) + X ) = B )
52	50, 51	eqtrd 2505	. . . . . . . . 9 |- ( ph -> ( ( B - X ) - -u X ) = B )
53	48, 52	oveq12d 6326	. . . . . . . 8 |- ( ph -> ( ( ( A - X ) - -u X ) [,] ( ( B - X ) - -u X ) ) = ( A [,] B ) )
54	53	eqcomd 2477	. . . . . . 7 |- ( ph -> ( A [,] B ) = ( ( ( A - X ) - -u X ) [,] ( ( B - X ) - -u X ) ) )
55	54	itgeq1d 37930	. . . . . 6 |- ( ph -> S. ( A [,] B ) ( F ` x ) _d x = S. ( ( ( A - X ) - -u X ) [,] ( ( B - X ) - -u X ) ) ( F ` x ) _d x )
56	55	adantr 472	. . . . 5 |- ( ( ph /\ X < 0 ) -> S. ( A [,] B ) ( F ` x ) _d x = S. ( ( ( A - X ) - -u X ) [,] ( ( B - X ) - -u X ) ) ( F ` x ) _d x )
57	1, 6	resubcld 10068	. . . . . . 7 |- ( ph -> ( A - X ) e. RR )
58	57	adantr 472	. . . . . 6 |- ( ( ph /\ X < 0 ) -> ( A - X ) e. RR )
59	3, 6	resubcld 10068	. . . . . . 7 |- ( ph -> ( B - X ) e. RR )
60	59	adantr 472	. . . . . 6 |- ( ( ph /\ X < 0 ) -> ( B - X ) e. RR )
61		eqid 2471	. . . . . 6 |- ( ( B - X ) - ( A - X ) ) = ( ( B - X ) - ( A - X ) )
62	6	renegcld 10067	. . . . . . . 8 |- ( ph -> -u X e. RR )
63	62	adantr 472	. . . . . . 7 |- ( ( ph /\ X < 0 ) -> -u X e. RR )
64	6	lt0neg1d 10204	. . . . . . . 8 |- ( ph -> ( X < 0 <-> 0 < -u X ) )
65	64	biimpa 492	. . . . . . 7 |- ( ( ph /\ X < 0 ) -> 0 < -u X )
66	63, 65	elrpd 11361	. . . . . 6 |- ( ( ph /\ X < 0 ) -> -u X e. RR+ )
67		fourierdlem109.o	. . . . . . 7 |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
68		fveq2 5879	. . . . . . . . . . . . 13 |- ( i = j -> ( p ` i ) = ( p ` j ) )
69		oveq1 6315	. . . . . . . . . . . . . 14 |- ( i = j -> ( i + 1 ) = ( j + 1 ) )
70	69	fveq2d 5883	. . . . . . . . . . . . 13 |- ( i = j -> ( p ` ( i + 1 ) ) = ( p ` ( j + 1 ) ) )
71	68, 70	breq12d 4408	. . . . . . . . . . . 12 |- ( i = j -> ( ( p ` i ) < ( p ` ( i + 1 ) ) <-> ( p ` j ) < ( p ` ( j + 1 ) ) ) )
72	71	cbvralv 3005	. . . . . . . . . . 11 |- ( A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. j e. ( 0..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) )
73	72	anbi2i 708	. . . . . . . . . 10 |- ( ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) <-> ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. j e. ( 0..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) )
74	73	a1i 11	. . . . . . . . 9 |- ( p e. ( RR ^m ( 0 ... m ) ) -> ( ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) <-> ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. j e. ( 0..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) ) )
75	74	rabbiia 3019	. . . . . . . 8 |- { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } = { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. j e. ( 0..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) }
76	75	mpteq2i 4479	. . . . . . 7 |- ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. j e. ( 0..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) } )
77	67, 76	eqtri 2493	. . . . . 6 |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. j e. ( 0..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) } )
78	10, 11, 13	fourierdlem11 38092	. . . . . . . . . . . 12 |- ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
79	78	simp3d 1044	. . . . . . . . . . 11 |- ( ph -> A < B )
80	1, 3, 6, 79	ltsub1dd 10246	. . . . . . . . . 10 |- ( ph -> ( A - X ) < ( B - X ) )
81		fourierdlem109.h	. . . . . . . . . 10 |- H = ( { ( A - X ) , ( B - X ) } u. { x e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
82		fourierdlem109.n	. . . . . . . . . 10 |- N = ( ( # ` H ) - 1 )
83		fourierdlem109.16	. . . . . . . . . 10 |- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
84	5, 10, 11, 13, 57, 59, 80, 67, 81, 82, 83	fourierdlem54 38136	. . . . . . . . 9 |- ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , H ) ) )
85	84	simpld 466	. . . . . . . 8 |- ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
86	85	simpld 466	. . . . . . 7 |- ( ph -> N e. NN )
87	86	adantr 472	. . . . . 6 |- ( ( ph /\ X < 0 ) -> N e. NN )
88	85	simprd 470	. . . . . . 7 |- ( ph -> S e. ( O ` N ) )
89	88	adantr 472	. . . . . 6 |- ( ( ph /\ X < 0 ) -> S e. ( O ` N ) )
90	15	adantr 472	. . . . . 6 |- ( ( ph /\ X < 0 ) -> F : RR --> CC )
91	31, 27, 44	nnncan2d 10040	. . . . . . . . . . . 12 |- ( ph -> ( ( B - X ) - ( A - X ) ) = ( B - A ) )
92	91, 5	syl6eqr 2523	. . . . . . . . . . 11 |- ( ph -> ( ( B - X ) - ( A - X ) ) = T )
93	92	oveq2d 6324	. . . . . . . . . 10 |- ( ph -> ( x + ( ( B - X ) - ( A - X ) ) ) = ( x + T ) )
94	93	adantr 472	. . . . . . . . 9 |- ( ( ph /\ x e. RR ) -> ( x + ( ( B - X ) - ( A - X ) ) ) = ( x + T ) )
95	94	fveq2d 5883	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + ( ( B - X ) - ( A - X ) ) ) ) = ( F ` ( x + T ) ) )
96	95, 17	eqtrd 2505	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + ( ( B - X ) - ( A - X ) ) ) ) = ( F ` x ) )
97	96	adantlr 729	. . . . . 6 |- ( ( ( ph /\ X < 0 ) /\ x e. RR ) -> ( F ` ( x + ( ( B - X ) - ( A - X ) ) ) ) = ( F ` x ) )
98	11	adantr 472	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ N ) ) -> M e. NN )
99	13	adantr 472	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ N ) ) -> Q e. ( P ` M ) )
100	15	adantr 472	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ N ) ) -> F : RR --> CC )
101	17	adantlr 729	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
102	19	adantlr 729	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
103	57	adantr 472	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( A - X ) e. RR )
104	57	rexrd 9708	. . . . . . . . . 10 |- ( ph -> ( A - X ) e. RR* )
105		pnfxr 11435	. . . . . . . . . . 11 |- +oo e. RR*
106	105	a1i 11	. . . . . . . . . 10 |- ( ph -> +oo e. RR* )
107	59	ltpnfd 11446	. . . . . . . . . 10 |- ( ph -> ( B - X ) < +oo )
108	104, 106, 59, 80, 107	eliood 37691	. . . . . . . . 9 |- ( ph -> ( B - X ) e. ( ( A - X ) (,) +oo ) )
109	108	adantr 472	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( B - X ) e. ( ( A - X ) (,) +oo ) )
110		oveq1 6315	. . . . . . . . . . . . 13 |- ( x = y -> ( x + ( k x. T ) ) = ( y + ( k x. T ) ) )
111	110	eleq1d 2533	. . . . . . . . . . . 12 |- ( x = y -> ( ( x + ( k x. T ) ) e. ran Q <-> ( y + ( k x. T ) ) e. ran Q ) )
112	111	rexbidv 2892	. . . . . . . . . . 11 |- ( x = y -> ( E. k e. ZZ ( x + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. T ) ) e. ran Q ) )
113	112	cbvrabv 3030	. . . . . . . . . 10 |- { x e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } = { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q }
114	113	uneq2i 3576	. . . . . . . . 9 |- ( { ( A - X ) , ( B - X ) } u. { x e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) = ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
115	81, 114	eqtri 2493	. . . . . . . 8 |- H = ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
116		fourierdlem109.17	. . . . . . . 8 |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
117		fourierdlem109.18	. . . . . . . 8 |- J = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
118		simpr 468	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ N ) ) -> j e. ( 0..^ N ) )
119		eqid 2471	. . . . . . . 8 |- ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) )
120		eqid 2471	. . . . . . . 8 |- ( F |` ( ( J ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) ) = ( F |` ( ( J ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) )
121		eqid 2471	. . . . . . . 8 |- ( y e. ( ( ( J ` ( E ` ( S ` j ) ) ) + ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) (,) ( ( E ` ( S ` ( j + 1 ) ) ) + ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) ) |-> ( ( F |` ( ( J ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) ) ` ( y - ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) ) ) = ( y e. ( ( ( J ` ( E ` ( S ` j ) ) ) + ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) (,) ( ( E ` ( S ` ( j + 1 ) ) ) + ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) ) |-> ( ( F |` ( ( J ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) ) ` ( y - ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) ) )
122		fourierdlem109.19	. . . . . . . . 9 |- I = ( x e. RR |-> sup ( { j e. ( 0..^ M ) | ( Q ` j ) <_ ( J ` ( E ` x ) ) } , RR , < ) )
123		fveq2 5879	. . . . . . . . . . . . 13 |- ( j = i -> ( Q ` j ) = ( Q ` i ) )
124	123	breq1d 4405	. . . . . . . . . . . 12 |- ( j = i -> ( ( Q ` j ) <_ ( J ` ( E ` x ) ) <-> ( Q ` i ) <_ ( J ` ( E ` x ) ) ) )
125	124	cbvrabv 3030	. . . . . . . . . . 11 |- { j e. ( 0..^ M ) | ( Q ` j ) <_ ( J ` ( E ` x ) ) } = { i e. ( 0..^ M ) | ( Q ` i ) <_ ( J ` ( E ` x ) ) }
126	125	supeq1i 7979	. . . . . . . . . 10 |- sup ( { j e. ( 0..^ M ) | ( Q ` j ) <_ ( J ` ( E ` x ) ) } , RR , < ) = sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( J ` ( E ` x ) ) } , RR , < )
127	126	mpteq2i 4479	. . . . . . . . 9 |- ( x e. RR |-> sup ( { j e. ( 0..^ M ) | ( Q ` j ) <_ ( J ` ( E ` x ) ) } , RR , < ) ) = ( x e. RR |-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( J ` ( E ` x ) ) } , RR , < ) )
128	122, 127	eqtri 2493	. . . . . . . 8 |- I = ( x e. RR |-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( J ` ( E ` x ) ) } , RR , < ) )
129	10, 5, 98, 99, 100, 101, 102, 103, 109, 67, 115, 82, 83, 116, 117, 118, 119, 120, 121, 128	fourierdlem90 38172	. . . . . . 7 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( F |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
130	129	adantlr 729	. . . . . 6 |- ( ( ( ph /\ X < 0 ) /\ j e. ( 0..^ N ) ) -> ( F |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
131	21	adantlr 729	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
132		eqid 2471	. . . . . . . 8 |- ( i e. ( 0..^ M ) |-> R ) = ( i e. ( 0..^ M ) |-> R )
133	10, 5, 98, 99, 100, 101, 102, 131, 103, 109, 67, 115, 82, 83, 116, 117, 118, 119, 128, 132	fourierdlem89 38171	. . . . . . 7 |- ( ( ph /\ j e. ( 0..^ N ) ) -> if ( ( J ` ( E ` ( S ` j ) ) ) = ( Q ` ( I ` ( S ` j ) ) ) , ( ( i e. ( 0..^ M ) |-> R ) ` ( I ` ( S ` j ) ) ) , ( F ` ( J ` ( E ` ( S ` j ) ) ) ) ) e. ( ( F |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` j ) ) )
134	133	adantlr 729	. . . . . 6 |- ( ( ( ph /\ X < 0 ) /\ j e. ( 0..^ N ) ) -> if ( ( J ` ( E ` ( S ` j ) ) ) = ( Q ` ( I ` ( S ` j ) ) ) , ( ( i e. ( 0..^ M ) |-> R ) ` ( I ` ( S ` j ) ) ) , ( F ` ( J ` ( E ` ( S ` j ) ) ) ) ) e. ( ( F |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` j ) ) )
135	23	adantlr 729	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
136		eqid 2471	. . . . . . . 8 |- ( i e. ( 0..^ M ) |-> L ) = ( i e. ( 0..^ M ) |-> L )
137	10, 5, 98, 99, 100, 101, 102, 135, 103, 109, 67, 115, 82, 83, 116, 117, 118, 119, 128, 136	fourierdlem91 38173	. . . . . . 7 |- ( ( ph /\ j e. ( 0..^ N ) ) -> if ( ( E ` ( S ` ( j + 1 ) ) ) = ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) , ( ( i e. ( 0..^ M ) |-> L ) ` ( I ` ( S ` j ) ) ) , ( F ` ( E ` ( S ` ( j + 1 ) ) ) ) ) e. ( ( F |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` ( j + 1 ) ) ) )
138	137	adantlr 729	. . . . . 6 |- ( ( ( ph /\ X < 0 ) /\ j e. ( 0..^ N ) ) -> if ( ( E ` ( S ` ( j + 1 ) ) ) = ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) , ( ( i e. ( 0..^ M ) |-> L ) ` ( I ` ( S ` j ) ) ) , ( F ` ( E ` ( S ` ( j + 1 ) ) ) ) ) e. ( ( F |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` ( j + 1 ) ) ) )
139	58, 60, 61, 66, 77, 87, 89, 90, 97, 130, 134, 138	fourierdlem108 38190	. . . . 5 |- ( ( ph /\ X < 0 ) -> S. ( ( ( A - X ) - -u X ) [,] ( ( B - X ) - -u X ) ) ( F ` x ) _d x = S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x )
140	56, 139	eqtr2d 2506	. . . 4 |- ( ( ph /\ X < 0 ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
141	37, 43, 140	syl2anc 673	. . 3 |- ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
142	36, 141	pm2.61dan 808	. 2 |- ( ( ph /\ -. 0 < X ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
143	25, 142	pm2.61dan 808	1 |- ( ph -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 376   = wceq 1452   e. wcel 1904   A.wral 2756   E.wrex 2757   {crab 2760   u. cun 3388   ifcif 3872   {cpr 3961   class class class wbr 4395   |-> cmpt 4454   ran crn 4840   |` cres 4841   iotacio 5551   -->wf 5585   ` cfv 5589   Isom wiso 5590  (class class class)co 6308   ^m cmap 7490   supcsup 7972   CCcc 9555   RRcr 9556   0cc0 9557   1c1 9558   + caddc 9560   x. cmul 9562   +oocpnf 9690   RR*cxr 9692   < clt 9693   <_ cle 9694   - cmin 9880   -ucneg 9881   / cdiv 10291   NNcn 10631   ZZcz 10961   (,)cioo 11660   (,]cioc 11661   [,]cicc 11663   ...cfz 11810  ..^cfzo 11942   |_cfl 12059   #chash 12553   -cn->ccncf 21986   S.citg 22655   lim CC climc 22896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cc 8883  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636  ax-mulf 9637

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-disj 4367  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-ofr 6551  df-om 6712  df-1st 6812  df-2nd 6813  df-supp 6934  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-omul 7205  df-er 7381  df-map 7492  df-pm 7493  df-ixp 7541  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fsupp 7902  df-fi 7943  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-acn 8394  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-4 10692  df-5 10693  df-6 10694  df-7 10695  df-8 10696  df-9 10697  df-10 10698  df-n0 10894  df-z 10962  df-dec 11075  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ioo 11664  df-ioc 11665  df-ico 11666  df-icc 11667  df-fz 11811  df-fzo 11943  df-fl 12061  df-mod 12130  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-limsup 13603  df-clim 13629  df-rlim 13630  df-sum 13830  df-struct 15201  df-ndx 15202  df-slot 15203  df-base 15204  df-sets 15205  df-ress 15206  df-plusg 15281  df-mulr 15282  df-starv 15283  df-sca 15284  df-vsca 15285  df-ip 15286  df-tset 15287  df-ple 15288  df-ds 15290  df-unif 15291  df-hom 15292  df-cco 15293  df-rest 15399  df-topn 15400  df-0g 15418  df-gsum 15419  df-topgen 15420  df-pt 15421  df-prds 15424  df-xrs 15478  df-qtop 15484  df-imas 15485  df-xps 15488  df-mre 15570  df-mrc 15571  df-acs 15573  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-submnd 16661  df-mulg 16754  df-cntz 17049  df-cmn 17510  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-fbas 19044  df-fg 19045  df-cnfld 19048  df-top 19998  df-bases 19999  df-topon 20000  df-topsp 20001  df-cld 20111  df-ntr 20112  df-cls 20113  df-nei 20191  df-lp 20229  df-perf 20230  df-cn 20320  df-cnp 20321  df-haus 20408  df-cmp 20479  df-tx 20654  df-hmeo 20847  df-fil 20939  df-fm 21031  df-flim 21032  df-flf 21033  df-xms 21413  df-ms 21414  df-tms 21415  df-cncf 21988  df-ovol 22494  df-vol 22496  df-mbf 22656  df-itg1 22657  df-itg2 22658  df-ibl 22659  df-itg 22660  df-0p 22707  df-ditg 22881  df-limc 22900  df-dv 22901

This theorem is referenced by:  fourierdlem110  38192