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 p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
fourierdlem15.2 φ M
fourierdlem15.3 φ Q P M
Assertion fourierdlem15 φ Q : 0 M A B

Proof

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