Metamath Proof Explorer


Theorem itg2cn

Description: A sort of absolute continuity of the Lebesgue integral (this is the core of ftc1a which is about actual absolute continuity). (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses itg2cn.1 φF:0+∞
itg2cn.2 φFMblFn
itg2cn.3 φ2F
itg2cn.4 φC+
Assertion itg2cn φd+udomvolvolu<d2xifxuFx0<C

Proof

Step Hyp Ref Expression
1 itg2cn.1 φF:0+∞
2 itg2cn.2 φFMblFn
3 itg2cn.3 φ2F
4 itg2cn.4 φC+
5 4 rphalfcld φC2+
6 3 5 ltsubrpd φ2FC2<2F
7 5 rpred φC2
8 3 7 resubcld φ2FC2
9 8 3 ltnled φ2FC2<2F¬2F2FC2
10 6 9 mpbid φ¬2F2FC2
11 1 ffvelrnda φxFx0+∞
12 elrege0 Fx0+∞Fx0Fx
13 11 12 sylib φxFx0Fx
14 13 simpld φxFx
15 14 rexrd φxFx*
16 13 simprd φx0Fx
17 elxrge0 Fx0+∞Fx*0Fx
18 15 16 17 sylanbrc φxFx0+∞
19 0e0iccpnf 00+∞
20 ifcl Fx0+∞00+∞ifFxnFx00+∞
21 18 19 20 sylancl φxifFxnFx00+∞
22 21 adantlr φnxifFxnFx00+∞
23 22 fmpttd φnxifFxnFx0:0+∞
24 itg2cl xifFxnFx0:0+∞2xifFxnFx0*
25 23 24 syl φn2xifFxnFx0*
26 25 fmpttd φn2xifFxnFx0:*
27 26 frnd φrann2xifFxnFx0*
28 8 rexrd φ2FC2*
29 supxrleub rann2xifFxnFx0*2FC2*suprann2xifFxnFx0*<2FC2zrann2xifFxnFx0z2FC2
30 27 28 29 syl2anc φsuprann2xifFxnFx0*<2FC2zrann2xifFxnFx0z2FC2
31 1 2 3 itg2cnlem1 φsuprann2xifFxnFx0*<=2F
32 31 breq1d φsuprann2xifFxnFx0*<2FC22F2FC2
33 26 ffnd φn2xifFxnFx0Fn
34 breq1 z=n2xifFxnFx0mz2FC2n2xifFxnFx0m2FC2
35 34 ralrn n2xifFxnFx0Fnzrann2xifFxnFx0z2FC2mn2xifFxnFx0m2FC2
36 breq2 n=mFxnFxm
37 36 ifbid n=mifFxnFx0=ifFxmFx0
38 37 mpteq2dv n=mxifFxnFx0=xifFxmFx0
39 38 fveq2d n=m2xifFxnFx0=2xifFxmFx0
40 eqid n2xifFxnFx0=n2xifFxnFx0
41 fvex 2xifFxmFx0V
42 39 40 41 fvmpt mn2xifFxnFx0m=2xifFxmFx0
43 42 breq1d mn2xifFxnFx0m2FC22xifFxmFx02FC2
44 43 ralbiia mn2xifFxnFx0m2FC2m2xifFxmFx02FC2
45 35 44 bitrdi n2xifFxnFx0Fnzrann2xifFxnFx0z2FC2m2xifFxmFx02FC2
46 33 45 syl φzrann2xifFxnFx0z2FC2m2xifFxmFx02FC2
47 30 32 46 3bitr3d φ2F2FC2m2xifFxmFx02FC2
48 10 47 mtbid φ¬m2xifFxmFx02FC2
49 rexnal m¬2xifFxmFx02FC2¬m2xifFxmFx02FC2
50 48 49 sylibr φm¬2xifFxmFx02FC2
51 1 adantr φm¬2xifFxmFx02FC2F:0+∞
52 2 adantr φm¬2xifFxmFx02FC2FMblFn
53 3 adantr φm¬2xifFxmFx02FC22F
54 4 adantr φm¬2xifFxmFx02FC2C+
55 simprl φm¬2xifFxmFx02FC2m
56 simprr φm¬2xifFxmFx02FC2¬2xifFxmFx02FC2
57 fveq2 x=yFx=Fy
58 57 breq1d x=yFxmFym
59 58 57 ifbieq1d x=yifFxmFx0=ifFymFy0
60 59 cbvmptv xifFxmFx0=yifFymFy0
61 60 fveq2i 2xifFxmFx0=2yifFymFy0
62 61 breq1i 2xifFxmFx02FC22yifFymFy02FC2
63 56 62 sylnib φm¬2xifFxmFx02FC2¬2yifFymFy02FC2
64 51 52 53 54 55 63 itg2cnlem2 φm¬2xifFxmFx02FC2d+udomvolvolu<d2yifyuFy0<C
65 elequ1 x=yxuyu
66 65 57 ifbieq1d x=yifxuFx0=ifyuFy0
67 66 cbvmptv xifxuFx0=yifyuFy0
68 67 fveq2i 2xifxuFx0=2yifyuFy0
69 68 breq1i 2xifxuFx0<C2yifyuFy0<C
70 69 imbi2i volu<d2xifxuFx0<Cvolu<d2yifyuFy0<C
71 70 ralbii udomvolvolu<d2xifxuFx0<Cudomvolvolu<d2yifyuFy0<C
72 71 rexbii d+udomvolvolu<d2xifxuFx0<Cd+udomvolvolu<d2yifyuFy0<C
73 64 72 sylibr φm¬2xifFxmFx02FC2d+udomvolvolu<d2xifxuFx0<C
74 50 73 rexlimddv φd+udomvolvolu<d2xifxuFx0<C