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 
|- ( ph -> F : RR --> ( 0 [,) +oo ) )
itg2cn.2 
|- ( ph -> F e. MblFn )
itg2cn.3 
|- ( ph -> ( S.2 ` F ) e. RR )
itg2cn.4 
|- ( ph -> C e. RR+ )
Assertion itg2cn 
|- ( ph -> E. d e. RR+ A. u e. dom vol ( ( vol ` u ) < d -> ( S.2 ` ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) ) < C ) )

Proof

Step Hyp Ref Expression
1 itg2cn.1 
 |-  ( ph -> F : RR --> ( 0 [,) +oo ) )
2 itg2cn.2 
 |-  ( ph -> F e. MblFn )
3 itg2cn.3 
 |-  ( ph -> ( S.2 ` F ) e. RR )
4 itg2cn.4 
 |-  ( ph -> C e. RR+ )
5 4 rphalfcld 
 |-  ( ph -> ( C / 2 ) e. RR+ )
6 3 5 ltsubrpd 
 |-  ( ph -> ( ( S.2 ` F ) - ( C / 2 ) ) < ( S.2 ` F ) )
7 5 rpred 
 |-  ( ph -> ( C / 2 ) e. RR )
8 3 7 resubcld 
 |-  ( ph -> ( ( S.2 ` F ) - ( C / 2 ) ) e. RR )
9 8 3 ltnled 
 |-  ( ph -> ( ( ( S.2 ` F ) - ( C / 2 ) ) < ( S.2 ` F ) <-> -. ( S.2 ` F ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) )
10 6 9 mpbid 
 |-  ( ph -> -. ( S.2 ` F ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) )
11 1 ffvelrnda 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
12 elrege0 
 |-  ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
13 11 12 sylib 
 |-  ( ( ph /\ x e. RR ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
14 13 simpld 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR )
15 14 rexrd 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR* )
16 13 simprd 
 |-  ( ( ph /\ x e. RR ) -> 0 <_ ( F ` x ) )
17 elxrge0 
 |-  ( ( F ` x ) e. ( 0 [,] +oo ) <-> ( ( F ` x ) e. RR* /\ 0 <_ ( F ` x ) ) )
18 15 16 17 sylanbrc 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) e. ( 0 [,] +oo ) )
19 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
20 ifcl 
 |-  ( ( ( F ` x ) e. ( 0 [,] +oo ) /\ 0 e. ( 0 [,] +oo ) ) -> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) e. ( 0 [,] +oo ) )
21 18 19 20 sylancl 
 |-  ( ( ph /\ x e. RR ) -> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) e. ( 0 [,] +oo ) )
22 21 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) e. ( 0 [,] +oo ) )
23 22 fmpttd 
 |-  ( ( ph /\ n e. NN ) -> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
24 itg2cl 
 |-  ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) e. RR* )
25 23 24 syl 
 |-  ( ( ph /\ n e. NN ) -> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) e. RR* )
26 25 fmpttd 
 |-  ( ph -> ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) : NN --> RR* )
27 26 frnd 
 |-  ( ph -> ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) C_ RR* )
28 8 rexrd 
 |-  ( ph -> ( ( S.2 ` F ) - ( C / 2 ) ) e. RR* )
29 supxrleub 
 |-  ( ( ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) C_ RR* /\ ( ( S.2 ` F ) - ( C / 2 ) ) e. RR* ) -> ( sup ( ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) , RR* , < ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) <-> A. z e. ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) z <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) )
30 27 28 29 syl2anc 
 |-  ( ph -> ( sup ( ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) , RR* , < ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) <-> A. z e. ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) z <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) )
31 1 2 3 itg2cnlem1 
 |-  ( ph -> sup ( ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) , RR* , < ) = ( S.2 ` F ) )
32 31 breq1d 
 |-  ( ph -> ( sup ( ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) , RR* , < ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) <-> ( S.2 ` F ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) )
33 26 ffnd 
 |-  ( ph -> ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) Fn NN )
34 breq1 
 |-  ( z = ( ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) ` m ) -> ( z <_ ( ( S.2 ` F ) - ( C / 2 ) ) <-> ( ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) ` m ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) )
35 34 ralrn 
 |-  ( ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) Fn NN -> ( A. z e. ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) z <_ ( ( S.2 ` F ) - ( C / 2 ) ) <-> A. m e. NN ( ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) ` m ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) )
36 breq2 
 |-  ( n = m -> ( ( F ` x ) <_ n <-> ( F ` x ) <_ m ) )
37 36 ifbid 
 |-  ( n = m -> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) = if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) )
38 37 mpteq2dv 
 |-  ( n = m -> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) )
39 38 fveq2d 
 |-  ( n = m -> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) )
40 eqid 
 |-  ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) = ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) )
41 fvex 
 |-  ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) e. _V
42 39 40 41 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) ` m ) = ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) )
43 42 breq1d 
 |-  ( m e. NN -> ( ( ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) ` m ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) <-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) )
44 43 ralbiia 
 |-  ( A. m e. NN ( ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) ` m ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) <-> A. m e. NN ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) )
45 35 44 bitrdi 
 |-  ( ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) Fn NN -> ( A. z e. ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) z <_ ( ( S.2 ` F ) - ( C / 2 ) ) <-> A. m e. NN ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) )
46 33 45 syl 
 |-  ( ph -> ( A. z e. ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) z <_ ( ( S.2 ` F ) - ( C / 2 ) ) <-> A. m e. NN ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) )
47 30 32 46 3bitr3d 
 |-  ( ph -> ( ( S.2 ` F ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) <-> A. m e. NN ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) )
48 10 47 mtbid 
 |-  ( ph -> -. A. m e. NN ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) )
49 rexnal 
 |-  ( E. m e. NN -. ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) <-> -. A. m e. NN ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) )
50 48 49 sylibr 
 |-  ( ph -> E. m e. NN -. ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) )
51 1 adantr 
 |-  ( ( ph /\ ( m e. NN /\ -. ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) ) -> F : RR --> ( 0 [,) +oo ) )
52 2 adantr 
 |-  ( ( ph /\ ( m e. NN /\ -. ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) ) -> F e. MblFn )
53 3 adantr 
 |-  ( ( ph /\ ( m e. NN /\ -. ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) ) -> ( S.2 ` F ) e. RR )
54 4 adantr 
 |-  ( ( ph /\ ( m e. NN /\ -. ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) ) -> C e. RR+ )
55 simprl 
 |-  ( ( ph /\ ( m e. NN /\ -. ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) ) -> m e. NN )
56 simprr 
 |-  ( ( ph /\ ( m e. NN /\ -. ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) ) -> -. ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) )
57 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
58 57 breq1d 
 |-  ( x = y -> ( ( F ` x ) <_ m <-> ( F ` y ) <_ m ) )
59 58 57 ifbieq1d 
 |-  ( x = y -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) = if ( ( F ` y ) <_ m , ( F ` y ) , 0 ) )
60 59 cbvmptv 
 |-  ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) = ( y e. RR |-> if ( ( F ` y ) <_ m , ( F ` y ) , 0 ) )
61 60 fveq2i 
 |-  ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) = ( S.2 ` ( y e. RR |-> if ( ( F ` y ) <_ m , ( F ` y ) , 0 ) ) )
62 61 breq1i 
 |-  ( ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) <-> ( S.2 ` ( y e. RR |-> if ( ( F ` y ) <_ m , ( F ` y ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) )
63 56 62 sylnib 
 |-  ( ( ph /\ ( m e. NN /\ -. ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) ) -> -. ( S.2 ` ( y e. RR |-> if ( ( F ` y ) <_ m , ( F ` y ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) )
64 51 52 53 54 55 63 itg2cnlem2 
 |-  ( ( ph /\ ( m e. NN /\ -. ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) ) -> E. d e. RR+ A. u e. dom vol ( ( vol ` u ) < d -> ( S.2 ` ( y e. RR |-> if ( y e. u , ( F ` y ) , 0 ) ) ) < C ) )
65 elequ1 
 |-  ( x = y -> ( x e. u <-> y e. u ) )
66 65 57 ifbieq1d 
 |-  ( x = y -> if ( x e. u , ( F ` x ) , 0 ) = if ( y e. u , ( F ` y ) , 0 ) )
67 66 cbvmptv 
 |-  ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) = ( y e. RR |-> if ( y e. u , ( F ` y ) , 0 ) )
68 67 fveq2i 
 |-  ( S.2 ` ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) ) = ( S.2 ` ( y e. RR |-> if ( y e. u , ( F ` y ) , 0 ) ) )
69 68 breq1i 
 |-  ( ( S.2 ` ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) ) < C <-> ( S.2 ` ( y e. RR |-> if ( y e. u , ( F ` y ) , 0 ) ) ) < C )
70 69 imbi2i 
 |-  ( ( ( vol ` u ) < d -> ( S.2 ` ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) ) < C ) <-> ( ( vol ` u ) < d -> ( S.2 ` ( y e. RR |-> if ( y e. u , ( F ` y ) , 0 ) ) ) < C ) )
71 70 ralbii 
 |-  ( A. u e. dom vol ( ( vol ` u ) < d -> ( S.2 ` ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) ) < C ) <-> A. u e. dom vol ( ( vol ` u ) < d -> ( S.2 ` ( y e. RR |-> if ( y e. u , ( F ` y ) , 0 ) ) ) < C ) )
72 71 rexbii 
 |-  ( E. d e. RR+ A. u e. dom vol ( ( vol ` u ) < d -> ( S.2 ` ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) ) < C ) <-> E. d e. RR+ A. u e. dom vol ( ( vol ` u ) < d -> ( S.2 ` ( y e. RR |-> if ( y e. u , ( F ` y ) , 0 ) ) ) < C ) )
73 64 72 sylibr 
 |-  ( ( ph /\ ( m e. NN /\ -. ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) ) ) -> E. d e. RR+ A. u e. dom vol ( ( vol ` u ) < d -> ( S.2 ` ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) ) < C ) )
74 50 73 rexlimddv 
 |-  ( ph -> E. d e. RR+ A. u e. dom vol ( ( vol ` u ) < d -> ( S.2 ` ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) ) < C ) )