bddiblnc

		Ref	Expression
	Assertion	bddiblnc	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to F \in 𝐿^{1}$

Proof

Step	Hyp	Ref	Expression
1		mbff	$⊢ F \in MblFn \to F : dom F ⟶ ℂ$
2	1	feqmptd	$⊢ F \in MblFn \to F = (z \in dom F ⟼ F (z))$
3	2	3ad2ant1	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to F = (z \in dom F ⟼ F (z))$
4		rzal	$⊢ dom F = \emptyset \to \forall z \in dom F F (z) = 0$
5		mpteq12	$⊢ (dom F = \emptyset \land \forall z \in dom F F (z) = 0) \to (z \in dom F ⟼ F (z)) = (z \in \emptyset ⟼ 0)$
6	4 5	mpdan	$⊢ dom F = \emptyset \to (z \in dom F ⟼ F (z)) = (z \in \emptyset ⟼ 0)$
7		fconstmpt	$⊢ \emptyset \times \{0\} = (z \in \emptyset ⟼ 0)$
8		0mbl	$⊢ \emptyset \in dom vol$
9		ibl0	$⊢ \emptyset \in dom vol \to \emptyset \times \{0\} \in 𝐿^{1}$
10	8 9	ax-mp	$⊢ \emptyset \times \{0\} \in 𝐿^{1}$
11	7 10	eqeltrri	$⊢ (z \in \emptyset ⟼ 0) \in 𝐿^{1}$
12	6 11	eqeltrdi	$⊢ dom F = \emptyset \to (z \in dom F ⟼ F (z)) \in 𝐿^{1}$
13	12	adantl	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land (x \in ℝ \land \forall y \in dom F \|F (y)\| \leq x)) \land dom F = \emptyset) \to (z \in dom F ⟼ F (z)) \in 𝐿^{1}$
14		r19.2z	$⊢ (dom F \neq \emptyset \land \forall y \in dom F \|F (y)\| \leq x) \to \exists y \in dom F \|F (y)\| \leq x$
15	14	anim1i	$⊢ ((dom F \neq \emptyset \land \forall y \in dom F \|F (y)\| \leq x) \land x \in ℝ) \to (\exists y \in dom F \|F (y)\| \leq x \land x \in ℝ)$
16	15	an31s	$⊢ ((x \in ℝ \land \forall y \in dom F \|F (y)\| \leq x) \land dom F \neq \emptyset) \to (\exists y \in dom F \|F (y)\| \leq x \land x \in ℝ)$
17	1	ad2antrr	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land x \in ℝ) \to F : dom F ⟶ ℂ$
18	17	ffvelrnda	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land x \in ℝ) \land y \in dom F) \to F (y) \in ℂ$
19	18	absge0d	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land x \in ℝ) \land y \in dom F) \to 0 \leq \|F (y)\|$
20		0red	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land x \in ℝ) \land y \in dom F) \to 0 \in ℝ$
21	18	abscld	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land x \in ℝ) \land y \in dom F) \to \|F (y)\| \in ℝ$
22		simplr	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land x \in ℝ) \land y \in dom F) \to x \in ℝ$
23		letr	$⊢ (0 \in ℝ \land \|F (y)\| \in ℝ \land x \in ℝ) \to ((0 \leq \|F (y)\| \land \|F (y)\| \leq x) \to 0 \leq x)$
24	20 21 22 23	syl3anc	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land x \in ℝ) \land y \in dom F) \to ((0 \leq \|F (y)\| \land \|F (y)\| \leq x) \to 0 \leq x)$
25	19 24	mpand	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land x \in ℝ) \land y \in dom F) \to (\|F (y)\| \leq x \to 0 \leq x)$
26	25	rexlimdva	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land x \in ℝ) \to (\exists y \in dom F \|F (y)\| \leq x \to 0 \leq x)$
27	26	ex	$⊢ (F \in MblFn \land vol (dom F) \in ℝ) \to (x \in ℝ \to (\exists y \in dom F \|F (y)\| \leq x \to 0 \leq x))$
28	27	com23	$⊢ (F \in MblFn \land vol (dom F) \in ℝ) \to (\exists y \in dom F \|F (y)\| \leq x \to (x \in ℝ \to 0 \leq x))$
29	28	imp32	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land (\exists y \in dom F \|F (y)\| \leq x \land x \in ℝ)) \to 0 \leq x$
30	16 29	sylan2	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land \forall y \in dom F \|F (y)\| \leq x) \land dom F \neq \emptyset)) \to 0 \leq x$
31	30	anassrs	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land (x \in ℝ \land \forall y \in dom F \|F (y)\| \leq x)) \land dom F \neq \emptyset) \to 0 \leq x$
32		an32	$⊢ ((x \in ℝ \land \forall y \in dom F \|F (y)\| \leq x) \land 0 \leq x) \leftrightarrow ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)$
33		id	$⊢ F \in MblFn \to F \in MblFn$
34	2 33	eqeltrrd	$⊢ F \in MblFn \to (z \in dom F ⟼ F (z)) \in MblFn$
35	34	ad2antrr	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in dom F ⟼ F (z)) \in MblFn$
36	1	ad3antrrr	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \to F : dom F ⟶ ℂ$
37	36	ffvelrnda	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land z \in dom F) \to F (z) \in ℂ$
38	37	recld	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land z \in dom F) \to ℜ (F (z)) \in ℝ$
39	38	rexrd	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land z \in dom F) \to ℜ (F (z)) \in ℝ^{*}$
40	39	adantrr	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land (z \in dom F \land 0 \leq ℜ (F (z)))) \to ℜ (F (z)) \in ℝ^{*}$
41		simprr	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land (z \in dom F \land 0 \leq ℜ (F (z)))) \to 0 \leq ℜ (F (z))$
42		elxrge0	$⊢ ℜ (F (z)) \in [0, +∞] \leftrightarrow (ℜ (F (z)) \in ℝ^{*} \land 0 \leq ℜ (F (z)))$
43	40 41 42	sylanbrc	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land (z \in dom F \land 0 \leq ℜ (F (z)))) \to ℜ (F (z)) \in [0, +∞]$
44		0e0iccpnf	$⊢ 0 \in [0, +∞]$
45	44	a1i	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land \neg (z \in dom F \land 0 \leq ℜ (F (z)))) \to 0 \in [0, +∞]$
46	43 45	ifclda	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \to if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0) \in [0, +∞]$
47	46	fmpttd	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0)) : ℝ ⟶ [0, +∞]$
48		mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$
49	48	ad2antrr	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to dom F \in dom vol$
50		simplr	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to vol (dom F) \in ℝ$
51		elrege0	$⊢ x \in [0, +∞) \leftrightarrow (x \in ℝ \land 0 \leq x)$
52	51	biimpri	$⊢ (x \in ℝ \land 0 \leq x) \to x \in [0, +∞)$
53	52	ad2antrl	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to x \in [0, +∞)$
54		itg2const	$⊢ (dom F \in dom vol \land vol (dom F) \in ℝ \land x \in [0, +∞)) \to \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0))) = x vol (dom F)$
55	49 50 53 54	syl3anc	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0))) = x vol (dom F)$
56		simprll	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to x \in ℝ$
57	56 50	remulcld	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to x vol (dom F) \in ℝ$
58	55 57	eqeltrd	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0))) \in ℝ$
59		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
60		elxrge0	$⊢ x \in [0, +∞] \leftrightarrow (x \in ℝ^{*} \land 0 \leq x)$
61	60	biimpri	$⊢ (x \in ℝ^{*} \land 0 \leq x) \to x \in [0, +∞]$
62	59 61	sylan	$⊢ (x \in ℝ \land 0 \leq x) \to x \in [0, +∞]$
63	62	ad2antrl	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to x \in [0, +∞]$
64	63	adantr	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \to x \in [0, +∞]$
65		ifcl	$⊢ (x \in [0, +∞] \land 0 \in [0, +∞]) \to if (z \in dom F, x, 0) \in [0, +∞]$
66	64 44 65	sylancl	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \to if (z \in dom F, x, 0) \in [0, +∞]$
67	66	fmpttd	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in ℝ ⟼ if (z \in dom F, x, 0)) : ℝ ⟶ [0, +∞]$
68		ifan	$⊢ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0) = if (z \in dom F, if (0 \leq ℜ (F (z)), ℜ (F (z)), 0), 0)$
69	1	ad2antrr	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to F : dom F ⟶ ℂ$
70	69	ffvelrnda	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to F (z) \in ℂ$
71	70	recld	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to ℜ (F (z)) \in ℝ$
72	70	abscld	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to \|F (z)\| \in ℝ$
73	56	adantr	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to x \in ℝ$
74	70	releabsd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to ℜ (F (z)) \leq \|F (z)\|$
75		2fveq3	$⊢ y = z \to \|F (y)\| = \|F (z)\|$
76	75	breq1d	$⊢ y = z \to (\|F (y)\| \leq x \leftrightarrow \|F (z)\| \leq x)$
77	76	rspccva	$⊢ (\forall y \in dom F \|F (y)\| \leq x \land z \in dom F) \to \|F (z)\| \leq x$
78	77	adantll	$⊢ (((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x) \land z \in dom F) \to \|F (z)\| \leq x$
79	78	adantll	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to \|F (z)\| \leq x$
80	71 72 73 74 79	letrd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to ℜ (F (z)) \leq x$
81		simprlr	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to 0 \leq x$
82	81	adantr	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to 0 \leq x$
83		breq1	$⊢ ℜ (F (z)) = if (0 \leq ℜ (F (z)), ℜ (F (z)), 0) \to (ℜ (F (z)) \leq x \leftrightarrow if (0 \leq ℜ (F (z)), ℜ (F (z)), 0) \leq x)$
84		breq1	$⊢ 0 = if (0 \leq ℜ (F (z)), ℜ (F (z)), 0) \to (0 \leq x \leftrightarrow if (0 \leq ℜ (F (z)), ℜ (F (z)), 0) \leq x)$
85	83 84	ifboth	$⊢ (ℜ (F (z)) \leq x \land 0 \leq x) \to if (0 \leq ℜ (F (z)), ℜ (F (z)), 0) \leq x$
86	80 82 85	syl2anc	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to if (0 \leq ℜ (F (z)), ℜ (F (z)), 0) \leq x$
87		iftrue	$⊢ z \in dom F \to if (z \in dom F, if (0 \leq ℜ (F (z)), ℜ (F (z)), 0), 0) = if (0 \leq ℜ (F (z)), ℜ (F (z)), 0)$
88	87	adantl	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to if (z \in dom F, if (0 \leq ℜ (F (z)), ℜ (F (z)), 0), 0) = if (0 \leq ℜ (F (z)), ℜ (F (z)), 0)$
89		iftrue	$⊢ z \in dom F \to if (z \in dom F, x, 0) = x$
90	89	adantl	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to if (z \in dom F, x, 0) = x$
91	86 88 90	3brtr4d	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to if (z \in dom F, if (0 \leq ℜ (F (z)), ℜ (F (z)), 0), 0) \leq if (z \in dom F, x, 0)$
92	91	ex	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in dom F \to if (z \in dom F, if (0 \leq ℜ (F (z)), ℜ (F (z)), 0), 0) \leq if (z \in dom F, x, 0))$
93		0le0	$⊢ 0 \leq 0$
94	93	a1i	$⊢ \neg z \in dom F \to 0 \leq 0$
95		iffalse	$⊢ \neg z \in dom F \to if (z \in dom F, if (0 \leq ℜ (F (z)), ℜ (F (z)), 0), 0) = 0$
96		iffalse	$⊢ \neg z \in dom F \to if (z \in dom F, x, 0) = 0$
97	94 95 96	3brtr4d	$⊢ \neg z \in dom F \to if (z \in dom F, if (0 \leq ℜ (F (z)), ℜ (F (z)), 0), 0) \leq if (z \in dom F, x, 0)$
98	92 97	pm2.61d1	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to if (z \in dom F, if (0 \leq ℜ (F (z)), ℜ (F (z)), 0), 0) \leq if (z \in dom F, x, 0)$
99	68 98	eqbrtrid	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0) \leq if (z \in dom F, x, 0)$
100	99	ralrimivw	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to \forall z \in ℝ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0) \leq if (z \in dom F, x, 0)$
101		reex	$⊢ ℝ \in V$
102	101	a1i	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to ℝ \in V$
103		eqidd	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0)) = (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0))$
104		eqidd	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in ℝ ⟼ if (z \in dom F, x, 0)) = (z \in ℝ ⟼ if (z \in dom F, x, 0))$
105	102 46 66 103 104	ofrfval2	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0)) \leq_{f} (z \in ℝ ⟼ if (z \in dom F, x, 0)) \leftrightarrow \forall z \in ℝ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0) \leq if (z \in dom F, x, 0))$
106	100 105	mpbird	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0)) \leq_{f} (z \in ℝ ⟼ if (z \in dom F, x, 0))$
107		itg2le	$⊢ ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0)) : ℝ ⟶ [0, +∞] \land (z \in ℝ ⟼ if (z \in dom F, x, 0)) : ℝ ⟶ [0, +∞] \land (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0)) \leq_{f} (z \in ℝ ⟼ if (z \in dom F, x, 0))) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0))) \leq \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0)))$
108	47 67 106 107	syl3anc	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0))) \leq \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0)))$
109		itg2lecl	$⊢ ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0)) : ℝ ⟶ [0, +∞] \land \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0))) \in ℝ \land \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0))) \leq \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0)))) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0))) \in ℝ$
110	47 58 108 109	syl3anc	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0))) \in ℝ$
111	38	renegcld	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land z \in dom F) \to - ℜ (F (z)) \in ℝ$
112	111	rexrd	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land z \in dom F) \to - ℜ (F (z)) \in ℝ^{*}$
113	112	adantrr	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land (z \in dom F \land 0 \leq - ℜ (F (z)))) \to - ℜ (F (z)) \in ℝ^{*}$
114		simprr	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land (z \in dom F \land 0 \leq - ℜ (F (z)))) \to 0 \leq - ℜ (F (z))$
115		elxrge0	$⊢ - ℜ (F (z)) \in [0, +∞] \leftrightarrow (- ℜ (F (z)) \in ℝ^{*} \land 0 \leq - ℜ (F (z)))$
116	113 114 115	sylanbrc	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land (z \in dom F \land 0 \leq - ℜ (F (z)))) \to - ℜ (F (z)) \in [0, +∞]$
117	44	a1i	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land \neg (z \in dom F \land 0 \leq - ℜ (F (z)))) \to 0 \in [0, +∞]$
118	116 117	ifclda	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \to if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0) \in [0, +∞]$
119	118	fmpttd	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0)) : ℝ ⟶ [0, +∞]$
120		ifan	$⊢ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0) = if (z \in dom F, if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0), 0)$
121	71	renegcld	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to - ℜ (F (z)) \in ℝ$
122	71	recnd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to ℜ (F (z)) \in ℂ$
123	122	abscld	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to \|ℜ (F (z))\| \in ℝ$
124	121	leabsd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to - ℜ (F (z)) \leq \|- ℜ (F (z))\|$
125	122	absnegd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to \|- ℜ (F (z))\| = \|ℜ (F (z))\|$
126	124 125	breqtrd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to - ℜ (F (z)) \leq \|ℜ (F (z))\|$
127		absrele	$⊢ F (z) \in ℂ \to \|ℜ (F (z))\| \leq \|F (z)\|$
128	70 127	syl	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to \|ℜ (F (z))\| \leq \|F (z)\|$
129	121 123 72 126 128	letrd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to - ℜ (F (z)) \leq \|F (z)\|$
130	121 72 73 129 79	letrd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to - ℜ (F (z)) \leq x$
131		breq1	$⊢ - ℜ (F (z)) = if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0) \to (- ℜ (F (z)) \leq x \leftrightarrow if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0) \leq x)$
132		breq1	$⊢ 0 = if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0) \to (0 \leq x \leftrightarrow if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0) \leq x)$
133	131 132	ifboth	$⊢ (- ℜ (F (z)) \leq x \land 0 \leq x) \to if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0) \leq x$
134	130 82 133	syl2anc	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0) \leq x$
135		iftrue	$⊢ z \in dom F \to if (z \in dom F, if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0), 0) = if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0)$
136	135	adantl	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to if (z \in dom F, if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0), 0) = if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0)$
137	134 136 90	3brtr4d	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to if (z \in dom F, if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0), 0) \leq if (z \in dom F, x, 0)$
138	137	ex	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in dom F \to if (z \in dom F, if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0), 0) \leq if (z \in dom F, x, 0))$
139		iffalse	$⊢ \neg z \in dom F \to if (z \in dom F, if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0), 0) = 0$
140	94 139 96	3brtr4d	$⊢ \neg z \in dom F \to if (z \in dom F, if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0), 0) \leq if (z \in dom F, x, 0)$
141	138 140	pm2.61d1	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to if (z \in dom F, if (0 \leq - ℜ (F (z)), - ℜ (F (z)), 0), 0) \leq if (z \in dom F, x, 0)$
142	120 141	eqbrtrid	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0) \leq if (z \in dom F, x, 0)$
143	142	ralrimivw	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to \forall z \in ℝ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0) \leq if (z \in dom F, x, 0)$
144		eqidd	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0)) = (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0))$
145	102 118 66 144 104	ofrfval2	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0)) \leq_{f} (z \in ℝ ⟼ if (z \in dom F, x, 0)) \leftrightarrow \forall z \in ℝ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0) \leq if (z \in dom F, x, 0))$
146	143 145	mpbird	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0)) \leq_{f} (z \in ℝ ⟼ if (z \in dom F, x, 0))$
147		itg2le	$⊢ ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0)) : ℝ ⟶ [0, +∞] \land (z \in ℝ ⟼ if (z \in dom F, x, 0)) : ℝ ⟶ [0, +∞] \land (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0)) \leq_{f} (z \in ℝ ⟼ if (z \in dom F, x, 0))) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0))) \leq \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0)))$
148	119 67 146 147	syl3anc	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0))) \leq \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0)))$
149		itg2lecl	$⊢ ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0)) : ℝ ⟶ [0, +∞] \land \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0))) \in ℝ \land \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0))) \leq \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0)))) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0))) \in ℝ$
150	119 58 148 149	syl3anc	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0))) \in ℝ$
151	110 150	jca	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (\int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0))) \in ℝ \land \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0))) \in ℝ)$
152	37	imcld	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land z \in dom F) \to ℑ (F (z)) \in ℝ$
153	152	rexrd	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land z \in dom F) \to ℑ (F (z)) \in ℝ^{*}$
154	153	adantrr	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land (z \in dom F \land 0 \leq ℑ (F (z)))) \to ℑ (F (z)) \in ℝ^{*}$
155		simprr	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land (z \in dom F \land 0 \leq ℑ (F (z)))) \to 0 \leq ℑ (F (z))$
156		elxrge0	$⊢ ℑ (F (z)) \in [0, +∞] \leftrightarrow (ℑ (F (z)) \in ℝ^{*} \land 0 \leq ℑ (F (z)))$
157	154 155 156	sylanbrc	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land (z \in dom F \land 0 \leq ℑ (F (z)))) \to ℑ (F (z)) \in [0, +∞]$
158	44	a1i	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land \neg (z \in dom F \land 0 \leq ℑ (F (z)))) \to 0 \in [0, +∞]$
159	157 158	ifclda	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \to if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0) \in [0, +∞]$
160	159	fmpttd	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0)) : ℝ ⟶ [0, +∞]$
161		ifan	$⊢ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0) = if (z \in dom F, if (0 \leq ℑ (F (z)), ℑ (F (z)), 0), 0)$
162	70	imcld	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to ℑ (F (z)) \in ℝ$
163	162	recnd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to ℑ (F (z)) \in ℂ$
164	163	abscld	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to \|ℑ (F (z))\| \in ℝ$
165	162	leabsd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to ℑ (F (z)) \leq \|ℑ (F (z))\|$
166		absimle	$⊢ F (z) \in ℂ \to \|ℑ (F (z))\| \leq \|F (z)\|$
167	70 166	syl	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to \|ℑ (F (z))\| \leq \|F (z)\|$
168	162 164 72 165 167	letrd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to ℑ (F (z)) \leq \|F (z)\|$
169	162 72 73 168 79	letrd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to ℑ (F (z)) \leq x$
170		breq1	$⊢ ℑ (F (z)) = if (0 \leq ℑ (F (z)), ℑ (F (z)), 0) \to (ℑ (F (z)) \leq x \leftrightarrow if (0 \leq ℑ (F (z)), ℑ (F (z)), 0) \leq x)$
171		breq1	$⊢ 0 = if (0 \leq ℑ (F (z)), ℑ (F (z)), 0) \to (0 \leq x \leftrightarrow if (0 \leq ℑ (F (z)), ℑ (F (z)), 0) \leq x)$
172	170 171	ifboth	$⊢ (ℑ (F (z)) \leq x \land 0 \leq x) \to if (0 \leq ℑ (F (z)), ℑ (F (z)), 0) \leq x$
173	169 82 172	syl2anc	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to if (0 \leq ℑ (F (z)), ℑ (F (z)), 0) \leq x$
174		iftrue	$⊢ z \in dom F \to if (z \in dom F, if (0 \leq ℑ (F (z)), ℑ (F (z)), 0), 0) = if (0 \leq ℑ (F (z)), ℑ (F (z)), 0)$
175	174	adantl	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to if (z \in dom F, if (0 \leq ℑ (F (z)), ℑ (F (z)), 0), 0) = if (0 \leq ℑ (F (z)), ℑ (F (z)), 0)$
176	173 175 90	3brtr4d	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to if (z \in dom F, if (0 \leq ℑ (F (z)), ℑ (F (z)), 0), 0) \leq if (z \in dom F, x, 0)$
177	176	ex	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in dom F \to if (z \in dom F, if (0 \leq ℑ (F (z)), ℑ (F (z)), 0), 0) \leq if (z \in dom F, x, 0))$
178		iffalse	$⊢ \neg z \in dom F \to if (z \in dom F, if (0 \leq ℑ (F (z)), ℑ (F (z)), 0), 0) = 0$
179	94 178 96	3brtr4d	$⊢ \neg z \in dom F \to if (z \in dom F, if (0 \leq ℑ (F (z)), ℑ (F (z)), 0), 0) \leq if (z \in dom F, x, 0)$
180	177 179	pm2.61d1	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to if (z \in dom F, if (0 \leq ℑ (F (z)), ℑ (F (z)), 0), 0) \leq if (z \in dom F, x, 0)$
181	161 180	eqbrtrid	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0) \leq if (z \in dom F, x, 0)$
182	181	ralrimivw	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to \forall z \in ℝ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0) \leq if (z \in dom F, x, 0)$
183		eqidd	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0)) = (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0))$
184	102 159 66 183 104	ofrfval2	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0)) \leq_{f} (z \in ℝ ⟼ if (z \in dom F, x, 0)) \leftrightarrow \forall z \in ℝ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0) \leq if (z \in dom F, x, 0))$
185	182 184	mpbird	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0)) \leq_{f} (z \in ℝ ⟼ if (z \in dom F, x, 0))$
186		itg2le	$⊢ ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0)) : ℝ ⟶ [0, +∞] \land (z \in ℝ ⟼ if (z \in dom F, x, 0)) : ℝ ⟶ [0, +∞] \land (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0)) \leq_{f} (z \in ℝ ⟼ if (z \in dom F, x, 0))) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0))) \leq \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0)))$
187	160 67 185 186	syl3anc	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0))) \leq \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0)))$
188		itg2lecl	$⊢ ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0)) : ℝ ⟶ [0, +∞] \land \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0))) \in ℝ \land \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0))) \leq \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0)))) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0))) \in ℝ$
189	160 58 187 188	syl3anc	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0))) \in ℝ$
190	152	renegcld	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land z \in dom F) \to - ℑ (F (z)) \in ℝ$
191	190	rexrd	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land z \in dom F) \to - ℑ (F (z)) \in ℝ^{*}$
192	191	adantrr	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land (z \in dom F \land 0 \leq - ℑ (F (z)))) \to - ℑ (F (z)) \in ℝ^{*}$
193		simprr	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land (z \in dom F \land 0 \leq - ℑ (F (z)))) \to 0 \leq - ℑ (F (z))$
194		elxrge0	$⊢ - ℑ (F (z)) \in [0, +∞] \leftrightarrow (- ℑ (F (z)) \in ℝ^{*} \land 0 \leq - ℑ (F (z)))$
195	192 193 194	sylanbrc	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land (z \in dom F \land 0 \leq - ℑ (F (z)))) \to - ℑ (F (z)) \in [0, +∞]$
196	44	a1i	$⊢ ((((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \land \neg (z \in dom F \land 0 \leq - ℑ (F (z)))) \to 0 \in [0, +∞]$
197	195 196	ifclda	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in ℝ) \to if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0) \in [0, +∞]$
198	197	fmpttd	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0)) : ℝ ⟶ [0, +∞]$
199		ifan	$⊢ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0) = if (z \in dom F, if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0), 0)$
200	162	renegcld	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to - ℑ (F (z)) \in ℝ$
201	200	leabsd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to - ℑ (F (z)) \leq \|- ℑ (F (z))\|$
202	163	absnegd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to \|- ℑ (F (z))\| = \|ℑ (F (z))\|$
203	201 202	breqtrd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to - ℑ (F (z)) \leq \|ℑ (F (z))\|$
204	200 164 72 203 167	letrd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to - ℑ (F (z)) \leq \|F (z)\|$
205	200 72 73 204 79	letrd	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to - ℑ (F (z)) \leq x$
206		breq1	$⊢ - ℑ (F (z)) = if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0) \to (- ℑ (F (z)) \leq x \leftrightarrow if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0) \leq x)$
207		breq1	$⊢ 0 = if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0) \to (0 \leq x \leftrightarrow if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0) \leq x)$
208	206 207	ifboth	$⊢ (- ℑ (F (z)) \leq x \land 0 \leq x) \to if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0) \leq x$
209	205 82 208	syl2anc	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0) \leq x$
210		iftrue	$⊢ z \in dom F \to if (z \in dom F, if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0), 0) = if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0)$
211	210	adantl	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to if (z \in dom F, if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0), 0) = if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0)$
212	209 211 90	3brtr4d	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \land z \in dom F) \to if (z \in dom F, if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0), 0) \leq if (z \in dom F, x, 0)$
213	212	ex	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in dom F \to if (z \in dom F, if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0), 0) \leq if (z \in dom F, x, 0))$
214		iffalse	$⊢ \neg z \in dom F \to if (z \in dom F, if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0), 0) = 0$
215	94 214 96	3brtr4d	$⊢ \neg z \in dom F \to if (z \in dom F, if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0), 0) \leq if (z \in dom F, x, 0)$
216	213 215	pm2.61d1	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to if (z \in dom F, if (0 \leq - ℑ (F (z)), - ℑ (F (z)), 0), 0) \leq if (z \in dom F, x, 0)$
217	199 216	eqbrtrid	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0) \leq if (z \in dom F, x, 0)$
218	217	ralrimivw	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to \forall z \in ℝ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0) \leq if (z \in dom F, x, 0)$
219		eqidd	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0)) = (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0))$
220	102 197 66 219 104	ofrfval2	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0)) \leq_{f} (z \in ℝ ⟼ if (z \in dom F, x, 0)) \leftrightarrow \forall z \in ℝ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0) \leq if (z \in dom F, x, 0))$
221	218 220	mpbird	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0)) \leq_{f} (z \in ℝ ⟼ if (z \in dom F, x, 0))$
222		itg2le	$⊢ ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0)) : ℝ ⟶ [0, +∞] \land (z \in ℝ ⟼ if (z \in dom F, x, 0)) : ℝ ⟶ [0, +∞] \land (z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0)) \leq_{f} (z \in ℝ ⟼ if (z \in dom F, x, 0))) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0))) \leq \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0)))$
223	198 67 221 222	syl3anc	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0))) \leq \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0)))$
224		itg2lecl	$⊢ ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0)) : ℝ ⟶ [0, +∞] \land \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0))) \in ℝ \land \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0))) \leq \int^{2} ((z \in ℝ ⟼ if (z \in dom F, x, 0)))) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0))) \in ℝ$
225	198 58 223 224	syl3anc	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0))) \in ℝ$
226	189 225	jca	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (\int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0))) \in ℝ \land \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0))) \in ℝ)$
227		eqid	$⊢ \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0))) = \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0)))$
228		eqid	$⊢ \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0))) = \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0)))$
229		eqid	$⊢ \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0))) = \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0)))$
230		eqid	$⊢ \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0))) = \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0)))$
231	227 228 229 230 70	iblcnlem1	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to ((z \in dom F ⟼ F (z)) \in 𝐿^{1} \leftrightarrow ((z \in dom F ⟼ F (z)) \in MblFn \land (\int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℜ (F (z))), ℜ (F (z)), 0))) \in ℝ \land \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℜ (F (z))), - ℜ (F (z)), 0))) \in ℝ) \land (\int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq ℑ (F (z))), ℑ (F (z)), 0))) \in ℝ \land \int^{2} ((z \in ℝ ⟼ if ((z \in dom F \land 0 \leq - ℑ (F (z))), - ℑ (F (z)), 0))) \in ℝ)))$
232	35 151 226 231	mpbir3and	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land 0 \leq x) \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in dom F ⟼ F (z)) \in 𝐿^{1}$
233	32 232	sylan2b	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land ((x \in ℝ \land \forall y \in dom F \|F (y)\| \leq x) \land 0 \leq x)) \to (z \in dom F ⟼ F (z)) \in 𝐿^{1}$
234	233	anassrs	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land (x \in ℝ \land \forall y \in dom F \|F (y)\| \leq x)) \land 0 \leq x) \to (z \in dom F ⟼ F (z)) \in 𝐿^{1}$
235	31 234	syldan	$⊢ (((F \in MblFn \land vol (dom F) \in ℝ) \land (x \in ℝ \land \forall y \in dom F \|F (y)\| \leq x)) \land dom F \neq \emptyset) \to (z \in dom F ⟼ F (z)) \in 𝐿^{1}$
236	13 235	pm2.61dane	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ) \land (x \in ℝ \land \forall y \in dom F \|F (y)\| \leq x)) \to (z \in dom F ⟼ F (z)) \in 𝐿^{1}$
237	236	rexlimdvaa	$⊢ (F \in MblFn \land vol (dom F) \in ℝ) \to (\exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x \to (z \in dom F ⟼ F (z)) \in 𝐿^{1})$
238	237	3impia	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to (z \in dom F ⟼ F (z)) \in 𝐿^{1}$
239	3 238	eqeltrd	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to F \in 𝐿^{1}$

Metamath Proof Explorer

Theorem bddiblnc

Proof