Metamath Proof Explorer


Theorem fourierdlem25

Description: If C is not in the range of the partition, then it is in an open interval induced by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem25.m
|- ( ph -> M e. NN )
fourierdlem25.qf
|- ( ph -> Q : ( 0 ... M ) --> RR )
fourierdlem25.cel
|- ( ph -> C e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
fourierdlem25.cnel
|- ( ph -> -. C e. ran Q )
fourierdlem25.i
|- I = sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) < C } , RR , < )
Assertion fourierdlem25
|- ( ph -> E. j e. ( 0 ..^ M ) C e. ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem25.m
 |-  ( ph -> M e. NN )
2 fourierdlem25.qf
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
3 fourierdlem25.cel
 |-  ( ph -> C e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
4 fourierdlem25.cnel
 |-  ( ph -> -. C e. ran Q )
5 fourierdlem25.i
 |-  I = sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) < C } , RR , < )
6 ssrab2
 |-  { k e. ( 0 ..^ M ) | ( Q ` k ) < C } C_ ( 0 ..^ M )
7 ltso
 |-  < Or RR
8 7 a1i
 |-  ( ph -> < Or RR )
9 fzofi
 |-  ( 0 ..^ M ) e. Fin
10 ssfi
 |-  ( ( ( 0 ..^ M ) e. Fin /\ { k e. ( 0 ..^ M ) | ( Q ` k ) < C } C_ ( 0 ..^ M ) ) -> { k e. ( 0 ..^ M ) | ( Q ` k ) < C } e. Fin )
11 9 6 10 mp2an
 |-  { k e. ( 0 ..^ M ) | ( Q ` k ) < C } e. Fin
12 11 a1i
 |-  ( ph -> { k e. ( 0 ..^ M ) | ( Q ` k ) < C } e. Fin )
13 0zd
 |-  ( ph -> 0 e. ZZ )
14 1 nnzd
 |-  ( ph -> M e. ZZ )
15 1 nngt0d
 |-  ( ph -> 0 < M )
16 fzolb
 |-  ( 0 e. ( 0 ..^ M ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
17 13 14 15 16 syl3anbrc
 |-  ( ph -> 0 e. ( 0 ..^ M ) )
18 elfzofz
 |-  ( 0 e. ( 0 ..^ M ) -> 0 e. ( 0 ... M ) )
19 17 18 syl
 |-  ( ph -> 0 e. ( 0 ... M ) )
20 2 19 ffvelrnd
 |-  ( ph -> ( Q ` 0 ) e. RR )
21 1 nnnn0d
 |-  ( ph -> M e. NN0 )
22 nn0uz
 |-  NN0 = ( ZZ>= ` 0 )
23 21 22 eleqtrdi
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
24 eluzfz2
 |-  ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
25 23 24 syl
 |-  ( ph -> M e. ( 0 ... M ) )
26 2 25 ffvelrnd
 |-  ( ph -> ( Q ` M ) e. RR )
27 20 26 iccssred
 |-  ( ph -> ( ( Q ` 0 ) [,] ( Q ` M ) ) C_ RR )
28 27 3 sseldd
 |-  ( ph -> C e. RR )
29 20 rexrd
 |-  ( ph -> ( Q ` 0 ) e. RR* )
30 26 rexrd
 |-  ( ph -> ( Q ` M ) e. RR* )
31 iccgelb
 |-  ( ( ( Q ` 0 ) e. RR* /\ ( Q ` M ) e. RR* /\ C e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( Q ` 0 ) <_ C )
32 29 30 3 31 syl3anc
 |-  ( ph -> ( Q ` 0 ) <_ C )
33 simpr
 |-  ( ( ph /\ C = ( Q ` 0 ) ) -> C = ( Q ` 0 ) )
34 2 ffnd
 |-  ( ph -> Q Fn ( 0 ... M ) )
35 34 adantr
 |-  ( ( ph /\ C = ( Q ` 0 ) ) -> Q Fn ( 0 ... M ) )
36 19 adantr
 |-  ( ( ph /\ C = ( Q ` 0 ) ) -> 0 e. ( 0 ... M ) )
37 fnfvelrn
 |-  ( ( Q Fn ( 0 ... M ) /\ 0 e. ( 0 ... M ) ) -> ( Q ` 0 ) e. ran Q )
38 35 36 37 syl2anc
 |-  ( ( ph /\ C = ( Q ` 0 ) ) -> ( Q ` 0 ) e. ran Q )
39 33 38 eqeltrd
 |-  ( ( ph /\ C = ( Q ` 0 ) ) -> C e. ran Q )
40 4 39 mtand
 |-  ( ph -> -. C = ( Q ` 0 ) )
41 40 neqned
 |-  ( ph -> C =/= ( Q ` 0 ) )
42 20 28 32 41 leneltd
 |-  ( ph -> ( Q ` 0 ) < C )
43 fveq2
 |-  ( k = 0 -> ( Q ` k ) = ( Q ` 0 ) )
44 43 breq1d
 |-  ( k = 0 -> ( ( Q ` k ) < C <-> ( Q ` 0 ) < C ) )
45 44 elrab
 |-  ( 0 e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } <-> ( 0 e. ( 0 ..^ M ) /\ ( Q ` 0 ) < C ) )
46 17 42 45 sylanbrc
 |-  ( ph -> 0 e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } )
47 46 ne0d
 |-  ( ph -> { k e. ( 0 ..^ M ) | ( Q ` k ) < C } =/= (/) )
48 fzossfz
 |-  ( 0 ..^ M ) C_ ( 0 ... M )
49 fzssz
 |-  ( 0 ... M ) C_ ZZ
50 zssre
 |-  ZZ C_ RR
51 49 50 sstri
 |-  ( 0 ... M ) C_ RR
52 48 51 sstri
 |-  ( 0 ..^ M ) C_ RR
53 6 52 sstri
 |-  { k e. ( 0 ..^ M ) | ( Q ` k ) < C } C_ RR
54 53 a1i
 |-  ( ph -> { k e. ( 0 ..^ M ) | ( Q ` k ) < C } C_ RR )
55 fisupcl
 |-  ( ( < Or RR /\ ( { k e. ( 0 ..^ M ) | ( Q ` k ) < C } e. Fin /\ { k e. ( 0 ..^ M ) | ( Q ` k ) < C } =/= (/) /\ { k e. ( 0 ..^ M ) | ( Q ` k ) < C } C_ RR ) ) -> sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) < C } , RR , < ) e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } )
56 8 12 47 54 55 syl13anc
 |-  ( ph -> sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) < C } , RR , < ) e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } )
57 6 56 sseldi
 |-  ( ph -> sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) < C } , RR , < ) e. ( 0 ..^ M ) )
58 5 57 eqeltrid
 |-  ( ph -> I e. ( 0 ..^ M ) )
59 48 58 sseldi
 |-  ( ph -> I e. ( 0 ... M ) )
60 2 59 ffvelrnd
 |-  ( ph -> ( Q ` I ) e. RR )
61 60 rexrd
 |-  ( ph -> ( Q ` I ) e. RR* )
62 fzofzp1
 |-  ( I e. ( 0 ..^ M ) -> ( I + 1 ) e. ( 0 ... M ) )
63 58 62 syl
 |-  ( ph -> ( I + 1 ) e. ( 0 ... M ) )
64 2 63 ffvelrnd
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. RR )
65 64 rexrd
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. RR* )
66 5 56 eqeltrid
 |-  ( ph -> I e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } )
67 fveq2
 |-  ( k = I -> ( Q ` k ) = ( Q ` I ) )
68 67 breq1d
 |-  ( k = I -> ( ( Q ` k ) < C <-> ( Q ` I ) < C ) )
69 68 elrab
 |-  ( I e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } <-> ( I e. ( 0 ..^ M ) /\ ( Q ` I ) < C ) )
70 66 69 sylib
 |-  ( ph -> ( I e. ( 0 ..^ M ) /\ ( Q ` I ) < C ) )
71 70 simprd
 |-  ( ph -> ( Q ` I ) < C )
72 52 58 sseldi
 |-  ( ph -> I e. RR )
73 ltp1
 |-  ( I e. RR -> I < ( I + 1 ) )
74 id
 |-  ( I e. RR -> I e. RR )
75 peano2re
 |-  ( I e. RR -> ( I + 1 ) e. RR )
76 74 75 ltnled
 |-  ( I e. RR -> ( I < ( I + 1 ) <-> -. ( I + 1 ) <_ I ) )
77 73 76 mpbid
 |-  ( I e. RR -> -. ( I + 1 ) <_ I )
78 72 77 syl
 |-  ( ph -> -. ( I + 1 ) <_ I )
79 48 49 sstri
 |-  ( 0 ..^ M ) C_ ZZ
80 6 79 sstri
 |-  { k e. ( 0 ..^ M ) | ( Q ` k ) < C } C_ ZZ
81 80 a1i
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> { k e. ( 0 ..^ M ) | ( Q ` k ) < C } C_ ZZ )
82 elrabi
 |-  ( h e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } -> h e. ( 0 ..^ M ) )
83 elfzo0le
 |-  ( h e. ( 0 ..^ M ) -> h <_ M )
84 82 83 syl
 |-  ( h e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } -> h <_ M )
85 84 adantl
 |-  ( ( ph /\ h e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } ) -> h <_ M )
86 85 ralrimiva
 |-  ( ph -> A. h e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } h <_ M )
87 breq2
 |-  ( m = M -> ( h <_ m <-> h <_ M ) )
88 87 ralbidv
 |-  ( m = M -> ( A. h e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } h <_ m <-> A. h e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } h <_ M ) )
89 88 rspcev
 |-  ( ( M e. ZZ /\ A. h e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } h <_ M ) -> E. m e. ZZ A. h e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } h <_ m )
90 14 86 89 syl2anc
 |-  ( ph -> E. m e. ZZ A. h e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } h <_ m )
91 90 adantr
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> E. m e. ZZ A. h e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } h <_ m )
92 elfzuz
 |-  ( ( I + 1 ) e. ( 0 ... M ) -> ( I + 1 ) e. ( ZZ>= ` 0 ) )
93 63 92 syl
 |-  ( ph -> ( I + 1 ) e. ( ZZ>= ` 0 ) )
94 93 adantr
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) e. ( ZZ>= ` 0 ) )
95 14 adantr
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> M e. ZZ )
96 51 63 sseldi
 |-  ( ph -> ( I + 1 ) e. RR )
97 96 adantr
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) e. RR )
98 95 zred
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> M e. RR )
99 elfzle2
 |-  ( ( I + 1 ) e. ( 0 ... M ) -> ( I + 1 ) <_ M )
100 63 99 syl
 |-  ( ph -> ( I + 1 ) <_ M )
101 100 adantr
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) <_ M )
102 simpr
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( Q ` ( I + 1 ) ) < C )
103 64 adantr
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( Q ` ( I + 1 ) ) e. RR )
104 28 adantr
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> C e. RR )
105 103 104 ltnled
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( ( Q ` ( I + 1 ) ) < C <-> -. C <_ ( Q ` ( I + 1 ) ) ) )
106 102 105 mpbid
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> -. C <_ ( Q ` ( I + 1 ) ) )
107 iccleub
 |-  ( ( ( Q ` 0 ) e. RR* /\ ( Q ` M ) e. RR* /\ C e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> C <_ ( Q ` M ) )
108 29 30 3 107 syl3anc
 |-  ( ph -> C <_ ( Q ` M ) )
109 108 adantr
 |-  ( ( ph /\ M = ( I + 1 ) ) -> C <_ ( Q ` M ) )
110 fveq2
 |-  ( M = ( I + 1 ) -> ( Q ` M ) = ( Q ` ( I + 1 ) ) )
111 110 adantl
 |-  ( ( ph /\ M = ( I + 1 ) ) -> ( Q ` M ) = ( Q ` ( I + 1 ) ) )
112 109 111 breqtrd
 |-  ( ( ph /\ M = ( I + 1 ) ) -> C <_ ( Q ` ( I + 1 ) ) )
113 112 adantlr
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) /\ M = ( I + 1 ) ) -> C <_ ( Q ` ( I + 1 ) ) )
114 106 113 mtand
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> -. M = ( I + 1 ) )
115 114 neqned
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> M =/= ( I + 1 ) )
116 97 98 101 115 leneltd
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) < M )
117 elfzo2
 |-  ( ( I + 1 ) e. ( 0 ..^ M ) <-> ( ( I + 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( I + 1 ) < M ) )
118 94 95 116 117 syl3anbrc
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) e. ( 0 ..^ M ) )
119 fveq2
 |-  ( k = ( I + 1 ) -> ( Q ` k ) = ( Q ` ( I + 1 ) ) )
120 119 breq1d
 |-  ( k = ( I + 1 ) -> ( ( Q ` k ) < C <-> ( Q ` ( I + 1 ) ) < C ) )
121 120 elrab
 |-  ( ( I + 1 ) e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } <-> ( ( I + 1 ) e. ( 0 ..^ M ) /\ ( Q ` ( I + 1 ) ) < C ) )
122 118 102 121 sylanbrc
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } )
123 suprzub
 |-  ( ( { k e. ( 0 ..^ M ) | ( Q ` k ) < C } C_ ZZ /\ E. m e. ZZ A. h e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } h <_ m /\ ( I + 1 ) e. { k e. ( 0 ..^ M ) | ( Q ` k ) < C } ) -> ( I + 1 ) <_ sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) < C } , RR , < ) )
124 81 91 122 123 syl3anc
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) <_ sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) < C } , RR , < ) )
125 124 5 breqtrrdi
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) <_ I )
126 78 125 mtand
 |-  ( ph -> -. ( Q ` ( I + 1 ) ) < C )
127 eqcom
 |-  ( ( Q ` ( I + 1 ) ) = C <-> C = ( Q ` ( I + 1 ) ) )
128 127 biimpi
 |-  ( ( Q ` ( I + 1 ) ) = C -> C = ( Q ` ( I + 1 ) ) )
129 128 adantl
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) = C ) -> C = ( Q ` ( I + 1 ) ) )
130 34 adantr
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) = C ) -> Q Fn ( 0 ... M ) )
131 63 adantr
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) = C ) -> ( I + 1 ) e. ( 0 ... M ) )
132 fnfvelrn
 |-  ( ( Q Fn ( 0 ... M ) /\ ( I + 1 ) e. ( 0 ... M ) ) -> ( Q ` ( I + 1 ) ) e. ran Q )
133 130 131 132 syl2anc
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) = C ) -> ( Q ` ( I + 1 ) ) e. ran Q )
134 129 133 eqeltrd
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) = C ) -> C e. ran Q )
135 4 134 mtand
 |-  ( ph -> -. ( Q ` ( I + 1 ) ) = C )
136 126 135 jca
 |-  ( ph -> ( -. ( Q ` ( I + 1 ) ) < C /\ -. ( Q ` ( I + 1 ) ) = C ) )
137 pm4.56
 |-  ( ( -. ( Q ` ( I + 1 ) ) < C /\ -. ( Q ` ( I + 1 ) ) = C ) <-> -. ( ( Q ` ( I + 1 ) ) < C \/ ( Q ` ( I + 1 ) ) = C ) )
138 136 137 sylib
 |-  ( ph -> -. ( ( Q ` ( I + 1 ) ) < C \/ ( Q ` ( I + 1 ) ) = C ) )
139 64 28 leloed
 |-  ( ph -> ( ( Q ` ( I + 1 ) ) <_ C <-> ( ( Q ` ( I + 1 ) ) < C \/ ( Q ` ( I + 1 ) ) = C ) ) )
140 138 139 mtbird
 |-  ( ph -> -. ( Q ` ( I + 1 ) ) <_ C )
141 28 64 ltnled
 |-  ( ph -> ( C < ( Q ` ( I + 1 ) ) <-> -. ( Q ` ( I + 1 ) ) <_ C ) )
142 140 141 mpbird
 |-  ( ph -> C < ( Q ` ( I + 1 ) ) )
143 61 65 28 71 142 eliood
 |-  ( ph -> C e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
144 fveq2
 |-  ( j = I -> ( Q ` j ) = ( Q ` I ) )
145 oveq1
 |-  ( j = I -> ( j + 1 ) = ( I + 1 ) )
146 145 fveq2d
 |-  ( j = I -> ( Q ` ( j + 1 ) ) = ( Q ` ( I + 1 ) ) )
147 144 146 oveq12d
 |-  ( j = I -> ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) = ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
148 147 eleq2d
 |-  ( j = I -> ( C e. ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) <-> C e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) )
149 148 rspcev
 |-  ( ( I e. ( 0 ..^ M ) /\ C e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> E. j e. ( 0 ..^ M ) C e. ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) )
150 58 143 149 syl2anc
 |-  ( ph -> E. j e. ( 0 ..^ M ) C e. ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) )