Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg1addlem2 Structured version   Unicode version

 Description: Lemma for itg1add 19595. The function represents the pieces into which we will break up the domain of the sum. Since it is infinite only when both and are zero, we arbitrarily define it to be zero there to simplify the sums that are manipulated in itg1addlem4 19593 and itg1addlem5 19594. (Contributed by Mario Carneiro, 26-Jun-2014.)
Hypotheses
Ref Expression
Assertion
Ref Expression
Distinct variable groups:   ,,   ,,   ,,
Allowed substitution hints:   (,)

StepHypRef Expression
1 iffalse 3748 . . . . . . . 8
21adantl 454 . . . . . . 7
3 i1fadd.1 . . . . . . . . . . 11
4 i1fima 19572 . . . . . . . . . . 11
53, 4syl 16 . . . . . . . . . 10
6 i1fadd.2 . . . . . . . . . . 11
7 i1fima 19572 . . . . . . . . . . 11
86, 7syl 16 . . . . . . . . . 10
9 inmbl 19438 . . . . . . . . . 10
105, 8, 9syl2anc 644 . . . . . . . . 9
1110ad2antrr 708 . . . . . . . 8
12 mblvol 19428 . . . . . . . 8
1311, 12syl 16 . . . . . . 7
142, 13eqtrd 2470 . . . . . 6
15 neorian 2693 . . . . . . 7
16 inss1 3563 . . . . . . . . . 10
1716a1i 11 . . . . . . . . 9
185ad2antrr 708 . . . . . . . . . 10
19 mblss 19429 . . . . . . . . . 10
2018, 19syl 16 . . . . . . . . 9
21 mblvol 19428 . . . . . . . . . . 11
2218, 21syl 16 . . . . . . . . . 10
233ad2antrr 708 . . . . . . . . . . 11
24 simplrl 738 . . . . . . . . . . . 12
25 simpr 449 . . . . . . . . . . . 12
26 eldifsn 3929 . . . . . . . . . . . 12
2724, 25, 26sylanbrc 647 . . . . . . . . . . 11
28 i1fima2sn 19574 . . . . . . . . . . 11
2923, 27, 28syl2anc 644 . . . . . . . . . 10
3022, 29eqeltrrd 2513 . . . . . . . . 9
31 ovolsscl 19384 . . . . . . . . 9
3217, 20, 30, 31syl3anc 1185 . . . . . . . 8
33 inss2 3564 . . . . . . . . . 10
3433a1i 11 . . . . . . . . 9
356adantr 453 . . . . . . . . . . . 12
3635, 7syl 16 . . . . . . . . . . 11
3736adantr 453 . . . . . . . . . 10
38 mblss 19429 . . . . . . . . . 10
3937, 38syl 16 . . . . . . . . 9
40 mblvol 19428 . . . . . . . . . . 11
4137, 40syl 16 . . . . . . . . . 10
426ad2antrr 708 . . . . . . . . . . 11
43 simplrr 739 . . . . . . . . . . . 12
44 simpr 449 . . . . . . . . . . . 12
45 eldifsn 3929 . . . . . . . . . . . 12
4643, 44, 45sylanbrc 647 . . . . . . . . . . 11
47 i1fima2sn 19574 . . . . . . . . . . 11
4842, 46, 47syl2anc 644 . . . . . . . . . 10
4941, 48eqeltrrd 2513 . . . . . . . . 9
50 ovolsscl 19384 . . . . . . . . 9
5134, 39, 49, 50syl3anc 1185 . . . . . . . 8
5232, 51jaodan 762 . . . . . . 7
5315, 52sylan2br 464 . . . . . 6
5414, 53eqeltrd 2512 . . . . 5
5554ex 425 . . . 4
56 iftrue 3747 . . . . 5
57 0re 9093 . . . . 5
5856, 57syl6eqel 2526 . . . 4
5955, 58pm2.61d2 155 . . 3
6059ralrimivva 2800 . 2