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