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 0le0 
 |-  0 <_ 0
32 31 a1i 
 |-  ( ph -> 0 <_ 0 )
33 0red 
 |-  ( ph -> 0 e. RR )
34 6 nnred 
 |-  ( ph -> M e. RR )
35 6 nngt0d 
 |-  ( ph -> 0 < M )
36 33 34 35 ltled 
 |-  ( ph -> 0 <_ M )
37 29 30 29 32 36 elfzd 
 |-  ( ph -> 0 e. ( 0 ... M ) )
38 14 37 ffvelrnd 
 |-  ( ph -> ( V ` 0 ) e. RR )
39 38 3 resubcld 
 |-  ( ph -> ( ( V ` 0 ) - X ) e. RR )
40 25 28 37 39 fvmptd 
 |-  ( ph -> ( Q ` 0 ) = ( ( V ` 0 ) - X ) )
41 11 simprd 
 |-  ( ph -> ( ( ( V ` 0 ) = ( A + X ) /\ ( V ` M ) = ( B + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) )
42 41 simpld 
 |-  ( ph -> ( ( V ` 0 ) = ( A + X ) /\ ( V ` M ) = ( B + X ) ) )
43 42 simpld 
 |-  ( ph -> ( V ` 0 ) = ( A + X ) )
44 43 oveq1d 
 |-  ( ph -> ( ( V ` 0 ) - X ) = ( ( A + X ) - X ) )
45 1 recnd 
 |-  ( ph -> A e. CC )
46 3 recnd 
 |-  ( ph -> X e. CC )
47 45 46 pncand 
 |-  ( ph -> ( ( A + X ) - X ) = A )
48 40 44 47 3eqtrd 
 |-  ( ph -> ( Q ` 0 ) = A )
49 fveq2 
 |-  ( i = M -> ( V ` i ) = ( V ` M ) )
50 49 oveq1d 
 |-  ( i = M -> ( ( V ` i ) - X ) = ( ( V ` M ) - X ) )
51 50 adantl 
 |-  ( ( ph /\ i = M ) -> ( ( V ` i ) - X ) = ( ( V ` M ) - X ) )
52 34 leidd 
 |-  ( ph -> M <_ M )
53 29 30 30 36 52 elfzd 
 |-  ( ph -> M e. ( 0 ... M ) )
54 14 53 ffvelrnd 
 |-  ( ph -> ( V ` M ) e. RR )
55 54 3 resubcld 
 |-  ( ph -> ( ( V ` M ) - X ) e. RR )
56 25 51 53 55 fvmptd 
 |-  ( ph -> ( Q ` M ) = ( ( V ` M ) - X ) )
57 42 simprd 
 |-  ( ph -> ( V ` M ) = ( B + X ) )
58 57 oveq1d 
 |-  ( ph -> ( ( V ` M ) - X ) = ( ( B + X ) - X ) )
59 2 recnd 
 |-  ( ph -> B e. CC )
60 59 46 pncand 
 |-  ( ph -> ( ( B + X ) - X ) = B )
61 56 58 60 3eqtrd 
 |-  ( ph -> ( Q ` M ) = B )
62 48 61 jca 
 |-  ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
63 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
64 63 15 sylan2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) e. RR )
65 14 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> V : ( 0 ... M ) --> RR )
66 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
67 66 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
68 65 67 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` ( i + 1 ) ) e. RR )
69 3 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. RR )
70 41 simprd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) )
71 70 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) < ( V ` ( i + 1 ) ) )
72 64 68 69 71 ltsub1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` i ) - X ) < ( ( V ` ( i + 1 ) ) - X ) )
73 63 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
74 63 17 sylan2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` i ) - X ) e. RR )
75 8 fvmpt2 
 |-  ( ( i e. ( 0 ... M ) /\ ( ( V ` i ) - X ) e. RR ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
76 73 74 75 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
77 fveq2 
 |-  ( i = j -> ( V ` i ) = ( V ` j ) )
78 77 oveq1d 
 |-  ( i = j -> ( ( V ` i ) - X ) = ( ( V ` j ) - X ) )
79 78 cbvmptv 
 |-  ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) ) = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) )
80 8 79 eqtri 
 |-  Q = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) )
81 80 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) ) )
82 fveq2 
 |-  ( j = ( i + 1 ) -> ( V ` j ) = ( V ` ( i + 1 ) ) )
83 82 oveq1d 
 |-  ( j = ( i + 1 ) -> ( ( V ` j ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
84 83 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( V ` j ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
85 68 69 resubcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` ( i + 1 ) ) - X ) e. RR )
86 81 84 67 85 fvmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
87 72 76 86 3brtr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
88 87 ralrimiva 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
89 24 62 88 jca32 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
90 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 ) ) ) ) ) )
91 6 90 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 ) ) ) ) ) )
92 89 91 mpbird 
 |-  ( ph -> Q e. ( O ` M ) )