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