This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+ ) → ( ( vol ‘ 𝐴 ) ∈ ℝ ↔ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) ∈ ℝ ) )

Proof

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