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

Theorem fourierdlem15 37861
Description: The range of the partition is between its starting point and its ending point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem15.1  |-  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 ) ) ) } )
fourierdlem15.2  |-  ( ph  ->  M  e.  NN )
fourierdlem15.3  |-  ( ph  ->  Q  e.  ( P `
 M ) )
Assertion
Ref Expression
fourierdlem15  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
Distinct variable groups:    A, i, m, p    B, i, m, p    i, M, m, p    Q, i, p    ph, i
Allowed substitution hints:    ph( m, p)    P( i, m, p)    Q( m)

Proof of Theorem fourierdlem15
Dummy variable  j is distinct from all other variables.
StepHypRef Expression
1 fourierdlem15.3 . . . . . 6  |-  ( ph  ->  Q  e.  ( P `
 M ) )
2 fourierdlem15.2 . . . . . . 7  |-  ( ph  ->  M  e.  NN )
3 fourierdlem15.1 . . . . . . . 8  |-  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 ) ) ) } )
43fourierdlem2 37848 . . . . . . 7  |-  ( 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 ) ) ) ) ) )
52, 4syl 17 . . . . . 6  |-  ( 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 ) ) ) ) ) )
61, 5mpbid 213 . . . . 5  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
76simpld 460 . . . 4  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
8 reex 9574 . . . . . 6  |-  RR  e.  _V
98a1i 11 . . . . 5  |-  ( ph  ->  RR  e.  _V )
10 ovex 6270 . . . . . 6  |-  ( 0 ... M )  e. 
_V
1110a1i 11 . . . . 5  |-  ( ph  ->  ( 0 ... M
)  e.  _V )
129, 11elmapd 7434 . . . 4  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  <-> 
Q : ( 0 ... M ) --> RR ) )
137, 12mpbid 213 . . 3  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
14 ffn 5682 . . 3  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
1513, 14syl 17 . 2  |-  ( ph  ->  Q  Fn  ( 0 ... M ) )
166simprd 464 . . . . . . . . 9  |-  ( ph  ->  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
1716simpld 460 . . . . . . . 8  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
1817simpld 460 . . . . . . 7  |-  ( ph  ->  ( Q `  0
)  =  A )
19 nnnn0 10820 . . . . . . . . . . 11  |-  ( M  e.  NN  ->  M  e.  NN0 )
20 nn0uz 11137 . . . . . . . . . . 11  |-  NN0  =  ( ZZ>= `  0 )
2119, 20syl6eleq 2510 . . . . . . . . . 10  |-  ( M  e.  NN  ->  M  e.  ( ZZ>= `  0 )
)
222, 21syl 17 . . . . . . . . 9  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
23 eluzfz1 11750 . . . . . . . . 9  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
2422, 23syl 17 . . . . . . . 8  |-  ( ph  ->  0  e.  ( 0 ... M ) )
2513, 24ffvelrnd 5975 . . . . . . 7  |-  ( ph  ->  ( Q `  0
)  e.  RR )
2618, 25eqeltrrd 2501 . . . . . 6  |-  ( ph  ->  A  e.  RR )
2726adantr 466 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  A  e.  RR )
2817simprd 464 . . . . . . 7  |-  ( ph  ->  ( Q `  M
)  =  B )
29 eluzfz2 11751 . . . . . . . . 9  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
3022, 29syl 17 . . . . . . . 8  |-  ( ph  ->  M  e.  ( 0 ... M ) )
3113, 30ffvelrnd 5975 . . . . . . 7  |-  ( ph  ->  ( Q `  M
)  e.  RR )
3228, 31eqeltrrd 2501 . . . . . 6  |-  ( ph  ->  B  e.  RR )
3332adantr 466 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  B  e.  RR )
3413ffvelrnda 5974 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  RR )
3518eqcomd 2428 . . . . . . 7  |-  ( ph  ->  A  =  ( Q `
 0 ) )
3635adantr 466 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  A  =  ( Q ` 
0 ) )
37 elfzuz 11740 . . . . . . . 8  |-  ( i  e.  ( 0 ... M )  ->  i  e.  ( ZZ>= `  0 )
)
3837adantl 467 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  i  e.  ( ZZ>= `  0 )
)
3913ad2antrr 730 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( 0 ... i
) )  ->  Q : ( 0 ... M ) --> RR )
40 elfzle1 11746 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... i )  ->  0  <_  j )
4140adantl 467 . . . . . . . . . 10  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... i ) )  ->  0  <_  j
)
42 elfzelz 11744 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... i )  ->  j  e.  ZZ )
4342zred 10984 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... i )  ->  j  e.  RR )
4443adantl 467 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... i ) )  ->  j  e.  RR )
45 elfzelz 11744 . . . . . . . . . . . . 13  |-  ( i  e.  ( 0 ... M )  ->  i  e.  ZZ )
4645zred 10984 . . . . . . . . . . . 12  |-  ( i  e.  ( 0 ... M )  ->  i  e.  RR )
4746adantr 466 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... i ) )  ->  i  e.  RR )
48 elfzel2 11742 . . . . . . . . . . . . 13  |-  ( i  e.  ( 0 ... M )  ->  M  e.  ZZ )
4948zred 10984 . . . . . . . . . . . 12  |-  ( i  e.  ( 0 ... M )  ->  M  e.  RR )
5049adantr 466 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... i ) )  ->  M  e.  RR )
51 elfzle2 11747 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... i )  ->  j  <_  i )
5251adantl 467 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... i ) )  ->  j  <_  i
)
53 elfzle2 11747 . . . . . . . . . . . 12  |-  ( i  e.  ( 0 ... M )  ->  i  <_  M )
5453adantr 466 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... i ) )  ->  i  <_  M
)
5544, 47, 50, 52, 54letrd 9736 . . . . . . . . . 10  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... i ) )  ->  j  <_  M
)
5642adantl 467 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... i ) )  ->  j  e.  ZZ )
57 0zd 10893 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... i ) )  ->  0  e.  ZZ )
5848adantr 466 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... i ) )  ->  M  e.  ZZ )
59 elfz 11734 . . . . . . . . . . 11  |-  ( ( j  e.  ZZ  /\  0  e.  ZZ  /\  M  e.  ZZ )  ->  (
j  e.  ( 0 ... M )  <->  ( 0  <_  j  /\  j  <_  M ) ) )
6056, 57, 58, 59syl3anc 1264 . . . . . . . . . 10  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... i ) )  ->  ( j  e.  ( 0 ... M
)  <->  ( 0  <_ 
j  /\  j  <_  M ) ) )
6141, 55, 60mpbir2and 930 . . . . . . . . 9  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... i ) )  ->  j  e.  ( 0 ... M ) )
6261adantll 718 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( 0 ... i
) )  ->  j  e.  ( 0 ... M
) )
6339, 62ffvelrnd 5975 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( 0 ... i
) )  ->  ( Q `  j )  e.  RR )
64 simpll 758 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( 0 ... (
i  -  1 ) ) )  ->  ph )
65 elfzle1 11746 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... ( i  -  1 ) )  ->  0  <_  j )
6665adantl 467 . . . . . . . . . 10  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  0  <_  j
)
67 elfzelz 11744 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... ( i  -  1 ) )  ->  j  e.  ZZ )
6867zred 10984 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... ( i  -  1 ) )  ->  j  e.  RR )
6968adantl 467 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  j  e.  RR )
7046adantr 466 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  i  e.  RR )
7149adantr 466 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  M  e.  RR )
72 peano2rem 9885 . . . . . . . . . . . . 13  |-  ( i  e.  RR  ->  (
i  -  1 )  e.  RR )
7370, 72syl 17 . . . . . . . . . . . 12  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  ( i  - 
1 )  e.  RR )
74 elfzle2 11747 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... ( i  -  1 ) )  ->  j  <_  ( i  -  1 ) )
7574adantl 467 . . . . . . . . . . . 12  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  j  <_  (
i  -  1 ) )
7670ltm1d 10483 . . . . . . . . . . . 12  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  ( i  - 
1 )  <  i
)
7769, 73, 70, 75, 76lelttrd 9737 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  j  <  i
)
7853adantr 466 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  i  <_  M
)
7969, 70, 71, 77, 78ltletrd 9739 . . . . . . . . . 10  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  j  <  M
)
8067adantl 467 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  j  e.  ZZ )
81 0zd 10893 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  0  e.  ZZ )
8248adantr 466 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  M  e.  ZZ )
83 elfzo 11866 . . . . . . . . . . 11  |-  ( ( j  e.  ZZ  /\  0  e.  ZZ  /\  M  e.  ZZ )  ->  (
j  e.  ( 0..^ M )  <->  ( 0  <_  j  /\  j  <  M ) ) )
8480, 81, 82, 83syl3anc 1264 . . . . . . . . . 10  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  ( j  e.  ( 0..^ M )  <-> 
( 0  <_  j  /\  j  <  M ) ) )
8566, 79, 84mpbir2and 930 . . . . . . . . 9  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( 0 ... ( i  - 
1 ) ) )  ->  j  e.  ( 0..^ M ) )
8685adantll 718 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( 0 ... (
i  -  1 ) ) )  ->  j  e.  ( 0..^ M ) )
8713adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
88 elfzofz 11879 . . . . . . . . . . 11  |-  ( j  e.  ( 0..^ M )  ->  j  e.  ( 0 ... M
) )
8988adantl 467 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  j  e.  ( 0 ... M ) )
9087, 89ffvelrnd 5975 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  ( Q `  j )  e.  RR )
91 fzofzp1 11951 . . . . . . . . . . 11  |-  ( j  e.  ( 0..^ M )  ->  ( j  +  1 )  e.  ( 0 ... M
) )
9291adantl 467 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  ( j  +  1 )  e.  ( 0 ... M ) )
9387, 92ffvelrnd 5975 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  ( Q `  ( j  +  1 ) )  e.  RR )
94 eleq1 2488 . . . . . . . . . . . 12  |-  ( i  =  j  ->  (
i  e.  ( 0..^ M )  <->  j  e.  ( 0..^ M ) ) )
9594anbi2d 708 . . . . . . . . . . 11  |-  ( i  =  j  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  j  e.  ( 0..^ M ) ) ) )
96 fveq2 5818 . . . . . . . . . . . 12  |-  ( i  =  j  ->  ( Q `  i )  =  ( Q `  j ) )
97 oveq1 6249 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  (
i  +  1 )  =  ( j  +  1 ) )
9897fveq2d 5822 . . . . . . . . . . . 12  |-  ( i  =  j  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( j  +  1 ) ) )
9996, 98breq12d 4372 . . . . . . . . . . 11  |-  ( i  =  j  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  j )  <  ( Q `  ( j  +  1 ) ) ) )
10095, 99imbi12d 321 . . . . . . . . . 10  |-  ( i  =  j  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  -> 
( Q `  i
)  <  ( Q `  ( i  +  1 ) ) )  <->  ( ( ph  /\  j  e.  ( 0..^ M ) )  ->  ( Q `  j )  <  ( Q `  ( j  +  1 ) ) ) ) )
10116simprd 464 . . . . . . . . . . 11  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
102101r19.21bi 2728 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
103100, 102chvarv 2073 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  ( Q `  j )  <  ( Q `  ( j  +  1 ) ) )
10490, 93, 103ltled 9727 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  ( Q `  j )  <_  ( Q `  ( j  +  1 ) ) )
10564, 86, 104syl2anc 665 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( 0 ... (
i  -  1 ) ) )  ->  ( Q `  j )  <_  ( Q `  (
j  +  1 ) ) )
10638, 63, 105monoord 12186 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  0 )  <_  ( Q `  i
) )
10736, 106eqbrtrd 4380 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  A  <_  ( Q `  i
) )
108 elfzuz3 11741 . . . . . . . 8  |-  ( i  e.  ( 0 ... M )  ->  M  e.  ( ZZ>= `  i )
)
109108adantl 467 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  M  e.  ( ZZ>= `  i )
)
11013ad2antrr 730 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... M
) )  ->  Q : ( 0 ... M ) --> RR )
111 fz0fzelfz0 11840 . . . . . . . . 9  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( i ... M ) )  -> 
j  e.  ( 0 ... M ) )
112111adantll 718 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... M
) )  ->  j  e.  ( 0 ... M
) )
113110, 112ffvelrnd 5975 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... M
) )  ->  ( Q `  j )  e.  RR )
11413ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  Q : ( 0 ... M ) --> RR )
115 0red 9588 . . . . . . . . . . . 12  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( i ... ( M  -  1 ) ) )  -> 
0  e.  RR )
11646adantr 466 . . . . . . . . . . . 12  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( i ... ( M  -  1 ) ) )  -> 
i  e.  RR )
117 elfzelz 11744 . . . . . . . . . . . . . 14  |-  ( j  e.  ( i ... ( M  -  1 ) )  ->  j  e.  ZZ )
118117zred 10984 . . . . . . . . . . . . 13  |-  ( j  e.  ( i ... ( M  -  1 ) )  ->  j  e.  RR )
119118adantl 467 . . . . . . . . . . . 12  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( i ... ( M  -  1 ) ) )  -> 
j  e.  RR )
120 elfzle1 11746 . . . . . . . . . . . . 13  |-  ( i  e.  ( 0 ... M )  ->  0  <_  i )
121120adantr 466 . . . . . . . . . . . 12  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( i ... ( M  -  1 ) ) )  -> 
0  <_  i )
122 elfzle1 11746 . . . . . . . . . . . . 13  |-  ( j  e.  ( i ... ( M  -  1 ) )  ->  i  <_  j )
123122adantl 467 . . . . . . . . . . . 12  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( i ... ( M  -  1 ) ) )  -> 
i  <_  j )
124115, 116, 119, 121, 123letrd 9736 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  j  e.  ( i ... ( M  -  1 ) ) )  -> 
0  <_  j )
125124adantll 718 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  0  <_  j )
126118adantl 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  j  e.  RR )
1272nnred 10568 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  RR )
128127adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  M  e.  RR )
129 1red 9602 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  1  e.  RR )
130128, 129resubcld 9991 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  ( M  -  1 )  e.  RR )
131 elfzle2 11747 . . . . . . . . . . . . . 14  |-  ( j  e.  ( i ... ( M  -  1 ) )  ->  j  <_  ( M  -  1 ) )
132131adantl 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  j  <_  ( M  -  1 ) )
133128ltm1d 10483 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  ( M  -  1 )  <  M )
134126, 130, 128, 132, 133lelttrd 9737 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  j  <  M )
135126, 128, 134ltled 9727 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  j  <_  M )
136135adantlr 719 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  j  <_  M )
137117adantl 467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  j  e.  ZZ )
138 0zd 10893 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  0  e.  ZZ )
13948ad2antlr 731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  M  e.  ZZ )
140137, 138, 139, 59syl3anc 1264 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  (
j  e.  ( 0 ... M )  <->  ( 0  <_  j  /\  j  <_  M ) ) )
141125, 136, 140mpbir2and 930 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  j  e.  ( 0 ... M
) )
142114, 141ffvelrnd 5975 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  ( Q `  j )  e.  RR )
143118adantl 467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  j  e.  RR )
144 1red 9602 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  1  e.  RR )
145 0le1 10081 . . . . . . . . . . . 12  |-  0  <_  1
146145a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  0  <_  1 )
147143, 144, 125, 146addge0d 10133 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  0  <_  ( j  +  1 ) )
148126, 130, 129, 132leadd1dd 10171 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  (
j  +  1 )  <_  ( ( M  -  1 )  +  1 ) )
1492nncnd 10569 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  CC )
150149adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  M  e.  CC )
151 1cnd 9603 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  1  e.  CC )
152150, 151npcand 9934 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  (
( M  -  1 )  +  1 )  =  M )
153148, 152breqtrd 4384 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  (
j  +  1 )  <_  M )
154153adantlr 719 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  (
j  +  1 )  <_  M )
155137peano2zd 10987 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  (
j  +  1 )  e.  ZZ )
156 elfz 11734 . . . . . . . . . . 11  |-  ( ( ( j  +  1 )  e.  ZZ  /\  0  e.  ZZ  /\  M  e.  ZZ )  ->  (
( j  +  1 )  e.  ( 0 ... M )  <->  ( 0  <_  ( j  +  1 )  /\  (
j  +  1 )  <_  M ) ) )
157155, 138, 139, 156syl3anc 1264 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  (
( j  +  1 )  e.  ( 0 ... M )  <->  ( 0  <_  ( j  +  1 )  /\  (
j  +  1 )  <_  M ) ) )
158147, 154, 157mpbir2and 930 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  (
j  +  1 )  e.  ( 0 ... M ) )
159114, 158ffvelrnd 5975 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  ( Q `  ( j  +  1 ) )  e.  RR )
160 simpll 758 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  ph )
161134adantlr 719 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  j  <  M )
162137, 138, 139, 83syl3anc 1264 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  (
j  e.  ( 0..^ M )  <->  ( 0  <_  j  /\  j  <  M ) ) )
163125, 161, 162mpbir2and 930 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  j  e.  ( 0..^ M ) )
164160, 163, 103syl2anc 665 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  ( Q `  j )  <  ( Q `  (
j  +  1 ) ) )
165142, 159, 164ltled 9727 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  j  e.  ( i ... ( M  -  1 ) ) )  ->  ( Q `  j )  <_  ( Q `  (
j  +  1 ) ) )
166109, 113, 165monoord 12186 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  <_  ( Q `  M
) )
16728adantr 466 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  M )  =  B )
168166, 167breqtrd 4384 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  <_  B )
16927, 33, 34, 107, 168eliccd 37487 . . . 4  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  ( A [,] B
) )
170169ralrimiva 2773 . . 3  |-  ( ph  ->  A. i  e.  ( 0 ... M ) ( Q `  i
)  e.  ( A [,] B ) )
171 fnfvrnss 6003 . . 3  |-  ( ( Q  Fn  ( 0 ... M )  /\  A. i  e.  ( 0 ... M ) ( Q `  i )  e.  ( A [,] B ) )  ->  ran  Q  C_  ( A [,] B ) )
17215, 170, 171syl2anc 665 . 2  |-  ( ph  ->  ran  Q  C_  ( A [,] B ) )
173 df-f 5541 . 2  |-  ( Q : ( 0 ... M ) --> ( A [,] B )  <->  ( Q  Fn  ( 0 ... M
)  /\  ran  Q  C_  ( A [,] B ) ) )
17415, 172, 173sylanbrc 668 1  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1872   A.wral 2708   {crab 2712   _Vcvv 3016    C_ wss 3372   class class class wbr 4359    |-> cmpt 4418   ran crn 4790    Fn wfn 5532   -->wf 5533   ` cfv 5537  (class class class)co 6242    ^m cmap 7420   CCcc 9481   RRcr 9482   0cc0 9483   1c1 9484    + caddc 9486    < clt 9619    <_ cle 9620    - cmin 9804   NNcn 10553   NN0cn0 10813   ZZcz 10881   ZZ>=cuz 11103   [,]cicc 11582   ...cfz 11728  ..^cfzo 11859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534  ax-cnex 9539  ax-resscn 9540  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-mulcom 9547  ax-addass 9548  ax-mulass 9549  ax-distr 9550  ax-i2m1 9551  ax-1ne0 9552  ax-1rid 9553  ax-rnegex 9554  ax-rrecex 9555  ax-cnre 9556  ax-pre-lttri 9557  ax-pre-lttrn 9558  ax-pre-ltadd 9559  ax-pre-mulgt0 9560
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-nel 2596  df-ral 2713  df-rex 2714  df-reu 2715  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-tp 3939  df-op 3941  df-uni 4156  df-iun 4237  df-br 4360  df-opab 4419  df-mpt 4420  df-tr 4455  df-eprel 4700  df-id 4704  df-po 4710  df-so 4711  df-fr 4748  df-we 4750  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-pred 5335  df-ord 5381  df-on 5382  df-lim 5383  df-suc 5384  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-riota 6204  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-om 6644  df-1st 6744  df-2nd 6745  df-wrecs 6976  df-recs 7038  df-rdg 7076  df-er 7311  df-map 7422  df-en 7518  df-dom 7519  df-sdom 7520  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-sub 9806  df-neg 9807  df-nn 10554  df-n0 10814  df-z 10882  df-uz 11104  df-icc 11586  df-fz 11729  df-fzo 11860
This theorem is referenced by:  fourierdlem38  37885  fourierdlem50  37897  fourierdlem54  37901  fourierdlem63  37910  fourierdlem65  37912  fourierdlem69  37916  fourierdlem70  37917  fourierdlem74  37921  fourierdlem75  37922  fourierdlem76  37923  fourierdlem79  37926  fourierdlem81  37928  fourierdlem84  37931  fourierdlem85  37932  fourierdlem88  37935  fourierdlem89  37936  fourierdlem90  37937  fourierdlem91  37938  fourierdlem92  37939  fourierdlem93  37940  fourierdlem100  37947  fourierdlem101  37948  fourierdlem103  37950  fourierdlem104  37951  fourierdlem107  37954  fourierdlem111  37958  fourierdlem112  37959  fourierdlem113  37960
  Copyright terms: Public domain W3C validator