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 AdomvolB+volA2xifxAB0

Proof

Step Hyp Ref Expression
1 simpll AdomvolB+volAAdomvol
2 simpr AdomvolB+volAvolA
3 rpre B+B
4 3 ad2antlr AdomvolB+volAB
5 rpge0 B+0B
6 5 ad2antlr AdomvolB+volA0B
7 elrege0 B0+∞B0B
8 4 6 7 sylanbrc AdomvolB+volAB0+∞
9 itg2const AdomvolvolAB0+∞2xifxAB0=BvolA
10 1 2 8 9 syl3anc AdomvolB+volA2xifxAB0=BvolA
11 4 2 remulcld AdomvolB+volABvolA
12 10 11 eqeltrd AdomvolB+volA2xifxAB0
13 mblvol AdomvolvolA=vol*A
14 13 ad2antrr AdomvolB+2xifxAB0volA=vol*A
15 mblss AdomvolA
16 15 ad3antrrr AdomvolB+2xifxAB0vol*A2xifxAB0+1BA
17 peano2re 2xifxAB02xifxAB0+1
18 17 adantl AdomvolB+2xifxAB02xifxAB0+1
19 simplr AdomvolB+2xifxAB0B+
20 18 19 rerpdivcld AdomvolB+2xifxAB02xifxAB0+1B
21 20 adantr AdomvolB+2xifxAB0vol*A2xifxAB0+1B2xifxAB0+1B
22 simpr AdomvolB+2xifxAB0vol*A2xifxAB0+1Bvol*A2xifxAB0+1B
23 ovollecl A2xifxAB0+1Bvol*A2xifxAB0+1Bvol*A
24 16 21 22 23 syl3anc AdomvolB+2xifxAB0vol*A2xifxAB0+1Bvol*A
25 simplll AdomvolB+2xifxAB02xifxAB0+1Bvol*AAdomvol
26 20 adantr AdomvolB+2xifxAB02xifxAB0+1Bvol*A2xifxAB0+1B
27 26 rexrd AdomvolB+2xifxAB02xifxAB0+1Bvol*A2xifxAB0+1B*
28 simpr AdomvolB+2xifxAB02xifxAB0
29 3 ad2antlr AdomvolB+xB
30 29 rexrd AdomvolB+xB*
31 5 ad2antlr AdomvolB+x0B
32 elxrge0 B0+∞B*0B
33 30 31 32 sylanbrc AdomvolB+xB0+∞
34 0e0iccpnf 00+∞
35 ifcl B0+∞00+∞ifxAB00+∞
36 33 34 35 sylancl AdomvolB+xifxAB00+∞
37 36 fmpttd AdomvolB+xifxAB0:0+∞
38 37 adantr AdomvolB+2xifxAB0xifxAB0:0+∞
39 itg2ge0 xifxAB0:0+∞02xifxAB0
40 38 39 syl AdomvolB+2xifxAB002xifxAB0
41 28 40 ge0p1rpd AdomvolB+2xifxAB02xifxAB0+1+
42 41 19 rpdivcld AdomvolB+2xifxAB02xifxAB0+1B+
43 42 rpge0d AdomvolB+2xifxAB002xifxAB0+1B
44 43 adantr AdomvolB+2xifxAB02xifxAB0+1Bvol*A02xifxAB0+1B
45 14 breq2d AdomvolB+2xifxAB02xifxAB0+1BvolA2xifxAB0+1Bvol*A
46 45 biimpar AdomvolB+2xifxAB02xifxAB0+1Bvol*A2xifxAB0+1BvolA
47 0xr 0*
48 iccssxr 0+∞*
49 volf vol:domvol0+∞
50 49 ffvelrni AdomvolvolA0+∞
51 48 50 sselid AdomvolvolA*
52 25 51 syl AdomvolB+2xifxAB02xifxAB0+1Bvol*AvolA*
53 elicc1 0*volA*2xifxAB0+1B0volA2xifxAB0+1B*02xifxAB0+1B2xifxAB0+1BvolA
54 47 52 53 sylancr AdomvolB+2xifxAB02xifxAB0+1Bvol*A2xifxAB0+1B0volA2xifxAB0+1B*02xifxAB0+1B2xifxAB0+1BvolA
55 27 44 46 54 mpbir3and AdomvolB+2xifxAB02xifxAB0+1Bvol*A2xifxAB0+1B0volA
56 volivth Adomvol2xifxAB0+1B0volAzdomvolzAvolz=2xifxAB0+1B
57 25 55 56 syl2anc AdomvolB+2xifxAB02xifxAB0+1Bvol*AzdomvolzAvolz=2xifxAB0+1B
58 57 ex AdomvolB+2xifxAB02xifxAB0+1Bvol*AzdomvolzAvolz=2xifxAB0+1B
59 simprl AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1Bzdomvol
60 simprrr AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1Bvolz=2xifxAB0+1B
61 20 adantr AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1B2xifxAB0+1B
62 60 61 eqeltrd AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1Bvolz
63 3 ad2antlr AdomvolB+2xifxAB0B
64 63 adantr AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1BB
65 19 adantr AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1BB+
66 65 rpge0d AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1B0B
67 64 66 7 sylanbrc AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1BB0+∞
68 itg2const zdomvolvolzB0+∞2xifxzB0=Bvolz
69 59 62 67 68 syl3anc AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1B2xifxzB0=Bvolz
70 60 oveq2d AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1BBvolz=B2xifxAB0+1B
71 18 recnd AdomvolB+2xifxAB02xifxAB0+1
72 63 recnd AdomvolB+2xifxAB0B
73 rpne0 B+B0
74 73 ad2antlr AdomvolB+2xifxAB0B0
75 71 72 74 divcan2d AdomvolB+2xifxAB0B2xifxAB0+1B=2xifxAB0+1
76 75 adantr AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1BB2xifxAB0+1B=2xifxAB0+1
77 69 70 76 3eqtrd AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1B2xifxzB0=2xifxAB0+1
78 3 adantl AdomvolB+B
79 78 rexrd AdomvolB+B*
80 5 adantl AdomvolB+0B
81 79 80 32 sylanbrc AdomvolB+B0+∞
82 ifcl B0+∞00+∞ifxzB00+∞
83 81 34 82 sylancl AdomvolB+ifxzB00+∞
84 83 adantr AdomvolB+xifxzB00+∞
85 84 fmpttd AdomvolB+xifxzB0:0+∞
86 85 ad2antrr AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1BxifxzB0:0+∞
87 38 adantr AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1BxifxAB0:0+∞
88 simpl AdomvolB+2xifxAB0AdomvolB+
89 simprl zdomvolzAvolz=2xifxAB0+1BzA
90 78 ad3antrrr AdomvolB+zAxxzB
91 90 leidd AdomvolB+zAxxzBB
92 iftrue xzifxzB0=B
93 92 adantl AdomvolB+zAxxzifxzB0=B
94 simplr AdomvolB+zAxzA
95 94 sselda AdomvolB+zAxxzxA
96 95 iftrued AdomvolB+zAxxzifxAB0=B
97 91 93 96 3brtr4d AdomvolB+zAxxzifxzB0ifxAB0
98 iffalse ¬xzifxzB0=0
99 98 adantl AdomvolB+zAx¬xzifxzB0=0
100 0le0 00
101 breq2 B=ifxAB00B0ifxAB0
102 breq2 0=ifxAB0000ifxAB0
103 101 102 ifboth 0B000ifxAB0
104 80 100 103 sylancl AdomvolB+0ifxAB0
105 104 ad3antrrr AdomvolB+zAx¬xz0ifxAB0
106 99 105 eqbrtrd AdomvolB+zAx¬xzifxzB0ifxAB0
107 97 106 pm2.61dan AdomvolB+zAxifxzB0ifxAB0
108 107 ralrimiva AdomvolB+zAxifxzB0ifxAB0
109 reex V
110 109 a1i AdomvolB+V
111 eqidd AdomvolB+xifxzB0=xifxzB0
112 eqidd AdomvolB+xifxAB0=xifxAB0
113 110 84 36 111 112 ofrfval2 AdomvolB+xifxzB0fxifxAB0xifxzB0ifxAB0
114 113 biimpar AdomvolB+xifxzB0ifxAB0xifxzB0fxifxAB0
115 108 114 syldan AdomvolB+zAxifxzB0fxifxAB0
116 88 89 115 syl2an AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1BxifxzB0fxifxAB0
117 itg2le xifxzB0:0+∞xifxAB0:0+∞xifxzB0fxifxAB02xifxzB02xifxAB0
118 86 87 116 117 syl3anc AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1B2xifxzB02xifxAB0
119 77 118 eqbrtrrd AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1B2xifxAB0+12xifxAB0
120 ltp1 2xifxAB02xifxAB0<2xifxAB0+1
121 120 ad2antlr AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1B2xifxAB0<2xifxAB0+1
122 simplr AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1B2xifxAB0
123 17 ad2antlr AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1B2xifxAB0+1
124 122 123 ltnled AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1B2xifxAB0<2xifxAB0+1¬2xifxAB0+12xifxAB0
125 121 124 mpbid AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1B¬2xifxAB0+12xifxAB0
126 119 125 pm2.21dd AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1Bvol*A
127 126 rexlimdvaa AdomvolB+2xifxAB0zdomvolzAvolz=2xifxAB0+1Bvol*A
128 58 127 syld AdomvolB+2xifxAB02xifxAB0+1Bvol*Avol*A
129 128 imp AdomvolB+2xifxAB02xifxAB0+1Bvol*Avol*A
130 51 ad2antrr AdomvolB+2xifxAB0volA*
131 14 130 eqeltrrd AdomvolB+2xifxAB0vol*A*
132 20 rexrd AdomvolB+2xifxAB02xifxAB0+1B*
133 xrletri vol*A*2xifxAB0+1B*vol*A2xifxAB0+1B2xifxAB0+1Bvol*A
134 131 132 133 syl2anc AdomvolB+2xifxAB0vol*A2xifxAB0+1B2xifxAB0+1Bvol*A
135 24 129 134 mpjaodan AdomvolB+2xifxAB0vol*A
136 14 135 eqeltrd AdomvolB+2xifxAB0volA
137 12 136 impbida AdomvolB+volA2xifxAB0