| 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
|
ffvelrni |
⊢ ( 𝐴 ∈ 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 ) ) ) ∈ ℝ ) ) |