Theorem fourierdlem63 32194

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.e	. . . . 5 |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
2	1	a1i 11	. . . 4 |- ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
3		id 22	. . . . . 6 |- ( x = ( S ` ( J + 1 ) ) -> x = ( S ` ( J + 1 ) ) )
4		oveq2 6278	. . . . . . . . 9 |- ( x = ( S ` ( J + 1 ) ) -> ( B - x ) = ( B - ( S ` ( J + 1 ) ) ) )
5	4	oveq1d 6285	. . . . . . . 8 |- ( x = ( S ` ( J + 1 ) ) -> ( ( B - x ) / T ) = ( ( B - ( S ` ( J + 1 ) ) ) / T ) )
6	5	fveq2d 5852	. . . . . . 7 |- ( x = ( S ` ( J + 1 ) ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
7	6	oveq1d 6285	. . . . . 6 |- ( x = ( S ` ( J + 1 ) ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
8	3, 7	oveq12d 6288	. . . . 5 |- ( x = ( S ` ( J + 1 ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
9	8	adantl 464	. . . 4 |- ( ( ph /\ x = ( S ` ( J + 1 ) ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
10		fourierdlem63.t	. . . . . . . . . . 11 |- T = ( B - A )
11		fourierdlem63.p	. . . . . . . . . . 11 |- 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 ) ) ) } )
12		fourierdlem63.m	. . . . . . . . . . 11 |- ( ph -> M e. NN )
13		fourierdlem63.q	. . . . . . . . . . 11 |- ( ph -> Q e. ( P ` M ) )
14		fourierdlem63.c	. . . . . . . . . . 11 |- ( ph -> C e. RR )
15		fourierdlem63.d	. . . . . . . . . . 11 |- ( ph -> D e. RR )
16		fourierdlem63.cltd	. . . . . . . . . . 11 |- ( ph -> C < D )
17		fourierdlem63.o	. . . . . . . . . . 11 |- 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 ) ) ) } )
18		fourierdlem63.h	. . . . . . . . . . 11 |- H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
19		fourierdlem63.n	. . . . . . . . . . 11 |- N = ( ( # ` H ) - 1 )
20		fourierdlem63.s	. . . . . . . . . . 11 |- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
21	10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20	fourierdlem54 32185	. . . . . . . . . 10 |- ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , H ) ) )
22	21	simpld 457	. . . . . . . . 9 |- ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
23	22	simprd 461	. . . . . . . 8 |- ( ph -> S e. ( O ` N ) )
24	22	simpld 457	. . . . . . . . 9 |- ( ph -> N e. NN )
25	17	fourierdlem2 32133	. . . . . . . . 9 |- ( 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 ) ) ) ) ) )
26	24, 25	syl 16	. . . . . . . 8 |- ( 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 ) ) ) ) ) )
27	23, 26	mpbid 210	. . . . . . 7 |- ( ph -> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) )
28	27	simpld 457	. . . . . 6 |- ( ph -> S e. ( RR ^m ( 0 ... N ) ) )
29		elmapi 7433	. . . . . 6 |- ( S e. ( RR ^m ( 0 ... N ) ) -> S : ( 0 ... N ) --> RR )
30	28, 29	syl 16	. . . . 5 |- ( ph -> S : ( 0 ... N ) --> RR )
31		fourierdlem63.j	. . . . . 6 |- ( ph -> J e. ( 0..^ N ) )
32		fzofzp1 11890	. . . . . 6 |- ( J e. ( 0..^ N ) -> ( J + 1 ) e. ( 0 ... N ) )
33	31, 32	syl 16	. . . . 5 |- ( ph -> ( J + 1 ) e. ( 0 ... N ) )
34	30, 33	ffvelrnd 6008	. . . 4 |- ( ph -> ( S ` ( J + 1 ) ) e. RR )
35	11, 12, 13	fourierdlem11 32142	. . . . . . . . . . 11 |- ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
36	35	simp2d 1007	. . . . . . . . . 10 |- ( ph -> B e. RR )
37	36, 34	resubcld 9983	. . . . . . . . 9 |- ( ph -> ( B - ( S ` ( J + 1 ) ) ) e. RR )
38	35	simp1d 1006	. . . . . . . . . . 11 |- ( ph -> A e. RR )
39	36, 38	resubcld 9983	. . . . . . . . . 10 |- ( ph -> ( B - A ) e. RR )
40	10, 39	syl5eqel 2546	. . . . . . . . 9 |- ( ph -> T e. RR )
41	35	simp3d 1008	. . . . . . . . . . . 12 |- ( ph -> A < B )
42	38, 36	posdifd 10135	. . . . . . . . . . . 12 |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
43	41, 42	mpbid 210	. . . . . . . . . . 11 |- ( ph -> 0 < ( B - A ) )
44	43, 10	syl6breqr 4479	. . . . . . . . . 10 |- ( ph -> 0 < T )
45	44	gt0ne0d 10113	. . . . . . . . 9 |- ( ph -> T =/= 0 )
46	37, 40, 45	redivcld 10368	. . . . . . . 8 |- ( ph -> ( ( B - ( S ` ( J + 1 ) ) ) / T ) e. RR )
47	46	flcld 11916	. . . . . . 7 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. ZZ )
48	47	zred 10965	. . . . . 6 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. RR )
49	48, 40	remulcld 9613	. . . . 5 |- ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. RR )
50	34, 49	readdcld 9612	. . . 4 |- ( ph -> ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) e. RR )
51	2, 9, 34, 50	fvmptd 5936	. . 3 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
52	51, 50	eqeltrd 2542	. 2 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. RR )
53	11	fourierdlem2 32133	. . . . . . 7 |- ( 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 ) ) ) ) ) )
54	12, 53	syl 16	. . . . . 6 |- ( 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 ) ) ) ) ) )
55	13, 54	mpbid 210	. . . . 5 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
56	55	simpld 457	. . . 4 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
57		elmapi 7433	. . . 4 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
58	56, 57	syl 16	. . 3 |- ( ph -> Q : ( 0 ... M ) --> RR )
59		fourierdlem63.k	. . 3 |- ( ph -> K e. ( 0 ... M ) )
60	58, 59	ffvelrnd 6008	. 2 |- ( ph -> ( Q ` K ) e. RR )
61	14	adantr 463	. . . . . . 7 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> C e. RR )
62	15	adantr 463	. . . . . . 7 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> D e. RR )
63	38	rexrd 9632	. . . . . . . . . . . 12 |- ( ph -> A e. RR* )
64		iocssre 11607	. . . . . . . . . . . 12 |- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
65	63, 36, 64	syl2anc 659	. . . . . . . . . . 11 |- ( ph -> ( A (,] B ) C_ RR )
66	38, 36, 41, 10, 1	fourierdlem4 32135	. . . . . . . . . . . 12 |- ( ph -> E : RR --> ( A (,] B ) )
67		fourierdlem63.y	. . . . . . . . . . . . . 14 |- ( ph -> Y e. ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) )
68		elfzofz 11819	. . . . . . . . . . . . . . . . 17 |- ( J e. ( 0..^ N ) -> J e. ( 0 ... N ) )
69	31, 68	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> J e. ( 0 ... N ) )
70	30, 69	ffvelrnd 6008	. . . . . . . . . . . . . . 15 |- ( ph -> ( S ` J ) e. RR )
71	34	rexrd 9632	. . . . . . . . . . . . . . 15 |- ( ph -> ( S ` ( J + 1 ) ) e. RR* )
72		elico2 11591	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) ) ) )
73	70, 71, 72	syl2anc 659	. . . . . . . . . . . . . 14 |- ( ph -> ( Y e. ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) <-> ( Y e. RR /\ ( S ` J ) <_ Y /\ Y < ( S ` ( J + 1 ) ) ) ) )
74	67, 73	mpbid 210	. . . . . . . . . . . . 13 |- ( ph -> ( Y e. RR /\ ( S ` J ) <_ Y /\ Y < ( S ` ( J + 1 ) ) ) )
75	74	simp1d 1006	. . . . . . . . . . . 12 |- ( ph -> Y e. RR )
76	66, 75	ffvelrnd 6008	. . . . . . . . . . 11 |- ( ph -> ( E ` Y ) e. ( A (,] B ) )
77	65, 76	sseldd 3490	. . . . . . . . . 10 |- ( ph -> ( E ` Y ) e. RR )
78	77, 75	resubcld 9983	. . . . . . . . 9 |- ( ph -> ( ( E ` Y ) - Y ) e. RR )
79	60, 78	resubcld 9983	. . . . . . . 8 |- ( ph -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. RR )
80	79	adantr 463	. . . . . . 7 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. RR )
81		icossicc 11614	. . . . . . . . . . . . . 14 |- ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) C_ ( ( S ` J ) [,] ( S ` ( J + 1 ) ) )
82	14	rexrd 9632	. . . . . . . . . . . . . . 15 |- ( ph -> C e. RR* )
83	15	rexrd 9632	. . . . . . . . . . . . . . 15 |- ( ph -> D e. RR* )
84	17, 24, 23	fourierdlem15 32146	. . . . . . . . . . . . . . 15 |- ( ph -> S : ( 0 ... N ) --> ( C [,] D ) )
85	82, 83, 84, 31	fourierdlem8 32139	. . . . . . . . . . . . . 14 |- ( ph -> ( ( S ` J ) [,] ( S ` ( J + 1 ) ) ) C_ ( C [,] D ) )
86	81, 85	syl5ss 3500	. . . . . . . . . . . . 13 |- ( ph -> ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) C_ ( C [,] D ) )
87	86, 67	sseldd 3490	. . . . . . . . . . . 12 |- ( ph -> Y e. ( C [,] D ) )
88		elicc2 11592	. . . . . . . . . . . . 13 |- ( ( C e. RR /\ D e. RR ) -> ( Y e. ( C [,] D ) <-> ( Y e. RR /\ C <_ Y /\ Y <_ D ) ) )
89	14, 15, 88	syl2anc 659	. . . . . . . . . . . 12 |- ( ph -> ( Y e. ( C [,] D ) <-> ( Y e. RR /\ C <_ Y /\ Y <_ D ) ) )
90	87, 89	mpbid 210	. . . . . . . . . . 11 |- ( ph -> ( Y e. RR /\ C <_ Y /\ Y <_ D ) )
91	90	simp2d 1007	. . . . . . . . . 10 |- ( ph -> C <_ Y )
92	60, 77	resubcld 9983	. . . . . . . . . . . . 13 |- ( ph -> ( ( Q ` K ) - ( E ` Y ) ) e. RR )
93		fourierdlem63.eyltqk	. . . . . . . . . . . . . 14 |- ( ph -> ( E ` Y ) < ( Q ` K ) )
94	77, 60	posdifd 10135	. . . . . . . . . . . . . 14 |- ( ph -> ( ( E ` Y ) < ( Q ` K ) <-> 0 < ( ( Q ` K ) - ( E ` Y ) ) ) )
95	93, 94	mpbid 210	. . . . . . . . . . . . 13 |- ( ph -> 0 < ( ( Q ` K ) - ( E ` Y ) ) )
96	92, 95	elrpd 11256	. . . . . . . . . . . 12 |- ( ph -> ( ( Q ` K ) - ( E ` Y ) ) e. RR+ )
97	75, 96	ltaddrpd 11288	. . . . . . . . . . 11 |- ( ph -> Y < ( Y + ( ( Q ` K ) - ( E ` Y ) ) ) )
98	60	recnd 9611	. . . . . . . . . . . . 13 |- ( ph -> ( Q ` K ) e. CC )
99	77	recnd 9611	. . . . . . . . . . . . 13 |- ( ph -> ( E ` Y ) e. CC )
100	75	recnd 9611	. . . . . . . . . . . . 13 |- ( ph -> Y e. CC )
101	98, 99, 100	subsub3d 9952	. . . . . . . . . . . 12 |- ( ph -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) = ( ( ( Q ` K ) + Y ) - ( E ` Y ) ) )
102	98, 100	addcomd 9771	. . . . . . . . . . . . 13 |- ( ph -> ( ( Q ` K ) + Y ) = ( Y + ( Q ` K ) ) )
103	102	oveq1d 6285	. . . . . . . . . . . 12 |- ( ph -> ( ( ( Q ` K ) + Y ) - ( E ` Y ) ) = ( ( Y + ( Q ` K ) ) - ( E ` Y ) ) )
104	100, 98, 99	addsubassd 9942	. . . . . . . . . . . 12 |- ( ph -> ( ( Y + ( Q ` K ) ) - ( E ` Y ) ) = ( Y + ( ( Q ` K ) - ( E ` Y ) ) ) )
105	101, 103, 104	3eqtrrd 2500	. . . . . . . . . . 11 |- ( ph -> ( Y + ( ( Q ` K ) - ( E ` Y ) ) ) = ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) )
106	97, 105	breqtrd 4463	. . . . . . . . . 10 |- ( ph -> Y < ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) )
107	14, 75, 79, 91, 106	lelttrd 9729	. . . . . . . . 9 |- ( ph -> C < ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) )
108	14, 79, 107	ltled 9722	. . . . . . . 8 |- ( ph -> C <_ ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) )
109	108	adantr 463	. . . . . . 7 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> C <_ ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) )
110	34	adantr 463	. . . . . . . . 9 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( S ` ( J + 1 ) ) e. RR )
111	60	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( Q ` K ) e. RR )
112	52, 34	resubcld 9983	. . . . . . . . . . . 12 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) e. RR )
113	112	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) e. RR )
114	111, 113	resubcld 9983	. . . . . . . . . 10 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) e. RR )
115	74	simp3d 1008	. . . . . . . . . . . . . 14 |- ( ph -> Y < ( S ` ( J + 1 ) ) )
116	75, 34, 115	ltled 9722	. . . . . . . . . . . . 13 |- ( ph -> Y <_ ( S ` ( J + 1 ) ) )
117	38, 36, 41, 10, 1, 75, 34, 116	fourierdlem7 32138	. . . . . . . . . . . 12 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) <_ ( ( E ` Y ) - Y ) )
118	112, 78, 60, 117	lesub2dd 10165	. . . . . . . . . . 11 |- ( ph -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) <_ ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) )
119	118	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) <_ ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) )
120	98	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( Q ` K ) e. CC )
121	52	recnd 9611	. . . . . . . . . . . . . 14 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. CC )
122	121	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) e. CC )
123	110	recnd 9611	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( S ` ( J + 1 ) ) e. CC )
124	120, 122, 123	subsubd 9950	. . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
125	98, 121	subcld 9922	. . . . . . . . . . . . . 14 |- ( ph -> ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. CC )
126	34	recnd 9611	. . . . . . . . . . . . . 14 |- ( ph -> ( S ` ( J + 1 ) ) e. CC )
127	125, 126	addcomd 9771	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) + ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
128	127	adantr 463	. . . . . . . . . . . 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 ) ) ) ) ) )
129	124, 128	eqtrd 2495	. . . . . . . . . . 11 |- ( ( 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 ) ) ) ) ) )
130		simpr 459	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) )
131	52	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) e. RR )
132	111, 131	sublt0d 31737	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) < 0 <-> ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) )
133	130, 132	mpbird 232	. . . . . . . . . . . 12 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) < 0 )
134	111, 131	resubcld 9983	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. RR )
135		ltaddneg 31727	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) ) )
136	134, 110, 135	syl2anc 659	. . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
137	133, 136	mpbid 210	. . . . . . . . . . 11 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( S ` ( J + 1 ) ) + ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) < ( S ` ( J + 1 ) ) )
138	129, 137	eqbrtrd 4459	. . . . . . . . . 10 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) < ( S ` ( J + 1 ) ) )
139	80, 114, 110, 119, 138	lelttrd 9729	. . . . . . . . 9 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) < ( S ` ( J + 1 ) ) )
140	84, 33	ffvelrnd 6008	. . . . . . . . . . . 12 |- ( ph -> ( S ` ( J + 1 ) ) e. ( C [,] D ) )
141		elicc2 11592	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
142	14, 15, 141	syl2anc 659	. . . . . . . . . . . 12 |- ( ph -> ( ( S ` ( J + 1 ) ) e. ( C [,] D ) <-> ( ( S ` ( J + 1 ) ) e. RR /\ C <_ ( S ` ( J + 1 ) ) /\ ( S ` ( J + 1 ) ) <_ D ) ) )
143	140, 142	mpbid 210	. . . . . . . . . . 11 |- ( ph -> ( ( S ` ( J + 1 ) ) e. RR /\ C <_ ( S ` ( J + 1 ) ) /\ ( S ` ( J + 1 ) ) <_ D ) )
144	143	simp3d 1008	. . . . . . . . . 10 |- ( ph -> ( S ` ( J + 1 ) ) <_ D )
145	144	adantr 463	. . . . . . . . 9 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( S ` ( J + 1 ) ) <_ D )
146	80, 110, 62, 139, 145	ltletrd 9731	. . . . . . . 8 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) < D )
147	80, 62, 146	ltled 9722	. . . . . . 7 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) <_ D )
148	61, 62, 80, 109, 147	eliccd 31780	. . . . . 6 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. ( C [,] D ) )
149		id 22	. . . . . . . . . . . . . . 15 |- ( x = Y -> x = Y )
150		oveq2 6278	. . . . . . . . . . . . . . . . . 18 |- ( x = Y -> ( B - x ) = ( B - Y ) )
151	150	oveq1d 6285	. . . . . . . . . . . . . . . . 17 |- ( x = Y -> ( ( B - x ) / T ) = ( ( B - Y ) / T ) )
152	151	fveq2d 5852	. . . . . . . . . . . . . . . 16 |- ( x = Y -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - Y ) / T ) ) )
153	152	oveq1d 6285	. . . . . . . . . . . . . . 15 |- ( x = Y -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) )
154	149, 153	oveq12d 6288	. . . . . . . . . . . . . 14 |- ( x = Y -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) )
155	154	adantl 464	. . . . . . . . . . . . 13 |- ( ( ph /\ x = Y ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) )
156	36, 75	resubcld 9983	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( B - Y ) e. RR )
157	156, 40, 45	redivcld 10368	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( B - Y ) / T ) e. RR )
158	157	flcld 11916	. . . . . . . . . . . . . . . 16 |- ( ph -> ( |_ ` ( ( B - Y ) / T ) ) e. ZZ )
159	158	zred 10965	. . . . . . . . . . . . . . 15 |- ( ph -> ( |_ ` ( ( B - Y ) / T ) ) e. RR )
160	159, 40	remulcld 9613	. . . . . . . . . . . . . 14 |- ( ph -> ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) e. RR )
161	75, 160	readdcld 9612	. . . . . . . . . . . . 13 |- ( ph -> ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) e. RR )
162	2, 155, 75, 161	fvmptd 5936	. . . . . . . . . . . 12 |- ( ph -> ( E ` Y ) = ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) )
163	162	oveq1d 6285	. . . . . . . . . . 11 |- ( ph -> ( ( E ` Y ) - Y ) = ( ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) - Y ) )
164	163	oveq1d 6285	. . . . . . . . . 10 |- ( ph -> ( ( ( E ` Y ) - Y ) / T ) = ( ( ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) - Y ) / T ) )
165	160	recnd 9611	. . . . . . . . . . . 12 |- ( ph -> ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) e. CC )
166	100, 165	pncan2d 9924	. . . . . . . . . . 11 |- ( ph -> ( ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) - Y ) = ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) )
167	166	oveq1d 6285	. . . . . . . . . 10 |- ( ph -> ( ( ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) - Y ) / T ) = ( ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) / T ) )
168	159	recnd 9611	. . . . . . . . . . 11 |- ( ph -> ( |_ ` ( ( B - Y ) / T ) ) e. CC )
169	40	recnd 9611	. . . . . . . . . . 11 |- ( ph -> T e. CC )
170	168, 169, 45	divcan4d 10322	. . . . . . . . . 10 |- ( ph -> ( ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) / T ) = ( |_ ` ( ( B - Y ) / T ) ) )
171	164, 167, 170	3eqtrd 2499	. . . . . . . . 9 |- ( ph -> ( ( ( E ` Y ) - Y ) / T ) = ( |_ ` ( ( B - Y ) / T ) ) )
172	171, 158	eqeltrd 2542	. . . . . . . 8 |- ( ph -> ( ( ( E ` Y ) - Y ) / T ) e. ZZ )
173	78	recnd 9611	. . . . . . . . . . . 12 |- ( ph -> ( ( E ` Y ) - Y ) e. CC )
174	173, 169, 45	divcan1d 10317	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( E ` Y ) - Y ) / T ) x. T ) = ( ( E ` Y ) - Y ) )
175	174	oveq2d 6286	. . . . . . . . . 10 |- ( ph -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) = ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( E ` Y ) - Y ) ) )
176	98, 173	npcand 9926	. . . . . . . . . 10 |- ( ph -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( E ` Y ) - Y ) ) = ( Q ` K ) )
177	175, 176	eqtrd 2495	. . . . . . . . 9 |- ( ph -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) = ( Q ` K ) )
178		ffun 5715	. . . . . . . . . . 11 |- ( Q : ( 0 ... M ) --> RR -> Fun Q )
179	58, 178	syl 16	. . . . . . . . . 10 |- ( ph -> Fun Q )
180		fdm 5717	. . . . . . . . . . . 12 |- ( Q : ( 0 ... M ) --> RR -> dom Q = ( 0 ... M ) )
181	58, 180	syl 16	. . . . . . . . . . 11 |- ( ph -> dom Q = ( 0 ... M ) )
182	59, 181	eleqtrrd 2545	. . . . . . . . . 10 |- ( ph -> K e. dom Q )
183		fvelrn 6000	. . . . . . . . . 10 |- ( ( Fun Q /\ K e. dom Q ) -> ( Q ` K ) e. ran Q )
184	179, 182, 183	syl2anc 659	. . . . . . . . 9 |- ( ph -> ( Q ` K ) e. ran Q )
185	177, 184	eqeltrd 2542	. . . . . . . 8 |- ( ph -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) e. ran Q )
186		oveq1 6277	. . . . . . . . . . 11 |- ( k = ( ( ( E ` Y ) - Y ) / T ) -> ( k x. T ) = ( ( ( ( E ` Y ) - Y ) / T ) x. T ) )
187	186	oveq2d 6286	. . . . . . . . . 10 |- ( k = ( ( ( E ` Y ) - Y ) / T ) -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) = ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) )
188	187	eleq1d 2523	. . . . . . . . 9 |- ( 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 ) )
189	188	rspcev 3207	. . . . . . . 8 |- ( ( ( ( ( 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 )
190	172, 185, 189	syl2anc 659	. . . . . . 7 |- ( ph -> E. k e. ZZ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q )
191	190	adantr 463	. . . . . 6 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> E. k e. ZZ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q )
192		oveq1 6277	. . . . . . . . 9 |- ( x = ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) -> ( x + ( k x. T ) ) = ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) )
193	192	eleq1d 2523	. . . . . . . 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 ) )
194	193	rexbidv 2965	. . . . . . 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 ) )
195	194	elrab 3254	. . . . . 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 ) )
196	148, 191, 195	sylanbrc 662	. . . . 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 } )
197		elun2 3658	. . . . 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 } ) )
198	196, 197	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 } ) )
199		fourierdlem63.x	. . . 4 |- X = ( ( Q ` K ) - ( ( E ` Y ) - Y ) )
200	198, 199, 18	3eltr4g 2560	. . 3 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> X e. H )
201		elfzelz 11691	. . . . . . . . 9 |- ( j e. ( 0 ... N ) -> j e. ZZ )
202	201	ad2antlr 724	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> j e. ZZ )
203		elfzoelz 11804	. . . . . . . . . . 11 |- ( J e. ( 0..^ N ) -> J e. ZZ )
204	31, 203	syl 16	. . . . . . . . . 10 |- ( ph -> J e. ZZ )
205	204	ad2antrr 723	. . . . . . . . 9 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> J e. ZZ )
206		simpr 459	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> ( S ` J ) < ( S ` j ) )
207	21	simprd 461	. . . . . . . . . . . . 13 |- ( ph -> S Isom < , < ( ( 0 ... N ) , H ) )
208	207	ad2antrr 723	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> S Isom < , < ( ( 0 ... N ) , H ) )
209	69	ad2antrr 723	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> J e. ( 0 ... N ) )
210		simplr 753	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> j e. ( 0 ... N ) )
211		isorel 6197	. . . . . . . . . . . 12 |- ( ( S Isom < , < ( ( 0 ... N ) , H ) /\ ( J e. ( 0 ... N ) /\ j e. ( 0 ... N ) ) ) -> ( J < j <-> ( S ` J ) < ( S ` j ) ) )
212	208, 209, 210, 211	syl12anc 1224	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> ( J < j <-> ( S ` J ) < ( S ` j ) ) )
213	206, 212	mpbird 232	. . . . . . . . . 10 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> J < j )
214	213	adantrr 714	. . . . . . . . 9 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> J < j )
215		simpr 459	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> ( S ` j ) < ( S ` ( J + 1 ) ) )
216	207	ad2antrr 723	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> S Isom < , < ( ( 0 ... N ) , H ) )
217		simplr 753	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> j e. ( 0 ... N ) )
218	33	ad2antrr 723	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> ( J + 1 ) e. ( 0 ... N ) )
219		isorel 6197	. . . . . . . . . . . 12 |- ( ( S Isom < , < ( ( 0 ... N ) , H ) /\ ( j e. ( 0 ... N ) /\ ( J + 1 ) e. ( 0 ... N ) ) ) -> ( j < ( J + 1 ) <-> ( S ` j ) < ( S ` ( J + 1 ) ) ) )
220	216, 217, 218, 219	syl12anc 1224	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> ( j < ( J + 1 ) <-> ( S ` j ) < ( S ` ( J + 1 ) ) ) )
221	215, 220	mpbird 232	. . . . . . . . . 10 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> j < ( J + 1 ) )
222	221	adantrl 713	. . . . . . . . 9 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> j < ( J + 1 ) )
223		btwnnz 10935	. . . . . . . . 9 |- ( ( J e. ZZ /\ J < j /\ j < ( J + 1 ) ) -> -. j e. ZZ )
224	205, 214, 222, 223	syl3anc 1226	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> -. j e. ZZ )
225	202, 224	pm2.65da 574	. . . . . . 7 |- ( ( ph /\ j e. ( 0 ... N ) ) -> -. ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) )
226	225	adantlr 712	. . . . . 6 |- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) -> -. ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) )
227	70	ad2antrr 723	. . . . . . . . 9 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` J ) e. RR )
228	75	ad2antrr 723	. . . . . . . . 9 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> Y e. RR )
229	30	ffvelrnda 6007	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( S ` j ) e. RR )
230	229	adantr 463	. . . . . . . . 9 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` j ) e. RR )
231	74	simp2d 1007	. . . . . . . . . 10 |- ( ph -> ( S ` J ) <_ Y )
232	231	ad2antrr 723	. . . . . . . . 9 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` J ) <_ Y )
233	106, 199	syl6breqr 4479	. . . . . . . . . . . 12 |- ( ph -> Y < X )
234	233	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ ( S ` j ) = X ) -> Y < X )
235		eqcom 2463	. . . . . . . . . . . . 13 |- ( X = ( S ` j ) <-> ( S ` j ) = X )
236	235	biimpri 206	. . . . . . . . . . . 12 |- ( ( S ` j ) = X -> X = ( S ` j ) )
237	236	adantl 464	. . . . . . . . . . 11 |- ( ( ph /\ ( S ` j ) = X ) -> X = ( S ` j ) )
238	234, 237	breqtrd 4463	. . . . . . . . . 10 |- ( ( ph /\ ( S ` j ) = X ) -> Y < ( S ` j ) )
239	238	adantlr 712	. . . . . . . . 9 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> Y < ( S ` j ) )
240	227, 228, 230, 232, 239	lelttrd 9729	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` J ) < ( S ` j ) )
241	240	adantllr 716	. . . . . . 7 |- ( ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` J ) < ( S ` j ) )
242		simpr 459	. . . . . . . . 9 |- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ ( S ` j ) = X ) -> ( S ` j ) = X )
243	199, 139	syl5eqbr 4472	. . . . . . . . . 10 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> X < ( S ` ( J + 1 ) ) )
244	243	adantr 463	. . . . . . . . 9 |- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ ( S ` j ) = X ) -> X < ( S ` ( J + 1 ) ) )
245	242, 244	eqbrtrd 4459	. . . . . . . 8 |- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ ( S ` j ) = X ) -> ( S ` j ) < ( S ` ( J + 1 ) ) )
246	245	adantlr 712	. . . . . . 7 |- ( ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` j ) < ( S ` ( J + 1 ) ) )
247	241, 246	jca 530	. . . . . 6 |- ( ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) )
248	226, 247	mtand 657	. . . . 5 |- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) -> -. ( S ` j ) = X )
249	248	nrexdv 2910	. . . 4 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> -. E. j e. ( 0 ... N ) ( S ` j ) = X )
250		isof1o 6196	. . . . . . . . 9 |- ( S Isom < , < ( ( 0 ... N ) , H ) -> S : ( 0 ... N ) -1-1-onto-> H )
251	207, 250	syl 16	. . . . . . . 8 |- ( ph -> S : ( 0 ... N ) -1-1-onto-> H )
252		f1ofo 5805	. . . . . . . 8 |- ( S : ( 0 ... N ) -1-1-onto-> H -> S : ( 0 ... N ) -onto-> H )
253	251, 252	syl 16	. . . . . . 7 |- ( ph -> S : ( 0 ... N ) -onto-> H )
254		foelrn 6026	. . . . . . 7 |- ( ( S : ( 0 ... N ) -onto-> H /\ X e. H ) -> E. j e. ( 0 ... N ) X = ( S ` j ) )
255	253, 254	sylan 469	. . . . . 6 |- ( ( ph /\ X e. H ) -> E. j e. ( 0 ... N ) X = ( S ` j ) )
256	235	rexbii 2956	. . . . . 6 |- ( E. j e. ( 0 ... N ) X = ( S ` j ) <-> E. j e. ( 0 ... N ) ( S ` j ) = X )
257	255, 256	sylib 196	. . . . 5 |- ( ( ph /\ X e. H ) -> E. j e. ( 0 ... N ) ( S ` j ) = X )
258	257	adantlr 712	. . . 4 |- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ X e. H ) -> E. j e. ( 0 ... N ) ( S ` j ) = X )
259	249, 258	mtand 657	. . 3 |- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> -. X e. H )
260	200, 259	pm2.65da 574	. 2 |- ( ph -> -. ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) )
261	52, 60, 260	nltled 31720	1 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` K ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 367   /\ w3a 971   = wceq 1398   e. wcel 1823   A.wral 2804   E.wrex 2805   {crab 2808   u. cun 3459   C_ wss 3461   {cpr 4018   class class class wbr 4439   |-> cmpt 4497   dom cdm 4988   ran crn 4989   iotacio 5532   Fun wfun 5564   -->wf 5566   -onto->wfo 5568   -1-1-onto->wf1o 5569   ` cfv 5570   Isom wiso 5571  (class class class)co 6270   ^m cmap 7412   CCcc 9479   RRcr 9480   0cc0 9481   1c1 9482   + caddc 9484   x. cmul 9486   RR*cxr 9616   < clt 9617   <_ cle 9618   - cmin 9796   / cdiv 10202   NNcn 10531   ZZcz 10860   (,]cioc 11533   [,)cico 11534   [,]cicc 11535   ...cfz 11675  ..^cfzo 11799   |_cfl 11908   #chash 12390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-inf2 8049  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558  ax-pre-sup 9559

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-iin 4318  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-se 4828  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-isom 5579  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-1st 6773  df-2nd 6774  df-recs 7034  df-rdg 7068  df-1o 7122  df-oadd 7126  df-er 7303  df-map 7414  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513  df-fi 7863  df-sup 7893  df-oi 7927  df-card 8311  df-cda 8539  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-div 10203  df-nn 10532  df-2 10590  df-3 10591  df-n0 10792  df-z 10861  df-uz 11083  df-q 11184  df-rp 11222  df-xneg 11321  df-xadd 11322  df-xmul 11323  df-ioo 11536  df-ioc 11537  df-ico 11538  df-icc 11539  df-fz 11676  df-fzo 11800  df-fl 11910  df-seq 12093  df-exp 12152  df-hash 12391  df-cj 13017  df-re 13018  df-im 13019  df-sqrt 13153  df-abs 13154  df-rest 14915  df-topgen 14936  df-psmet 18609  df-xmet 18610  df-met 18611  df-bl 18612  df-mopn 18613  df-top 19569  df-bases 19571  df-topon 19572  df-cld 19690  df-ntr 19691  df-cls 19692  df-nei 19769  df-lp 19807  df-cmp 20057

This theorem is referenced by:  fourierdlem79  32210