Metamath Proof Explorer

Theorem fourierdlem14

Description: Given the partition V , Q is the partition shifted to the left by X . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem14.1 
|- ( ph -> A e. RR )
fourierdlem14.2 
|- ( ph -> B e. RR )
fourierdlem14.x 
|- ( ph -> X e. RR )
fourierdlem14.p 
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + X ) /\ ( p ` m ) = ( B + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem14.o 
|- O = ( 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 ) ) ) } )
fourierdlem14.m 
|- ( ph -> M e. NN )
fourierdlem14.v 
|- ( ph -> V e. ( P ` M ) )
fourierdlem14.q 
|- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
Assertion fourierdlem14 
|- ( ph -> Q e. ( O ` M ) )

Proof

Step Hyp Ref Expression
1 fourierdlem14.1 
 |-  ( ph -> A e. RR )
2 fourierdlem14.2 
 |-  ( ph -> B e. RR )
3 fourierdlem14.x 
 |-  ( ph -> X e. RR )
4 fourierdlem14.p 
 |-  P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + X ) /\ ( p ` m ) = ( B + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
5 fourierdlem14.o 
 |-  O = ( 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 ) ) ) } )
6 fourierdlem14.m 
 |-  ( ph -> M e. NN )
7 fourierdlem14.v 
 |-  ( ph -> V e. ( P ` M ) )
8 fourierdlem14.q 
 |-  Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
9 4 fourierdlem2 
 |-  ( M e. NN -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( A + X ) /\ ( V ` M ) = ( B + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
10 6 9 syl 
 |-  ( ph -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( A + X ) /\ ( V ` M ) = ( B + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
11 7 10 mpbid 
 |-  ( ph -> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( A + X ) /\ ( V ` M ) = ( B + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) )
12 11 simpld 
 |-  ( ph -> V e. ( RR ^m ( 0 ... M ) ) )
13 elmapi 
 |-  ( V e. ( RR ^m ( 0 ... M ) ) -> V : ( 0 ... M ) --> RR )
14 12 13 syl 
 |-  ( ph -> V : ( 0 ... M ) --> RR )
15 14 ffvelrnda 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( V ` i ) e. RR )
16 3 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> X e. RR )
17 15 16 resubcld 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) - X ) e. RR )
18 17 8 fmptd 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
19 reex 
 |-  RR e. _V
20 19 a1i 
 |-  ( ph -> RR e. _V )
21 ovex 
 |-  ( 0 ... M ) e. _V
22 21 a1i 
 |-  ( ph -> ( 0 ... M ) e. _V )
23 20 22 elmapd 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) <-> Q : ( 0 ... M ) --> RR ) )
24 18 23 mpbird 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
25 8 a1i 
 |-  ( ph -> Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) ) )
26 fveq2 
 |-  ( i = 0 -> ( V ` i ) = ( V ` 0 ) )
27 26 oveq1d 
 |-  ( i = 0 -> ( ( V ` i ) - X ) = ( ( V ` 0 ) - X ) )
28 27 adantl 
 |-  ( ( ph /\ i = 0 ) -> ( ( V ` i ) - X ) = ( ( V ` 0 ) - X ) )
29 0zd 
 |-  ( ph -> 0 e. ZZ )
30 6 nnzd 
 |-  ( ph -> M e. ZZ )
31 29 30 29 3jca 
 |-  ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) )
32 0le0 
 |-  0 <_ 0
33 32 a1i 
 |-  ( ph -> 0 <_ 0 )
34 0red 
 |-  ( ph -> 0 e. RR )
35 6 nnred 
 |-  ( ph -> M e. RR )
36 6 nngt0d 
 |-  ( ph -> 0 < M )
37 34 35 36 ltled 
 |-  ( ph -> 0 <_ M )
38 31 33 37 jca32 
 |-  ( ph -> ( ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) /\ ( 0 <_ 0 /\ 0 <_ M ) ) )
39 elfz2 
 |-  ( 0 e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) /\ ( 0 <_ 0 /\ 0 <_ M ) ) )
40 38 39 sylibr 
 |-  ( ph -> 0 e. ( 0 ... M ) )
41 14 40 ffvelrnd 
 |-  ( ph -> ( V ` 0 ) e. RR )
42 41 3 resubcld 
 |-  ( ph -> ( ( V ` 0 ) - X ) e. RR )
43 25 28 40 42 fvmptd 
 |-  ( ph -> ( Q ` 0 ) = ( ( V ` 0 ) - X ) )
44 11 simprd 
 |-  ( ph -> ( ( ( V ` 0 ) = ( A + X ) /\ ( V ` M ) = ( B + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) )
45 44 simpld 
 |-  ( ph -> ( ( V ` 0 ) = ( A + X ) /\ ( V ` M ) = ( B + X ) ) )
46 45 simpld 
 |-  ( ph -> ( V ` 0 ) = ( A + X ) )
47 46 oveq1d 
 |-  ( ph -> ( ( V ` 0 ) - X ) = ( ( A + X ) - X ) )
48 1 recnd 
 |-  ( ph -> A e. CC )
49 3 recnd 
 |-  ( ph -> X e. CC )
50 48 49 pncand 
 |-  ( ph -> ( ( A + X ) - X ) = A )
51 43 47 50 3eqtrd 
 |-  ( ph -> ( Q ` 0 ) = A )
52 fveq2 
 |-  ( i = M -> ( V ` i ) = ( V ` M ) )
53 52 oveq1d 
 |-  ( i = M -> ( ( V ` i ) - X ) = ( ( V ` M ) - X ) )
54 53 adantl 
 |-  ( ( ph /\ i = M ) -> ( ( V ` i ) - X ) = ( ( V ` M ) - X ) )
55 29 30 30 3jca 
 |-  ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ M e. ZZ ) )
56 35 leidd 
 |-  ( ph -> M <_ M )
57 55 37 56 jca32 
 |-  ( ph -> ( ( 0 e. ZZ /\ M e. ZZ /\ M e. ZZ ) /\ ( 0 <_ M /\ M <_ M ) ) )
58 elfz2 
 |-  ( M e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ M e. ZZ ) /\ ( 0 <_ M /\ M <_ M ) ) )
59 57 58 sylibr 
 |-  ( ph -> M e. ( 0 ... M ) )
60 14 59 ffvelrnd 
 |-  ( ph -> ( V ` M ) e. RR )
61 60 3 resubcld 
 |-  ( ph -> ( ( V ` M ) - X ) e. RR )
62 25 54 59 61 fvmptd 
 |-  ( ph -> ( Q ` M ) = ( ( V ` M ) - X ) )
63 45 simprd 
 |-  ( ph -> ( V ` M ) = ( B + X ) )
64 63 oveq1d 
 |-  ( ph -> ( ( V ` M ) - X ) = ( ( B + X ) - X ) )
65 2 recnd 
 |-  ( ph -> B e. CC )
66 65 49 pncand 
 |-  ( ph -> ( ( B + X ) - X ) = B )
67 62 64 66 3eqtrd 
 |-  ( ph -> ( Q ` M ) = B )
68 51 67 jca 
 |-  ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
69 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
70 69 15 sylan2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) e. RR )
71 14 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> V : ( 0 ... M ) --> RR )
72 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
73 72 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
74 71 73 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` ( i + 1 ) ) e. RR )
75 3 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. RR )
76 44 simprd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) )
77 76 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) < ( V ` ( i + 1 ) ) )
78 70 74 75 77 ltsub1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` i ) - X ) < ( ( V ` ( i + 1 ) ) - X ) )
79 69 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
80 69 17 sylan2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` i ) - X ) e. RR )
81 8 fvmpt2 
 |-  ( ( i e. ( 0 ... M ) /\ ( ( V ` i ) - X ) e. RR ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
82 79 80 81 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
83 fveq2 
 |-  ( i = j -> ( V ` i ) = ( V ` j ) )
84 83 oveq1d 
 |-  ( i = j -> ( ( V ` i ) - X ) = ( ( V ` j ) - X ) )
85 84 cbvmptv 
 |-  ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) ) = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) )
86 8 85 eqtri 
 |-  Q = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) )
87 86 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) ) )
88 fveq2 
 |-  ( j = ( i + 1 ) -> ( V ` j ) = ( V ` ( i + 1 ) ) )
89 88 oveq1d 
 |-  ( j = ( i + 1 ) -> ( ( V ` j ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
90 89 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( V ` j ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
91 74 75 resubcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` ( i + 1 ) ) - X ) e. RR )
92 87 90 73 91 fvmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
93 78 82 92 3brtr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
94 93 ralrimiva 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
95 24 68 94 jca32 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
96 5 fourierdlem2 
 |-  ( M e. NN -> ( Q e. ( O ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
97 6 96 syl 
 |-  ( ph -> ( Q e. ( O ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
98 95 97 mpbird 
 |-  ( ph -> Q e. ( O ` M ) )