Metamath Proof Explorer

Theorem fourierdlem11

Description: If there is a partition, than the lower bound is strictly less than the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem11.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 ) ) ) } )
fourierdlem11.m 
|- ( ph -> M e. NN )
fourierdlem11.q 
|- ( ph -> Q e. ( P ` M ) )
Assertion fourierdlem11 
|- ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )

Proof

Step Hyp Ref Expression
1 fourierdlem11.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 fourierdlem11.m 
 |-  ( ph -> M e. NN )
3 fourierdlem11.q 
 |-  ( ph -> Q e. ( P ` M ) )
4 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 ) ) ) ) ) )
5 2 4 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 ) ) ) ) ) )
6 3 5 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
7 6 simprd 
 |-  ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
8 7 simpld 
 |-  ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
9 8 simpld 
 |-  ( ph -> ( Q ` 0 ) = A )
10 6 simpld 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
11 elmapi 
 |-  ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
12 10 11 syl 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
13 0red 
 |-  ( ph -> 0 e. RR )
14 13 leidd 
 |-  ( ph -> 0 <_ 0 )
15 2 nnred 
 |-  ( ph -> M e. RR )
16 2 nngt0d 
 |-  ( ph -> 0 < M )
17 13 15 16 ltled 
 |-  ( ph -> 0 <_ M )
18 0zd 
 |-  ( ph -> 0 e. ZZ )
19 2 nnzd 
 |-  ( ph -> M e. ZZ )
20 elfz 
 |-  ( ( 0 e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( 0 e. ( 0 ... M ) <-> ( 0 <_ 0 /\ 0 <_ M ) ) )
21 18 18 19 20 syl3anc 
 |-  ( ph -> ( 0 e. ( 0 ... M ) <-> ( 0 <_ 0 /\ 0 <_ M ) ) )
22 14 17 21 mpbir2and 
 |-  ( ph -> 0 e. ( 0 ... M ) )
23 12 22 ffvelrnd 
 |-  ( ph -> ( Q ` 0 ) e. RR )
24 9 23 eqeltrrd 
 |-  ( ph -> A e. RR )
25 8 simprd 
 |-  ( ph -> ( Q ` M ) = B )
26 15 leidd 
 |-  ( ph -> M <_ M )
27 elfz 
 |-  ( ( M e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( M e. ( 0 ... M ) <-> ( 0 <_ M /\ M <_ M ) ) )
28 19 18 19 27 syl3anc 
 |-  ( ph -> ( M e. ( 0 ... M ) <-> ( 0 <_ M /\ M <_ M ) ) )
29 17 26 28 mpbir2and 
 |-  ( ph -> M e. ( 0 ... M ) )
30 12 29 ffvelrnd 
 |-  ( ph -> ( Q ` M ) e. RR )
31 25 30 eqeltrrd 
 |-  ( ph -> B e. RR )
32 0le1 
 |-  0 <_ 1
33 32 a1i 
 |-  ( ph -> 0 <_ 1 )
34 2 nnge1d 
 |-  ( ph -> 1 <_ M )
35 1zzd 
 |-  ( ph -> 1 e. ZZ )
36 elfz 
 |-  ( ( 1 e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( 1 e. ( 0 ... M ) <-> ( 0 <_ 1 /\ 1 <_ M ) ) )
37 35 18 19 36 syl3anc 
 |-  ( ph -> ( 1 e. ( 0 ... M ) <-> ( 0 <_ 1 /\ 1 <_ M ) ) )
38 33 34 37 mpbir2and 
 |-  ( ph -> 1 e. ( 0 ... M ) )
39 12 38 ffvelrnd 
 |-  ( ph -> ( Q ` 1 ) e. RR )
40 elfzo 
 |-  ( ( 0 e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( 0 e. ( 0 ..^ M ) <-> ( 0 <_ 0 /\ 0 < M ) ) )
41 18 18 19 40 syl3anc 
 |-  ( ph -> ( 0 e. ( 0 ..^ M ) <-> ( 0 <_ 0 /\ 0 < M ) ) )
42 14 16 41 mpbir2and 
 |-  ( ph -> 0 e. ( 0 ..^ M ) )
43 0re 
 |-  0 e. RR
44 eleq1 
 |-  ( i = 0 -> ( i e. ( 0 ..^ M ) <-> 0 e. ( 0 ..^ M ) ) )
45 44 anbi2d 
 |-  ( i = 0 -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ 0 e. ( 0 ..^ M ) ) ) )
46 fveq2 
 |-  ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
47 oveq1 
 |-  ( i = 0 -> ( i + 1 ) = ( 0 + 1 ) )
48 47 fveq2d 
 |-  ( i = 0 -> ( Q ` ( i + 1 ) ) = ( Q ` ( 0 + 1 ) ) )
49 46 48 breq12d 
 |-  ( i = 0 -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
50 45 49 imbi12d 
 |-  ( i = 0 -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) ) )
51 7 simprd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
52 51 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
53 50 52 vtoclg 
 |-  ( 0 e. RR -> ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
54 43 53 ax-mp 
 |-  ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
55 42 54 mpdan 
 |-  ( ph -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
56 0p1e1 
 |-  ( 0 + 1 ) = 1
57 56 a1i 
 |-  ( ph -> ( 0 + 1 ) = 1 )
58 57 fveq2d 
 |-  ( ph -> ( Q ` ( 0 + 1 ) ) = ( Q ` 1 ) )
59 55 9 58 3brtr3d 
 |-  ( ph -> A < ( Q ` 1 ) )
60 nnuz 
 |-  NN = ( ZZ>= ` 1 )
61 2 60 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
62 12 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> Q : ( 0 ... M ) --> RR )
63 0red 
 |-  ( i e. ( 1 ... M ) -> 0 e. RR )
64 elfzelz 
 |-  ( i e. ( 1 ... M ) -> i e. ZZ )
65 64 zred 
 |-  ( i e. ( 1 ... M ) -> i e. RR )
66 1red 
 |-  ( i e. ( 1 ... M ) -> 1 e. RR )
67 0lt1 
 |-  0 < 1
68 67 a1i 
 |-  ( i e. ( 1 ... M ) -> 0 < 1 )
69 elfzle1 
 |-  ( i e. ( 1 ... M ) -> 1 <_ i )
70 63 66 65 68 69 ltletrd 
 |-  ( i e. ( 1 ... M ) -> 0 < i )
71 63 65 70 ltled 
 |-  ( i e. ( 1 ... M ) -> 0 <_ i )
72 elfzle2 
 |-  ( i e. ( 1 ... M ) -> i <_ M )
73 0zd 
 |-  ( i e. ( 1 ... M ) -> 0 e. ZZ )
74 elfzel2 
 |-  ( i e. ( 1 ... M ) -> M e. ZZ )
75 elfz 
 |-  ( ( i e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( i e. ( 0 ... M ) <-> ( 0 <_ i /\ i <_ M ) ) )
76 64 73 74 75 syl3anc 
 |-  ( i e. ( 1 ... M ) -> ( i e. ( 0 ... M ) <-> ( 0 <_ i /\ i <_ M ) ) )
77 71 72 76 mpbir2and 
 |-  ( i e. ( 1 ... M ) -> i e. ( 0 ... M ) )
78 77 adantl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> i e. ( 0 ... M ) )
79 62 78 ffvelrnd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( Q ` i ) e. RR )
80 12 adantr 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> Q : ( 0 ... M ) --> RR )
81 0red 
 |-  ( i e. ( 1 ... ( M - 1 ) ) -> 0 e. RR )
82 elfzelz 
 |-  ( i e. ( 1 ... ( M - 1 ) ) -> i e. ZZ )
83 82 zred 
 |-  ( i e. ( 1 ... ( M - 1 ) ) -> i e. RR )
84 1red 
 |-  ( i e. ( 1 ... ( M - 1 ) ) -> 1 e. RR )
85 67 a1i 
 |-  ( i e. ( 1 ... ( M - 1 ) ) -> 0 < 1 )
86 elfzle1 
 |-  ( i e. ( 1 ... ( M - 1 ) ) -> 1 <_ i )
87 81 84 83 85 86 ltletrd 
 |-  ( i e. ( 1 ... ( M - 1 ) ) -> 0 < i )
88 81 83 87 ltled 
 |-  ( i e. ( 1 ... ( M - 1 ) ) -> 0 <_ i )
89 88 adantl 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> 0 <_ i )
90 83 adantl 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> i e. RR )
91 15 adantr 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> M e. RR )
92 peano2rem 
 |-  ( M e. RR -> ( M - 1 ) e. RR )
93 91 92 syl 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( M - 1 ) e. RR )
94 elfzle2 
 |-  ( i e. ( 1 ... ( M - 1 ) ) -> i <_ ( M - 1 ) )
95 94 adantl 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> i <_ ( M - 1 ) )
96 91 ltm1d 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( M - 1 ) < M )
97 90 93 91 95 96 lelttrd 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> i < M )
98 90 91 97 ltled 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> i <_ M )
99 82 adantl 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> i e. ZZ )
100 0zd 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> 0 e. ZZ )
101 19 adantr 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> M e. ZZ )
102 99 100 101 75 syl3anc 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( i e. ( 0 ... M ) <-> ( 0 <_ i /\ i <_ M ) ) )
103 89 98 102 mpbir2and 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> i e. ( 0 ... M ) )
104 80 103 ffvelrnd 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( Q ` i ) e. RR )
105 0red 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> 0 e. RR )
106 peano2re 
 |-  ( i e. RR -> ( i + 1 ) e. RR )
107 90 106 syl 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( i + 1 ) e. RR )
108 1red 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> 1 e. RR )
109 67 a1i 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> 0 < 1 )
110 83 106 syl 
 |-  ( i e. ( 1 ... ( M - 1 ) ) -> ( i + 1 ) e. RR )
111 83 ltp1d 
 |-  ( i e. ( 1 ... ( M - 1 ) ) -> i < ( i + 1 ) )
112 84 83 110 86 111 lelttrd 
 |-  ( i e. ( 1 ... ( M - 1 ) ) -> 1 < ( i + 1 ) )
113 112 adantl 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> 1 < ( i + 1 ) )
114 105 108 107 109 113 lttrd 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> 0 < ( i + 1 ) )
115 105 107 114 ltled 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> 0 <_ ( i + 1 ) )
116 90 93 108 95 leadd1dd 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( i + 1 ) <_ ( ( M - 1 ) + 1 ) )
117 2 nncnd 
 |-  ( ph -> M e. CC )
118 1cnd 
 |-  ( ph -> 1 e. CC )
119 117 118 npcand 
 |-  ( ph -> ( ( M - 1 ) + 1 ) = M )
120 119 adantr 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( ( M - 1 ) + 1 ) = M )
121 116 120 breqtrd 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( i + 1 ) <_ M )
122 99 peano2zd 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( i + 1 ) e. ZZ )
123 elfz 
 |-  ( ( ( i + 1 ) e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( ( i + 1 ) e. ( 0 ... M ) <-> ( 0 <_ ( i + 1 ) /\ ( i + 1 ) <_ M ) ) )
124 122 100 101 123 syl3anc 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( ( i + 1 ) e. ( 0 ... M ) <-> ( 0 <_ ( i + 1 ) /\ ( i + 1 ) <_ M ) ) )
125 115 121 124 mpbir2and 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( i + 1 ) e. ( 0 ... M ) )
126 80 125 ffvelrnd 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
127 elfzo 
 |-  ( ( i e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( i e. ( 0 ..^ M ) <-> ( 0 <_ i /\ i < M ) ) )
128 99 100 101 127 syl3anc 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( i e. ( 0 ..^ M ) <-> ( 0 <_ i /\ i < M ) ) )
129 89 97 128 mpbir2and 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> i e. ( 0 ..^ M ) )
130 129 52 syldan 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
131 104 126 130 ltled 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( Q ` i ) <_ ( Q ` ( i + 1 ) ) )
132 61 79 131 monoord 
 |-  ( ph -> ( Q ` 1 ) <_ ( Q ` M ) )
133 132 25 breqtrd 
 |-  ( ph -> ( Q ` 1 ) <_ B )
134 24 39 31 59 133 ltletrd 
 |-  ( ph -> A < B )
135 24 31 134 3jca 
 |-  ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )