Metamath Proof Explorer

Theorem fourierdlem37

Description: I is a function that maps any real point to the point that in the partition that immediately precedes the corresponding periodic point in the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem37.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 ) ) ) } )
fourierdlem37.m 
|- ( ph -> M e. NN )
fourierdlem37.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem37.t 
|- T = ( B - A )
fourierdlem37.e 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
fourierdlem37.l 
|- L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
fourierdlem37.i 
|- I = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) )
Assertion 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 ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem37.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 ) ) ) } )
2 fourierdlem37.m 
 |-  ( ph -> M e. NN )
3 fourierdlem37.q 
 |-  ( ph -> Q e. ( P ` M ) )
4 fourierdlem37.t 
 |-  T = ( B - A )
5 fourierdlem37.e 
 |-  E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
6 fourierdlem37.l 
 |-  L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
7 fourierdlem37.i 
 |-  I = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) )
8 ssrab2 
 |-  { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } C_ ( 0 ..^ M )
9 ltso 
 |-  < Or RR
10 9 a1i 
 |-  ( ( ph /\ x e. RR ) -> < Or RR )
11 fzfi 
 |-  ( 0 ... M ) e. Fin
12 fzossfz 
 |-  ( 0 ..^ M ) C_ ( 0 ... M )
13 8 12 sstri 
 |-  { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } C_ ( 0 ... M )
14 ssfi 
 |-  ( ( ( 0 ... M ) e. Fin /\ { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } C_ ( 0 ... M ) ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } e. Fin )
15 11 13 14 mp2an 
 |-  { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } e. Fin
16 15 a1i 
 |-  ( ( ph /\ x e. RR ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } e. Fin )
17 0zd 
 |-  ( ph -> 0 e. ZZ )
18 2 nnzd 
 |-  ( ph -> M e. ZZ )
19 2 nngt0d 
 |-  ( ph -> 0 < M )
20 fzolb 
 |-  ( 0 e. ( 0 ..^ M ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
21 17 18 19 20 syl3anbrc 
 |-  ( ph -> 0 e. ( 0 ..^ M ) )
22 21 adantr 
 |-  ( ( ph /\ x e. RR ) -> 0 e. ( 0 ..^ M ) )
23 1 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 ) ) ) ) ) )
24 2 23 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 ) ) ) ) ) )
25 3 24 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
26 25 simprd 
 |-  ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
27 26 simplld 
 |-  ( ph -> ( Q ` 0 ) = A )
28 1 2 3 fourierdlem11 
 |-  ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
29 28 simp1d 
 |-  ( ph -> A e. RR )
30 27 29 eqeltrd 
 |-  ( ph -> ( Q ` 0 ) e. RR )
31 30 27 eqled 
 |-  ( ph -> ( Q ` 0 ) <_ A )
32 31 ad2antrr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( E ` x ) = B ) -> ( Q ` 0 ) <_ A )
33 iftrue 
 |-  ( ( E ` x ) = B -> if ( ( E ` x ) = B , A , ( E ` x ) ) = A )
34 33 eqcomd 
 |-  ( ( E ` x ) = B -> A = if ( ( E ` x ) = B , A , ( E ` x ) ) )
35 34 adantl 
 |-  ( ( ( ph /\ x e. RR ) /\ ( E ` x ) = B ) -> A = if ( ( E ` x ) = B , A , ( E ` x ) ) )
36 32 35 breqtrd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( E ` x ) = B ) -> ( Q ` 0 ) <_ if ( ( E ` x ) = B , A , ( E ` x ) ) )
37 30 adantr 
 |-  ( ( ph /\ x e. RR ) -> ( Q ` 0 ) e. RR )
38 29 adantr 
 |-  ( ( ph /\ x e. RR ) -> A e. RR )
39 38 rexrd 
 |-  ( ( ph /\ x e. RR ) -> A e. RR* )
40 28 simp2d 
 |-  ( ph -> B e. RR )
41 40 adantr 
 |-  ( ( ph /\ x e. RR ) -> B e. RR )
42 iocssre 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
43 39 41 42 syl2anc 
 |-  ( ( ph /\ x e. RR ) -> ( A (,] B ) C_ RR )
44 28 simp3d 
 |-  ( ph -> A < B )
45 29 40 44 4 5 fourierdlem4 
 |-  ( ph -> E : RR --> ( A (,] B ) )
46 45 ffvelrnda 
 |-  ( ( ph /\ x e. RR ) -> ( E ` x ) e. ( A (,] B ) )
47 43 46 sseldd 
 |-  ( ( ph /\ x e. RR ) -> ( E ` x ) e. RR )
48 27 adantr 
 |-  ( ( ph /\ x e. RR ) -> ( Q ` 0 ) = A )
49 elioc2 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( ( E ` x ) e. ( A (,] B ) <-> ( ( E ` x ) e. RR /\ A < ( E ` x ) /\ ( E ` x ) <_ B ) ) )
50 39 41 49 syl2anc 
 |-  ( ( ph /\ x e. RR ) -> ( ( E ` x ) e. ( A (,] B ) <-> ( ( E ` x ) e. RR /\ A < ( E ` x ) /\ ( E ` x ) <_ B ) ) )
51 46 50 mpbid 
 |-  ( ( ph /\ x e. RR ) -> ( ( E ` x ) e. RR /\ A < ( E ` x ) /\ ( E ` x ) <_ B ) )
52 51 simp2d 
 |-  ( ( ph /\ x e. RR ) -> A < ( E ` x ) )
53 48 52 eqbrtrd 
 |-  ( ( ph /\ x e. RR ) -> ( Q ` 0 ) < ( E ` x ) )
54 37 47 53 ltled 
 |-  ( ( ph /\ x e. RR ) -> ( Q ` 0 ) <_ ( E ` x ) )
55 54 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ -. ( E ` x ) = B ) -> ( Q ` 0 ) <_ ( E ` x ) )
56 iffalse 
 |-  ( -. ( E ` x ) = B -> if ( ( E ` x ) = B , A , ( E ` x ) ) = ( E ` x ) )
57 56 eqcomd 
 |-  ( -. ( E ` x ) = B -> ( E ` x ) = if ( ( E ` x ) = B , A , ( E ` x ) ) )
58 57 adantl 
 |-  ( ( ( ph /\ x e. RR ) /\ -. ( E ` x ) = B ) -> ( E ` x ) = if ( ( E ` x ) = B , A , ( E ` x ) ) )
59 55 58 breqtrd 
 |-  ( ( ( ph /\ x e. RR ) /\ -. ( E ` x ) = B ) -> ( Q ` 0 ) <_ if ( ( E ` x ) = B , A , ( E ` x ) ) )
60 36 59 pm2.61dan 
 |-  ( ( ph /\ x e. RR ) -> ( Q ` 0 ) <_ if ( ( E ` x ) = B , A , ( E ` x ) ) )
61 6 a1i 
 |-  ( ( ph /\ x e. RR ) -> L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) )
62 eqeq1 
 |-  ( y = ( E ` x ) -> ( y = B <-> ( E ` x ) = B ) )
63 id 
 |-  ( y = ( E ` x ) -> y = ( E ` x ) )
64 62 63 ifbieq2d 
 |-  ( y = ( E ` x ) -> if ( y = B , A , y ) = if ( ( E ` x ) = B , A , ( E ` x ) ) )
65 64 adantl 
 |-  ( ( ( ph /\ x e. RR ) /\ y = ( E ` x ) ) -> if ( y = B , A , y ) = if ( ( E ` x ) = B , A , ( E ` x ) ) )
66 38 47 ifcld 
 |-  ( ( ph /\ x e. RR ) -> if ( ( E ` x ) = B , A , ( E ` x ) ) e. RR )
67 61 65 46 66 fvmptd 
 |-  ( ( ph /\ x e. RR ) -> ( L ` ( E ` x ) ) = if ( ( E ` x ) = B , A , ( E ` x ) ) )
68 60 67 breqtrrd 
 |-  ( ( ph /\ x e. RR ) -> ( Q ` 0 ) <_ ( L ` ( E ` x ) ) )
69 fveq2 
 |-  ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
70 69 breq1d 
 |-  ( i = 0 -> ( ( Q ` i ) <_ ( L ` ( E ` x ) ) <-> ( Q ` 0 ) <_ ( L ` ( E ` x ) ) ) )
71 70 elrab 
 |-  ( 0 e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } <-> ( 0 e. ( 0 ..^ M ) /\ ( Q ` 0 ) <_ ( L ` ( E ` x ) ) ) )
72 22 68 71 sylanbrc 
 |-  ( ( ph /\ x e. RR ) -> 0 e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } )
73 72 ne0d 
 |-  ( ( ph /\ x e. RR ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } =/= (/) )
74 fzssz 
 |-  ( 0 ... M ) C_ ZZ
75 12 74 sstri 
 |-  ( 0 ..^ M ) C_ ZZ
76 zssre 
 |-  ZZ C_ RR
77 75 76 sstri 
 |-  ( 0 ..^ M ) C_ RR
78 8 77 sstri 
 |-  { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } C_ RR
79 78 a1i 
 |-  ( ( ph /\ x e. RR ) -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } C_ RR )
80 fisupcl 
 |-  ( ( < Or RR /\ ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } e. Fin /\ { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } =/= (/) /\ { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } C_ RR ) ) -> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } )
81 10 16 73 79 80 syl13anc 
 |-  ( ( 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 ) ) } )
82 8 81 sselid 
 |-  ( ( ph /\ x e. RR ) -> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) e. ( 0 ..^ M ) )
83 82 7 fmptd 
 |-  ( ph -> I : RR --> ( 0 ..^ M ) )
84 81 ex 
 |-  ( 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 ) ) } ) )
85 83 84 jca 
 |-  ( 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 ) ) } ) ) )