This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bddiblnc

Description: Choice-free proof of bddibl . (Contributed by Brendan Leahy, 2-Nov-2017) (Revised by Brendan Leahy, 6-Nov-2017)

Ref Expression
Assertion bddiblnc ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → 𝐹 ∈ 𝐿1 )

Proof

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