bddiblnc - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > bddiblnc		Structured version Visualization version GIF version

Theorem bddiblnc 24911

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

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

Distinct variable group: 𝑥,𝑦,𝐹

Proof of Theorem bddiblnc Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mbff 24694	. . . 4 ⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ)
2	1	feqmptd 6819	. . 3 ⊢ (𝐹 ∈ MblFn → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)))
3	2	3ad2ant1 1131	. 2 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)))
4		rzal 4436	. . . . . . . 8 ⊢ (dom 𝐹 = ∅ → ∀𝑧 ∈ dom 𝐹(𝐹‘𝑧) = 0)
5		mpteq12 5162	. . . . . . . 8 ⊢ ((dom 𝐹 = ∅ ∧ ∀𝑧 ∈ dom 𝐹(𝐹‘𝑧) = 0) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) = (𝑧 ∈ ∅ ↦ 0))
6	4, 5	mpdan 683	. . . . . . 7 ⊢ (dom 𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) = (𝑧 ∈ ∅ ↦ 0))
7		fconstmpt 5640	. . . . . . . 8 ⊢ (∅ × {0}) = (𝑧 ∈ ∅ ↦ 0)
8		0mbl 24608	. . . . . . . . 9 ⊢ ∅ ∈ dom vol
9		ibl0 24856	. . . . . . . . 9 ⊢ (∅ ∈ dom vol → (∅ × {0}) ∈ 𝐿¹)
10	8, 9	ax-mp 5	. . . . . . . 8 ⊢ (∅ × {0}) ∈ 𝐿¹
11	7, 10	eqeltrri 2836	. . . . . . 7 ⊢ (𝑧 ∈ ∅ ↦ 0) ∈ 𝐿¹
12	6, 11	eqeltrdi 2847	. . . . . 6 ⊢ (dom 𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
13	12	adantl 481	. . . . 5 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 = ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
14		r19.2z 4422	. . . . . . . . . 10 ⊢ ((dom 𝐹 ≠ ∅ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → ∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)
15	14	anim1i 614	. . . . . . . . 9 ⊢ (((dom 𝐹 ≠ ∅ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑥 ∈ ℝ))
16	15	an31s 650	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑥 ∈ ℝ))
17	1	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝐹:dom 𝐹⟶ℂ)
18	17	ffvelrnda 6943	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) ∈ ℂ)
19	18	absge0d 15084	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 0 ≤ (abs‘(𝐹‘𝑦)))
20		0red 10909	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 0 ∈ ℝ)
21	18	abscld 15076	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → (abs‘(𝐹‘𝑦)) ∈ ℝ)
22		simplr 765	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
23		letr 10999	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (abs‘(𝐹‘𝑦)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((0 ≤ (abs‘(𝐹‘𝑦)) ∧ (abs‘(𝐹‘𝑦)) ≤ 𝑥) → 0 ≤ 𝑥))
24	20, 21, 22, 23	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → ((0 ≤ (abs‘(𝐹‘𝑦)) ∧ (abs‘(𝐹‘𝑦)) ≤ 𝑥) → 0 ≤ 𝑥))
25	19, 24	mpand 691	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → ((abs‘(𝐹‘𝑦)) ≤ 𝑥 → 0 ≤ 𝑥))
26	25	rexlimdva 3212	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → 0 ≤ 𝑥))
27	26	ex 412	. . . . . . . . . 10 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (𝑥 ∈ ℝ → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → 0 ≤ 𝑥)))
28	27	com23 86	. . . . . . . . 9 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → (𝑥 ∈ ℝ → 0 ≤ 𝑥)))
29	28	imp32 418	. . . . . . . 8 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑥 ∈ ℝ)) → 0 ≤ 𝑥)
30	16, 29	sylan2 592	. . . . . . 7 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅)) → 0 ≤ 𝑥)
31	30	anassrs 467	. . . . . 6 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → 0 ≤ 𝑥)
32		an32 642	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥))
33		id 22	. . . . . . . . . . 11 ⊢ (𝐹 ∈ MblFn → 𝐹 ∈ MblFn)
34	2, 33	eqeltrrd 2840	. . . . . . . . . 10 ⊢ (𝐹 ∈ MblFn → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ MblFn)
35	34	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ MblFn)
36	1	ad3antrrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝐹:dom 𝐹⟶ℂ)
37	36	ffvelrnda 6943	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ)
38	37	recld 14833	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ)
39	38	rexrd 10956	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ^*)
40	39	adantrr 713	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ^*)
41		simprr 769	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → 0 ≤ (ℜ‘(𝐹‘𝑧)))
42		elxrge0 13118	. . . . . . . . . . . . . 14 ⊢ ((ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔ ((ℜ‘(𝐹‘𝑧)) ∈ ℝ^* ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))))
43	40, 41, 42	sylanbrc 582	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → (ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞))
44		0e0iccpnf 13120	. . . . . . . . . . . . . 14 ⊢ 0 ∈ (0[,]+∞)
45	44	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → 0 ∈ (0[,]+∞))
46	43, 45	ifclda 4491	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
47	46	fmpttd 6971	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
48		mbfdm 24695	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
49	48	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → dom 𝐹 ∈ dom vol)
50		simplr 765	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (vol‘dom 𝐹) ∈ ℝ)
51		elrege0 13115	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
52	51	biimpri 227	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,)+∞))
53	52	ad2antrl 724	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,)+∞))
54		itg2const 24810	. . . . . . . . . . . . 13 ⊢ ((dom 𝐹 ∈ dom vol ∧ (vol‘dom 𝐹) ∈ ℝ ∧ 𝑥 ∈ (0[,)+∞)) → (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹)))
55	49, 50, 53, 54	syl3anc 1369	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹)))
56		simprll 775	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ ℝ)
57	56, 50	remulcld 10936	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑥 · (vol‘dom 𝐹)) ∈ ℝ)
58	55, 57	eqeltrd 2839	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ)
59		rexr 10952	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ^*)
60		elxrge0 13118	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (0[,]+∞) ↔ (𝑥 ∈ ℝ^* ∧ 0 ≤ 𝑥))
61	60	biimpri 227	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,]+∞))
62	59, 61	sylan 579	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,]+∞))
63	62	ad2antrl 724	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,]+∞))
64	63	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝑥 ∈ (0[,]+∞))
65		ifcl 4501	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞))
66	64, 44, 65	sylancl 585	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞))
67	66	fmpttd 6971	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞))
68		ifan 4509	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0)
69	1	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐹:dom 𝐹⟶ℂ)
70	69	ffvelrnda 6943	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ)
71	70	recld 14833	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ)
72	70	abscld 15076	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ∈ ℝ)
73	56	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
74	70	releabsd 15091	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
75		2fveq3 6761	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑧 → (abs‘(𝐹‘𝑦)) = (abs‘(𝐹‘𝑧)))
76	75	breq1d 5080	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑧 → ((abs‘(𝐹‘𝑦)) ≤ 𝑥 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑥))
77	76	rspccva 3551	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥)
78	77	adantll 710	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥)
79	78	adantll 710	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥)
80	71, 72, 73, 74, 79	letrd 11062	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ≤ 𝑥)
81		simprlr 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 0 ≤ 𝑥)
82	81	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 0 ≤ 𝑥)
83		breq1 5073	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℜ‘(𝐹‘𝑧)) = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) → ((ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
84		breq1 5073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
85	83, 84	ifboth 4495	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
86	80, 82, 85	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
87		iftrue 4462	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0))
88	87	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0))
89		iftrue 4462	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 𝑥)
90	89	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 𝑥)
91	86, 88, 90	3brtr4d 5102	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
92	91	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
93		0le0 12004	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 0
94	93	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → 0 ≤ 0)
95		iffalse 4465	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) = 0)
96		iffalse 4465	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 0)
97	94, 95, 96	3brtr4d 5102	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
98	92, 97	pm2.61d1 180	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
99	68, 98	eqbrtrid 5105	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
100	99	ralrimivw 3108	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
101		reex 10893	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ V
102	101	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ℝ ∈ V)
103		eqidd 2739	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)))
104		eqidd 2739	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
105	102, 46, 66, 103, 104	ofrfval2 7532	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ 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 256	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
107		itg2le 24809	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞) ∧ (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
108	47, 67, 106, 107	syl3anc 1369	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
109		itg2lecl 24808	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ)
110	47, 58, 108, 109	syl3anc 1369	. . . . . . . . . 10 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ)
111	38	renegcld 11332	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ)
112	111	rexrd 10956	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ^*)
113	112	adantrr 713	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ^*)
114		simprr 769	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → 0 ≤ -(ℜ‘(𝐹‘𝑧)))
115		elxrge0 13118	. . . . . . . . . . . . . 14 ⊢ (-(ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔ (-(ℜ‘(𝐹‘𝑧)) ∈ ℝ^* ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))))
116	113, 114, 115	sylanbrc 582	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → -(ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞))
117	44	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → 0 ∈ (0[,]+∞))
118	116, 117	ifclda 4491	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
119	118	fmpttd 6971	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
120		ifan 4509	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0)
121	71	renegcld 11332	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ)
122	71	recnd 10934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℂ)
123	122	abscld 15076	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹‘𝑧))) ∈ ℝ)
124	121	leabsd 15054	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘-(ℜ‘(𝐹‘𝑧))))
125	122	absnegd 15089	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℜ‘(𝐹‘𝑧))) = (abs‘(ℜ‘(𝐹‘𝑧))))
126	124, 125	breqtrd 5096	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘(ℜ‘(𝐹‘𝑧))))
127		absrele 14948	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑧) ∈ ℂ → (abs‘(ℜ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧)))
128	70, 127	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧)))
129	121, 123, 72, 126, 128	letrd 11062	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
130	121, 72, 73, 129, 79	letrd 11062	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ 𝑥)
131		breq1 5073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-(ℜ‘(𝐹‘𝑧)) = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) → (-(ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
132		breq1 5073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
133	131, 132	ifboth 4495	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-(ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
134	130, 82, 133	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
135		iftrue 4462	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0))
136	135	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0))
137	134, 136, 90	3brtr4d 5102	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
138	137	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
139		iffalse 4465	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) = 0)
140	94, 139, 96	3brtr4d 5102	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
141	138, 140	pm2.61d1 180	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
142	120, 141	eqbrtrid 5105	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
143	142	ralrimivw 3108	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
144		eqidd 2739	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)))
145	102, 118, 66, 144, 104	ofrfval2 7532	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ 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 256	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
147		itg2le 24809	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞) ∧ (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
148	119, 67, 146, 147	syl3anc 1369	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
149		itg2lecl 24808	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ)
150	119, 58, 148, 149	syl3anc 1369	. . . . . . . . . 10 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ)
151	110, 150	jca 511	. . . . . . . . 9 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ ∧ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ))
152	37	imcld 14834	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ)
153	152	rexrd 10956	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ^*)
154	153	adantrr 713	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ^*)
155		simprr 769	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → 0 ≤ (ℑ‘(𝐹‘𝑧)))
156		elxrge0 13118	. . . . . . . . . . . . . 14 ⊢ ((ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔ ((ℑ‘(𝐹‘𝑧)) ∈ ℝ^* ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))))
157	154, 155, 156	sylanbrc 582	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → (ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞))
158	44	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → 0 ∈ (0[,]+∞))
159	157, 158	ifclda 4491	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
160	159	fmpttd 6971	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
161		ifan 4509	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0)
162	70	imcld 14834	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ)
163	162	recnd 10934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℂ)
164	163	abscld 15076	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹‘𝑧))) ∈ ℝ)
165	162	leabsd 15054	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ (abs‘(ℑ‘(𝐹‘𝑧))))
166		absimle 14949	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑧) ∈ ℂ → (abs‘(ℑ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧)))
167	70, 166	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧)))
168	162, 164, 72, 165, 167	letrd 11062	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
169	162, 72, 73, 168, 79	letrd 11062	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ 𝑥)
170		breq1 5073	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℑ‘(𝐹‘𝑧)) = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) → ((ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
171		breq1 5073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
172	170, 171	ifboth 4495	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
173	169, 82, 172	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
174		iftrue 4462	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0))
175	174	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0))
176	173, 175, 90	3brtr4d 5102	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
177	176	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
178		iffalse 4465	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) = 0)
179	94, 178, 96	3brtr4d 5102	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
180	177, 179	pm2.61d1 180	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
181	161, 180	eqbrtrid 5105	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
182	181	ralrimivw 3108	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
183		eqidd 2739	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)))
184	102, 159, 66, 183, 104	ofrfval2 7532	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ 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 256	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
186		itg2le 24809	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞) ∧ (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
187	160, 67, 185, 186	syl3anc 1369	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
188		itg2lecl 24808	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ)
189	160, 58, 187, 188	syl3anc 1369	. . . . . . . . . 10 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ)
190	152	renegcld 11332	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ)
191	190	rexrd 10956	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ^*)
192	191	adantrr 713	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ^*)
193		simprr 769	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → 0 ≤ -(ℑ‘(𝐹‘𝑧)))
194		elxrge0 13118	. . . . . . . . . . . . . 14 ⊢ (-(ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔ (-(ℑ‘(𝐹‘𝑧)) ∈ ℝ^* ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))))
195	192, 193, 194	sylanbrc 582	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → -(ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞))
196	44	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → 0 ∈ (0[,]+∞))
197	195, 196	ifclda 4491	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
198	197	fmpttd 6971	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
199		ifan 4509	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0)
200	162	renegcld 11332	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ)
201	200	leabsd 15054	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘-(ℑ‘(𝐹‘𝑧))))
202	163	absnegd 15089	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℑ‘(𝐹‘𝑧))) = (abs‘(ℑ‘(𝐹‘𝑧))))
203	201, 202	breqtrd 5096	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘(ℑ‘(𝐹‘𝑧))))
204	200, 164, 72, 203, 167	letrd 11062	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
205	200, 72, 73, 204, 79	letrd 11062	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ 𝑥)
206		breq1 5073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-(ℑ‘(𝐹‘𝑧)) = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) → (-(ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
207		breq1 5073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
208	206, 207	ifboth 4495	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-(ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
209	205, 82, 208	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
210		iftrue 4462	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0))
211	210	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0))
212	209, 211, 90	3brtr4d 5102	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
213	212	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
214		iffalse 4465	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) = 0)
215	94, 214, 96	3brtr4d 5102	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
216	213, 215	pm2.61d1 180	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
217	199, 216	eqbrtrid 5105	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
218	217	ralrimivw 3108	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
219		eqidd 2739	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)))
220	102, 197, 66, 219, 104	ofrfval2 7532	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ 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 256	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
222		itg2le 24809	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞) ∧ (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
223	198, 67, 221, 222	syl3anc 1369	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
224		itg2lecl 24808	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ ∧ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ)
225	198, 58, 223, 224	syl3anc 1369	. . . . . . . . . 10 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ)
226	189, 225	jca 511	. . . . . . . . 9 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ ∧ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ))
227		eqid 2738	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)))
228		eqid 2738	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)))
229		eqid 2738	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)))
230		eqid 2738	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)))
231	227, 228, 229, 230, 70	iblcnlem1 24857	. . . . . . . . 9 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹ ↔ ((𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ MblFn ∧ ((∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ ∧ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ) ∧ ((∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ ∧ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ))))
232	35, 151, 226, 231	mpbir3and 1340	. . . . . . . 8 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
233	32, 232	sylan2b 593	. . . . . . 7 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
234	233	anassrs 467	. . . . . 6 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 0 ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
235	31, 234	syldan 590	. . . . 5 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
236	13, 235	pm2.61dane 3031	. . . 4 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
237	236	rexlimdvaa 3213	. . 3 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹))
238	237	3impia 1115	. 2 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
239	3, 238	eqeltrd 2839	1 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿¹)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 Vcvv 3422 ∅c0 4253 ifcif 4456 {csn 4558 class class class wbr 5070 ↦ cmpt 5153 × cxp 5578 dom cdm 5580 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ∘_r cofr 7510 ℂcc 10800 ℝcr 10801 0cc0 10802 · cmul 10807 +∞cpnf 10937 ℝ^*cxr 10939 ≤ cle 10941 -cneg 11136 [,)cico 13010 [,]cicc 13011 ℜcre 14736 ℑcim 14737 abscabs 14873 volcvol 24532 MblFncmbf 24683 ∫₂citg2 24685 𝐿¹cibl 24686

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880 ax-addf 10881

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-disj 5036 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-ofr 7512 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-er 8456 df-map 8575 df-pm 8576 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-inf 9132 df-oi 9199 df-dju 9590 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-z 12250 df-uz 12512 df-q 12618 df-rp 12660 df-xadd 12778 df-ioo 13012 df-ico 13014 df-icc 13015 df-fz 13169 df-fzo 13312 df-fl 13440 df-seq 13650 df-exp 13711 df-hash 13973 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-clim 15125 df-sum 15326 df-xmet 20503 df-met 20504 df-ovol 24533 df-vol 24534 df-mbf 24688 df-itg1 24689 df-itg2 24690 df-ibl 24691 df-0p 24739

This theorem is referenced by: cnicciblnc 24912

W3C validator