Step | Hyp | Ref
| Expression |
1 | | mbff 24789 |
. . . 4
⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ) |
2 | 1 | feqmptd 6837 |
. . 3
⊢ (𝐹 ∈ MblFn → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧))) |
3 | 2 | 3ad2ant1 1132 |
. 2
⊢ ((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ ∧ ∃𝑥
∈ ℝ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧))) |
4 | | rzal 4439 |
. . . . . . . 8
⊢ (dom
𝐹 = ∅ →
∀𝑧 ∈ dom 𝐹(𝐹‘𝑧) = 0) |
5 | | mpteq12 5166 |
. . . . . . . 8
⊢ ((dom
𝐹 = ∅ ∧
∀𝑧 ∈ dom 𝐹(𝐹‘𝑧) = 0) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) = (𝑧 ∈ ∅ ↦ 0)) |
6 | 4, 5 | mpdan 684 |
. . . . . . 7
⊢ (dom
𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) = (𝑧 ∈ ∅ ↦ 0)) |
7 | | fconstmpt 5649 |
. . . . . . . 8
⊢ (∅
× {0}) = (𝑧 ∈
∅ ↦ 0) |
8 | | 0mbl 24703 |
. . . . . . . . 9
⊢ ∅
∈ dom vol |
9 | | ibl0 24951 |
. . . . . . . . 9
⊢ (∅
∈ dom vol → (∅ × {0}) ∈
𝐿1) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
⊢ (∅
× {0}) ∈ 𝐿1 |
11 | 7, 10 | eqeltrri 2836 |
. . . . . . 7
⊢ (𝑧 ∈ ∅ ↦ 0)
∈ 𝐿1 |
12 | 6, 11 | eqeltrdi 2847 |
. . . . . 6
⊢ (dom
𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
13 | 12 | adantl 482 |
. . . . 5
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ (𝑥 ∈
ℝ ∧ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 = ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
14 | | r19.2z 4425 |
. . . . . . . . . 10
⊢ ((dom
𝐹 ≠ ∅ ∧
∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → ∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) |
15 | 14 | anim1i 615 |
. . . . . . . . 9
⊢ (((dom
𝐹 ≠ ∅ ∧
∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑥 ∈ ℝ)) |
16 | 15 | an31s 651 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑥 ∈ ℝ)) |
17 | 1 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) → 𝐹:dom 𝐹⟶ℂ) |
18 | 17 | ffvelrnda 6961 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ 𝑦 ∈ dom
𝐹) → (𝐹‘𝑦) ∈ ℂ) |
19 | 18 | absge0d 15156 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ 𝑦 ∈ dom
𝐹) → 0 ≤
(abs‘(𝐹‘𝑦))) |
20 | | 0red 10978 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ 𝑦 ∈ dom
𝐹) → 0 ∈
ℝ) |
21 | 18 | abscld 15148 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ 𝑦 ∈ dom
𝐹) → (abs‘(𝐹‘𝑦)) ∈ ℝ) |
22 | | simplr 766 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ 𝑦 ∈ dom
𝐹) → 𝑥 ∈
ℝ) |
23 | | letr 11069 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (abs‘(𝐹‘𝑦)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((0 ≤
(abs‘(𝐹‘𝑦)) ∧ (abs‘(𝐹‘𝑦)) ≤ 𝑥) → 0 ≤ 𝑥)) |
24 | 20, 21, 22, 23 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ 𝑦 ∈ dom
𝐹) → ((0 ≤
(abs‘(𝐹‘𝑦)) ∧ (abs‘(𝐹‘𝑦)) ≤ 𝑥) → 0 ≤ 𝑥)) |
25 | 19, 24 | mpand 692 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ 𝑦 ∈ dom
𝐹) →
((abs‘(𝐹‘𝑦)) ≤ 𝑥 → 0 ≤ 𝑥)) |
26 | 25 | rexlimdva 3213 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) → (∃𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → 0 ≤ 𝑥)) |
27 | 26 | ex 413 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) → (𝑥 ∈
ℝ → (∃𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → 0 ≤ 𝑥))) |
28 | 27 | com23 86 |
. . . . . . . . 9
⊢ ((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) → (∃𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → (𝑥 ∈ ℝ → 0 ≤ 𝑥))) |
29 | 28 | imp32 419 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ (∃𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑥 ∈ ℝ)) → 0 ≤ 𝑥) |
30 | 16, 29 | sylan2 593 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅)) → 0 ≤ 𝑥) |
31 | 30 | anassrs 468 |
. . . . . 6
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ (𝑥 ∈
ℝ ∧ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → 0 ≤ 𝑥) |
32 | | an32 643 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) |
33 | | id 22 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ MblFn → 𝐹 ∈ MblFn) |
34 | 2, 33 | eqeltrrd 2840 |
. . . . . . . . . 10
⊢ (𝐹 ∈ MblFn → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ MblFn) |
35 | 34 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ MblFn) |
36 | 1 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝐹:dom 𝐹⟶ℂ) |
37 | 36 | ffvelrnda 6961 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ) |
38 | 37 | recld 14905 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ) |
39 | 38 | rexrd 11025 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈
ℝ*) |
40 | 39 | adantrr 714 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → (ℜ‘(𝐹‘𝑧)) ∈
ℝ*) |
41 | | simprr 770 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → 0 ≤ (ℜ‘(𝐹‘𝑧))) |
42 | | elxrge0 13189 |
. . . . . . . . . . . . . 14
⊢
((ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔
((ℜ‘(𝐹‘𝑧)) ∈ ℝ* ∧ 0 ≤
(ℜ‘(𝐹‘𝑧)))) |
43 | 40, 41, 42 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → (ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞)) |
44 | | 0e0iccpnf 13191 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
(0[,]+∞) |
45 | 44 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → 0 ∈
(0[,]+∞)) |
46 | 43, 45 | ifclda 4494 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ∈
(0[,]+∞)) |
47 | 46 | fmpttd 6989 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)),
0)):ℝ⟶(0[,]+∞)) |
48 | | mbfdm 24790 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
49 | 48 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → dom 𝐹 ∈ dom vol) |
50 | | simplr 766 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (vol‘dom 𝐹) ∈ ℝ) |
51 | | elrege0 13186 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥)) |
52 | 51 | biimpri 227 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → 𝑥 ∈
(0[,)+∞)) |
53 | 52 | ad2antrl 725 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,)+∞)) |
54 | | itg2const 24905 |
. . . . . . . . . . . . 13
⊢ ((dom
𝐹 ∈ dom vol ∧
(vol‘dom 𝐹) ∈
ℝ ∧ 𝑥 ∈
(0[,)+∞)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹))) |
55 | 49, 50, 53, 54 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹))) |
56 | | simprll 776 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ ℝ) |
57 | 56, 50 | remulcld 11005 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑥 · (vol‘dom 𝐹)) ∈ ℝ) |
58 | 55, 57 | eqeltrd 2839 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ) |
59 | | rexr 11021 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
60 | | elxrge0 13189 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (0[,]+∞) ↔
(𝑥 ∈
ℝ* ∧ 0 ≤ 𝑥)) |
61 | 60 | biimpri 227 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
𝑥 ∈
(0[,]+∞)) |
62 | 59, 61 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → 𝑥 ∈
(0[,]+∞)) |
63 | 62 | ad2antrl 725 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,]+∞)) |
64 | 63 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝑥 ∈ (0[,]+∞)) |
65 | | ifcl 4504 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (0[,]+∞) ∧ 0
∈ (0[,]+∞)) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞)) |
66 | 64, 44, 65 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞)) |
67 | 66 | fmpttd 6989 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥,
0)):ℝ⟶(0[,]+∞)) |
68 | | ifan 4512 |
. . . . . . . . . . . . . . 15
⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) |
69 | 1 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐹:dom 𝐹⟶ℂ) |
70 | 69 | ffvelrnda 6961 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ) |
71 | 70 | recld 14905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ) |
72 | 70 | abscld 15148 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ∈ ℝ) |
73 | 56 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 𝑥 ∈ ℝ) |
74 | 70 | releabsd 15163 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧))) |
75 | | 2fveq3 6779 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑧 → (abs‘(𝐹‘𝑦)) = (abs‘(𝐹‘𝑧))) |
76 | 75 | breq1d 5084 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑧 → ((abs‘(𝐹‘𝑦)) ≤ 𝑥 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑥)) |
77 | 76 | rspccva 3560 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑦 ∈
dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥) |
78 | 77 | adantll 711 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥) |
79 | 78 | adantll 711 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥) |
80 | 71, 72, 73, 74, 79 | letrd 11132 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ≤ 𝑥) |
81 | | simprlr 777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 0 ≤ 𝑥) |
82 | 81 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 0 ≤ 𝑥) |
83 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((ℜ‘(𝐹‘𝑧)) = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) → ((ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
84 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 = if(0
≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
85 | 83, 84 | ifboth 4498 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
86 | 80, 82, 85 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
87 | | iftrue 4465 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0)) |
88 | 87 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0)) |
89 | | iftrue 4465 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 𝑥) |
90 | 89 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 𝑥) |
91 | 86, 88, 90 | 3brtr4d 5106 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
92 | 91 | ex 413 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
93 | | 0le0 12074 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ≤
0 |
94 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ dom 𝐹 → 0 ≤
0) |
95 | | iffalse 4468 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) = 0) |
96 | | iffalse 4468 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 0) |
97 | 94, 95, 96 | 3brtr4d 5106 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
98 | 92, 97 | pm2.61d1 180 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
99 | 68, 98 | eqbrtrid 5109 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
100 | 99 | ralrimivw 3104 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
101 | | reex 10962 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
102 | 101 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ℝ ∈ V) |
103 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) |
104 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
105 | 102, 46, 66, 103, 104 | ofrfval2 7554 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) ∘r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) ↔ ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
106 | 100, 105 | mpbird 256 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) ∘r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
107 | | itg2le 24904 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) ∘r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
108 | 47, 67, 106, 107 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
109 | | itg2lecl 24903 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) →
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
110 | 47, 58, 108, 109 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
111 | 38 | renegcld 11402 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ) |
112 | 111 | rexrd 11025 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈
ℝ*) |
113 | 112 | adantrr 714 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → -(ℜ‘(𝐹‘𝑧)) ∈
ℝ*) |
114 | | simprr 770 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → 0 ≤ -(ℜ‘(𝐹‘𝑧))) |
115 | | elxrge0 13189 |
. . . . . . . . . . . . . 14
⊢
(-(ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔
(-(ℜ‘(𝐹‘𝑧)) ∈ ℝ* ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧)))) |
116 | 113, 114,
115 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → -(ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞)) |
117 | 44 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → 0 ∈
(0[,]+∞)) |
118 | 116, 117 | ifclda 4494 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ∈
(0[,]+∞)) |
119 | 118 | fmpttd 6989 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)),
0)):ℝ⟶(0[,]+∞)) |
120 | | ifan 4512 |
. . . . . . . . . . . . . . 15
⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) |
121 | 71 | renegcld 11402 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ) |
122 | 71 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℂ) |
123 | 122 | abscld 15148 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹‘𝑧))) ∈ ℝ) |
124 | 121 | leabsd 15126 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘-(ℜ‘(𝐹‘𝑧)))) |
125 | 122 | absnegd 15161 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℜ‘(𝐹‘𝑧))) = (abs‘(ℜ‘(𝐹‘𝑧)))) |
126 | 124, 125 | breqtrd 5100 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘(ℜ‘(𝐹‘𝑧)))) |
127 | | absrele 15020 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑧) ∈ ℂ →
(abs‘(ℜ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧))) |
128 | 70, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧))) |
129 | 121, 123,
72, 126, 128 | letrd 11132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧))) |
130 | 121, 72, 73, 129, 79 | letrd 11132 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ 𝑥) |
131 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(-(ℜ‘(𝐹‘𝑧)) = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) → (-(ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
132 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 = if(0
≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
133 | 131, 132 | ifboth 4498 |
. . . . . . . . . . . . . . . . . . 19
⊢
((-(ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
134 | 130, 82, 133 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
135 | | iftrue 4465 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0)) |
136 | 135 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0)) |
137 | 134, 136,
90 | 3brtr4d 5106 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
138 | 137 | ex 413 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
139 | | iffalse 4468 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) = 0) |
140 | 94, 139, 96 | 3brtr4d 5106 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
141 | 138, 140 | pm2.61d1 180 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
142 | 120, 141 | eqbrtrid 5109 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
143 | 142 | ralrimivw 3104 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
144 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) |
145 | 102, 118,
66, 144, 104 | ofrfval2 7554 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) ∘r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) ↔ ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
146 | 143, 145 | mpbird 256 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) ∘r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
147 | | itg2le 24904 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) ∘r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
148 | 119, 67, 146, 147 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
149 | | itg2lecl 24903 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) →
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
150 | 119, 58, 148, 149 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
151 | 110, 150 | jca 512 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ)) |
152 | 37 | imcld 14906 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ) |
153 | 152 | rexrd 11025 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈
ℝ*) |
154 | 153 | adantrr 714 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → (ℑ‘(𝐹‘𝑧)) ∈
ℝ*) |
155 | | simprr 770 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → 0 ≤ (ℑ‘(𝐹‘𝑧))) |
156 | | elxrge0 13189 |
. . . . . . . . . . . . . 14
⊢
((ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔
((ℑ‘(𝐹‘𝑧)) ∈ ℝ* ∧ 0 ≤
(ℑ‘(𝐹‘𝑧)))) |
157 | 154, 155,
156 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → (ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞)) |
158 | 44 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → 0 ∈
(0[,]+∞)) |
159 | 157, 158 | ifclda 4494 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ∈
(0[,]+∞)) |
160 | 159 | fmpttd 6989 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)),
0)):ℝ⟶(0[,]+∞)) |
161 | | ifan 4512 |
. . . . . . . . . . . . . . 15
⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) |
162 | 70 | imcld 14906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ) |
163 | 162 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℂ) |
164 | 163 | abscld 15148 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹‘𝑧))) ∈ ℝ) |
165 | 162 | leabsd 15126 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ (abs‘(ℑ‘(𝐹‘𝑧)))) |
166 | | absimle 15021 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑧) ∈ ℂ →
(abs‘(ℑ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧))) |
167 | 70, 166 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧))) |
168 | 162, 164,
72, 165, 167 | letrd 11132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧))) |
169 | 162, 72, 73, 168, 79 | letrd 11132 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ 𝑥) |
170 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((ℑ‘(𝐹‘𝑧)) = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) → ((ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
171 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 = if(0
≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
172 | 170, 171 | ifboth 4498 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
173 | 169, 82, 172 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
174 | | iftrue 4465 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0)) |
175 | 174 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0)) |
176 | 173, 175,
90 | 3brtr4d 5106 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
177 | 176 | ex 413 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
178 | | iffalse 4468 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) = 0) |
179 | 94, 178, 96 | 3brtr4d 5106 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
180 | 177, 179 | pm2.61d1 180 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
181 | 161, 180 | eqbrtrid 5109 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
182 | 181 | ralrimivw 3104 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
183 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) |
184 | 102, 159,
66, 183, 104 | ofrfval2 7554 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) ∘r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) ↔ ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
185 | 182, 184 | mpbird 256 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) ∘r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
186 | | itg2le 24904 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) ∘r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
187 | 160, 67, 185, 186 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
188 | | itg2lecl 24903 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) →
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
189 | 160, 58, 187, 188 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
190 | 152 | renegcld 11402 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ) |
191 | 190 | rexrd 11025 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈
ℝ*) |
192 | 191 | adantrr 714 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → -(ℑ‘(𝐹‘𝑧)) ∈
ℝ*) |
193 | | simprr 770 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → 0 ≤ -(ℑ‘(𝐹‘𝑧))) |
194 | | elxrge0 13189 |
. . . . . . . . . . . . . 14
⊢
(-(ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔
(-(ℑ‘(𝐹‘𝑧)) ∈ ℝ* ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧)))) |
195 | 192, 193,
194 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → -(ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞)) |
196 | 44 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → 0 ∈
(0[,]+∞)) |
197 | 195, 196 | ifclda 4494 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ∈
(0[,]+∞)) |
198 | 197 | fmpttd 6989 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)),
0)):ℝ⟶(0[,]+∞)) |
199 | | ifan 4512 |
. . . . . . . . . . . . . . 15
⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) |
200 | 162 | renegcld 11402 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ) |
201 | 200 | leabsd 15126 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘-(ℑ‘(𝐹‘𝑧)))) |
202 | 163 | absnegd 15161 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℑ‘(𝐹‘𝑧))) = (abs‘(ℑ‘(𝐹‘𝑧)))) |
203 | 201, 202 | breqtrd 5100 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘(ℑ‘(𝐹‘𝑧)))) |
204 | 200, 164,
72, 203, 167 | letrd 11132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧))) |
205 | 200, 72, 73, 204, 79 | letrd 11132 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ 𝑥) |
206 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(-(ℑ‘(𝐹‘𝑧)) = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) → (-(ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
207 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 = if(0
≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
208 | 206, 207 | ifboth 4498 |
. . . . . . . . . . . . . . . . . . 19
⊢
((-(ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
209 | 205, 82, 208 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
210 | | iftrue 4465 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0)) |
211 | 210 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0)) |
212 | 209, 211,
90 | 3brtr4d 5106 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
213 | 212 | ex 413 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
214 | | iffalse 4468 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) = 0) |
215 | 94, 214, 96 | 3brtr4d 5106 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
216 | 213, 215 | pm2.61d1 180 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
217 | 199, 216 | eqbrtrid 5109 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
218 | 217 | ralrimivw 3104 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
219 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) |
220 | 102, 197,
66, 219, 104 | ofrfval2 7554 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) ∘r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) ↔ ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
221 | 218, 220 | mpbird 256 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) ∘r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
222 | | itg2le 24904 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) ∘r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
223 | 198, 67, 221, 222 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
224 | | itg2lecl 24903 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) →
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
225 | 198, 58, 223, 224 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
226 | 189, 225 | jca 512 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ)) |
227 | | eqid 2738 |
. . . . . . . . . 10
⊢
(∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) |
228 | | eqid 2738 |
. . . . . . . . . 10
⊢
(∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) |
229 | | eqid 2738 |
. . . . . . . . . 10
⊢
(∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) |
230 | | eqid 2738 |
. . . . . . . . . 10
⊢
(∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) |
231 | 227, 228,
229, 230, 70 | iblcnlem1 24952 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿1 ↔
((𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ MblFn ∧
((∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ) ∧
((∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ)))) |
232 | 35, 151, 226, 231 | mpbir3and 1341 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
233 | 32, 232 | sylan2b 594 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
234 | 233 | anassrs 468 |
. . . . . 6
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ (𝑥 ∈
ℝ ∧ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 0 ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
235 | 31, 234 | syldan 591 |
. . . . 5
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ (𝑥 ∈
ℝ ∧ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
236 | 13, 235 | pm2.61dane 3032 |
. . . 4
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ (𝑥 ∈
ℝ ∧ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
237 | 236 | rexlimdvaa 3214 |
. . 3
⊢ ((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) → (∃𝑥
∈ ℝ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1)) |
238 | 237 | 3impia 1116 |
. 2
⊢ ((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ ∧ ∃𝑥
∈ ℝ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
239 | 3, 238 | eqeltrd 2839 |
1
⊢ ((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ ∧ ∃𝑥
∈ ℝ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈
𝐿1) |