Metamath Proof Explorer

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 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) e. RR )
44 28 43 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( I ` ( S ` j ) ) e. ( 0 ... M ) )
45 22 44 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( 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 ffvelcdmd 
 |-  ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 ) ) ) )