Theorem fourierdlem63 31793

Description: The upper bound of intervals in the moved partition are mapped to points that are not greater than the corresponding upper bounds in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem63.t	|- T = ( B - A )
fourierdlem63.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 ) ) ) } )
fourierdlem63.m	|- ( ph -> M e. NN )
fourierdlem63.q	|- ( ph -> Q e. ( P ` M ) )
fourierdlem63.c	|- ( ph -> C e. RR )
fourierdlem63.d	|- ( ph -> D e. RR )
fourierdlem63.cltd	|- ( ph -> C < D )
fourierdlem63.o	|- O = ( 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 ) ) ) } )
fourierdlem63.h	|- H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
fourierdlem63.n	|- N = ( ( # ` H ) - 1 )
fourierdlem63.s	|- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
fourierdlem63.e	|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
fourierdlem63.k	|- ( ph -> K e. ( 0 ... M ) )
fourierdlem63.j	|- ( ph -> J e. ( 0..^ N ) )
fourierdlem63.y	|- ( ph -> Y e. ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) )
fourierdlem63.eyltqk	|- ( ph -> ( E ` Y ) < ( Q ` K ) )
fourierdlem63.x	|- X = ( ( Q ` K ) - ( ( E ` Y ) - Y ) )

Assertion

Ref	Expression
fourierdlem63	|- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` K ) )

Distinct variable groups:   A, i, m, p   x, A, i   B, i, m, p   x, B   C, i, m, p   x, C   D, i, m, p   x, D   k, E, x   f, H   x, H   k, J, x   k, K, x   i, M, m, p   f, N   i, N, m, p   x, N   Q, i, k, x   Q, p   S, f   S, i, k, x   S, p   T, i, k, x   k, Y, x   ph, f   ph, i, k, x

Allowed substitution hints:   ph( m, p)   A( f, k)   B( f, k)   C( f, k)   D( f, k)   P( x, f, i, k, m, p)   Q( f, m)   S( m)   T( f, m, p)   E( f, i, m, p)   H( i, k, m, p)   J( f, i, m, p)   K( f, i, m, p)   M( x, f, k)   N( k)   O( x, f, i, k, m, p)   X( x, f, i, k, m, p)   Y( f, i, m, p)

Proof of Theorem fourierdlem63

Dummy variable j is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem63.c	. . . . . . . . 9 |- ( ph -> C e. RR )
2	1	adantr 465	. . . . . . . 8 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> C e. RR )
3		fourierdlem63.d	. . . . . . . . 9 |- ( ph -> D e. RR )
4	3	adantr 465	. . . . . . . 8 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> D e. RR )
5		fourierdlem63.q	. . . . . . . . . . . . . 14 |- ( ph -> Q e. ( P ` M ) )
6		fourierdlem63.m	. . . . . . . . . . . . . . 15 |- ( ph -> M e. NN )
7		fourierdlem63.p	. . . . . . . . . . . . . . . 16 |- 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 ) ) ) } )
8	7	fourierdlem2 31732	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) ) )
9	6, 8	syl 16	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) ) ) )
10	5, 9	mpbid 210	. . . . . . . . . . . . 13 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
11	10	simpld 459	. . . . . . . . . . . 12 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
12		elmapi 7452	. . . . . . . . . . . 12 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
13	11, 12	syl 16	. . . . . . . . . . 11 |- ( ph -> Q : ( 0 ... M ) --> RR )
14		fourierdlem63.k	. . . . . . . . . . 11 |- ( ph -> K e. ( 0 ... M ) )
15	13, 14	ffvelrnd 6033	. . . . . . . . . 10 |- ( ph -> ( Q ` K ) e. RR )
16	7, 6, 5	fourierdlem11 31741	. . . . . . . . . . . . . . 15 |- ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
17	16	simp1d 1008	. . . . . . . . . . . . . 14 |- ( ph -> A e. RR )
18	17	rexrd 9655	. . . . . . . . . . . . 13 |- ( ph -> A e. RR* )
19	16	simp2d 1009	. . . . . . . . . . . . 13 |- ( ph -> B e. RR )
20		iocssre 11616	. . . . . . . . . . . . 13 |- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
21	18, 19, 20	syl2anc 661	. . . . . . . . . . . 12 |- ( ph -> ( A (,] B ) C_ RR )
22	16	simp3d 1010	. . . . . . . . . . . . . 14 |- ( ph -> A < B )
23		fourierdlem63.t	. . . . . . . . . . . . . 14 |- T = ( B - A )
24		fourierdlem63.e	. . . . . . . . . . . . . 14 |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
25	17, 19, 22, 23, 24	fourierdlem4 31734	. . . . . . . . . . . . 13 |- ( ph -> E : RR --> ( A (,] B ) )
26		fourierdlem63.y	. . . . . . . . . . . . . . 15 |- ( ph -> Y e. ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) )
27		fourierdlem63.cltd	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> C < D )
28		fourierdlem63.o	. . . . . . . . . . . . . . . . . . . . . . 23 |- O = ( 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 ) ) ) } )
29		fourierdlem63.h	. . . . . . . . . . . . . . . . . . . . . . 23 |- H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
30		fourierdlem63.n	. . . . . . . . . . . . . . . . . . . . . . 23 |- N = ( ( # ` H ) - 1 )
31		fourierdlem63.s	. . . . . . . . . . . . . . . . . . . . . . 23 |- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
32	23, 7, 6, 5, 1, 3, 27, 28, 29, 30, 31	fourierdlem54 31784	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , H ) ) )
33	32	simpld 459	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
34	33	simprd 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> S e. ( O ` N ) )
35	33	simpld 459	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> N e. NN )
36	28	fourierdlem2 31732	. . . . . . . . . . . . . . . . . . . . 21 |- ( N e. NN -> ( S e. ( O ` N ) <-> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) )
37	35, 36	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( S e. ( O ` N ) <-> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) )
38	34, 37	mpbid 210	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) )
39	38	simpld 459	. . . . . . . . . . . . . . . . . 18 |- ( ph -> S e. ( RR ^m ( 0 ... N ) ) )
40		elmapi 7452	. . . . . . . . . . . . . . . . . 18 |- ( S e. ( RR ^m ( 0 ... N ) ) -> S : ( 0 ... N ) --> RR )
41	39, 40	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> S : ( 0 ... N ) --> RR )
42		fourierdlem63.j	. . . . . . . . . . . . . . . . . 18 |- ( ph -> J e. ( 0..^ N ) )
43		elfzofz 11823	. . . . . . . . . . . . . . . . . 18 |- ( J e. ( 0..^ N ) -> J e. ( 0 ... N ) )
44	42, 43	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> J e. ( 0 ... N ) )
45	41, 44	ffvelrnd 6033	. . . . . . . . . . . . . . . 16 |- ( ph -> ( S ` J ) e. RR )
46		fzofzp1 11889	. . . . . . . . . . . . . . . . . . 19 |- ( J e. ( 0..^ N ) -> ( J + 1 ) e. ( 0 ... N ) )
47	42, 46	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( J + 1 ) e. ( 0 ... N ) )
48	41, 47	ffvelrnd 6033	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( S ` ( J + 1 ) ) e. RR )
49	48	rexrd 9655	. . . . . . . . . . . . . . . 16 |- ( ph -> ( S ` ( J + 1 ) ) e. RR* )
50		elico2 11600	. . . . . . . . . . . . . . . 16 |- ( ( ( S ` J ) e. RR /\ ( S ` ( J + 1 ) ) e. RR* ) -> ( Y e. ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) <-> ( Y e. RR /\ ( S ` J ) <_ Y /\ Y < ( S ` ( J + 1 ) ) ) ) )
51	45, 49, 50	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ph -> ( Y e. ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) <-> ( Y e. RR /\ ( S ` J ) <_ Y /\ Y < ( S ` ( J + 1 ) ) ) ) )
52	26, 51	mpbid 210	. . . . . . . . . . . . . 14 |- ( ph -> ( Y e. RR /\ ( S ` J ) <_ Y /\ Y < ( S ` ( J + 1 ) ) ) )
53	52	simp1d 1008	. . . . . . . . . . . . 13 |- ( ph -> Y e. RR )
54	25, 53	ffvelrnd 6033	. . . . . . . . . . . 12 |- ( ph -> ( E ` Y ) e. ( A (,] B ) )
55	21, 54	sseldd 3510	. . . . . . . . . . 11 |- ( ph -> ( E ` Y ) e. RR )
56	55, 53	resubcld 9999	. . . . . . . . . 10 |- ( ph -> ( ( E ` Y ) - Y ) e. RR )
57	15, 56	resubcld 9999	. . . . . . . . 9 |- ( ph -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. RR )
58	57	adantr 465	. . . . . . . 8 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. RR )
59		icossicc 11623	. . . . . . . . . . . . . . . 16 |- ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) C_ ( ( S ` J ) [,] ( S ` ( J + 1 ) ) )
60	59	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) C_ ( ( S ` J ) [,] ( S ` ( J + 1 ) ) ) )
61	1	rexrd 9655	. . . . . . . . . . . . . . . 16 |- ( ph -> C e. RR* )
62	3	rexrd 9655	. . . . . . . . . . . . . . . 16 |- ( ph -> D e. RR* )
63	28, 35, 34	fourierdlem15 31745	. . . . . . . . . . . . . . . 16 |- ( ph -> S : ( 0 ... N ) --> ( C [,] D ) )
64	61, 62, 63, 42	fourierdlem8 31738	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( S ` J ) [,] ( S ` ( J + 1 ) ) ) C_ ( C [,] D ) )
65	60, 64	sstrd 3519	. . . . . . . . . . . . . 14 |- ( ph -> ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) C_ ( C [,] D ) )
66	65, 26	sseldd 3510	. . . . . . . . . . . . 13 |- ( ph -> Y e. ( C [,] D ) )
67		elicc2 11601	. . . . . . . . . . . . . 14 |- ( ( C e. RR /\ D e. RR ) -> ( Y e. ( C [,] D ) <-> ( Y e. RR /\ C <_ Y /\ Y <_ D ) ) )
68	1, 3, 67	syl2anc 661	. . . . . . . . . . . . 13 |- ( ph -> ( Y e. ( C [,] D ) <-> ( Y e. RR /\ C <_ Y /\ Y <_ D ) ) )
69	66, 68	mpbid 210	. . . . . . . . . . . 12 |- ( ph -> ( Y e. RR /\ C <_ Y /\ Y <_ D ) )
70	69	simp2d 1009	. . . . . . . . . . 11 |- ( ph -> C <_ Y )
71	15, 55	resubcld 9999	. . . . . . . . . . . . . 14 |- ( ph -> ( ( Q ` K ) - ( E ` Y ) ) e. RR )
72		fourierdlem63.eyltqk	. . . . . . . . . . . . . . 15 |- ( ph -> ( E ` Y ) < ( Q ` K ) )
73	55, 15	posdifd 10151	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( E ` Y ) < ( Q ` K ) <-> 0 < ( ( Q ` K ) - ( E ` Y ) ) ) )
74	72, 73	mpbid 210	. . . . . . . . . . . . . 14 |- ( ph -> 0 < ( ( Q ` K ) - ( E ` Y ) ) )
75	71, 74	elrpd 11266	. . . . . . . . . . . . 13 |- ( ph -> ( ( Q ` K ) - ( E ` Y ) ) e. RR+ )
76		ltaddrp 11264	. . . . . . . . . . . . 13 |- ( ( Y e. RR /\ ( ( Q ` K ) - ( E ` Y ) ) e. RR+ ) -> Y < ( Y + ( ( Q ` K ) - ( E ` Y ) ) ) )
77	53, 75, 76	syl2anc 661	. . . . . . . . . . . 12 |- ( ph -> Y < ( Y + ( ( Q ` K ) - ( E ` Y ) ) ) )
78	15	recnd 9634	. . . . . . . . . . . . . 14 |- ( ph -> ( Q ` K ) e. CC )
79	55	recnd 9634	. . . . . . . . . . . . . 14 |- ( ph -> ( E ` Y ) e. CC )
80	53	recnd 9634	. . . . . . . . . . . . . 14 |- ( ph -> Y e. CC )
81	78, 79, 80	subsub3d 9972	. . . . . . . . . . . . 13 |- ( ph -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) = ( ( ( Q ` K ) + Y ) - ( E ` Y ) ) )
82	78, 80	addcomd 9793	. . . . . . . . . . . . . 14 |- ( ph -> ( ( Q ` K ) + Y ) = ( Y + ( Q ` K ) ) )
83	82	oveq1d 6310	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( Q ` K ) + Y ) - ( E ` Y ) ) = ( ( Y + ( Q ` K ) ) - ( E ` Y ) ) )
84	80, 78, 79	addsubassd 9962	. . . . . . . . . . . . 13 |- ( ph -> ( ( Y + ( Q ` K ) ) - ( E ` Y ) ) = ( Y + ( ( Q ` K ) - ( E ` Y ) ) ) )
85	81, 83, 84	3eqtrrd 2513	. . . . . . . . . . . 12 |- ( ph -> ( Y + ( ( Q ` K ) - ( E ` Y ) ) ) = ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) )
86	77, 85	breqtrd 4477	. . . . . . . . . . 11 |- ( ph -> Y < ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) )
87	1, 53, 57, 70, 86	lelttrd 9751	. . . . . . . . . 10 |- ( ph -> C < ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) )
88	1, 57, 87	ltled 9744	. . . . . . . . 9 |- ( ph -> C <_ ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) )
89	88	adantr 465	. . . . . . . 8 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> C <_ ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) )
90	48	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( S ` ( J + 1 ) ) e. RR )
91	15	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( Q ` K ) e. RR )
92	24	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
93		id 22	. . . . . . . . . . . . . . . . . 18 |- ( x = ( S ` ( J + 1 ) ) -> x = ( S ` ( J + 1 ) ) )
94		oveq2 6303	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( S ` ( J + 1 ) ) -> ( B - x ) = ( B - ( S ` ( J + 1 ) ) ) )
95	94	oveq1d 6310	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( S ` ( J + 1 ) ) -> ( ( B - x ) / T ) = ( ( B - ( S ` ( J + 1 ) ) ) / T ) )
96	95	fveq2d 5876	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( S ` ( J + 1 ) ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
97	96	oveq1d 6310	. . . . . . . . . . . . . . . . . 18 |- ( x = ( S ` ( J + 1 ) ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
98	93, 97	oveq12d 6313	. . . . . . . . . . . . . . . . 17 |- ( x = ( S ` ( J + 1 ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
99	98	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x = ( S ` ( J + 1 ) ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
100	19, 48	resubcld 9999	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( B - ( S ` ( J + 1 ) ) ) e. RR )
101	23	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> T = ( B - A ) )
102	19, 17	resubcld 9999	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( B - A ) e. RR )
103	101, 102	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> T e. RR )
104		0re 9608	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. RR
105	104	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> 0 e. RR )
106	17, 19	posdifd 10151	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
107	22, 106	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> 0 < ( B - A ) )
108	101	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( B - A ) = T )
109	107, 108	breqtrd 4477	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> 0 < T )
110	105, 109	gtned 9731	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> T =/= 0 )
111	100, 103, 110	redivcld 10384	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( B - ( S ` ( J + 1 ) ) ) / T ) e. RR )
112	111	flcld 11915	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. ZZ )
113	112	zred 10978	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. RR )
114	113, 103	remulcld 9636	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. RR )
115	48, 114	readdcld 9635	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) e. RR )
116	92, 99, 48, 115	fvmptd 5962	. . . . . . . . . . . . . . 15 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
117	116, 115	eqeltrd 2555	. . . . . . . . . . . . . 14 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. RR )
118	117, 48	resubcld 9999	. . . . . . . . . . . . 13 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) e. RR )
119	118	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) e. RR )
120	91, 119	resubcld 9999	. . . . . . . . . . 11 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) e. RR )
121	52	simp3d 1010	. . . . . . . . . . . . . . 15 |- ( ph -> Y < ( S ` ( J + 1 ) ) )
122	53, 48, 121	ltled 9744	. . . . . . . . . . . . . 14 |- ( ph -> Y <_ ( S ` ( J + 1 ) ) )
123	17, 19, 22, 23, 24, 53, 48, 122	fourierdlem7 31737	. . . . . . . . . . . . 13 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) <_ ( ( E ` Y ) - Y ) )
124	118, 56, 15	lesub2d 10172	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) <_ ( ( E ` Y ) - Y ) <-> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) <_ ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) ) )
125	123, 124	mpbid 210	. . . . . . . . . . . 12 |- ( ph -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) <_ ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) )
126	125	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) <_ ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) )
127	78	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( Q ` K ) e. CC )
128	117	recnd 9634	. . . . . . . . . . . . . . 15 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. CC )
129	128	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) e. CC )
130	90	recnd 9634	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( S ` ( J + 1 ) ) e. CC )
131	127, 129, 130	subsubd 9970	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) = ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) + ( S ` ( J + 1 ) ) ) )
132	78, 128	subcld 9942	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. CC )
133	48	recnd 9634	. . . . . . . . . . . . . . 15 |- ( ph -> ( S ` ( J + 1 ) ) e. CC )
134	132, 133	addcomd 9793	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) + ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
135	134	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) + ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
136	131, 135	eqtrd 2508	. . . . . . . . . . . 12 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
137		simpr 461	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) )
138	117	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) e. RR )
139	91, 138	sublt0d 31395	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) < 0 <-> ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) )
140	137, 139	mpbird 232	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) < 0 )
141	91, 138	resubcld 9999	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. RR )
142		ltaddneg 31384	. . . . . . . . . . . . . 14 |- ( ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. RR /\ ( S ` ( J + 1 ) ) e. RR ) -> ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) < 0 <-> ( ( S ` ( J + 1 ) ) + ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) < ( S ` ( J + 1 ) ) ) )
143	141, 90, 142	syl2anc 661	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) < 0 <-> ( ( S ` ( J + 1 ) ) + ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) < ( S ` ( J + 1 ) ) ) )
144	140, 143	mpbid 210	. . . . . . . . . . . 12 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( S ` ( J + 1 ) ) + ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) < ( S ` ( J + 1 ) ) )
145	136, 144	eqbrtrd 4473	. . . . . . . . . . 11 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) < ( S ` ( J + 1 ) ) )
146	58, 120, 90, 126, 145	lelttrd 9751	. . . . . . . . . 10 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) < ( S ` ( J + 1 ) ) )
147	63, 47	ffvelrnd 6033	. . . . . . . . . . . . 13 |- ( ph -> ( S ` ( J + 1 ) ) e. ( C [,] D ) )
148		elicc2 11601	. . . . . . . . . . . . . 14 |- ( ( C e. RR /\ D e. RR ) -> ( ( S ` ( J + 1 ) ) e. ( C [,] D ) <-> ( ( S ` ( J + 1 ) ) e. RR /\ C <_ ( S ` ( J + 1 ) ) /\ ( S ` ( J + 1 ) ) <_ D ) ) )
149	1, 3, 148	syl2anc 661	. . . . . . . . . . . . 13 |- ( ph -> ( ( S ` ( J + 1 ) ) e. ( C [,] D ) <-> ( ( S ` ( J + 1 ) ) e. RR /\ C <_ ( S ` ( J + 1 ) ) /\ ( S ` ( J + 1 ) ) <_ D ) ) )
150	147, 149	mpbid 210	. . . . . . . . . . . 12 |- ( ph -> ( ( S ` ( J + 1 ) ) e. RR /\ C <_ ( S ` ( J + 1 ) ) /\ ( S ` ( J + 1 ) ) <_ D ) )
151	150	simp3d 1010	. . . . . . . . . . 11 |- ( ph -> ( S ` ( J + 1 ) ) <_ D )
152	151	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( S ` ( J + 1 ) ) <_ D )
153	58, 90, 4, 146, 152	ltletrd 9753	. . . . . . . . 9 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) < D )
154	58, 4, 153	ltled 9744	. . . . . . . 8 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) <_ D )
155	2, 4, 58, 89, 154	eliccd 31425	. . . . . . 7 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. ( C [,] D ) )
156		id 22	. . . . . . . . . . . . . . . 16 |- ( x = Y -> x = Y )
157		oveq2 6303	. . . . . . . . . . . . . . . . . . 19 |- ( x = Y -> ( B - x ) = ( B - Y ) )
158	157	oveq1d 6310	. . . . . . . . . . . . . . . . . 18 |- ( x = Y -> ( ( B - x ) / T ) = ( ( B - Y ) / T ) )
159	158	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( x = Y -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - Y ) / T ) ) )
160	159	oveq1d 6310	. . . . . . . . . . . . . . . 16 |- ( x = Y -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) )
161	156, 160	oveq12d 6313	. . . . . . . . . . . . . . 15 |- ( x = Y -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) )
162	161	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ x = Y ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) )
163	19, 53	resubcld 9999	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( B - Y ) e. RR )
164	163, 103, 110	redivcld 10384	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( B - Y ) / T ) e. RR )
165	164	flcld 11915	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( |_ ` ( ( B - Y ) / T ) ) e. ZZ )
166	165	zred 10978	. . . . . . . . . . . . . . . 16 |- ( ph -> ( |_ ` ( ( B - Y ) / T ) ) e. RR )
167	166, 103	remulcld 9636	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) e. RR )
168	53, 167	readdcld 9635	. . . . . . . . . . . . . 14 |- ( ph -> ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) e. RR )
169	92, 162, 53, 168	fvmptd 5962	. . . . . . . . . . . . 13 |- ( ph -> ( E ` Y ) = ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) )
170	169	oveq1d 6310	. . . . . . . . . . . 12 |- ( ph -> ( ( E ` Y ) - Y ) = ( ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) - Y ) )
171	170	oveq1d 6310	. . . . . . . . . . 11 |- ( ph -> ( ( ( E ` Y ) - Y ) / T ) = ( ( ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) - Y ) / T ) )
172	167	recnd 9634	. . . . . . . . . . . . 13 |- ( ph -> ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) e. CC )
173	80, 172	pncan2d 9944	. . . . . . . . . . . 12 |- ( ph -> ( ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) - Y ) = ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) )
174	173	oveq1d 6310	. . . . . . . . . . 11 |- ( ph -> ( ( ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) - Y ) / T ) = ( ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) / T ) )
175	166	recnd 9634	. . . . . . . . . . . 12 |- ( ph -> ( |_ ` ( ( B - Y ) / T ) ) e. CC )
176	103	recnd 9634	. . . . . . . . . . . 12 |- ( ph -> T e. CC )
177	175, 176, 110	divcan4d 10338	. . . . . . . . . . 11 |- ( ph -> ( ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) / T ) = ( |_ ` ( ( B - Y ) / T ) ) )
178	171, 174, 177	3eqtrd 2512	. . . . . . . . . 10 |- ( ph -> ( ( ( E ` Y ) - Y ) / T ) = ( |_ ` ( ( B - Y ) / T ) ) )
179	178, 165	eqeltrd 2555	. . . . . . . . 9 |- ( ph -> ( ( ( E ` Y ) - Y ) / T ) e. ZZ )
180	56	recnd 9634	. . . . . . . . . . . . 13 |- ( ph -> ( ( E ` Y ) - Y ) e. CC )
181	180, 176, 110	divcan1d 10333	. . . . . . . . . . . 12 |- ( ph -> ( ( ( ( E ` Y ) - Y ) / T ) x. T ) = ( ( E ` Y ) - Y ) )
182	181	oveq2d 6311	. . . . . . . . . . 11 |- ( ph -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) = ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( E ` Y ) - Y ) ) )
183	78, 180	npcand 9946	. . . . . . . . . . 11 |- ( ph -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( E ` Y ) - Y ) ) = ( Q ` K ) )
184	182, 183	eqtrd 2508	. . . . . . . . . 10 |- ( ph -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) = ( Q ` K ) )
185		ffun 5739	. . . . . . . . . . . 12 |- ( Q : ( 0 ... M ) --> RR -> Fun Q )
186	13, 185	syl 16	. . . . . . . . . . 11 |- ( ph -> Fun Q )
187		fdm 5741	. . . . . . . . . . . . . 14 |- ( Q : ( 0 ... M ) --> RR -> dom Q = ( 0 ... M ) )
188	13, 187	syl 16	. . . . . . . . . . . . 13 |- ( ph -> dom Q = ( 0 ... M ) )
189	188	eqcomd 2475	. . . . . . . . . . . 12 |- ( ph -> ( 0 ... M ) = dom Q )
190	14, 189	eleqtrd 2557	. . . . . . . . . . 11 |- ( ph -> K e. dom Q )
191		fvelrn 6025	. . . . . . . . . . 11 |- ( ( Fun Q /\ K e. dom Q ) -> ( Q ` K ) e. ran Q )
192	186, 190, 191	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( Q ` K ) e. ran Q )
193	184, 192	eqeltrd 2555	. . . . . . . . 9 |- ( ph -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) e. ran Q )
194		oveq1 6302	. . . . . . . . . . . 12 |- ( k = ( ( ( E ` Y ) - Y ) / T ) -> ( k x. T ) = ( ( ( ( E ` Y ) - Y ) / T ) x. T ) )
195	194	oveq2d 6311	. . . . . . . . . . 11 |- ( k = ( ( ( E ` Y ) - Y ) / T ) -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) = ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) )
196	195	eleq1d 2536	. . . . . . . . . 10 |- ( k = ( ( ( E ` Y ) - Y ) / T ) -> ( ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q <-> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) e. ran Q ) )
197	196	rspcev 3219	. . . . . . . . 9 |- ( ( ( ( ( E ` Y ) - Y ) / T ) e. ZZ /\ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) e. ran Q ) -> E. k e. ZZ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q )
198	179, 193, 197	syl2anc 661	. . . . . . . 8 |- ( ph -> E. k e. ZZ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q )
199	198	adantr 465	. . . . . . 7 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> E. k e. ZZ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q )
200	155, 199	jca 532	. . . . . 6 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. ( C [,] D ) /\ E. k e. ZZ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q ) )
201		oveq1 6302	. . . . . . . . 9 |- ( x = ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) -> ( x + ( k x. T ) ) = ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) )
202	201	eleq1d 2536	. . . . . . . 8 |- ( x = ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) -> ( ( x + ( k x. T ) ) e. ran Q <-> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q ) )
203	202	rexbidv 2978	. . . . . . 7 |- ( x = ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) -> ( E. k e. ZZ ( x + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q ) )
204	203	elrab 3266	. . . . . 6 |- ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } <-> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. ( C [,] D ) /\ E. k e. ZZ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q ) )
205	200, 204	sylibr 212	. . . . 5 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
206		elun2 3677	. . . . 5 |- ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) )
207	205, 206	syl 16	. . . 4 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) )
208		fourierdlem63.x	. . . . . 6 |- X = ( ( Q ` K ) - ( ( E ` Y ) - Y ) )
209	208	a1i 11	. . . . 5 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> X = ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) )
210	29	a1i 11	. . . . 5 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) )
211	209, 210	eleq12d 2549	. . . 4 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( X e. H <-> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) ) )
212	207, 211	mpbird 232	. . 3 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> X e. H )
213	32	simprd 463	. . . . . . . . . 10 |- ( ph -> S Isom < , < ( ( 0 ... N ) , H ) )
214		isof1o 6220	. . . . . . . . . 10 |- ( S Isom < , < ( ( 0 ... N ) , H ) -> S : ( 0 ... N ) -1-1-onto-> H )
215	213, 214	syl 16	. . . . . . . . 9 |- ( ph -> S : ( 0 ... N ) -1-1-onto-> H )
216		f1ofo 5829	. . . . . . . . 9 |- ( S : ( 0 ... N ) -1-1-onto-> H -> S : ( 0 ... N ) -onto-> H )
217	215, 216	syl 16	. . . . . . . 8 |- ( ph -> S : ( 0 ... N ) -onto-> H )
218	217	adantr 465	. . . . . . 7 |- ( ( ph /\ X e. H ) -> S : ( 0 ... N ) -onto-> H )
219		simpr 461	. . . . . . 7 |- ( ( ph /\ X e. H ) -> X e. H )
220		foelrn 6051	. . . . . . 7 |- ( ( S : ( 0 ... N ) -onto-> H /\ X e. H ) -> E. j e. ( 0 ... N ) X = ( S ` j ) )
221	218, 219, 220	syl2anc 661	. . . . . 6 |- ( ( ph /\ X e. H ) -> E. j e. ( 0 ... N ) X = ( S ` j ) )
222		eqcom 2476	. . . . . . . 8 |- ( X = ( S ` j ) <-> ( S ` j ) = X )
223	222	rexbii 2969	. . . . . . 7 |- ( E. j e. ( 0 ... N ) X = ( S ` j ) <-> E. j e. ( 0 ... N ) ( S ` j ) = X )
224	223	imbi2i 312	. . . . . 6 |- ( ( ( ph /\ X e. H ) -> E. j e. ( 0 ... N ) X = ( S ` j ) ) <-> ( ( ph /\ X e. H ) -> E. j e. ( 0 ... N ) ( S ` j ) = X ) )
225	221, 224	mpbi 208	. . . . 5 |- ( ( ph /\ X e. H ) -> E. j e. ( 0 ... N ) ( S ` j ) = X )
226	225	adantlr 714	. . . 4 |- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ X e. H ) -> E. j e. ( 0 ... N ) ( S ` j ) = X )
227	45	ad2antrr 725	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` J ) e. RR )
228	53	ad2antrr 725	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> Y e. RR )
229	41	ffvelrnda 6032	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( S ` j ) e. RR )
230	229	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` j ) e. RR )
231	52	simp2d 1009	. . . . . . . . . . . 12 |- ( ph -> ( S ` J ) <_ Y )
232	231	ad2antrr 725	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` J ) <_ Y )
233	208	eqcomi 2480	. . . . . . . . . . . . . . 15 |- ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) = X
234	86, 233	syl6breq 4492	. . . . . . . . . . . . . 14 |- ( ph -> Y < X )
235	234	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ ( S ` j ) = X ) -> Y < X )
236	222	biimpri 206	. . . . . . . . . . . . . 14 |- ( ( S ` j ) = X -> X = ( S ` j ) )
237	236	adantl 466	. . . . . . . . . . . . 13 |- ( ( ph /\ ( S ` j ) = X ) -> X = ( S ` j ) )
238	235, 237	breqtrd 4477	. . . . . . . . . . . 12 |- ( ( ph /\ ( S ` j ) = X ) -> Y < ( S ` j ) )
239	238	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> Y < ( S ` j ) )
240	227, 228, 230, 232, 239	lelttrd 9751	. . . . . . . . . 10 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` J ) < ( S ` j ) )
241	240	adantllr 718	. . . . . . . . 9 |- ( ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` J ) < ( S ` j ) )
242		simpr 461	. . . . . . . . . . 11 |- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ ( S ` j ) = X ) -> ( S ` j ) = X )
243	146	idi 2	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) < ( S ` ( J + 1 ) ) )
244	208, 243	syl5eqbr 4486	. . . . . . . . . . . 12 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> X < ( S ` ( J + 1 ) ) )
245	244	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ ( S ` j ) = X ) -> X < ( S ` ( J + 1 ) ) )
246	242, 245	eqbrtrd 4473	. . . . . . . . . 10 |- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ ( S ` j ) = X ) -> ( S ` j ) < ( S ` ( J + 1 ) ) )
247	246	adantlr 714	. . . . . . . . 9 |- ( ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` j ) < ( S ` ( J + 1 ) ) )
248	241, 247	jca 532	. . . . . . . 8 |- ( ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) )
249		elfzelz 11700	. . . . . . . . . . . 12 |- ( j e. ( 0 ... N ) -> j e. ZZ )
250	249	ad2antlr 726	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> j e. ZZ )
251		elfzoelz 11809	. . . . . . . . . . . . . 14 |- ( J e. ( 0..^ N ) -> J e. ZZ )
252	42, 251	syl 16	. . . . . . . . . . . . 13 |- ( ph -> J e. ZZ )
253	252	ad2antrr 725	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> J e. ZZ )
254		simpr 461	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> ( S ` J ) < ( S ` j ) )
255	213	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> S Isom < , < ( ( 0 ... N ) , H ) )
256	44	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> J e. ( 0 ... N ) )
257		simplr 754	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> j e. ( 0 ... N ) )
258		isorel 6221	. . . . . . . . . . . . . . 15 |- ( ( S Isom < , < ( ( 0 ... N ) , H ) /\ ( J e. ( 0 ... N ) /\ j e. ( 0 ... N ) ) ) -> ( J < j <-> ( S ` J ) < ( S ` j ) ) )
259	255, 256, 257, 258	syl12anc 1226	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> ( J < j <-> ( S ` J ) < ( S ` j ) ) )
260	254, 259	mpbird 232	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> J < j )
261	260	adantrr 716	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> J < j )
262		simpr 461	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> ( S ` j ) < ( S ` ( J + 1 ) ) )
263	213	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> S Isom < , < ( ( 0 ... N ) , H ) )
264		simplr 754	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> j e. ( 0 ... N ) )
265	47	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> ( J + 1 ) e. ( 0 ... N ) )
266		isorel 6221	. . . . . . . . . . . . . . 15 |- ( ( S Isom < , < ( ( 0 ... N ) , H ) /\ ( j e. ( 0 ... N ) /\ ( J + 1 ) e. ( 0 ... N ) ) ) -> ( j < ( J + 1 ) <-> ( S ` j ) < ( S ` ( J + 1 ) ) ) )
267	263, 264, 265, 266	syl12anc 1226	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> ( j < ( J + 1 ) <-> ( S ` j ) < ( S ` ( J + 1 ) ) ) )
268	262, 267	mpbird 232	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> j < ( J + 1 ) )
269	268	adantrl 715	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> j < ( J + 1 ) )
270		btwnnz 10949	. . . . . . . . . . . 12 |- ( ( J e. ZZ /\ J < j /\ j < ( J + 1 ) ) -> -. j e. ZZ )
271	253, 261, 269, 270	syl3anc 1228	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> -. j e. ZZ )
272	250, 271	pm2.65da 576	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... N ) ) -> -. ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) )
273	272	adantlr 714	. . . . . . . . 9 |- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) -> -. ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) )
274	273	adantr 465	. . . . . . . 8 |- ( ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> -. ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) )
275	248, 274	pm2.65da 576	. . . . . . 7 |- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) -> -. ( S ` j ) = X )
276	275	ralrimiva 2881	. . . . . 6 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> A. j e. ( 0 ... N ) -. ( S ` j ) = X )
277		ralnex 2913	. . . . . 6 |- ( A. j e. ( 0 ... N ) -. ( S ` j ) = X <-> -. E. j e. ( 0 ... N ) ( S ` j ) = X )
278	276, 277	sylib 196	. . . . 5 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> -. E. j e. ( 0 ... N ) ( S ` j ) = X )
279	278	adantr 465	. . . 4 |- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ X e. H ) -> -. E. j e. ( 0 ... N ) ( S ` j ) = X )
280	226, 279	pm2.65da 576	. . 3 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> -. X e. H )
281	212, 280	pm2.65da 576	. 2 |- ( ph -> -. ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) )
282	117, 15	lenltd 9742	. 2 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` K ) <-> -. ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) )
283	281, 282	mpbird 232	1 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` K ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   A.wral 2817   E.wrex 2818   {crab 2821   u. cun 3479   C_ wss 3481   {cpr 4035   class class class wbr 4453   |-> cmpt 4511   dom cdm 5005   ran crn 5006   iotacio 5555   Fun wfun 5588   -->wf 5590   -onto->wfo 5592   -1-1-onto->wf1o 5593   ` cfv 5594   Isom wiso 5595  (class class class)co 6295   ^m cmap 7432   CCcc 9502   RRcr 9503   0cc0 9504   1c1 9505   + caddc 9507   x. cmul 9509   RR*cxr 9639   < clt 9640   <_ cle 9641   - cmin 9817   / cdiv 10218   NNcn 10548   ZZcz 10876   RR+crp 11232   (,]cioc 11542   [,)cico 11543   [,]cicc 11544   ...cfz 11684  ..^cfzo 11804   |_cfl 11907   #chash 12385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581  ax-pre-sup 9582

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-iin 4334  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6696  df-1st 6795  df-2nd 6796  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-er 7323  df-map 7434  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-fi 7883  df-sup 7913  df-oi 7947  df-card 8332  df-cda 8560  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-div 10219  df-nn 10549  df-2 10606  df-3 10607  df-n0 10808  df-z 10877  df-uz 11095  df-q 11195  df-rp 11233  df-xneg 11330  df-xadd 11331  df-xmul 11332  df-ioo 11545  df-ioc 11546  df-ico 11547  df-icc 11548  df-fz 11685  df-fzo 11805  df-fl 11909  df-seq 12088  df-exp 12147  df-hash 12386  df-cj 12912  df-re 12913  df-im 12914  df-sqrt 13048  df-abs 13049  df-rest 14695  df-topgen 14716  df-psmet 18281  df-xmet 18282  df-met 18283  df-bl 18284  df-mopn 18285  df-top 19268  df-bases 19270  df-topon 19271  df-cld 19388  df-ntr 19389  df-cls 19390  df-nei 19467  df-lp 19505  df-cmp 19755

This theorem is referenced by:  fourierdlem79  31809