Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem25 Structured version   Unicode version

Theorem fourierdlem25 31723
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.)
Hypotheses
Ref Expression
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
Ref Expression
fourierdlem25  |-  ( ph  ->  E. j  e.  ( 0..^ M ) C  e.  ( ( Q `
 j ) (,) ( Q `  (
j  +  1 ) ) ) )
Distinct variable groups:    C, k    C, j    j, I    k, I    k, M    j, M    Q, k    Q, j
Allowed substitution hints:    ph( j, k)

Proof of Theorem fourierdlem25
Dummy variables  h  m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem25.i . . 3  |-  I  =  sup ( { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
C } ,  RR ,  <  )
2 ssrab2 3590 . . . . 5  |-  { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
C }  C_  (
0..^ M )
32a1i 11 . . . 4  |-  ( ph  ->  { k  e.  ( 0..^ M )  |  ( Q `  k
)  <  C }  C_  ( 0..^ M ) )
4 ltso 9675 . . . . . 6  |-  <  Or  RR
54a1i 11 . . . . 5  |-  ( ph  ->  <  Or  RR )
6 fzofi 12062 . . . . . . 7  |-  ( 0..^ M )  e.  Fin
7 ssfi 7750 . . . . . . 7  |-  ( ( ( 0..^ M )  e.  Fin  /\  {
k  e.  ( 0..^ M )  |  ( Q `  k )  <  C }  C_  ( 0..^ M ) )  ->  { k  e.  ( 0..^ M )  |  ( Q `  k )  <  C }  e.  Fin )
86, 2, 7mp2an 672 . . . . . 6  |-  { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
C }  e.  Fin
98a1i 11 . . . . 5  |-  ( ph  ->  { k  e.  ( 0..^ M )  |  ( Q `  k
)  <  C }  e.  Fin )
10 0z 10885 . . . . . . . . . . 11  |-  0  e.  ZZ
1110a1i 11 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ZZ )
12 fourierdlem25.m . . . . . . . . . . 11  |-  ( ph  ->  M  e.  NN )
1312nnzd 10975 . . . . . . . . . 10  |-  ( ph  ->  M  e.  ZZ )
1412nngt0d 10589 . . . . . . . . . 10  |-  ( ph  ->  0  <  M )
1511, 13, 143jca 1176 . . . . . . . . 9  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  <  M ) )
16 fzolb 11812 . . . . . . . . 9  |-  ( 0  e.  ( 0..^ M )  <->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  < 
M ) )
1715, 16sylibr 212 . . . . . . . 8  |-  ( ph  ->  0  e.  ( 0..^ M ) )
18 fourierdlem25.qf . . . . . . . . . 10  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
19 elfzofz 11821 . . . . . . . . . . 11  |-  ( 0  e.  ( 0..^ M )  ->  0  e.  ( 0 ... M
) )
2017, 19syl 16 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ( 0 ... M ) )
2118, 20ffvelrnd 6032 . . . . . . . . 9  |-  ( ph  ->  ( Q `  0
)  e.  RR )
2212nnnn0d 10862 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  NN0 )
23 nn0uz 11126 . . . . . . . . . . . . . 14  |-  NN0  =  ( ZZ>= `  0 )
2422, 23syl6eleq 2565 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
25 eluzfz2 11704 . . . . . . . . . . . . 13  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
2624, 25syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ( 0 ... M ) )
2718, 26ffvelrnd 6032 . . . . . . . . . . 11  |-  ( ph  ->  ( Q `  M
)  e.  RR )
2821, 27iccssred 31394 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q ` 
0 ) [,] ( Q `  M )
)  C_  RR )
29 fourierdlem25.cel . . . . . . . . . 10  |-  ( ph  ->  C  e.  ( ( Q `  0 ) [,] ( Q `  M ) ) )
3028, 29sseldd 3510 . . . . . . . . 9  |-  ( ph  ->  C  e.  RR )
3121rexrd 9653 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  0
)  e.  RR* )
3227rexrd 9653 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  M
)  e.  RR* )
33 iccgelb 11591 . . . . . . . . . 10  |-  ( ( ( Q `  0
)  e.  RR*  /\  ( Q `  M )  e.  RR*  /\  C  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  ( Q `  0 )  <_  C )
3431, 32, 29, 33syl3anc 1228 . . . . . . . . 9  |-  ( ph  ->  ( Q `  0
)  <_  C )
35 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  C  =  ( Q `  0 ) )  ->  C  =  ( Q `  0 ) )
36 ffn 5736 . . . . . . . . . . . . . . 15  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
3718, 36syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  Q  Fn  ( 0 ... M ) )
3837adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  C  =  ( Q `  0 ) )  ->  Q  Fn  ( 0 ... M
) )
3920adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  C  =  ( Q `  0 ) )  ->  0  e.  ( 0 ... M
) )
40 fnfvelrn 6028 . . . . . . . . . . . . 13  |-  ( ( Q  Fn  ( 0 ... M )  /\  0  e.  ( 0 ... M ) )  ->  ( Q ` 
0 )  e.  ran  Q )
4138, 39, 40syl2anc 661 . . . . . . . . . . . 12  |-  ( (
ph  /\  C  =  ( Q `  0 ) )  ->  ( Q `  0 )  e. 
ran  Q )
4235, 41eqeltrd 2555 . . . . . . . . . . 11  |-  ( (
ph  /\  C  =  ( Q `  0 ) )  ->  C  e.  ran  Q )
43 fourierdlem25.cnel . . . . . . . . . . . 12  |-  ( ph  ->  -.  C  e.  ran  Q )
4443adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  C  =  ( Q `  0 ) )  ->  -.  C  e.  ran  Q )
4542, 44pm2.65da 576 . . . . . . . . . 10  |-  ( ph  ->  -.  C  =  ( Q `  0 ) )
4645neqned 2670 . . . . . . . . 9  |-  ( ph  ->  C  =/=  ( Q `
 0 ) )
4721, 30, 34, 46leneltd 31362 . . . . . . . 8  |-  ( ph  ->  ( Q `  0
)  <  C )
4817, 47jca 532 . . . . . . 7  |-  ( ph  ->  ( 0  e.  ( 0..^ M )  /\  ( Q `  0 )  <  C ) )
49 fveq2 5871 . . . . . . . . 9  |-  ( k  =  0  ->  ( Q `  k )  =  ( Q ` 
0 ) )
5049breq1d 4462 . . . . . . . 8  |-  ( k  =  0  ->  (
( Q `  k
)  <  C  <->  ( Q `  0 )  < 
C ) )
5150elrab 3266 . . . . . . 7  |-  ( 0  e.  { k  e.  ( 0..^ M )  |  ( Q `  k )  <  C } 
<->  ( 0  e.  ( 0..^ M )  /\  ( Q `  0 )  <  C ) )
5248, 51sylibr 212 . . . . . 6  |-  ( ph  ->  0  e.  { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
C } )
53 ne0i 3796 . . . . . 6  |-  ( 0  e.  { k  e.  ( 0..^ M )  |  ( Q `  k )  <  C }  ->  { k  e.  ( 0..^ M )  |  ( Q `  k )  <  C }  =/=  (/) )
5452, 53syl 16 . . . . 5  |-  ( ph  ->  { k  e.  ( 0..^ M )  |  ( Q `  k
)  <  C }  =/=  (/) )
55 fzossfz 11824 . . . . . . . 8  |-  ( 0..^ M )  C_  (
0 ... M )
56 fzssz 31334 . . . . . . . . 9  |-  ( 0 ... M )  C_  ZZ
57 zssre 10881 . . . . . . . . 9  |-  ZZ  C_  RR
5856, 57sstri 3518 . . . . . . . 8  |-  ( 0 ... M )  C_  RR
5955, 58sstri 3518 . . . . . . 7  |-  ( 0..^ M )  C_  RR
602, 59sstri 3518 . . . . . 6  |-  { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
C }  C_  RR
6160a1i 11 . . . . 5  |-  ( ph  ->  { k  e.  ( 0..^ M )  |  ( Q `  k
)  <  C }  C_  RR )
62 fisupcl 7937 . . . . 5  |-  ( (  <  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 }
)
635, 9, 54, 61, 62syl13anc 1230 . . . 4  |-  ( ph  ->  sup ( { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
C } ,  RR ,  <  )  e.  {
k  e.  ( 0..^ M )  |  ( Q `  k )  <  C } )
643, 63sseldd 3510 . . 3  |-  ( ph  ->  sup ( { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
C } ,  RR ,  <  )  e.  ( 0..^ M ) )
651, 64syl5eqel 2559 . 2  |-  ( ph  ->  I  e.  ( 0..^ M ) )
6655, 65sseldi 3507 . . . . 5  |-  ( ph  ->  I  e.  ( 0 ... M ) )
6718, 66ffvelrnd 6032 . . . 4  |-  ( ph  ->  ( Q `  I
)  e.  RR )
6867rexrd 9653 . . 3  |-  ( ph  ->  ( Q `  I
)  e.  RR* )
69 fzofzp1 11887 . . . . . 6  |-  ( I  e.  ( 0..^ M )  ->  ( I  +  1 )  e.  ( 0 ... M
) )
7065, 69syl 16 . . . . 5  |-  ( ph  ->  ( I  +  1 )  e.  ( 0 ... M ) )
7118, 70ffvelrnd 6032 . . . 4  |-  ( ph  ->  ( Q `  (
I  +  1 ) )  e.  RR )
7271rexrd 9653 . . 3  |-  ( ph  ->  ( Q `  (
I  +  1 ) )  e.  RR* )
731, 63syl5eqel 2559 . . . . 5  |-  ( ph  ->  I  e.  { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
C } )
74 fveq2 5871 . . . . . . 7  |-  ( k  =  I  ->  ( Q `  k )  =  ( Q `  I ) )
7574breq1d 4462 . . . . . 6  |-  ( k  =  I  ->  (
( Q `  k
)  <  C  <->  ( Q `  I )  <  C
) )
7675elrab 3266 . . . . 5  |-  ( I  e.  { k  e.  ( 0..^ M )  |  ( Q `  k )  <  C } 
<->  ( I  e.  ( 0..^ M )  /\  ( Q `  I )  <  C ) )
7773, 76sylib 196 . . . 4  |-  ( ph  ->  ( I  e.  ( 0..^ M )  /\  ( Q `  I )  <  C ) )
7877simprd 463 . . 3  |-  ( ph  ->  ( Q `  I
)  <  C )
7955, 56sstri 3518 . . . . . . . . . . . 12  |-  ( 0..^ M )  C_  ZZ
802, 79sstri 3518 . . . . . . . . . . 11  |-  { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
C }  C_  ZZ
8180a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  { k  e.  ( 0..^ M )  |  ( Q `  k )  <  C }  C_  ZZ )
822sseli 3505 . . . . . . . . . . . . . . 15  |-  ( h  e.  { k  e.  ( 0..^ M )  |  ( Q `  k )  <  C }  ->  h  e.  ( 0..^ M ) )
8359sseli 3505 . . . . . . . . . . . . . . . 16  |-  ( h  e.  ( 0..^ M )  ->  h  e.  RR )
84 elfzoel2 11806 . . . . . . . . . . . . . . . . 17  |-  ( h  e.  ( 0..^ M )  ->  M  e.  ZZ )
8557sseli 3505 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  ZZ  ->  M  e.  RR )
8684, 85syl 16 . . . . . . . . . . . . . . . 16  |-  ( h  e.  ( 0..^ M )  ->  M  e.  RR )
87 elfzolt2 11815 . . . . . . . . . . . . . . . 16  |-  ( h  e.  ( 0..^ M )  ->  h  <  M )
8883, 86, 87ltled 9742 . . . . . . . . . . . . . . 15  |-  ( h  e.  ( 0..^ M )  ->  h  <_  M )
8982, 88syl 16 . . . . . . . . . . . . . 14  |-  ( h  e.  { k  e.  ( 0..^ M )  |  ( Q `  k )  <  C }  ->  h  <_  M
)
9089adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  h  e.  { k  e.  ( 0..^ M )  |  ( Q `  k )  <  C } )  ->  h  <_  M
)
9190ralrimiva 2881 . . . . . . . . . . . 12  |-  ( ph  ->  A. h  e.  {
k  e.  ( 0..^ M )  |  ( Q `  k )  <  C } h  <_  M )
92 breq2 4456 . . . . . . . . . . . . . 14  |-  ( m  =  M  ->  (
h  <_  m  <->  h  <_  M ) )
9392ralbidv 2906 . . . . . . . . . . . . 13  |-  ( 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 ) )
9493rspcev 3219 . . . . . . . . . . . 12  |-  ( ( 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 )
9513, 91, 94syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  E. m  e.  ZZ  A. h  e.  { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
C } h  <_  m )
9695adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  E. m  e.  ZZ  A. h  e. 
{ k  e.  ( 0..^ M )  |  ( Q `  k
)  <  C }
h  <_  m )
97 elfzuz 11694 . . . . . . . . . . . . . . . 16  |-  ( ( I  +  1 )  e.  ( 0 ... M )  ->  (
I  +  1 )  e.  ( ZZ>= `  0
) )
9870, 97syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( I  +  1 )  e.  ( ZZ>= ` 
0 ) )
9998adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  ( I  +  1 )  e.  ( ZZ>= `  0 )
)
10013adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  M  e.  ZZ )
10158, 70sseldi 3507 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( I  +  1 )  e.  RR )
102101adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  ( I  +  1 )  e.  RR )
103100, 85syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  M  e.  RR )
104 elfzle2 11700 . . . . . . . . . . . . . . . . 17  |-  ( ( I  +  1 )  e.  ( 0 ... M )  ->  (
I  +  1 )  <_  M )
10570, 104syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( I  +  1 )  <_  M )
106105adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  ( I  +  1 )  <_  M )
107 iccleub 11590 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( Q `  0
)  e.  RR*  /\  ( Q `  M )  e.  RR*  /\  C  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  C  <_  ( Q `  M
) )
10831, 32, 29, 107syl3anc 1228 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  C  <_  ( Q `  M ) )
109108adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  M  =  ( I  +  1
) )  ->  C  <_  ( Q `  M
) )
110 fveq2 5871 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  =  ( I  + 
1 )  ->  ( Q `  M )  =  ( Q `  ( I  +  1
) ) )
111110adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  M  =  ( I  +  1
) )  ->  ( Q `  M )  =  ( Q `  ( I  +  1
) ) )
112109, 111breqtrd 4476 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  M  =  ( I  +  1
) )  ->  C  <_  ( Q `  (
I  +  1 ) ) )
113112adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ( Q `  ( I  +  1 ) )  <  C )  /\  M  =  ( I  +  1 ) )  ->  C  <_  ( Q `  ( I  +  1 ) ) )
114 simpr 461 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  ( Q `  ( I  +  1 ) )  <  C
)
11571adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  ( Q `  ( I  +  1 ) )  e.  RR )
11630adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  C  e.  RR )
117115, 116ltnled 9741 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  ( ( Q `  ( I  +  1 ) )  <  C  <->  -.  C  <_  ( Q `  (
I  +  1 ) ) ) )
118114, 117mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  -.  C  <_  ( Q `  (
I  +  1 ) ) )
119118adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ( Q `  ( I  +  1 ) )  <  C )  /\  M  =  ( I  +  1 ) )  ->  -.  C  <_  ( Q `  ( I  +  1 ) ) )
120113, 119pm2.65da 576 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  -.  M  =  ( I  + 
1 ) )
121120neqned 2670 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  M  =/=  ( I  +  1
) )
122102, 103, 106, 121leneltd 31362 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  ( I  +  1 )  < 
M )
12399, 100, 1223jca 1176 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  ( (
I  +  1 )  e.  ( ZZ>= `  0
)  /\  M  e.  ZZ  /\  ( I  + 
1 )  <  M
) )
124 elfzo2 11810 . . . . . . . . . . . . 13  |-  ( ( I  +  1 )  e.  ( 0..^ M )  <->  ( ( I  +  1 )  e.  ( ZZ>= `  0 )  /\  M  e.  ZZ  /\  ( I  +  1 )  <  M ) )
125123, 124sylibr 212 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  ( I  +  1 )  e.  ( 0..^ M ) )
126125, 114jca 532 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  ( (
I  +  1 )  e.  ( 0..^ M )  /\  ( Q `
 ( I  + 
1 ) )  < 
C ) )
127 fveq2 5871 . . . . . . . . . . . . 13  |-  ( k  =  ( I  + 
1 )  ->  ( Q `  k )  =  ( Q `  ( I  +  1
) ) )
128127breq1d 4462 . . . . . . . . . . . 12  |-  ( k  =  ( I  + 
1 )  ->  (
( Q `  k
)  <  C  <->  ( Q `  ( I  +  1 ) )  <  C
) )
129128elrab 3266 . . . . . . . . . . 11  |-  ( ( I  +  1 )  e.  { k  e.  ( 0..^ M )  |  ( Q `  k )  <  C } 
<->  ( ( I  + 
1 )  e.  ( 0..^ M )  /\  ( Q `  ( I  +  1 ) )  <  C ) )
130126, 129sylibr 212 . . . . . . . . . 10  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  ( I  +  1 )  e. 
{ k  e.  ( 0..^ M )  |  ( Q `  k
)  <  C }
)
131 suprzub 11183 . . . . . . . . . 10  |-  ( ( { 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 ,  <  )
)
13281, 96, 130, 131syl3anc 1228 . . . . . . . . 9  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  ( I  +  1 )  <_  sup ( { k  e.  ( 0..^ M )  |  ( Q `  k )  <  C } ,  RR ,  <  ) )
1331eqcomi 2480 . . . . . . . . . 10  |-  sup ( { k  e.  ( 0..^ M )  |  ( Q `  k
)  <  C } ,  RR ,  <  )  =  I
134133a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  sup ( { k  e.  ( 0..^ M )  |  ( Q `  k
)  <  C } ,  RR ,  <  )  =  I )
135132, 134breqtrd 4476 . . . . . . . 8  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  ( I  +  1 )  <_  I )
13659, 65sseldi 3507 . . . . . . . . . 10  |-  ( ph  ->  I  e.  RR )
137 ltp1 10390 . . . . . . . . . . 11  |-  ( I  e.  RR  ->  I  <  ( I  +  1 ) )
138 id 22 . . . . . . . . . . . 12  |-  ( I  e.  RR  ->  I  e.  RR )
139 peano2re 9762 . . . . . . . . . . . 12  |-  ( I  e.  RR  ->  (
I  +  1 )  e.  RR )
140138, 139ltnled 9741 . . . . . . . . . . 11  |-  ( I  e.  RR  ->  (
I  <  ( I  +  1 )  <->  -.  (
I  +  1 )  <_  I ) )
141137, 140mpbid 210 . . . . . . . . . 10  |-  ( I  e.  RR  ->  -.  ( I  +  1
)  <_  I )
142136, 141syl 16 . . . . . . . . 9  |-  ( ph  ->  -.  ( I  + 
1 )  <_  I
)
143142adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  <  C
)  ->  -.  (
I  +  1 )  <_  I )
144135, 143pm2.65da 576 . . . . . . 7  |-  ( ph  ->  -.  ( Q `  ( I  +  1
) )  <  C
)
145 eqcom 2476 . . . . . . . . . . 11  |-  ( ( Q `  ( I  +  1 ) )  =  C  <->  C  =  ( Q `  ( I  +  1 ) ) )
146145biimpi 194 . . . . . . . . . 10  |-  ( ( Q `  ( I  +  1 ) )  =  C  ->  C  =  ( Q `  ( I  +  1
) ) )
147146adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  =  C )  ->  C  =  ( Q `  ( I  +  1 ) ) )
14837adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  =  C )  ->  Q  Fn  ( 0 ... M
) )
14970adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  =  C )  ->  ( I  +  1 )  e.  ( 0 ... M
) )
150 fnfvelrn 6028 . . . . . . . . . 10  |-  ( ( Q  Fn  ( 0 ... M )  /\  ( I  +  1
)  e.  ( 0 ... M ) )  ->  ( Q `  ( I  +  1
) )  e.  ran  Q )
151148, 149, 150syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  =  C )  ->  ( Q `  ( I  +  1 ) )  e.  ran  Q )
152147, 151eqeltrd 2555 . . . . . . . 8  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  =  C )  ->  C  e.  ran  Q )
15343adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( Q `  ( I  +  1 ) )  =  C )  ->  -.  C  e.  ran  Q )
154152, 153pm2.65da 576 . . . . . . 7  |-  ( ph  ->  -.  ( Q `  ( I  +  1
) )  =  C )
155144, 154jca 532 . . . . . 6  |-  ( ph  ->  ( -.  ( Q `
 ( I  + 
1 ) )  < 
C  /\  -.  ( Q `  ( I  +  1 ) )  =  C ) )
156 pm4.56 495 . . . . . 6  |-  ( ( -.  ( Q `  ( I  +  1
) )  <  C  /\  -.  ( Q `  ( I  +  1
) )  =  C )  <->  -.  ( ( Q `  ( I  +  1 ) )  <  C  \/  ( Q `  ( I  +  1 ) )  =  C ) )
157155, 156sylib 196 . . . . 5  |-  ( ph  ->  -.  ( ( Q `
 ( I  + 
1 ) )  < 
C  \/  ( Q `
 ( I  + 
1 ) )  =  C ) )
158 leloe 9681 . . . . . 6  |-  ( ( ( Q `  (
I  +  1 ) )  e.  RR  /\  C  e.  RR )  ->  ( ( Q `  ( I  +  1
) )  <_  C  <->  ( ( Q `  (
I  +  1 ) )  <  C  \/  ( Q `  ( I  +  1 ) )  =  C ) ) )
15971, 30, 158syl2anc 661 . . . . 5  |-  ( ph  ->  ( ( Q `  ( I  +  1
) )  <_  C  <->  ( ( Q `  (
I  +  1 ) )  <  C  \/  ( Q `  ( I  +  1 ) )  =  C ) ) )
160157, 159mtbird 301 . . . 4  |-  ( ph  ->  -.  ( Q `  ( I  +  1
) )  <_  C
)
16130, 71ltnled 9741 . . . 4  |-  ( ph  ->  ( C  <  ( Q `  ( I  +  1 ) )  <->  -.  ( Q `  (
I  +  1 ) )  <_  C )
)
162160, 161mpbird 232 . . 3  |-  ( ph  ->  C  <  ( Q `
 ( I  + 
1 ) ) )
16368, 72, 30, 78, 162eliood 31386 . 2  |-  ( ph  ->  C  e.  ( ( Q `  I ) (,) ( Q `  ( I  +  1
) ) ) )
164 fveq2 5871 . . . . 5  |-  ( j  =  I  ->  ( Q `  j )  =  ( Q `  I ) )
165 oveq1 6301 . . . . . 6  |-  ( j  =  I  ->  (
j  +  1 )  =  ( I  + 
1 ) )
166165fveq2d 5875 . . . . 5  |-  ( j  =  I  ->  ( Q `  ( j  +  1 ) )  =  ( Q `  ( I  +  1
) ) )
167164, 166oveq12d 6312 . . . 4  |-  ( j  =  I  ->  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) )  =  ( ( Q `
 I ) (,) ( Q `  (
I  +  1 ) ) ) )
168167eleq2d 2537 . . 3  |-  ( j  =  I  ->  ( C  e.  ( ( Q `  j ) (,) ( Q `  (
j  +  1 ) ) )  <->  C  e.  ( ( Q `  I ) (,) ( Q `  ( I  +  1 ) ) ) ) )
169168rspcev 3219 . 2  |-  ( ( I  e.  ( 0..^ M )  /\  C  e.  ( ( Q `  I ) (,) ( Q `  ( I  +  1 ) ) ) )  ->  E. j  e.  ( 0..^ M ) C  e.  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) )
17065, 163, 169syl2anc 661 1  |-  ( ph  ->  E. j  e.  ( 0..^ M ) C  e.  ( ( Q `
 j ) (,) ( Q `  (
j  +  1 ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767    =/= wne 2662   A.wral 2817   E.wrex 2818   {crab 2821    C_ wss 3481   (/)c0 3790   class class class wbr 4452    Or wor 4804   ran crn 5005    Fn wfn 5588   -->wf 5589   ` cfv 5593  (class class class)co 6294   Fincfn 7526   supcsup 7910   RRcr 9501   0cc0 9502   1c1 9503    + caddc 9505   RR*cxr 9637    < clt 9638    <_ cle 9639   NNcn 10546   NN0cn0 10805   ZZcz 10874   ZZ>=cuz 11092   (,)cioo 11539   [,]cicc 11542   ...cfz 11682  ..^cfzo 11802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6586  ax-cnex 9558  ax-resscn 9559  ax-1cn 9560  ax-icn 9561  ax-addcl 9562  ax-addrcl 9563  ax-mulcl 9564  ax-mulrcl 9565  ax-mulcom 9566  ax-addass 9567  ax-mulass 9568  ax-distr 9569  ax-i2m1 9570  ax-1ne0 9571  ax-1rid 9572  ax-rnegex 9573  ax-rrecex 9574  ax-cnre 9575  ax-pre-lttri 9576  ax-pre-lttrn 9577  ax-pre-ltadd 9578  ax-pre-mulgt0 9579
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4251  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6255  df-ov 6297  df-oprab 6298  df-mpt2 6299  df-om 6695  df-1st 6794  df-2nd 6795  df-recs 7052  df-rdg 7086  df-1o 7140  df-er 7321  df-en 7527  df-dom 7528  df-sdom 7529  df-fin 7530  df-sup 7911  df-pnf 9640  df-mnf 9641  df-xr 9642  df-ltxr 9643  df-le 9644  df-sub 9817  df-neg 9818  df-nn 10547  df-n0 10806  df-z 10875  df-uz 11093  df-ioo 11543  df-icc 11546  df-fz 11683  df-fzo 11803
This theorem is referenced by:  fourierdlem41  31739  fourierdlem48  31746  fourierdlem49  31747  fourierdlem70  31768  fourierdlem71  31769  fourierdlem103  31801  fourierdlem104  31802
  Copyright terms: Public domain W3C validator