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

 Description: Alternate proof of itg2add 19604 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 19553, 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 8271, 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

Proof of Theorem itg2addnc
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprr 734 . . . . . . 7
2 itg1cl 19530 . . . . . . . 8
32adantr 452 . . . . . . 7
41, 3eqeltrd 2478 . . . . . 6
54rexlimiva 2785 . . . . 5
65abssi 3378 . . . 4
76a1i 11 . . 3
8 i1f0 19532 . . . . . 6
9 3nn 10090 . . . . . . . 8
10 nnrp 10577 . . . . . . . 8
11 ne0i 3594 . . . . . . . 8
129, 10, 11mp2b 10 . . . . . . 7
13 itg2addnc.f2 . . . . . . . . . . . . 13
1413ffvelrnda 5829 . . . . . . . . . . . 12
15 elrege0 10963 . . . . . . . . . . . 12
1614, 15sylib 189 . . . . . . . . . . 11
1716simprd 450 . . . . . . . . . 10
1817ralrimiva 2749 . . . . . . . . 9
19 reex 9037 . . . . . . . . . . 11
2019a1i 11 . . . . . . . . . 10
21 c0ex 9041 . . . . . . . . . . 11
2221a1i 11 . . . . . . . . . 10
23 eqidd 2405 . . . . . . . . . 10
2413feqmptd 5738 . . . . . . . . . 10
2520, 22, 14, 23, 24ofrfval2 6282 . . . . . . . . 9
2618, 25mpbird 224 . . . . . . . 8
2726ralrimivw 2750 . . . . . . 7
28 r19.2z 3677 . . . . . . 7
2912, 27, 28sylancr 645 . . . . . 6
30 fveq2 5687 . . . . . . . . . 10
31 itg10 19533 . . . . . . . . . 10
3230, 31syl6req 2453 . . . . . . . . 9
3332biantrud 494 . . . . . . . 8
34 fveq1 5686 . . . . . . . . . . . . 13
3521fvconst2 5906 . . . . . . . . . . . . 13
3634, 35sylan9eq 2456 . . . . . . . . . . . 12
37 iftrue 3705 . . . . . . . . . . . 12
3836, 37syl 16 . . . . . . . . . . 11
3938mpteq2dva 4255 . . . . . . . . . 10
4039breq1d 4182 . . . . . . . . 9
4140rexbidv 2687 . . . . . . . 8
4233, 41bitr3d 247 . . . . . . 7
4342rspcev 3012 . . . . . 6
448, 29, 43sylancr 645 . . . . 5
45 eqeq1 2410 . . . . . . . 8
4645anbi2d 685 . . . . . . 7
4746rexbidv 2687 . . . . . 6
4821, 47elab 3042 . . . . 5
4944, 48sylibr 204 . . . 4
50 ne0i 3594 . . . 4
5149, 50syl 16 . . 3
52 icossicc 24082 . . . . . . 7
53 fss 5558 . . . . . . 7
5452, 53mpan2 653 . . . . . 6
55 eqid 2404 . . . . . . 7
5655itg2addnclem 26155 . . . . . 6
5713, 54, 563syl 19 . . . . 5
58 itg2addnc.f3 . . . . 5
5957, 58eqeltrrd 2479 . . . 4
60 ressxr 9085 . . . . . . 7
616, 60sstri 3317 . . . . . 6
62 supxrub 10859 . . . . . 6
6361, 62mpan 652 . . . . 5
6463rgen 2731 . . . 4
65 breq2 4176 . . . . . 6
6665ralbidv 2686 . . . . 5
6766rspcev 3012 . . . 4
6859, 64, 67sylancl 644 . . 3
69 simprr 734 . . . . . . 7
70 itg1cl 19530 . . . . . . . 8
7170adantr 452 . . . . . . 7
7269, 71eqeltrd 2478 . . . . . 6
7372rexlimiva 2785 . . . . 5
7473abssi 3378 . . . 4
7574a1i 11 . . 3
76 itg2addnc.g2 . . . . . . . . . . . . 13
7776ffvelrnda 5829 . . . . . . . . . . . 12
78 elrege0 10963 . . . . . . . . . . . 12
7977, 78sylib 189 . . . . . . . . . . 11
8079simprd 450 . . . . . . . . . 10
8180ralrimiva 2749 . . . . . . . . 9
8276feqmptd 5738 . . . . . . . . . 10
8320, 22, 77, 23, 82ofrfval2 6282 . . . . . . . . 9
8481, 83mpbird 224 . . . . . . . 8
8584ralrimivw 2750 . . . . . . 7
86 r19.2z 3677 . . . . . . 7
8712, 85, 86sylancr 645 . . . . . 6
88 fveq2 5687 . . . . . . . . . 10
8988, 31syl6req 2453 . . . . . . . . 9
9089biantrud 494 . . . . . . . 8
91 fveq1 5686 . . . . . . . . . . . . 13
9291, 35sylan9eq 2456 . . . . . . . . . . . 12
93 iftrue 3705 . . . . . . . . . . . 12
9492, 93syl 16 . . . . . . . . . . 11
9594mpteq2dva 4255 . . . . . . . . . 10
9695breq1d 4182 . . . . . . . . 9
9796rexbidv 2687 . . . . . . . 8
9890, 97bitr3d 247 . . . . . . 7
9998rspcev 3012 . . . . . 6
1008, 87, 99sylancr 645 . . . . 5
101 eqeq1 2410 . . . . . . . 8
102101anbi2d 685 . . . . . . 7
103102rexbidv 2687 . . . . . 6
10421, 103elab 3042 . . . . 5
105100, 104sylibr 204 . . . 4
106 ne0i 3594 . . . 4
107105, 106syl 16 . . 3
108 fss 5558 . . . . . . 7
10952, 108mpan2 653 . . . . . 6
110 eqid 2404 . . . . . . 7
111110itg2addnclem 26155 . . . . . 6
11276, 109, 1113syl 19 . . . . 5
113 itg2addnc.g3 . . . . 5
114112, 113eqeltrrd 2479 . . . 4
11574, 60sstri 3317 . . . . . 6
116 supxrub 10859 . . . . . 6
117115, 116mpan 652 . . . . 5
118117rgen 2731 . . . 4
119 breq2 4176 . . . . . 6
120119ralbidv 2686 . . . . 5
121120rspcev 3012 . . . 4
122114, 118, 121sylancl 644 . . 3
123 eqid 2404 . . 3
1247, 51, 68, 75, 107, 122, 123supadd 26138 . 2
125 supxrre 10862 . . . . 5
1267, 51, 68, 125syl3anc 1184 . . . 4
12757, 126eqtrd 2436 . . 3
128 supxrre 10862 . . . . 5
12975, 107, 122, 128syl3anc 1184 . . . 4
130112, 129eqtrd 2436 . . 3
131127, 130oveq12d 6058 . 2
132 rexr 9086 . . . . . . . . . 10
133132anim1i 552 . . . . . . . . 9
134 elrege0 10963 . . . . . . . . 9
135 elxrge0 10964 . . . . . . . . 9
136133, 134, 1353imtr4i 258 . . . . . . . 8
137136ssriv 3312 . . . . . . 7
138 ge0addcl 10965 . . . . . . 7
139137, 138sseldi 3306 . . . . . 6
140139adantl 453 . . . . 5
141 inidm 3510 . . . . 5
142140, 13, 76, 20, 20, 141off 6279 . . . 4
143 eqid 2404 . . . . 5
144143itg2addnclem 26155 . . . 4
145142, 144syl 16 . . 3
146 itg2addnc.f1 . . . . . . . 8 MblFn
147146, 13, 58, 76, 113itg2addnclem3 26157 . . . . . . 7
148 simpl 444 . . . . . . . . . . . . . 14
149 simpr 448 . . . . . . . . . . . . . 14
150148, 149i1fadd 19540 . . . . . . . . . . . . 13
151150ad3antlr 712 . . . . . . . . . . . 12
152 reeanv 2835 . . . . . . . . . . . . . . . . 17
153152biimpri 198 . . . . . . . . . . . . . . . 16
154153ad2ant2r 728 . . . . . . . . . . . . . . 15
155 ifcl 3735 . . . . . . . . . . . . . . . . . . 19
156155ad2antlr 708 . . . . . . . . . . . . . . . . . 18
157 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . 24
158157anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . 23
159158imbi1d 309 . . . . . . . . . . . . . . . . . . . . . 22
160 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . 24
161160anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . 23
162161imbi1d 309 . . . . . . . . . . . . . . . . . . . . . 22
163 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . . 25
164163anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . 24
165164imbi1d 309 . . . . . . . . . . . . . . . . . . . . . . 23
166 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . . 25
167166anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . 24
168167imbi1d 309 . . . . . . . . . . . . . . . . . . . . . . 23
169 oveq12 6049 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
170 00id 9197 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
171169, 170syl6eq 2452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
172 iftrue 3705 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9558 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
181175, 180sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . 26
182181ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 25
183174, 182eqbrtrd 4192 . . . . . . . . . . . . . . . . . . . . . . . 24
184183a1d 23 . . . . . . . . . . . . . . . . . . . . . . 23
185181ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
186 oveq1 6047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
187 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
188 i1ff 19521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
189188ffvelrnda 5829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
190187, 189sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
191190recnd 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
192191addid2d 9223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
193186, 192sylan9eqr 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
194193oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
195194adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
196155rpred 10604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
197196ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
198190, 197readdcld 9071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
199198adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
200175, 179sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
201200adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
202175, 177sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
203202, 200readdcld 9071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
204203adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
205 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
206205rpred 10604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
207 rpre 10574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
208 rpre 10574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
209 min2 10733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
210207, 208, 209syl2an 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
211210ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
212197, 206, 190, 211leadd2dd 9597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
213190, 206readdcld 9071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
214 letr 9123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
215198, 213, 200, 214syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
216212, 215mpand 657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
217216imp 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
218179, 177addge02d 9571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
21917, 218mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
220175, 219sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
221220adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
222199, 201, 204, 217, 221letrd 9183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
223222adantlr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
224195, 223eqbrtrd 4192 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
225 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
226 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
227225, 226ifboth 3730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
228185, 224, 227syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26
229228ex 424 . . . . . . . . . . . . . . . . . . . . . . . . 25
230229adantld 454 . . . . . . . . . . . . . . . . . . . . . . . 24
231230adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
232165, 168, 184, 231ifbothda 3729 . . . . . . . . . . . . . . . . . . . . . 22
233163anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . 24
234233imbi1d 309 . . . . . . . . . . . . . . . . . . . . . . 23