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

 Description: Alternate proof of itg2add 19641 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 19590, 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 8305, 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 734 . . . . . . 7
2 itg1cl 19567 . . . . . . . 8
32adantr 452 . . . . . . 7
41, 3eqeltrd 2509 . . . . . 6
54rexlimiva 2817 . . . . 5
65abssi 3410 . . . 4
76a1i 11 . . 3
8 i1f0 19569 . . . . . 6
9 3nn 10124 . . . . . . . 8
10 nnrp 10611 . . . . . . . 8
11 ne0i 3626 . . . . . . . 8
129, 10, 11mp2b 10 . . . . . . 7
13 itg2addnc.f2 . . . . . . . . . . . . 13
1413ffvelrnda 5862 . . . . . . . . . . . 12
15 elrege0 10997 . . . . . . . . . . . 12
1614, 15sylib 189 . . . . . . . . . . 11
1716simprd 450 . . . . . . . . . 10
1817ralrimiva 2781 . . . . . . . . 9
19 reex 9071 . . . . . . . . . . 11
2019a1i 11 . . . . . . . . . 10
21 c0ex 9075 . . . . . . . . . . 11
2221a1i 11 . . . . . . . . . 10
23 eqidd 2436 . . . . . . . . . 10
2413feqmptd 5771 . . . . . . . . . 10
2520, 22, 14, 23, 24ofrfval2 6315 . . . . . . . . 9
2618, 25mpbird 224 . . . . . . . 8
2726ralrimivw 2782 . . . . . . 7
28 r19.2z 3709 . . . . . . 7
2912, 27, 28sylancr 645 . . . . . 6
30 fveq2 5720 . . . . . . . . . 10
31 itg10 19570 . . . . . . . . . 10
3230, 31syl6req 2484 . . . . . . . . 9
3332biantrud 494 . . . . . . . 8
34 fveq1 5719 . . . . . . . . . . . . 13
3521fvconst2 5939 . . . . . . . . . . . . 13
3634, 35sylan9eq 2487 . . . . . . . . . . . 12
37 iftrue 3737 . . . . . . . . . . . 12
3836, 37syl 16 . . . . . . . . . . 11
3938mpteq2dva 4287 . . . . . . . . . 10
4039breq1d 4214 . . . . . . . . 9
4140rexbidv 2718 . . . . . . . 8
4233, 41bitr3d 247 . . . . . . 7
4342rspcev 3044 . . . . . 6
448, 29, 43sylancr 645 . . . . 5
45 eqeq1 2441 . . . . . . . 8
4645anbi2d 685 . . . . . . 7
4746rexbidv 2718 . . . . . 6
4821, 47elab 3074 . . . . 5
4944, 48sylibr 204 . . . 4
50 ne0i 3626 . . . 4
5149, 50syl 16 . . 3
52 icossicc 24119 . . . . . . 7
53 fss 5591 . . . . . . 7
5452, 53mpan2 653 . . . . . 6
55 eqid 2435 . . . . . . 7
5655itg2addnclem 26219 . . . . . 6
5713, 54, 563syl 19 . . . . 5
58 itg2addnc.f3 . . . . 5
5957, 58eqeltrrd 2510 . . . 4
60 ressxr 9119 . . . . . . 7
616, 60sstri 3349 . . . . . 6
62 supxrub 10893 . . . . . 6
6361, 62mpan 652 . . . . 5
6463rgen 2763 . . . 4
65 breq2 4208 . . . . . 6
6665ralbidv 2717 . . . . 5
6766rspcev 3044 . . . 4
6859, 64, 67sylancl 644 . . 3
69 simprr 734 . . . . . . 7
70 itg1cl 19567 . . . . . . . 8
7170adantr 452 . . . . . . 7
7269, 71eqeltrd 2509 . . . . . 6
7372rexlimiva 2817 . . . . 5
7473abssi 3410 . . . 4
7574a1i 11 . . 3
76 itg2addnc.g2 . . . . . . . . . . . . 13
7776ffvelrnda 5862 . . . . . . . . . . . 12
78 elrege0 10997 . . . . . . . . . . . 12
7977, 78sylib 189 . . . . . . . . . . 11
8079simprd 450 . . . . . . . . . 10
8180ralrimiva 2781 . . . . . . . . 9
8276feqmptd 5771 . . . . . . . . . 10
8320, 22, 77, 23, 82ofrfval2 6315 . . . . . . . . 9
8481, 83mpbird 224 . . . . . . . 8
8584ralrimivw 2782 . . . . . . 7
86 r19.2z 3709 . . . . . . 7
8712, 85, 86sylancr 645 . . . . . 6
88 fveq2 5720 . . . . . . . . . 10
8988, 31syl6req 2484 . . . . . . . . 9
9089biantrud 494 . . . . . . . 8
91 fveq1 5719 . . . . . . . . . . . . 13
9291, 35sylan9eq 2487 . . . . . . . . . . . 12
93 iftrue 3737 . . . . . . . . . . . 12
9492, 93syl 16 . . . . . . . . . . 11
9594mpteq2dva 4287 . . . . . . . . . 10
9695breq1d 4214 . . . . . . . . 9
9796rexbidv 2718 . . . . . . . 8
9890, 97bitr3d 247 . . . . . . 7
9998rspcev 3044 . . . . . 6
1008, 87, 99sylancr 645 . . . . 5
101 eqeq1 2441 . . . . . . . 8
102101anbi2d 685 . . . . . . 7
103102rexbidv 2718 . . . . . 6
10421, 103elab 3074 . . . . 5
105100, 104sylibr 204 . . . 4
106 ne0i 3626 . . . 4
107105, 106syl 16 . . 3
108 fss 5591 . . . . . . 7
10952, 108mpan2 653 . . . . . 6
110 eqid 2435 . . . . . . 7
111110itg2addnclem 26219 . . . . . 6
11276, 109, 1113syl 19 . . . . 5
113 itg2addnc.g3 . . . . 5
114112, 113eqeltrrd 2510 . . . 4
11574, 60sstri 3349 . . . . . 6
116 supxrub 10893 . . . . . 6
117115, 116mpan 652 . . . . 5
118117rgen 2763 . . . 4
119 breq2 4208 . . . . . 6
120119ralbidv 2717 . . . . 5
121120rspcev 3044 . . . 4
122114, 118, 121sylancl 644 . . 3
123 eqid 2435 . . 3
1247, 51, 68, 75, 107, 122, 123supadd 26202 . 2
125 supxrre 10896 . . . . 5
1267, 51, 68, 125syl3anc 1184 . . . 4
12757, 126eqtrd 2467 . . 3
128 supxrre 10896 . . . . 5
12975, 107, 122, 128syl3anc 1184 . . . 4
130112, 129eqtrd 2467 . . 3
131127, 130oveq12d 6091 . 2
132 rexr 9120 . . . . . . . . . 10
133132anim1i 552 . . . . . . . . 9
134 elrege0 10997 . . . . . . . . 9
135 elxrge0 10998 . . . . . . . . 9
136133, 134, 1353imtr4i 258 . . . . . . . 8
137136ssriv 3344 . . . . . . 7
138 ge0addcl 10999 . . . . . . 7
139137, 138sseldi 3338 . . . . . 6
140139adantl 453 . . . . 5
141 inidm 3542 . . . . 5
142140, 13, 76, 20, 20, 141off 6312 . . . 4
143 eqid 2435 . . . . 5
144143itg2addnclem 26219 . . . 4
145142, 144syl 16 . . 3
146 itg2addnc.f1 . . . . . . . 8 MblFn
147146, 13, 58, 76, 113itg2addnclem3 26221 . . . . . . 7
148 simpl 444 . . . . . . . . . . . . . 14
149 simpr 448 . . . . . . . . . . . . . 14
150148, 149i1fadd 19577 . . . . . . . . . . . . 13
151150ad3antlr 712 . . . . . . . . . . . 12
152 reeanv 2867 . . . . . . . . . . . . . . . . 17
153152biimpri 198 . . . . . . . . . . . . . . . 16
154153ad2ant2r 728 . . . . . . . . . . . . . . 15
155 ifcl 3767 . . . . . . . . . . . . . . . . . . 19
156155ad2antlr 708 . . . . . . . . . . . . . . . . . 18
157 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . 24
158157anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . 23
159158imbi1d 309 . . . . . . . . . . . . . . . . . . . . . 22
160 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . 24
161160anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . 23
162161imbi1d 309 . . . . . . . . . . . . . . . . . . . . . 22
163 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . . 25
164163anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . 24
165164imbi1d 309 . . . . . . . . . . . . . . . . . . . . . . 23
166 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . . 25
167166anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . 24
168167imbi1d 309 . . . . . . . . . . . . . . . . . . . . . . 23
169 oveq12 6082 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
170 00id 9231 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
171169, 170syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
172 iftrue 3737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
173171, 172syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
174173adantll 695 . . . . . . . . . . . . . . . . . . . . . . . . 25
175 simpll 731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
17615simplbi 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
17714, 176syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
17878simplbi 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
17977, 178syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
180177, 179, 17, 80addge0d 9592 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
181175, 180sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . 26
182181ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 25
183174, 182eqbrtrd 4224 . . . . . . . . . . . . . . . . . . . . . . . 24
184183a1d 23 . . . . . . . . . . . . . . . . . . . . . . 23
185181ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
186 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
187 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
188 i1ff 19558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
189188ffvelrnda 5862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
190187, 189sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
191190recnd 9104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
192191addid2d 9257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
193186, 192sylan9eqr 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
194193oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
195194adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
196155rpred 10638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
197196ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
198190, 197readdcld 9105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
199198adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
200175, 179sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
201200adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
202175, 177sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
203202, 200readdcld 9105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
204203adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
205 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
206205rpred 10638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
207 rpre 10608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
208 rpre 10608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
209 min2 10767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
210207, 208, 209syl2an 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
211210ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
212197, 206, 190, 211leadd2dd 9631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
213190, 206readdcld 9105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
214 letr 9157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
215198, 213, 200, 214syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
216212, 215mpand 657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
217216imp 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
218179, 177addge02d 9605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
21917, 218mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
220175, 219sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
221220adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
222199, 201, 204, 217, 221letrd 9217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
223222adantlr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
224195, 223eqbrtrd 4224 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
225 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
226 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
227225, 226ifboth 3762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
228185, 224, 227syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26
229228ex 424 . . . . . . . . . . . . . . . . . . . . . . . . 25
230229adantld 454 . . . . . . . . . . . . . . . . . . . . . . . 24
231230adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
232165, 168, 184, 231ifbothda 3761 . . . . . . . . . . . . . . . . . . . . . 22
233163anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . 24
234233imbi1d 309 . . . . . . . . . . . . . . . . . . . . . . 23