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 26072

Description: Choice-free proof of bddibl 26070. (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 25856	. . . 4 ⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ)
2	1	feqmptd 6947	. . 3 ⊢ (𝐹 ∈ MblFn → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)))
3	2	3ad2ant1 1151	. 2 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)))
4		rzal 4450	. . . . . . . 8 ⊢ (dom 𝐹 = ∅ → ∀𝑧 ∈ dom 𝐹(𝐹‘𝑧) = 0)
5		mpteq12 5193	. . . . . . . 8 ⊢ ((dom 𝐹 = ∅ ∧ ∀𝑧 ∈ dom 𝐹(𝐹‘𝑧) = 0) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) = (𝑧 ∈ ∅ ↦ 0))
6	4, 5	mpdan 700	. . . . . . 7 ⊢ (dom 𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) = (𝑧 ∈ ∅ ↦ 0))
7		fconstmpt 5717	. . . . . . . 8 ⊢ (∅ × {0}) = (𝑧 ∈ ∅ ↦ 0)
8		0mbl 25770	. . . . . . . . 9 ⊢ ∅ ∈ dom vol
9		ibl0 26017	. . . . . . . . 9 ⊢ (∅ ∈ dom vol → (∅ × {0}) ∈ 𝐿¹)
10	8, 9	ax-mp 5	. . . . . . . 8 ⊢ (∅ × {0}) ∈ 𝐿¹
11	7, 10	eqeltrri 2857	. . . . . . 7 ⊢ (𝑧 ∈ ∅ ↦ 0) ∈ 𝐿¹
12	6, 11	eqeltrdi 2868	. . . . . 6 ⊢ (dom 𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
13	12	adantl 487	. . . . 5 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 = ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
14		r19.2z 4455	. . . . . . . . . 10 ⊢ ((dom 𝐹 ≠ ∅ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → ∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)
15	14	anim1i 627	. . . . . . . . 9 ⊢ (((dom 𝐹 ≠ ∅ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑥 ∈ ℝ))
16	15	an31s 667	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑥 ∈ ℝ))
17	1	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝐹:dom 𝐹⟶ℂ)
18	17	ffvelcdmda 7078	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) ∈ ℂ)
19	18	absge0d 15537	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 0 ≤ (abs‘(𝐹‘𝑦)))
20		0red 11238	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 0 ∈ ℝ)
21	18	abscld 15529	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → (abs‘(𝐹‘𝑦)) ∈ ℝ)
22		simplr 781	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
23		letr 11331	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (abs‘(𝐹‘𝑦)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((0 ≤ (abs‘(𝐹‘𝑦)) ∧ (abs‘(𝐹‘𝑦)) ≤ 𝑥) → 0 ≤ 𝑥))
24	20, 21, 22, 23	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → ((0 ≤ (abs‘(𝐹‘𝑦)) ∧ (abs‘(𝐹‘𝑦)) ≤ 𝑥) → 0 ≤ 𝑥))
25	19, 24	mpand 708	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → ((abs‘(𝐹‘𝑦)) ≤ 𝑥 → 0 ≤ 𝑥))
26	25	rexlimdva 3163	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → 0 ≤ 𝑥))
27	26	ex 418	. . . . . . . . . 10 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (𝑥 ∈ ℝ → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → 0 ≤ 𝑥)))
28	27	com23 87	. . . . . . . . 9 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → (𝑥 ∈ ℝ → 0 ≤ 𝑥)))
29	28	imp32 424	. . . . . . . 8 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (∃𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑥 ∈ ℝ)) → 0 ≤ 𝑥)
30	16, 29	sylan2 605	. . . . . . 7 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ dom 𝐹 ≠ ∅)) → 0 ≤ 𝑥)
31	30	anassrs 473	. . . . . 6 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → 0 ≤ 𝑥)
32		an32 659	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥))
33		id 23	. . . . . . . . . . 11 ⊢ (𝐹 ∈ MblFn → 𝐹 ∈ MblFn)
34	2, 33	eqeltrrd 2861	. . . . . . . . . 10 ⊢ (𝐹 ∈ MblFn → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ MblFn)
35	34	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ MblFn)
36	1	ad3antrrr 743	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝐹:dom 𝐹⟶ℂ)
37	36	ffvelcdmda 7078	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ)
38	37	recld 15284	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ)
39	38	rexrd 11286	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ^*)
40	39	adantrr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ^*)
41		simprr 785	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → 0 ≤ (ℜ‘(𝐹‘𝑧)))
42		elxrge0 13513	. . . . . . . . . . . . . 14 ⊢ ((ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔ ((ℜ‘(𝐹‘𝑧)) ∈ ℝ^* ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))))
43	40, 41, 42	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → (ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞))
44		0e0iccpnf 13515	. . . . . . . . . . . . . 14 ⊢ 0 ∈ (0[,]+∞)
45	44	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → 0 ∈ (0[,]+∞))
46	43, 45	ifclda 4518	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
47	46	fmpttd 7109	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
48		mbfdm 25857	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
49	48	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → dom 𝐹 ∈ dom vol)
50		simplr 781	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (vol‘dom 𝐹) ∈ ℝ)
51		elrege0 13510	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
52	51	biimpri 231	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,)+∞))
53	52	ad2antrl 741	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,)+∞))
54		itg2const 25971	. . . . . . . . . . . . 13 ⊢ ((dom 𝐹 ∈ dom vol ∧ (vol‘dom 𝐹) ∈ ℝ ∧ 𝑥 ∈ (0[,)+∞)) → (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹)))
55	49, 50, 53, 54	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) = (𝑥 · (vol‘dom 𝐹)))
56		simprll 791	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ ℝ)
57	56, 50	remulcld 11266	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑥 · (vol‘dom 𝐹)) ∈ ℝ)
58	55, 57	eqeltrd 2860	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ)
59		rexr 11282	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ^*)
60		elxrge0 13513	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (0[,]+∞) ↔ (𝑥 ∈ ℝ^* ∧ 0 ≤ 𝑥))
61	60	biimpri 231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,]+∞))
62	59, 61	sylan 592	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,]+∞))
63	62	ad2antrl 741	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,]+∞))
64	63	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → 𝑥 ∈ (0[,]+∞))
65		ifcl 4528	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞))
66	64, 44, 65	sylancl 598	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) ∈ (0[,]+∞))
67	66	fmpttd 7109	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞))
68		ifan 4536	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0)
69	1	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐹:dom 𝐹⟶ℂ)
70	69	ffvelcdmda 7078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ)
71	70	recld 15284	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ)
72	70	abscld 15529	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ∈ ℝ)
73	56	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
74	70	releabsd 15544	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
75		2fveq3 6884	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑧 → (abs‘(𝐹‘𝑦)) = (abs‘(𝐹‘𝑧)))
76	75	breq1d 5113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑧 → ((abs‘(𝐹‘𝑦)) ≤ 𝑥 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑥))
77	76	rspccva 3575	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥)
78	77	adantll 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥)
79	78	adantll 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥)
80	71, 72, 73, 74, 79	letrd 11394	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ≤ 𝑥)
81		simprlr 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 0 ≤ 𝑥)
82	81	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 0 ≤ 𝑥)
83		breq1 5106	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℜ‘(𝐹‘𝑧)) = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) → ((ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
84		breq1 5106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
85	83, 84	ifboth 4522	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
86	80, 82, 85	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
87		iftrue 4488	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0))
88	87	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0))
89		iftrue 4488	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 𝑥)
90	89	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 𝑥)
91	86, 88, 90	3brtr4d 5137	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
92	91	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
93		0le0 12369	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 0
94	93	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → 0 ≤ 0)
95		iffalse 4491	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) = 0)
96		iffalse 4491	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 0)
97	94, 95, 96	3brtr4d 5137	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
98	92, 97	pm2.61d1 182	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
99	68, 98	eqbrtrid 5140	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
100	99	ralrimivw 3158	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
101		reex 11218	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ V
102	101	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ℝ ∈ V)
103		eqidd 2761	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)))
104		eqidd 2761	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
105	102, 46, 66, 103, 104	ofrfval2 7700	. . . . . . . . . . . . 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 260	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
107		itg2le 25970	. . . . . . . . . . . 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 1398	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
109		itg2lecl 25969	. . . . . . . . . . 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 1398	. . . . . . . . . 10 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ)
111	38	renegcld 11668	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ)
112	111	rexrd 11286	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ^*)
113	112	adantrr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ^*)
114		simprr 785	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧)))) → 0 ≤ -(ℜ‘(𝐹‘𝑧)))
115		elxrge0 13513	. . . . . . . . . . . . . 14 ⊢ (-(ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔ (-(ℜ‘(𝐹‘𝑧)) ∈ ℝ^* ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))))
116	113, 114, 115	sylanbrc 595	. . . . . . . . . . . . 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 4518	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
119	118	fmpttd 7109	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
120		ifan 4536	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0)
121	71	renegcld 11668	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ)
122	71	recnd 11264	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℂ)
123	122	abscld 15529	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹‘𝑧))) ∈ ℝ)
124	121	leabsd 15505	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘-(ℜ‘(𝐹‘𝑧))))
125	122	absnegd 15542	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℜ‘(𝐹‘𝑧))) = (abs‘(ℜ‘(𝐹‘𝑧))))
126	124, 125	breqtrd 5131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘(ℜ‘(𝐹‘𝑧))))
127		absrele 15398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑧) ∈ ℂ → (abs‘(ℜ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧)))
128	70, 127	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧)))
129	121, 123, 72, 126, 128	letrd 11394	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
130	121, 72, 73, 129, 79	letrd 11394	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ 𝑥)
131		breq1 5106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-(ℜ‘(𝐹‘𝑧)) = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) → (-(ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
132		breq1 5106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
133	131, 132	ifboth 4522	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-(ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
134	130, 82, 133	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
135		iftrue 4488	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0))
136	135	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0))
137	134, 136, 90	3brtr4d 5137	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
138	137	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
139		iffalse 4491	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) = 0)
140	94, 139, 96	3brtr4d 5137	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
141	138, 140	pm2.61d1 182	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
142	120, 141	eqbrtrid 5140	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
143	142	ralrimivw 3158	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
144		eqidd 2761	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)))
145	102, 118, 66, 144, 104	ofrfval2 7700	. . . . . . . . . . . . 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 260	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
147		itg2le 25970	. . . . . . . . . . . 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 1398	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
149		itg2lecl 25969	. . . . . . . . . . 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 1398	. . . . . . . . . 10 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ)
151	110, 150	jca 521	. . . . . . . . 9 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ ∧ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) ∈ ℝ))
152	37	imcld 15285	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ)
153	152	rexrd 11286	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ^*)
154	153	adantrr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ^*)
155		simprr 785	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧)))) → 0 ≤ (ℑ‘(𝐹‘𝑧)))
156		elxrge0 13513	. . . . . . . . . . . . . 14 ⊢ ((ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔ ((ℑ‘(𝐹‘𝑧)) ∈ ℝ^* ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))))
157	154, 155, 156	sylanbrc 595	. . . . . . . . . . . . 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 4518	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
160	159	fmpttd 7109	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
161		ifan 4536	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0)
162	70	imcld 15285	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ)
163	162	recnd 11264	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℂ)
164	163	abscld 15529	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹‘𝑧))) ∈ ℝ)
165	162	leabsd 15505	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ (abs‘(ℑ‘(𝐹‘𝑧))))
166		absimle 15399	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑧) ∈ ℂ → (abs‘(ℑ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧)))
167	70, 166	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹‘𝑧))) ≤ (abs‘(𝐹‘𝑧)))
168	162, 164, 72, 165, 167	letrd 11394	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
169	162, 72, 73, 168, 79	letrd 11394	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ 𝑥)
170		breq1 5106	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℑ‘(𝐹‘𝑧)) = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) → ((ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
171		breq1 5106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
172	170, 171	ifboth 4522	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
173	169, 82, 172	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
174		iftrue 4488	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0))
175	174	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0))
176	173, 175, 90	3brtr4d 5137	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
177	176	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
178		iffalse 4491	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) = 0)
179	94, 178, 96	3brtr4d 5137	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
180	177, 179	pm2.61d1 182	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
181	161, 180	eqbrtrid 5140	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
182	181	ralrimivw 3158	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
183		eqidd 2761	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)))
184	102, 159, 66, 183, 104	ofrfval2 7700	. . . . . . . . . . . . 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 260	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
186		itg2le 25970	. . . . . . . . . . . 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 1398	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
188		itg2lecl 25969	. . . . . . . . . . 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 1398	. . . . . . . . . 10 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ)
190	152	renegcld 11668	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ)
191	190	rexrd 11286	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ^*)
192	191	adantrr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ^*)
193		simprr 785	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧)))) → 0 ≤ -(ℑ‘(𝐹‘𝑧)))
194		elxrge0 13513	. . . . . . . . . . . . . 14 ⊢ (-(ℑ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔ (-(ℑ‘(𝐹‘𝑧)) ∈ ℝ^* ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))))
195	192, 193, 194	sylanbrc 595	. . . . . . . . . . . . 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 4518	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
198	197	fmpttd 7109	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
199		ifan 4536	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0)
200	162	renegcld 11668	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ)
201	200	leabsd 15505	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘-(ℑ‘(𝐹‘𝑧))))
202	163	absnegd 15542	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℑ‘(𝐹‘𝑧))) = (abs‘(ℑ‘(𝐹‘𝑧))))
203	201, 202	breqtrd 5131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘(ℑ‘(𝐹‘𝑧))))
204	200, 164, 72, 203, 167	letrd 11394	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
205	200, 72, 73, 204, 79	letrd 11394	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ 𝑥)
206		breq1 5106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-(ℑ‘(𝐹‘𝑧)) = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) → (-(ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
207		breq1 5106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
208	206, 207	ifboth 4522	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-(ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
209	205, 82, 208	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
210		iftrue 4488	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0))
211	210	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0))
212	209, 211, 90	3brtr4d 5137	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
213	212	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
214		iffalse 4491	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) = 0)
215	94, 214, 96	3brtr4d 5137	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
216	213, 215	pm2.61d1 182	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
217	199, 216	eqbrtrid 5140	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
218	217	ralrimivw 3158	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
219		eqidd 2761	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)))
220	102, 197, 66, 219, 104	ofrfval2 7700	. . . . . . . . . . . . 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 260	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) ∘_r ≤ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
222		itg2le 25970	. . . . . . . . . . . 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 1398	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ≤ (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))))
224		itg2lecl 25969	. . . . . . . . . . 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 1398	. . . . . . . . . 10 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ)
226	189, 225	jca 521	. . . . . . . . 9 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ ∧ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) ∈ ℝ))
227		eqid 2760	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)))
228		eqid 2760	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)))
229		eqid 2760	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)))
230		eqid 2760	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)))
231	227, 228, 229, 230, 70	iblcnlem1 26018	. . . . . . . . 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 1361	. . . . . . . 8 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
233	32, 232	sylan2b 606	. . . . . . 7 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ∧ 0 ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
234	233	anassrs 473	. . . . . 6 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 0 ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
235	31, 234	syldan 603	. . . . 5 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 ≠ ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
236	13, 235	pm2.61dane 3042	. . . 4 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
237	236	rexlimdvaa 3164	. . 3 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹))
238	237	3impia 1135	. 2 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
239	3, 238	eqeltrd 2860	1 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿¹)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 Vcvv 3450 ∅c0 4279 ifcif 4482 {csn 4584 class class class wbr 5103 ↦ cmpt 5186 × cxp 5653 dom cdm 5655 ⟶wf 6529 ‘cfv 6533 (class class class)co 7414 ∘_r cofr 7678 ℂcc 11125 ℝcr 11126 0cc0 11127 · cmul 11132 +∞cpnf 11267 ℝ^*cxr 11269 ≤ cle 11271 -cneg 11469 [,)cico 13403 [,]cicc 13404 ℜcre 15187 ℑcim 15188 abscabs 15324 volcvol 25694 MblFncmbf 25845 ∫₂citg2 25847 𝐿¹cibl 25848

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-inf2 9623 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205 ax-addf 11206

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-disj 5071 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-of 7679 df-ofr 7680 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8458 df-2o 8459 df-er 8699 df-map 8831 df-pm 8832 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-sup 9415 df-inf 9416 df-oi 9485 df-dju 9909 df-card 9947 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-n0 12532 df-z 12619 df-uz 12891 df-q 13001 df-rp 13046 df-xadd 13167 df-ioo 13405 df-ico 13407 df-icc 13408 df-fz 13565 df-fzo 13713 df-fl 13856 df-seq 14069 df-exp 14129 df-hash 14398 df-cj 15189 df-re 15190 df-im 15191 df-sqrt 15325 df-abs 15326 df-clim 15578 df-sum 15777 df-xmet 21581 df-met 21582 df-ovol 25695 df-vol 25696 df-mbf 25850 df-itg1 25851 df-itg2 25852 df-ibl 25853 df-0p 25901

This theorem is used by: cnicciblnc 26073

W3C validator