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 33812
Description: Choice-free proof of bddibl 23826. (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 23613 . . . 4 (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ)
21feqmptd 6391 . . 3 (𝐹 ∈ MblFn → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)))
323ad2ant1 1127 . 2 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)))
4 rzal 4214 . . . . . . . 8 (dom 𝐹 = ∅ → ∀𝑧 ∈ dom 𝐹(𝐹𝑧) = 0)
5 mpteq12 4870 . . . . . . . 8 ((dom 𝐹 = ∅ ∧ ∀𝑧 ∈ dom 𝐹(𝐹𝑧) = 0) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) = (𝑧 ∈ ∅ ↦ 0))
64, 5mpdan 659 . . . . . . 7 (dom 𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) = (𝑧 ∈ ∅ ↦ 0))
7 fconstmpt 5303 . . . . . . . 8 (∅ × {0}) = (𝑧 ∈ ∅ ↦ 0)
8 0mbl 23527 . . . . . . . . 9 ∅ ∈ dom vol
9 ibl0 23773 . . . . . . . . 9 (∅ ∈ dom vol → (∅ × {0}) ∈ 𝐿1)
108, 9ax-mp 5 . . . . . . . 8 (∅ × {0}) ∈ 𝐿1
117, 10eqeltrri 2847 . . . . . . 7 (𝑧 ∈ ∅ ↦ 0) ∈ 𝐿1
126, 11syl6eqel 2858 . . . . . 6 (dom 𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
1312adantl 467 . . . . 5 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ dom 𝐹 = ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
14 r19.2z 4201 . . . . . . . . . 10 ((dom 𝐹 ≠ ∅ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) → ∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)
1514anim1i 594 . . . . . . . . 9 (((dom 𝐹 ≠ ∅ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥𝑥 ∈ ℝ))
1615an31s 625 . . . . . . . 8 (((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥𝑥 ∈ ℝ))
171ad2antrr 697 . . . . . . . . . . . . . . 15 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝐹:dom 𝐹⟶ℂ)
1817ffvelrnda 6502 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → (𝐹𝑦) ∈ ℂ)
1918absge0d 14391 . . . . . . . . . . . . 13 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 0 ≤ (abs‘(𝐹𝑦)))
20 0red 10243 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 0 ∈ ℝ)
2118abscld 14383 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → (abs‘(𝐹𝑦)) ∈ ℝ)
22 simplr 744 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
23 letr 10333 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ (abs‘(𝐹𝑦)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((0 ≤ (abs‘(𝐹𝑦)) ∧ (abs‘(𝐹𝑦)) ≤ 𝑥) → 0 ≤ 𝑥))
2420, 21, 22, 23syl3anc 1476 . . . . . . . . . . . . 13 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → ((0 ≤ (abs‘(𝐹𝑦)) ∧ (abs‘(𝐹𝑦)) ≤ 𝑥) → 0 ≤ 𝑥))
2519, 24mpand 667 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → ((abs‘(𝐹𝑦)) ≤ 𝑥 → 0 ≤ 𝑥))
2625rexlimdva 3179 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥 → 0 ≤ 𝑥))
2726ex 397 . . . . . . . . . 10 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (𝑥 ∈ ℝ → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥 → 0 ≤ 𝑥)))
2827com23 86 . . . . . . . . 9 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥 → (𝑥 ∈ ℝ → 0 ≤ 𝑥)))
2928imp32 405 . . . . . . . 8 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥𝑥 ∈ ℝ)) → 0 ≤ 𝑥)
3016, 29sylan2 572 . . . . . . 7 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅)) → 0 ≤ 𝑥)
3130anassrs 458 . . . . . 6 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → 0 ≤ 𝑥)
32 an32 617 . . . . . . . 8 (((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥))
33 id 22 . . . . . . . . . . 11 (𝐹 ∈ MblFn → 𝐹 ∈ MblFn)
342, 33eqeltrrd 2851 . . . . . . . . . 10 (𝐹 ∈ MblFn → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ MblFn)
3534ad2antrr 697 . . . . . . . . 9 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ MblFn)
361ad3antrrr 701 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝐹:dom 𝐹⟶ℂ)
3736ffvelrnda 6502 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (𝐹𝑧) ∈ ℂ)
3837recld 14142 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ∈ ℝ)
3938rexrd 10291 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ∈ ℝ*)
4039adantrr 688 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧)))) → (ℜ‘(𝐹𝑧)) ∈ ℝ*)
41 simprr 748 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧)))) → 0 ≤ (ℜ‘(𝐹𝑧)))
42 elxrge0 12488 . . . . . . . . . . . . . 14 ((ℜ‘(𝐹𝑧)) ∈ (0[,]+∞) ↔ ((ℜ‘(𝐹𝑧)) ∈ ℝ* ∧ 0 ≤ (ℜ‘(𝐹𝑧))))
4340, 41, 42sylanbrc 564 . . . . . . . . . . . . 13 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧)))) → (ℜ‘(𝐹𝑧)) ∈ (0[,]+∞))
44 0e0iccpnf 12490 . . . . . . . . . . . . . 14 0 ∈ (0[,]+∞)
4544a1i 11 . . . . . . . . . . . . 13 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧)))) → 0 ∈ (0[,]+∞))
4643, 45ifclda 4259 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0) ∈ (0[,]+∞))
47 eqid 2771 . . . . . . . . . . . 12 (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))
4846, 47fmptd 6527 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞))
49 mbfdm 23614 . . . . . . . . . . . . . 14 (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
5049ad2antrr 697 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → dom 𝐹 ∈ dom vol)
51 simplr 744 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (vol‘dom 𝐹) ∈ ℝ)
52 elrege0 12485 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
5352biimpri 218 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,)+∞))
5453ad2antrl 699 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,)+∞))
55 itg2const 23727 . . . . . . . . . . . . 13 ((dom 𝐹 ∈ dom vol ∧ (vol‘dom 𝐹) ∈ ℝ ∧ 𝑥 ∈ (0[,)+∞)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹)))
5650, 51, 54, 55syl3anc 1476 . . . . . . . . . . . 12 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹)))
57 simprll 756 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 𝑥 ∈ ℝ)
5857, 51remulcld 10272 . . . . . . . . . . . 12 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑥 · (vol‘dom 𝐹)) ∈ ℝ)
5956, 58eqeltrd 2850 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ)
60 rexr 10287 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
61 elxrge0 12488 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (0[,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥))
6261biimpri 218 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,]+∞))
6360, 62sylan 561 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,]+∞))
6463ad2antrl 699 . . . . . . . . . . . . . . 15 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,]+∞))
6564adantr 466 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝑥 ∈ (0[,]+∞))
66 ifcl 4269 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞))
6765, 44, 66sylancl 566 . . . . . . . . . . . . 13 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞))
68 eqid 2771 . . . . . . . . . . . . 13 (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
6967, 68fmptd 6527 . . . . . . . . . . . 12 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞))
70 ifan 4273 . . . . . . . . . . . . . . 15 if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0)
711ad2antrr 697 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 𝐹:dom 𝐹⟶ℂ)
7271ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹𝑧) ∈ ℂ)
7372recld 14142 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ∈ ℝ)
7472abscld 14383 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹𝑧)) ∈ ℝ)
7557adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
7672releabsd 14398 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑧)))
77 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝐹𝑦) = (𝐹𝑧))
7877fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → (abs‘(𝐹𝑦)) = (abs‘(𝐹𝑧)))
7978breq1d 4796 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑧 → ((abs‘(𝐹𝑦)) ≤ 𝑥 ↔ (abs‘(𝐹𝑧)) ≤ 𝑥))
8079rspccva 3459 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥𝑧 ∈ dom 𝐹) → (abs‘(𝐹𝑧)) ≤ 𝑥)
8180adantll 685 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹𝑧)) ≤ 𝑥)
8281adantll 685 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹𝑧)) ≤ 𝑥)
8373, 74, 75, 76, 82letrd 10396 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ≤ 𝑥)
84 simprlr 757 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 0 ≤ 𝑥)
8584adantr 466 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 0 ≤ 𝑥)
86 breq1 4789 . . . . . . . . . . . . . . . . . . . 20 ((ℜ‘(𝐹𝑧)) = if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) → ((ℜ‘(𝐹𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) ≤ 𝑥))
87 breq1 4789 . . . . . . . . . . . . . . . . . . . 20 (0 = if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) ≤ 𝑥))
8886, 87ifboth 4263 . . . . . . . . . . . . . . . . . . 19 (((ℜ‘(𝐹𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) ≤ 𝑥)
8983, 85, 88syl2anc 565 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) ≤ 𝑥)
90 iftrue 4231 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) = if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0))
9190adantl 467 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) = if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0))
92 iftrue 4231 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 𝑥)
9392adantl 467 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 𝑥)
9489, 91, 933brtr4d 4818 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
9594ex 397 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
96 0le0 11312 . . . . . . . . . . . . . . . . . 18 0 ≤ 0
9796a1i 11 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → 0 ≤ 0)
98 iffalse 4234 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) = 0)
99 iffalse 4234 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 0)
10097, 98, 993brtr4d 4818 . . . . . . . . . . . . . . . 16 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
10195, 100pm2.61d1 172 . . . . . . . . . . . . . . 15 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
10270, 101syl5eqbr 4821 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
103102ralrimivw 3116 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
104 reex 10229 . . . . . . . . . . . . . . 15 ℝ ∈ V
105104a1i 11 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ℝ ∈ V)
106 eqidd 2772 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)))
107 eqidd 2772 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
108105, 46, 67, 106, 107ofrfval2 7062 . . . . . . . . . . . . 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 23726 . . . . . . . . . . . 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 1476 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
112 itg2lecl 23725 . . . . . . . . . . 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 1476 . . . . . . . . . 10 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))) ∈ ℝ)
11438renegcld 10659 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ∈ ℝ)
115114rexrd 10291 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ∈ ℝ*)
116115adantrr 688 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧)))) → -(ℜ‘(𝐹𝑧)) ∈ ℝ*)
117 simprr 748 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧)))) → 0 ≤ -(ℜ‘(𝐹𝑧)))
118 elxrge0 12488 . . . . . . . . . . . . . 14 (-(ℜ‘(𝐹𝑧)) ∈ (0[,]+∞) ↔ (-(ℜ‘(𝐹𝑧)) ∈ ℝ* ∧ 0 ≤ -(ℜ‘(𝐹𝑧))))
119116, 117, 118sylanbrc 564 . . . . . . . . . . . . 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 4259 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0) ∈ (0[,]+∞))
122 eqid 2771 . . . . . . . . . . . 12 (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))
123121, 122fmptd 6527 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞))
124 ifan 4273 . . . . . . . . . . . . . . 15 if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0)
12573renegcld 10659 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ∈ ℝ)
12673recnd 10270 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ∈ ℂ)
127126abscld 14383 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹𝑧))) ∈ ℝ)
128125leabsd 14361 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ≤ (abs‘-(ℜ‘(𝐹𝑧))))
129126absnegd 14396 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℜ‘(𝐹𝑧))) = (abs‘(ℜ‘(𝐹𝑧))))
130128, 129breqtrd 4812 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ≤ (abs‘(ℜ‘(𝐹𝑧))))
131 absrele 14256 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑧) ∈ ℂ → (abs‘(ℜ‘(𝐹𝑧))) ≤ (abs‘(𝐹𝑧)))
13272, 131syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹𝑧))) ≤ (abs‘(𝐹𝑧)))
133125, 127, 74, 130, 132letrd 10396 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑧)))
134125, 74, 75, 133, 82letrd 10396 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ≤ 𝑥)
135 breq1 4789 . . . . . . . . . . . . . . . . . . . 20 (-(ℜ‘(𝐹𝑧)) = if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) → (-(ℜ‘(𝐹𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) ≤ 𝑥))
136 breq1 4789 . . . . . . . . . . . . . . . . . . . 20 (0 = if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) ≤ 𝑥))
137135, 136ifboth 4263 . . . . . . . . . . . . . . . . . . 19 ((-(ℜ‘(𝐹𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) ≤ 𝑥)
138134, 85, 137syl2anc 565 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) ≤ 𝑥)
139 iftrue 4231 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) = if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0))
140139adantl 467 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) = if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0))
141138, 140, 933brtr4d 4818 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
142141ex 397 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
143 iffalse 4234 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) = 0)
14497, 143, 993brtr4d 4818 . . . . . . . . . . . . . . . 16 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
145142, 144pm2.61d1 172 . . . . . . . . . . . . . . 15 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
146124, 145syl5eqbr 4821 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
147146ralrimivw 3116 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
148 eqidd 2772 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)))
149105, 121, 67, 148, 107ofrfval2 7062 . . . . . . . . . . . . 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 23726 . . . . . . . . . . . 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 1476 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
153 itg2lecl 23725 . . . . . . . . . . 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 1476 . . . . . . . . . 10 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))) ∈ ℝ)
155113, 154jca 495 . . . . . . . . 9 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ((∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))) ∈ ℝ ∧ (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))) ∈ ℝ))
15637imcld 14143 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ∈ ℝ)
157156rexrd 10291 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ∈ ℝ*)
158157adantrr 688 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧)))) → (ℑ‘(𝐹𝑧)) ∈ ℝ*)
159 simprr 748 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧)))) → 0 ≤ (ℑ‘(𝐹𝑧)))
160 elxrge0 12488 . . . . . . . . . . . . . 14 ((ℑ‘(𝐹𝑧)) ∈ (0[,]+∞) ↔ ((ℑ‘(𝐹𝑧)) ∈ ℝ* ∧ 0 ≤ (ℑ‘(𝐹𝑧))))
161158, 159, 160sylanbrc 564 . . . . . . . . . . . . 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 4259 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0) ∈ (0[,]+∞))
164 eqid 2771 . . . . . . . . . . . 12 (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))
165163, 164fmptd 6527 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞))
166 ifan 4273 . . . . . . . . . . . . . . 15 if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0)
16772imcld 14143 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ∈ ℝ)
168167recnd 10270 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ∈ ℂ)
169168abscld 14383 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹𝑧))) ∈ ℝ)
170167leabsd 14361 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ≤ (abs‘(ℑ‘(𝐹𝑧))))
171 absimle 14257 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑧) ∈ ℂ → (abs‘(ℑ‘(𝐹𝑧))) ≤ (abs‘(𝐹𝑧)))
17272, 171syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹𝑧))) ≤ (abs‘(𝐹𝑧)))
173167, 169, 74, 170, 172letrd 10396 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑧)))
174167, 74, 75, 173, 82letrd 10396 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ≤ 𝑥)
175 breq1 4789 . . . . . . . . . . . . . . . . . . . 20 ((ℑ‘(𝐹𝑧)) = if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) → ((ℑ‘(𝐹𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) ≤ 𝑥))
176 breq1 4789 . . . . . . . . . . . . . . . . . . . 20 (0 = if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) ≤ 𝑥))
177175, 176ifboth 4263 . . . . . . . . . . . . . . . . . . 19 (((ℑ‘(𝐹𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) ≤ 𝑥)
178174, 85, 177syl2anc 565 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) ≤ 𝑥)
179 iftrue 4231 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) = if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0))
180179adantl 467 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) = if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0))
181178, 180, 933brtr4d 4818 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
182181ex 397 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
183 iffalse 4234 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) = 0)
18497, 183, 993brtr4d 4818 . . . . . . . . . . . . . . . 16 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
185182, 184pm2.61d1 172 . . . . . . . . . . . . . . 15 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
186166, 185syl5eqbr 4821 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
187186ralrimivw 3116 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
188 eqidd 2772 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)))
189105, 163, 67, 188, 107ofrfval2 7062 . . . . . . . . . . . . 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 23726 . . . . . . . . . . . 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 1476 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
193 itg2lecl 23725 . . . . . . . . . . 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 1476 . . . . . . . . . 10 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))) ∈ ℝ)
195156renegcld 10659 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ∈ ℝ)
196195rexrd 10291 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ∈ ℝ*)
197196adantrr 688 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧)))) → -(ℑ‘(𝐹𝑧)) ∈ ℝ*)
198 simprr 748 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧)))) → 0 ≤ -(ℑ‘(𝐹𝑧)))
199 elxrge0 12488 . . . . . . . . . . . . . 14 (-(ℑ‘(𝐹𝑧)) ∈ (0[,]+∞) ↔ (-(ℑ‘(𝐹𝑧)) ∈ ℝ* ∧ 0 ≤ -(ℑ‘(𝐹𝑧))))
200197, 198, 199sylanbrc 564 . . . . . . . . . . . . 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 4259 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0) ∈ (0[,]+∞))
203 eqid 2771 . . . . . . . . . . . 12 (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))
204202, 203fmptd 6527 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞))
205 ifan 4273 . . . . . . . . . . . . . . 15 if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0)
206167renegcld 10659 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ∈ ℝ)
207206leabsd 14361 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ≤ (abs‘-(ℑ‘(𝐹𝑧))))
208168absnegd 14396 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℑ‘(𝐹𝑧))) = (abs‘(ℑ‘(𝐹𝑧))))
209207, 208breqtrd 4812 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ≤ (abs‘(ℑ‘(𝐹𝑧))))
210206, 169, 74, 209, 172letrd 10396 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑧)))
211206, 74, 75, 210, 82letrd 10396 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ≤ 𝑥)
212 breq1 4789 . . . . . . . . . . . . . . . . . . . 20 (-(ℑ‘(𝐹𝑧)) = if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) → (-(ℑ‘(𝐹𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) ≤ 𝑥))
213 breq1 4789 . . . . . . . . . . . . . . . . . . . 20 (0 = if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) ≤ 𝑥))
214212, 213ifboth 4263 . . . . . . . . . . . . . . . . . . 19 ((-(ℑ‘(𝐹𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) ≤ 𝑥)
215211, 85, 214syl2anc 565 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) ≤ 𝑥)
216 iftrue 4231 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) = if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0))
217216adantl 467 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) = if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0))
218215, 217, 933brtr4d 4818 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
219218ex 397 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
220 iffalse 4234 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) = 0)
22197, 220, 993brtr4d 4818 . . . . . . . . . . . . . . . 16 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
222219, 221pm2.61d1 172 . . . . . . . . . . . . . . 15 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
223205, 222syl5eqbr 4821 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
224223ralrimivw 3116 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
225 eqidd 2772 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)))
226105, 202, 67, 225, 107ofrfval2 7062 . . . . . . . . . . . . 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 23726 . . . . . . . . . . . 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 1476 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
230 itg2lecl 23725 . . . . . . . . . . 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 1476 . . . . . . . . . 10 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))) ∈ ℝ)
232194, 231jca 495 . . . . . . . . 9 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ((∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))) ∈ ℝ ∧ (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))) ∈ ℝ))
233 eqid 2771 . . . . . . . . . 10 (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)))
234 eqid 2771 . . . . . . . . . 10 (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)))
235 eqid 2771 . . . . . . . . . 10 (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)))
236 eqid 2771 . . . . . . . . . 10 (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)))
237233, 234, 235, 236, 72iblcnlem1 23774 . . . . . . . . 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 1427 . . . . . . . 8 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
23932, 238sylan2b 573 . . . . . . 7 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
240239anassrs 458 . . . . . 6 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 0 ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
24131, 240syldan 571 . . . . 5 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
24213, 241pm2.61dane 3030 . . . 4 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
243242rexlimdvaa 3180 . . 3 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥 → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1))
2442433impia 1109 . 2 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
2453, 244eqeltrd 2850 1 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  Vcvv 3351  c0 4063  ifcif 4225  {csn 4316   class class class wbr 4786  cmpt 4863   × cxp 5247  dom cdm 5249  wf 6027  cfv 6031  (class class class)co 6793  𝑟 cofr 7043  cc 10136  cr 10137  0cc0 10138   · cmul 10143  +∞cpnf 10273  *cxr 10275  cle 10277  -cneg 10469  [,)cico 12382  [,]cicc 12383  cre 14045  cim 14046  abscabs 14182  volcvol 23451  MblFncmbf 23602  2citg2 23604  𝐿1cibl 23605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216  ax-addf 10217
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-disj 4755  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-ofr 7045  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-z 11580  df-uz 11889  df-q 11992  df-rp 12036  df-xadd 12152  df-ioo 12384  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-clim 14427  df-sum 14625  df-xmet 19954  df-met 19955  df-ovol 23452  df-vol 23453  df-mbf 23607  df-itg1 23608  df-itg2 23609  df-ibl 23610  df-0p 23657
This theorem is referenced by:  cnicciblnc  33813
  Copyright terms: Public domain W3C validator