ftc1anclem6

Description: Lemma for ftc1anc - construction of simple functions within an arbitrary absolute distance of the given function. Similar to Lemma 565Ib of Fremlin5 p. 218, but without Fremlin's additional step of converting the simple function into a continuous one, which is unnecessary to this lemma's use; also, two simple functions are used to allow for complex-valued F . (Contributed by Brendan Leahy, 31-May-2018)

	Ref	Expression
Hypotheses	ftc1anc.g	$⊢ G = (x \in [A, B] ⟼ \int_{(A, x)} F (t) d t)$
	ftc1anc.a	$⊢ φ \to A \in ℝ$
	ftc1anc.b	$⊢ φ \to B \in ℝ$
	ftc1anc.le	$⊢ φ \to A \leq B$
	ftc1anc.s	$⊢ φ \to (A, B) \subseteq D$
	ftc1anc.d	$⊢ φ \to D \subseteq ℝ$
	ftc1anc.i	$⊢ φ \to F \in 𝐿^{1}$
	ftc1anc.f	$⊢ φ \to F : D ⟶ ℂ$
Assertion	ftc1anclem6	$⊢ (φ \land Y \in ℝ^{+}) \to \exists f \in dom \int^{1} \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < Y$

Proof

Step	Hyp	Ref	Expression
1		ftc1anc.g	$⊢ G = (x \in [A, B] ⟼ \int_{(A, x)} F (t) d t)$
2		ftc1anc.a	$⊢ φ \to A \in ℝ$
3		ftc1anc.b	$⊢ φ \to B \in ℝ$
4		ftc1anc.le	$⊢ φ \to A \leq B$
5		ftc1anc.s	$⊢ φ \to (A, B) \subseteq D$
6		ftc1anc.d	$⊢ φ \to D \subseteq ℝ$
7		ftc1anc.i	$⊢ φ \to F \in 𝐿^{1}$
8		ftc1anc.f	$⊢ φ \to F : D ⟶ ℂ$
9		rphalfcl	$⊢ Y \in ℝ^{+} \to \frac{Y}{2} \in ℝ^{+}$
10	1 2 3 4 5 6 7 8	ftc1anclem5	$⊢ (φ \land \frac{Y}{2} \in ℝ^{+}) \to \exists f \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < \frac{Y}{2}$
11	9 10	sylan2	$⊢ (φ \land Y \in ℝ^{+}) \to \exists f \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < \frac{Y}{2}$
12		eqid	$⊢ (x \in [A, B] ⟼ \int_{(A, x)} (y \in D ⟼ (\frac{1}{i}) F (y)) (t) d t) = (x \in [A, B] ⟼ \int_{(A, x)} (y \in D ⟼ (\frac{1}{i}) F (y)) (t) d t)$
13		ax-icn	$⊢ i \in ℂ$
14		ine0	$⊢ i \neq 0$
15	13 14	reccli	$⊢ \frac{1}{i} \in ℂ$
16	15	a1i	$⊢ φ \to \frac{1}{i} \in ℂ$
17	8	ffvelcdmda	$⊢ (φ \land y \in D) \to F (y) \in ℂ$
18	8	feqmptd	$⊢ φ \to F = (y \in D ⟼ F (y))$
19	18 7	eqeltrrd	$⊢ φ \to (y \in D ⟼ F (y)) \in 𝐿^{1}$
20		divrec2	$⊢ (F (y) \in ℂ \land i \in ℂ \land i \neq 0) \to \frac{F (y)}{i} = (\frac{1}{i}) F (y)$
21	13 14 20	mp3an23	$⊢ F (y) \in ℂ \to \frac{F (y)}{i} = (\frac{1}{i}) F (y)$
22	17 21	syl	$⊢ (φ \land y \in D) \to \frac{F (y)}{i} = (\frac{1}{i}) F (y)$
23	22	mpteq2dva	$⊢ φ \to (y \in D ⟼ \frac{F (y)}{i}) = (y \in D ⟼ (\frac{1}{i}) F (y))$
24		iblmbf	$⊢ (y \in D ⟼ F (y)) \in 𝐿^{1} \to (y \in D ⟼ F (y)) \in MblFn$
25	19 24	syl	$⊢ φ \to (y \in D ⟼ F (y)) \in MblFn$
26		2fveq3	$⊢ y = x \to ℜ (F (y)) = ℜ (F (x))$
27	26	cbvmptv	$⊢ (y \in D ⟼ ℜ (F (y))) = (x \in D ⟼ ℜ (F (x)))$
28	27	eleq1i	$⊢ (y \in D ⟼ ℜ (F (y))) \in MblFn \leftrightarrow (x \in D ⟼ ℜ (F (x))) \in MblFn$
29	17	recld	$⊢ (φ \land y \in D) \to ℜ (F (y)) \in ℝ$
30	29	recnd	$⊢ (φ \land y \in D) \to ℜ (F (y)) \in ℂ$
31	30	adantlr	$⊢ ((φ \land (x \in D ⟼ ℜ (F (x))) \in MblFn) \land y \in D) \to ℜ (F (y)) \in ℂ$
32	28	bilanri	$⊢ (φ \land (x \in D ⟼ ℜ (F (x))) \in MblFn) \to (y \in D ⟼ ℜ (F (y))) \in MblFn$
33	31 32	mbfneg	$⊢ (φ \land (x \in D ⟼ ℜ (F (x))) \in MblFn) \to (y \in D ⟼ - ℜ (F (y))) \in MblFn$
34	28 33	sylan2b	$⊢ (φ \land (y \in D ⟼ ℜ (F (y))) \in MblFn) \to (y \in D ⟼ - ℜ (F (y))) \in MblFn$
35	8	ffvelcdmda	$⊢ (φ \land x \in D) \to F (x) \in ℂ$
36	35	recld	$⊢ (φ \land x \in D) \to ℜ (F (x)) \in ℝ$
37	36	recnd	$⊢ (φ \land x \in D) \to ℜ (F (x)) \in ℂ$
38	37	negnegd	$⊢ (φ \land x \in D) \to - (- ℜ (F (x))) = ℜ (F (x))$
39	38	mpteq2dva	$⊢ φ \to (x \in D ⟼ - (- ℜ (F (x)))) = (x \in D ⟼ ℜ (F (x)))$
40	39 27	eqtr4di	$⊢ φ \to (x \in D ⟼ - (- ℜ (F (x)))) = (y \in D ⟼ ℜ (F (y)))$
41	40	adantr	$⊢ (φ \land (y \in D ⟼ - ℜ (F (y))) \in MblFn) \to (x \in D ⟼ - (- ℜ (F (x)))) = (y \in D ⟼ ℜ (F (y)))$
42		negex	$⊢ - ℜ (F (x)) \in V$
43	42	a1i	$⊢ ((φ \land (y \in D ⟼ - ℜ (F (y))) \in MblFn) \land x \in D) \to - ℜ (F (x)) \in V$
44	26	negeqd	$⊢ y = x \to - ℜ (F (y)) = - ℜ (F (x))$
45	44	cbvmptv	$⊢ (y \in D ⟼ - ℜ (F (y))) = (x \in D ⟼ - ℜ (F (x)))$
46	45	eleq1i	$⊢ (y \in D ⟼ - ℜ (F (y))) \in MblFn \leftrightarrow (x \in D ⟼ - ℜ (F (x))) \in MblFn$
47	46	bilani	$⊢ (φ \land (y \in D ⟼ - ℜ (F (y))) \in MblFn) \to (x \in D ⟼ - ℜ (F (x))) \in MblFn$
48	43 47	mbfneg	$⊢ (φ \land (y \in D ⟼ - ℜ (F (y))) \in MblFn) \to (x \in D ⟼ - (- ℜ (F (x)))) \in MblFn$
49	41 48	eqeltrrd	$⊢ (φ \land (y \in D ⟼ - ℜ (F (y))) \in MblFn) \to (y \in D ⟼ ℜ (F (y))) \in MblFn$
50	34 49	impbida	$⊢ φ \to ((y \in D ⟼ ℜ (F (y))) \in MblFn \leftrightarrow (y \in D ⟼ - ℜ (F (y))) \in MblFn)$
51		divcl	$⊢ (F (y) \in ℂ \land i \in ℂ \land i \neq 0) \to \frac{F (y)}{i} \in ℂ$
52		imre	$⊢ \frac{F (y)}{i} \in ℂ \to ℑ (\frac{F (y)}{i}) = ℜ ((- i) (\frac{F (y)}{i}))$
53	51 52	syl	$⊢ (F (y) \in ℂ \land i \in ℂ \land i \neq 0) \to ℑ (\frac{F (y)}{i}) = ℜ ((- i) (\frac{F (y)}{i}))$
54	13 14 53	mp3an23	$⊢ F (y) \in ℂ \to ℑ (\frac{F (y)}{i}) = ℜ ((- i) (\frac{F (y)}{i}))$
55	13 14 51	mp3an23	$⊢ F (y) \in ℂ \to \frac{F (y)}{i} \in ℂ$
56		mulneg1	$⊢ (i \in ℂ \land \frac{F (y)}{i} \in ℂ) \to (- i) (\frac{F (y)}{i}) = - i (\frac{F (y)}{i})$
57	13 55 56	sylancr	$⊢ F (y) \in ℂ \to (- i) (\frac{F (y)}{i}) = - i (\frac{F (y)}{i})$
58		divcan2	$⊢ (F (y) \in ℂ \land i \in ℂ \land i \neq 0) \to i (\frac{F (y)}{i}) = F (y)$
59	13 14 58	mp3an23	$⊢ F (y) \in ℂ \to i (\frac{F (y)}{i}) = F (y)$
60	59	negeqd	$⊢ F (y) \in ℂ \to - i (\frac{F (y)}{i}) = - F (y)$
61	57 60	eqtrd	$⊢ F (y) \in ℂ \to (- i) (\frac{F (y)}{i}) = - F (y)$
62	61	fveq2d	$⊢ F (y) \in ℂ \to ℜ ((- i) (\frac{F (y)}{i})) = ℜ (- F (y))$
63		reneg	$⊢ F (y) \in ℂ \to ℜ (- F (y)) = - ℜ (F (y))$
64	54 62 63	3eqtrd	$⊢ F (y) \in ℂ \to ℑ (\frac{F (y)}{i}) = - ℜ (F (y))$
65	17 64	syl	$⊢ (φ \land y \in D) \to ℑ (\frac{F (y)}{i}) = - ℜ (F (y))$
66	65	mpteq2dva	$⊢ φ \to (y \in D ⟼ ℑ (\frac{F (y)}{i})) = (y \in D ⟼ - ℜ (F (y)))$
67	66	eleq1d	$⊢ φ \to ((y \in D ⟼ ℑ (\frac{F (y)}{i})) \in MblFn \leftrightarrow (y \in D ⟼ - ℜ (F (y))) \in MblFn)$
68	50 67	bitr4d	$⊢ φ \to ((y \in D ⟼ ℜ (F (y))) \in MblFn \leftrightarrow (y \in D ⟼ ℑ (\frac{F (y)}{i})) \in MblFn)$
69		imval	$⊢ F (y) \in ℂ \to ℑ (F (y)) = ℜ (\frac{F (y)}{i})$
70	17 69	syl	$⊢ (φ \land y \in D) \to ℑ (F (y)) = ℜ (\frac{F (y)}{i})$
71	70	mpteq2dva	$⊢ φ \to (y \in D ⟼ ℑ (F (y))) = (y \in D ⟼ ℜ (\frac{F (y)}{i}))$
72	71	eleq1d	$⊢ φ \to ((y \in D ⟼ ℑ (F (y))) \in MblFn \leftrightarrow (y \in D ⟼ ℜ (\frac{F (y)}{i})) \in MblFn)$
73	68 72	anbi12d	$⊢ φ \to (((y \in D ⟼ ℜ (F (y))) \in MblFn \land (y \in D ⟼ ℑ (F (y))) \in MblFn) \leftrightarrow ((y \in D ⟼ ℑ (\frac{F (y)}{i})) \in MblFn \land (y \in D ⟼ ℜ (\frac{F (y)}{i})) \in MblFn))$
74		ancom	$⊢ ((y \in D ⟼ ℑ (\frac{F (y)}{i})) \in MblFn \land (y \in D ⟼ ℜ (\frac{F (y)}{i})) \in MblFn) \leftrightarrow ((y \in D ⟼ ℜ (\frac{F (y)}{i})) \in MblFn \land (y \in D ⟼ ℑ (\frac{F (y)}{i})) \in MblFn)$
75	73 74	bitrdi	$⊢ φ \to (((y \in D ⟼ ℜ (F (y))) \in MblFn \land (y \in D ⟼ ℑ (F (y))) \in MblFn) \leftrightarrow ((y \in D ⟼ ℜ (\frac{F (y)}{i})) \in MblFn \land (y \in D ⟼ ℑ (\frac{F (y)}{i})) \in MblFn))$
76	17	ismbfcn2	$⊢ φ \to ((y \in D ⟼ F (y)) \in MblFn \leftrightarrow ((y \in D ⟼ ℜ (F (y))) \in MblFn \land (y \in D ⟼ ℑ (F (y))) \in MblFn))$
77	17 55	syl	$⊢ (φ \land y \in D) \to \frac{F (y)}{i} \in ℂ$
78	77	ismbfcn2	$⊢ φ \to ((y \in D ⟼ \frac{F (y)}{i}) \in MblFn \leftrightarrow ((y \in D ⟼ ℜ (\frac{F (y)}{i})) \in MblFn \land (y \in D ⟼ ℑ (\frac{F (y)}{i})) \in MblFn))$
79	75 76 78	3bitr4d	$⊢ φ \to ((y \in D ⟼ F (y)) \in MblFn \leftrightarrow (y \in D ⟼ \frac{F (y)}{i}) \in MblFn)$
80	25 79	mpbid	$⊢ φ \to (y \in D ⟼ \frac{F (y)}{i}) \in MblFn$
81	23 80	eqeltrrd	$⊢ φ \to (y \in D ⟼ (\frac{1}{i}) F (y)) \in MblFn$
82	16 17 19 81	iblmulc2nc	$⊢ φ \to (y \in D ⟼ (\frac{1}{i}) F (y)) \in 𝐿^{1}$
83		mulcl	$⊢ (\frac{1}{i} \in ℂ \land F (y) \in ℂ) \to (\frac{1}{i}) F (y) \in ℂ$
84	15 17 83	sylancr	$⊢ (φ \land y \in D) \to (\frac{1}{i}) F (y) \in ℂ$
85	84	fmpttd	$⊢ φ \to (y \in D ⟼ (\frac{1}{i}) F (y)) : D ⟶ ℂ$
86	12 2 3 4 5 6 82 85	ftc1anclem5	$⊢ (φ \land \frac{Y}{2} \in ℝ^{+}) \to \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, (y \in D ⟼ (\frac{1}{i}) F (y)) (t), 0)) - g (t)\|)) < \frac{Y}{2}$
87	9 86	sylan2	$⊢ (φ \land Y \in ℝ^{+}) \to \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, (y \in D ⟼ (\frac{1}{i}) F (y)) (t), 0)) - g (t)\|)) < \frac{Y}{2}$
88	8	ffvelcdmda	$⊢ (φ \land t \in D) \to F (t) \in ℂ$
89		0cnd	$⊢ (φ \land \neg t \in D) \to 0 \in ℂ$
90	88 89	ifclda	$⊢ φ \to if (t \in D, F (t), 0) \in ℂ$
91		imval	$⊢ if (t \in D, F (t), 0) \in ℂ \to ℑ (if (t \in D, F (t), 0)) = ℜ (\frac{if (t \in D, F (t), 0)}{i})$
92	90 91	syl	$⊢ φ \to ℑ (if (t \in D, F (t), 0)) = ℜ (\frac{if (t \in D, F (t), 0)}{i})$
93		fveq2	$⊢ y = t \to F (y) = F (t)$
94	93	oveq2d	$⊢ y = t \to (\frac{1}{i}) F (y) = (\frac{1}{i}) F (t)$
95		eqid	$⊢ (y \in D ⟼ (\frac{1}{i}) F (y)) = (y \in D ⟼ (\frac{1}{i}) F (y))$
96		ovex	$⊢ (\frac{1}{i}) F (t) \in V$
97	94 95 96	fvmpt	$⊢ t \in D \to (y \in D ⟼ (\frac{1}{i}) F (y)) (t) = (\frac{1}{i}) F (t)$
98	97	adantl	$⊢ (φ \land t \in D) \to (y \in D ⟼ (\frac{1}{i}) F (y)) (t) = (\frac{1}{i}) F (t)$
99		divrec2	$⊢ (F (t) \in ℂ \land i \in ℂ \land i \neq 0) \to \frac{F (t)}{i} = (\frac{1}{i}) F (t)$
100	13 14 99	mp3an23	$⊢ F (t) \in ℂ \to \frac{F (t)}{i} = (\frac{1}{i}) F (t)$
101	88 100	syl	$⊢ (φ \land t \in D) \to \frac{F (t)}{i} = (\frac{1}{i}) F (t)$
102	98 101	eqtr4d	$⊢ (φ \land t \in D) \to (y \in D ⟼ (\frac{1}{i}) F (y)) (t) = \frac{F (t)}{i}$
103	102	ifeq1da	$⊢ φ \to if (t \in D, (y \in D ⟼ (\frac{1}{i}) F (y)) (t), 0) = if (t \in D, \frac{F (t)}{i}, 0)$
104		ovif	$⊢ \frac{if (t \in D, F (t), 0)}{i} = if (t \in D, \frac{F (t)}{i}, \frac{0}{i})$
105	13 14	div0i	$⊢ \frac{0}{i} = 0$
106		ifeq2	$⊢ \frac{0}{i} = 0 \to if (t \in D, \frac{F (t)}{i}, \frac{0}{i}) = if (t \in D, \frac{F (t)}{i}, 0)$
107	105 106	ax-mp	$⊢ if (t \in D, \frac{F (t)}{i}, \frac{0}{i}) = if (t \in D, \frac{F (t)}{i}, 0)$
108	104 107	eqtri	$⊢ \frac{if (t \in D, F (t), 0)}{i} = if (t \in D, \frac{F (t)}{i}, 0)$
109	103 108	eqtr4di	$⊢ φ \to if (t \in D, (y \in D ⟼ (\frac{1}{i}) F (y)) (t), 0) = \frac{if (t \in D, F (t), 0)}{i}$
110	109	fveq2d	$⊢ φ \to ℜ (if (t \in D, (y \in D ⟼ (\frac{1}{i}) F (y)) (t), 0)) = ℜ (\frac{if (t \in D, F (t), 0)}{i})$
111	92 110	eqtr4d	$⊢ φ \to ℑ (if (t \in D, F (t), 0)) = ℜ (if (t \in D, (y \in D ⟼ (\frac{1}{i}) F (y)) (t), 0))$
112	111	fvoveq1d	$⊢ φ \to \|ℑ (if (t \in D, F (t), 0)) - g (t)\| = \|ℜ (if (t \in D, (y \in D ⟼ (\frac{1}{i}) F (y)) (t), 0)) - g (t)\|$
113	112	mpteq2dv	$⊢ φ \to (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|) = (t \in ℝ ⟼ \|ℜ (if (t \in D, (y \in D ⟼ (\frac{1}{i}) F (y)) (t), 0)) - g (t)\|)$
114	113	fveq2d	$⊢ φ \to \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) = \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, (y \in D ⟼ (\frac{1}{i}) F (y)) (t), 0)) - g (t)\|))$
115	114	breq1d	$⊢ φ \to (\int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < \frac{Y}{2} \leftrightarrow \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, (y \in D ⟼ (\frac{1}{i}) F (y)) (t), 0)) - g (t)\|)) < \frac{Y}{2})$
116	115	rexbidv	$⊢ φ \to (\exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < \frac{Y}{2} \leftrightarrow \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, (y \in D ⟼ (\frac{1}{i}) F (y)) (t), 0)) - g (t)\|)) < \frac{Y}{2})$
117	116	adantr	$⊢ (φ \land Y \in ℝ^{+}) \to (\exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < \frac{Y}{2} \leftrightarrow \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, (y \in D ⟼ (\frac{1}{i}) F (y)) (t), 0)) - g (t)\|)) < \frac{Y}{2})$
118	87 117	mpbird	$⊢ (φ \land Y \in ℝ^{+}) \to \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < \frac{Y}{2}$
119		reeanv	$⊢ \exists f \in dom \int^{1} \exists g \in dom \int^{1} (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < \frac{Y}{2} \land \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < \frac{Y}{2}) \leftrightarrow (\exists f \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < \frac{Y}{2} \land \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < \frac{Y}{2})$
120		eleq1w	$⊢ x = t \to (x \in D \leftrightarrow t \in D)$
121		fveq2	$⊢ x = t \to F (x) = F (t)$
122	120 121	ifbieq1d	$⊢ x = t \to if (x \in D, F (x), 0) = if (t \in D, F (t), 0)$
123	122	fveq2d	$⊢ x = t \to ℜ (if (x \in D, F (x), 0)) = ℜ (if (t \in D, F (t), 0))$
124		eqid	$⊢ (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) = (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0)))$
125		fvex	$⊢ ℜ (if (t \in D, F (t), 0)) \in V$
126	123 124 125	fvmpt	$⊢ t \in ℝ \to (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) = ℜ (if (t \in D, F (t), 0))$
127	126	fvoveq1d	$⊢ t \in ℝ \to \|(x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) - f (t)\| = \|ℜ (if (t \in D, F (t), 0)) - f (t)\|$
128	127	mpteq2ia	$⊢ (t \in ℝ ⟼ \|(x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) - f (t)\|) = (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)$
129	128	fveq2i	$⊢ \int^{2} ((t \in ℝ ⟼ \|(x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) - f (t)\|)) = \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|))$
130		rembl	$⊢ ℝ \in dom vol$
131	130	a1i	$⊢ φ \to ℝ \in dom vol$
132		0cnd	$⊢ (φ \land \neg x \in D) \to 0 \in ℂ$
133	35 132	ifclda	$⊢ φ \to if (x \in D, F (x), 0) \in ℂ$
134	133	adantr	$⊢ (φ \land x \in D) \to if (x \in D, F (x), 0) \in ℂ$
135		eldifn	$⊢ x \in (ℝ ∖ D) \to \neg x \in D$
136	135	adantl	$⊢ (φ \land x \in (ℝ ∖ D)) \to \neg x \in D$
137	136	iffalsed	$⊢ (φ \land x \in (ℝ ∖ D)) \to if (x \in D, F (x), 0) = 0$
138	8	feqmptd	$⊢ φ \to F = (x \in D ⟼ F (x))$
139		iftrue	$⊢ x \in D \to if (x \in D, F (x), 0) = F (x)$
140	139	mpteq2ia	$⊢ (x \in D ⟼ if (x \in D, F (x), 0)) = (x \in D ⟼ F (x))$
141	138 140	eqtr4di	$⊢ φ \to F = (x \in D ⟼ if (x \in D, F (x), 0))$
142	141 7	eqeltrrd	$⊢ φ \to (x \in D ⟼ if (x \in D, F (x), 0)) \in 𝐿^{1}$
143	6 131 134 137 142	iblss2	$⊢ φ \to (x \in ℝ ⟼ if (x \in D, F (x), 0)) \in 𝐿^{1}$
144	133	adantr	$⊢ (φ \land x \in ℝ) \to if (x \in D, F (x), 0) \in ℂ$
145	144	iblcn	$⊢ φ \to ((x \in ℝ ⟼ if (x \in D, F (x), 0)) \in 𝐿^{1} \leftrightarrow ((x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) \in 𝐿^{1} \land (x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) \in 𝐿^{1}))$
146	143 145	mpbid	$⊢ φ \to ((x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) \in 𝐿^{1} \land (x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) \in 𝐿^{1})$
147	146	simpld	$⊢ φ \to (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) \in 𝐿^{1}$
148	144	recld	$⊢ (φ \land x \in ℝ) \to ℜ (if (x \in D, F (x), 0)) \in ℝ$
149	148	fmpttd	$⊢ φ \to (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) : ℝ ⟶ ℝ$
150	147 149	jca	$⊢ φ \to ((x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) \in 𝐿^{1} \land (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) : ℝ ⟶ ℝ)$
151		ftc1anclem4	$⊢ (f \in dom \int^{1} \land (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) \in 𝐿^{1} \land (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ \|(x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) - f (t)\|)) \in ℝ$
152	151	3expb	$⊢ (f \in dom \int^{1} \land ((x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) \in 𝐿^{1} \land (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) : ℝ ⟶ ℝ)) \to \int^{2} ((t \in ℝ ⟼ \|(x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) - f (t)\|)) \in ℝ$
153	150 152	sylan2	$⊢ (f \in dom \int^{1} \land φ) \to \int^{2} ((t \in ℝ ⟼ \|(x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) - f (t)\|)) \in ℝ$
154	153	ancoms	$⊢ (φ \land f \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ \|(x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) - f (t)\|)) \in ℝ$
155	129 154	eqeltrrid	$⊢ (φ \land f \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) \in ℝ$
156	122	fveq2d	$⊢ x = t \to ℑ (if (x \in D, F (x), 0)) = ℑ (if (t \in D, F (t), 0))$
157		eqid	$⊢ (x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) = (x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0)))$
158		fvex	$⊢ ℑ (if (t \in D, F (t), 0)) \in V$
159	156 157 158	fvmpt	$⊢ t \in ℝ \to (x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) (t) = ℑ (if (t \in D, F (t), 0))$
160	159	fvoveq1d	$⊢ t \in ℝ \to \|(x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) (t) - g (t)\| = \|ℑ (if (t \in D, F (t), 0)) - g (t)\|$
161	160	mpteq2ia	$⊢ (t \in ℝ ⟼ \|(x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) (t) - g (t)\|) = (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)$
162	161	fveq2i	$⊢ \int^{2} ((t \in ℝ ⟼ \|(x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) (t) - g (t)\|)) = \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|))$
163	146	simprd	$⊢ φ \to (x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) \in 𝐿^{1}$
164	133	imcld	$⊢ φ \to ℑ (if (x \in D, F (x), 0)) \in ℝ$
165	164	adantr	$⊢ (φ \land x \in ℝ) \to ℑ (if (x \in D, F (x), 0)) \in ℝ$
166	165	fmpttd	$⊢ φ \to (x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) : ℝ ⟶ ℝ$
167	163 166	jca	$⊢ φ \to ((x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) \in 𝐿^{1} \land (x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) : ℝ ⟶ ℝ)$
168		ftc1anclem4	$⊢ (g \in dom \int^{1} \land (x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) \in 𝐿^{1} \land (x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ \|(x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) (t) - g (t)\|)) \in ℝ$
169	168	3expb	$⊢ (g \in dom \int^{1} \land ((x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) \in 𝐿^{1} \land (x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) : ℝ ⟶ ℝ)) \to \int^{2} ((t \in ℝ ⟼ \|(x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) (t) - g (t)\|)) \in ℝ$
170	167 169	sylan2	$⊢ (g \in dom \int^{1} \land φ) \to \int^{2} ((t \in ℝ ⟼ \|(x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) (t) - g (t)\|)) \in ℝ$
171	170	ancoms	$⊢ (φ \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ \|(x \in ℝ ⟼ ℑ (if (x \in D, F (x), 0))) (t) - g (t)\|)) \in ℝ$
172	162 171	eqeltrrid	$⊢ (φ \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) \in ℝ$
173	155 172	anim12dan	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) \in ℝ \land \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) \in ℝ)$
174	9	rpred	$⊢ Y \in ℝ^{+} \to \frac{Y}{2} \in ℝ$
175	174 174	jca	$⊢ Y \in ℝ^{+} \to (\frac{Y}{2} \in ℝ \land \frac{Y}{2} \in ℝ)$
176		lt2add	$⊢ ((\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) \in ℝ \land \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) \in ℝ) \land (\frac{Y}{2} \in ℝ \land \frac{Y}{2} \in ℝ)) \to ((\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < \frac{Y}{2} \land \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < \frac{Y}{2}) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < (\frac{Y}{2}) + (\frac{Y}{2}))$
177	173 175 176	syl2an	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land Y \in ℝ^{+}) \to ((\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < \frac{Y}{2} \land \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < \frac{Y}{2}) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < (\frac{Y}{2}) + (\frac{Y}{2}))$
178	177	an32s	$⊢ ((φ \land Y \in ℝ^{+}) \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to ((\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < \frac{Y}{2} \land \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < \frac{Y}{2}) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < (\frac{Y}{2}) + (\frac{Y}{2}))$
179	90	recld	$⊢ φ \to ℜ (if (t \in D, F (t), 0)) \in ℝ$
180	179	recnd	$⊢ φ \to ℜ (if (t \in D, F (t), 0)) \in ℂ$
181		i1ff	$⊢ f \in dom \int^{1} \to f : ℝ ⟶ ℝ$
182	181	ffvelcdmda	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to f (t) \in ℝ$
183	182	recnd	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to f (t) \in ℂ$
184		subcl	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℂ \land f (t) \in ℂ) \to ℜ (if (t \in D, F (t), 0)) - f (t) \in ℂ$
185	180 183 184	syl2an	$⊢ (φ \land (f \in dom \int^{1} \land t \in ℝ)) \to ℜ (if (t \in D, F (t), 0)) - f (t) \in ℂ$
186	185	anassrs	$⊢ ((φ \land f \in dom \int^{1}) \land t \in ℝ) \to ℜ (if (t \in D, F (t), 0)) - f (t) \in ℂ$
187	186	adantlrr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to ℜ (if (t \in D, F (t), 0)) - f (t) \in ℂ$
188	90	imcld	$⊢ φ \to ℑ (if (t \in D, F (t), 0)) \in ℝ$
189	188	recnd	$⊢ φ \to ℑ (if (t \in D, F (t), 0)) \in ℂ$
190		i1ff	$⊢ g \in dom \int^{1} \to g : ℝ ⟶ ℝ$
191	190	ffvelcdmda	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) \in ℝ$
192	191	recnd	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) \in ℂ$
193		subcl	$⊢ (ℑ (if (t \in D, F (t), 0)) \in ℂ \land g (t) \in ℂ) \to ℑ (if (t \in D, F (t), 0)) - g (t) \in ℂ$
194	189 192 193	syl2an	$⊢ (φ \land (g \in dom \int^{1} \land t \in ℝ)) \to ℑ (if (t \in D, F (t), 0)) - g (t) \in ℂ$
195	194	anassrs	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to ℑ (if (t \in D, F (t), 0)) - g (t) \in ℂ$
196		mulcl	$⊢ (i \in ℂ \land ℑ (if (t \in D, F (t), 0)) - g (t) \in ℂ) \to i (ℑ (if (t \in D, F (t), 0)) - g (t)) \in ℂ$
197	13 195 196	sylancr	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to i (ℑ (if (t \in D, F (t), 0)) - g (t)) \in ℂ$
198	197	adantlrl	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to i (ℑ (if (t \in D, F (t), 0)) - g (t)) \in ℂ$
199	187 198	addcld	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t)) \in ℂ$
200	199	abscld	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\| \in ℝ$
201	200	rexrd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\| \in ℝ^{*}$
202	199	absge0d	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to 0 \leq \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|$
203		elxrge0	$⊢ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\| \in [0, +∞] \leftrightarrow (\|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\| \in ℝ^{*} \land 0 \leq \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)$
204	201 202 203	sylanbrc	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\| \in [0, +∞]$
205	204	fmpttd	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|) : ℝ ⟶ [0, +∞]$
206		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
207		ge0addcl	$⊢ (x \in [0, +∞) \land y \in [0, +∞)) \to x + y \in [0, +∞)$
208	206 207	sselid	$⊢ (x \in [0, +∞) \land y \in [0, +∞)) \to x + y \in [0, +∞]$
209	208	adantl	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (x \in [0, +∞) \land y \in [0, +∞))) \to x + y \in [0, +∞]$
210	186	abscld	$⊢ ((φ \land f \in dom \int^{1}) \land t \in ℝ) \to \|ℜ (if (t \in D, F (t), 0)) - f (t)\| \in ℝ$
211	186	absge0d	$⊢ ((φ \land f \in dom \int^{1}) \land t \in ℝ) \to 0 \leq \|ℜ (if (t \in D, F (t), 0)) - f (t)\|$
212		elrege0	$⊢ \|ℜ (if (t \in D, F (t), 0)) - f (t)\| \in [0, +∞) \leftrightarrow (\|ℜ (if (t \in D, F (t), 0)) - f (t)\| \in ℝ \land 0 \leq \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)$
213	210 211 212	sylanbrc	$⊢ ((φ \land f \in dom \int^{1}) \land t \in ℝ) \to \|ℜ (if (t \in D, F (t), 0)) - f (t)\| \in [0, +∞)$
214	213	fmpttd	$⊢ (φ \land f \in dom \int^{1}) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) : ℝ ⟶ [0, +∞)$
215	214	adantrr	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) : ℝ ⟶ [0, +∞)$
216	195	abscld	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to \|ℑ (if (t \in D, F (t), 0)) - g (t)\| \in ℝ$
217	195	absge0d	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to 0 \leq \|ℑ (if (t \in D, F (t), 0)) - g (t)\|$
218		elrege0	$⊢ \|ℑ (if (t \in D, F (t), 0)) - g (t)\| \in [0, +∞) \leftrightarrow (\|ℑ (if (t \in D, F (t), 0)) - g (t)\| \in ℝ \land 0 \leq \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)$
219	216 217 218	sylanbrc	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to \|ℑ (if (t \in D, F (t), 0)) - g (t)\| \in [0, +∞)$
220	219	fmpttd	$⊢ (φ \land g \in dom \int^{1}) \to (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|) : ℝ ⟶ [0, +∞)$
221	220	adantrl	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|) : ℝ ⟶ [0, +∞)$
222		reex	$⊢ ℝ \in V$
223	222	a1i	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to ℝ \in V$
224		inidm	$⊢ ℝ \cap ℝ = ℝ$
225	209 215 221 223 223 224	off	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) +_{f} (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) : ℝ ⟶ [0, +∞]$
226	187 198	abstrid	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\| \leq \|ℜ (if (t \in D, F (t), 0)) - f (t)\| + \|i (ℑ (if (t \in D, F (t), 0)) - g (t))\|$
227	226	ralrimiva	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \forall t \in ℝ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\| \leq \|ℜ (if (t \in D, F (t), 0)) - f (t)\| + \|i (ℑ (if (t \in D, F (t), 0)) - g (t))\|$
228		ovexd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to \|ℜ (if (t \in D, F (t), 0)) - f (t)\| + \|i (ℑ (if (t \in D, F (t), 0)) - g (t))\| \in V$
229		eqidd	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|) = (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)$
230		fvexd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to \|ℜ (if (t \in D, F (t), 0)) - f (t)\| \in V$
231		fvexd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to \|i (ℑ (if (t \in D, F (t), 0)) - g (t))\| \in V$
232		eqidd	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) = (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)$
233		absmul	$⊢ (i \in ℂ \land ℑ (if (t \in D, F (t), 0)) - g (t) \in ℂ) \to \|i (ℑ (if (t \in D, F (t), 0)) - g (t))\| = \|i\| \|ℑ (if (t \in D, F (t), 0)) - g (t)\|$
234	13 195 233	sylancr	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to \|i (ℑ (if (t \in D, F (t), 0)) - g (t))\| = \|i\| \|ℑ (if (t \in D, F (t), 0)) - g (t)\|$
235		absi	$⊢ \|i\| = 1$
236	235	oveq1i	$⊢ \|i\| \|ℑ (if (t \in D, F (t), 0)) - g (t)\| = 1 \|ℑ (if (t \in D, F (t), 0)) - g (t)\|$
237	216	recnd	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to \|ℑ (if (t \in D, F (t), 0)) - g (t)\| \in ℂ$
238	237	mullidd	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to 1 \|ℑ (if (t \in D, F (t), 0)) - g (t)\| = \|ℑ (if (t \in D, F (t), 0)) - g (t)\|$
239	236 238	eqtrid	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to \|i\| \|ℑ (if (t \in D, F (t), 0)) - g (t)\| = \|ℑ (if (t \in D, F (t), 0)) - g (t)\|$
240	234 239	eqtr2d	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to \|ℑ (if (t \in D, F (t), 0)) - g (t)\| = \|i (ℑ (if (t \in D, F (t), 0)) - g (t))\|$
241	240	mpteq2dva	$⊢ (φ \land g \in dom \int^{1}) \to (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|) = (t \in ℝ ⟼ \|i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)$
242	241	adantrl	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|) = (t \in ℝ ⟼ \|i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)$
243	223 230 231 232 242	offval2	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) +_{f} (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|) = (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\| + \|i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)$
244	223 200 228 229 243	ofrfval2	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|) \leq_{f} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) +_{f} (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) \leftrightarrow \forall t \in ℝ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\| \leq \|ℜ (if (t \in D, F (t), 0)) - f (t)\| + \|i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)$
245	227 244	mpbird	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|) \leq_{f} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) +_{f} (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|))$
246		itg2le	$⊢ ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|) : ℝ ⟶ [0, +∞] \land ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) +_{f} (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) : ℝ ⟶ [0, +∞] \land (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|) \leq_{f} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) +_{f} (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|))) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) +_{f} (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|))$
247	205 225 245 246	syl3anc	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) +_{f} (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|))$
248		absf	$⊢ abs : ℂ ⟶ ℝ$
249	248	a1i	$⊢ (φ \land f \in dom \int^{1}) \to abs : ℂ ⟶ ℝ$
250	249 186	cofmpt	$⊢ (φ \land f \in dom \int^{1}) \to abs \circ (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t)) = (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)$
251		resubcl	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land f (t) \in ℝ) \to ℜ (if (t \in D, F (t), 0)) - f (t) \in ℝ$
252	179 182 251	syl2an	$⊢ (φ \land (f \in dom \int^{1} \land t \in ℝ)) \to ℜ (if (t \in D, F (t), 0)) - f (t) \in ℝ$
253	252	anassrs	$⊢ ((φ \land f \in dom \int^{1}) \land t \in ℝ) \to ℜ (if (t \in D, F (t), 0)) - f (t) \in ℝ$
254	253	fmpttd	$⊢ (φ \land f \in dom \int^{1}) \to (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t)) : ℝ ⟶ ℝ$
255	130	a1i	$⊢ (φ \land f \in dom \int^{1}) \to ℝ \in dom vol$
256		iunin2	$⊢ ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap f^{-1} [\{y\}]) = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap ⋃_{y \in ran f} f^{-1} [\{y\}]$
257		imaiun	$⊢ f^{-1} [⋃_{y \in ran f} \{y\}] = ⋃_{y \in ran f} f^{-1} [\{y\}]$
258		iunid	$⊢ ⋃_{y \in ran f} \{y\} = ran f$
259	258	imaeq2i	$⊢ f^{-1} [⋃_{y \in ran f} \{y\}] = f^{-1} [ran f]$
260	257 259	eqtr3i	$⊢ ⋃_{y \in ran f} f^{-1} [\{y\}] = f^{-1} [ran f]$
261	260	ineq2i	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap ⋃_{y \in ran f} f^{-1} [\{y\}] = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap f^{-1} [ran f]$
262	256 261	eqtri	$⊢ ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap f^{-1} [\{y\}]) = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap f^{-1} [ran f]$
263		cnvimass	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \subseteq dom (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))$
264		ovex	$⊢ ℜ (if (t \in D, F (t), 0)) - f (t) \in V$
265		eqid	$⊢ (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t)) = (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))$
266	264 265	dmmpti	$⊢ dom (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t)) = ℝ$
267	263 266	sseqtri	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \subseteq ℝ$
268		cnvimarndm	$⊢ f^{-1} [ran f] = dom f$
269	181	fdmd	$⊢ f \in dom \int^{1} \to dom f = ℝ$
270	268 269	eqtrid	$⊢ f \in dom \int^{1} \to f^{-1} [ran f] = ℝ$
271	267 270	sseqtrrid	$⊢ f \in dom \int^{1} \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \subseteq f^{-1} [ran f]$
272		dfss2	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \subseteq f^{-1} [ran f] \leftrightarrow {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap f^{-1} [ran f] = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)]$
273	271 272	sylib	$⊢ f \in dom \int^{1} \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap f^{-1} [ran f] = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)]$
274	262 273	eqtrid	$⊢ f \in dom \int^{1} \to ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap f^{-1} [\{y\}]) = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)]$
275	274	ad2antlr	$⊢ ((φ \land f \in dom \int^{1}) \land x \in ℝ) \to ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap f^{-1} [\{y\}]) = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)]$
276	181	frnd	$⊢ f \in dom \int^{1} \to ran f \subseteq ℝ$
277	276	ad2antlr	$⊢ ((φ \land f \in dom \int^{1}) \land x \in ℝ) \to ran f \subseteq ℝ$
278	277	sselda	$⊢ (((φ \land f \in dom \int^{1}) \land x \in ℝ) \land y \in ran f) \to y \in ℝ$
279	179	ad2antrr	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to ℜ (if (t \in D, F (t), 0)) \in ℝ$
280		resubcl	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land y \in ℝ) \to ℜ (if (t \in D, F (t), 0)) - y \in ℝ$
281	179 280	sylan	$⊢ (φ \land y \in ℝ) \to ℜ (if (t \in D, F (t), 0)) - y \in ℝ$
282	281	adantlr	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to ℜ (if (t \in D, F (t), 0)) - y \in ℝ$
283	279 282	2thd	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) \in ℝ \leftrightarrow ℜ (if (t \in D, F (t), 0)) - y \in ℝ)$
284		ltaddsub	$⊢ (x \in ℝ \land y \in ℝ \land ℜ (if (t \in D, F (t), 0)) \in ℝ) \to (x + y < ℜ (if (t \in D, F (t), 0)) \leftrightarrow x < ℜ (if (t \in D, F (t), 0)) - y)$
285	179 284	syl3an3	$⊢ (x \in ℝ \land y \in ℝ \land φ) \to (x + y < ℜ (if (t \in D, F (t), 0)) \leftrightarrow x < ℜ (if (t \in D, F (t), 0)) - y)$
286	285	3comr	$⊢ (φ \land x \in ℝ \land y \in ℝ) \to (x + y < ℜ (if (t \in D, F (t), 0)) \leftrightarrow x < ℜ (if (t \in D, F (t), 0)) - y)$
287	286	3expa	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to (x + y < ℜ (if (t \in D, F (t), 0)) \leftrightarrow x < ℜ (if (t \in D, F (t), 0)) - y)$
288	283 287	anbi12d	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to ((ℜ (if (t \in D, F (t), 0)) \in ℝ \land x + y < ℜ (if (t \in D, F (t), 0))) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) - y \in ℝ \land x < ℜ (if (t \in D, F (t), 0)) - y))$
289		readdcl	$⊢ (x \in ℝ \land y \in ℝ) \to x + y \in ℝ$
290	289	rexrd	$⊢ (x \in ℝ \land y \in ℝ) \to x + y \in ℝ^{*}$
291	290	adantll	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to x + y \in ℝ^{*}$
292		elioopnf	$⊢ x + y \in ℝ^{*} \to (ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) \in ℝ \land x + y < ℜ (if (t \in D, F (t), 0))))$
293	291 292	syl	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) \in ℝ \land x + y < ℜ (if (t \in D, F (t), 0))))$
294		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
295	294	ad2antlr	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to x \in ℝ^{*}$
296		elioopnf	$⊢ x \in ℝ^{*} \to (ℜ (if (t \in D, F (t), 0)) - y \in (x, +∞) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) - y \in ℝ \land x < ℜ (if (t \in D, F (t), 0)) - y))$
297	295 296	syl	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) - y \in (x, +∞) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) - y \in ℝ \land x < ℜ (if (t \in D, F (t), 0)) - y))$
298	288 293 297	3bitr4rd	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) - y \in (x, +∞) \leftrightarrow ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞))$
299		oveq2	$⊢ f (t) = y \to ℜ (if (t \in D, F (t), 0)) - f (t) = ℜ (if (t \in D, F (t), 0)) - y$
300	299	eleq1d	$⊢ f (t) = y \to (ℜ (if (t \in D, F (t), 0)) - f (t) \in (x, +∞) \leftrightarrow ℜ (if (t \in D, F (t), 0)) - y \in (x, +∞))$
301	300	bibi1d	$⊢ f (t) = y \to ((ℜ (if (t \in D, F (t), 0)) - f (t) \in (x, +∞) \leftrightarrow ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞)) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) - y \in (x, +∞) \leftrightarrow ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞)))$
302	298 301	syl5ibrcom	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to (f (t) = y \to (ℜ (if (t \in D, F (t), 0)) - f (t) \in (x, +∞) \leftrightarrow ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞)))$
303	302	pm5.32rd	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to ((ℜ (if (t \in D, F (t), 0)) - f (t) \in (x, +∞) \land f (t) = y) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞) \land f (t) = y))$
304	303	adantllr	$⊢ (((φ \land f \in dom \int^{1}) \land x \in ℝ) \land y \in ℝ) \to ((ℜ (if (t \in D, F (t), 0)) - f (t) \in (x, +∞) \land f (t) = y) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞) \land f (t) = y))$
305	278 304	syldan	$⊢ (((φ \land f \in dom \int^{1}) \land x \in ℝ) \land y \in ran f) \to ((ℜ (if (t \in D, F (t), 0)) - f (t) \in (x, +∞) \land f (t) = y) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞) \land f (t) = y))$
306	305	rabbidv	$⊢ (((φ \land f \in dom \int^{1}) \land x \in ℝ) \land y \in ran f) \to \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) - f (t) \in (x, +∞) \land f (t) = y)\} = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞) \land f (t) = y)\}$
307	181	feqmptd	$⊢ f \in dom \int^{1} \to f = (t \in ℝ ⟼ f (t))$
308	307	cnveqd	$⊢ f \in dom \int^{1} \to f^{-1} = {(t \in ℝ ⟼ f (t))}^{-1}$
309	308	imaeq1d	$⊢ f \in dom \int^{1} \to f^{-1} [\{y\}] = {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}]$
310	309	ineq2d	$⊢ f \in dom \int^{1} \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap f^{-1} [\{y\}] = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}]$
311	265	mptpreima	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] = \{t \in ℝ \| ℜ (if (t \in D, F (t), 0)) - f (t) \in (x, +∞)\}$
312		vex	$⊢ y \in V$
313		eqid	$⊢ (t \in ℝ ⟼ f (t)) = (t \in ℝ ⟼ f (t))$
314	313	mptiniseg	$⊢ y \in V \to {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}] = \{t \in ℝ \| f (t) = y\}$
315	312 314	ax-mp	$⊢ {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}] = \{t \in ℝ \| f (t) = y\}$
316	311 315	ineq12i	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}] = \{t \in ℝ \| ℜ (if (t \in D, F (t), 0)) - f (t) \in (x, +∞)\} \cap \{t \in ℝ \| f (t) = y\}$
317		inrab	$⊢ \{t \in ℝ \| ℜ (if (t \in D, F (t), 0)) - f (t) \in (x, +∞)\} \cap \{t \in ℝ \| f (t) = y\} = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) - f (t) \in (x, +∞) \land f (t) = y)\}$
318	316 317	eqtri	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}] = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) - f (t) \in (x, +∞) \land f (t) = y)\}$
319	310 318	eqtrdi	$⊢ f \in dom \int^{1} \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap f^{-1} [\{y\}] = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) - f (t) \in (x, +∞) \land f (t) = y)\}$
320	319	ad3antlr	$⊢ (((φ \land f \in dom \int^{1}) \land x \in ℝ) \land y \in ran f) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap f^{-1} [\{y\}] = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) - f (t) \in (x, +∞) \land f (t) = y)\}$
321	309	ineq2d	$⊢ f \in dom \int^{1} \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap f^{-1} [\{y\}] = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}]$
322		eqid	$⊢ (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) = (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))$
323	322	mptpreima	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] = \{t \in ℝ \| ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞)\}$
324	323 315	ineq12i	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}] = \{t \in ℝ \| ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞)\} \cap \{t \in ℝ \| f (t) = y\}$
325		inrab	$⊢ \{t \in ℝ \| ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞)\} \cap \{t \in ℝ \| f (t) = y\} = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞) \land f (t) = y)\}$
326	324 325	eqtri	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}] = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞) \land f (t) = y)\}$
327	321 326	eqtrdi	$⊢ f \in dom \int^{1} \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap f^{-1} [\{y\}] = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞) \land f (t) = y)\}$
328	327	ad3antlr	$⊢ (((φ \land f \in dom \int^{1}) \land x \in ℝ) \land y \in ran f) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap f^{-1} [\{y\}] = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) \in (x + y, +∞) \land f (t) = y)\}$
329	306 320 328	3eqtr4d	$⊢ (((φ \land f \in dom \int^{1}) \land x \in ℝ) \land y \in ran f) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap f^{-1} [\{y\}] = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap f^{-1} [\{y\}]$
330	329	iuneq2dv	$⊢ ((φ \land f \in dom \int^{1}) \land x \in ℝ) \to ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \cap f^{-1} [\{y\}]) = ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap f^{-1} [\{y\}])$
331	275 330	eqtr3d	$⊢ ((φ \land f \in dom \int^{1}) \land x \in ℝ) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] = ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap f^{-1} [\{y\}])$
332		i1frn	$⊢ f \in dom \int^{1} \to ran f \in Fin$
333	332	adantl	$⊢ (φ \land f \in dom \int^{1}) \to ran f \in Fin$
334	90	adantr	$⊢ (φ \land t \in D) \to if (t \in D, F (t), 0) \in ℂ$
335		eldifn	$⊢ t \in (ℝ ∖ D) \to \neg t \in D$
336	335	adantl	$⊢ (φ \land t \in (ℝ ∖ D)) \to \neg t \in D$
337	336	iffalsed	$⊢ (φ \land t \in (ℝ ∖ D)) \to if (t \in D, F (t), 0) = 0$
338	8	feqmptd	$⊢ φ \to F = (t \in D ⟼ F (t))$
339		iftrue	$⊢ t \in D \to if (t \in D, F (t), 0) = F (t)$
340	339	mpteq2ia	$⊢ (t \in D ⟼ if (t \in D, F (t), 0)) = (t \in D ⟼ F (t))$
341	338 340	eqtr4di	$⊢ φ \to F = (t \in D ⟼ if (t \in D, F (t), 0))$
342		iblmbf	$⊢ F \in 𝐿^{1} \to F \in MblFn$
343	7 342	syl	$⊢ φ \to F \in MblFn$
344	341 343	eqeltrrd	$⊢ φ \to (t \in D ⟼ if (t \in D, F (t), 0)) \in MblFn$
345	6 131 334 337 344	mbfss	$⊢ φ \to (t \in ℝ ⟼ if (t \in D, F (t), 0)) \in MblFn$
346	90	adantr	$⊢ (φ \land t \in ℝ) \to if (t \in D, F (t), 0) \in ℂ$
347	346	ismbfcn2	$⊢ φ \to ((t \in ℝ ⟼ if (t \in D, F (t), 0)) \in MblFn \leftrightarrow ((t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) \in MblFn \land (t \in ℝ ⟼ ℑ (if (t \in D, F (t), 0))) \in MblFn))$
348	345 347	mpbid	$⊢ φ \to ((t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) \in MblFn \land (t \in ℝ ⟼ ℑ (if (t \in D, F (t), 0))) \in MblFn)$
349	348	simpld	$⊢ φ \to (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) \in MblFn$
350	179	adantr	$⊢ (φ \land t \in ℝ) \to ℜ (if (t \in D, F (t), 0)) \in ℝ$
351	350	fmpttd	$⊢ φ \to (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) : ℝ ⟶ ℝ$
352		mbfima	$⊢ ((t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) \in MblFn \land (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) : ℝ ⟶ ℝ) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \in dom vol$
353	349 351 352	syl2anc	$⊢ φ \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \in dom vol$
354		i1fima	$⊢ f \in dom \int^{1} \to f^{-1} [\{y\}] \in dom vol$
355		inmbl	$⊢ ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \in dom vol \land f^{-1} [\{y\}] \in dom vol) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap f^{-1} [\{y\}] \in dom vol$
356	353 354 355	syl2an	$⊢ (φ \land f \in dom \int^{1}) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap f^{-1} [\{y\}] \in dom vol$
357	356	ralrimivw	$⊢ (φ \land f \in dom \int^{1}) \to \forall y \in ran f {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap f^{-1} [\{y\}] \in dom vol$
358		finiunmbl	$⊢ (ran f \in Fin \land \forall y \in ran f {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap f^{-1} [\{y\}] \in dom vol) \to ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap f^{-1} [\{y\}]) \in dom vol$
359	333 357 358	syl2anc	$⊢ (φ \land f \in dom \int^{1}) \to ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap f^{-1} [\{y\}]) \in dom vol$
360	359	adantr	$⊢ ((φ \land f \in dom \int^{1}) \land x \in ℝ) \to ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(x + y, +∞)] \cap f^{-1} [\{y\}]) \in dom vol$
361	331 360	eqeltrd	$⊢ ((φ \land f \in dom \int^{1}) \land x \in ℝ) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(x, +∞)] \in dom vol$
362		iunin2	$⊢ ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap f^{-1} [\{y\}]) = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap ⋃_{y \in ran f} f^{-1} [\{y\}]$
363	260	ineq2i	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap ⋃_{y \in ran f} f^{-1} [\{y\}] = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap f^{-1} [ran f]$
364	362 363	eqtri	$⊢ ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap f^{-1} [\{y\}]) = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap f^{-1} [ran f]$
365		cnvimass	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \subseteq dom (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))$
366	365 266	sseqtri	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \subseteq ℝ$
367	366 270	sseqtrrid	$⊢ f \in dom \int^{1} \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \subseteq f^{-1} [ran f]$
368		dfss2	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \subseteq f^{-1} [ran f] \leftrightarrow {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap f^{-1} [ran f] = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)]$
369	367 368	sylib	$⊢ f \in dom \int^{1} \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap f^{-1} [ran f] = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)]$
370	364 369	eqtrid	$⊢ f \in dom \int^{1} \to ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap f^{-1} [\{y\}]) = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)]$
371	370	ad2antlr	$⊢ ((φ \land f \in dom \int^{1}) \land x \in ℝ) \to ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap f^{-1} [\{y\}]) = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)]$
372	282 279	2thd	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) - y \in ℝ \leftrightarrow ℜ (if (t \in D, F (t), 0)) \in ℝ)$
373		ltsubadd	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land y \in ℝ \land x \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) - y < x \leftrightarrow ℜ (if (t \in D, F (t), 0)) < x + y)$
374	179 373	syl3an1	$⊢ (φ \land y \in ℝ \land x \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) - y < x \leftrightarrow ℜ (if (t \in D, F (t), 0)) < x + y)$
375	374	3expa	$⊢ ((φ \land y \in ℝ) \land x \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) - y < x \leftrightarrow ℜ (if (t \in D, F (t), 0)) < x + y)$
376	375	an32s	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) - y < x \leftrightarrow ℜ (if (t \in D, F (t), 0)) < x + y)$
377	372 376	anbi12d	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to ((ℜ (if (t \in D, F (t), 0)) - y \in ℝ \land ℜ (if (t \in D, F (t), 0)) - y < x) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) \in ℝ \land ℜ (if (t \in D, F (t), 0)) < x + y))$
378		elioomnf	$⊢ x \in ℝ^{*} \to (ℜ (if (t \in D, F (t), 0)) - y \in (−∞, x) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) - y \in ℝ \land ℜ (if (t \in D, F (t), 0)) - y < x))$
379	295 378	syl	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) - y \in (−∞, x) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) - y \in ℝ \land ℜ (if (t \in D, F (t), 0)) - y < x))$
380		elioomnf	$⊢ x + y \in ℝ^{*} \to (ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) \in ℝ \land ℜ (if (t \in D, F (t), 0)) < x + y))$
381	291 380	syl	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) \in ℝ \land ℜ (if (t \in D, F (t), 0)) < x + y))$
382	377 379 381	3bitr4d	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) - y \in (−∞, x) \leftrightarrow ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y))$
383	299	eleq1d	$⊢ f (t) = y \to (ℜ (if (t \in D, F (t), 0)) - f (t) \in (−∞, x) \leftrightarrow ℜ (if (t \in D, F (t), 0)) - y \in (−∞, x))$
384	383	bibi1d	$⊢ f (t) = y \to ((ℜ (if (t \in D, F (t), 0)) - f (t) \in (−∞, x) \leftrightarrow ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y)) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) - y \in (−∞, x) \leftrightarrow ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y)))$
385	382 384	syl5ibrcom	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to (f (t) = y \to (ℜ (if (t \in D, F (t), 0)) - f (t) \in (−∞, x) \leftrightarrow ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y)))$
386	385	pm5.32rd	$⊢ ((φ \land x \in ℝ) \land y \in ℝ) \to ((ℜ (if (t \in D, F (t), 0)) - f (t) \in (−∞, x) \land f (t) = y) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y) \land f (t) = y))$
387	386	adantllr	$⊢ (((φ \land f \in dom \int^{1}) \land x \in ℝ) \land y \in ℝ) \to ((ℜ (if (t \in D, F (t), 0)) - f (t) \in (−∞, x) \land f (t) = y) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y) \land f (t) = y))$
388	278 387	syldan	$⊢ (((φ \land f \in dom \int^{1}) \land x \in ℝ) \land y \in ran f) \to ((ℜ (if (t \in D, F (t), 0)) - f (t) \in (−∞, x) \land f (t) = y) \leftrightarrow (ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y) \land f (t) = y))$
389	388	rabbidv	$⊢ (((φ \land f \in dom \int^{1}) \land x \in ℝ) \land y \in ran f) \to \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) - f (t) \in (−∞, x) \land f (t) = y)\} = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y) \land f (t) = y)\}$
390	309	ineq2d	$⊢ f \in dom \int^{1} \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap f^{-1} [\{y\}] = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}]$
391	265	mptpreima	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] = \{t \in ℝ \| ℜ (if (t \in D, F (t), 0)) - f (t) \in (−∞, x)\}$
392	391 315	ineq12i	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}] = \{t \in ℝ \| ℜ (if (t \in D, F (t), 0)) - f (t) \in (−∞, x)\} \cap \{t \in ℝ \| f (t) = y\}$
393		inrab	$⊢ \{t \in ℝ \| ℜ (if (t \in D, F (t), 0)) - f (t) \in (−∞, x)\} \cap \{t \in ℝ \| f (t) = y\} = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) - f (t) \in (−∞, x) \land f (t) = y)\}$
394	392 393	eqtri	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}] = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) - f (t) \in (−∞, x) \land f (t) = y)\}$
395	390 394	eqtrdi	$⊢ f \in dom \int^{1} \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap f^{-1} [\{y\}] = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) - f (t) \in (−∞, x) \land f (t) = y)\}$
396	395	ad3antlr	$⊢ (((φ \land f \in dom \int^{1}) \land x \in ℝ) \land y \in ran f) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap f^{-1} [\{y\}] = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) - f (t) \in (−∞, x) \land f (t) = y)\}$
397	309	ineq2d	$⊢ f \in dom \int^{1} \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap f^{-1} [\{y\}] = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}]$
398	322	mptpreima	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] = \{t \in ℝ \| ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y)\}$
399	398 315	ineq12i	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}] = \{t \in ℝ \| ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y)\} \cap \{t \in ℝ \| f (t) = y\}$
400		inrab	$⊢ \{t \in ℝ \| ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y)\} \cap \{t \in ℝ \| f (t) = y\} = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y) \land f (t) = y)\}$
401	399 400	eqtri	$⊢ {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap {(t \in ℝ ⟼ f (t))}^{-1} [\{y\}] = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y) \land f (t) = y)\}$
402	397 401	eqtrdi	$⊢ f \in dom \int^{1} \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap f^{-1} [\{y\}] = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y) \land f (t) = y)\}$
403	402	ad3antlr	$⊢ (((φ \land f \in dom \int^{1}) \land x \in ℝ) \land y \in ran f) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap f^{-1} [\{y\}] = \{t \in ℝ \| (ℜ (if (t \in D, F (t), 0)) \in (−∞, x + y) \land f (t) = y)\}$
404	389 396 403	3eqtr4d	$⊢ (((φ \land f \in dom \int^{1}) \land x \in ℝ) \land y \in ran f) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap f^{-1} [\{y\}] = {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap f^{-1} [\{y\}]$
405	404	iuneq2dv	$⊢ ((φ \land f \in dom \int^{1}) \land x \in ℝ) \to ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \cap f^{-1} [\{y\}]) = ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap f^{-1} [\{y\}])$
406	371 405	eqtr3d	$⊢ ((φ \land f \in dom \int^{1}) \land x \in ℝ) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] = ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap f^{-1} [\{y\}])$
407		mbfima	$⊢ ((t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) \in MblFn \land (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) : ℝ ⟶ ℝ) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \in dom vol$
408	349 351 407	syl2anc	$⊢ φ \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \in dom vol$
409		inmbl	$⊢ ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \in dom vol \land f^{-1} [\{y\}] \in dom vol) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap f^{-1} [\{y\}] \in dom vol$
410	408 354 409	syl2an	$⊢ (φ \land f \in dom \int^{1}) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap f^{-1} [\{y\}] \in dom vol$
411	410	ralrimivw	$⊢ (φ \land f \in dom \int^{1}) \to \forall y \in ran f {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap f^{-1} [\{y\}] \in dom vol$
412		finiunmbl	$⊢ (ran f \in Fin \land \forall y \in ran f {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap f^{-1} [\{y\}] \in dom vol) \to ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap f^{-1} [\{y\}]) \in dom vol$
413	333 411 412	syl2anc	$⊢ (φ \land f \in dom \int^{1}) \to ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap f^{-1} [\{y\}]) \in dom vol$
414	413	adantr	$⊢ ((φ \land f \in dom \int^{1}) \land x \in ℝ) \to ⋃_{y \in ran f} ({(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))}^{-1} [(−∞, x + y)] \cap f^{-1} [\{y\}]) \in dom vol$
415	406 414	eqeltrd	$⊢ ((φ \land f \in dom \int^{1}) \land x \in ℝ) \to {(t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t))}^{-1} [(−∞, x)] \in dom vol$
416	254 255 361 415	ismbf2d	$⊢ (φ \land f \in dom \int^{1}) \to (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t)) \in MblFn$
417		ftc1anclem1	$⊢ ((t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t)) : ℝ ⟶ ℝ \land (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t)) \in MblFn) \to abs \circ (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t)) \in MblFn$
418	254 416 417	syl2anc	$⊢ (φ \land f \in dom \int^{1}) \to abs \circ (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)) - f (t)) \in MblFn$
419	250 418	eqeltrrd	$⊢ (φ \land f \in dom \int^{1}) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) \in MblFn$
420	419	adantrr	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) \in MblFn$
421	155	adantrr	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) \in ℝ$
422	172	adantrl	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) \in ℝ$
423	420 215 421 221 422	itg2addnc	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) +_{f} (t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) = \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|))$
424	247 423	breqtrd	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|))$
425	424	adantlr	$⊢ ((φ \land Y \in ℝ^{+}) \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|))$
426		itg2cl	$⊢ (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|) : ℝ ⟶ [0, +∞] \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) \in ℝ^{*}$
427	205 426	syl	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) \in ℝ^{*}$
428	427	adantlr	$⊢ ((φ \land Y \in ℝ^{+}) \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) \in ℝ^{*}$
429		readdcl	$⊢ (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) \in ℝ \land \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) \in ℝ) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) \in ℝ$
430	155 172 429	syl2an	$⊢ ((φ \land f \in dom \int^{1}) \land (φ \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) \in ℝ$
431	430	anandis	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) \in ℝ$
432	431	rexrd	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) \in ℝ^{*}$
433	432	adantlr	$⊢ ((φ \land Y \in ℝ^{+}) \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) \in ℝ^{*}$
434	9 9	rpaddcld	$⊢ Y \in ℝ^{+} \to (\frac{Y}{2}) + (\frac{Y}{2}) \in ℝ^{+}$
435	434	rpxrd	$⊢ Y \in ℝ^{+} \to (\frac{Y}{2}) + (\frac{Y}{2}) \in ℝ^{*}$
436	435	ad2antlr	$⊢ ((φ \land Y \in ℝ^{+}) \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (\frac{Y}{2}) + (\frac{Y}{2}) \in ℝ^{*}$
437		xrlelttr	$⊢ (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) \in ℝ^{} \land \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) \in ℝ^{} \land (\frac{Y}{2}) + (\frac{Y}{2}) \in ℝ^{*}) \to ((\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) \land \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < (\frac{Y}{2}) + (\frac{Y}{2})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) < (\frac{Y}{2}) + (\frac{Y}{2}))$
438	428 433 436 437	syl3anc	$⊢ ((φ \land Y \in ℝ^{+}) \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to ((\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) \land \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < (\frac{Y}{2}) + (\frac{Y}{2})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) < (\frac{Y}{2}) + (\frac{Y}{2}))$
439	425 438	mpand	$⊢ ((φ \land Y \in ℝ^{+}) \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < (\frac{Y}{2}) + (\frac{Y}{2}) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) < (\frac{Y}{2}) + (\frac{Y}{2}))$
440	178 439	syld	$⊢ ((φ \land Y \in ℝ^{+}) \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to ((\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < \frac{Y}{2} \land \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < \frac{Y}{2}) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) < (\frac{Y}{2}) + (\frac{Y}{2}))$
441		mulcl	$⊢ (i \in ℂ \land ℑ (if (t \in D, F (t), 0)) \in ℂ) \to i ℑ (if (t \in D, F (t), 0)) \in ℂ$
442	13 189 441	sylancr	$⊢ φ \to i ℑ (if (t \in D, F (t), 0)) \in ℂ$
443	180 442	jca	$⊢ φ \to (ℜ (if (t \in D, F (t), 0)) \in ℂ \land i ℑ (if (t \in D, F (t), 0)) \in ℂ)$
444		mulcl	$⊢ (i \in ℂ \land g (t) \in ℂ) \to i g (t) \in ℂ$
445	13 192 444	sylancr	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to i g (t) \in ℂ$
446	183 445	anim12i	$⊢ ((f \in dom \int^{1} \land t \in ℝ) \land (g \in dom \int^{1} \land t \in ℝ)) \to (f (t) \in ℂ \land i g (t) \in ℂ)$
447	446	anandirs	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to (f (t) \in ℂ \land i g (t) \in ℂ)$
448		addsub4	$⊢ ((ℜ (if (t \in D, F (t), 0)) \in ℂ \land i ℑ (if (t \in D, F (t), 0)) \in ℂ) \land (f (t) \in ℂ \land i g (t) \in ℂ)) \to ℜ (if (t \in D, F (t), 0)) + i ℑ (if (t \in D, F (t), 0)) - (f (t) + i g (t)) = (ℜ (if (t \in D, F (t), 0)) - f (t)) + i ℑ (if (t \in D, F (t), 0)) - i g (t)$
449	443 447 448	syl2an	$⊢ (φ \land ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ)) \to ℜ (if (t \in D, F (t), 0)) + i ℑ (if (t \in D, F (t), 0)) - (f (t) + i g (t)) = (ℜ (if (t \in D, F (t), 0)) - f (t)) + i ℑ (if (t \in D, F (t), 0)) - i g (t)$
450	449	anassrs	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to ℜ (if (t \in D, F (t), 0)) + i ℑ (if (t \in D, F (t), 0)) - (f (t) + i g (t)) = (ℜ (if (t \in D, F (t), 0)) - f (t)) + i ℑ (if (t \in D, F (t), 0)) - i g (t)$
451	90	replimd	$⊢ φ \to if (t \in D, F (t), 0) = ℜ (if (t \in D, F (t), 0)) + i ℑ (if (t \in D, F (t), 0))$
452	451	ad2antrr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to if (t \in D, F (t), 0) = ℜ (if (t \in D, F (t), 0)) + i ℑ (if (t \in D, F (t), 0))$
453	452	oveq1d	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to if (t \in D, F (t), 0) - (f (t) + i g (t)) = ℜ (if (t \in D, F (t), 0)) + i ℑ (if (t \in D, F (t), 0)) - (f (t) + i g (t))$
454	192	adantll	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to g (t) \in ℂ$
455		subdi	$⊢ (i \in ℂ \land ℑ (if (t \in D, F (t), 0)) \in ℂ \land g (t) \in ℂ) \to i (ℑ (if (t \in D, F (t), 0)) - g (t)) = i ℑ (if (t \in D, F (t), 0)) - i g (t)$
456	13 189 454 455	mp3an3an	$⊢ (φ \land ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ)) \to i (ℑ (if (t \in D, F (t), 0)) - g (t)) = i ℑ (if (t \in D, F (t), 0)) - i g (t)$
457	456	anassrs	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to i (ℑ (if (t \in D, F (t), 0)) - g (t)) = i ℑ (if (t \in D, F (t), 0)) - i g (t)$
458	457	oveq2d	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t)) = (ℜ (if (t \in D, F (t), 0)) - f (t)) + i ℑ (if (t \in D, F (t), 0)) - i g (t)$
459	450 453 458	3eqtr4rd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t)) = if (t \in D, F (t), 0) - (f (t) + i g (t))$
460	459	fveq2d	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\| = \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|$
461	460	mpteq2dva	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|) = (t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)$
462	461	fveq2d	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) = \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|))$
463	462	adantlr	$⊢ ((φ \land Y \in ℝ^{+}) \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) = \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|))$
464		rpcn	$⊢ Y \in ℝ^{+} \to Y \in ℂ$
465	464	2halvesd	$⊢ Y \in ℝ^{+} \to (\frac{Y}{2}) + (\frac{Y}{2}) = Y$
466	465	ad2antlr	$⊢ ((φ \land Y \in ℝ^{+}) \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (\frac{Y}{2}) + (\frac{Y}{2}) = Y$
467	463 466	breq12d	$⊢ ((φ \land Y \in ℝ^{+}) \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t) + i (ℑ (if (t \in D, F (t), 0)) - g (t))\|)) < (\frac{Y}{2}) + (\frac{Y}{2}) \leftrightarrow \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < Y)$
468	440 467	sylibd	$⊢ ((φ \land Y \in ℝ^{+}) \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to ((\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < \frac{Y}{2} \land \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < \frac{Y}{2}) \to \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < Y)$
469	468	reximdvva	$⊢ (φ \land Y \in ℝ^{+}) \to (\exists f \in dom \int^{1} \exists g \in dom \int^{1} (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < \frac{Y}{2} \land \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < \frac{Y}{2}) \to \exists f \in dom \int^{1} \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < Y)$
470	119 469	biimtrrid	$⊢ (φ \land Y \in ℝ^{+}) \to ((\exists f \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < \frac{Y}{2} \land \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℑ (if (t \in D, F (t), 0)) - g (t)\|)) < \frac{Y}{2}) \to \exists f \in dom \int^{1} \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < Y)$
471	11 118 470	mp2and	$⊢ (φ \land Y \in ℝ^{+}) \to \exists f \in dom \int^{1} \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < Y$

Metamath Proof Explorer

Theorem ftc1anclem6

Proof