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