Theorem fourierdlem79

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)

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

Proof

Step	Hyp	Ref	Expression
1		fourierdlem79.t	|- T = ( B - A )
2		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 ) ) ) } )
3		fourierdlem79.m	|- ( ph -> M e. NN )
4		fourierdlem79.q	|- ( ph -> Q e. ( P ` M ) )
5		fourierdlem79.c	|- ( ph -> C e. RR )
6		fourierdlem79.d	|- ( ph -> D e. RR )
7		fourierdlem79.cltd	|- ( ph -> C < D )
8		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 ) ) ) } )
9		fourierdlem79.h	|- H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
10		fourierdlem79.n	|- N = ( ( # ` H ) - 1 )
11		fourierdlem79.s	|- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
12		fourierdlem79.e	|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
13		fourierdlem79.l	|- L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
14		fourierdlem79.z	|- Z = ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) )
15		fourierdlem79.i	|- I = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) )
16	2	fourierdlem2	|- ( 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 ) ) ) ) ) )
17	3 16	syl	|- ( 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 ) ) ) ) ) )
18	4 17	mpbid	|- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
19	18	simpld	|- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
20		elmapi	|- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
21	19 20	syl	|- ( ph -> Q : ( 0 ... M ) --> RR )
22	21	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> Q : ( 0 ... M ) --> RR )
23	2 3 4 1 12 13 15	fourierdlem37	|- ( 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 ) ) } ) ) )
24	23	simpld	|- ( ph -> I : RR --> ( 0 ..^ M ) )
25		fzossfz	|- ( 0 ..^ M ) C_ ( 0 ... M )
26	25	a1i	|- ( ph -> ( 0 ..^ M ) C_ ( 0 ... M ) )
27	24 26	fssd	|- ( ph -> I : RR --> ( 0 ... M ) )
28	27	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> I : RR --> ( 0 ... M ) )
29	1 2 3 4 5 6 7 8 9 10 11	fourierdlem54	|- ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , H ) ) )
30	29	simpld	|- ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
31	30	simprd	|- ( ph -> S e. ( O ` N ) )
32	31	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> S e. ( O ` N ) )
33	30	simpld	|- ( ph -> N e. NN )
34	33	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> N e. NN )
35	8	fourierdlem2	|- ( 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 ) ) ) ) ) )
36	34 35	syl	|- ( ( 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 ) ) ) ) ) )
37	32 36	mpbid	|- ( ( 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 ) ) ) ) )
38	37	simpld	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> S e. ( RR ^m ( 0 ... N ) ) )
39		elmapi	|- ( S e. ( RR ^m ( 0 ... N ) ) -> S : ( 0 ... N ) --> RR )
40	38 39	syl	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> S : ( 0 ... N ) --> RR )
41		elfzofz	|- ( j e. ( 0 ..^ N ) -> j e. ( 0 ... N ) )
42	41	adantl	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> j e. ( 0 ... N ) )
43	40 42	ffvelrnd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) e. RR )
44	28 43	ffvelrnd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( I ` ( S ` j ) ) e. ( 0 ... M ) )
45	22 44	ffvelrnd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( Q ` ( I ` ( S ` j ) ) ) e. RR )
46	45	rexrd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( Q ` ( I ` ( S ` j ) ) ) e. RR* )
47	24	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> I : RR --> ( 0 ..^ M ) )
48	47 43	ffvelrnd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( I ` ( S ` j ) ) e. ( 0 ..^ M ) )
49		fzofzp1	|- ( ( I ` ( S ` j ) ) e. ( 0 ..^ M ) -> ( ( I ` ( S ` j ) ) + 1 ) e. ( 0 ... M ) )
50	48 49	syl	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( I ` ( S ` j ) ) + 1 ) e. ( 0 ... M ) )
51	22 50	ffvelrnd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) e. RR )
52	51	rexrd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) e. RR* )
53	15	a1i	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> I = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) ) )
54		fveq2	|- ( x = ( S ` j ) -> ( E ` x ) = ( E ` ( S ` j ) ) )
55	54	fveq2d	|- ( x = ( S ` j ) -> ( L ` ( E ` x ) ) = ( L ` ( E ` ( S ` j ) ) ) )
56	55	breq2d	|- ( x = ( S ` j ) -> ( ( Q ` i ) <_ ( L ` ( E ` x ) ) <-> ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) ) )
57	56	rabbidv	|- ( x = ( S ` j ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } = { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } )
58	57	supeq1d	|- ( 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	58	adantl	|- ( ( ( 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 , < ) )
60		ltso	|- < Or RR
61	60	supex	|- sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) e. _V
62	61	a1i	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) e. _V )
63	53 59 43 62	fvmptd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( I ` ( S ` j ) ) = sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) )
64	63	fveq2d	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( Q ` ( I ` ( S ` j ) ) ) = ( Q ` sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) ) )
65		simpl	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ph )
66	65 43	jca	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ph /\ ( S ` j ) e. RR ) )
67		eleq1	|- ( x = ( S ` j ) -> ( x e. RR <-> ( S ` j ) e. RR ) )
68	67	anbi2d	|- ( x = ( S ` j ) -> ( ( ph /\ x e. RR ) <-> ( ph /\ ( S ` j ) e. RR ) ) )
69	58 57	eleq12d	|- ( 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 ) ) ) } ) )
70	68 69	imbi12d	|- ( 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 ) ) ) } ) ) )
71	23	simprd	|- ( 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	71	imp	|- ( ( 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 ) ) } )
73	70 72	vtoclg	|- ( ( 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 ) ) ) } ) )
74	43 66 73	sylc	|- ( ( 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 ) ) ) } )
75		nfrab1	|- F/_ i { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) }
76		nfcv	|- F/_ i RR
77		nfcv	|- F/_ i <
78	75 76 77	nfsup	|- F/_ i sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < )
79		nfcv	|- F/_ i ( 0 ..^ M )
80		nfcv	|- F/_ i Q
81	80 78	nffv	|- F/_ i ( Q ` sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) )
82		nfcv	|- F/_ i <_
83		nfcv	|- F/_ i ( L ` ( E ` ( S ` j ) ) )
84	81 82 83	nfbr	|- F/ i ( Q ` sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) ) <_ ( L ` ( E ` ( S ` j ) ) )
85		fveq2	|- ( 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 , < ) ) )
86	85	breq1d	|- ( 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 ) ) ) ) )
87	78 79 84 86	elrabf	|- ( 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 ) ) ) ) )
88	74 87	sylib	|- ( ( 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 ) ) ) ) )
89	88	simprd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( Q ` sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) ) <_ ( L ` ( E ` ( S ` j ) ) ) )
90	64 89	eqbrtrd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( Q ` ( I ` ( S ` j ) ) ) <_ ( L ` ( E ` ( S ` j ) ) ) )
91	3	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> M e. NN )
92	4	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> Q e. ( P ` M ) )
93	5	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> C e. RR )
94	6	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> D e. RR )
95	7	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> C < D )
96		0zd	|- ( ph -> 0 e. ZZ )
97	3	nnzd	|- ( ph -> M e. ZZ )
98		1zzd	|- ( ph -> 1 e. ZZ )
99		0le1	|- 0 <_ 1
100	99	a1i	|- ( ph -> 0 <_ 1 )
101	3	nnge1d	|- ( ph -> 1 <_ M )
102	96 97 98 100 101	elfzd	|- ( ph -> 1 e. ( 0 ... M ) )
103	102	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> 1 e. ( 0 ... M ) )
104		simplr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> j e. ( 0 ..^ N ) )
105		fzofzp1	|- ( j e. ( 0 ..^ N ) -> ( j + 1 ) e. ( 0 ... N ) )
106	105	adantl	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( j + 1 ) e. ( 0 ... N ) )
107	40 106	ffvelrnd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` ( j + 1 ) ) e. RR )
108	107 43	resubcld	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) e. RR )
109	108	rehalfcld	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) e. RR )
110	21 102	ffvelrnd	|- ( ph -> ( Q ` 1 ) e. RR )
111	2 3 4	fourierdlem11	|- ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
112	111	simp1d	|- ( ph -> A e. RR )
113	110 112	resubcld	|- ( ph -> ( ( Q ` 1 ) - A ) e. RR )
114	113	rehalfcld	|- ( ph -> ( ( ( Q ` 1 ) - A ) / 2 ) e. RR )
115	114	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( Q ` 1 ) - A ) / 2 ) e. RR )
116	109 115	ifcld	|- ( ( 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 )
117	43 116	readdcld	|- ( ( 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 )
118	14 117	eqeltrid	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> Z e. RR )
119		2re	|- 2 e. RR
120	119	a1i	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> 2 e. RR )
121		elfzoelz	|- ( j e. ( 0 ..^ N ) -> j e. ZZ )
122	121	zred	|- ( j e. ( 0 ..^ N ) -> j e. RR )
123	122	ltp1d	|- ( j e. ( 0 ..^ N ) -> j < ( j + 1 ) )
124	123	adantl	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> j < ( j + 1 ) )
125	29	simprd	|- ( ph -> S Isom < , < ( ( 0 ... N ) , H ) )
126	125	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> S Isom < , < ( ( 0 ... N ) , H ) )
127		isorel	|- ( ( S Isom < , < ( ( 0 ... N ) , H ) /\ ( j e. ( 0 ... N ) /\ ( j + 1 ) e. ( 0 ... N ) ) ) -> ( j < ( j + 1 ) <-> ( S ` j ) < ( S ` ( j + 1 ) ) ) )
128	126 42 106 127	syl12anc	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( j < ( j + 1 ) <-> ( S ` j ) < ( S ` ( j + 1 ) ) ) )
129	124 128	mpbid	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) < ( S ` ( j + 1 ) ) )
130	43 107	posdifd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) < ( S ` ( j + 1 ) ) <-> 0 < ( ( S ` ( j + 1 ) ) - ( S ` j ) ) ) )
131	129 130	mpbid	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> 0 < ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
132		2pos	|- 0 < 2
133	132	a1i	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> 0 < 2 )
134	108 120 131 133	divgt0d	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> 0 < ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) )
135	109 134	elrpd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) e. RR+ )
136	119	a1i	|- ( ph -> 2 e. RR )
137	3	nngt0d	|- ( ph -> 0 < M )
138		fzolb	|- ( 0 e. ( 0 ..^ M ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
139	96 97 137 138	syl3anbrc	|- ( ph -> 0 e. ( 0 ..^ M ) )
140		0re	|- 0 e. RR
141		eleq1	|- ( i = 0 -> ( i e. ( 0 ..^ M ) <-> 0 e. ( 0 ..^ M ) ) )
142	141	anbi2d	|- ( i = 0 -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ 0 e. ( 0 ..^ M ) ) ) )
143		fveq2	|- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
144		oveq1	|- ( i = 0 -> ( i + 1 ) = ( 0 + 1 ) )
145	144	fveq2d	|- ( i = 0 -> ( Q ` ( i + 1 ) ) = ( Q ` ( 0 + 1 ) ) )
146	143 145	breq12d	|- ( i = 0 -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
147	142 146	imbi12d	|- ( i = 0 -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) ) )
148	18	simprd	|- ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
149	148	simprd	|- ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
150	149	r19.21bi	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
151	147 150	vtoclg	|- ( 0 e. RR -> ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
152	140 151	ax-mp	|- ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
153	139 152	mpdan	|- ( ph -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
154	148	simpld	|- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
155	154	simpld	|- ( ph -> ( Q ` 0 ) = A )
156		0p1e1	|- ( 0 + 1 ) = 1
157	156	fveq2i	|- ( Q ` ( 0 + 1 ) ) = ( Q ` 1 )
158	157	a1i	|- ( ph -> ( Q ` ( 0 + 1 ) ) = ( Q ` 1 ) )
159	153 155 158	3brtr3d	|- ( ph -> A < ( Q ` 1 ) )
160	112 110	posdifd	|- ( ph -> ( A < ( Q ` 1 ) <-> 0 < ( ( Q ` 1 ) - A ) ) )
161	159 160	mpbid	|- ( ph -> 0 < ( ( Q ` 1 ) - A ) )
162	132	a1i	|- ( ph -> 0 < 2 )
163	113 136 161 162	divgt0d	|- ( ph -> 0 < ( ( ( Q ` 1 ) - A ) / 2 ) )
164	114 163	elrpd	|- ( ph -> ( ( ( Q ` 1 ) - A ) / 2 ) e. RR+ )
165	164	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( Q ` 1 ) - A ) / 2 ) e. RR+ )
166	135 165	ifcld	|- ( ( 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+ )
167	43 166	ltaddrpd	|- ( ( 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 ) ) ) )
168	43 117 167	ltled	|- ( ( 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 ) ) ) )
169	168 14	breqtrrdi	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) <_ Z )
170	43 109	readdcld	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) e. RR )
171		iftrue	|- ( ( ( 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 ) )
172	171	adantl	|- ( ( ( 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 ) )
173	109	leidd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) <_ ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) )
174	173	adantr	|- ( ( ( 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 ) )
175	172 174	eqbrtrd	|- ( ( ( 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 ) )
176		iffalse	|- ( -. ( ( 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 ) )
177	176	adantl	|- ( ( ( 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 ) )
178	113	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( Q ` 1 ) - A ) e. RR )
179	108	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) e. RR )
180		2rp	|- 2 e. RR+
181	180	a1i	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> 2 e. RR+ )
182		simpr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) )
183	178 179 182	nltled	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( Q ` 1 ) - A ) <_ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
184	178 179 181 183	lediv1dd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( ( Q ` 1 ) - A ) / 2 ) <_ ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) )
185	177 184	eqbrtrd	|- ( ( ( 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 ) )
186	175 185	pm2.61dan	|- ( ( 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 ) )
187	116 109 43 186	leadd2dd	|- ( ( 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 ) ) )
188	43	recnd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) e. CC )
189	107	recnd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` ( j + 1 ) ) e. CC )
190	188 189	addcomd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( S ` ( j + 1 ) ) ) = ( ( S ` ( j + 1 ) ) + ( S ` j ) ) )
191	190	oveq1d	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) = ( ( ( S ` ( j + 1 ) ) + ( S ` j ) ) / 2 ) )
192	191	oveq1d	|- ( ( 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 ) ) )
193		halfaddsub	|- ( ( ( 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 ) ) )
194	189 188 193	syl2anc	|- ( ( 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 ) ) )
195	194	simprd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( S ` ( j + 1 ) ) + ( S ` j ) ) / 2 ) - ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) = ( S ` j ) )
196	192 195	eqtrd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) - ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) = ( S ` j ) )
197	188 189	addcld	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( S ` ( j + 1 ) ) ) e. CC )
198	197	halfcld	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) e. CC )
199	109	recnd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) e. CC )
200	198 199 188	subsub23d	|- ( ( 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 ) ) )
201	196 200	mpbid	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) - ( S ` j ) ) = ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) )
202	198 188 199	subaddd	|- ( ( 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 ) ) )
203	201 202	mpbid	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) = ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) )
204		avglt2	|- ( ( ( S ` j ) e. RR /\ ( S ` ( j + 1 ) ) e. RR ) -> ( ( S ` j ) < ( S ` ( j + 1 ) ) <-> ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) < ( S ` ( j + 1 ) ) ) )
205	43 107 204	syl2anc	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) < ( S ` ( j + 1 ) ) <-> ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) < ( S ` ( j + 1 ) ) ) )
206	129 205	mpbid	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( S ` j ) + ( S ` ( j + 1 ) ) ) / 2 ) < ( S ` ( j + 1 ) ) )
207	203 206	eqbrtrd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) < ( S ` ( j + 1 ) ) )
208	117 170 107 187 207	lelttrd	|- ( ( 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 ) ) )
209	14 208	eqbrtrid	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> Z < ( S ` ( j + 1 ) ) )
210	107	rexrd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` ( j + 1 ) ) e. RR* )
211		elico2	|- ( ( ( 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 ) ) ) ) )
212	43 210 211	syl2anc	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( Z e. ( ( S ` j ) [,) ( S ` ( j + 1 ) ) ) <-> ( Z e. RR /\ ( S ` j ) <_ Z /\ Z < ( S ` ( j + 1 ) ) ) ) )
213	118 169 209 212	mpbir3and	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> Z e. ( ( S ` j ) [,) ( S ` ( j + 1 ) ) ) )
214	213	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> Z e. ( ( S ` j ) [,) ( S ` ( j + 1 ) ) ) )
215	112	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> A e. RR )
216	111	simp2d	|- ( ph -> B e. RR )
217	216	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> B e. RR )
218	111	simp3d	|- ( ph -> A < B )
219	218	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> A < B )
220	43	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( S ` j ) e. RR )
221		simpr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) = B )
222	167 14	breqtrrdi	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) < Z )
223	216 112	resubcld	|- ( ph -> ( B - A ) e. RR )
224	1 223	eqeltrid	|- ( ph -> T e. RR )
225	224	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> T e. RR )
226	109	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) e. RR )
227	114	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( ( Q ` 1 ) - A ) / 2 ) e. RR )
228	108	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) e. RR )
229	113	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( Q ` 1 ) - A ) e. RR )
230	180	a1i	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> 2 e. RR+ )
231		simpr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) )
232	228 229 230 231	ltdiv1dd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) < ( ( ( Q ` 1 ) - A ) / 2 ) )
233	226 227 232	ltled	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) <_ ( ( ( Q ` 1 ) - A ) / 2 ) )
234	172 233	eqbrtrd	|- ( ( ( 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 ) )
235	176	adantl	|- ( ( 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 ) )
236	114	leidd	|- ( ph -> ( ( ( Q ` 1 ) - A ) / 2 ) <_ ( ( ( Q ` 1 ) - A ) / 2 ) )
237	236	adantr	|- ( ( ph /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( ( ( Q ` 1 ) - A ) / 2 ) <_ ( ( ( Q ` 1 ) - A ) / 2 ) )
238	235 237	eqbrtrd	|- ( ( 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 ) )
239	238	adantlr	|- ( ( ( 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 ) )
240	234 239	pm2.61dan	|- ( ( 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 ) )
241	223	rehalfcld	|- ( ph -> ( ( B - A ) / 2 ) e. RR )
242	180	a1i	|- ( ph -> 2 e. RR+ )
243	112	rexrd	|- ( ph -> A e. RR* )
244	216	rexrd	|- ( ph -> B e. RR* )
245	2 3 4	fourierdlem15	|- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
246	245 102	ffvelrnd	|- ( ph -> ( Q ` 1 ) e. ( A [,] B ) )
247		iccleub	|- ( ( A e. RR* /\ B e. RR* /\ ( Q ` 1 ) e. ( A [,] B ) ) -> ( Q ` 1 ) <_ B )
248	243 244 246 247	syl3anc	|- ( ph -> ( Q ` 1 ) <_ B )
249	110 216 112 248	lesub1dd	|- ( ph -> ( ( Q ` 1 ) - A ) <_ ( B - A ) )
250	113 223 242 249	lediv1dd	|- ( ph -> ( ( ( Q ` 1 ) - A ) / 2 ) <_ ( ( B - A ) / 2 ) )
251	1	eqcomi	|- ( B - A ) = T
252	251	oveq1i	|- ( ( B - A ) / 2 ) = ( T / 2 )
253	112 216	posdifd	|- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
254	218 253	mpbid	|- ( ph -> 0 < ( B - A ) )
255	254 1	breqtrrdi	|- ( ph -> 0 < T )
256	224 255	elrpd	|- ( ph -> T e. RR+ )
257		rphalflt	|- ( T e. RR+ -> ( T / 2 ) < T )
258	256 257	syl	|- ( ph -> ( T / 2 ) < T )
259	252 258	eqbrtrid	|- ( ph -> ( ( B - A ) / 2 ) < T )
260	114 241 224 250 259	lelttrd	|- ( ph -> ( ( ( Q ` 1 ) - A ) / 2 ) < T )
261	114 224 260	ltled	|- ( ph -> ( ( ( Q ` 1 ) - A ) / 2 ) <_ T )
262	261	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( Q ` 1 ) - A ) / 2 ) <_ T )
263	116 115 225 240 262	letrd	|- ( ( 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 )
264	116 225 43 263	leadd2dd	|- ( ( 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 ) )
265	14 264	eqbrtrid	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> Z <_ ( ( S ` j ) + T ) )
266	43	rexrd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) e. RR* )
267	43 225	readdcld	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + T ) e. RR )
268		elioc2	|- ( ( ( 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 ) ) ) )
269	266 267 268	syl2anc	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( Z e. ( ( S ` j ) (,] ( ( S ` j ) + T ) ) <-> ( Z e. RR /\ ( S ` j ) < Z /\ Z <_ ( ( S ` j ) + T ) ) ) )
270	118 222 265 269	mpbir3and	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> Z e. ( ( S ` j ) (,] ( ( S ` j ) + T ) ) )
271	270	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> Z e. ( ( S ` j ) (,] ( ( S ` j ) + T ) ) )
272	215 217 219 1 12 220 221 271	fourierdlem26	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` Z ) = ( A + ( Z - ( S ` j ) ) ) )
273	14	a1i	|- ( ( 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 ) ) ) )
274	273	oveq1d	|- ( ( 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 ) ) )
275	274	oveq2d	|- ( ( 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 ) ) ) )
276	275	adantr	|- ( ( ( 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 ) ) ) )
277	116	recnd	|- ( ( 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 )
278	188 277	pncan2d	|- ( ( 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 ) ) )
279	278	oveq2d	|- ( ( 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 ) ) ) )
280	279	adantr	|- ( ( ( 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 ) ) ) )
281	272 276 280	3eqtrd	|- ( ( ( 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 ) ) ) )
282	171	oveq2d	|- ( ( ( 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 ) ) )
283	282	adantl	|- ( ( ( 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 ) ) )
284	112	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> A e. RR )
285	284 109	readdcld	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( A + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) e. RR )
286	285	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) e. RR )
287	284 115	readdcld	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) e. RR )
288	287	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) e. RR )
289	110	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( Q ` 1 ) e. RR )
290	112	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> A e. RR )
291	226 227 290 232	ltadd2dd	|- ( ( ( 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 ) ) )
292	110	recnd	|- ( ph -> ( Q ` 1 ) e. CC )
293	112	recnd	|- ( ph -> A e. CC )
294		halfaddsub	|- ( ( ( 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 ) )
295	292 293 294	syl2anc	|- ( ph -> ( ( ( ( ( Q ` 1 ) + A ) / 2 ) + ( ( ( Q ` 1 ) - A ) / 2 ) ) = ( Q ` 1 ) /\ ( ( ( ( Q ` 1 ) + A ) / 2 ) - ( ( ( Q ` 1 ) - A ) / 2 ) ) = A ) )
296	295	simprd	|- ( ph -> ( ( ( ( Q ` 1 ) + A ) / 2 ) - ( ( ( Q ` 1 ) - A ) / 2 ) ) = A )
297	296	oveq1d	|- ( ph -> ( ( ( ( ( Q ` 1 ) + A ) / 2 ) - ( ( ( Q ` 1 ) - A ) / 2 ) ) + ( ( ( Q ` 1 ) - A ) / 2 ) ) = ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) )
298	110 112	readdcld	|- ( ph -> ( ( Q ` 1 ) + A ) e. RR )
299	298	rehalfcld	|- ( ph -> ( ( ( Q ` 1 ) + A ) / 2 ) e. RR )
300	299	recnd	|- ( ph -> ( ( ( Q ` 1 ) + A ) / 2 ) e. CC )
301	114	recnd	|- ( ph -> ( ( ( Q ` 1 ) - A ) / 2 ) e. CC )
302	300 301	npcand	|- ( ph -> ( ( ( ( ( Q ` 1 ) + A ) / 2 ) - ( ( ( Q ` 1 ) - A ) / 2 ) ) + ( ( ( Q ` 1 ) - A ) / 2 ) ) = ( ( ( Q ` 1 ) + A ) / 2 ) )
303	297 302	eqtr3d	|- ( ph -> ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) = ( ( ( Q ` 1 ) + A ) / 2 ) )
304	110 110	readdcld	|- ( ph -> ( ( Q ` 1 ) + ( Q ` 1 ) ) e. RR )
305	112 110 110 159	ltadd2dd	|- ( ph -> ( ( Q ` 1 ) + A ) < ( ( Q ` 1 ) + ( Q ` 1 ) ) )
306	298 304 242 305	ltdiv1dd	|- ( ph -> ( ( ( Q ` 1 ) + A ) / 2 ) < ( ( ( Q ` 1 ) + ( Q ` 1 ) ) / 2 ) )
307	292	2timesd	|- ( ph -> ( 2 x. ( Q ` 1 ) ) = ( ( Q ` 1 ) + ( Q ` 1 ) ) )
308	307	eqcomd	|- ( ph -> ( ( Q ` 1 ) + ( Q ` 1 ) ) = ( 2 x. ( Q ` 1 ) ) )
309	308	oveq1d	|- ( ph -> ( ( ( Q ` 1 ) + ( Q ` 1 ) ) / 2 ) = ( ( 2 x. ( Q ` 1 ) ) / 2 ) )
310		2cnd	|- ( ph -> 2 e. CC )
311		2ne0	|- 2 =/= 0
312	311	a1i	|- ( ph -> 2 =/= 0 )
313	292 310 312	divcan3d	|- ( ph -> ( ( 2 x. ( Q ` 1 ) ) / 2 ) = ( Q ` 1 ) )
314	309 313	eqtrd	|- ( ph -> ( ( ( Q ` 1 ) + ( Q ` 1 ) ) / 2 ) = ( Q ` 1 ) )
315	306 314	breqtrd	|- ( ph -> ( ( ( Q ` 1 ) + A ) / 2 ) < ( Q ` 1 ) )
316	303 315	eqbrtrd	|- ( ph -> ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) < ( Q ` 1 ) )
317	316	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) < ( Q ` 1 ) )
318	286 288 289 291 317	lttrd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) ) < ( Q ` 1 ) )
319	283 318	eqbrtrd	|- ( ( ( 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 ) )
320	176	oveq2d	|- ( -. ( ( 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 ) ) )
321	320	adantl	|- ( ( ( 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 ) ) )
322	316	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) ) -> ( A + ( ( ( Q ` 1 ) - A ) / 2 ) ) < ( Q ` 1 ) )
323	321 322	eqbrtrd	|- ( ( ( 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 ) )
324	319 323	pm2.61dan	|- ( ( 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 ) )
325	324	adantr	|- ( ( ( 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 ) )
326	281 325	eqbrtrd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` Z ) < ( Q ` 1 ) )
327		eqid	|- ( ( Q ` 1 ) - ( ( E ` Z ) - Z ) ) = ( ( Q ` 1 ) - ( ( E ` Z ) - Z ) )
328	1 2 91 92 93 94 95 8 9 10 11 12 103 104 214 326 327	fourierdlem63	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` ( j + 1 ) ) ) <_ ( Q ` 1 ) )
329	15	a1i	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> I = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) ) )
330	58	adantl	|- ( ( ( ( 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 , < ) )
331	61	a1i	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) e. _V )
332	329 330 220 331	fvmptd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( I ` ( S ` j ) ) = sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) )
333		fveq2	|- ( ( E ` ( S ` j ) ) = B -> ( L ` ( E ` ( S ` j ) ) ) = ( L ` B ) )
334	13	a1i	|- ( ph -> L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) )
335		iftrue	|- ( y = B -> if ( y = B , A , y ) = A )
336	335	adantl	|- ( ( ph /\ y = B ) -> if ( y = B , A , y ) = A )
337		ubioc1	|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> B e. ( A (,] B ) )
338	243 244 218 337	syl3anc	|- ( ph -> B e. ( A (,] B ) )
339	334 336 338 112	fvmptd	|- ( ph -> ( L ` B ) = A )
340	333 339	sylan9eqr	|- ( ( ph /\ ( E ` ( S ` j ) ) = B ) -> ( L ` ( E ` ( S ` j ) ) ) = A )
341	340	breq2d	|- ( ( ph /\ ( E ` ( S ` j ) ) = B ) -> ( ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) <-> ( Q ` i ) <_ A ) )
342	341	rabbidv	|- ( ( ph /\ ( E ` ( S ` j ) ) = B ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } = { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } )
343	342	supeq1d	|- ( ( ph /\ ( E ` ( S ` j ) ) = B ) -> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) = sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } , RR , < ) )
344	343	adantlr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) = sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } , RR , < ) )
345		simpl	|- ( ( ph /\ j e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } ) -> ph )
346		elrabi	|- ( j e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } -> j e. ( 0 ..^ M ) )
347	346	adantl	|- ( ( ph /\ j e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } ) -> j e. ( 0 ..^ M ) )
348		fveq2	|- ( i = j -> ( Q ` i ) = ( Q ` j ) )
349	348	breq1d	|- ( i = j -> ( ( Q ` i ) <_ A <-> ( Q ` j ) <_ A ) )
350	349	elrab	|- ( j e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } <-> ( j e. ( 0 ..^ M ) /\ ( Q ` j ) <_ A ) )
351	350	simprbi	|- ( j e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } -> ( Q ` j ) <_ A )
352	351	adantl	|- ( ( ph /\ j e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } ) -> ( Q ` j ) <_ A )
353		simp3	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( Q ` j ) <_ A ) -> ( Q ` j ) <_ A )
354	112	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> A e. RR )
355	110	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> ( Q ` 1 ) e. RR )
356	21	adantr	|- ( ( ph /\ j e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
357	26	sselda	|- ( ( ph /\ j e. ( 0 ..^ M ) ) -> j e. ( 0 ... M ) )
358	356 357	ffvelrnd	|- ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` j ) e. RR )
359	358	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> ( Q ` j ) e. RR )
360	159	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> A < ( Q ` 1 ) )
361		1zzd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> 1 e. ZZ )
362		elfzoelz	|- ( j e. ( 0 ..^ M ) -> j e. ZZ )
363	362	ad2antlr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> j e. ZZ )
364		1e0p1	|- 1 = ( 0 + 1 )
365		simpr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> -. j <_ 0 )
366		0red	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> 0 e. RR )
367	363	zred	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> j e. RR )
368	366 367	ltnled	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> ( 0 < j <-> -. j <_ 0 ) )
369	365 368	mpbird	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> 0 < j )
370		0zd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> 0 e. ZZ )
371		zltp1le	|- ( ( 0 e. ZZ /\ j e. ZZ ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
372	370 363 371	syl2anc	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
373	369 372	mpbid	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> ( 0 + 1 ) <_ j )
374	364 373	eqbrtrid	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> 1 <_ j )
375		eluz2	|- ( j e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ j e. ZZ /\ 1 <_ j ) )
376	361 363 374 375	syl3anbrc	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> j e. ( ZZ>= ` 1 ) )
377	21	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... j ) ) -> Q : ( 0 ... M ) --> RR )
378		0zd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... j ) ) -> 0 e. ZZ )
379	97	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... j ) ) -> M e. ZZ )
380		elfzelz	|- ( l e. ( 1 ... j ) -> l e. ZZ )
381	380	adantl	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... j ) ) -> l e. ZZ )
382		0red	|- ( l e. ( 1 ... j ) -> 0 e. RR )
383	380	zred	|- ( l e. ( 1 ... j ) -> l e. RR )
384		1red	|- ( l e. ( 1 ... j ) -> 1 e. RR )
385		0lt1	|- 0 < 1
386	385	a1i	|- ( l e. ( 1 ... j ) -> 0 < 1 )
387		elfzle1	|- ( l e. ( 1 ... j ) -> 1 <_ l )
388	382 384 383 386 387	ltletrd	|- ( l e. ( 1 ... j ) -> 0 < l )
389	382 383 388	ltled	|- ( l e. ( 1 ... j ) -> 0 <_ l )
390	389	adantl	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... j ) ) -> 0 <_ l )
391	383	adantl	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... j ) ) -> l e. RR )
392	97	zred	|- ( ph -> M e. RR )
393	392	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... j ) ) -> M e. RR )
394	362	zred	|- ( j e. ( 0 ..^ M ) -> j e. RR )
395	394	ad2antlr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... j ) ) -> j e. RR )
396		elfzle2	|- ( l e. ( 1 ... j ) -> l <_ j )
397	396	adantl	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... j ) ) -> l <_ j )
398		elfzolt2	|- ( j e. ( 0 ..^ M ) -> j < M )
399	398	ad2antlr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... j ) ) -> j < M )
400	391 395 393 397 399	lelttrd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... j ) ) -> l < M )
401	391 393 400	ltled	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... j ) ) -> l <_ M )
402	378 379 381 390 401	elfzd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... j ) ) -> l e. ( 0 ... M ) )
403	377 402	ffvelrnd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... j ) ) -> ( Q ` l ) e. RR )
404	403	adantlr	|- ( ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) /\ l e. ( 1 ... j ) ) -> ( Q ` l ) e. RR )
405	21	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> Q : ( 0 ... M ) --> RR )
406		0zd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> 0 e. ZZ )
407	97	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> M e. ZZ )
408		elfzelz	|- ( l e. ( 1 ... ( j - 1 ) ) -> l e. ZZ )
409	408	adantl	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l e. ZZ )
410		0red	|- ( l e. ( 1 ... ( j - 1 ) ) -> 0 e. RR )
411	408	zred	|- ( l e. ( 1 ... ( j - 1 ) ) -> l e. RR )
412		1red	|- ( l e. ( 1 ... ( j - 1 ) ) -> 1 e. RR )
413	385	a1i	|- ( l e. ( 1 ... ( j - 1 ) ) -> 0 < 1 )
414		elfzle1	|- ( l e. ( 1 ... ( j - 1 ) ) -> 1 <_ l )
415	410 412 411 413 414	ltletrd	|- ( l e. ( 1 ... ( j - 1 ) ) -> 0 < l )
416	410 411 415	ltled	|- ( l e. ( 1 ... ( j - 1 ) ) -> 0 <_ l )
417	416	adantl	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> 0 <_ l )
418	409	zred	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l e. RR )
419	392	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> M e. RR )
420	394	ad2antlr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> j e. RR )
421	411	adantl	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l e. RR )
422		peano2rem	|- ( j e. RR -> ( j - 1 ) e. RR )
423	394 422	syl	|- ( j e. ( 0 ..^ M ) -> ( j - 1 ) e. RR )
424	423	adantr	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( j - 1 ) e. RR )
425	394	adantr	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> j e. RR )
426		elfzle2	|- ( l e. ( 1 ... ( j - 1 ) ) -> l <_ ( j - 1 ) )
427	426	adantl	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l <_ ( j - 1 ) )
428	425	ltm1d	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( j - 1 ) < j )
429	421 424 425 427 428	lelttrd	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l < j )
430	429	adantll	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l < j )
431	398	ad2antlr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> j < M )
432	418 420 419 430 431	lttrd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l < M )
433	418 419 432	ltled	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l <_ M )
434	406 407 409 417 433	elfzd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l e. ( 0 ... M ) )
435	405 434	ffvelrnd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( Q ` l ) e. RR )
436	409	peano2zd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) e. ZZ )
437	411 412	readdcld	|- ( l e. ( 1 ... ( j - 1 ) ) -> ( l + 1 ) e. RR )
438	411 412 415 413	addgt0d	|- ( l e. ( 1 ... ( j - 1 ) ) -> 0 < ( l + 1 ) )
439	410 437 438	ltled	|- ( l e. ( 1 ... ( j - 1 ) ) -> 0 <_ ( l + 1 ) )
440	439	adantl	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> 0 <_ ( l + 1 ) )
441	437	adantl	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) e. RR )
442	437	recnd	|- ( l e. ( 1 ... ( j - 1 ) ) -> ( l + 1 ) e. CC )
443		1cnd	|- ( l e. ( 1 ... ( j - 1 ) ) -> 1 e. CC )
444	442 443	npcand	|- ( l e. ( 1 ... ( j - 1 ) ) -> ( ( ( l + 1 ) - 1 ) + 1 ) = ( l + 1 ) )
445	444	eqcomd	|- ( l e. ( 1 ... ( j - 1 ) ) -> ( l + 1 ) = ( ( ( l + 1 ) - 1 ) + 1 ) )
446	445	adantl	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) = ( ( ( l + 1 ) - 1 ) + 1 ) )
447		peano2re	|- ( l e. RR -> ( l + 1 ) e. RR )
448		peano2rem	|- ( ( l + 1 ) e. RR -> ( ( l + 1 ) - 1 ) e. RR )
449	421 447 448	3syl	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( ( l + 1 ) - 1 ) e. RR )
450		peano2re	|- ( ( j - 1 ) e. RR -> ( ( j - 1 ) + 1 ) e. RR )
451		peano2rem	|- ( ( ( j - 1 ) + 1 ) e. RR -> ( ( ( j - 1 ) + 1 ) - 1 ) e. RR )
452	424 450 451	3syl	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( ( ( j - 1 ) + 1 ) - 1 ) e. RR )
453		1red	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> 1 e. RR )
454		elfzel2	|- ( l e. ( 1 ... ( j - 1 ) ) -> ( j - 1 ) e. ZZ )
455	454	zred	|- ( l e. ( 1 ... ( j - 1 ) ) -> ( j - 1 ) e. RR )
456	455 412	readdcld	|- ( l e. ( 1 ... ( j - 1 ) ) -> ( ( j - 1 ) + 1 ) e. RR )
457	411 455 412 426	leadd1dd	|- ( l e. ( 1 ... ( j - 1 ) ) -> ( l + 1 ) <_ ( ( j - 1 ) + 1 ) )
458	437 456 412 457	lesub1dd	|- ( l e. ( 1 ... ( j - 1 ) ) -> ( ( l + 1 ) - 1 ) <_ ( ( ( j - 1 ) + 1 ) - 1 ) )
459	458	adantl	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( ( l + 1 ) - 1 ) <_ ( ( ( j - 1 ) + 1 ) - 1 ) )
460	449 452 453 459	leadd1dd	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( ( ( l + 1 ) - 1 ) + 1 ) <_ ( ( ( ( j - 1 ) + 1 ) - 1 ) + 1 ) )
461		peano2zm	|- ( j e. ZZ -> ( j - 1 ) e. ZZ )
462	362 461	syl	|- ( j e. ( 0 ..^ M ) -> ( j - 1 ) e. ZZ )
463	462	peano2zd	|- ( j e. ( 0 ..^ M ) -> ( ( j - 1 ) + 1 ) e. ZZ )
464	463	zcnd	|- ( j e. ( 0 ..^ M ) -> ( ( j - 1 ) + 1 ) e. CC )
465		1cnd	|- ( j e. ( 0 ..^ M ) -> 1 e. CC )
466	464 465	npcand	|- ( j e. ( 0 ..^ M ) -> ( ( ( ( j - 1 ) + 1 ) - 1 ) + 1 ) = ( ( j - 1 ) + 1 ) )
467	394	recnd	|- ( j e. ( 0 ..^ M ) -> j e. CC )
468	467 465	npcand	|- ( j e. ( 0 ..^ M ) -> ( ( j - 1 ) + 1 ) = j )
469	466 468	eqtrd	|- ( j e. ( 0 ..^ M ) -> ( ( ( ( j - 1 ) + 1 ) - 1 ) + 1 ) = j )
470	469	adantr	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( ( ( ( j - 1 ) + 1 ) - 1 ) + 1 ) = j )
471	460 470	breqtrd	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( ( ( l + 1 ) - 1 ) + 1 ) <_ j )
472	446 471	eqbrtrd	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) <_ j )
473	472	adantll	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) <_ j )
474	441 420 419 473 431	lelttrd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) < M )
475	441 419 474	ltled	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) <_ M )
476	406 407 436 440 475	elfzd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) e. ( 0 ... M ) )
477	405 476	ffvelrnd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( Q ` ( l + 1 ) ) e. RR )
478		simpll	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ph )
479		0zd	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> 0 e. ZZ )
480	408	adantl	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l e. ZZ )
481	416	adantl	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> 0 <_ l )
482		eluz2	|- ( l e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ l e. ZZ /\ 0 <_ l ) )
483	479 480 481 482	syl3anbrc	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l e. ( ZZ>= ` 0 ) )
484		elfzoel2	|- ( j e. ( 0 ..^ M ) -> M e. ZZ )
485	484	adantr	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> M e. ZZ )
486	485	zred	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> M e. RR )
487	398	adantr	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> j < M )
488	421 425 486 429 487	lttrd	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l < M )
489		elfzo2	|- ( l e. ( 0 ..^ M ) <-> ( l e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ l < M ) )
490	483 485 488 489	syl3anbrc	|- ( ( j e. ( 0 ..^ M ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l e. ( 0 ..^ M ) )
491	490	adantll	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l e. ( 0 ..^ M ) )
492		eleq1	|- ( i = l -> ( i e. ( 0 ..^ M ) <-> l e. ( 0 ..^ M ) ) )
493	492	anbi2d	|- ( i = l -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ l e. ( 0 ..^ M ) ) ) )
494		fveq2	|- ( i = l -> ( Q ` i ) = ( Q ` l ) )
495		oveq1	|- ( i = l -> ( i + 1 ) = ( l + 1 ) )
496	495	fveq2d	|- ( i = l -> ( Q ` ( i + 1 ) ) = ( Q ` ( l + 1 ) ) )
497	494 496	breq12d	|- ( i = l -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` l ) < ( Q ` ( l + 1 ) ) ) )
498	493 497	imbi12d	|- ( i = l -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ l e. ( 0 ..^ M ) ) -> ( Q ` l ) < ( Q ` ( l + 1 ) ) ) ) )
499	498 150	chvarvv	|- ( ( ph /\ l e. ( 0 ..^ M ) ) -> ( Q ` l ) < ( Q ` ( l + 1 ) ) )
500	478 491 499	syl2anc	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( Q ` l ) < ( Q ` ( l + 1 ) ) )
501	435 477 500	ltled	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( Q ` l ) <_ ( Q ` ( l + 1 ) ) )
502	501	adantlr	|- ( ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( Q ` l ) <_ ( Q ` ( l + 1 ) ) )
503	376 404 502	monoord	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> ( Q ` 1 ) <_ ( Q ` j ) )
504	354 355 359 360 503	ltletrd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> A < ( Q ` j ) )
505	354 359	ltnled	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> ( A < ( Q ` j ) <-> -. ( Q ` j ) <_ A ) )
506	504 505	mpbid	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. j <_ 0 ) -> -. ( Q ` j ) <_ A )
507	506	ex	|- ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( -. j <_ 0 -> -. ( Q ` j ) <_ A ) )
508	507	3adant3	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( Q ` j ) <_ A ) -> ( -. j <_ 0 -> -. ( Q ` j ) <_ A ) )
509	353 508	mt4d	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( Q ` j ) <_ A ) -> j <_ 0 )
510		elfzole1	|- ( j e. ( 0 ..^ M ) -> 0 <_ j )
511	510	3ad2ant2	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( Q ` j ) <_ A ) -> 0 <_ j )
512	394	3ad2ant2	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( Q ` j ) <_ A ) -> j e. RR )
513		0red	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( Q ` j ) <_ A ) -> 0 e. RR )
514	512 513	letri3d	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( Q ` j ) <_ A ) -> ( j = 0 <-> ( j <_ 0 /\ 0 <_ j ) ) )
515	509 511 514	mpbir2and	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( Q ` j ) <_ A ) -> j = 0 )
516	345 347 352 515	syl3anc	|- ( ( ph /\ j e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } ) -> j = 0 )
517		velsn	|- ( j e. { 0 } <-> j = 0 )
518	516 517	sylibr	|- ( ( ph /\ j e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } ) -> j e. { 0 } )
519	518	ralrimiva	|- ( ph -> A. j e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } j e. { 0 } )
520		dfss3	|- ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } C_ { 0 } <-> A. j e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } j e. { 0 } )
521	519 520	sylibr	|- ( ph -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } C_ { 0 } )
522	155 112	eqeltrd	|- ( ph -> ( Q ` 0 ) e. RR )
523	522 155	eqled	|- ( ph -> ( Q ` 0 ) <_ A )
524	143	breq1d	|- ( i = 0 -> ( ( Q ` i ) <_ A <-> ( Q ` 0 ) <_ A ) )
525	524	elrab	|- ( 0 e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } <-> ( 0 e. ( 0 ..^ M ) /\ ( Q ` 0 ) <_ A ) )
526	139 523 525	sylanbrc	|- ( ph -> 0 e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } )
527	526	snssd	|- ( ph -> { 0 } C_ { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } )
528	521 527	eqssd	|- ( ph -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } = { 0 } )
529	528	supeq1d	|- ( ph -> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } , RR , < ) = sup ( { 0 } , RR , < ) )
530		supsn	|- ( ( < Or RR /\ 0 e. RR ) -> sup ( { 0 } , RR , < ) = 0 )
531	60 140 530	mp2an	|- sup ( { 0 } , RR , < ) = 0
532	531	a1i	|- ( ph -> sup ( { 0 } , RR , < ) = 0 )
533	529 532	eqtrd	|- ( ph -> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } , RR , < ) = 0 )
534	533	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ A } , RR , < ) = 0 )
535	332 344 534	3eqtrd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( I ` ( S ` j ) ) = 0 )
536	535	oveq1d	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( I ` ( S ` j ) ) + 1 ) = ( 0 + 1 ) )
537	536	fveq2d	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) = ( Q ` ( 0 + 1 ) ) )
538	537 157	eqtr2di	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( Q ` 1 ) = ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
539	328 538	breqtrd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` ( j + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
540	66	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ph /\ ( S ` j ) e. RR ) )
541		simplr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> j e. ( 0 ..^ N ) )
542	13	a1i	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) )
543		simpr	|- ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> y = ( E ` ( S ` j ) ) )
544		neqne	|- ( -. ( E ` ( S ` j ) ) = B -> ( E ` ( S ` j ) ) =/= B )
545	544	adantr	|- ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> ( E ` ( S ` j ) ) =/= B )
546	543 545	eqnetrd	|- ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> y =/= B )
547	546	neneqd	|- ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> -. y = B )
548	547	iffalsed	|- ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> if ( y = B , A , y ) = y )
549	548 543	eqtrd	|- ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> if ( y = B , A , y ) = ( E ` ( S ` j ) ) )
550	549	adantll	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ y = ( E ` ( S ` j ) ) ) -> if ( y = B , A , y ) = ( E ` ( S ` j ) ) )
551	112 216 218 1 12	fourierdlem4	|- ( ph -> E : RR --> ( A (,] B ) )
552	551	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> E : RR --> ( A (,] B ) )
553	552 43	ffvelrnd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E ` ( S ` j ) ) e. ( A (,] B ) )
554	553	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) e. ( A (,] B ) )
555	542 550 554 554	fvmptd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( L ` ( E ` ( S ` j ) ) ) = ( E ` ( S ` j ) ) )
556	555	eqcomd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) = ( L ` ( E ` ( S ` j ) ) ) )
557	112 216 218 13	fourierdlem17	|- ( ph -> L : ( A (,] B ) --> ( A [,] B ) )
558	557	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> L : ( A (,] B ) --> ( A [,] B ) )
559	112 216	iccssred	|- ( ph -> ( A [,] B ) C_ RR )
560	559	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( A [,] B ) C_ RR )
561	558 560	fssd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> L : ( A (,] B ) --> RR )
562	561 553	ffvelrnd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( L ` ( E ` ( S ` j ) ) ) e. RR )
563	562	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( L ` ( E ` ( S ` j ) ) ) e. RR )
564	556 563	eqeltrd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) e. RR )
565	216	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> B e. RR )
566	243	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> A e. RR* )
567	216	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> B e. RR )
568		elioc2	|- ( ( A e. RR* /\ B e. RR ) -> ( ( E ` ( S ` j ) ) e. ( A (,] B ) <-> ( ( E ` ( S ` j ) ) e. RR /\ A < ( E ` ( S ` j ) ) /\ ( E ` ( S ` j ) ) <_ B ) ) )
569	566 567 568	syl2anc	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` j ) ) e. ( A (,] B ) <-> ( ( E ` ( S ` j ) ) e. RR /\ A < ( E ` ( S ` j ) ) /\ ( E ` ( S ` j ) ) <_ B ) ) )
570	553 569	mpbid	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` j ) ) e. RR /\ A < ( E ` ( S ` j ) ) /\ ( E ` ( S ` j ) ) <_ B ) )
571	570	simp3d	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E ` ( S ` j ) ) <_ B )
572	571	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) <_ B )
573	544	necomd	|- ( -. ( E ` ( S ` j ) ) = B -> B =/= ( E ` ( S ` j ) ) )
574	573	adantl	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> B =/= ( E ` ( S ` j ) ) )
575	564 565 572 574	leneltd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) < B )
576	575	adantr	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( E ` ( S ` j ) ) < B )
577		oveq1	|- ( ( I ` ( S ` j ) ) = ( M - 1 ) -> ( ( I ` ( S ` j ) ) + 1 ) = ( ( M - 1 ) + 1 ) )
578	3	nncnd	|- ( ph -> M e. CC )
579		1cnd	|- ( ph -> 1 e. CC )
580	578 579	npcand	|- ( ph -> ( ( M - 1 ) + 1 ) = M )
581	577 580	sylan9eqr	|- ( ( ph /\ ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( ( I ` ( S ` j ) ) + 1 ) = M )
582	581	fveq2d	|- ( ( ph /\ ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) = ( Q ` M ) )
583	154	simprd	|- ( ph -> ( Q ` M ) = B )
584	583	adantr	|- ( ( ph /\ ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( Q ` M ) = B )
585	582 584	eqtr2d	|- ( ( ph /\ ( I ` ( S ` j ) ) = ( M - 1 ) ) -> B = ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
586	585	adantlr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( I ` ( S ` j ) ) = ( M - 1 ) ) -> B = ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
587	586	adantlr	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( I ` ( S ` j ) ) = ( M - 1 ) ) -> B = ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
588	576 587	breqtrd	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
589	556	adantr	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( E ` ( S ` j ) ) = ( L ` ( E ` ( S ` j ) ) ) )
590		ssrab2	|- { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } C_ ( 0 ..^ M )
591		fzssz	|- ( 0 ... M ) C_ ZZ
592	25 591	sstri	|- ( 0 ..^ M ) C_ ZZ
593		zssre	|- ZZ C_ RR
594	592 593	sstri	|- ( 0 ..^ M ) C_ RR
595	590 594	sstri	|- { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } C_ RR
596	595	a1i	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) /\ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } C_ RR )
597	57	neeq1d	|- ( x = ( S ` j ) -> ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } =/= (/) <-> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } =/= (/) ) )
598	68 597	imbi12d	|- ( x = ( S ` j ) -> ( ( ( ph /\ x e. RR ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } =/= (/) ) <-> ( ( ph /\ ( S ` j ) e. RR ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } =/= (/) ) ) )
599	139	adantr	|- ( ( ph /\ x e. RR ) -> 0 e. ( 0 ..^ M ) )
600	523	ad2antrr	|- ( ( ( ph /\ x e. RR ) /\ ( E ` x ) = B ) -> ( Q ` 0 ) <_ A )
601		iftrue	|- ( ( E ` x ) = B -> if ( ( E ` x ) = B , A , ( E ` x ) ) = A )
602	601	eqcomd	|- ( ( E ` x ) = B -> A = if ( ( E ` x ) = B , A , ( E ` x ) ) )
603	602	adantl	|- ( ( ( ph /\ x e. RR ) /\ ( E ` x ) = B ) -> A = if ( ( E ` x ) = B , A , ( E ` x ) ) )
604	600 603	breqtrd	|- ( ( ( ph /\ x e. RR ) /\ ( E ` x ) = B ) -> ( Q ` 0 ) <_ if ( ( E ` x ) = B , A , ( E ` x ) ) )
605	522	adantr	|- ( ( ph /\ x e. RR ) -> ( Q ` 0 ) e. RR )
606	112	adantr	|- ( ( ph /\ x e. RR ) -> A e. RR )
607	606	rexrd	|- ( ( ph /\ x e. RR ) -> A e. RR* )
608	216	adantr	|- ( ( ph /\ x e. RR ) -> B e. RR )
609		iocssre	|- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
610	607 608 609	syl2anc	|- ( ( ph /\ x e. RR ) -> ( A (,] B ) C_ RR )
611	551	ffvelrnda	|- ( ( ph /\ x e. RR ) -> ( E ` x ) e. ( A (,] B ) )
612	610 611	sseldd	|- ( ( ph /\ x e. RR ) -> ( E ` x ) e. RR )
613	155	adantr	|- ( ( ph /\ x e. RR ) -> ( Q ` 0 ) = A )
614		elioc2	|- ( ( A e. RR* /\ B e. RR ) -> ( ( E ` x ) e. ( A (,] B ) <-> ( ( E ` x ) e. RR /\ A < ( E ` x ) /\ ( E ` x ) <_ B ) ) )
615	607 608 614	syl2anc	|- ( ( ph /\ x e. RR ) -> ( ( E ` x ) e. ( A (,] B ) <-> ( ( E ` x ) e. RR /\ A < ( E ` x ) /\ ( E ` x ) <_ B ) ) )
616	611 615	mpbid	|- ( ( ph /\ x e. RR ) -> ( ( E ` x ) e. RR /\ A < ( E ` x ) /\ ( E ` x ) <_ B ) )
617	616	simp2d	|- ( ( ph /\ x e. RR ) -> A < ( E ` x ) )
618	613 617	eqbrtrd	|- ( ( ph /\ x e. RR ) -> ( Q ` 0 ) < ( E ` x ) )
619	605 612 618	ltled	|- ( ( ph /\ x e. RR ) -> ( Q ` 0 ) <_ ( E ` x ) )
620	619	adantr	|- ( ( ( ph /\ x e. RR ) /\ -. ( E ` x ) = B ) -> ( Q ` 0 ) <_ ( E ` x ) )
621		iffalse	|- ( -. ( E ` x ) = B -> if ( ( E ` x ) = B , A , ( E ` x ) ) = ( E ` x ) )
622	621	eqcomd	|- ( -. ( E ` x ) = B -> ( E ` x ) = if ( ( E ` x ) = B , A , ( E ` x ) ) )
623	622	adantl	|- ( ( ( ph /\ x e. RR ) /\ -. ( E ` x ) = B ) -> ( E ` x ) = if ( ( E ` x ) = B , A , ( E ` x ) ) )
624	620 623	breqtrd	|- ( ( ( ph /\ x e. RR ) /\ -. ( E ` x ) = B ) -> ( Q ` 0 ) <_ if ( ( E ` x ) = B , A , ( E ` x ) ) )
625	604 624	pm2.61dan	|- ( ( ph /\ x e. RR ) -> ( Q ` 0 ) <_ if ( ( E ` x ) = B , A , ( E ` x ) ) )
626	13	a1i	|- ( ( ph /\ x e. RR ) -> L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) )
627		eqeq1	|- ( y = ( E ` x ) -> ( y = B <-> ( E ` x ) = B ) )
628		id	|- ( y = ( E ` x ) -> y = ( E ` x ) )
629	627 628	ifbieq2d	|- ( y = ( E ` x ) -> if ( y = B , A , y ) = if ( ( E ` x ) = B , A , ( E ` x ) ) )
630	629	adantl	|- ( ( ( ph /\ x e. RR ) /\ y = ( E ` x ) ) -> if ( y = B , A , y ) = if ( ( E ` x ) = B , A , ( E ` x ) ) )
631	606 612	ifcld	|- ( ( ph /\ x e. RR ) -> if ( ( E ` x ) = B , A , ( E ` x ) ) e. RR )
632	626 630 611 631	fvmptd	|- ( ( ph /\ x e. RR ) -> ( L ` ( E ` x ) ) = if ( ( E ` x ) = B , A , ( E ` x ) ) )
633	625 632	breqtrrd	|- ( ( ph /\ x e. RR ) -> ( Q ` 0 ) <_ ( L ` ( E ` x ) ) )
634	143	breq1d	|- ( i = 0 -> ( ( Q ` i ) <_ ( L ` ( E ` x ) ) <-> ( Q ` 0 ) <_ ( L ` ( E ` x ) ) ) )
635	634	elrab	|- ( 0 e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } <-> ( 0 e. ( 0 ..^ M ) /\ ( Q ` 0 ) <_ ( L ` ( E ` x ) ) ) )
636	599 633 635	sylanbrc	|- ( ( ph /\ x e. RR ) -> 0 e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } )
637		ne0i	|- ( 0 e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } =/= (/) )
638	636 637	syl	|- ( ( ph /\ x e. RR ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } =/= (/) )
639	598 638	vtoclg	|- ( ( S ` j ) e. RR -> ( ( ph /\ ( S ` j ) e. RR ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } =/= (/) ) )
640	43 66 639	sylc	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } =/= (/) )
641	640	ad2antrr	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) /\ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } =/= (/) )
642	595	a1i	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } C_ RR )
643		fzofi	|- ( 0 ..^ M ) e. Fin
644		ssfi	|- ( ( ( 0 ..^ M ) e. Fin /\ { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } C_ ( 0 ..^ M ) ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } e. Fin )
645	643 590 644	mp2an	|- { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } e. Fin
646	645	a1i	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } e. Fin )
647		fimaxre2	|- ( ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } C_ RR /\ { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } e. Fin ) -> E. x e. RR A. l e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } l <_ x )
648	642 646 647	syl2anc	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> E. x e. RR A. l e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } l <_ x )
649	648	ad2antrr	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) /\ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) -> E. x e. RR A. l e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } l <_ x )
650		0red	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> 0 e. RR )
651	594 48	sselid	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( I ` ( S ` j ) ) e. RR )
652		1red	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> 1 e. RR )
653	651 652	readdcld	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( I ` ( S ` j ) ) + 1 ) e. RR )
654		elfzouz	|- ( ( I ` ( S ` j ) ) e. ( 0 ..^ M ) -> ( I ` ( S ` j ) ) e. ( ZZ>= ` 0 ) )
655		eluzle	|- ( ( I ` ( S ` j ) ) e. ( ZZ>= ` 0 ) -> 0 <_ ( I ` ( S ` j ) ) )
656	48 654 655	3syl	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> 0 <_ ( I ` ( S ` j ) ) )
657	385	a1i	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> 0 < 1 )
658	651 652 656 657	addgegt0d	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> 0 < ( ( I ` ( S ` j ) ) + 1 ) )
659	650 653 658	ltled	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> 0 <_ ( ( I ` ( S ` j ) ) + 1 ) )
660	659	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> 0 <_ ( ( I ` ( S ` j ) ) + 1 ) )
661	651	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( I ` ( S ` j ) ) e. RR )
662		1red	|- ( ph -> 1 e. RR )
663	392 662	resubcld	|- ( ph -> ( M - 1 ) e. RR )
664	663	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( M - 1 ) e. RR )
665		1red	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> 1 e. RR )
666		elfzolt2	|- ( ( I ` ( S ` j ) ) e. ( 0 ..^ M ) -> ( I ` ( S ` j ) ) < M )
667	48 666	syl	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( I ` ( S ` j ) ) < M )
668	44	elfzelzd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( I ` ( S ` j ) ) e. ZZ )
669	97	adantr	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> M e. ZZ )
670		zltlem1	|- ( ( ( I ` ( S ` j ) ) e. ZZ /\ M e. ZZ ) -> ( ( I ` ( S ` j ) ) < M <-> ( I ` ( S ` j ) ) <_ ( M - 1 ) ) )
671	668 669 670	syl2anc	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( I ` ( S ` j ) ) < M <-> ( I ` ( S ` j ) ) <_ ( M - 1 ) ) )
672	667 671	mpbid	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( I ` ( S ` j ) ) <_ ( M - 1 ) )
673	672	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( I ` ( S ` j ) ) <_ ( M - 1 ) )
674		neqne	|- ( -. ( I ` ( S ` j ) ) = ( M - 1 ) -> ( I ` ( S ` j ) ) =/= ( M - 1 ) )
675	674	necomd	|- ( -. ( I ` ( S ` j ) ) = ( M - 1 ) -> ( M - 1 ) =/= ( I ` ( S ` j ) ) )
676	675	adantl	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( M - 1 ) =/= ( I ` ( S ` j ) ) )
677	661 664 673 676	leneltd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( I ` ( S ` j ) ) < ( M - 1 ) )
678	661 664 665 677	ltadd1dd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( ( I ` ( S ` j ) ) + 1 ) < ( ( M - 1 ) + 1 ) )
679	580	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( ( M - 1 ) + 1 ) = M )
680	678 679	breqtrd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( ( I ` ( S ` j ) ) + 1 ) < M )
681	50	elfzelzd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( I ` ( S ` j ) ) + 1 ) e. ZZ )
682	681	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( ( I ` ( S ` j ) ) + 1 ) e. ZZ )
683		0zd	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> 0 e. ZZ )
684	97	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> M e. ZZ )
685		elfzo	|- ( ( ( ( I ` ( S ` j ) ) + 1 ) e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( ( ( I ` ( S ` j ) ) + 1 ) e. ( 0 ..^ M ) <-> ( 0 <_ ( ( I ` ( S ` j ) ) + 1 ) /\ ( ( I ` ( S ` j ) ) + 1 ) < M ) ) )
686	682 683 684 685	syl3anc	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( ( ( I ` ( S ` j ) ) + 1 ) e. ( 0 ..^ M ) <-> ( 0 <_ ( ( I ` ( S ` j ) ) + 1 ) /\ ( ( I ` ( S ` j ) ) + 1 ) < M ) ) )
687	660 680 686	mpbir2and	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( ( I ` ( S ` j ) ) + 1 ) e. ( 0 ..^ M ) )
688	687	adantr	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) /\ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) -> ( ( I ` ( S ` j ) ) + 1 ) e. ( 0 ..^ M ) )
689		simpr	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) /\ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) )
690		fveq2	|- ( i = ( ( I ` ( S ` j ) ) + 1 ) -> ( Q ` i ) = ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
691	690	breq1d	|- ( i = ( ( I ` ( S ` j ) ) + 1 ) -> ( ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) <-> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) )
692	691	elrab	|- ( ( ( I ` ( S ` j ) ) + 1 ) e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } <-> ( ( ( I ` ( S ` j ) ) + 1 ) e. ( 0 ..^ M ) /\ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) )
693	688 689 692	sylanbrc	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) /\ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) -> ( ( I ` ( S ` j ) ) + 1 ) e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } )
694		suprub	|- ( ( ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } C_ RR /\ { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } =/= (/) /\ E. x e. RR A. l e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } l <_ x ) /\ ( ( I ` ( S ` j ) ) + 1 ) e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } ) -> ( ( I ` ( S ` j ) ) + 1 ) <_ sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) )
695	596 641 649 693 694	syl31anc	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) /\ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) -> ( ( I ` ( S ` j ) ) + 1 ) <_ sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) )
696	63	eqcomd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) = ( I ` ( S ` j ) ) )
697	696	ad2antrr	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) /\ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) -> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` ( S ` j ) ) ) } , RR , < ) = ( I ` ( S ` j ) ) )
698	695 697	breqtrd	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) /\ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) -> ( ( I ` ( S ` j ) ) + 1 ) <_ ( I ` ( S ` j ) ) )
699	651	ltp1d	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( I ` ( S ` j ) ) < ( ( I ` ( S ` j ) ) + 1 ) )
700	651 653	ltnled	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( I ` ( S ` j ) ) < ( ( I ` ( S ` j ) ) + 1 ) <-> -. ( ( I ` ( S ` j ) ) + 1 ) <_ ( I ` ( S ` j ) ) ) )
701	699 700	mpbid	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> -. ( ( I ` ( S ` j ) ) + 1 ) <_ ( I ` ( S ` j ) ) )
702	701	ad2antrr	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) /\ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) -> -. ( ( I ` ( S ` j ) ) + 1 ) <_ ( I ` ( S ` j ) ) )
703	698 702	pm2.65da	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> -. ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) )
704	562	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( L ` ( E ` ( S ` j ) ) ) e. RR )
705	51	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) e. RR )
706	704 705	ltnled	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( ( L ` ( E ` ( S ` j ) ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <-> -. ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) <_ ( L ` ( E ` ( S ` j ) ) ) ) )
707	703 706	mpbird	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( L ` ( E ` ( S ` j ) ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
708	707	adantlr	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( L ` ( E ` ( S ` j ) ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
709	589 708	eqbrtrd	|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ -. ( I ` ( S ` j ) ) = ( M - 1 ) ) -> ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
710	588 709	pm2.61dan	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
711	3	3ad2ant1	|- ( ( ph /\ j e. ( 0 ..^ N ) /\ ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) -> M e. NN )
712	4	3ad2ant1	|- ( ( ph /\ j e. ( 0 ..^ N ) /\ ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) -> Q e. ( P ` M ) )
713	5	3ad2ant1	|- ( ( ph /\ j e. ( 0 ..^ N ) /\ ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) -> C e. RR )
714	6	3ad2ant1	|- ( ( ph /\ j e. ( 0 ..^ N ) /\ ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) -> D e. RR )
715	7	3ad2ant1	|- ( ( ph /\ j e. ( 0 ..^ N ) /\ ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) -> C < D )
716	50	3adant3	|- ( ( ph /\ j e. ( 0 ..^ N ) /\ ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) -> ( ( I ` ( S ` j ) ) + 1 ) e. ( 0 ... M ) )
717		simp2	|- ( ( ph /\ j e. ( 0 ..^ N ) /\ ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) -> j e. ( 0 ..^ N ) )
718	43	leidd	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) <_ ( S ` j ) )
719		elico2	|- ( ( ( S ` j ) e. RR /\ ( S ` ( j + 1 ) ) e. RR* ) -> ( ( S ` j ) e. ( ( S ` j ) [,) ( S ` ( j + 1 ) ) ) <-> ( ( S ` j ) e. RR /\ ( S ` j ) <_ ( S ` j ) /\ ( S ` j ) < ( S ` ( j + 1 ) ) ) ) )
720	43 210 719	syl2anc	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) e. ( ( S ` j ) [,) ( S ` ( j + 1 ) ) ) <-> ( ( S ` j ) e. RR /\ ( S ` j ) <_ ( S ` j ) /\ ( S ` j ) < ( S ` ( j + 1 ) ) ) ) )
721	43 718 129 720	mpbir3and	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) e. ( ( S ` j ) [,) ( S ` ( j + 1 ) ) ) )
722	721	3adant3	|- ( ( ph /\ j e. ( 0 ..^ N ) /\ ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) -> ( S ` j ) e. ( ( S ` j ) [,) ( S ` ( j + 1 ) ) ) )
723		simp3	|- ( ( ph /\ j e. ( 0 ..^ N ) /\ ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) -> ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
724		eqid	|- ( ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) - ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) = ( ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) - ( ( E ` ( S ` j ) ) - ( S ` j ) ) )
725	1 2 711 712 713 714 715 8 9 10 11 12 716 717 722 723 724	fourierdlem63	|- ( ( ph /\ j e. ( 0 ..^ N ) /\ ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) -> ( E ` ( S ` ( j + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
726	725	3adant1r	|- ( ( ( ph /\ ( S ` j ) e. RR ) /\ j e. ( 0 ..^ N ) /\ ( E ` ( S ` j ) ) < ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) -> ( E ` ( S ` ( j + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
727	540 541 710 726	syl3anc	|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` ( j + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
728	539 727	pm2.61dan	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E ` ( S ` ( j + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) )
729		ioossioo	|- ( ( ( ( Q ` ( I ` ( S ` j ) ) ) e. RR* /\ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) e. RR* ) /\ ( ( Q ` ( I ` ( S ` j ) ) ) <_ ( L ` ( E ` ( S ` j ) ) ) /\ ( E ` ( S ` ( j + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) ) -> ( ( L ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) )
730	46 52 90 728 729	syl22anc	|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( L ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) )