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 25801

Description: Choice-free proof of bddibl 25799. (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 25584	. . . 4 ⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ)
2	1	feqmptd 6902	. . 3 ⊢ (𝐹 ∈ MblFn → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)))
3	2	3ad2ant1 1133	. 2 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)))
4		rzal 4447	. . . . . . . 8 ⊢ (dom 𝐹 = ∅ → ∀𝑧 ∈ dom 𝐹(𝐹‘𝑧) = 0)
5		mpteq12 5186	. . . . . . . 8 ⊢ ((dom 𝐹 = ∅ ∧ ∀𝑧 ∈ dom 𝐹(𝐹‘𝑧) = 0) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) = (𝑧 ∈ ∅ ↦ 0))
6	4, 5	mpdan 687	. . . . . . 7 ⊢ (dom 𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) = (𝑧 ∈ ∅ ↦ 0))
7		fconstmpt 5686	. . . . . . . 8 ⊢ (∅ × {0}) = (𝑧 ∈ ∅ ↦ 0)
8		0mbl 25498	. . . . . . . . 9 ⊢ ∅ ∈ dom vol
9		ibl0 25746	. . . . . . . . 9 ⊢ (∅ ∈ dom vol → (∅ × {0}) ∈ 𝐿¹)
10	8, 9	ax-mp 5	. . . . . . . 8 ⊢ (∅ × {0}) ∈ 𝐿¹
11	7, 10	eqeltrri 2833	. . . . . . 7 ⊢ (𝑧 ∈ ∅ ↦ 0) ∈ 𝐿¹
12	6, 11	eqeltrdi 2844	. . . . . 6 ⊢ (dom 𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
13	12	adantl 481	. . . . 5 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 = ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
14		r19.2z 4452	. . . . . . . . . 10 ⊢ ((dom 𝐹 ≠ ∅ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → ∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)
15	14	anim1i 615	. . . . . . . . 9 ⊢ (((dom 𝐹 ≠ ∅ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑥 ∈ ℝ))
16	15	an31s 654	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑥 ∈ ℝ))
17	1	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝐹:dom 𝐹⟶ℂ)
18	17	ffvelcdmda 7029	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) ∈ ℂ)
19	18	absge0d 15372	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 0 ≤ (abs‘(𝐹‘𝑦)))
20		0red 11137	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 0 ∈ ℝ)
21	18	abscld 15364	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → (abs‘(𝐹‘𝑦)) ∈ ℝ)
22		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
23		letr 11229	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (abs‘(𝐹‘𝑦)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((0 ≤ (abs‘(𝐹‘𝑦)) ∧ (abs‘(𝐹‘𝑦)) ≤ 𝑥) → 0 ≤ 𝑥))
24	20, 21, 22, 23	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → ((0 ≤ (abs‘(𝐹‘𝑦)) ∧ (abs‘(𝐹‘𝑦)) ≤ 𝑥) → 0 ≤ 𝑥))
25	19, 24	mpand 695	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → ((abs‘(𝐹‘𝑦)) ≤ 𝑥 → 0 ≤ 𝑥))
26	25	rexlimdva 3137	. . . . . . . . . . 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 593	. . . . . . 7 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅)) → 0 ≤ 𝑥)
31	30	anassrs 467	. . . . . 6 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → 0 ≤ 𝑥)
32		an32 646	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥))
33		id 22	. . . . . . . . . . 11 ⊢ (𝐹 ∈ MblFn → 𝐹 ∈ MblFn)
34	2, 33	eqeltrrd 2837	. . . . . . . . . 10 ⊢ (𝐹 ∈ MblFn → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ MblFn)
35	34	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ MblFn)
36	1	ad3antrrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝐹:dom 𝐹⟶ℂ)
37	36	ffvelcdmda 7029	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ)
38	37	recld 15119	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ)
39	38	rexrd 11184	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ^*)
40	39	adantrr 717	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ^*)
41		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → 0 ≤ (ℜ‘(𝐹‘𝑧)))
42		elxrge0 13375	. . . . . . . . . . . . . 14 ⊢ ((ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔ ((ℜ‘(𝐹‘𝑧)) ∈ ℝ^* ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))))
43	40, 41, 42	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → (ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞))
44		0e0iccpnf 13377	. . . . . . . . . . . . . 14 ⊢ 0 ∈ (0[,]+∞)
45	44	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → 0 ∈ (0[,]+∞))
46	43, 45	ifclda 4515	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
47	46	fmpttd 7060	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
48		mbfdm 25585	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
49	48	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → dom 𝐹 ∈ dom vol)
50		simplr 768	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (vol‘dom 𝐹) ∈ ℝ)
51		elrege0 13372	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
52	51	biimpri 228	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,)+∞))
53	52	ad2antrl 728	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,)+∞))
54		itg2const 25699	. . . . . . . . . . . . 13 ⊢ ((dom 𝐹 ∈ dom vol ∧ (vol‘dom 𝐹) ∈ ℝ ∧ 𝑥 ∈ (0[,)+∞)) → (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹)))
55	49, 50, 53, 54	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹)))
56		simprll 778	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ ℝ)
57	56, 50	remulcld 11164	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑥 · (vol‘dom 𝐹)) ∈ ℝ)
58	55, 57	eqeltrd 2836	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ)
59		rexr 11180	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ^*)
60		elxrge0 13375	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (0[,]+∞) ↔ (𝑥 ∈ ℝ^* ∧ 0 ≤ 𝑥))
61	60	biimpri 228	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,]+∞))
62	59, 61	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,]+∞))
63	62	ad2antrl 728	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,]+∞))
64	63	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝑥 ∈ (0[,]+∞))
65		ifcl 4525	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞))
66	64, 44, 65	sylancl 586	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞))
67	66	fmpttd 7060	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞))
68		ifan 4533	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0)
69	1	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐹:dom 𝐹⟶ℂ)
70	69	ffvelcdmda 7029	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ)
71	70	recld 15119	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ)
72	70	abscld 15364	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ∈ ℝ)
73	56	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
74	70	releabsd 15379	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
75		2fveq3 6839	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑧 → (abs‘(𝐹‘𝑦)) = (abs‘(𝐹‘𝑧)))
76	75	breq1d 5108	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑧 → ((abs‘(𝐹‘𝑦)) ≤ 𝑥 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑥))
77	76	rspccva 3575	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥)
78	77	adantll 714	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥)
79	78	adantll 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥)
80	71, 72, 73, 74, 79	letrd 11292	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ≤ 𝑥)
81		simprlr 779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 0 ≤ 𝑥)
82	81	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 0 ≤ 𝑥)
83		breq1 5101	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℜ‘(𝐹‘𝑧)) = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) → ((ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
84		breq1 5101	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
85	83, 84	ifboth 4519	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
86	80, 82, 85	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
87		iftrue 4485	. . . . . . . . . . . . . . . . . . 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 4485	. . . . . . . . . . . . . . . . . . 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 5130	. . . . . . . . . . . . . . . . 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 12248	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 0
94	93	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → 0 ≤ 0)
95		iffalse 4488	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) = 0)
96		iffalse 4488	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 0)
97	94, 95, 96	3brtr4d 5130	. . . . . . . . . . . . . . . 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 5133	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
100	99	ralrimivw 3132	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
101		reex 11119	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ V
102	101	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ℝ ∈ V)
103		eqidd 2737	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)))
104		eqidd 2737	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
105	102, 46, 66, 103, 104	ofrfval2 7643	. . . . . . . . . . . . 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 257	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
107		itg2le 25698	. . . . . . . . . . . 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 1373	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
109		itg2lecl 25697	. . . . . . . . . . 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 1373	. . . . . . . . . 10 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ)
111	38	renegcld 11566	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ)
112	111	rexrd 11184	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ^*)
113	112	adantrr 717	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ^*)
114		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → 0 ≤ -(ℜ‘(𝐹‘𝑧)))
115		elxrge0 13375	. . . . . . . . . . . . . 14 ⊢ (-(ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔ (-(ℜ‘(𝐹‘𝑧)) ∈ ℝ^* ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))))
116	113, 114, 115	sylanbrc 583	. . . . . . . . . . . . 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 4515	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
119	118	fmpttd 7060	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
120		ifan 4533	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0)
121	71	renegcld 11566	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ)
122	71	recnd 11162	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℂ)
123	122	abscld 15364	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹‘𝑧))) ∈ ℝ)
124	121	leabsd 15340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘-(ℜ‘(𝐹‘𝑧))))
125	122	absnegd 15377	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℜ‘(𝐹‘𝑧))) = (abs‘(ℜ‘(𝐹‘𝑧))))
126	124, 125	breqtrd 5124	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘(ℜ‘(𝐹‘𝑧))))
127		absrele 15233	. . . . . . . . . . . . . . . . . . . . . 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 11292	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
130	121, 72, 73, 129, 79	letrd 11292	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ 𝑥)
131		breq1 5101	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-(ℜ‘(𝐹‘𝑧)) = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) → (-(ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
132		breq1 5101	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
133	131, 132	ifboth 4519	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-(ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
134	130, 82, 133	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
135		iftrue 4485	. . . . . . . . . . . . . . . . . . 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 5130	. . . . . . . . . . . . . . . . 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 4488	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) = 0)
140	94, 139, 96	3brtr4d 5130	. . . . . . . . . . . . . . . 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 5133	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
143	142	ralrimivw 3132	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
144		eqidd 2737	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)))
145	102, 118, 66, 144, 104	ofrfval2 7643	. . . . . . . . . . . . 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 257	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
147		itg2le 25698	. . . . . . . . . . . 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 1373	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
149		itg2lecl 25697	. . . . . . . . . . 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 1373	. . . . . . . . . 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 15120	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ)
153	152	rexrd 11184	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ^*)
154	153	adantrr 717	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ^*)
155		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → 0 ≤ (ℑ‘(𝐹‘𝑧)))
156		elxrge0 13375	. . . . . . . . . . . . . 14 ⊢ ((ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔ ((ℑ‘(𝐹‘𝑧)) ∈ ℝ^* ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))))
157	154, 155, 156	sylanbrc 583	. . . . . . . . . . . . 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 4515	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
160	159	fmpttd 7060	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
161		ifan 4533	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0)
162	70	imcld 15120	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ)
163	162	recnd 11162	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℂ)
164	163	abscld 15364	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹‘𝑧))) ∈ ℝ)
165	162	leabsd 15340	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ (abs‘(ℑ‘(𝐹‘𝑧))))
166		absimle 15234	. . . . . . . . . . . . . . . . . . . . . 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 11292	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
169	162, 72, 73, 168, 79	letrd 11292	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ 𝑥)
170		breq1 5101	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℑ‘(𝐹‘𝑧)) = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) → ((ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
171		breq1 5101	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
172	170, 171	ifboth 4519	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
173	169, 82, 172	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
174		iftrue 4485	. . . . . . . . . . . . . . . . . . 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 5130	. . . . . . . . . . . . . . . . 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 4488	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) = 0)
179	94, 178, 96	3brtr4d 5130	. . . . . . . . . . . . . . . 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 5133	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
182	181	ralrimivw 3132	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
183		eqidd 2737	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)))
184	102, 159, 66, 183, 104	ofrfval2 7643	. . . . . . . . . . . . 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 257	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
186		itg2le 25698	. . . . . . . . . . . 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 1373	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
188		itg2lecl 25697	. . . . . . . . . . 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 1373	. . . . . . . . . 10 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ)
190	152	renegcld 11566	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ)
191	190	rexrd 11184	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ^*)
192	191	adantrr 717	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ^*)
193		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → 0 ≤ -(ℑ‘(𝐹‘𝑧)))
194		elxrge0 13375	. . . . . . . . . . . . . 14 ⊢ (-(ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔ (-(ℑ‘(𝐹‘𝑧)) ∈ ℝ^* ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))))
195	192, 193, 194	sylanbrc 583	. . . . . . . . . . . . 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 4515	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
198	197	fmpttd 7060	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
199		ifan 4533	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0)
200	162	renegcld 11566	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ)
201	200	leabsd 15340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘-(ℑ‘(𝐹‘𝑧))))
202	163	absnegd 15377	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℑ‘(𝐹‘𝑧))) = (abs‘(ℑ‘(𝐹‘𝑧))))
203	201, 202	breqtrd 5124	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘(ℑ‘(𝐹‘𝑧))))
204	200, 164, 72, 203, 167	letrd 11292	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
205	200, 72, 73, 204, 79	letrd 11292	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ 𝑥)
206		breq1 5101	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-(ℑ‘(𝐹‘𝑧)) = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) → (-(ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
207		breq1 5101	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
208	206, 207	ifboth 4519	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-(ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
209	205, 82, 208	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
210		iftrue 4485	. . . . . . . . . . . . . . . . . . 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 5130	. . . . . . . . . . . . . . . . 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 4488	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) = 0)
215	94, 214, 96	3brtr4d 5130	. . . . . . . . . . . . . . . 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 5133	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
218	217	ralrimivw 3132	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
219		eqidd 2737	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)))
220	102, 197, 66, 219, 104	ofrfval2 7643	. . . . . . . . . . . . 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 257	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
222		itg2le 25698	. . . . . . . . . . . 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 1373	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
224		itg2lecl 25697	. . . . . . . . . . 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 1373	. . . . . . . . . 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 2736	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)))
228		eqid 2736	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)))
229		eqid 2736	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)))
230		eqid 2736	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)))
231	227, 228, 229, 230, 70	iblcnlem1 25747	. . . . . . . . 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 1343	. . . . . . . 8 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
233	32, 232	sylan2b 594	. . . . . . 7 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
234	233	anassrs 467	. . . . . 6 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 0 ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
235	31, 234	syldan 591	. . . . 5 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
236	13, 235	pm2.61dane 3019	. . . 4 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
237	236	rexlimdvaa 3138	. . 3 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹))
238	237	3impia 1117	. 2 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
239	3, 238	eqeltrd 2836	1 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿¹)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2932 ∀wral 3051 ∃wrex 3060 Vcvv 3440 ∅c0 4285 ifcif 4479 {csn 4580 class class class wbr 5098 ↦ cmpt 5179 × cxp 5622 dom cdm 5624 ⟶wf 6488 ‘cfv 6492 (class class class)co 7358 ∘_r cofr 7621 ℂcc 11026 ℝcr 11027 0cc0 11028 · cmul 11033 +∞cpnf 11165 ℝ^*cxr 11167 ≤ cle 11169 -cneg 11367 [,)cico 13265 [,]cicc 13266 ℜcre 15022 ℑcim 15023 abscabs 15159 volcvol 25422 MblFncmbf 25573 ∫₂citg2 25575 𝐿¹cibl 25576

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-inf2 9552 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106 ax-addf 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-disj 5066 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-ofr 7623 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-er 8635 df-map 8767 df-pm 8768 df-en 8886 df-dom 8887 df-sdom 8888 df-fin 8889 df-sup 9347 df-inf 9348 df-oi 9417 df-dju 9815 df-card 9853 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12148 df-2 12210 df-3 12211 df-n0 12404 df-z 12491 df-uz 12754 df-q 12864 df-rp 12908 df-xadd 13029 df-ioo 13267 df-ico 13269 df-icc 13270 df-fz 13426 df-fzo 13573 df-fl 13714 df-seq 13927 df-exp 13987 df-hash 14256 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161 df-clim 15413 df-sum 15612 df-xmet 21304 df-met 21305 df-ovol 25423 df-vol 25424 df-mbf 25578 df-itg1 25579 df-itg2 25580 df-ibl 25581 df-0p 25629

This theorem is referenced by: cnicciblnc 25802

W3C validator