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 26054

Description: Choice-free proof of bddibl 26052. (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 25837	. . . 4 ⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ)
2	1	feqmptd 6953	. . 3 ⊢ (𝐹 ∈ MblFn → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)))
3	2	3ad2ant1 1151	. 2 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)))
4		rzal 4457	. . . . . . . 8 ⊢ (dom 𝐹 = ∅ → ∀𝑧 ∈ dom 𝐹(𝐹‘𝑧) = 0)
5		mpteq12 5201	. . . . . . . 8 ⊢ ((dom 𝐹 = ∅ ∧ ∀𝑧 ∈ dom 𝐹(𝐹‘𝑧) = 0) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) = (𝑧 ∈ ∅ ↦ 0))
6	4, 5	mpdan 700	. . . . . . 7 ⊢ (dom 𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) = (𝑧 ∈ ∅ ↦ 0))
7		fconstmpt 5725	. . . . . . . 8 ⊢ (∅ × {0}) = (𝑧 ∈ ∅ ↦ 0)
8		0mbl 25751	. . . . . . . . 9 ⊢ ∅ ∈ dom vol
9		ibl0 25999	. . . . . . . . 9 ⊢ (∅ ∈ dom vol → (∅ × {0}) ∈ 𝐿¹)
10	8, 9	ax-mp 5	. . . . . . . 8 ⊢ (∅ × {0}) ∈ 𝐿¹
11	7, 10	eqeltrri 2862	. . . . . . 7 ⊢ (𝑧 ∈ ∅ ↦ 0) ∈ 𝐿¹
12	6, 11	eqeltrdi 2873	. . . . . 6 ⊢ (dom 𝐹 = ∅ → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
13	12	adantl 487	. . . . 5 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ dom 𝐹 = ∅) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
14		r19.2z 4462	. . . . . . . . . 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 7083	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) ∈ ℂ)
19	18	absge0d 15524	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 0 ≤ (abs‘(𝐹‘𝑦)))
20		0red 11228	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 0 ∈ ℝ)
21	18	abscld 15516	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → (abs‘(𝐹‘𝑦)) ∈ ℝ)
22		simplr 781	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
23		letr 11321	. . . . . . . . . . . . . 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 3168	. . . . . . . . . . 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 2866	. . . . . . . . . 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 7083	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ)
38	37	recld 15271	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ)
39	38	rexrd 11276	. . . . . . . . . . . . . . 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 13502	. . . . . . . . . . . . . 14 ⊢ ((ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞) ↔ ((ℜ‘(𝐹‘𝑧)) ∈ ℝ^* ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))))
43	40, 41, 42	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → (ℜ‘(𝐹‘𝑧)) ∈ (0[,]+∞))
44		0e0iccpnf 13504	. . . . . . . . . . . . . 14 ⊢ 0 ∈ (0[,]+∞)
45	44	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧)))) → 0 ∈ (0[,]+∞))
46	43, 45	ifclda 4525	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
47	46	fmpttd 7114	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
48		mbfdm 25838	. . . . . . . . . . . . . 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 13499	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
52	51	biimpri 231	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,)+∞))
53	52	ad2antrl 741	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ (0[,)+∞))
54		itg2const 25952	. . . . . . . . . . . . 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 11256	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑥 · (vol‘dom 𝐹)) ∈ ℝ)
58	55, 57	eqeltrd 2865	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫₂‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0))) ∈ ℝ)
59		rexr 11272	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ^*)
60		elxrge0 13502	. . . . . . . . . . . . . . . . . 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 4535	. . . . . . . . . . . . . 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 7114	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)):ℝ⟶(0[,]+∞))
68		ifan 4543	. . . . . . . . . . . . . . 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 7083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ)
71	70	recld 15271	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℝ)
72	70	abscld 15516	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ∈ ℝ)
73	56	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
74	70	releabsd 15531	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
75		2fveq3 6890	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑧 → (abs‘(𝐹‘𝑦)) = (abs‘(𝐹‘𝑧)))
76	75	breq1d 5121	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑧 → ((abs‘(𝐹‘𝑦)) ≤ 𝑥 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑥))
77	76	rspccva 3582	. . . . . . . . . . . . . . . . . . . . . 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 11384	. . . . . . . . . . . . . . . . . . 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 5114	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℜ‘(𝐹‘𝑧)) = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) → ((ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
84		breq1 5114	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
85	83, 84	ifboth 4529	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
86	80, 82, 85	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
87		iftrue 4495	. . . . . . . . . . . . . . . . . . 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 4495	. . . . . . . . . . . . . . . . . . 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 5145	. . . . . . . . . . . . . . . . 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 12359	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 0
94	93	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → 0 ≤ 0)
95		iffalse 4498	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℜ‘(𝐹‘𝑧)), (ℜ‘(𝐹‘𝑧)), 0), 0) = 0)
96		iffalse 4498	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, 𝑥, 0) = 0)
97	94, 95, 96	3brtr4d 5145	. . . . . . . . . . . . . . . 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 5148	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
100	99	ralrimivw 3163	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
101		reex 11208	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ V
102	101	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ℝ ∈ V)
103		eqidd 2766	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)))
104		eqidd 2766	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ dom 𝐹, 𝑥, 0)))
105	102, 46, 66, 103, 104	ofrfval2 7705	. . . . . . . . . . . . 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 25951	. . . . . . . . . . . 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 25950	. . . . . . . . . . 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 11658	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ)
112	111	rexrd 11276	. . . . . . . . . . . . . . 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 13502	. . . . . . . . . . . . . 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 4525	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
119	118	fmpttd 7114	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
120		ifan 4543	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0)
121	71	renegcld 11658	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ∈ ℝ)
122	71	recnd 11254	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℜ‘(𝐹‘𝑧)) ∈ ℂ)
123	122	abscld 15516	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℜ‘(𝐹‘𝑧))) ∈ ℝ)
124	121	leabsd 15492	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘-(ℜ‘(𝐹‘𝑧))))
125	122	absnegd 15529	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℜ‘(𝐹‘𝑧))) = (abs‘(ℜ‘(𝐹‘𝑧))))
126	124, 125	breqtrd 5139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘(ℜ‘(𝐹‘𝑧))))
127		absrele 15385	. . . . . . . . . . . . . . . . . . . . . 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 11384	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
130	121, 72, 73, 129, 79	letrd 11384	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℜ‘(𝐹‘𝑧)) ≤ 𝑥)
131		breq1 5114	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-(ℜ‘(𝐹‘𝑧)) = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) → (-(ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
132		breq1 5114	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
133	131, 132	ifboth 4529	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-(ℜ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
134	130, 82, 133	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
135		iftrue 4495	. . . . . . . . . . . . . . . . . . 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 5145	. . . . . . . . . . . . . . . . 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 4498	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℜ‘(𝐹‘𝑧)), -(ℜ‘(𝐹‘𝑧)), 0), 0) = 0)
140	94, 139, 96	3brtr4d 5145	. . . . . . . . . . . . . . . 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 5148	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
143	142	ralrimivw 3163	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
144		eqidd 2766	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)))
145	102, 118, 66, 144, 104	ofrfval2 7705	. . . . . . . . . . . . 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 25951	. . . . . . . . . . . 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 25950	. . . . . . . . . . 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 15272	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ)
153	152	rexrd 11276	. . . . . . . . . . . . . . 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 13502	. . . . . . . . . . . . . 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 4525	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
160	159	fmpttd 7114	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
161		ifan 4543	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0)
162	70	imcld 15272	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℝ)
163	162	recnd 11254	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ∈ ℂ)
164	163	abscld 15516	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(ℑ‘(𝐹‘𝑧))) ∈ ℝ)
165	162	leabsd 15492	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ (abs‘(ℑ‘(𝐹‘𝑧))))
166		absimle 15386	. . . . . . . . . . . . . . . . . . . . . 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 11384	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
169	162, 72, 73, 168, 79	letrd 11384	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (ℑ‘(𝐹‘𝑧)) ≤ 𝑥)
170		breq1 5114	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℑ‘(𝐹‘𝑧)) = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) → ((ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
171		breq1 5114	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
172	170, 171	ifboth 4529	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
173	169, 82, 172	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
174		iftrue 4495	. . . . . . . . . . . . . . . . . . 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 5145	. . . . . . . . . . . . . . . . 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 4498	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ (ℑ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧)), 0), 0) = 0)
179	94, 178, 96	3brtr4d 5145	. . . . . . . . . . . . . . . 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 5148	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
182	181	ralrimivw 3163	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
183		eqidd 2766	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)))
184	102, 159, 66, 183, 104	ofrfval2 7705	. . . . . . . . . . . . 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 25951	. . . . . . . . . . . 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 25950	. . . . . . . . . . 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 11658	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ)
191	190	rexrd 11276	. . . . . . . . . . . . . . 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 13502	. . . . . . . . . . . . . 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 4525	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ∈ (0[,]+∞))
198	197	fmpttd 7114	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)):ℝ⟶(0[,]+∞))
199		ifan 4543	. . . . . . . . . . . . . . 15 ⊢ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) = if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0)
200	162	renegcld 11658	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ∈ ℝ)
201	200	leabsd 15492	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘-(ℑ‘(𝐹‘𝑧))))
202	163	absnegd 15529	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (abs‘-(ℑ‘(𝐹‘𝑧))) = (abs‘(ℑ‘(𝐹‘𝑧))))
203	201, 202	breqtrd 5139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘(ℑ‘(𝐹‘𝑧))))
204	200, 164, 72, 203, 167	letrd 11384	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑧)))
205	200, 72, 73, 204, 79	letrd 11384	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → -(ℑ‘(𝐹‘𝑧)) ≤ 𝑥)
206		breq1 5114	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-(ℑ‘(𝐹‘𝑧)) = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) → (-(ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
207		breq1 5114	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) → (0 ≤ 𝑥 ↔ if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥))
208	206, 207	ifboth 4529	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-(ℑ‘(𝐹‘𝑧)) ≤ 𝑥 ∧ 0 ≤ 𝑥) → if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
209	205, 82, 208	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0) ≤ 𝑥)
210		iftrue 4495	. . . . . . . . . . . . . . . . . . 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 5145	. . . . . . . . . . . . . . . . 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 4498	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ dom 𝐹 → if(𝑧 ∈ dom 𝐹, if(0 ≤ -(ℑ‘(𝐹‘𝑧)), -(ℑ‘(𝐹‘𝑧)), 0), 0) = 0)
215	94, 214, 96	3brtr4d 5145	. . . . . . . . . . . . . . . 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 5148	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
218	217	ralrimivw 3163	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0) ≤ if(𝑧 ∈ dom 𝐹, 𝑥, 0))
219		eqidd 2766	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)))
220	102, 197, 66, 219, 104	ofrfval2 7705	. . . . . . . . . . . . 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 25951	. . . . . . . . . . . 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 25950	. . . . . . . . . . 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 2765	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘(𝐹‘𝑧))), (ℜ‘(𝐹‘𝑧)), 0)))
228		eqid 2765	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℜ‘(𝐹‘𝑧))), -(ℜ‘(𝐹‘𝑧)), 0)))
229		eqid 2765	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ (ℑ‘(𝐹‘𝑧))), (ℑ‘(𝐹‘𝑧)), 0)))
230		eqid 2765	. . . . . . . . . 10 ⊢ (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0))) = (∫₂‘(𝑧 ∈ ℝ ↦ if((𝑧 ∈ dom 𝐹 ∧ 0 ≤ -(ℑ‘(𝐹‘𝑧))), -(ℑ‘(𝐹‘𝑧)), 0)))
231	227, 228, 229, 230, 70	iblcnlem1 26000	. . . . . . . . 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 3047	. . . 4 ⊢ (((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
237	236	rexlimdvaa 3169	. . 3 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ) → (∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹))
238	237	3impia 1135	. 2 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ∈ 𝐿¹)
239	3, 238	eqeltrd 2865	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 2146 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 Vcvv 3457 ∅c0 4286 ifcif 4489 {csn 4591 class class class wbr 5111 ↦ cmpt 5194 × cxp 5661 dom cdm 5663 ⟶wf 6536 ‘cfv 6540 (class class class)co 7419 ∘_r cofr 7683 ℂcc 11115 ℝcr 11116 0cc0 11117 · cmul 11122 +∞cpnf 11257 ℝ^*cxr 11259 ≤ cle 11261 -cneg 11459 [,)cico 13392 [,]cicc 13393 ℜcre 15174 ℑcim 15175 abscabs 15311 volcvol 25675 MblFncmbf 25826 ∫₂citg2 25828 𝐿¹cibl 25829

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-inf2 9617 ax-cnex 11173 ax-resscn 11174 ax-1cn 11175 ax-icn 11176 ax-addcl 11177 ax-addrcl 11178 ax-mulcl 11179 ax-mulrcl 11180 ax-mulcom 11181 ax-addass 11182 ax-mulass 11183 ax-distr 11184 ax-i2m1 11185 ax-1ne0 11186 ax-1rid 11187 ax-rnegex 11188 ax-rrecex 11189 ax-cnre 11190 ax-pre-lttri 11191 ax-pre-lttrn 11192 ax-pre-ltadd 11193 ax-pre-mulgt0 11194 ax-pre-sup 11195 ax-addf 11196

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 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-disj 5079 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-of 7684 df-ofr 7685 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-pm 8833 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-sup 9409 df-inf 9410 df-oi 9479 df-dju 9903 df-card 9941 df-pnf 11262 df-mnf 11263 df-xr 11264 df-ltxr 11265 df-le 11266 df-sub 11460 df-neg 11461 df-div 11889 df-nn 12251 df-2 12320 df-3 12321 df-n0 12522 df-z 12609 df-uz 12881 df-q 12991 df-rp 13035 df-xadd 13156 df-ioo 13394 df-ico 13396 df-icc 13397 df-fz 13554 df-fzo 13702 df-fl 13845 df-seq 14058 df-exp 14118 df-hash 14387 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-clim 15565 df-sum 15764 df-xmet 21567 df-met 21568 df-ovol 25676 df-vol 25677 df-mbf 25831 df-itg1 25832 df-itg2 25833 df-ibl 25834 df-0p 25882

This theorem is used by: cnicciblnc 26055

W3C validator