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