Theorem fourierdlem79 37317

Description: E projects every interval of the partition induced by S on H into a corresponding interval of the partition induced by Q on [ A , B ]. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem79.t	|- T = ( B - A )
fourierdlem79.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 ) ) ) } )
fourierdlem79.m	|- ( ph -> M e. NN )
fourierdlem79.q	|- ( ph -> Q e. ( P ` M ) )
fourierdlem79.c	|- ( ph -> C e. RR )
fourierdlem79.d	|- ( ph -> D e. RR )
fourierdlem79.cltd	|- ( ph -> C < D )
fourierdlem79.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 ) ) ) } )
fourierdlem79.h	|- H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
fourierdlem79.n	|- N = ( ( # ` H ) - 1 )
fourierdlem79.s	|- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
fourierdlem79.e	|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
fourierdlem79.l	|- L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
fourierdlem79.z	|- Z = ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) )
fourierdlem79.i	|- I = ( x e. RR |-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) )

Assertion

Ref	Expression
fourierdlem79	|- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( L ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) )

Distinct variable groups:   A, i, j, x   A, m, p, i   y, A, j, x   B, f   B, i, k, x   B, m, p   y, B   C, i, m, p   x, C   D, i, m, p   x, D   f, E   i, E, k, x   y, E   f, H   x, H   f, I   i, I, k, x   i, L, x   i, M, j, x   m, M, p   f, N   i, N, k, x   m, N, p   y, N   Q, f, j   Q, i, k, x, j   Q, p   S, f   S, i, k, x   S, p   y, S   T, i, k, x   k, Z, x   ph, f, j   ph, i, k, x   ph, y

Allowed substitution hints:   ph( m, p)   A( f, k)   B( j)   C( y, f, j, k)   D( y, f, j, k)   P( x, y, f, i, j, k, m, p)   Q( y, m)   S( j, m)   T( y, f, j, m, p)   E( j, m, p)   H( y, i, j, k, m, p)   I( y, j, m, p)   L( y, f, j, k, m, p)   M( y, f, k)   N( j)   O( x, y, f, i, j, k, m, p)   Z( y, f, i, j, m, p)

Proof of Theorem fourierdlem79

Dummy variable l is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem79.q	. . . . . . . 8 |- ( ph -> Q e. ( P ` M ) )
2		fourierdlem79.m	. . . . . . . . 9 |- ( ph -> M e. NN )
3		fourierdlem79.p	. . . . . . . . . 10 |- 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 ) ) ) } )
4	3	fourierdlem2 37240	. . . . . . . . 9 |- ( 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 ) ) ) ) ) )
5	2, 4	syl 17	. . . . . . . 8 |- ( 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 ) ) ) ) ) )
6	1, 5	mpbid 210	. . . . . . 7 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
7	6	simpld 457	. . . . . 6 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
8		elmapi 7477	. . . . . 6 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
9	7, 8	syl 17	. . . . 5 |- ( ph -> Q : ( 0 ... M ) --> RR )
10	9	adantr 463	. . . 4 |- ( ( ph /\ j e. ( 0..^ N ) ) -> Q : ( 0 ... M ) --> RR )
11		fourierdlem79.t	. . . . . . . . 9 |- T = ( B - A )
12		fourierdlem79.e	. . . . . . . . 9 |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
13		fourierdlem79.l	. . . . . . . . 9 |- L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
14		fourierdlem79.i	. . . . . . . . 9 |- I = ( x e. RR |-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) )
15	3, 2, 1, 11, 12, 13, 14	fourierdlem37 37275	. . . . . . . 8 |- ( ph -> ( I : RR --> ( 0..^ M ) /\ ( x e. RR -> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) e. { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } ) ) )
16	15	simpld 457	. . . . . . 7 |- ( ph -> I : RR --> ( 0..^ M ) )
17		fzossfz 11875	. . . . . . . 8 |- ( 0..^ M ) C_ ( 0 ... M )
18	17	a1i 11	. . . . . . 7 |- ( ph -> ( 0..^ M ) C_ ( 0 ... M ) )
19	16, 18	fssd 5722	. . . . . 6 |- ( ph -> I : RR --> ( 0 ... M ) )
20	19	adantr 463	. . . . 5 |- ( ( ph /\ j e. ( 0..^ N ) ) -> I : RR --> ( 0 ... M ) )
21		fourierdlem79.c	. . . . . . . . . . . . 13 |- ( ph -> C e. RR )
22		fourierdlem79.d	. . . . . . . . . . . . 13 |- ( ph -> D e. RR )
23		fourierdlem79.cltd	. . . . . . . . . . . . 13 |- ( ph -> C < D )
24		fourierdlem79.o	. . . . . . . . . . . . 13 |- 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 ) ) ) } )
25		fourierdlem79.h	. . . . . . . . . . . . 13 |- H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
26		fourierdlem79.n	. . . . . . . . . . . . 13 |- N = ( ( # ` H ) - 1 )
27		fourierdlem79.s	. . . . . . . . . . . . 13 |- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
28	11, 3, 2, 1, 21, 22, 23, 24, 25, 26, 27	fourierdlem54 37292	. . . . . . . . . . . 12 |- ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , H ) ) )
29	28	simpld 457	. . . . . . . . . . 11 |- ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
30	29	simprd 461	. . . . . . . . . 10 |- ( ph -> S e. ( O ` N ) )
31	30	adantr 463	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ N ) ) -> S e. ( O ` N ) )
32	29	simpld 457	. . . . . . . . . . 11 |- ( ph -> N e. NN )
33	32	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ N ) ) -> N e. NN )
34	24	fourierdlem2 37240	. . . . . . . . . 10 |- ( 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 ) ) ) ) ) )
35	33, 34	syl 17	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( 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 ) ) ) ) ) )
36	31, 35	mpbid 210	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) )
37	36	simpld 457	. . . . . . 7 |- ( ( ph /\ j e. ( 0..^ N ) ) -> S e. ( RR ^m ( 0 ... N ) ) )
38		elmapi 7477	. . . . . . 7 |- ( S e. ( RR ^m ( 0 ... N ) ) -> S : ( 0 ... N ) --> RR )
39	37, 38	syl 17	. . . . . 6 |- ( ( ph /\ j e. ( 0..^ N ) ) -> S : ( 0 ... N ) --> RR )
40		elfzofz 11872	. . . . . . 7 |- ( j e. ( 0..^ N ) -> j e. ( 0 ... N ) )
41	40	adantl 464	. . . . . 6 |- ( ( ph /\ j e. ( 0..^ N ) ) -> j e. ( 0 ... N ) )
42	39, 41	ffvelrnd 6009	. . . . 5 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( S ` j ) e. RR )
43	20, 42	ffvelrnd 6009	. . . 4 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( I ` ( S ` j ) ) e. ( 0 ... M ) )
44	10, 43	ffvelrnd 6009	. . 3 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( Q ` ( I ` ( S ` j ) ) ) e. RR )
45	44	rexrd 9672	. 2 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( Q ` ( I ` ( S ` j ) ) ) e. RR* )
46	16	adantr 463	. . . . . 6 |- ( ( ph /\ j e. ( 0..^ N ) ) -> I : RR --> ( 0..^ M ) )
47	46, 42	ffvelrnd 6009	. . . . 5 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( I ` ( S ` j ) ) e. ( 0..^ M ) )
48		fzofzp1 11944	. . . . 5 |- ( ( I ` ( S ` j ) ) e. ( 0..^ M ) -> ( ( I ` ( S ` j ) ) + 1 ) e. ( 0 ... M ) )
49	47, 48	syl 17	. . . 4 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( I ` ( S ` j ) ) + 1 ) e. ( 0 ... M ) )
50	10, 49	ffvelrnd 6009	. . 3 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) e. RR )
51	50	rexrd 9672	. 2 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) e. RR* )
52	14	a1i 11	. . . . 5 |- ( ( ph /\ j e. ( 0..^ N ) ) -> I = ( x e. RR |-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) ) )
53		fveq2 5848	. . . . . . . . . 10 |- ( x = ( S ` j ) -> ( E ` x ) = ( E ` ( S ` j ) ) )
54	53	fveq2d 5852	. . . . . . . . 9 |- ( x = ( S ` j ) -> ( L ` ( E ` x ) ) = ( L ` ( E ` ( S ` j ) ) ) )
55	54	breq2d 4406	. . . . . . . 8 |- ( x = ( S ` j ) -> ( ( Q ` i ) <_ ( L ` ( E ` x ) ) <-> ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) ) )
56	55	rabbidv 3050	. . . . . . 7 |- ( x = ( S ` j ) -> { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } = { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } )
57	56	supeq1d 7938	. . . . . 6 |- ( x = ( S ` j ) -> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) = sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) )
58	57	adantl 464	. . . . 5 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ x = ( S ` j ) ) -> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) = sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) )
59		ltso 9695	. . . . . . 7 |- < Or RR
60	59	supex 7955	. . . . . 6 |- sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) e. _V
61	60	a1i 11	. . . . 5 |- ( ( ph /\ j e. ( 0..^ N ) ) -> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) e. _V )
62	52, 58, 42, 61	fvmptd 5937	. . . 4 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( I ` ( S ` j ) ) = sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) )
63	62	fveq2d 5852	. . 3 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( Q ` ( I ` ( S ` j ) ) ) = ( Q ` sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) ) )
64		simpl 455	. . . . . . 7 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ph )
65	64, 42	jca 530	. . . . . 6 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ph /\ ( S ` j ) e. RR ) )
66		eleq1 2474	. . . . . . . . 9 |- ( x = ( S ` j ) -> ( x e. RR <-> ( S ` j ) e. RR ) )
67	66	anbi2d 702	. . . . . . . 8 |- ( x = ( S ` j ) -> ( ( ph /\ x e. RR ) <-> ( ph /\ ( S ` j ) e. RR ) ) )
68	57, 56	eleq12d 2484	. . . . . . . 8 |- ( x = ( S ` j ) -> ( sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) e. { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } <-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) e. { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } ) )
69	67, 68	imbi12d 318	. . . . . . 7 |- ( x = ( S ` j ) -> ( ( ( ph /\ x e. RR ) -> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) e. { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } ) <-> ( ( ph /\ ( S ` j ) e. RR ) -> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) e. { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } ) ) )
70	15	simprd 461	. . . . . . . 8 |- ( ph -> ( x e. RR -> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) e. { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } ) )
71	70	imp 427	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) e. { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } )
72	69, 71	vtoclg 3116	. . . . . 6 |- ( ( S ` j ) e. RR -> ( ( ph /\ ( S ` j ) e. RR ) -> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) e. { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } ) )
73	42, 65, 72	sylc 59	. . . . 5 |- ( ( ph /\ j e. ( 0..^ N ) ) -> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) e. { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } )
74		nfrab1 2987	. . . . . . 7 |- F/_ i { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) }
75		nfcv 2564	. . . . . . 7 |- F/_ i RR
76		nfcv 2564	. . . . . . 7 |- F/_ i <
77	74, 75, 76	nfsup 7943	. . . . . 6 |- F/_ i sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < )
78		nfcv 2564	. . . . . 6 |- F/_ i ( 0..^ M )
79		nfcv 2564	. . . . . . . 8 |- F/_ i Q
80	79, 77	nffv 5855	. . . . . . 7 |- F/_ i ( Q ` sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) )
81		nfcv 2564	. . . . . . 7 |- F/_ i <_
82		nfcv 2564	. . . . . . 7 |- F/_ i ( L ` ( E ` ( S ` j ) ) )
83	80, 81, 82	nfbr 4438	. . . . . 6 |- F/ i ( Q ` sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) ) <_ ( L ` ( E ` ( S ` j ) ) )
84		fveq2 5848	. . . . . . 7 |- ( i = sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) -> ( Q ` i ) = ( Q ` sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) ) )
85	84	breq1d 4404	. . . . . 6 |- ( i = sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) -> ( ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) <-> ( Q ` sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) )
86	77, 78, 83, 85	elrabf 3204	. . . . 5 |- ( sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) e. { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } <-> ( sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) e. ( 0..^ M ) /\ ( Q ` sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) )
87	73, 86	sylib 196	. . . 4 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) e. ( 0..^ M ) /\ ( Q ` sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) )
88	87	simprd 461	. . 3 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( Q ` sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) ) <_ ( L ` ( E ` ( S ` j ) ) ) )
89	63, 88	eqbrtrd 4414	. 2 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( Q ` ( I ` ( S ` j ) ) ) <_ ( L ` ( E ` ( S ` j ) ) ) )
90	2	ad2antrr 724	. . . . 5 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> M e. NN )
91	1	ad2antrr 724	. . . . 5 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> Q e. ( P ` M ) )
92	21	ad2antrr 724	. . . . 5 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> C e. RR )
93	22	ad2antrr 724	. . . . 5 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> D e. RR )
94	23	ad2antrr 724	. . . . 5 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> C < D )
95		0le1 10115	. . . . . . . 8 |- 0 <_ 1
96	95	a1i 11	. . . . . . 7 |- ( ph -> 0 <_ 1 )
97	2	nnge1d 10618	. . . . . . 7 |- ( ph -> 1 <_ M )
98		1zzd 10935	. . . . . . . 8 |- ( ph -> 1 e. ZZ )
99		0zd 10916	. . . . . . . 8 |- ( ph -> 0 e. ZZ )
100	2	nnzd 11006	. . . . . . . 8 |- ( ph -> M e. ZZ )
101		elfz 11730	. . . . . . . 8 |- ( ( 1 e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( 1 e. ( 0 ... M ) <-> ( 0 <_ 1 /\ 1 <_ M ) ) )
102	98, 99, 100, 101	syl3anc 1230	. . . . . . 7 |- ( ph -> ( 1 e. ( 0 ... M ) <-> ( 0 <_ 1 /\ 1 <_ M ) ) )
103	96, 97, 102	mpbir2and 923	. . . . . 6 |- ( ph -> 1 e. ( 0 ... M ) )
104	103	ad2antrr 724	. . . . 5 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> 1 e. ( 0 ... M ) )
105		simplr 754	. . . . 5 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> j e. ( 0..^ N ) )
106		fourierdlem79.z	. . . . . . . 8 |- Z = ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) )
107		fzofzp1 11944	. . . . . . . . . . . . . 14 |- ( j e. ( 0..^ N ) -> ( j + 1 ) e. ( 0 ... N ) )
108	107	adantl 464	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( j + 1 ) e. ( 0 ... N ) )
109	39, 108	ffvelrnd 6009	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( S ` ( j + 1 ) ) e. RR )
110	109, 42	resubcld 10027	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) e. RR )
111	110	rehalfcld 10825	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) e. RR )
112	9, 103	ffvelrnd 6009	. . . . . . . . . . . . 13 |- ( ph -> ( Q ` 1 ) e. RR )
113	3, 2, 1	fourierdlem11 37249	. . . . . . . . . . . . . 14 |- ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
114	113	simp1d 1009	. . . . . . . . . . . . 13 |- ( ph -> A e. RR )
115	112, 114	resubcld 10027	. . . . . . . . . . . 12 |- ( ph -> ( ( Q ` 1 ) - A ) e. RR )
116	115	rehalfcld 10825	. . . . . . . . . . 11 |- ( ph -> ( ( ( Q ` 1 ) - A ) / 2 ) e. RR )
117	116	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( Q ` 1 ) - A ) / 2 ) e. RR )
118	111, 117	ifcld 3927	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ N ) ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) e. RR )
119	42, 118	readdcld 9652	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) e. RR )
120	106, 119	syl5eqel 2494	. . . . . . 7 |- ( ( ph /\ j e. ( 0..^ N ) ) -> Z e. RR )
121		2re 10645	. . . . . . . . . . . . . 14 |- 2 e. RR
122	121	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> 2 e. RR )
123		elfzoelz 11857	. . . . . . . . . . . . . . . . . 18 |- ( j e. ( 0..^ N ) -> j e. ZZ )
124	123	zred 11007	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0..^ N ) -> j e. RR )
125	124	ltp1d 10515	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0..^ N ) -> j < ( j + 1 ) )
126	125	adantl 464	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0..^ N ) ) -> j < ( j + 1 ) )
127	28	simprd 461	. . . . . . . . . . . . . . . . 17 |- ( ph -> S Isom < , < ( ( 0 ... N ) , H ) )
128	127	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 0..^ N ) ) -> S Isom < , < ( ( 0 ... N ) , H ) )
129		isorel 6204	. . . . . . . . . . . . . . . 16 |- ( ( S Isom < , < ( ( 0 ... N ) , H ) /\ ( j e. ( 0 ... N ) /\ ( j + 1 ) e. ( 0 ... N ) ) ) -> ( j < ( j + 1 ) <-> ( S ` j ) < ( S ` ( j + 1 ) ) ) )
130	128, 41, 108, 129	syl12anc 1228	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( j < ( j + 1 ) <-> ( S ` j ) < ( S ` ( j + 1 ) ) ) )
131	126, 130	mpbid 210	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( S ` j ) < ( S ` ( j + 1 ) ) )
132	42, 109	posdifd 10178	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( S ` j ) < ( S ` ( j + 1 ) ) <-> 0 < ( ( S ` ( j + 1 ) ) - ( S ` j ) ) ) )
133	131, 132	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> 0 < ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
134		2pos 10667	. . . . . . . . . . . . . 14 |- 0 < 2
135	134	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> 0 < 2 )
136	110, 122, 133, 135	divgt0d 10520	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0..^ N ) ) -> 0 < ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) )
137	111, 136	elrpd 11300	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) e. RR+ )
138	121	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> 2 e. RR )
139	2	nngt0d 10619	. . . . . . . . . . . . . . . . . 18 |- ( ph -> 0 < M )
140		fzolb 11863	. . . . . . . . . . . . . . . . . 18 |- ( 0 e. ( 0..^ M ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
141	99, 100, 139, 140	syl3anbrc 1181	. . . . . . . . . . . . . . . . 17 |- ( ph -> 0 e. ( 0..^ M ) )
142		0re 9625	. . . . . . . . . . . . . . . . . 18 |- 0 e. RR
143		eleq1 2474	. . . . . . . . . . . . . . . . . . . . 21 |- ( i = 0 -> ( i e. ( 0..^ M ) <-> 0 e. ( 0..^ M ) ) )
144	143	anbi2d 702	. . . . . . . . . . . . . . . . . . . 20 |- ( i = 0 -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ 0 e. ( 0..^ M ) ) ) )
145		fveq2 5848	. . . . . . . . . . . . . . . . . . . . 21 |- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
146		oveq1 6284	. . . . . . . . . . . . . . . . . . . . . 22 |- ( i = 0 -> ( i + 1 ) = ( 0 + 1 ) )
147	146	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . 21 |- ( i = 0 -> ( Q ` ( i + 1 ) ) = ( Q ` ( 0 + 1 ) ) )
148	145, 147	breq12d 4407	. . . . . . . . . . . . . . . . . . . 20 |- ( i = 0 -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
149	144, 148	imbi12d 318	. . . . . . . . . . . . . . . . . . 19 |- ( i = 0 -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ 0 e. ( 0..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) ) )
150	6	simprd 461	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
151	150	simprd 461	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
152	151	r19.21bi 2772	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
153	149, 152	vtoclg 3116	. . . . . . . . . . . . . . . . . 18 |- ( 0 e. RR -> ( ( ph /\ 0 e. ( 0..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
154	142, 153	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ 0 e. ( 0..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
155	141, 154	mpdan 666	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
156	150	simpld 457	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
157	156	simpld 457	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Q ` 0 ) = A )
158		0p1e1 10687	. . . . . . . . . . . . . . . . . 18 |- ( 0 + 1 ) = 1
159	158	fveq2i 5851	. . . . . . . . . . . . . . . . 17 |- ( Q ` ( 0 + 1 ) ) = ( Q ` 1 )
160	159	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Q ` ( 0 + 1 ) ) = ( Q ` 1 ) )
161	155, 157, 160	3brtr3d 4423	. . . . . . . . . . . . . . 15 |- ( ph -> A < ( Q ` 1 ) )
162	114, 112	posdifd 10178	. . . . . . . . . . . . . . 15 |- ( ph -> ( A < ( Q ` 1 ) <-> 0 < ( ( Q ` 1 ) - A ) ) )
163	161, 162	mpbid 210	. . . . . . . . . . . . . 14 |- ( ph -> 0 < ( ( Q ` 1 ) - A ) )
164	134	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> 0 < 2 )
165	115, 138, 163, 164	divgt0d 10520	. . . . . . . . . . . . 13 |- ( ph -> 0 < ( ( ( Q ` 1 ) - A ) / 2 ) )
166	116, 165	elrpd 11300	. . . . . . . . . . . 12 |- ( ph -> ( ( ( Q ` 1 ) - A ) / 2 ) e. RR+ )
167	166	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( Q ` 1 ) - A ) / 2 ) e. RR+ )
168	137, 167	ifcld 3927	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ N ) ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) e. RR+ )
169	42, 168	ltaddrpd 11332	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( S ` j ) < ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) )
170	42, 119, 169	ltled 9764	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( S ` j ) <_ ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) )
171	170, 106	syl6breqr 4434	. . . . . . 7 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( S ` j ) <_ Z )
172	42, 111	readdcld 9652	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( S ` j ) + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) e. RR )
173		iftrue 3890	. . . . . . . . . . . . 13 |- ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) = ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) )
174	173	adantl 464	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) = ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) )
175	111	leidd 10158	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) <_ ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) )
176	175	adantr 463	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) <_ ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) )
177	174, 176	eqbrtrd 4414	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) <_ ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) )
178		iffalse 3893	. . . . . . . . . . . . 13 |- ( -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) = ( ( ( Q ` 1 ) - A ) / 2 ) )
179	178	adantl 464	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) = ( ( ( Q ` 1 ) - A ) / 2 ) )
180	115	ad2antrr 724	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( Q ` 1 ) - A ) e. RR )
181	110	adantr 463	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) e. RR )
182		2rp 11269	. . . . . . . . . . . . . 14 |- 2 e. RR+
183	182	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> 2 e. RR+ )
184		simpr 459	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) )
185	180, 181, 184	nltled 9766	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( Q ` 1 ) - A ) <_ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
186	180, 181, 183, 185	lediv1dd 11357	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( ( Q ` 1 ) - A ) / 2 ) <_ ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) )
187	179, 186	eqbrtrd 4414	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) <_ ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) )
188	177, 187	pm2.61dan 792	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ N ) ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) <_ ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) )
189	118, 111, 42, 188	leadd2dd 10206	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) <_ ( ( S ` j ) + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) )
190	42	recnd 9651	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( S ` j ) e. CC )
191	109	recnd 9651	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( S ` ( j + 1 ) ) e. CC )
192	190, 191	addcomd 9815	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( S ` j ) + ( S ` ( j + 1 ) ) ) = ( ( S ` ( j + 1 ) ) + ( S ` j ) ) )
193	192	oveq1d 6292	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) = ( ( ( S ` ( j + 1 ) ) + ( S ` j ) ) / 2 ) )
194	193	oveq1d 6292	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) - ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) = ( ( ( ( S ` ( j + 1 ) ) + ( S ` j ) ) / 2 ) - ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) )
195		halfaddsub 10812	. . . . . . . . . . . . . . 15 |- ( ( ( S ` ( j + 1 ) ) e. CC /\ ( S ` j ) e. CC ) -> ( ( ( ( ( S ` ( j + 1 ) ) + ( S ` j ) ) / 2 ) + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) = ( S ` ( j + 1 ) ) /\ ( ( ( ( S ` ( j + 1 ) ) + ( S ` j ) ) / 2 ) - ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) = ( S ` j ) ) )
196	191, 190, 195	syl2anc 659	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( ( ( S ` ( j + 1 ) ) + ( S ` j ) ) / 2 ) + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) = ( S ` ( j + 1 ) ) /\ ( ( ( ( S ` ( j + 1 ) ) + ( S ` j ) ) / 2 ) - ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) = ( S ` j ) ) )
197	196	simprd 461	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( ( S ` ( j + 1 ) ) + ( S ` j ) ) / 2 ) - ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) = ( S ` j ) )
198	194, 197	eqtrd 2443	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) - ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) = ( S ` j ) )
199	190, 191	addcld 9644	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( S ` j ) + ( S ` ( j + 1 ) ) ) e. CC )
200	199	halfcld 10823	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) e. CC )
201	111	recnd 9651	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) e. CC )
202	200, 201, 190	subsub23d 36827	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) - ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) = ( S ` j ) <-> ( ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) - ( S ` j ) ) = ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) )
203	198, 202	mpbid 210	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) - ( S ` j ) ) = ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) )
204	200, 190, 201	subaddd 9984	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) - ( S ` j ) ) = ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) <-> ( ( S ` j ) + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) = ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) ) )
205	203, 204	mpbid 210	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( S ` j ) + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) = ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) )
206		avglt2 10817	. . . . . . . . . . . 12 |- ( ( ( S ` j ) e. RR /\ ( S ` ( j + 1 ) ) e. RR ) -> ( ( S ` j ) < ( S ` ( j + 1 ) ) <-> ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) < ( S ` ( j + 1 ) ) ) )
207	42, 109, 206	syl2anc 659	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( S ` j ) < ( S ` ( j + 1 ) ) <-> ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) < ( S ` ( j + 1 ) ) ) )
208	131, 207	mpbid 210	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) < ( S ` ( j + 1 ) ) )
209	205, 208	eqbrtrd 4414	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( S ` j ) + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) < ( S ` ( j + 1 ) ) )
210	119, 172, 109, 189, 209	lelttrd 9773	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) < ( S ` ( j + 1 ) ) )
211	106, 210	syl5eqbr 4427	. . . . . . 7 |- ( ( ph /\ j e. ( 0..^ N ) ) -> Z < ( S ` ( j + 1 ) ) )
212	109	rexrd 9672	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( S ` ( j + 1 ) ) e. RR* )
213		elico2 11640	. . . . . . . 8 |- ( ( ( S ` j ) e. RR /\ ( S ` ( j + 1 ) ) e. RR* ) -> ( Z e. ( ( S ` j ) [,) ( S ` ( j + 1 ) ) ) <-> ( Z e. RR /\ ( S ` j ) <_ Z /\ Z < ( S ` ( j + 1 ) ) ) ) )
214	42, 212, 213	syl2anc 659	. . . . . . 7 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( Z e. ( ( S ` j ) [,) ( S ` ( j + 1 ) ) ) <-> ( Z e. RR /\ ( S ` j ) <_ Z /\ Z < ( S ` ( j + 1 ) ) ) ) )
215	120, 171, 211, 214	mpbir3and 1180	. . . . . 6 |- ( ( ph /\ j e. ( 0..^ N ) ) -> Z e. ( ( S ` j ) [,) ( S ` ( j + 1 ) ) ) )
216	215	adantr 463	. . . . 5 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> Z e. ( ( S ` j ) [,) ( S ` ( j + 1 ) ) ) )
217	114	ad2antrr 724	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> A e. RR )
218	113	simp2d 1010	. . . . . . . . 9 |- ( ph -> B e. RR )
219	218	ad2antrr 724	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> B e. RR )
220	113	simp3d 1011	. . . . . . . . 9 |- ( ph -> A < B )
221	220	ad2antrr 724	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> A < B )
222	42	adantr 463	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( S ` j ) e. RR )
223		simpr 459	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) = B )
224	169, 106	syl6breqr 4434	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( S ` j ) < Z )
225	218, 114	resubcld 10027	. . . . . . . . . . . . . 14 |- ( ph -> ( B - A ) e. RR )
226	11, 225	syl5eqel 2494	. . . . . . . . . . . . 13 |- ( ph -> T e. RR )
227	226	adantr 463	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0..^ N ) ) -> T e. RR )
228	111	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) e. RR )
229	116	ad2antrr 724	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( ( Q ` 1 ) - A ) / 2 ) e. RR )
230	110	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) e. RR )
231	115	ad2antrr 724	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( Q ` 1 ) - A ) e. RR )
232	182	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> 2 e. RR+ )
233		simpr 459	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) )
234	230, 231, 232, 233	ltdiv1dd 11356	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) < ( ( ( Q ` 1 ) - A ) / 2 ) )
235	228, 229, 234	ltled 9764	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) <_ ( ( ( Q ` 1 ) - A ) / 2 ) )
236	174, 235	eqbrtrd 4414	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) <_ ( ( ( Q ` 1 ) - A ) / 2 ) )
237	178	adantl 464	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) = ( ( ( Q ` 1 ) - A ) / 2 ) )
238	116	leidd 10158	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( Q ` 1 ) - A ) / 2 ) <_ ( ( ( Q ` 1 ) - A ) / 2 ) )
239	238	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( ( Q ` 1 ) - A ) / 2 ) <_ ( ( ( Q ` 1 ) - A ) / 2 ) )
240	237, 239	eqbrtrd 4414	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) <_ ( ( ( Q ` 1 ) - A ) / 2 ) )
241	240	adantlr 713	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) <_ ( ( ( Q ` 1 ) - A ) / 2 ) )
242	236, 241	pm2.61dan 792	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) <_ ( ( ( Q ` 1 ) - A ) / 2 ) )
243	225	rehalfcld 10825	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B - A ) / 2 ) e. RR )
244	182	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> 2 e. RR+ )
245	114	rexrd 9672	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A e. RR* )
246	218	rexrd 9672	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> B e. RR* )
247	3, 2, 1	fourierdlem15 37253	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
248	247, 103	ffvelrnd 6009	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( Q ` 1 ) e. ( A [,] B ) )
249		iccleub 11632	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. RR* /\ B e. RR* /\ ( Q ` 1 ) e. ( A [,] B ) ) -> ( Q ` 1 ) <_ B )
250	245, 246, 248, 249	syl3anc 1230	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( Q ` 1 ) <_ B )
251	112, 218, 114, 250	lesub1dd 10207	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( Q ` 1 ) - A ) <_ ( B - A ) )
252	115, 225, 244, 251	lediv1dd 11357	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( Q ` 1 ) - A ) / 2 ) <_ ( ( B - A ) / 2 ) )
253	11	eqcomi 2415	. . . . . . . . . . . . . . . . . 18 |- ( B - A ) = T
254	253	oveq1i 6287	. . . . . . . . . . . . . . . . 17 |- ( ( B - A ) / 2 ) = ( T / 2 )
255	114, 218	posdifd 10178	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
256	220, 255	mpbid 210	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> 0 < ( B - A ) )
257	256, 11	syl6breqr 4434	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> 0 < T )
258	226, 257	elrpd 11300	. . . . . . . . . . . . . . . . . 18 |- ( ph -> T e. RR+ )
259		rphalflt 11291	. . . . . . . . . . . . . . . . . 18 |- ( T e. RR+ -> ( T / 2 ) < T )
260	258, 259	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( T / 2 ) < T )
261	254, 260	syl5eqbr 4427	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B - A ) / 2 ) < T )
262	116, 243, 226, 252, 261	lelttrd 9773	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( Q ` 1 ) - A ) / 2 ) < T )
263	116, 226, 262	ltled 9764	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( Q ` 1 ) - A ) / 2 ) <_ T )
264	263	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( Q ` 1 ) - A ) / 2 ) <_ T )
265	118, 117, 227, 242, 264	letrd 9772	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0..^ N ) ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) <_ T )
266	118, 227, 42, 265	leadd2dd 10206	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) <_ ( ( S ` j ) + T ) )
267	106, 266	syl5eqbr 4427	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ N ) ) -> Z <_ ( ( S ` j ) + T ) )
268	42	rexrd 9672	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( S ` j ) e. RR* )
269	42, 227	readdcld 9652	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( S ` j ) + T ) e. RR )
270		elioc2 11639	. . . . . . . . . . 11 |- ( ( ( S ` j ) e. RR* /\ ( ( S ` j ) + T ) e. RR ) -> ( Z e. ( ( S ` j ) (,] ( ( S ` j ) + T ) ) <-> ( Z e. RR /\ ( S ` j ) < Z /\ Z <_ ( ( S ` j ) + T ) ) ) )
271	268, 269, 270	syl2anc 659	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( Z e. ( ( S ` j ) (,] ( ( S ` j ) + T ) ) <-> ( Z e. RR /\ ( S ` j ) < Z /\ Z <_ ( ( S ` j ) + T ) ) ) )
272	120, 224, 267, 271	mpbir3and 1180	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ N ) ) -> Z e. ( ( S ` j ) (,] ( ( S ` j ) + T ) ) )
273	272	adantr 463	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> Z e. ( ( S ` j ) (,] ( ( S ` j ) + T ) ) )
274	217, 219, 221, 11, 12, 222, 223, 273	fourierdlem26 37264	. . . . . . 7 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` Z ) = ( A + ( Z - ( S ` j ) ) ) )
275	106	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ N ) ) -> Z = ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) )
276	275	oveq1d 6292	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( Z - ( S ` j ) ) = ( ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) - ( S ` j ) ) )
277	276	oveq2d 6293	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( A + ( Z - ( S ` j ) ) ) = ( A + ( ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) - ( S ` j ) ) ) )
278	277	adantr 463	. . . . . . 7 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( A + ( Z - ( S ` j ) ) ) = ( A + ( ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) - ( S ` j ) ) ) )
279	118	recnd 9651	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ N ) ) -> if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) e. CC )
280	190, 279	pncan2d 9968	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) - ( S ` j ) ) = if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) )
281	280	oveq2d 6293	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( A + ( ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) - ( S ` j ) ) ) = ( A + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) )
282	281	adantr 463	. . . . . . 7 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( A + ( ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) - ( S ` j ) ) ) = ( A + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) )
283	274, 278, 282	3eqtrd 2447	. . . . . 6 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` Z ) = ( A + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) )
284	173	oveq2d 6293	. . . . . . . . . 10 |- ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) -> ( A + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) = ( A + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) )
285	284	adantl 464	. . . . . . . . 9 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) = ( A + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) )
286	114	adantr 463	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0..^ N ) ) -> A e. RR )
287	286, 111	readdcld 9652	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( A + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) e. RR )
288	287	adantr 463	. . . . . . . . . 10 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) e. RR )
289	286, 117	readdcld 9652	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) e. RR )
290	289	adantr 463	. . . . . . . . . 10 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) e. RR )
291	112	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( Q ` 1 ) e. RR )
292	114	ad2antrr 724	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> A e. RR )
293	228, 229, 292, 234	ltadd2dd 9774	. . . . . . . . . 10 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) < ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) )
294	112	recnd 9651	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Q ` 1 ) e. CC )
295	114	recnd 9651	. . . . . . . . . . . . . . . 16 |- ( ph -> A e. CC )
296		halfaddsub 10812	. . . . . . . . . . . . . . . 16 |- ( ( ( Q ` 1 ) e. CC /\ A e. CC ) -> ( ( ( ( ( Q ` 1 ) + A ) / 2 ) + ( ( ( Q ` 1 ) - A ) / 2 ) ) = ( Q ` 1 ) /\ ( ( ( ( Q ` 1 ) + A ) / 2 ) - ( ( ( Q ` 1 ) - A ) / 2 ) ) = A ) )
297	294, 295, 296	syl2anc 659	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( ( ( Q ` 1 ) + A ) / 2 ) + ( ( ( Q ` 1 ) - A ) / 2 ) ) = ( Q ` 1 ) /\ ( ( ( ( Q ` 1 ) + A ) / 2 ) - ( ( ( Q ` 1 ) - A ) / 2 ) ) = A ) )
298	297	simprd 461	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( ( Q ` 1 ) + A ) / 2 ) - ( ( ( Q ` 1 ) - A ) / 2 ) ) = A )
299	298	oveq1d 6292	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( ( ( Q ` 1 ) + A ) / 2 ) - ( ( ( Q ` 1 ) - A ) / 2 ) ) + ( ( ( Q ` 1 ) - A ) / 2 ) ) = ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) )
300	112, 114	readdcld 9652	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( Q ` 1 ) + A ) e. RR )
301	300	rehalfcld 10825	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( Q ` 1 ) + A ) / 2 ) e. RR )
302	301	recnd 9651	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( Q ` 1 ) + A ) / 2 ) e. CC )
303	116	recnd 9651	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( Q ` 1 ) - A ) / 2 ) e. CC )
304	302, 303	npcand 9970	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( ( ( Q ` 1 ) + A ) / 2 ) - ( ( ( Q ` 1 ) - A ) / 2 ) ) + ( ( ( Q ` 1 ) - A ) / 2 ) ) = ( ( ( Q ` 1 ) + A ) / 2 ) )
305	299, 304	eqtr3d 2445	. . . . . . . . . . . 12 |- ( ph -> ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) = ( ( ( Q ` 1 ) + A ) / 2 ) )
306	112, 112	readdcld 9652	. . . . . . . . . . . . . 14 |- ( ph -> ( ( Q ` 1 ) + ( Q ` 1 ) ) e. RR )
307	114, 112, 112, 161	ltadd2dd 9774	. . . . . . . . . . . . . 14 |- ( ph -> ( ( Q ` 1 ) + A ) < ( ( Q ` 1 ) + ( Q ` 1 ) ) )
308	300, 306, 244, 307	ltdiv1dd 11356	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( Q ` 1 ) + A ) / 2 ) < ( ( ( Q ` 1 ) + ( Q ` 1 ) ) / 2 ) )
309	294	2timesd 10821	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 2 x. ( Q ` 1 ) ) = ( ( Q ` 1 ) + ( Q ` 1 ) ) )
310	309	eqcomd 2410	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( Q ` 1 ) + ( Q ` 1 ) ) = ( 2 x. ( Q ` 1 ) ) )
311	310	oveq1d 6292	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( Q ` 1 ) + ( Q ` 1 ) ) / 2 ) = ( ( 2 x. ( Q ` 1 ) ) / 2 ) )
312		2cnd 10648	. . . . . . . . . . . . . . 15 |- ( ph -> 2 e. CC )
313		2ne0 10668	. . . . . . . . . . . . . . . 16 |- 2 =/= 0
314	313	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 2 =/= 0 )
315	294, 312, 314	divcan3d 10365	. . . . . . . . . . . . . 14 |- ( ph -> ( ( 2 x. ( Q ` 1 ) ) / 2 ) = ( Q ` 1 ) )
316	311, 315	eqtrd 2443	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( Q ` 1 ) + ( Q ` 1 ) ) / 2 ) = ( Q ` 1 ) )
317	308, 316	breqtrd 4418	. . . . . . . . . . . 12 |- ( ph -> ( ( ( Q ` 1 ) + A ) / 2 ) < ( Q ` 1 ) )
318	305, 317	eqbrtrd 4414	. . . . . . . . . . 11 |- ( ph -> ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) < ( Q ` 1 ) )
319	318	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) < ( Q ` 1 ) )
320	288, 290, 291, 293, 319	lttrd 9776	. . . . . . . . 9 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) < ( Q ` 1 ) )
321	285, 320	eqbrtrd 4414	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) < ( Q ` 1 ) )
322	178	oveq2d 6293	. . . . . . . . . 10 |- ( -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) -> ( A + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) = ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) )
323	322	adantl 464	. . . . . . . . 9 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) = ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) )
324	318	ad2antrr 724	. . . . . . . . 9 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) < ( Q ` 1 ) )
325	323, 324	eqbrtrd 4414	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) < ( Q ` 1 ) )
326	321, 325	pm2.61dan 792	. . . . . . 7 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( A + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) < ( Q ` 1 ) )
327	326	adantr 463	. . . . . 6 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( A + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) < ( Q ` 1 ) )
328	283, 327	eqbrtrd 4414	. . . . 5 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` Z ) < ( Q ` 1 ) )
329		eqid 2402	. . . . 5 |- ( ( Q ` 1 ) - ( ( E ` Z ) - Z ) ) = ( ( Q ` 1 ) - ( ( E ` Z ) - Z ) )
330	11, 3, 90, 91, 92, 93, 94, 24, 25, 26, 27, 12, 104, 105, 216, 328, 329	fourierdlem63 37301	. . . 4 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` ( j + 1 ) ) ) <_ ( Q ` 1 ) )
331	14	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> I = ( x e. RR |-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) ) )
332	57	adantl 464	. . . . . . . . 9 |- ( ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) /\ x = ( S ` j ) ) -> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) = sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) )
333	60	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) e. _V )
334	331, 332, 222, 333	fvmptd 5937	. . . . . . . 8 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( I ` ( S ` j ) ) = sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) )
335		fveq2 5848	. . . . . . . . . . . . 13 |- ( ( E ` ( S ` j ) ) = B -> ( L ` ( E ` ( S ` j ) ) ) = ( L ` B ) )
336	13	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) )
337		iftrue 3890	. . . . . . . . . . . . . . 15 |- ( y = B -> if ( y = B , A , y ) = A )
338	337	adantl 464	. . . . . . . . . . . . . 14 |- ( ( ph /\ y = B ) -> if ( y = B , A , y ) = A )
339		ubioc1 11630	. . . . . . . . . . . . . . 15 |- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> B e. ( A (,] B ) )
340	245, 246, 220, 339	syl3anc 1230	. . . . . . . . . . . . . 14 |- ( ph -> B e. ( A (,] B ) )
341	336, 338, 340, 114	fvmptd 5937	. . . . . . . . . . . . 13 |- ( ph -> ( L ` B