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	ffvelrnda	⊢ ( ( ( ( 𝐹 ∈ 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	ffvelrnda	⊢ ( ( ( ( ( 𝐹 ∈ 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	ffvelrnda	⊢ ( ( ( ( 𝐹 ∈ 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 )