Metamath Proof Explorer

Theorem fourierdlem12

Description: A point of a partition is not an element of any open interval determined by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem12.1 
|- 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 ) ) ) } )
fourierdlem12.2 
|- ( ph -> M e. NN )
fourierdlem12.3 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem12.4 
|- ( ph -> X e. ran Q )
Assertion fourierdlem12 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> -. X e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem12.1 
 |-  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 fourierdlem12.2 
 |-  ( ph -> M e. NN )
3 fourierdlem12.3 
 |-  ( ph -> Q e. ( P ` M ) )
4 fourierdlem12.4 
 |-  ( ph -> X e. ran Q )
5 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 ) ) ) ) ) )
6 2 5 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 ) ) ) ) ) )
7 3 6 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
8 7 simpld 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
9 elmapi 
 |-  ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
10 ffn 
 |-  ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
11 fvelrnb 
 |-  ( Q Fn ( 0 ... M ) -> ( X e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = X ) )
12 8 9 10 11 4syl 
 |-  ( ph -> ( X e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = X ) )
13 4 12 mpbid 
 |-  ( ph -> E. j e. ( 0 ... M ) ( Q ` j ) = X )
14 13 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> E. j e. ( 0 ... M ) ( Q ` j ) = X )
15 8 9 syl 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
16 15 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
17 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
18 17 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
19 16 18 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
20 19 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ i < j ) -> ( Q ` ( i + 1 ) ) e. RR )
21 20 3ad2antl1 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> ( Q ` ( i + 1 ) ) e. RR )
22 frn 
 |-  ( Q : ( 0 ... M ) --> RR -> ran Q C_ RR )
23 15 22 syl 
 |-  ( ph -> ran Q C_ RR )
24 23 4 sseldd 
 |-  ( ph -> X e. RR )
25 24 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ i < j ) -> X e. RR )
26 25 3ad2antl1 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> X e. RR )
27 16 ffvelcdmda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR )
28 27 3adant3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> ( Q ` j ) e. RR )
29 28 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> ( Q ` j ) e. RR )
30 simpr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> i < j )
31 elfzoelz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ZZ )
32 31 ad2antrr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> i e. ZZ )
33 elfzelz 
 |-  ( j e. ( 0 ... M ) -> j e. ZZ )
34 33 ad2antlr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> j e. ZZ )
35 zltp1le 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> ( i < j <-> ( i + 1 ) <_ j ) )
36 32 34 35 syl2anc 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> ( i < j <-> ( i + 1 ) <_ j ) )
37 30 36 mpbid 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> ( i + 1 ) <_ j )
38 32 peano2zd 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> ( i + 1 ) e. ZZ )
39 eluz 
 |-  ( ( ( i + 1 ) e. ZZ /\ j e. ZZ ) -> ( j e. ( ZZ>= ` ( i + 1 ) ) <-> ( i + 1 ) <_ j ) )
40 38 34 39 syl2anc 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> ( j e. ( ZZ>= ` ( i + 1 ) ) <-> ( i + 1 ) <_ j ) )
41 37 40 mpbird 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> j e. ( ZZ>= ` ( i + 1 ) ) )
42 41 adantlll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> j e. ( ZZ>= ` ( i + 1 ) ) )
43 16 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> Q : ( 0 ... M ) --> RR )
44 0zd 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> 0 e. ZZ )
45 elfzel2 
 |-  ( j e. ( 0 ... M ) -> M e. ZZ )
46 45 ad2antlr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> M e. ZZ )
47 elfzelz 
 |-  ( w e. ( ( i + 1 ) ... j ) -> w e. ZZ )
48 47 adantl 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> w e. ZZ )
49 0red 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> 0 e. RR )
50 47 zred 
 |-  ( w e. ( ( i + 1 ) ... j ) -> w e. RR )
51 50 adantl 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> w e. RR )
52 31 peano2zd 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ZZ )
53 52 zred 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. RR )
54 53 adantr 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> ( i + 1 ) e. RR )
55 31 zred 
 |-  ( i e. ( 0 ..^ M ) -> i e. RR )
56 55 adantr 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> i e. RR )
57 elfzole1 
 |-  ( i e. ( 0 ..^ M ) -> 0 <_ i )
58 57 adantr 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> 0 <_ i )
59 56 ltp1d 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> i < ( i + 1 ) )
60 49 56 54 58 59 lelttrd 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> 0 < ( i + 1 ) )
61 elfzle1 
 |-  ( w e. ( ( i + 1 ) ... j ) -> ( i + 1 ) <_ w )
62 61 adantl 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> ( i + 1 ) <_ w )
63 49 54 51 60 62 ltletrd 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> 0 < w )
64 49 51 63 ltled 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> 0 <_ w )
65 64 adantlr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> 0 <_ w )
66 50 adantl 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... j ) ) -> w e. RR )
67 33 zred 
 |-  ( j e. ( 0 ... M ) -> j e. RR )
68 67 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... j ) ) -> j e. RR )
69 45 zred 
 |-  ( j e. ( 0 ... M ) -> M e. RR )
70 69 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... j ) ) -> M e. RR )
71 elfzle2 
 |-  ( w e. ( ( i + 1 ) ... j ) -> w <_ j )
72 71 adantl 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... j ) ) -> w <_ j )
73 elfzle2 
 |-  ( j e. ( 0 ... M ) -> j <_ M )
74 73 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... j ) ) -> j <_ M )
75 66 68 70 72 74 letrd 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... j ) ) -> w <_ M )
76 75 adantll 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> w <_ M )
77 44 46 48 65 76 elfzd 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> w e. ( 0 ... M ) )
78 77 adantlll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> w e. ( 0 ... M ) )
79 43 78 ffvelcdmd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> ( Q ` w ) e. RR )
80 79 adantlr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... j ) ) -> ( Q ` w ) e. RR )
81 simp-4l 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> ph )
82 0red 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 e. RR )
83 elfzelz 
 |-  ( w e. ( ( i + 1 ) ... ( j - 1 ) ) -> w e. ZZ )
84 83 zred 
 |-  ( w e. ( ( i + 1 ) ... ( j - 1 ) ) -> w e. RR )
85 84 adantl 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w e. RR )
86 0red 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 e. RR )
87 53 adantr 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> ( i + 1 ) e. RR )
88 84 adantl 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w e. RR )
89 0red 
 |-  ( i e. ( 0 ..^ M ) -> 0 e. RR )
90 55 ltp1d 
 |-  ( i e. ( 0 ..^ M ) -> i < ( i + 1 ) )
91 89 55 53 57 90 lelttrd 
 |-  ( i e. ( 0 ..^ M ) -> 0 < ( i + 1 ) )
92 91 adantr 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 < ( i + 1 ) )
93 elfzle1 
 |-  ( w e. ( ( i + 1 ) ... ( j - 1 ) ) -> ( i + 1 ) <_ w )
94 93 adantl 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> ( i + 1 ) <_ w )
95 86 87 88 92 94 ltletrd 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 < w )
96 95 adantlr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 < w )
97 82 85 96 ltled 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 <_ w )
98 97 adantlll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 <_ w )
99 98 adantlr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 <_ w )
100 84 adantl 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w e. RR )
101 peano2rem 
 |-  ( j e. RR -> ( j - 1 ) e. RR )
102 67 101 syl 
 |-  ( j e. ( 0 ... M ) -> ( j - 1 ) e. RR )
103 102 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> ( j - 1 ) e. RR )
104 69 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> M e. RR )
105 elfzle2 
 |-  ( w e. ( ( i + 1 ) ... ( j - 1 ) ) -> w <_ ( j - 1 ) )
106 105 adantl 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w <_ ( j - 1 ) )
107 zlem1lt 
 |-  ( ( j e. ZZ /\ M e. ZZ ) -> ( j <_ M <-> ( j - 1 ) < M ) )
108 33 45 107 syl2anc 
 |-  ( j e. ( 0 ... M ) -> ( j <_ M <-> ( j - 1 ) < M ) )
109 73 108 mpbid 
 |-  ( j e. ( 0 ... M ) -> ( j - 1 ) < M )
110 109 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> ( j - 1 ) < M )
111 100 103 104 106 110 lelttrd 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w < M )
112 111 adantlr 
 |-  ( ( ( j e. ( 0 ... M ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w < M )
113 112 adantlll 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w < M )
114 83 adantl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w e. ZZ )
115 0zd 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 e. ZZ )
116 45 ad3antlr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> M e. ZZ )
117 elfzo 
 |-  ( ( w e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( w e. ( 0 ..^ M ) <-> ( 0 <_ w /\ w < M ) ) )
118 114 115 116 117 syl3anc 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> ( w e. ( 0 ..^ M ) <-> ( 0 <_ w /\ w < M ) ) )
119 99 113 118 mpbir2and 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w e. ( 0 ..^ M ) )
120 15 adantr 
 |-  ( ( ph /\ w e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
121 elfzofz 
 |-  ( w e. ( 0 ..^ M ) -> w e. ( 0 ... M ) )
122 121 adantl 
 |-  ( ( ph /\ w e. ( 0 ..^ M ) ) -> w e. ( 0 ... M ) )
123 120 122 ffvelcdmd 
 |-  ( ( ph /\ w e. ( 0 ..^ M ) ) -> ( Q ` w ) e. RR )
124 fzofzp1 
 |-  ( w e. ( 0 ..^ M ) -> ( w + 1 ) e. ( 0 ... M ) )
125 124 adantl 
 |-  ( ( ph /\ w e. ( 0 ..^ M ) ) -> ( w + 1 ) e. ( 0 ... M ) )
126 120 125 ffvelcdmd 
 |-  ( ( ph /\ w e. ( 0 ..^ M ) ) -> ( Q ` ( w + 1 ) ) e. RR )
127 eleq1w 
 |-  ( i = w -> ( i e. ( 0 ..^ M ) <-> w e. ( 0 ..^ M ) ) )
128 127 anbi2d 
 |-  ( i = w -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ w e. ( 0 ..^ M ) ) ) )
129 fveq2 
 |-  ( i = w -> ( Q ` i ) = ( Q ` w ) )
130 oveq1 
 |-  ( i = w -> ( i + 1 ) = ( w + 1 ) )
131 130 fveq2d 
 |-  ( i = w -> ( Q ` ( i + 1 ) ) = ( Q ` ( w + 1 ) ) )
132 129 131 breq12d 
 |-  ( i = w -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` w ) < ( Q ` ( w + 1 ) ) ) )
133 128 132 imbi12d 
 |-  ( i = w -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ w e. ( 0 ..^ M ) ) -> ( Q ` w ) < ( Q ` ( w + 1 ) ) ) ) )
134 7 simprrd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
135 134 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
136 133 135 chvarvv 
 |-  ( ( ph /\ w e. ( 0 ..^ M ) ) -> ( Q ` w ) < ( Q ` ( w + 1 ) ) )
137 123 126 136 ltled 
 |-  ( ( ph /\ w e. ( 0 ..^ M ) ) -> ( Q ` w ) <_ ( Q ` ( w + 1 ) ) )
138 81 119 137 syl2anc 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> ( Q ` w ) <_ ( Q ` ( w + 1 ) ) )
139 42 80 138 monoord 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> ( Q ` ( i + 1 ) ) <_ ( Q ` j ) )
140 139 3adantl3 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> ( Q ` ( i + 1 ) ) <_ ( Q ` j ) )
141 15 ffvelcdmda 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR )
142 141 3adant3 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> ( Q ` j ) e. RR )
143 simp3 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> ( Q ` j ) = X )
144 142 143 eqled 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> ( Q ` j ) <_ X )
145 144 3adant1r 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> ( Q ` j ) <_ X )
146 145 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> ( Q ` j ) <_ X )
147 21 29 26 140 146 letrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> ( Q ` ( i + 1 ) ) <_ X )
148 21 26 147 lensymd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> -. X < ( Q ` ( i + 1 ) ) )
149 148 intnand 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> -. ( ( Q ` i ) < X /\ X < ( Q ` ( i + 1 ) ) ) )
150 67 ad2antlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ -. i < j ) -> j e. RR )
151 55 ad3antlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ -. i < j ) -> i e. RR )
152 simpr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ -. i < j ) -> -. i < j )
153 150 151 152 nltled 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ -. i < j ) -> j <_ i )
154 153 3adantl3 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ -. i < j ) -> j <_ i )
155 eqcom 
 |-  ( ( Q ` j ) = X <-> X = ( Q ` j ) )
156 155 biimpi 
 |-  ( ( Q ` j ) = X -> X = ( Q ` j ) )
157 156 adantr 
 |-  ( ( ( Q ` j ) = X /\ j <_ i ) -> X = ( Q ` j ) )
158 157 3ad2antl3 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ j <_ i ) -> X = ( Q ` j ) )
159 33 ad2antlr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) -> j e. ZZ )
160 31 ad2antrr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) -> i e. ZZ )
161 simpr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) -> j <_ i )
162 eluz2 
 |-  ( i e. ( ZZ>= ` j ) <-> ( j e. ZZ /\ i e. ZZ /\ j <_ i ) )
163 159 160 161 162 syl3anbrc 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) -> i e. ( ZZ>= ` j ) )
164 163 adantlll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) -> i e. ( ZZ>= ` j ) )
165 16 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> Q : ( 0 ... M ) --> RR )
166 0zd 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> 0 e. ZZ )
167 45 ad2antlr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> M e. ZZ )
168 elfzelz 
 |-  ( w e. ( j ... i ) -> w e. ZZ )
169 168 adantl 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> w e. ZZ )
170 166 167 169 3jca 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> ( 0 e. ZZ /\ M e. ZZ /\ w e. ZZ ) )
171 0red 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( j ... i ) ) -> 0 e. RR )
172 67 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( j ... i ) ) -> j e. RR )
173 168 zred 
 |-  ( w e. ( j ... i ) -> w e. RR )
174 173 adantl 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( j ... i ) ) -> w e. RR )
175 elfzle1 
 |-  ( j e. ( 0 ... M ) -> 0 <_ j )
176 175 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( j ... i ) ) -> 0 <_ j )
177 elfzle1 
 |-  ( w e. ( j ... i ) -> j <_ w )
178 177 adantl 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( j ... i ) ) -> j <_ w )
179 171 172 174 176 178 letrd 
 |-  ( ( j e. ( 0 ... M ) /\ w e. ( j ... i ) ) -> 0 <_ w )
180 179 adantll 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> 0 <_ w )
181 173 adantl 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... i ) ) -> w e. RR )
182 elfzoel2 
 |-  ( i e. ( 0 ..^ M ) -> M e. ZZ )
183 182 zred 
 |-  ( i e. ( 0 ..^ M ) -> M e. RR )
184 183 adantr 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... i ) ) -> M e. RR )
185 55 adantr 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... i ) ) -> i e. RR )
186 elfzle2 
 |-  ( w e. ( j ... i ) -> w <_ i )
187 186 adantl 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... i ) ) -> w <_ i )
188 elfzolt2 
 |-  ( i e. ( 0 ..^ M ) -> i < M )
189 188 adantr 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... i ) ) -> i < M )
190 181 185 184 187 189 lelttrd 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... i ) ) -> w < M )
191 181 184 190 ltled 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... i ) ) -> w <_ M )
192 191 adantlr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> w <_ M )
193 170 180 192 jca32 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> ( ( 0 e. ZZ /\ M e. ZZ /\ w e. ZZ ) /\ ( 0 <_ w /\ w <_ M ) ) )
194 193 adantlll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> ( ( 0 e. ZZ /\ M e. ZZ /\ w e. ZZ ) /\ ( 0 <_ w /\ w <_ M ) ) )
195 elfz2 
 |-  ( w e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ w e. ZZ ) /\ ( 0 <_ w /\ w <_ M ) ) )
196 194 195 sylibr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> w e. ( 0 ... M ) )
197 165 196 ffvelcdmd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> ( Q ` w ) e. RR )
198 197 adantlr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) /\ w e. ( j ... i ) ) -> ( Q ` w ) e. RR )
199 simplll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> ph )
200 0red 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> 0 e. RR )
201 67 ad2antlr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> j e. RR )
202 elfzelz 
 |-  ( w e. ( j ... ( i - 1 ) ) -> w e. ZZ )
203 202 zred 
 |-  ( w e. ( j ... ( i - 1 ) ) -> w e. RR )
204 203 adantl 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> w e. RR )
205 175 ad2antlr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> 0 <_ j )
206 elfzle1 
 |-  ( w e. ( j ... ( i - 1 ) ) -> j <_ w )
207 206 adantl 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> j <_ w )
208 200 201 204 205 207 letrd 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> 0 <_ w )
209 203 adantl 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> w e. RR )
210 55 adantr 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> i e. RR )
211 183 adantr 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> M e. RR )
212 peano2rem 
 |-  ( i e. RR -> ( i - 1 ) e. RR )
213 210 212 syl 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> ( i - 1 ) e. RR )
214 elfzle2 
 |-  ( w e. ( j ... ( i - 1 ) ) -> w <_ ( i - 1 ) )
215 214 adantl 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> w <_ ( i - 1 ) )
216 210 ltm1d 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> ( i - 1 ) < i )
217 209 213 210 215 216 lelttrd 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> w < i )
218 188 adantr 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> i < M )
219 209 210 211 217 218 lttrd 
 |-  ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> w < M )
220 219 adantlr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> w < M )
221 202 adantl 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> w e. ZZ )
222 0zd 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> 0 e. ZZ )
223 182 ad2antrr 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> M e. ZZ )
224 221 222 223 117 syl3anc 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> ( w e. ( 0 ..^ M ) <-> ( 0 <_ w /\ w < M ) ) )
225 208 220 224 mpbir2and 
 |-  ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> w e. ( 0 ..^ M ) )
226 225 adantlll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> w e. ( 0 ..^ M ) )
227 199 226 137 syl2anc 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> ( Q ` w ) <_ ( Q ` ( w + 1 ) ) )
228 227 adantlr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) /\ w e. ( j ... ( i - 1 ) ) ) -> ( Q ` w ) <_ ( Q ` ( w + 1 ) ) )
229 164 198 228 monoord 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) -> ( Q ` j ) <_ ( Q ` i ) )
230 229 3adantl3 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ j <_ i ) -> ( Q ` j ) <_ ( Q ` i ) )
231 158 230 eqbrtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ j <_ i ) -> X <_ ( Q ` i ) )
232 24 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. RR )
233 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
234 233 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
235 16 234 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
236 232 235 lenltd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X <_ ( Q ` i ) <-> -. ( Q ` i ) < X ) )
237 236 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j <_ i ) -> ( X <_ ( Q ` i ) <-> -. ( Q ` i ) < X ) )
238 237 3ad2antl1 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ j <_ i ) -> ( X <_ ( Q ` i ) <-> -. ( Q ` i ) < X ) )
239 231 238 mpbid 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ j <_ i ) -> -. ( Q ` i ) < X )
240 154 239 syldan 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ -. i < j ) -> -. ( Q ` i ) < X )
241 240 intnanrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ -. i < j ) -> -. ( ( Q ` i ) < X /\ X < ( Q ` ( i + 1 ) ) ) )
242 149 241 pm2.61dan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> -. ( ( Q ` i ) < X /\ X < ( Q ` ( i + 1 ) ) ) )
243 242 intnand 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> -. ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( Q ` i ) < X /\ X < ( Q ` ( i + 1 ) ) ) ) )
244 elioo3g 
 |-  ( X e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( Q ` i ) < X /\ X < ( Q ` ( i + 1 ) ) ) ) )
245 243 244 sylnibr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> -. X e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
246 245 rexlimdv3a 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( E. j e. ( 0 ... M ) ( Q ` j ) = X -> -. X e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
247 14 246 mpd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -. X e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )