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 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 ffvelrnd
 |-  ( ( ( ( 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 ffvelrnd
 |-  ( ( 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 ffvelrnd
 |-  ( ( 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 ffvelrnda
 |-  ( ( 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 ffvelrnd
 |-  ( ( ( ( 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 ffvelrnd
 |-  ( ( 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 ) ) ) )