| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fconstmpt |
⊢ ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
| 2 |
|
mbfconst |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( 𝐴 × { 𝐵 } ) ∈ MblFn ) |
| 3 |
2
|
3adant2 |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 × { 𝐵 } ) ∈ MblFn ) |
| 4 |
1 3
|
eqeltrrid |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) |
| 5 |
|
ifan |
⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) |
| 6 |
5
|
mpteq2i |
⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ) |
| 7 |
6
|
fveq2i |
⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ) ) |
| 8 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 𝐴 ∈ dom vol ) |
| 9 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( vol ‘ 𝐴 ) ∈ ℝ ) |
| 10 |
|
simpl3 |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 𝐵 ∈ ℂ ) |
| 11 |
|
ax-icn |
⊢ i ∈ ℂ |
| 12 |
|
ine0 |
⊢ i ≠ 0 |
| 13 |
|
elfzelz |
⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℤ ) |
| 14 |
13
|
adantl |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 𝑘 ∈ ℤ ) |
| 15 |
|
expclz |
⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ∈ ℂ ) |
| 16 |
11 12 14 15
|
mp3an12i |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( i ↑ 𝑘 ) ∈ ℂ ) |
| 17 |
|
expne0i |
⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ≠ 0 ) |
| 18 |
11 12 14 17
|
mp3an12i |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( i ↑ 𝑘 ) ≠ 0 ) |
| 19 |
10 16 18
|
divcld |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝐵 / ( i ↑ 𝑘 ) ) ∈ ℂ ) |
| 20 |
19
|
recld |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ∈ ℝ ) |
| 21 |
|
0re |
⊢ 0 ∈ ℝ |
| 22 |
|
ifcl |
⊢ ( ( ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ ) |
| 23 |
20 21 22
|
sylancl |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ ) |
| 24 |
|
max1 |
⊢ ( ( 0 ∈ ℝ ∧ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) |
| 25 |
21 20 24
|
sylancr |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) |
| 26 |
|
elrege0 |
⊢ ( if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) ↔ ( if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) |
| 27 |
23 25 26
|
sylanbrc |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) ) |
| 28 |
|
itg2const |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ) ) = ( if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) · ( vol ‘ 𝐴 ) ) ) |
| 29 |
8 9 27 28
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ) ) = ( if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) · ( vol ‘ 𝐴 ) ) ) |
| 30 |
7 29
|
syl5eq |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) · ( vol ‘ 𝐴 ) ) ) |
| 31 |
23 9
|
remulcld |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) · ( vol ‘ 𝐴 ) ) ∈ ℝ ) |
| 32 |
30 31
|
eqeltrd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) |
| 33 |
32
|
ralrimiva |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) |
| 34 |
|
eqidd |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) |
| 35 |
|
eqidd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) |
| 36 |
|
simpl3 |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) |
| 37 |
34 35 36
|
isibl2 |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ) ) |
| 38 |
4 33 37
|
mpbir2and |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ) |
| 39 |
1 38
|
eqeltrid |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 × { 𝐵 } ) ∈ 𝐿1 ) |