Metamath Proof Explorer


Theorem itgeqa

Description: Approximate equality of integrals. If C ( x ) = D ( x ) for almost all x , then S. B C ( x )d x = S. B D ( x ) d x and one is integrable iff the other is. (Contributed by Mario Carneiro, 12-Aug-2014) (Revised by Mario Carneiro, 2-Sep-2014)

Ref Expression
Hypotheses itgeqa.1 φxBC
itgeqa.2 φxBD
itgeqa.3 φA
itgeqa.4 φvol*A=0
itgeqa.5 φxBAC=D
Assertion itgeqa φxBC𝐿1xBD𝐿1BCdx=BDdx

Proof

Step Hyp Ref Expression
1 itgeqa.1 φxBC
2 itgeqa.2 φxBD
3 itgeqa.3 φA
4 itgeqa.4 φvol*A=0
5 itgeqa.5 φxBAC=D
6 3 4 5 1 2 mbfeqa φxBCMblFnxBDMblFn
7 ifan ifxB0CikCik0=ifxBif0CikCik00
8 1 adantlr φk03xBC
9 ax-icn i
10 ine0 i0
11 elfzelz k03k
12 11 ad2antlr φk03xBk
13 expclz ii0kik
14 9 10 12 13 mp3an12i φk03xBik
15 expne0i ii0kik0
16 9 10 12 15 mp3an12i φk03xBik0
17 8 14 16 divcld φk03xBCik
18 17 recld φk03xBCik
19 0re 0
20 ifcl Cik0if0CikCik0
21 18 19 20 sylancl φk03xBif0CikCik0
22 21 rexrd φk03xBif0CikCik0*
23 max1 0Cik0if0CikCik0
24 19 18 23 sylancr φk03xB0if0CikCik0
25 elxrge0 if0CikCik00+∞if0CikCik0*0if0CikCik0
26 22 24 25 sylanbrc φk03xBif0CikCik00+∞
27 0e0iccpnf 00+∞
28 27 a1i φk03¬xB00+∞
29 26 28 ifclda φk03ifxBif0CikCik000+∞
30 7 29 eqeltrid φk03ifxB0CikCik00+∞
31 30 adantr φk03xifxB0CikCik00+∞
32 31 fmpttd φk03xifxB0CikCik0:0+∞
33 ifan ifxB0DikDik0=ifxBif0DikDik00
34 2 adantlr φk03xBD
35 34 14 16 divcld φk03xBDik
36 35 recld φk03xBDik
37 ifcl Dik0if0DikDik0
38 36 19 37 sylancl φk03xBif0DikDik0
39 38 rexrd φk03xBif0DikDik0*
40 max1 0Dik0if0DikDik0
41 19 36 40 sylancr φk03xB0if0DikDik0
42 elxrge0 if0DikDik00+∞if0DikDik0*0if0DikDik0
43 39 41 42 sylanbrc φk03xBif0DikDik00+∞
44 43 28 ifclda φk03ifxBif0DikDik000+∞
45 33 44 eqeltrid φk03ifxB0DikDik00+∞
46 45 adantr φk03xifxB0DikDik00+∞
47 46 fmpttd φk03xifxB0DikDik0:0+∞
48 3 adantr φk03A
49 4 adantr φk03vol*A=0
50 simpll φxAxBφ
51 simpr φxAxBxB
52 eldifn xA¬xA
53 52 ad2antlr φxAxB¬xA
54 51 53 eldifd φxAxBxBA
55 50 54 5 syl2anc φxAxBC=D
56 55 fvoveq1d φxAxBCik=Dik
57 56 ibllem φxAifxB0CikCik0=ifxB0DikDik0
58 eldifi xAx
59 58 adantl φxAx
60 fvex CikV
61 c0ex 0V
62 60 61 ifex ifxB0CikCik0V
63 eqid xifxB0CikCik0=xifxB0CikCik0
64 63 fvmpt2 xifxB0CikCik0VxifxB0CikCik0x=ifxB0CikCik0
65 59 62 64 sylancl φxAxifxB0CikCik0x=ifxB0CikCik0
66 fvex DikV
67 66 61 ifex ifxB0DikDik0V
68 eqid xifxB0DikDik0=xifxB0DikDik0
69 68 fvmpt2 xifxB0DikDik0VxifxB0DikDik0x=ifxB0DikDik0
70 59 67 69 sylancl φxAxifxB0DikDik0x=ifxB0DikDik0
71 57 65 70 3eqtr4d φxAxifxB0CikCik0x=xifxB0DikDik0x
72 71 ralrimiva φxAxifxB0CikCik0x=xifxB0DikDik0x
73 nfv yxifxB0CikCik0x=xifxB0DikDik0x
74 nffvmpt1 _xxifxB0CikCik0y
75 nffvmpt1 _xxifxB0DikDik0y
76 74 75 nfeq xxifxB0CikCik0y=xifxB0DikDik0y
77 fveq2 x=yxifxB0CikCik0x=xifxB0CikCik0y
78 fveq2 x=yxifxB0DikDik0x=xifxB0DikDik0y
79 77 78 eqeq12d x=yxifxB0CikCik0x=xifxB0DikDik0xxifxB0CikCik0y=xifxB0DikDik0y
80 73 76 79 cbvralw xAxifxB0CikCik0x=xifxB0DikDik0xyAxifxB0CikCik0y=xifxB0DikDik0y
81 72 80 sylib φyAxifxB0CikCik0y=xifxB0DikDik0y
82 81 r19.21bi φyAxifxB0CikCik0y=xifxB0DikDik0y
83 82 adantlr φk03yAxifxB0CikCik0y=xifxB0DikDik0y
84 32 47 48 49 83 itg2eqa φk032xifxB0CikCik0=2xifxB0DikDik0
85 84 eleq1d φk032xifxB0CikCik02xifxB0DikDik0
86 85 ralbidva φk032xifxB0CikCik0k032xifxB0DikDik0
87 6 86 anbi12d φxBCMblFnk032xifxB0CikCik0xBDMblFnk032xifxB0DikDik0
88 eqidd φxifxB0CikCik0=xifxB0CikCik0
89 eqidd φxBCik=Cik
90 88 89 1 isibl2 φxBC𝐿1xBCMblFnk032xifxB0CikCik0
91 eqidd φxifxB0DikDik0=xifxB0DikDik0
92 eqidd φxBDik=Dik
93 91 92 2 isibl2 φxBD𝐿1xBDMblFnk032xifxB0DikDik0
94 87 90 93 3bitr4d φxBC𝐿1xBD𝐿1
95 84 oveq2d φk03ik2xifxB0CikCik0=ik2xifxB0DikDik0
96 95 sumeq2dv φk=03ik2xifxB0CikCik0=k=03ik2xifxB0DikDik0
97 eqid Cik=Cik
98 97 dfitg BCdx=k=03ik2xifxB0CikCik0
99 eqid Dik=Dik
100 99 dfitg BDdx=k=03ik2xifxB0DikDik0
101 96 98 100 3eqtr4g φBCdx=BDdx
102 94 101 jca φxBC𝐿1xBD𝐿1BCdx=BDdx