Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bddiblnc Structured version   Visualization version   GIF version

Theorem bddiblnc 33610
Description: Choice-free proof of bddibl 23651. (Contributed by Brendan Leahy, 2-Nov-2017.) (Revised by Brendan Leahy, 6-Nov-2017.)
Assertion
Ref Expression
bddiblnc ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿1)
Distinct variable group:   𝑥,𝑦,𝐹

Proof of Theorem bddiblnc
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 mbff 23439 . . . 4 (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ)
21feqmptd 6288 . . 3 (𝐹 ∈ MblFn → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)))
323ad2ant1 1102 . 2 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)))
4 rzal 4106 . . . . . . . 8 (dom 𝐹 = ∅ → ∀𝑧 ∈ dom 𝐹(𝐹𝑧) = 0)
5 mpteq12 4769 . . . . . . . 8 ((dom 𝐹 = ∅ ∧ ∀𝑧 ∈ dom 𝐹(𝐹𝑧) = 0) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) = (𝑧 ∈ ∅ ↦ 0))
64, 5mpdan 703 . . . . . . 7 (dom 𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) = (𝑧 ∈ ∅ ↦ 0))
7 fconstmpt 5197 . . . . . . . 8 (∅ × {0}) = (𝑧 ∈ ∅ ↦ 0)
8 0mbl 23353 . . . . . . . . 9 ∅ ∈ dom vol
9 ibl0 23598 . . . . . . . . 9 (∅ ∈ dom vol → (∅ × {0}) ∈ 𝐿1)
108, 9ax-mp 5 . . . . . . . 8 (∅ × {0}) ∈ 𝐿1
117, 10eqeltrri 2727 . . . . . . 7 (𝑧 ∈ ∅ ↦ 0) ∈ 𝐿1
126, 11syl6eqel 2738 . . . . . 6 (dom 𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
1312adantl 481 . . . . 5 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ dom 𝐹 = ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
14 r19.2z 4093 . . . . . . . . . 10 ((dom 𝐹 ≠ ∅ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) → ∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)
1514anim1i 591 . . . . . . . . 9 (((dom 𝐹 ≠ ∅ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥𝑥 ∈ ℝ))
1615an31s 865 . . . . . . . 8 (((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥𝑥 ∈ ℝ))
171ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝐹:dom 𝐹⟶ℂ)
1817ffvelrnda 6399 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → (𝐹𝑦) ∈ ℂ)
1918absge0d 14227 . . . . . . . . . . . . 13 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 0 ≤ (abs‘(𝐹𝑦)))
20 0red 10079 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 0 ∈ ℝ)
2118abscld 14219 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → (abs‘(𝐹𝑦)) ∈ ℝ)
22 simplr 807 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
23 letr 10169 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ (abs‘(𝐹𝑦)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((0 ≤ (abs‘(𝐹𝑦)) ∧ (abs‘(𝐹𝑦)) ≤ 𝑥) → 0 ≤ 𝑥))
2420, 21, 22, 23syl3anc 1366 . . . . . . . . . . . . 13 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → ((0 ≤ (abs‘(𝐹𝑦)) ∧ (abs‘(𝐹𝑦)) ≤ 𝑥) → 0 ≤ 𝑥))
2519, 24mpand 711 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → ((abs‘(𝐹𝑦)) ≤ 𝑥 → 0 ≤ 𝑥))
2625rexlimdva 3060 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥 → 0 ≤ 𝑥))
2726ex 449 . . . . . . . . . 10 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (𝑥 ∈ ℝ → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥 → 0 ≤ 𝑥)))
2827com23 86 . . . . . . . . 9 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥 → (𝑥 ∈ ℝ → 0 ≤ 𝑥)))
2928imp32 448 . . . . . . . 8 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥𝑥 ∈ ℝ)) → 0 ≤ 𝑥)
3016, 29sylan2 490 . . . . . . 7 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅)) → 0 ≤ 𝑥)
3130anassrs 681 . . . . . 6 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → 0 ≤ 𝑥)
32 an32 856 . . . . . . . 8 (((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥))
33 id 22 . . . . . . . . . . 11 (𝐹 ∈ MblFn → 𝐹 ∈ MblFn)
342, 33eqeltrrd 2731 . . . . . . . . . 10 (𝐹 ∈ MblFn → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ MblFn)
3534ad2antrr 762 . . . . . . . . 9 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ MblFn)
361ad3antrrr 766 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝐹:dom 𝐹⟶ℂ)
3736ffvelrnda 6399 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (𝐹𝑧) ∈ ℂ)
3837recld 13978 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ∈ ℝ)
3938rexrd 10127 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ∈ ℝ*)
4039adantrr 753 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧)))) → (ℜ‘(𝐹𝑧)) ∈ ℝ*)
41 simprr 811 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧)))) → 0 ≤ (ℜ‘(𝐹𝑧)))
42 elxrge0 12319 . . . . . . . . . . . . . 14 ((ℜ‘(𝐹𝑧)) ∈ (0[,]+∞) ↔ ((ℜ‘(𝐹𝑧)) ∈ ℝ* ∧ 0 ≤ (ℜ‘(𝐹𝑧))))
4340, 41, 42sylanbrc 699 . . . . . . . . . . . . 13 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧)))) → (ℜ‘(𝐹𝑧)) ∈ (0[,]+∞))
44 0e0iccpnf 12321 . . . . . . . . . . . . . 14 0 ∈ (0[,]+∞)
4544a1i 11 . . . . . . . . . . . . 13 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧)))) → 0 ∈ (0[,]+∞))
4643, 45ifclda 4153 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0) ∈ (0[,]+∞))
47 eqid 2651 . . . . . . . . . . . 12 (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))
4846, 47fmptd 6425 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞))
49 mbfdm 23440 . . . . . . . . . . . . . 14 (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
5049ad2antrr 762 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → dom 𝐹 ∈ dom vol)
51 simplr 807 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (vol‘dom 𝐹) ∈ ℝ)
52 elrege0 12316 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
5352biimpri 218 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,)+∞))
5453ad2antrl 764 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,)+∞))
55 itg2const 23552 . . . . . . . . . . . . 13 ((dom 𝐹 ∈ dom vol ∧ (vol‘dom 𝐹) ∈ ℝ ∧ 𝑥 ∈ (0[,)+∞)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹)))
5650, 51, 54, 55syl3anc 1366 . . . . . . . . . . . 12 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹)))
57 simprll 819 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 𝑥 ∈ ℝ)
5857, 51remulcld 10108 . . . . . . . . . . . 12 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑥 · (vol‘dom 𝐹)) ∈ ℝ)
5956, 58eqeltrd 2730 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ)
60 rexr 10123 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
61 elxrge0 12319 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (0[,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥))
6261biimpri 218 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,]+∞))
6360, 62sylan 487 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,]+∞))
6463ad2antrl 764 . . . . . . . . . . . . . . 15 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,]+∞))
6564adantr 480 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝑥 ∈ (0[,]+∞))
66 ifcl 4163 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞))
6765, 44, 66sylancl 695 . . . . . . . . . . . . 13 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞))
68 eqid 2651 . . . . . . . . . . . . 13 (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
6967, 68fmptd 6425 . . . . . . . . . . . 12 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞))
70 ifan 4167 . . . . . . . . . . . . . . 15 if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0)
711ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 𝐹:dom 𝐹⟶ℂ)
7271ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹𝑧) ∈ ℂ)
7372recld 13978 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ∈ ℝ)
7472abscld 14219 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹𝑧)) ∈ ℝ)
7557adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
7672releabsd 14234 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑧)))
77 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝐹𝑦) = (𝐹𝑧))
7877fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → (abs‘(𝐹𝑦)) = (abs‘(𝐹𝑧)))
7978breq1d 4695 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑧 → ((abs‘(𝐹𝑦)) ≤ 𝑥 ↔ (abs‘(𝐹𝑧)) ≤ 𝑥))
8079rspccva 3339 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥𝑧 ∈ dom 𝐹) → (abs‘(𝐹𝑧)) ≤ 𝑥)
8180adantll 750 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹𝑧)) ≤ 𝑥)
8281adantll 750 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹𝑧)) ≤ 𝑥)
8373, 74, 75, 76, 82letrd 10232 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ≤ 𝑥)
84 simprlr 820 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 0 ≤ 𝑥)
8584adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 0 ≤ 𝑥)
86 breq1 4688 . . . . . . . . . . . . . . . . . . . 20 ((ℜ‘(𝐹𝑧)) = if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) → ((ℜ‘(𝐹𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) ≤ 𝑥))
87 breq1 4688 . . . . . . . . . . . . . . . . . . . 20 (0 = if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) ≤ 𝑥))
8886, 87ifboth 4157 . . . . . . . . . . . . . . . . . . 19 (((ℜ‘(𝐹𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) ≤ 𝑥)
8983, 85, 88syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) ≤ 𝑥)
90 iftrue 4125 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) = if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0))
9190adantl 481 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) = if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0))
92 iftrue 4125 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 𝑥)
9392adantl 481 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 𝑥)
9489, 91, 933brtr4d 4717 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
9594ex 449 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
96 0le0 11148 . . . . . . . . . . . . . . . . . 18 0 ≤ 0
9796a1i 11 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → 0 ≤ 0)
98 iffalse 4128 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) = 0)
99 iffalse 4128 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 0)
10097, 98, 993brtr4d 4717 . . . . . . . . . . . . . . . 16 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
10195, 100pm2.61d1 171 . . . . . . . . . . . . . . 15 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
10270, 101syl5eqbr 4720 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
103102ralrimivw 2996 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
104 reex 10065 . . . . . . . . . . . . . . 15 ℝ ∈ V
105104a1i 11 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ℝ ∈ V)
106 eqidd 2652 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)))
107 eqidd 2652 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
108105, 46, 67, 106, 107ofrfval2 6957 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)) ∘𝑟 ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) ↔ ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
109103, 108mpbird 247 . . . . . . . . . . . 12 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)) ∘𝑟 ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
110 itg2le 23551 . . . . . . . . . . . 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))))
11148, 69, 109, 110syl3anc 1366 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
112 itg2lecl 23550 . . . . . . . . . . 11 (((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞) ∧ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧ (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))) ∈ ℝ)
11348, 59, 111, 112syl3anc 1366 . . . . . . . . . 10 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))) ∈ ℝ)
11438renegcld 10495 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ∈ ℝ)
115114rexrd 10127 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ∈ ℝ*)
116115adantrr 753 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧)))) → -(ℜ‘(𝐹𝑧)) ∈ ℝ*)
117 simprr 811 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧)))) → 0 ≤ -(ℜ‘(𝐹𝑧)))
118 elxrge0 12319 . . . . . . . . . . . . . 14 (-(ℜ‘(𝐹𝑧)) ∈ (0[,]+∞) ↔ (-(ℜ‘(𝐹𝑧)) ∈ ℝ* ∧ 0 ≤ -(ℜ‘(𝐹𝑧))))
119116, 117, 118sylanbrc 699 . . . . . . . . . . . . 13 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧)))) → -(ℜ‘(𝐹𝑧)) ∈ (0[,]+∞))
12044a1i 11 . . . . . . . . . . . . 13 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧)))) → 0 ∈ (0[,]+∞))
121119, 120ifclda 4153 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0) ∈ (0[,]+∞))
122 eqid 2651 . . . . . . . . . . . 12 (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))
123121, 122fmptd 6425 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞))
124 ifan 4167 . . . . . . . . . . . . . . 15 if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0)
12573renegcld 10495 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ∈ ℝ)
12673recnd 10106 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ∈ ℂ)
127126abscld 14219 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹𝑧))) ∈ ℝ)
128125leabsd 14197 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ≤ (abs‘-(ℜ‘(𝐹𝑧))))
129126absnegd 14232 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℜ‘(𝐹𝑧))) = (abs‘(ℜ‘(𝐹𝑧))))
130128, 129breqtrd 4711 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ≤ (abs‘(ℜ‘(𝐹𝑧))))
131 absrele 14092 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑧) ∈ ℂ → (abs‘(ℜ‘(𝐹𝑧))) ≤ (abs‘(𝐹𝑧)))
13272, 131syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹𝑧))) ≤ (abs‘(𝐹𝑧)))
133125, 127, 74, 130, 132letrd 10232 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑧)))
134125, 74, 75, 133, 82letrd 10232 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ≤ 𝑥)
135 breq1 4688 . . . . . . . . . . . . . . . . . . . 20 (-(ℜ‘(𝐹𝑧)) = if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) → (-(ℜ‘(𝐹𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) ≤ 𝑥))
136 breq1 4688 . . . . . . . . . . . . . . . . . . . 20 (0 = if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) ≤ 𝑥))
137135, 136ifboth 4157 . . . . . . . . . . . . . . . . . . 19 ((-(ℜ‘(𝐹𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) ≤ 𝑥)
138134, 85, 137syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) ≤ 𝑥)
139 iftrue 4125 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) = if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0))
140139adantl 481 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) = if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0))
141138, 140, 933brtr4d 4717 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
142141ex 449 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
143 iffalse 4128 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) = 0)
14497, 143, 993brtr4d 4717 . . . . . . . . . . . . . . . 16 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
145142, 144pm2.61d1 171 . . . . . . . . . . . . . . 15 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
146124, 145syl5eqbr 4720 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
147146ralrimivw 2996 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
148 eqidd 2652 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)))
149105, 121, 67, 148, 107ofrfval2 6957 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)) ∘𝑟 ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) ↔ ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
150147, 149mpbird 247 . . . . . . . . . . . 12 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)) ∘𝑟 ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
151 itg2le 23551 . . . . . . . . . . . 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))))
152123, 69, 150, 151syl3anc 1366 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
153 itg2lecl 23550 . . . . . . . . . . 11 (((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞) ∧ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧ (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))) ∈ ℝ)
154123, 59, 152, 153syl3anc 1366 . . . . . . . . . 10 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))) ∈ ℝ)
155113, 154jca 553 . . . . . . . . 9 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ((∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))) ∈ ℝ ∧ (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))) ∈ ℝ))
15637imcld 13979 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ∈ ℝ)
157156rexrd 10127 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ∈ ℝ*)
158157adantrr 753 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧)))) → (ℑ‘(𝐹𝑧)) ∈ ℝ*)
159 simprr 811 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧)))) → 0 ≤ (ℑ‘(𝐹𝑧)))
160 elxrge0 12319 . . . . . . . . . . . . . 14 ((ℑ‘(𝐹𝑧)) ∈ (0[,]+∞) ↔ ((ℑ‘(𝐹𝑧)) ∈ ℝ* ∧ 0 ≤ (ℑ‘(𝐹𝑧))))
161158, 159, 160sylanbrc 699 . . . . . . . . . . . . 13 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧)))) → (ℑ‘(𝐹𝑧)) ∈ (0[,]+∞))
16244a1i 11 . . . . . . . . . . . . 13 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧)))) → 0 ∈ (0[,]+∞))
163161, 162ifclda 4153 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0) ∈ (0[,]+∞))
164 eqid 2651 . . . . . . . . . . . 12 (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))
165163, 164fmptd 6425 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞))
166 ifan 4167 . . . . . . . . . . . . . . 15 if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0)
16772imcld 13979 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ∈ ℝ)
168167recnd 10106 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ∈ ℂ)
169168abscld 14219 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹𝑧))) ∈ ℝ)
170167leabsd 14197 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ≤ (abs‘(ℑ‘(𝐹𝑧))))
171 absimle 14093 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑧) ∈ ℂ → (abs‘(ℑ‘(𝐹𝑧))) ≤ (abs‘(𝐹𝑧)))
17272, 171syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹𝑧))) ≤ (abs‘(𝐹𝑧)))
173167, 169, 74, 170, 172letrd 10232 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑧)))
174167, 74, 75, 173, 82letrd 10232 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ≤ 𝑥)
175 breq1 4688 . . . . . . . . . . . . . . . . . . . 20 ((ℑ‘(𝐹𝑧)) = if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) → ((ℑ‘(𝐹𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) ≤ 𝑥))
176 breq1 4688 . . . . . . . . . . . . . . . . . . . 20 (0 = if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) ≤ 𝑥))
177175, 176ifboth 4157 . . . . . . . . . . . . . . . . . . 19 (((ℑ‘(𝐹𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) ≤ 𝑥)
178174, 85, 177syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) ≤ 𝑥)
179 iftrue 4125 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) = if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0))
180179adantl 481 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) = if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0))
181178, 180, 933brtr4d 4717 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
182181ex 449 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
183 iffalse 4128 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) = 0)
18497, 183, 993brtr4d 4717 . . . . . . . . . . . . . . . 16 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
185182, 184pm2.61d1 171 . . . . . . . . . . . . . . 15 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
186166, 185syl5eqbr 4720 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
187186ralrimivw 2996 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
188 eqidd 2652 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)))
189105, 163, 67, 188, 107ofrfval2 6957 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)) ∘𝑟 ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) ↔ ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
190187, 189mpbird 247 . . . . . . . . . . . 12 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)) ∘𝑟 ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
191 itg2le 23551 . . . . . . . . . . . 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))))
192165, 69, 190, 191syl3anc 1366 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
193 itg2lecl 23550 . . . . . . . . . . 11 (((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞) ∧ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧ (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))) ∈ ℝ)
194165, 59, 192, 193syl3anc 1366 . . . . . . . . . 10 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))) ∈ ℝ)
195156renegcld 10495 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ∈ ℝ)
196195rexrd 10127 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ∈ ℝ*)
197196adantrr 753 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧)))) → -(ℑ‘(𝐹𝑧)) ∈ ℝ*)
198 simprr 811 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧)))) → 0 ≤ -(ℑ‘(𝐹𝑧)))
199 elxrge0 12319 . . . . . . . . . . . . . 14 (-(ℑ‘(𝐹𝑧)) ∈ (0[,]+∞) ↔ (-(ℑ‘(𝐹𝑧)) ∈ ℝ* ∧ 0 ≤ -(ℑ‘(𝐹𝑧))))
200197, 198, 199sylanbrc 699 . . . . . . . . . . . . 13 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧)))) → -(ℑ‘(𝐹𝑧)) ∈ (0[,]+∞))
20144a1i 11 . . . . . . . . . . . . 13 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧)))) → 0 ∈ (0[,]+∞))
202200, 201ifclda 4153 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0) ∈ (0[,]+∞))
203 eqid 2651 . . . . . . . . . . . 12 (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))
204202, 203fmptd 6425 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞))
205 ifan 4167 . . . . . . . . . . . . . . 15 if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0)
206167renegcld 10495 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ∈ ℝ)
207206leabsd 14197 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ≤ (abs‘-(ℑ‘(𝐹𝑧))))
208168absnegd 14232 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℑ‘(𝐹𝑧))) = (abs‘(ℑ‘(𝐹𝑧))))
209207, 208breqtrd 4711 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ≤ (abs‘(ℑ‘(𝐹𝑧))))
210206, 169, 74, 209, 172letrd 10232 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑧)))
211206, 74, 75, 210, 82letrd 10232 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ≤ 𝑥)
212 breq1 4688 . . . . . . . . . . . . . . . . . . . 20 (-(ℑ‘(𝐹𝑧)) = if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) → (-(ℑ‘(𝐹𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) ≤ 𝑥))
213 breq1 4688 . . . . . . . . . . . . . . . . . . . 20 (0 = if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) ≤ 𝑥))
214212, 213ifboth 4157 . . . . . . . . . . . . . . . . . . 19 ((-(ℑ‘(𝐹𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) ≤ 𝑥)
215211, 85, 214syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) ≤ 𝑥)
216 iftrue 4125 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) = if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0))
217216adantl 481 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) = if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0))
218215, 217, 933brtr4d 4717 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
219218ex 449 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
220 iffalse 4128 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) = 0)
22197, 220, 993brtr4d 4717 . . . . . . . . . . . . . . . 16 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
222219, 221pm2.61d1 171 . . . . . . . . . . . . . . 15 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
223205, 222syl5eqbr 4720 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
224223ralrimivw 2996 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
225 eqidd 2652 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)))
226105, 202, 67, 225, 107ofrfval2 6957 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)) ∘𝑟 ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) ↔ ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
227224, 226mpbird 247 . . . . . . . . . . . 12 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)) ∘𝑟 ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
228 itg2le 23551 . . . . . . . . . . . 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))))
229204, 69, 227, 228syl3anc 1366 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
230 itg2lecl 23550 . . . . . . . . . . 11 (((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞) ∧ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧ (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))) ∈ ℝ)
231204, 59, 229, 230syl3anc 1366 . . . . . . . . . 10 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))) ∈ ℝ)
232194, 231jca 553 . . . . . . . . 9 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ((∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))) ∈ ℝ ∧ (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))) ∈ ℝ))
233 eqid 2651 . . . . . . . . . 10 (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)))
234 eqid 2651 . . . . . . . . . 10 (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)))
235 eqid 2651 . . . . . . . . . 10 (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)))
236 eqid 2651 . . . . . . . . . 10 (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)))
237233, 234, 235, 236, 72iblcnlem1 23599 . . . . . . . . 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))) ∈ ℝ))))
23835, 155, 232, 237mpbir3and 1264 . . . . . . . 8 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
23932, 238sylan2b 491 . . . . . . 7 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
240239anassrs 681 . . . . . 6 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 0 ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
24131, 240syldan 486 . . . . 5 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
24213, 241pm2.61dane 2910 . . . 4 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
243242rexlimdvaa 3061 . . 3 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥 → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1))
2442433impia 1280 . 2 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
2453, 244eqeltrd 2730 1 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  c0 3948  ifcif 4119  {csn 4210   class class class wbr 4685  cmpt 4762   × cxp 5141  dom cdm 5143  wf 5922  cfv 5926  (class class class)co 6690  𝑟 cofr 6938  cc 9972  cr 9973  0cc0 9974   · cmul 9979  +∞cpnf 10109  *cxr 10111  cle 10113  -cneg 10305  [,)cico 12215  [,]cicc 12216  cre 13881  cim 13882  abscabs 14018  volcvol 23278  MblFncmbf 23428  2citg2 23430  𝐿1cibl 23431
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-ofr 6940  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-xadd 11985  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-xmet 19787  df-met 19788  df-ovol 23279  df-vol 23280  df-mbf 23433  df-itg1 23434  df-itg2 23435  df-ibl 23436  df-0p 23482
This theorem is referenced by:  cnicciblnc  33611
  Copyright terms: Public domain W3C validator