Step | Hyp | Ref
| Expression |
1 | | mbff 23394 |
. . . 4
⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ) |
2 | 1 | feqmptd 6249 |
. . 3
⊢ (𝐹 ∈ MblFn → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧))) |
3 | 2 | 3ad2ant1 1082 |
. 2
⊢ ((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ ∧ ∃𝑥
∈ ℝ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧))) |
4 | | rzal 4073 |
. . . . . . . 8
⊢ (dom
𝐹 = ∅ →
∀𝑧 ∈ dom 𝐹(𝐹‘𝑧) = 0) |
5 | | mpteq12 4736 |
. . . . . . . 8
⊢ ((dom
𝐹 = ∅ ∧
∀𝑧 ∈ dom 𝐹(𝐹‘𝑧) = 0) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) = (𝑧 ∈ ∅ ↦ 0)) |
6 | 4, 5 | mpdan 702 |
. . . . . . 7
⊢ (dom
𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) = (𝑧 ∈ ∅ ↦ 0)) |
7 | | fconstmpt 5163 |
. . . . . . . 8
⊢ (∅
× {0}) = (𝑧 ∈
∅ ↦ 0) |
8 | | 0mbl 23307 |
. . . . . . . . 9
⊢ ∅
∈ dom vol |
9 | | ibl0 23553 |
. . . . . . . . 9
⊢ (∅
∈ dom vol → (∅ × {0}) ∈
𝐿1) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
⊢ (∅
× {0}) ∈ 𝐿1 |
11 | 7, 10 | eqeltrri 2698 |
. . . . . . 7
⊢ (𝑧 ∈ ∅ ↦ 0)
∈ 𝐿1 |
12 | 6, 11 | syl6eqel 2709 |
. . . . . 6
⊢ (dom
𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
13 | 12 | adantl 482 |
. . . . 5
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ (𝑥 ∈
ℝ ∧ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 = ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
14 | | r19.2z 4060 |
. . . . . . . . . 10
⊢ ((dom
𝐹 ≠ ∅ ∧
∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → ∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) |
15 | 14 | anim1i 592 |
. . . . . . . . 9
⊢ (((dom
𝐹 ≠ ∅ ∧
∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑥 ∈ ℝ)) |
16 | 15 | an31s 848 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑥 ∈ ℝ)) |
17 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) → 𝐹:dom 𝐹⟶ℂ) |
18 | 17 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ 𝑦 ∈ dom
𝐹) → (𝐹‘𝑦) ∈ ℂ) |
19 | 18 | absge0d 14183 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ 𝑦 ∈ dom
𝐹) → 0 ≤
(abs‘(𝐹‘𝑦))) |
20 | | 0red 10041 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ 𝑦 ∈ dom
𝐹) → 0 ∈
ℝ) |
21 | 18 | abscld 14175 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ 𝑦 ∈ dom
𝐹) → (abs‘(𝐹‘𝑦)) ∈ ℝ) |
22 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ 𝑦 ∈ dom
𝐹) → 𝑥 ∈
ℝ) |
23 | | letr 10131 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (abs‘(𝐹‘𝑦)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((0 ≤
(abs‘(𝐹‘𝑦)) ∧ (abs‘(𝐹‘𝑦)) ≤ 𝑥) → 0 ≤ 𝑥)) |
24 | 20, 21, 22, 23 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ 𝑦 ∈ dom
𝐹) → ((0 ≤
(abs‘(𝐹‘𝑦)) ∧ (abs‘(𝐹‘𝑦)) ≤ 𝑥) → 0 ≤ 𝑥)) |
25 | 19, 24 | mpand 711 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ 𝑦 ∈ dom
𝐹) →
((abs‘(𝐹‘𝑦)) ≤ 𝑥 → 0 ≤ 𝑥)) |
26 | 25 | rexlimdva 3031 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ 𝑥 ∈
ℝ) → (∃𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → 0 ≤ 𝑥)) |
27 | 26 | ex 450 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) → (𝑥 ∈
ℝ → (∃𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → 0 ≤ 𝑥))) |
28 | 27 | com23 86 |
. . . . . . . . 9
⊢ ((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) → (∃𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → (𝑥 ∈ ℝ → 0 ≤ 𝑥))) |
29 | 28 | imp32 449 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ (∃𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑥 ∈ ℝ)) → 0 ≤ 𝑥) |
30 | 16, 29 | sylan2 491 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅)) → 0 ≤ 𝑥) |
31 | 30 | anassrs 680 |
. . . . . 6
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ (𝑥 ∈
ℝ ∧ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → 0 ≤ 𝑥) |
32 | | an32 839 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) |
33 | | id 22 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ MblFn → 𝐹 ∈ MblFn) |
34 | 2, 33 | eqeltrrd 2702 |
. . . . . . . . . 10
⊢ (𝐹 ∈ MblFn → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ MblFn) |
35 | 34 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ MblFn) |
36 | 1 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝐹:dom 𝐹⟶ℂ) |
37 | 36 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ) |
38 | 37 | recld 13934 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ) |
39 | 38 | rexrd 10089 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈
ℝ*) |
40 | 39 | adantrr 753 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → (ℜ‘(𝐹‘𝑧)) ∈
ℝ*) |
41 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → 0 ≤ (ℜ‘(𝐹‘𝑧))) |
42 | | elxrge0 12281 |
. . . . . . . . . . . . . 14
⊢
((ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔
((ℜ‘(𝐹‘𝑧)) ∈ ℝ* ∧ 0 ≤
(ℜ‘(𝐹‘𝑧)))) |
43 | 40, 41, 42 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → (ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞)) |
44 | | 0e0iccpnf 12283 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
(0[,]+∞) |
45 | 44 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → 0 ∈
(0[,]+∞)) |
46 | 43, 45 | ifclda 4120 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ∈
(0[,]+∞)) |
47 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) |
48 | 46, 47 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)),
0)):ℝ⟶(0[,]+∞)) |
49 | | mbfdm 23395 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
50 | 49 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → dom 𝐹 ∈ dom vol) |
51 | | simplr 792 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (vol‘dom 𝐹) ∈ ℝ) |
52 | | elrege0 12278 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥)) |
53 | 52 | biimpri 218 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → 𝑥 ∈
(0[,)+∞)) |
54 | 53 | ad2antrl 764 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,)+∞)) |
55 | | itg2const 23507 |
. . . . . . . . . . . . 13
⊢ ((dom
𝐹 ∈ dom vol ∧
(vol‘dom 𝐹) ∈
ℝ ∧ 𝑥 ∈
(0[,)+∞)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹))) |
56 | 50, 51, 54, 55 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹))) |
57 | | simprll 802 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ ℝ) |
58 | 57, 51 | remulcld 10070 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑥 · (vol‘dom 𝐹)) ∈ ℝ) |
59 | 56, 58 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ) |
60 | | rexr 10085 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
61 | | elxrge0 12281 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (0[,]+∞) ↔
(𝑥 ∈
ℝ* ∧ 0 ≤ 𝑥)) |
62 | 61 | biimpri 218 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
𝑥 ∈
(0[,]+∞)) |
63 | 60, 62 | sylan 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → 𝑥 ∈
(0[,]+∞)) |
64 | 63 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,]+∞)) |
65 | 64 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝑥 ∈ (0[,]+∞)) |
66 | | ifcl 4130 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (0[,]+∞) ∧ 0
∈ (0[,]+∞)) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞)) |
67 | 65, 44, 66 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞)) |
68 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
69 | 67, 68 | fmptd 6385 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥,
0)):ℝ⟶(0[,]+∞)) |
70 | | ifan 4134 |
. . . . . . . . . . . . . . 15
⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) |
71 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐹:dom 𝐹⟶ℂ) |
72 | 71 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ) |
73 | 72 | recld 13934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ) |
74 | 72 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ∈ ℝ) |
75 | 57 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 𝑥 ∈ ℝ) |
76 | 72 | releabsd 14190 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧))) |
77 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧)) |
78 | 77 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑧 → (abs‘(𝐹‘𝑦)) = (abs‘(𝐹‘𝑧))) |
79 | 78 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑧 → ((abs‘(𝐹‘𝑦)) ≤ 𝑥 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑥)) |
80 | 79 | rspccva 3308 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑦 ∈
dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥) |
81 | 80 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥) |
82 | 81 | adantll 750 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥) |
83 | 73, 74, 75, 76, 82 | letrd 10194 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ≤ 𝑥) |
84 | | simprlr 803 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 0 ≤ 𝑥) |
85 | 84 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 0 ≤ 𝑥) |
86 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((ℜ‘(𝐹‘𝑧)) = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) → ((ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
87 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 = if(0
≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
88 | 86, 87 | ifboth 4124 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
89 | 83, 85, 88 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
90 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0)) |
91 | 90 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0)) |
92 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 𝑥) |
93 | 92 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 𝑥) |
94 | 89, 91, 93 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
95 | 94 | ex 450 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
96 | | 0le0 11110 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ≤
0 |
97 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ dom 𝐹 → 0 ≤
0) |
98 | | iffalse 4095 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) = 0) |
99 | | iffalse 4095 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 0) |
100 | 97, 98, 99 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
101 | 95, 100 | pm2.61d1 171 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
102 | 70, 101 | syl5eqbr 4688 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
103 | 102 | ralrimivw 2967 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
104 | | reex 10027 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ℝ ∈ V) |
106 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) |
107 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
108 | 105, 46, 67, 106, 107 | ofrfval2 6915 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0)) ↔ ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
109 | 103, 108 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
110 | | itg2le 23506 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0))) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
111 | 48, 69, 109, 110 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
112 | | itg2lecl 23505 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) →
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
113 | 48, 59, 111, 112 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
114 | 38 | renegcld 10457 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ) |
115 | 114 | rexrd 10089 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈
ℝ*) |
116 | 115 | adantrr 753 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → -(ℜ‘(𝐹‘𝑧)) ∈
ℝ*) |
117 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → 0 ≤ -(ℜ‘(𝐹‘𝑧))) |
118 | | elxrge0 12281 |
. . . . . . . . . . . . . 14
⊢
(-(ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔
(-(ℜ‘(𝐹‘𝑧)) ∈ ℝ* ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧)))) |
119 | 116, 117,
118 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → -(ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞)) |
120 | 44 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → 0 ∈
(0[,]+∞)) |
121 | 119, 120 | ifclda 4120 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ∈
(0[,]+∞)) |
122 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) |
123 | 121, 122 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)),
0)):ℝ⟶(0[,]+∞)) |
124 | | ifan 4134 |
. . . . . . . . . . . . . . 15
⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) |
125 | 73 | renegcld 10457 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ) |
126 | 73 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℂ) |
127 | 126 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹‘𝑧))) ∈ ℝ) |
128 | 125 | leabsd 14153 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘-(ℜ‘(𝐹‘𝑧)))) |
129 | 126 | absnegd 14188 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℜ‘(𝐹‘𝑧))) = (abs‘(ℜ‘(𝐹‘𝑧)))) |
130 | 128, 129 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘(ℜ‘(𝐹‘𝑧)))) |
131 | | absrele 14048 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑧) ∈ ℂ →
(abs‘(ℜ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧))) |
132 | 72, 131 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧))) |
133 | 125, 127,
74, 130, 132 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧))) |
134 | 125, 74, 75, 133, 82 | letrd 10194 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ 𝑥) |
135 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(-(ℜ‘(𝐹‘𝑧)) = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) → (-(ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
136 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 = if(0
≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
137 | 135, 136 | ifboth 4124 |
. . . . . . . . . . . . . . . . . . 19
⊢
((-(ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
138 | 134, 85, 137 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
139 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0)) |
140 | 139 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0)) |
141 | 138, 140,
93 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
142 | 141 | ex 450 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
143 | | iffalse 4095 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) = 0) |
144 | 97, 143, 99 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
145 | 142, 144 | pm2.61d1 171 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
146 | 124, 145 | syl5eqbr 4688 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
147 | 146 | ralrimivw 2967 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
148 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) |
149 | 105, 121,
67, 148, 107 | ofrfval2 6915 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0)) ↔ ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
150 | 147, 149 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
151 | | itg2le 23506 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0))) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
152 | 123, 69, 150, 151 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
153 | | itg2lecl 23505 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) →
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
154 | 123, 59, 152, 153 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
155 | 113, 154 | jca 554 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ)) |
156 | 37 | imcld 13935 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ) |
157 | 156 | rexrd 10089 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈
ℝ*) |
158 | 157 | adantrr 753 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → (ℑ‘(𝐹‘𝑧)) ∈
ℝ*) |
159 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → 0 ≤ (ℑ‘(𝐹‘𝑧))) |
160 | | elxrge0 12281 |
. . . . . . . . . . . . . 14
⊢
((ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔
((ℑ‘(𝐹‘𝑧)) ∈ ℝ* ∧ 0 ≤
(ℑ‘(𝐹‘𝑧)))) |
161 | 158, 159,
160 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → (ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞)) |
162 | 44 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → 0 ∈
(0[,]+∞)) |
163 | 161, 162 | ifclda 4120 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ∈
(0[,]+∞)) |
164 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) |
165 | 163, 164 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)),
0)):ℝ⟶(0[,]+∞)) |
166 | | ifan 4134 |
. . . . . . . . . . . . . . 15
⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) |
167 | 72 | imcld 13935 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ) |
168 | 167 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℂ) |
169 | 168 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹‘𝑧))) ∈ ℝ) |
170 | 167 | leabsd 14153 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ (abs‘(ℑ‘(𝐹‘𝑧)))) |
171 | | absimle 14049 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑧) ∈ ℂ →
(abs‘(ℑ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧))) |
172 | 72, 171 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧))) |
173 | 167, 169,
74, 170, 172 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧))) |
174 | 167, 74, 75, 173, 82 | letrd 10194 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ 𝑥) |
175 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((ℑ‘(𝐹‘𝑧)) = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) → ((ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
176 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 = if(0
≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
177 | 175, 176 | ifboth 4124 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
178 | 174, 85, 177 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
179 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0)) |
180 | 179 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0)) |
181 | 178, 180,
93 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
182 | 181 | ex 450 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
183 | | iffalse 4095 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) = 0) |
184 | 97, 183, 99 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
185 | 182, 184 | pm2.61d1 171 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
186 | 166, 185 | syl5eqbr 4688 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
187 | 186 | ralrimivw 2967 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
188 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) |
189 | 105, 163,
67, 188, 107 | ofrfval2 6915 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0)) ↔ ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
190 | 187, 189 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
191 | | itg2le 23506 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0))) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
192 | 165, 69, 190, 191 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
193 | | itg2lecl 23505 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) →
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
194 | 165, 59, 192, 193 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
195 | 156 | renegcld 10457 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ) |
196 | 195 | rexrd 10089 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈
ℝ*) |
197 | 196 | adantrr 753 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → -(ℑ‘(𝐹‘𝑧)) ∈
ℝ*) |
198 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → 0 ≤ -(ℑ‘(𝐹‘𝑧))) |
199 | | elxrge0 12281 |
. . . . . . . . . . . . . 14
⊢
(-(ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔
(-(ℑ‘(𝐹‘𝑧)) ∈ ℝ* ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧)))) |
200 | 197, 198,
199 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → -(ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞)) |
201 | 44 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈ MblFn
∧ (vol‘dom 𝐹)
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → 0 ∈
(0[,]+∞)) |
202 | 200, 201 | ifclda 4120 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ∈
(0[,]+∞)) |
203 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) |
204 | 202, 203 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)),
0)):ℝ⟶(0[,]+∞)) |
205 | | ifan 4134 |
. . . . . . . . . . . . . . 15
⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) |
206 | 167 | renegcld 10457 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ) |
207 | 206 | leabsd 14153 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘-(ℑ‘(𝐹‘𝑧)))) |
208 | 168 | absnegd 14188 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℑ‘(𝐹‘𝑧))) = (abs‘(ℑ‘(𝐹‘𝑧)))) |
209 | 207, 208 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘(ℑ‘(𝐹‘𝑧)))) |
210 | 206, 169,
74, 209, 172 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧))) |
211 | 206, 74, 75, 210, 82 | letrd 10194 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ 𝑥) |
212 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(-(ℑ‘(𝐹‘𝑧)) = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) → (-(ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
213 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 = if(0
≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)) |
214 | 212, 213 | ifboth 4124 |
. . . . . . . . . . . . . . . . . . 19
⊢
((-(ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
215 | 211, 85, 214 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥) |
216 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0)) |
217 | 216 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0)) |
218 | 215, 217,
93 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
219 | 218 | ex 450 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
220 | | iffalse 4095 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) = 0) |
221 | 97, 220, 99 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
222 | 219, 221 | pm2.61d1 171 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
223 | 205, 222 | syl5eqbr 4688 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
224 | 223 | ralrimivw 2967 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) |
225 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) |
226 | 105, 202,
67, 225, 107 | ofrfval2 6915 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0)) ↔ ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
227 | 224, 226 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0))) |
228 | | itg2le 23506 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ dom 𝐹, 𝑥, 0))) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
229 | 204, 69, 227, 228 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) |
230 | | itg2lecl 23505 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) →
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
231 | 204, 59, 229, 230 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ) |
232 | 194, 231 | jca 554 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ)) |
233 | | eqid 2622 |
. . . . . . . . . 10
⊢
(∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) |
234 | | eqid 2622 |
. . . . . . . . . 10
⊢
(∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) |
235 | | eqid 2622 |
. . . . . . . . . 10
⊢
(∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
(ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) |
236 | | eqid 2622 |
. . . . . . . . . 10
⊢
(∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦
if((𝑧 ∈ dom 𝐹 ∧ 0 ≤
-(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) |
237 | 233, 234,
235, 236, 72 | iblcnlem1 23554 |
. . . . . . . . 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))) ∈ ℝ)))) |
238 | 35, 155, 232, 237 | mpbir3and 1245 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ 0 ≤ 𝑥)
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
239 | 32, 238 | sylan2b 492 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ ((𝑥 ∈
ℝ ∧ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
240 | 239 | anassrs 680 |
. . . . . 6
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ (𝑥 ∈
ℝ ∧ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 0 ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
241 | 31, 240 | syldan 487 |
. . . . 5
⊢ ((((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ (𝑥 ∈
ℝ ∧ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
242 | 13, 241 | pm2.61dane 2881 |
. . . 4
⊢ (((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) ∧ (𝑥 ∈
ℝ ∧ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
243 | 242 | rexlimdvaa 3032 |
. . 3
⊢ ((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ) → (∃𝑥
∈ ℝ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1)) |
244 | 243 | 3impia 1261 |
. 2
⊢ ((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ ∧ ∃𝑥
∈ ℝ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈
𝐿1) |
245 | 3, 244 | eqeltrd 2701 |
1
⊢ ((𝐹 ∈ MblFn ∧
(vol‘dom 𝐹) ∈
ℝ ∧ ∃𝑥
∈ ℝ ∀𝑦
∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈
𝐿1) |