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 33147
Description: Choice-free proof of bddibl 23529. (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 23317 . . . 4 (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ)
21feqmptd 6211 . . 3 (𝐹 ∈ MblFn → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)))
323ad2ant1 1080 . 2 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)))
4 rzal 4050 . . . . . . . 8 (dom 𝐹 = ∅ → ∀𝑧 ∈ dom 𝐹(𝐹𝑧) = 0)
5 mpteq12 4701 . . . . . . . 8 ((dom 𝐹 = ∅ ∧ ∀𝑧 ∈ dom 𝐹(𝐹𝑧) = 0) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) = (𝑧 ∈ ∅ ↦ 0))
64, 5mpdan 701 . . . . . . 7 (dom 𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) = (𝑧 ∈ ∅ ↦ 0))
7 fconstmpt 5128 . . . . . . . 8 (∅ × {0}) = (𝑧 ∈ ∅ ↦ 0)
8 0mbl 23230 . . . . . . . . 9 ∅ ∈ dom vol
9 ibl0 23476 . . . . . . . . 9 (∅ ∈ dom vol → (∅ × {0}) ∈ 𝐿1)
108, 9ax-mp 5 . . . . . . . 8 (∅ × {0}) ∈ 𝐿1
117, 10eqeltrri 2695 . . . . . . 7 (𝑧 ∈ ∅ ↦ 0) ∈ 𝐿1
126, 11syl6eqel 2706 . . . . . 6 (dom 𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
1312adantl 482 . . . . 5 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ dom 𝐹 = ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
14 r19.2z 4037 . . . . . . . . . 10 ((dom 𝐹 ≠ ∅ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) → ∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)
1514anim1i 591 . . . . . . . . 9 (((dom 𝐹 ≠ ∅ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥𝑥 ∈ ℝ))
1615an31s 847 . . . . . . . 8 (((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥𝑥 ∈ ℝ))
171ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝐹:dom 𝐹⟶ℂ)
1817ffvelrnda 6320 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → (𝐹𝑦) ∈ ℂ)
1918absge0d 14125 . . . . . . . . . . . . 13 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 0 ≤ (abs‘(𝐹𝑦)))
20 0red 9993 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 0 ∈ ℝ)
2118abscld 14117 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → (abs‘(𝐹𝑦)) ∈ ℝ)
22 simplr 791 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
23 letr 10083 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ (abs‘(𝐹𝑦)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((0 ≤ (abs‘(𝐹𝑦)) ∧ (abs‘(𝐹𝑦)) ≤ 𝑥) → 0 ≤ 𝑥))
2420, 21, 22, 23syl3anc 1323 . . . . . . . . . . . . 13 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → ((0 ≤ (abs‘(𝐹𝑦)) ∧ (abs‘(𝐹𝑦)) ≤ 𝑥) → 0 ≤ 𝑥))
2519, 24mpand 710 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → ((abs‘(𝐹𝑦)) ≤ 𝑥 → 0 ≤ 𝑥))
2625rexlimdva 3025 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥 → 0 ≤ 𝑥))
2726ex 450 . . . . . . . . . 10 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (𝑥 ∈ ℝ → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥 → 0 ≤ 𝑥)))
2827com23 86 . . . . . . . . 9 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥 → (𝑥 ∈ ℝ → 0 ≤ 𝑥)))
2928imp32 449 . . . . . . . 8 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (∃𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥𝑥 ∈ ℝ)) → 0 ≤ 𝑥)
3016, 29sylan2 491 . . . . . . 7 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅)) → 0 ≤ 𝑥)
3130anassrs 679 . . . . . 6 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → 0 ≤ 𝑥)
32 an32 838 . . . . . . . 8 (((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥))
33 id 22 . . . . . . . . . . 11 (𝐹 ∈ MblFn → 𝐹 ∈ MblFn)
342, 33eqeltrrd 2699 . . . . . . . . . 10 (𝐹 ∈ MblFn → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ MblFn)
3534ad2antrr 761 . . . . . . . . 9 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ MblFn)
361ad3antrrr 765 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝐹:dom 𝐹⟶ℂ)
3736ffvelrnda 6320 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (𝐹𝑧) ∈ ℂ)
3837recld 13876 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ∈ ℝ)
3938rexrd 10041 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ∈ ℝ*)
4039adantrr 752 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧)))) → (ℜ‘(𝐹𝑧)) ∈ ℝ*)
41 simprr 795 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧)))) → 0 ≤ (ℜ‘(𝐹𝑧)))
42 elxrge0 12231 . . . . . . . . . . . . . 14 ((ℜ‘(𝐹𝑧)) ∈ (0[,]+∞) ↔ ((ℜ‘(𝐹𝑧)) ∈ ℝ* ∧ 0 ≤ (ℜ‘(𝐹𝑧))))
4340, 41, 42sylanbrc 697 . . . . . . . . . . . . 13 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧)))) → (ℜ‘(𝐹𝑧)) ∈ (0[,]+∞))
44 0e0iccpnf 12233 . . . . . . . . . . . . . 14 0 ∈ (0[,]+∞)
4544a1i 11 . . . . . . . . . . . . 13 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧)))) → 0 ∈ (0[,]+∞))
4643, 45ifclda 4097 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0) ∈ (0[,]+∞))
47 eqid 2621 . . . . . . . . . . . 12 (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))
4846, 47fmptd 6346 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞))
49 mbfdm 23318 . . . . . . . . . . . . . 14 (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
5049ad2antrr 761 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → dom 𝐹 ∈ dom vol)
51 simplr 791 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (vol‘dom 𝐹) ∈ ℝ)
52 elrege0 12228 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
5352biimpri 218 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,)+∞))
5453ad2antrl 763 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,)+∞))
55 itg2const 23430 . . . . . . . . . . . . 13 ((dom 𝐹 ∈ dom vol ∧ (vol‘dom 𝐹) ∈ ℝ ∧ 𝑥 ∈ (0[,)+∞)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹)))
5650, 51, 54, 55syl3anc 1323 . . . . . . . . . . . 12 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹)))
57 simprll 801 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 𝑥 ∈ ℝ)
5857, 51remulcld 10022 . . . . . . . . . . . 12 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑥 · (vol‘dom 𝐹)) ∈ ℝ)
5956, 58eqeltrd 2698 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ)
60 rexr 10037 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
61 elxrge0 12231 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (0[,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥))
6261biimpri 218 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,]+∞))
6360, 62sylan 488 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,]+∞))
6463ad2antrl 763 . . . . . . . . . . . . . . 15 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,]+∞))
6564adantr 481 . . . . . . . . . . . . . 14 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝑥 ∈ (0[,]+∞))
66 ifcl 4107 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞))
6765, 44, 66sylancl 693 . . . . . . . . . . . . 13 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞))
68 eqid 2621 . . . . . . . . . . . . 13 (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
6967, 68fmptd 6346 . . . . . . . . . . . 12 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞))
70 ifan 4111 . . . . . . . . . . . . . . 15 if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0)
711ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 𝐹:dom 𝐹⟶ℂ)
7271ffvelrnda 6320 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹𝑧) ∈ ℂ)
7372recld 13876 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ∈ ℝ)
7472abscld 14117 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹𝑧)) ∈ ℝ)
7557adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
7672releabsd 14132 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑧)))
77 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝐹𝑦) = (𝐹𝑧))
7877fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → (abs‘(𝐹𝑦)) = (abs‘(𝐹𝑧)))
7978breq1d 4628 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑧 → ((abs‘(𝐹𝑦)) ≤ 𝑥 ↔ (abs‘(𝐹𝑧)) ≤ 𝑥))
8079rspccva 3297 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥𝑧 ∈ dom 𝐹) → (abs‘(𝐹𝑧)) ≤ 𝑥)
8180adantll 749 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹𝑧)) ≤ 𝑥)
8281adantll 749 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹𝑧)) ≤ 𝑥)
8373, 74, 75, 76, 82letrd 10146 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ≤ 𝑥)
84 simprlr 802 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → 0 ≤ 𝑥)
8584adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 0 ≤ 𝑥)
86 breq1 4621 . . . . . . . . . . . . . . . . . . . 20 ((ℜ‘(𝐹𝑧)) = if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) → ((ℜ‘(𝐹𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) ≤ 𝑥))
87 breq1 4621 . . . . . . . . . . . . . . . . . . . 20 (0 = if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) ≤ 𝑥))
8886, 87ifboth 4101 . . . . . . . . . . . . . . . . . . 19 (((ℜ‘(𝐹𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) ≤ 𝑥)
8983, 85, 88syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0) ≤ 𝑥)
90 iftrue 4069 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) = if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0))
9190adantl 482 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) = if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0))
92 iftrue 4069 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 𝑥)
9392adantl 482 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 𝑥)
9489, 91, 933brtr4d 4650 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
9594ex 450 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
96 0le0 11062 . . . . . . . . . . . . . . . . . 18 0 ≤ 0
9796a1i 11 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → 0 ≤ 0)
98 iffalse 4072 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹𝑧)), (ℜ‘(𝐹𝑧)), 0), 0) = 0)
99 iffalse 4072 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 0)
10097, 98, 993brtr4d 4650 . . . . . . . . . . . . . . . 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 4653 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
103102ralrimivw 2962 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
104 reex 9979 . . . . . . . . . . . . . . 15 ℝ ∈ V
105104a1i 11 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ℝ ∈ V)
106 eqidd 2622 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)))
107 eqidd 2622 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
108105, 46, 67, 106, 107ofrfval2 6875 . . . . . . . . . . . . 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 23429 . . . . . . . . . . . 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 1323 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
112 itg2lecl 23428 . . . . . . . . . . 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 1323 . . . . . . . . . 10 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))) ∈ ℝ)
11438renegcld 10409 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ∈ ℝ)
115114rexrd 10041 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ∈ ℝ*)
116115adantrr 752 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧)))) → -(ℜ‘(𝐹𝑧)) ∈ ℝ*)
117 simprr 795 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧)))) → 0 ≤ -(ℜ‘(𝐹𝑧)))
118 elxrge0 12231 . . . . . . . . . . . . . 14 (-(ℜ‘(𝐹𝑧)) ∈ (0[,]+∞) ↔ (-(ℜ‘(𝐹𝑧)) ∈ ℝ* ∧ 0 ≤ -(ℜ‘(𝐹𝑧))))
119116, 117, 118sylanbrc 697 . . . . . . . . . . . . 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 4097 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0) ∈ (0[,]+∞))
122 eqid 2621 . . . . . . . . . . . 12 (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))
123121, 122fmptd 6346 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞))
124 ifan 4111 . . . . . . . . . . . . . . 15 if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0)
12573renegcld 10409 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ∈ ℝ)
12673recnd 10020 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹𝑧)) ∈ ℂ)
127126abscld 14117 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹𝑧))) ∈ ℝ)
128125leabsd 14095 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ≤ (abs‘-(ℜ‘(𝐹𝑧))))
129126absnegd 14130 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℜ‘(𝐹𝑧))) = (abs‘(ℜ‘(𝐹𝑧))))
130128, 129breqtrd 4644 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ≤ (abs‘(ℜ‘(𝐹𝑧))))
131 absrele 13990 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑧) ∈ ℂ → (abs‘(ℜ‘(𝐹𝑧))) ≤ (abs‘(𝐹𝑧)))
13272, 131syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹𝑧))) ≤ (abs‘(𝐹𝑧)))
133125, 127, 74, 130, 132letrd 10146 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑧)))
134125, 74, 75, 133, 82letrd 10146 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹𝑧)) ≤ 𝑥)
135 breq1 4621 . . . . . . . . . . . . . . . . . . . 20 (-(ℜ‘(𝐹𝑧)) = if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) → (-(ℜ‘(𝐹𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) ≤ 𝑥))
136 breq1 4621 . . . . . . . . . . . . . . . . . . . 20 (0 = if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) ≤ 𝑥))
137135, 136ifboth 4101 . . . . . . . . . . . . . . . . . . 19 ((-(ℜ‘(𝐹𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) ≤ 𝑥)
138134, 85, 137syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0) ≤ 𝑥)
139 iftrue 4069 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) = if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0))
140139adantl 482 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) = if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0))
141138, 140, 933brtr4d 4650 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
142141ex 450 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
143 iffalse 4072 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹𝑧)), -(ℜ‘(𝐹𝑧)), 0), 0) = 0)
14497, 143, 993brtr4d 4650 . . . . . . . . . . . . . . . 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 4653 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
147146ralrimivw 2962 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
148 eqidd 2622 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)))
149105, 121, 67, 148, 107ofrfval2 6875 . . . . . . . . . . . . 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 23429 . . . . . . . . . . . 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 1323 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
153 itg2lecl 23428 . . . . . . . . . . 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 1323 . . . . . . . . . 10 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))) ∈ ℝ)
155113, 154jca 554 . . . . . . . . 9 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ((∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))) ∈ ℝ ∧ (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))) ∈ ℝ))
15637imcld 13877 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ∈ ℝ)
157156rexrd 10041 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ∈ ℝ*)
158157adantrr 752 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧)))) → (ℑ‘(𝐹𝑧)) ∈ ℝ*)
159 simprr 795 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧)))) → 0 ≤ (ℑ‘(𝐹𝑧)))
160 elxrge0 12231 . . . . . . . . . . . . . 14 ((ℑ‘(𝐹𝑧)) ∈ (0[,]+∞) ↔ ((ℑ‘(𝐹𝑧)) ∈ ℝ* ∧ 0 ≤ (ℑ‘(𝐹𝑧))))
161158, 159, 160sylanbrc 697 . . . . . . . . . . . . 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 4097 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0) ∈ (0[,]+∞))
164 eqid 2621 . . . . . . . . . . . 12 (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))
165163, 164fmptd 6346 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞))
166 ifan 4111 . . . . . . . . . . . . . . 15 if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0)
16772imcld 13877 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ∈ ℝ)
168167recnd 10020 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ∈ ℂ)
169168abscld 14117 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹𝑧))) ∈ ℝ)
170167leabsd 14095 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ≤ (abs‘(ℑ‘(𝐹𝑧))))
171 absimle 13991 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑧) ∈ ℂ → (abs‘(ℑ‘(𝐹𝑧))) ≤ (abs‘(𝐹𝑧)))
17272, 171syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹𝑧))) ≤ (abs‘(𝐹𝑧)))
173167, 169, 74, 170, 172letrd 10146 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑧)))
174167, 74, 75, 173, 82letrd 10146 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹𝑧)) ≤ 𝑥)
175 breq1 4621 . . . . . . . . . . . . . . . . . . . 20 ((ℑ‘(𝐹𝑧)) = if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) → ((ℑ‘(𝐹𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) ≤ 𝑥))
176 breq1 4621 . . . . . . . . . . . . . . . . . . . 20 (0 = if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) ≤ 𝑥))
177175, 176ifboth 4101 . . . . . . . . . . . . . . . . . . 19 (((ℑ‘(𝐹𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) ≤ 𝑥)
178174, 85, 177syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0) ≤ 𝑥)
179 iftrue 4069 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) = if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0))
180179adantl 482 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) = if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0))
181178, 180, 933brtr4d 4650 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
182181ex 450 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
183 iffalse 4072 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹𝑧)), (ℑ‘(𝐹𝑧)), 0), 0) = 0)
18497, 183, 993brtr4d 4650 . . . . . . . . . . . . . . . 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 4653 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
187186ralrimivw 2962 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
188 eqidd 2622 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)))
189105, 163, 67, 188, 107ofrfval2 6875 . . . . . . . . . . . . 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 23429 . . . . . . . . . . . 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 1323 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
193 itg2lecl 23428 . . . . . . . . . . 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 1323 . . . . . . . . . 10 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))) ∈ ℝ)
195156renegcld 10409 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ∈ ℝ)
196195rexrd 10041 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ∈ ℝ*)
197196adantrr 752 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧)))) → -(ℑ‘(𝐹𝑧)) ∈ ℝ*)
198 simprr 795 . . . . . . . . . . . . . 14 (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧)))) → 0 ≤ -(ℑ‘(𝐹𝑧)))
199 elxrge0 12231 . . . . . . . . . . . . . 14 (-(ℑ‘(𝐹𝑧)) ∈ (0[,]+∞) ↔ (-(ℑ‘(𝐹𝑧)) ∈ ℝ* ∧ 0 ≤ -(ℑ‘(𝐹𝑧))))
200197, 198, 199sylanbrc 697 . . . . . . . . . . . . 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 4097 . . . . . . . . . . . 12 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0) ∈ (0[,]+∞))
203 eqid 2621 . . . . . . . . . . . 12 (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))
204202, 203fmptd 6346 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)):ℝ⟶(0[,]+∞))
205 ifan 4111 . . . . . . . . . . . . . . 15 if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0)
206167renegcld 10409 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ∈ ℝ)
207206leabsd 14095 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ≤ (abs‘-(ℑ‘(𝐹𝑧))))
208168absnegd 14130 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℑ‘(𝐹𝑧))) = (abs‘(ℑ‘(𝐹𝑧))))
209207, 208breqtrd 4644 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ≤ (abs‘(ℑ‘(𝐹𝑧))))
210206, 169, 74, 209, 172letrd 10146 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑧)))
211206, 74, 75, 210, 82letrd 10146 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹𝑧)) ≤ 𝑥)
212 breq1 4621 . . . . . . . . . . . . . . . . . . . 20 (-(ℑ‘(𝐹𝑧)) = if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) → (-(ℑ‘(𝐹𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) ≤ 𝑥))
213 breq1 4621 . . . . . . . . . . . . . . . . . . . 20 (0 = if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) ≤ 𝑥))
214212, 213ifboth 4101 . . . . . . . . . . . . . . . . . . 19 ((-(ℑ‘(𝐹𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) ≤ 𝑥)
215211, 85, 214syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0) ≤ 𝑥)
216 iftrue 4069 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) = if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0))
217216adantl 482 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) = if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0))
218215, 217, 933brtr4d 4650 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
219218ex 450 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
220 iffalse 4072 . . . . . . . . . . . . . . . . 17 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹𝑧)), -(ℑ‘(𝐹𝑧)), 0), 0) = 0)
22197, 220, 993brtr4d 4650 . . . . . . . . . . . . . . . 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 4653 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
224223ralrimivw 2962 . . . . . . . . . . . . 13 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
225 eqidd 2622 . . . . . . . . . . . . . 14 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)))
226105, 202, 67, 225, 107ofrfval2 6875 . . . . . . . . . . . . 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 23429 . . . . . . . . . . . 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 1323 . . . . . . . . . . 11 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))) ≤ (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
230 itg2lecl 23428 . . . . . . . . . . 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 1323 . . . . . . . . . 10 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))) ∈ ℝ)
232194, 231jca 554 . . . . . . . . 9 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → ((∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))) ∈ ℝ ∧ (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))) ∈ ℝ))
233 eqid 2621 . . . . . . . . . 10 (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹𝑧))), (ℜ‘(𝐹𝑧)), 0)))
234 eqid 2621 . . . . . . . . . 10 (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹𝑧))), -(ℜ‘(𝐹𝑧)), 0)))
235 eqid 2621 . . . . . . . . . 10 (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹𝑧))), (ℑ‘(𝐹𝑧)), 0)))
236 eqid 2621 . . . . . . . . . 10 (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0))) = (∫2‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹𝑧))), -(ℑ‘(𝐹𝑧)), 0)))
237233, 234, 235, 236, 72iblcnlem1 23477 . . . . . . . . 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 1243 . . . . . . . 8 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
23932, 238sylan2b 492 . . . . . . 7 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
240239anassrs 679 . . . . . 6 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ 0 ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
24131, 240syldan 487 . . . . 5 ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
24213, 241pm2.61dane 2877 . . . 4 (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
243242rexlimdvaa 3026 . . 3 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥 → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1))
2442433impia 1258 . 2 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹𝑧)) ∈ 𝐿1)
2453, 244eqeltrd 2698 1 ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3189  c0 3896  ifcif 4063  {csn 4153   class class class wbr 4618  cmpt 4678   × cxp 5077  dom cdm 5079  wf 5848  cfv 5852  (class class class)co 6610  𝑟 cofr 6856  cc 9886  cr 9887  0cc0 9888   · cmul 9893  +∞cpnf 10023  *cxr 10025  cle 10027  -cneg 10219  [,)cico 12127  [,]cicc 12128  cre 13779  cim 13780  abscabs 13916  volcvol 23155  MblFncmbf 23306  2citg2 23308  𝐿1cibl 23309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8490  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966  ax-addf 9967
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-disj 4589  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-ofr 6858  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-sup 8300  df-inf 8301  df-oi 8367  df-card 8717  df-cda 8942  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-div 10637  df-nn 10973  df-2 11031  df-3 11032  df-n0 11245  df-z 11330  df-uz 11640  df-q 11741  df-rp 11785  df-xadd 11899  df-ioo 12129  df-ico 12131  df-icc 12132  df-fz 12277  df-fzo 12415  df-fl 12541  df-seq 12750  df-exp 12809  df-hash 13066  df-cj 13781  df-re 13782  df-im 13783  df-sqrt 13917  df-abs 13918  df-clim 14161  df-sum 14359  df-xmet 19671  df-met 19672  df-ovol 23156  df-vol 23157  df-mbf 23311  df-itg1 23312  df-itg2 23313  df-ibl 23314  df-0p 23360
This theorem is referenced by:  cnicciblnc  33148
  Copyright terms: Public domain W3C validator