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