Metamath Proof Explorer

Theorem itg2const2

Description: When the base set of a constant function has infinite volume, the integral is also infinite and vice-versa. (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Assertion itg2const2 
|- ( ( A e. dom vol /\ B e. RR+ ) -> ( ( vol ` A ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( vol ` A ) e. RR ) -> A e. dom vol )
2 simpr 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( vol ` A ) e. RR ) -> ( vol ` A ) e. RR )
3 rpre 
 |-  ( B e. RR+ -> B e. RR )
4 3 ad2antlr 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( vol ` A ) e. RR ) -> B e. RR )
5 rpge0 
 |-  ( B e. RR+ -> 0 <_ B )
6 5 ad2antlr 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( vol ` A ) e. RR ) -> 0 <_ B )
7 elrege0 
 |-  ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )
8 4 6 7 sylanbrc 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( vol ` A ) e. RR ) -> B e. ( 0 [,) +oo ) )
9 itg2const 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) = ( B x. ( vol ` A ) ) )
10 1 2 8 9 syl3anc 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( vol ` A ) e. RR ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) = ( B x. ( vol ` A ) ) )
11 4 2 remulcld 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( vol ` A ) e. RR ) -> ( B x. ( vol ` A ) ) e. RR )
12 10 11 eqeltrd 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( vol ` A ) e. RR ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR )
13 mblvol 
 |-  ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) )
14 13 ad2antrr 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( vol ` A ) = ( vol* ` A ) )
15 mblss 
 |-  ( A e. dom vol -> A C_ RR )
16 15 ad3antrrr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( vol* ` A ) <_ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) -> A C_ RR )
17 peano2re 
 |-  ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR -> ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) e. RR )
18 17 adantl 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) e. RR )
19 simplr 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> B e. RR+ )
20 18 19 rerpdivcld 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. RR )
21 20 adantr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( vol* ` A ) <_ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) -> ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. RR )
22 simpr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( vol* ` A ) <_ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) -> ( vol* ` A ) <_ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) )
23 ovollecl 
 |-  ( ( A C_ RR /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. RR /\ ( vol* ` A ) <_ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) -> ( vol* ` A ) e. RR )
24 16 21 22 23 syl3anc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( vol* ` A ) <_ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) -> ( vol* ` A ) e. RR )
25 simplll 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) ) -> A e. dom vol )
26 20 adantr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) ) -> ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. RR )
27 26 rexrd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) ) -> ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. RR* )
28 simpr 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR )
29 3 ad2antlr 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ x e. RR ) -> B e. RR )
30 29 rexrd 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ x e. RR ) -> B e. RR* )
31 5 ad2antlr 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ x e. RR ) -> 0 <_ B )
32 elxrge0 
 |-  ( B e. ( 0 [,] +oo ) <-> ( B e. RR* /\ 0 <_ B ) )
33 30 31 32 sylanbrc 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ x e. RR ) -> B e. ( 0 [,] +oo ) )
34 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
35 ifcl 
 |-  ( ( B e. ( 0 [,] +oo ) /\ 0 e. ( 0 [,] +oo ) ) -> if ( x e. A , B , 0 ) e. ( 0 [,] +oo ) )
36 33 34 35 sylancl 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ x e. RR ) -> if ( x e. A , B , 0 ) e. ( 0 [,] +oo ) )
37 36 fmpttd 
 |-  ( ( A e. dom vol /\ B e. RR+ ) -> ( x e. RR |-> if ( x e. A , B , 0 ) ) : RR --> ( 0 [,] +oo ) )
38 37 adantr 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( x e. RR |-> if ( x e. A , B , 0 ) ) : RR --> ( 0 [,] +oo ) )
39 itg2ge0 
 |-  ( ( x e. RR |-> if ( x e. A , B , 0 ) ) : RR --> ( 0 [,] +oo ) -> 0 <_ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
40 38 39 syl 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> 0 <_ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
41 28 40 ge0p1rpd 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) e. RR+ )
42 41 19 rpdivcld 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. RR+ )
43 42 rpge0d 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> 0 <_ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) )
44 43 adantr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) ) -> 0 <_ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) )
45 14 breq2d 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol ` A ) <-> ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) ) )
46 45 biimpar 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) ) -> ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol ` A ) )
47 0xr 
 |-  0 e. RR*
48 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
49 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
50 49 ffvelcdmi 
 |-  ( A e. dom vol -> ( vol ` A ) e. ( 0 [,] +oo ) )
51 48 50 sselid 
 |-  ( A e. dom vol -> ( vol ` A ) e. RR* )
52 25 51 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) ) -> ( vol ` A ) e. RR* )
53 elicc1 
 |-  ( ( 0 e. RR* /\ ( vol ` A ) e. RR* ) -> ( ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. ( 0 [,] ( vol ` A ) ) <-> ( ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. RR* /\ 0 <_ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol ` A ) ) ) )
54 47 52 53 sylancr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) ) -> ( ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. ( 0 [,] ( vol ` A ) ) <-> ( ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. RR* /\ 0 <_ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol ` A ) ) ) )
55 27 44 46 54 mpbir3and 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) ) -> ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. ( 0 [,] ( vol ` A ) ) )
56 volivth 
 |-  ( ( A e. dom vol /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. ( 0 [,] ( vol ` A ) ) ) -> E. z e. dom vol ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) )
57 25 55 56 syl2anc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) ) -> E. z e. dom vol ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) )
58 57 ex 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) -> E. z e. dom vol ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) )
59 simprl 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> z e. dom vol )
60 simprrr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) )
61 20 adantr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. RR )
62 60 61 eqeltrd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( vol ` z ) e. RR )
63 3 ad2antlr 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> B e. RR )
64 63 adantr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> B e. RR )
65 19 adantr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> B e. RR+ )
66 65 rpge0d 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> 0 <_ B )
67 64 66 7 sylanbrc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> B e. ( 0 [,) +oo ) )
68 itg2const 
 |-  ( ( z e. dom vol /\ ( vol ` z ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. z , B , 0 ) ) ) = ( B x. ( vol ` z ) ) )
69 59 62 67 68 syl3anc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. z , B , 0 ) ) ) = ( B x. ( vol ` z ) ) )
70 60 oveq2d 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( B x. ( vol ` z ) ) = ( B x. ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) )
71 18 recnd 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) e. CC )
72 63 recnd 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> B e. CC )
73 rpne0 
 |-  ( B e. RR+ -> B =/= 0 )
74 73 ad2antlr 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> B =/= 0 )
75 71 72 74 divcan2d 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( B x. ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) = ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) )
76 75 adantr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( B x. ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) = ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) )
77 69 70 76 3eqtrd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. z , B , 0 ) ) ) = ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) )
78 3 adantl 
 |-  ( ( A e. dom vol /\ B e. RR+ ) -> B e. RR )
79 78 rexrd 
 |-  ( ( A e. dom vol /\ B e. RR+ ) -> B e. RR* )
80 5 adantl 
 |-  ( ( A e. dom vol /\ B e. RR+ ) -> 0 <_ B )
81 79 80 32 sylanbrc 
 |-  ( ( A e. dom vol /\ B e. RR+ ) -> B e. ( 0 [,] +oo ) )
82 ifcl 
 |-  ( ( B e. ( 0 [,] +oo ) /\ 0 e. ( 0 [,] +oo ) ) -> if ( x e. z , B , 0 ) e. ( 0 [,] +oo ) )
83 81 34 82 sylancl 
 |-  ( ( A e. dom vol /\ B e. RR+ ) -> if ( x e. z , B , 0 ) e. ( 0 [,] +oo ) )
84 83 adantr 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ x e. RR ) -> if ( x e. z , B , 0 ) e. ( 0 [,] +oo ) )
85 84 fmpttd 
 |-  ( ( A e. dom vol /\ B e. RR+ ) -> ( x e. RR |-> if ( x e. z , B , 0 ) ) : RR --> ( 0 [,] +oo ) )
86 85 ad2antrr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( x e. RR |-> if ( x e. z , B , 0 ) ) : RR --> ( 0 [,] +oo ) )
87 38 adantr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( x e. RR |-> if ( x e. A , B , 0 ) ) : RR --> ( 0 [,] +oo ) )
88 simpl 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( A e. dom vol /\ B e. RR+ ) )
89 simprl 
 |-  ( ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) -> z C_ A )
90 78 ad3antrrr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ z C_ A ) /\ x e. RR ) /\ x e. z ) -> B e. RR )
91 90 leidd 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ z C_ A ) /\ x e. RR ) /\ x e. z ) -> B <_ B )
92 iftrue 
 |-  ( x e. z -> if ( x e. z , B , 0 ) = B )
93 92 adantl 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ z C_ A ) /\ x e. RR ) /\ x e. z ) -> if ( x e. z , B , 0 ) = B )
94 simplr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ z C_ A ) /\ x e. RR ) -> z C_ A )
95 94 sselda 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ z C_ A ) /\ x e. RR ) /\ x e. z ) -> x e. A )
96 95 iftrued 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ z C_ A ) /\ x e. RR ) /\ x e. z ) -> if ( x e. A , B , 0 ) = B )
97 91 93 96 3brtr4d 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ z C_ A ) /\ x e. RR ) /\ x e. z ) -> if ( x e. z , B , 0 ) <_ if ( x e. A , B , 0 ) )
98 iffalse 
 |-  ( -. x e. z -> if ( x e. z , B , 0 ) = 0 )
99 98 adantl 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ z C_ A ) /\ x e. RR ) /\ -. x e. z ) -> if ( x e. z , B , 0 ) = 0 )
100 0le0 
 |-  0 <_ 0
101 breq2 
 |-  ( B = if ( x e. A , B , 0 ) -> ( 0 <_ B <-> 0 <_ if ( x e. A , B , 0 ) ) )
102 breq2 
 |-  ( 0 = if ( x e. A , B , 0 ) -> ( 0 <_ 0 <-> 0 <_ if ( x e. A , B , 0 ) ) )
103 101 102 ifboth 
 |-  ( ( 0 <_ B /\ 0 <_ 0 ) -> 0 <_ if ( x e. A , B , 0 ) )
104 80 100 103 sylancl 
 |-  ( ( A e. dom vol /\ B e. RR+ ) -> 0 <_ if ( x e. A , B , 0 ) )
105 104 ad3antrrr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ z C_ A ) /\ x e. RR ) /\ -. x e. z ) -> 0 <_ if ( x e. A , B , 0 ) )
106 99 105 eqbrtrd 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ z C_ A ) /\ x e. RR ) /\ -. x e. z ) -> if ( x e. z , B , 0 ) <_ if ( x e. A , B , 0 ) )
107 97 106 pm2.61dan 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ z C_ A ) /\ x e. RR ) -> if ( x e. z , B , 0 ) <_ if ( x e. A , B , 0 ) )
108 107 ralrimiva 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ z C_ A ) -> A. x e. RR if ( x e. z , B , 0 ) <_ if ( x e. A , B , 0 ) )
109 reex 
 |-  RR e. _V
110 109 a1i 
 |-  ( ( A e. dom vol /\ B e. RR+ ) -> RR e. _V )
111 eqidd 
 |-  ( ( A e. dom vol /\ B e. RR+ ) -> ( x e. RR |-> if ( x e. z , B , 0 ) ) = ( x e. RR |-> if ( x e. z , B , 0 ) ) )
112 eqidd 
 |-  ( ( A e. dom vol /\ B e. RR+ ) -> ( x e. RR |-> if ( x e. A , B , 0 ) ) = ( x e. RR |-> if ( x e. A , B , 0 ) ) )
113 110 84 36 111 112 ofrfval2 
 |-  ( ( A e. dom vol /\ B e. RR+ ) -> ( ( x e. RR |-> if ( x e. z , B , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , B , 0 ) ) <-> A. x e. RR if ( x e. z , B , 0 ) <_ if ( x e. A , B , 0 ) ) )
114 113 biimpar 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ A. x e. RR if ( x e. z , B , 0 ) <_ if ( x e. A , B , 0 ) ) -> ( x e. RR |-> if ( x e. z , B , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , B , 0 ) ) )
115 108 114 syldan 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ z C_ A ) -> ( x e. RR |-> if ( x e. z , B , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , B , 0 ) ) )
116 88 89 115 syl2an 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( x e. RR |-> if ( x e. z , B , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , B , 0 ) ) )
117 itg2le 
 |-  ( ( ( x e. RR |-> if ( x e. z , B , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( x e. A , B , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( x e. z , B , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , B , 0 ) ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. z , B , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
118 86 87 116 117 syl3anc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. z , B , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
119 77 118 eqbrtrrd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
120 ltp1 
 |-  ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) < ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) )
121 120 ad2antlr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) < ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) )
122 simplr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR )
123 17 ad2antlr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) e. RR )
124 122 123 ltnled 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) < ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) <-> -. ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) ) )
125 121 124 mpbid 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> -. ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
126 119 125 pm2.21dd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( z e. dom vol /\ ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) ) ) -> ( vol* ` A ) e. RR )
127 126 rexlimdvaa 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( E. z e. dom vol ( z C_ A /\ ( vol ` z ) = ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) ) -> ( vol* ` A ) e. RR ) )
128 58 127 syld 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) -> ( vol* ` A ) e. RR ) )
129 128 imp 
 |-  ( ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) ) -> ( vol* ` A ) e. RR )
130 51 ad2antrr 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( vol ` A ) e. RR* )
131 14 130 eqeltrrd 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( vol* ` A ) e. RR* )
132 20 rexrd 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. RR* )
133 xrletri 
 |-  ( ( ( vol* ` A ) e. RR* /\ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) e. RR* ) -> ( ( vol* ` A ) <_ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) \/ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) ) )
134 131 132 133 syl2anc 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( ( vol* ` A ) <_ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) \/ ( ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + 1 ) / B ) <_ ( vol* ` A ) ) )
135 24 129 134 mpjaodan 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( vol* ` A ) e. RR )
136 14 135 eqeltrd 
 |-  ( ( ( A e. dom vol /\ B e. RR+ ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) -> ( vol ` A ) e. RR )
137 12 136 impbida 
 |-  ( ( A e. dom vol /\ B e. RR+ ) -> ( ( vol ` A ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) )