Metamath Proof Explorer

Theorem fourierdlem15

Description: The range of the partition is between its starting point and its ending point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem15.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 ) ) ) } )
fourierdlem15.2 
|- ( ph -> M e. NN )
fourierdlem15.3 
|- ( ph -> Q e. ( P ` M ) )
Assertion fourierdlem15 
|- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )

Proof

Step Hyp Ref Expression
1 fourierdlem15.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 fourierdlem15.2 
 |-  ( ph -> M e. NN )
3 fourierdlem15.3 
 |-  ( ph -> Q e. ( P ` M ) )
4 1 fourierdlem2 
 |-  ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
5 2 4 syl 
 |-  ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
6 3 5 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
7 6 simpld 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
8 reex 
 |-  RR e. _V
9 8 a1i 
 |-  ( ph -> RR e. _V )
10 ovex 
 |-  ( 0 ... M ) e. _V
11 10 a1i 
 |-  ( ph -> ( 0 ... M ) e. _V )
12 9 11 elmapd 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) <-> Q : ( 0 ... M ) --> RR ) )
13 7 12 mpbid 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
14 ffn 
 |-  ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
15 13 14 syl 
 |-  ( ph -> Q Fn ( 0 ... M ) )
16 6 simprd 
 |-  ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
17 16 simpld 
 |-  ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
18 17 simpld 
 |-  ( ph -> ( Q ` 0 ) = A )
19 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
20 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
21 19 20 eleqtrdi 
 |-  ( M e. NN -> M e. ( ZZ>= ` 0 ) )
22 2 21 syl 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
23 eluzfz1 
 |-  ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
24 22 23 syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
25 13 24 ffvelrnd 
 |-  ( ph -> ( Q ` 0 ) e. RR )
26 18 25 eqeltrrd 
 |-  ( ph -> A e. RR )
27 26 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> A e. RR )
28 17 simprd 
 |-  ( ph -> ( Q ` M ) = B )
29 eluzfz2 
 |-  ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
30 22 29 syl 
 |-  ( ph -> M e. ( 0 ... M ) )
31 13 30 ffvelrnd 
 |-  ( ph -> ( Q ` M ) e. RR )
32 28 31 eqeltrrd 
 |-  ( ph -> B e. RR )
33 32 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> B e. RR )
34 13 ffvelrnda 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
35 18 eqcomd 
 |-  ( ph -> A = ( Q ` 0 ) )
36 35 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> A = ( Q ` 0 ) )
37 elfzuz 
 |-  ( i e. ( 0 ... M ) -> i e. ( ZZ>= ` 0 ) )
38 37 adantl 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> i e. ( ZZ>= ` 0 ) )
39 13 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... i ) ) -> Q : ( 0 ... M ) --> RR )
40 elfzle1 
 |-  ( j e. ( 0 ... i ) -> 0 <_ j )
41 40 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> 0 <_ j )
42 elfzelz 
 |-  ( j e. ( 0 ... i ) -> j e. ZZ )
43 42 zred 
 |-  ( j e. ( 0 ... i ) -> j e. RR )
44 43 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j e. RR )
45 elfzelz 
 |-  ( i e. ( 0 ... M ) -> i e. ZZ )
46 45 zred 
 |-  ( i e. ( 0 ... M ) -> i e. RR )
47 46 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> i e. RR )
48 elfzel2 
 |-  ( i e. ( 0 ... M ) -> M e. ZZ )
49 48 zred 
 |-  ( i e. ( 0 ... M ) -> M e. RR )
50 49 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> M e. RR )
51 elfzle2 
 |-  ( j e. ( 0 ... i ) -> j <_ i )
52 51 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j <_ i )
53 elfzle2 
 |-  ( i e. ( 0 ... M ) -> i <_ M )
54 53 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> i <_ M )
55 44 47 50 52 54 letrd 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j <_ M )
56 42 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j e. ZZ )
57 0zd 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> 0 e. ZZ )
58 48 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> M e. ZZ )
59 elfz 
 |-  ( ( j e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( j e. ( 0 ... M ) <-> ( 0 <_ j /\ j <_ M ) ) )
60 56 57 58 59 syl3anc 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> ( j e. ( 0 ... M ) <-> ( 0 <_ j /\ j <_ M ) ) )
61 41 55 60 mpbir2and 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j e. ( 0 ... M ) )
62 61 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... i ) ) -> j e. ( 0 ... M ) )
63 39 62 ffvelrnd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... i ) ) -> ( Q ` j ) e. RR )
64 simpll 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ph )
65 elfzle1 
 |-  ( j e. ( 0 ... ( i - 1 ) ) -> 0 <_ j )
66 65 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> 0 <_ j )
67 elfzelz 
 |-  ( j e. ( 0 ... ( i - 1 ) ) -> j e. ZZ )
68 67 zred 
 |-  ( j e. ( 0 ... ( i - 1 ) ) -> j e. RR )
69 68 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. RR )
70 46 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> i e. RR )
71 49 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> M e. RR )
72 peano2rem 
 |-  ( i e. RR -> ( i - 1 ) e. RR )
73 70 72 syl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( i - 1 ) e. RR )
74 elfzle2 
 |-  ( j e. ( 0 ... ( i - 1 ) ) -> j <_ ( i - 1 ) )
75 74 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j <_ ( i - 1 ) )
76 70 ltm1d 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( i - 1 ) < i )
77 69 73 70 75 76 lelttrd 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j < i )
78 53 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> i <_ M )
79 69 70 71 77 78 ltletrd 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j < M )
80 67 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. ZZ )
81 0zd 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> 0 e. ZZ )
82 48 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> M e. ZZ )
83 elfzo 
 |-  ( ( j e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( j e. ( 0 ..^ M ) <-> ( 0 <_ j /\ j < M ) ) )
84 80 81 82 83 syl3anc 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( j e. ( 0 ..^ M ) <-> ( 0 <_ j /\ j < M ) ) )
85 66 79 84 mpbir2and 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. ( 0 ..^ M ) )
86 85 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. ( 0 ..^ M ) )
87 13 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
88 elfzofz 
 |-  ( j e. ( 0 ..^ M ) -> j e. ( 0 ... M ) )
89 88 adantl 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> j e. ( 0 ... M ) )
90 87 89 ffvelrnd 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` j ) e. RR )
91 fzofzp1 
 |-  ( j e. ( 0 ..^ M ) -> ( j + 1 ) e. ( 0 ... M ) )
92 91 adantl 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( j + 1 ) e. ( 0 ... M ) )
93 87 92 ffvelrnd 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` ( j + 1 ) ) e. RR )
94 eleq1w 
 |-  ( i = j -> ( i e. ( 0 ..^ M ) <-> j e. ( 0 ..^ M ) ) )
95 94 anbi2d 
 |-  ( i = j -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ j e. ( 0 ..^ M ) ) ) )
96 fveq2 
 |-  ( i = j -> ( Q ` i ) = ( Q ` j ) )
97 oveq1 
 |-  ( i = j -> ( i + 1 ) = ( j + 1 ) )
98 97 fveq2d 
 |-  ( i = j -> ( Q ` ( i + 1 ) ) = ( Q ` ( j + 1 ) ) )
99 96 98 breq12d 
 |-  ( i = j -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` j ) < ( Q ` ( j + 1 ) ) ) )
100 95 99 imbi12d 
 |-  ( i = j -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) ) ) )
101 16 simprd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
102 101 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
103 100 102 chvarvv 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) )
104 90 93 103 ltled 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` j ) <_ ( Q ` ( j + 1 ) ) )
105 64 86 104 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( Q ` j ) <_ ( Q ` ( j + 1 ) ) )
106 38 63 105 monoord 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` 0 ) <_ ( Q ` i ) )
107 36 106 eqbrtrd 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> A <_ ( Q ` i ) )
108 elfzuz3 
 |-  ( i e. ( 0 ... M ) -> M e. ( ZZ>= ` i ) )
109 108 adantl 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> M e. ( ZZ>= ` i ) )
110 13 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... M ) ) -> Q : ( 0 ... M ) --> RR )
111 fz0fzelfz0 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( i ... M ) ) -> j e. ( 0 ... M ) )
112 111 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... M ) ) -> j e. ( 0 ... M ) )
113 110 112 ffvelrnd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... M ) ) -> ( Q ` j ) e. RR )
114 13 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> Q : ( 0 ... M ) --> RR )
115 0red 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 e. RR )
116 46 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> i e. RR )
117 elfzelz 
 |-  ( j e. ( i ... ( M - 1 ) ) -> j e. ZZ )
118 117 zred 
 |-  ( j e. ( i ... ( M - 1 ) ) -> j e. RR )
119 118 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. RR )
120 elfzle1 
 |-  ( i e. ( 0 ... M ) -> 0 <_ i )
121 120 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ i )
122 elfzle1 
 |-  ( j e. ( i ... ( M - 1 ) ) -> i <_ j )
123 122 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> i <_ j )
124 115 116 119 121 123 letrd 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ j )
125 124 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ j )
126 118 adantl 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j e. RR )
127 2 nnred 
 |-  ( ph -> M e. RR )
128 127 adantr 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> M e. RR )
129 1red 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> 1 e. RR )
130 128 129 resubcld 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( M - 1 ) e. RR )
131 elfzle2 
 |-  ( j e. ( i ... ( M - 1 ) ) -> j <_ ( M - 1 ) )
132 131 adantl 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j <_ ( M - 1 ) )
133 128 ltm1d 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( M - 1 ) < M )
134 126 130 128 132 133 lelttrd 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j < M )
135 126 128 134 ltled 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j <_ M )
136 135 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j <_ M )
137 117 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. ZZ )
138 0zd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 e. ZZ )
139 48 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> M e. ZZ )
140 137 138 139 59 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j e. ( 0 ... M ) <-> ( 0 <_ j /\ j <_ M ) ) )
141 125 136 140 mpbir2and 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. ( 0 ... M ) )
142 114 141 ffvelrnd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` j ) e. RR )
143 118 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. RR )
144 1red 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 1 e. RR )
145 0le1 
 |-  0 <_ 1
146 145 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ 1 )
147 143 144 125 146 addge0d 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ ( j + 1 ) )
148 126 130 129 132 leadd1dd 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) <_ ( ( M - 1 ) + 1 ) )
149 2 nncnd 
 |-  ( ph -> M e. CC )
150 149 adantr 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> M e. CC )
151 1cnd 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> 1 e. CC )
152 150 151 npcand 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( ( M - 1 ) + 1 ) = M )
153 148 152 breqtrd 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) <_ M )
154 153 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) <_ M )
155 137 peano2zd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) e. ZZ )
156 elfz 
 |-  ( ( ( j + 1 ) e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( ( j + 1 ) e. ( 0 ... M ) <-> ( 0 <_ ( j + 1 ) /\ ( j + 1 ) <_ M ) ) )
157 155 138 139 156 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( ( j + 1 ) e. ( 0 ... M ) <-> ( 0 <_ ( j + 1 ) /\ ( j + 1 ) <_ M ) ) )
158 147 154 157 mpbir2and 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) e. ( 0 ... M ) )
159 114 158 ffvelrnd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` ( j + 1 ) ) e. RR )
160 simpll 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ph )
161 134 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j < M )
162 137 138 139 83 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j e. ( 0 ..^ M ) <-> ( 0 <_ j /\ j < M ) ) )
163 125 161 162 mpbir2and 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. ( 0 ..^ M ) )
164 160 163 103 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) )
165 142 159 164 ltled 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` j ) <_ ( Q ` ( j + 1 ) ) )
166 109 113 165 monoord 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) <_ ( Q ` M ) )
167 28 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` M ) = B )
168 166 167 breqtrd 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) <_ B )
169 27 33 34 107 168 eliccd 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. ( A [,] B ) )
170 169 ralrimiva 
 |-  ( ph -> A. i e. ( 0 ... M ) ( Q ` i ) e. ( A [,] B ) )
171 fnfvrnss 
 |-  ( ( Q Fn ( 0 ... M ) /\ A. i e. ( 0 ... M ) ( Q ` i ) e. ( A [,] B ) ) -> ran Q C_ ( A [,] B ) )
172 15 170 171 syl2anc 
 |-  ( ph -> ran Q C_ ( A [,] B ) )
173 df-f 
 |-  ( Q : ( 0 ... M ) --> ( A [,] B ) <-> ( Q Fn ( 0 ... M ) /\ ran Q C_ ( A [,] B ) ) )
174 15 172 173 sylanbrc 
 |-  ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )