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 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 sseldi
 |-  ( ( 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 ) ) ) )