Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itg2addnc Structured version   Visualization version   Unicode version

 Description: Alternate proof of itg2add 22796 using the "buffer zone" definition from the first lemma, in which every simple function in the set is divided into to by dividing its buffer by a third and finding the largest allowable function locked to a grid laid out in increments of the new, smaller buffer up to the original simple function. The measurability of this function follows from that of the augend, and subtracting it from the original simple function yields another simple function by i1fsub 22745, which is allowable by the fact that the grid must have a mark between one third and two thirds the original buffer. This has two advantages over the current approach: first, eliminating ax-cc 8883, and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017.) (Revised by Brendan Leahy, 13-Mar-2018.)
Hypotheses
Ref Expression
Assertion
Ref Expression

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprr 774 . . . . . . 7
2 itg1cl 22722 . . . . . . . 8
32adantr 472 . . . . . . 7
41, 3eqeltrd 2549 . . . . . 6
54rexlimiva 2868 . . . . 5
65abssi 3490 . . . 4
76a1i 11 . . 3
8 i1f0 22724 . . . . . 6
9 3nn 10791 . . . . . . . 8
10 nnrp 11334 . . . . . . . 8
11 ne0i 3728 . . . . . . . 8
129, 10, 11mp2b 10 . . . . . . 7
13 itg2addnc.f2 . . . . . . . . . . . . 13
1413ffvelrnda 6037 . . . . . . . . . . . 12
15 elrege0 11764 . . . . . . . . . . . 12
1614, 15sylib 201 . . . . . . . . . . 11
1716simprd 470 . . . . . . . . . 10
1817ralrimiva 2809 . . . . . . . . 9
19 reex 9648 . . . . . . . . . . 11
2019a1i 11 . . . . . . . . . 10
21 c0ex 9655 . . . . . . . . . . 11
2221a1i 11 . . . . . . . . . 10
23 eqidd 2472 . . . . . . . . . 10
2413feqmptd 5932 . . . . . . . . . 10
2520, 22, 14, 23, 24ofrfval2 6568 . . . . . . . . 9
2618, 25mpbird 240 . . . . . . . 8
2726ralrimivw 2810 . . . . . . 7
28 r19.2z 3849 . . . . . . 7
2912, 27, 28sylancr 676 . . . . . 6
30 fveq2 5879 . . . . . . . . . 10
31 itg10 22725 . . . . . . . . . 10
3230, 31syl6req 2522 . . . . . . . . 9
3332biantrud 515 . . . . . . . 8
34 fveq1 5878 . . . . . . . . . . . . 13
3521fvconst2 6136 . . . . . . . . . . . . 13
3634, 35sylan9eq 2525 . . . . . . . . . . . 12
3736iftrued 3880 . . . . . . . . . . 11
3837mpteq2dva 4482 . . . . . . . . . 10
3938breq1d 4405 . . . . . . . . 9
4039rexbidv 2892 . . . . . . . 8
4133, 40bitr3d 263 . . . . . . 7
4241rspcev 3136 . . . . . 6
438, 29, 42sylancr 676 . . . . 5
44 eqeq1 2475 . . . . . . . 8
4544anbi2d 718 . . . . . . 7
4645rexbidv 2892 . . . . . 6
4721, 46elab 3173 . . . . 5
4843, 47sylibr 217 . . . 4
49 ne0i 3728 . . . 4
5048, 49syl 17 . . 3
51 icossicc 11746 . . . . . . 7
52 fss 5749 . . . . . . 7
5351, 52mpan2 685 . . . . . 6
54 eqid 2471 . . . . . . 7
5554itg2addnclem 32057 . . . . . 6
5613, 53, 553syl 18 . . . . 5
57 itg2addnc.f3 . . . . 5
5856, 57eqeltrrd 2550 . . . 4
59 ressxr 9702 . . . . . . 7
606, 59sstri 3427 . . . . . 6
61 supxrub 11635 . . . . . 6
6260, 61mpan 684 . . . . 5
6362rgen 2766 . . . 4
64 breq2 4399 . . . . . 6
6564ralbidv 2829 . . . . 5
6665rspcev 3136 . . . 4
6758, 63, 66sylancl 675 . . 3
68 simprr 774 . . . . . . 7
69 itg1cl 22722 . . . . . . . 8
7069adantr 472 . . . . . . 7
7168, 70eqeltrd 2549 . . . . . 6
7271rexlimiva 2868 . . . . 5
7372abssi 3490 . . . 4
7473a1i 11 . . 3
75 itg2addnc.g2 . . . . . . . . . . . . 13
7675ffvelrnda 6037 . . . . . . . . . . . 12
77 elrege0 11764 . . . . . . . . . . . 12
7876, 77sylib 201 . . . . . . . . . . 11
7978simprd 470 . . . . . . . . . 10
8079ralrimiva 2809 . . . . . . . . 9
8175feqmptd 5932 . . . . . . . . . 10
8220, 22, 76, 23, 81ofrfval2 6568 . . . . . . . . 9
8380, 82mpbird 240 . . . . . . . 8
8483ralrimivw 2810 . . . . . . 7
85 r19.2z 3849 . . . . . . 7
8612, 84, 85sylancr 676 . . . . . 6
87 fveq2 5879 . . . . . . . . . 10
8887, 31syl6req 2522 . . . . . . . . 9
8988biantrud 515 . . . . . . . 8
90 fveq1 5878 . . . . . . . . . . . . 13
9190, 35sylan9eq 2525 . . . . . . . . . . . 12
9291iftrued 3880 . . . . . . . . . . 11
9392mpteq2dva 4482 . . . . . . . . . 10
9493breq1d 4405 . . . . . . . . 9
9594rexbidv 2892 . . . . . . . 8
9689, 95bitr3d 263 . . . . . . 7
9796rspcev 3136 . . . . . 6
988, 86, 97sylancr 676 . . . . 5
99 eqeq1 2475 . . . . . . . 8
10099anbi2d 718 . . . . . . 7
101100rexbidv 2892 . . . . . 6
10221, 101elab 3173 . . . . 5
10398, 102sylibr 217 . . . 4
104 ne0i 3728 . . . 4
105103, 104syl 17 . . 3
106 fss 5749 . . . . . . 7
10751, 106mpan2 685 . . . . . 6
108 eqid 2471 . . . . . . 7
109108itg2addnclem 32057 . . . . . 6
11075, 107, 1093syl 18 . . . . 5
111 itg2addnc.g3 . . . . 5
112110, 111eqeltrrd 2550 . . . 4
11373, 59sstri 3427 . . . . . 6
114 supxrub 11635 . . . . . 6
115113, 114mpan 684 . . . . 5
116115rgen 2766 . . . 4
117 breq2 4399 . . . . . 6
118117ralbidv 2829 . . . . 5
119118rspcev 3136 . . . 4
120112, 116, 119sylancl 675 . . 3
121 eqid 2471 . . 3
1227, 50, 67, 74, 105, 120, 121supadd 10597 . 2
123 supxrre 11638 . . . . 5
1247, 50, 67, 123syl3anc 1292 . . . 4
12556, 124eqtrd 2505 . . 3
126 supxrre 11638 . . . . 5
12774, 105, 120, 126syl3anc 1292 . . . 4
128110, 127eqtrd 2505 . . 3
129125, 128oveq12d 6326 . 2
130 ge0addcl 11770 . . . . . . 7
13151, 130sseldi 3416 . . . . . 6
132131adantl 473 . . . . 5
133 inidm 3632 . . . . 5
134132, 13, 75, 20, 20, 133off 6565 . . . 4
135 eqid 2471 . . . . 5
136135itg2addnclem 32057 . . . 4
137134, 136syl 17 . . 3
138 itg2addnc.f1 . . . . . . . 8 MblFn
139138, 13, 57, 75, 111itg2addnclem3 32059 . . . . . . 7
140 simpl 464 . . . . . . . . . . . . . 14
141 simpr 468 . . . . . . . . . . . . . 14
142140, 141i1fadd 22732 . . . . . . . . . . . . 13
143142ad3antlr 745 . . . . . . . . . . . 12
144 reeanv 2944 . . . . . . . . . . . . . . . . 17
145144biimpri 211 . . . . . . . . . . . . . . . 16
146145ad2ant2r 761 . . . . . . . . . . . . . . 15
147 ifcl 3914 . . . . . . . . . . . . . . . . . . 19
148147ad2antlr 741 . . . . . . . . . . . . . . . . . 18
149 breq1 4398 . . . . . . . . . . . . . . . . . . . . . . . 24
150149anbi1d 719 . . . . . . . . . . . . . . . . . . . . . . 23
151150imbi1d 324 . . . . . . . . . . . . . . . . . . . . . 22
152 breq1 4398 . . . . . . . . . . . . . . . . . . . . . . . 24
153152anbi1d 719 . . . . . . . . . . . . . . . . . . . . . . 23
154153imbi1d 324 . . . . . . . . . . . . . . . . . . . . . 22
155 breq1 4398 . . . . . . . . . . . . . . . . . . . . . . . . 25
156155anbi2d 718 . . . . . . . . . . . . . . . . . . . . . . . 24
157156imbi1d 324 . . . . . . . . . . . . . . . . . . . . . . 23
158 breq1 4398 . . . . . . . . . . . . . . . . . . . . . . . . 25
159158anbi2d 718 . . . . . . . . . . . . . . . . . . . . . . . 24
160159imbi1d 324 . . . . . . . . . . . . . . . . . . . . . . 23
161 oveq12 6317 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
162 00id 9826 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
163161, 162syl6eq 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
164163iftrued 3880 . . . . . . . . . . . . . . . . . . . . . . . . . 26
165164adantll 728 . . . . . . . . . . . . . . . . . . . . . . . . 25
166 simpll 768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
16715simplbi 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
16814, 167syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
16977simplbi 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
17076, 169syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
171168, 170, 17, 79addge0d 10210 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
172166, 171sylan 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26
173172ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . 25
174165, 173eqbrtrd 4416 . . . . . . . . . . . . . . . . . . . . . . . 24
175174a1d 25 . . . . . . . . . . . . . . . . . . . . . . 23
176172ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
177 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
178 simplrr 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
179 i1ff 22713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
180179ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
181178, 180sylan 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
182181recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
183182addid2d 9852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
184177, 183sylan9eqr 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
185184oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
186185adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
187147rpred 11364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
188187ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
189181, 188readdcld 9688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
190189adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
191166, 170sylan 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
192191adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
193166, 168sylan 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
194193, 191readdcld 9688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
195194adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
196 simplrr 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
197196rpred 11364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
198 rpre 11331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
199 rpre 11331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
200 min2 11507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
201198, 199, 200syl2an 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
202201ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
203188, 197, 181, 202leadd2dd 10249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
204181, 197readdcld 9688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
205 letr 9745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
206189, 204, 191, 205syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
207203, 206mpand 689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
208207imp 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
209170, 168addge02d 10223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
21017, 209mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211166, 210sylan 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212211adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
213190, 192, 195, 208, 212letrd 9809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
214213adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
215186, 214eqbrtrd 4416 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
216 breq1 4398 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
217 breq1 4398 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
218216, 217ifboth 3908 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
219176, 215, 218syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . 26
220219ex 441 . . . . . . . . . . . . . . . . . . . . . . . . 25
221220adantld 474 . . . . . . . . . . . . . . . . . . . . . . . 24
222221adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
223157, 160, 175, 222ifbothda 3907 . . . . . . . . . . . . . . . . . . . . . 22
224155anbi2d 718 . . . . . . . . . . . . . . . . . . . . . . . 24
225224imbi1d 324 . . . . . . . . . . . . . . . . . . . . . . 23
226158anbi2d 718 . . . . . . . . . . . . . . . . . . . . . . . 24