Step | Hyp | Ref
| Expression |
1 | | fconstmpt 5163 |
. 2
⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
2 | | mbfconst 23402 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ) → (𝐴 × {𝐵}) ∈ MblFn) |
3 | 2 | 3adant2 1080 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (𝐴 ×
{𝐵}) ∈
MblFn) |
4 | 1, 3 | syl5eqelr 2706 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (𝑥 ∈
𝐴 ↦ 𝐵) ∈ MblFn) |
5 | | ifan 4134 |
. . . . . . . 8
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0), 0) |
6 | 5 | mpteq2i 4741 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0), 0)) |
7 | 6 | fveq2i 6194 |
. . . . . 6
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0), 0))) |
8 | | simpl1 1064 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → 𝐴 ∈
dom vol) |
9 | | simpl2 1065 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → (vol‘𝐴) ∈ ℝ) |
10 | | simpl3 1066 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → 𝐵 ∈
ℂ) |
11 | | elfzelz 12342 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℤ) |
12 | 11 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → 𝑘 ∈
ℤ) |
13 | | ax-icn 9995 |
. . . . . . . . . . . . 13
⊢ i ∈
ℂ |
14 | | ine0 10465 |
. . . . . . . . . . . . 13
⊢ i ≠
0 |
15 | | expclz 12885 |
. . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ∈
ℂ) |
16 | 13, 14, 15 | mp3an12 1414 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℤ →
(i↑𝑘) ∈
ℂ) |
17 | 12, 16 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → (i↑𝑘)
∈ ℂ) |
18 | | expne0i 12892 |
. . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ≠ 0) |
19 | 13, 14, 18 | mp3an12 1414 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℤ →
(i↑𝑘) ≠
0) |
20 | 12, 19 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → (i↑𝑘)
≠ 0) |
21 | 10, 17, 20 | divcld 10801 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → (𝐵 /
(i↑𝑘)) ∈
ℂ) |
22 | 21 | recld 13934 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → (ℜ‘(𝐵 / (i↑𝑘))) ∈ ℝ) |
23 | | 0re 10040 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
24 | | ifcl 4130 |
. . . . . . . . 9
⊢
(((ℜ‘(𝐵 /
(i↑𝑘))) ∈ ℝ
∧ 0 ∈ ℝ) → if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ∈ ℝ) |
25 | 22, 23, 24 | sylancl 694 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ∈ ℝ) |
26 | | max1 12016 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ (ℜ‘(𝐵 / (i↑𝑘))) ∈ ℝ) → 0 ≤ if(0 ≤
(ℜ‘(𝐵 /
(i↑𝑘))),
(ℜ‘(𝐵 /
(i↑𝑘))),
0)) |
27 | 23, 22, 26 | sylancr 695 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → 0 ≤ if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) |
28 | | elrege0 12278 |
. . . . . . . 8
⊢ (if(0
≤ (ℜ‘(𝐵 /
(i↑𝑘))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0) ∈
(0[,)+∞) ↔ (if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
(ℜ‘(𝐵 /
(i↑𝑘))),
(ℜ‘(𝐵 /
(i↑𝑘))),
0))) |
29 | 25, 27, 28 | sylanbrc 698 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ∈
(0[,)+∞)) |
30 | | itg2const 23507 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ∈ (0[,)+∞)) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤
(ℜ‘(𝐵 /
(i↑𝑘))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0), 0))) =
(if(0 ≤ (ℜ‘(𝐵
/ (i↑𝑘))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0) ·
(vol‘𝐴))) |
31 | 8, 9, 29, 30 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0), 0))) = (if(0 ≤
(ℜ‘(𝐵 /
(i↑𝑘))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0) ·
(vol‘𝐴))) |
32 | 7, 31 | syl5eq 2668 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) · (vol‘𝐴))) |
33 | 25, 9 | remulcld 10070 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → (if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) · (vol‘𝐴)) ∈ ℝ) |
34 | 32, 33 | eqeltrd 2701 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑘 ∈
(0...3)) → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) |
35 | 34 | ralrimiva 2966 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → ∀𝑘
∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) |
36 | | eqidd 2623 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (𝑥 ∈
ℝ ↦ if((𝑥
∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))),
0))) |
37 | | eqidd 2623 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑥 ∈
𝐴) →
(ℜ‘(𝐵 /
(i↑𝑘))) =
(ℜ‘(𝐵 /
(i↑𝑘)))) |
38 | | simpl3 1066 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑥 ∈
𝐴) → 𝐵 ∈ ℂ) |
39 | 36, 37, 38 | isibl2 23533 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → ((𝑥 ∈
𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ))) |
40 | 4, 35, 39 | mpbir2and 957 |
. 2
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (𝑥 ∈
𝐴 ↦ 𝐵) ∈
𝐿1) |
41 | 1, 40 | syl5eqel 2705 |
1
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (𝐴 ×
{𝐵}) ∈
𝐿1) |