ftc1anclem8

	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	ftc1anclem8	$⊢ ((((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2}) \land \exists r \in (ran f \cup ran g) r \neq 0) \land y \in ℝ^{+}) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land \|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)}) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0))) < 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	1 2 3 4 5 6 7 8	ftc1anclem7	$⊢ ((((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2}) \land \exists r \in (ran f \cup ran g) r \neq 0) \land y \in ℝ^{+}) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land \|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)}) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) < (\frac{y}{2}) + (\frac{y}{2})$
10		simplll	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2}) \land \exists r \in (ran f \cup ran g) r \neq 0) \land y \in ℝ^{+}) \to (φ \land (f \in dom \int^{1} \land g \in dom \int^{1}))$
11		3simpa	$⊢ (u \in [A, B] \land w \in [A, B] \land u \leq w) \to (u \in [A, B] \land w \in [A, B])$
12		ioossre	$⊢ (u, w) \subseteq ℝ$
13	12	a1i	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (u, w) \subseteq ℝ$
14		rembl	$⊢ ℝ \in dom vol$
15	14	a1i	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to ℝ \in dom vol$
16		fvex	$⊢ \|f (t) + i g (t)\| \in V$
17		c0ex	$⊢ 0 \in V$
18	16 17	ifex	$⊢ if (t \in (u, w), \|f (t) + i g (t)\|, 0) \in V$
19	18	a1i	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in (u, w)) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) \in V$
20		eldifn	$⊢ t \in (ℝ ∖ (u, w)) \to \neg t \in (u, w)$
21	20	adantl	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in (ℝ ∖ (u, w))) \to \neg t \in (u, w)$
22	21	iffalsed	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in (ℝ ∖ (u, w))) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) = 0$
23		iftrue	$⊢ t \in (u, w) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) = \|f (t) + i g (t)\|$
24	23	mpteq2ia	$⊢ (t \in (u, w) ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) = (t \in (u, w) ⟼ \|f (t) + i g (t)\|)$
25		resmpt	$⊢ (u, w) \subseteq ℝ \to {(t \in ℝ ⟼ \|f (t) + i g (t)\|) ↾}_{(u, w)} = (t \in (u, w) ⟼ \|f (t) + i g (t)\|)$
26	12 25	ax-mp	$⊢ {(t \in ℝ ⟼ \|f (t) + i g (t)\|) ↾}_{(u, w)} = (t \in (u, w) ⟼ \|f (t) + i g (t)\|)$
27	24 26	eqtr4i	$⊢ (t \in (u, w) ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) = {(t \in ℝ ⟼ \|f (t) + i g (t)\|) ↾}_{(u, w)}$
28		i1ff	$⊢ f \in dom \int^{1} \to f : ℝ ⟶ ℝ$
29	28	ffvelcdmda	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to f (t) \in ℝ$
30	29	recnd	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to f (t) \in ℂ$
31		ax-icn	$⊢ i \in ℂ$
32		i1ff	$⊢ g \in dom \int^{1} \to g : ℝ ⟶ ℝ$
33	32	ffvelcdmda	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) \in ℝ$
34	33	recnd	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) \in ℂ$
35		mulcl	$⊢ (i \in ℂ \land g (t) \in ℂ) \to i g (t) \in ℂ$
36	31 34 35	sylancr	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to i g (t) \in ℂ$
37		addcl	$⊢ (f (t) \in ℂ \land i g (t) \in ℂ) \to f (t) + i g (t) \in ℂ$
38	30 36 37	syl2an	$⊢ ((f \in dom \int^{1} \land t \in ℝ) \land (g \in dom \int^{1} \land t \in ℝ)) \to f (t) + i g (t) \in ℂ$
39	38	anandirs	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to f (t) + i g (t) \in ℂ$
40		reex	$⊢ ℝ \in V$
41	40	a1i	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ℝ \in V$
42	29	adantlr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to f (t) \in ℝ$
43	36	adantll	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to i g (t) \in ℂ$
44	28	feqmptd	$⊢ f \in dom \int^{1} \to f = (t \in ℝ ⟼ f (t))$
45	44	adantr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to f = (t \in ℝ ⟼ f (t))$
46	40	a1i	$⊢ g \in dom \int^{1} \to ℝ \in V$
47	31	a1i	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to i \in ℂ$
48		fconstmpt	$⊢ ℝ \times \{i\} = (t \in ℝ ⟼ i)$
49	48	a1i	$⊢ g \in dom \int^{1} \to ℝ \times \{i\} = (t \in ℝ ⟼ i)$
50	32	feqmptd	$⊢ g \in dom \int^{1} \to g = (t \in ℝ ⟼ g (t))$
51	46 47 33 49 50	offval2	$⊢ g \in dom \int^{1} \to (ℝ \times \{i\}) \times_{f} g = (t \in ℝ ⟼ i g (t))$
52	51	adantl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (ℝ \times \{i\}) \times_{f} g = (t \in ℝ ⟼ i g (t))$
53	41 42 43 45 52	offval2	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to f +_{f} ((ℝ \times \{i\}) \times_{f} g) = (t \in ℝ ⟼ f (t) + i g (t))$
54		absf	$⊢ abs : ℂ ⟶ ℝ$
55	54	a1i	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs : ℂ ⟶ ℝ$
56	55	feqmptd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs = (x \in ℂ ⟼ \|x\|)$
57		fveq2	$⊢ x = f (t) + i g (t) \to \|x\| = \|f (t) + i g (t)\|$
58	39 53 56 57	fmptco	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} g)) = (t \in ℝ ⟼ \|f (t) + i g (t)\|)$
59		ftc1anclem3	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} g)) \in dom \int^{1}$
60	58 59	eqeltrrd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in ℝ ⟼ \|f (t) + i g (t)\|) \in dom \int^{1}$
61		i1fmbf	$⊢ (t \in ℝ ⟼ \|f (t) + i g (t)\|) \in dom \int^{1} \to (t \in ℝ ⟼ \|f (t) + i g (t)\|) \in MblFn$
62	60 61	syl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in ℝ ⟼ \|f (t) + i g (t)\|) \in MblFn$
63		ioombl	$⊢ (u, w) \in dom vol$
64		mbfres	$⊢ ((t \in ℝ ⟼ \|f (t) + i g (t)\|) \in MblFn \land (u, w) \in dom vol) \to {(t \in ℝ ⟼ \|f (t) + i g (t)\|) ↾}_{(u, w)} \in MblFn$
65	62 63 64	sylancl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to {(t \in ℝ ⟼ \|f (t) + i g (t)\|) ↾}_{(u, w)} \in MblFn$
66	27 65	eqeltrid	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in (u, w) ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \in MblFn$
67	66	adantl	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in (u, w) ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \in MblFn$
68	13 15 19 22 67	mbfss	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \in MblFn$
69	68	adantr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \in MblFn$
70	39	abscld	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t) + i g (t)\| \in ℝ$
71	39	absge0d	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to 0 \leq \|f (t) + i g (t)\|$
72		elrege0	$⊢ \|f (t) + i g (t)\| \in [0, +∞) \leftrightarrow (\|f (t) + i g (t)\| \in ℝ \land 0 \leq \|f (t) + i g (t)\|)$
73	70 71 72	sylanbrc	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t) + i g (t)\| \in [0, +∞)$
74		0e0icopnf	$⊢ 0 \in [0, +∞)$
75		ifcl	$⊢ (\|f (t) + i g (t)\| \in [0, +∞) \land 0 \in [0, +∞)) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) \in [0, +∞)$
76	73 74 75	sylancl	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) \in [0, +∞)$
77	76	fmpttd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞)$
78	77	ad2antlr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞)$
79	70	rexrd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t) + i g (t)\| \in ℝ^{*}$
80		elxrge0	$⊢ \|f (t) + i g (t)\| \in [0, +∞] \leftrightarrow (\|f (t) + i g (t)\| \in ℝ^{*} \land 0 \leq \|f (t) + i g (t)\|)$
81	79 71 80	sylanbrc	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t) + i g (t)\| \in [0, +∞]$
82		0e0iccpnf	$⊢ 0 \in [0, +∞]$
83		ifcl	$⊢ (\|f (t) + i g (t)\| \in [0, +∞] \land 0 \in [0, +∞]) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) \in [0, +∞]$
84	81 82 83	sylancl	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) \in [0, +∞]$
85	84	fmpttd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞]$
86	85	ad2antlr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞]$
87		ifcl	$⊢ (\|f (t) + i g (t)\| \in [0, +∞] \land 0 \in [0, +∞]) \to if (t \in D, \|f (t) + i g (t)\|, 0) \in [0, +∞]$
88	81 82 87	sylancl	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to if (t \in D, \|f (t) + i g (t)\|, 0) \in [0, +∞]$
89	88	fmpttd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞]$
90		ffn	$⊢ f : ℝ ⟶ ℝ \to f Fn ℝ$
91		frn	$⊢ f : ℝ ⟶ ℝ \to ran f \subseteq ℝ$
92		ax-resscn	$⊢ ℝ \subseteq ℂ$
93	91 92	sstrdi	$⊢ f : ℝ ⟶ ℝ \to ran f \subseteq ℂ$
94		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
95	54 94	ax-mp	$⊢ abs Fn ℂ$
96		fnco	$⊢ (abs Fn ℂ \land f Fn ℝ \land ran f \subseteq ℂ) \to (abs \circ f) Fn ℝ$
97	95 96	mp3an1	$⊢ (f Fn ℝ \land ran f \subseteq ℂ) \to (abs \circ f) Fn ℝ$
98	90 93 97	syl2anc	$⊢ f : ℝ ⟶ ℝ \to (abs \circ f) Fn ℝ$
99	28 98	syl	$⊢ f \in dom \int^{1} \to (abs \circ f) Fn ℝ$
100	99	adantr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (abs \circ f) Fn ℝ$
101		ffn	$⊢ g : ℝ ⟶ ℝ \to g Fn ℝ$
102		frn	$⊢ g : ℝ ⟶ ℝ \to ran g \subseteq ℝ$
103	102 92	sstrdi	$⊢ g : ℝ ⟶ ℝ \to ran g \subseteq ℂ$
104		fnco	$⊢ (abs Fn ℂ \land g Fn ℝ \land ran g \subseteq ℂ) \to (abs \circ g) Fn ℝ$
105	95 104	mp3an1	$⊢ (g Fn ℝ \land ran g \subseteq ℂ) \to (abs \circ g) Fn ℝ$
106	101 103 105	syl2anc	$⊢ g : ℝ ⟶ ℝ \to (abs \circ g) Fn ℝ$
107	32 106	syl	$⊢ g \in dom \int^{1} \to (abs \circ g) Fn ℝ$
108	107	adantl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (abs \circ g) Fn ℝ$
109		inidm	$⊢ ℝ \cap ℝ = ℝ$
110	28	adantr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to f : ℝ ⟶ ℝ$
111		fvco3	$⊢ (f : ℝ ⟶ ℝ \land t \in ℝ) \to (abs \circ f) (t) = \|f (t)\|$
112	110 111	sylan	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to (abs \circ f) (t) = \|f (t)\|$
113	32	adantl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to g : ℝ ⟶ ℝ$
114		fvco3	$⊢ (g : ℝ ⟶ ℝ \land t \in ℝ) \to (abs \circ g) (t) = \|g (t)\|$
115	113 114	sylan	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to (abs \circ g) (t) = \|g (t)\|$
116	100 108 41 41 109 112 115	offval	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (abs \circ f) +_{f} (abs \circ g) = (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|)$
117	30	addridd	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to f (t) + 0 = f (t)$
118	117	mpteq2dva	$⊢ f \in dom \int^{1} \to (t \in ℝ ⟼ f (t) + 0) = (t \in ℝ ⟼ f (t))$
119	40	a1i	$⊢ f \in dom \int^{1} \to ℝ \in V$
120	17	a1i	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to 0 \in V$
121	31	a1i	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to i \in ℂ$
122	48	a1i	$⊢ f \in dom \int^{1} \to ℝ \times \{i\} = (t \in ℝ ⟼ i)$
123		fconstmpt	$⊢ ℝ \times \{0\} = (t \in ℝ ⟼ 0)$
124	123	a1i	$⊢ f \in dom \int^{1} \to ℝ \times \{0\} = (t \in ℝ ⟼ 0)$
125	119 121 120 122 124	offval2	$⊢ f \in dom \int^{1} \to (ℝ \times \{i\}) \times_{f} (ℝ \times \{0\}) = (t \in ℝ ⟼ i \cdot 0)$
126		it0e0	$⊢ i \cdot 0 = 0$
127	126	mpteq2i	$⊢ (t \in ℝ ⟼ i \cdot 0) = (t \in ℝ ⟼ 0)$
128	125 127	eqtrdi	$⊢ f \in dom \int^{1} \to (ℝ \times \{i\}) \times_{f} (ℝ \times \{0\}) = (t \in ℝ ⟼ 0)$
129	119 29 120 44 128	offval2	$⊢ f \in dom \int^{1} \to f +_{f} ((ℝ \times \{i\}) \times_{f} (ℝ \times \{0\})) = (t \in ℝ ⟼ f (t) + 0)$
130	118 129 44	3eqtr4d	$⊢ f \in dom \int^{1} \to f +_{f} ((ℝ \times \{i\}) \times_{f} (ℝ \times \{0\})) = f$
131	130	coeq2d	$⊢ f \in dom \int^{1} \to abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} (ℝ \times \{0\}))) = abs \circ f$
132		i1f0	$⊢ ℝ \times \{0\} \in dom \int^{1}$
133		ftc1anclem3	$⊢ (f \in dom \int^{1} \land ℝ \times \{0\} \in dom \int^{1}) \to abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} (ℝ \times \{0\}))) \in dom \int^{1}$
134	132 133	mpan2	$⊢ f \in dom \int^{1} \to abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} (ℝ \times \{0\}))) \in dom \int^{1}$
135	131 134	eqeltrrd	$⊢ f \in dom \int^{1} \to abs \circ f \in dom \int^{1}$
136	135	adantr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs \circ f \in dom \int^{1}$
137		coeq2	$⊢ f = g \to abs \circ f = abs \circ g$
138	137	eleq1d	$⊢ f = g \to (abs \circ f \in dom \int^{1} \leftrightarrow abs \circ g \in dom \int^{1})$
139	138 135	vtoclga	$⊢ g \in dom \int^{1} \to abs \circ g \in dom \int^{1}$
140	139	adantl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs \circ g \in dom \int^{1}$
141	136 140	i1fadd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (abs \circ f) +_{f} (abs \circ g) \in dom \int^{1}$
142	116 141	eqeltrrd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) \in dom \int^{1}$
143	30	abscld	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to \|f (t)\| \in ℝ$
144	30	absge0d	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to 0 \leq \|f (t)\|$
145		elrege0	$⊢ \|f (t)\| \in [0, +∞) \leftrightarrow (\|f (t)\| \in ℝ \land 0 \leq \|f (t)\|)$
146	143 144 145	sylanbrc	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to \|f (t)\| \in [0, +∞)$
147	34	abscld	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to \|g (t)\| \in ℝ$
148	34	absge0d	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to 0 \leq \|g (t)\|$
149		elrege0	$⊢ \|g (t)\| \in [0, +∞) \leftrightarrow (\|g (t)\| \in ℝ \land 0 \leq \|g (t)\|)$
150	147 148 149	sylanbrc	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to \|g (t)\| \in [0, +∞)$
151		ge0addcl	$⊢ (\|f (t)\| \in [0, +∞) \land \|g (t)\| \in [0, +∞)) \to \|f (t)\| + \|g (t)\| \in [0, +∞)$
152	146 150 151	syl2an	$⊢ ((f \in dom \int^{1} \land t \in ℝ) \land (g \in dom \int^{1} \land t \in ℝ)) \to \|f (t)\| + \|g (t)\| \in [0, +∞)$
153	152	anandirs	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t)\| + \|g (t)\| \in [0, +∞)$
154	153	fmpttd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) : ℝ ⟶ [0, +∞)$
155		0plef	$⊢ (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) : ℝ ⟶ [0, +∞) \leftrightarrow ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) : ℝ ⟶ ℝ \land 0_{𝑝} \leq_{f} (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|))$
156	154 155	sylib	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) : ℝ ⟶ ℝ \land 0_{𝑝} \leq_{f} (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|))$
157	156	simprd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to 0_{𝑝} \leq_{f} (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|)$
158		itg2itg1	$⊢ ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) \in dom \int^{1} \land 0_{𝑝} \leq_{f} (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|)) \to \int^{2} ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|)) = \int^{1} ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|))$
159		itg1cl	$⊢ (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) \in dom \int^{1} \to \int^{1} ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|)) \in ℝ$
160	159	adantr	$⊢ ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) \in dom \int^{1} \land 0_{𝑝} \leq_{f} (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|)) \to \int^{1} ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|)) \in ℝ$
161	158 160	eqeltrd	$⊢ ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) \in dom \int^{1} \land 0_{𝑝} \leq_{f} (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|)) \to \int^{2} ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|)) \in ℝ$
162	142 157 161	syl2anc	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|)) \in ℝ$
163		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
164		fss	$⊢ ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) : ℝ ⟶ [0, +∞]$
165	154 163 164	sylancl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) : ℝ ⟶ [0, +∞]$
166		0re	$⊢ 0 \in ℝ$
167		ifcl	$⊢ (\|f (t) + i g (t)\| \in ℝ \land 0 \in ℝ) \to if (t \in D, \|f (t) + i g (t)\|, 0) \in ℝ$
168	70 166 167	sylancl	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to if (t \in D, \|f (t) + i g (t)\|, 0) \in ℝ$
169		readdcl	$⊢ (\|f (t)\| \in ℝ \land \|g (t)\| \in ℝ) \to \|f (t)\| + \|g (t)\| \in ℝ$
170	143 147 169	syl2an	$⊢ ((f \in dom \int^{1} \land t \in ℝ) \land (g \in dom \int^{1} \land t \in ℝ)) \to \|f (t)\| + \|g (t)\| \in ℝ$
171	170	anandirs	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t)\| + \|g (t)\| \in ℝ$
172	70	leidd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t) + i g (t)\| \leq \|f (t) + i g (t)\|$
173		breq1	$⊢ \|f (t) + i g (t)\| = if (t \in D, \|f (t) + i g (t)\|, 0) \to (\|f (t) + i g (t)\| \leq \|f (t) + i g (t)\| \leftrightarrow if (t \in D, \|f (t) + i g (t)\|, 0) \leq \|f (t) + i g (t)\|)$
174		breq1	$⊢ 0 = if (t \in D, \|f (t) + i g (t)\|, 0) \to (0 \leq \|f (t) + i g (t)\| \leftrightarrow if (t \in D, \|f (t) + i g (t)\|, 0) \leq \|f (t) + i g (t)\|)$
175	173 174	ifboth	$⊢ (\|f (t) + i g (t)\| \leq \|f (t) + i g (t)\| \land 0 \leq \|f (t) + i g (t)\|) \to if (t \in D, \|f (t) + i g (t)\|, 0) \leq \|f (t) + i g (t)\|$
176	172 71 175	syl2anc	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to if (t \in D, \|f (t) + i g (t)\|, 0) \leq \|f (t) + i g (t)\|$
177		abstri	$⊢ (f (t) \in ℂ \land i g (t) \in ℂ) \to \|f (t) + i g (t)\| \leq \|f (t)\| + \|i g (t)\|$
178	30 36 177	syl2an	$⊢ ((f \in dom \int^{1} \land t \in ℝ) \land (g \in dom \int^{1} \land t \in ℝ)) \to \|f (t) + i g (t)\| \leq \|f (t)\| + \|i g (t)\|$
179	178	anandirs	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t) + i g (t)\| \leq \|f (t)\| + \|i g (t)\|$
180		absmul	$⊢ (i \in ℂ \land g (t) \in ℂ) \to \|i g (t)\| = \|i\| \|g (t)\|$
181	31 34 180	sylancr	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to \|i g (t)\| = \|i\| \|g (t)\|$
182		absi	$⊢ \|i\| = 1$
183	182	oveq1i	$⊢ \|i\| \|g (t)\| = 1 \|g (t)\|$
184	181 183	eqtrdi	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to \|i g (t)\| = 1 \|g (t)\|$
185	147	recnd	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to \|g (t)\| \in ℂ$
186	185	mullidd	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to 1 \|g (t)\| = \|g (t)\|$
187	184 186	eqtrd	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to \|i g (t)\| = \|g (t)\|$
188	187	adantll	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|i g (t)\| = \|g (t)\|$
189	188	oveq2d	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t)\| + \|i g (t)\| = \|f (t)\| + \|g (t)\|$
190	179 189	breqtrd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t) + i g (t)\| \leq \|f (t)\| + \|g (t)\|$
191	168 70 171 176 190	letrd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to if (t \in D, \|f (t) + i g (t)\|, 0) \leq \|f (t)\| + \|g (t)\|$
192	191	ralrimiva	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to \forall t \in ℝ if (t \in D, \|f (t) + i g (t)\|, 0) \leq \|f (t)\| + \|g (t)\|$
193		eqidd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) = (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))$
194		eqidd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) = (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|)$
195	41 168 171 193 194	ofrfval2	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) \leq_{f} (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) \leftrightarrow \forall t \in ℝ if (t \in D, \|f (t) + i g (t)\|, 0) \leq \|f (t)\| + \|g (t)\|)$
196	192 195	mpbird	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) \leq_{f} (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|)$
197		itg2le	$⊢ ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞] \land (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|) : ℝ ⟶ [0, +∞] \land (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) \leq_{f} (t \in ℝ ⟼ \|f (t)\| + \|g (t)\|)) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|))$
198	89 165 196 197	syl3anc	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|))$
199		itg2lecl	$⊢ ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞] \land \int^{2} ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|)) \in ℝ \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ \|f (t)\| + \|g (t)\|))) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) \in ℝ$
200	89 162 198 199	syl3anc	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) \in ℝ$
201	200	ad2antlr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) \in ℝ$
202	89	ad2antlr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞]$
203		breq1	$⊢ \|f (t) + i g (t)\| = if (t \in (u, w), \|f (t) + i g (t)\|, 0) \to (\|f (t) + i g (t)\| \leq if (t \in D, \|f (t) + i g (t)\|, 0) \leftrightarrow if (t \in (u, w), \|f (t) + i g (t)\|, 0) \leq if (t \in D, \|f (t) + i g (t)\|, 0))$
204		breq1	$⊢ 0 = if (t \in (u, w), \|f (t) + i g (t)\|, 0) \to (0 \leq if (t \in D, \|f (t) + i g (t)\|, 0) \leftrightarrow if (t \in (u, w), \|f (t) + i g (t)\|, 0) \leq if (t \in D, \|f (t) + i g (t)\|, 0))$
205		elioore	$⊢ t \in (u, w) \to t \in ℝ$
206	205 172	sylan2	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in (u, w)) \to \|f (t) + i g (t)\| \leq \|f (t) + i g (t)\|$
207	206	adantll	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in (u, w)) \to \|f (t) + i g (t)\| \leq \|f (t) + i g (t)\|$
208	207	adantlr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to \|f (t) + i g (t)\| \leq \|f (t) + i g (t)\|$
209	2	rexrd	$⊢ φ \to A \in ℝ^{*}$
210	3	rexrd	$⊢ φ \to B \in ℝ^{*}$
211	209 210	jca	$⊢ φ \to (A \in ℝ^{} \land B \in ℝ^{})$
212		df-icc	$⊢ [.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{t \in ℝ^{*} \| (x \leq t \land t \leq y)\})$
213	212	elixx3g	$⊢ u \in [A, B] \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land u \in ℝ^{*}) \land (A \leq u \land u \leq B))$
214	213	simprbi	$⊢ u \in [A, B] \to (A \leq u \land u \leq B)$
215	214	simpld	$⊢ u \in [A, B] \to A \leq u$
216	212	elixx3g	$⊢ w \in [A, B] \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land w \in ℝ^{*}) \land (A \leq w \land w \leq B))$
217	216	simprbi	$⊢ w \in [A, B] \to (A \leq w \land w \leq B)$
218	217	simprd	$⊢ w \in [A, B] \to w \leq B$
219	215 218	anim12i	$⊢ (u \in [A, B] \land w \in [A, B]) \to (A \leq u \land w \leq B)$
220		ioossioo	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A \leq u \land w \leq B)) \to (u, w) \subseteq (A, B)$
221	211 219 220	syl2an	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (u, w) \subseteq (A, B)$
222	5	adantr	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (A, B) \subseteq D$
223	221 222	sstrd	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (u, w) \subseteq D$
224	223	sselda	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to t \in D$
225		iftrue	$⊢ t \in D \to if (t \in D, \|f (t) + i g (t)\|, 0) = \|f (t) + i g (t)\|$
226	224 225	syl	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to if (t \in D, \|f (t) + i g (t)\|, 0) = \|f (t) + i g (t)\|$
227	226	adantllr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to if (t \in D, \|f (t) + i g (t)\|, 0) = \|f (t) + i g (t)\|$
228	208 227	breqtrrd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to \|f (t) + i g (t)\| \leq if (t \in D, \|f (t) + i g (t)\|, 0)$
229		breq2	$⊢ \|f (t) + i g (t)\| = if (t \in D, \|f (t) + i g (t)\|, 0) \to (0 \leq \|f (t) + i g (t)\| \leftrightarrow 0 \leq if (t \in D, \|f (t) + i g (t)\|, 0))$
230		breq2	$⊢ 0 = if (t \in D, \|f (t) + i g (t)\|, 0) \to (0 \leq 0 \leftrightarrow 0 \leq if (t \in D, \|f (t) + i g (t)\|, 0))$
231	6	sselda	$⊢ (φ \land t \in D) \to t \in ℝ$
232	231	adantlr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to t \in ℝ$
233	71	adantll	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to 0 \leq \|f (t) + i g (t)\|$
234	232 233	syldan	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to 0 \leq \|f (t) + i g (t)\|$
235		0le0	$⊢ 0 \leq 0$
236	235	a1i	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \neg t \in D) \to 0 \leq 0$
237	229 230 234 236	ifbothda	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to 0 \leq if (t \in D, \|f (t) + i g (t)\|, 0)$
238	237	ad2antrr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land \neg t \in (u, w)) \to 0 \leq if (t \in D, \|f (t) + i g (t)\|, 0)$
239	203 204 228 238	ifbothda	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) \leq if (t \in D, \|f (t) + i g (t)\|, 0)$
240	239	ralrimivw	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to \forall t \in ℝ if (t \in (u, w), \|f (t) + i g (t)\|, 0) \leq if (t \in D, \|f (t) + i g (t)\|, 0)$
241	40	a1i	$⊢ φ \to ℝ \in V$
242	18	a1i	$⊢ (φ \land t \in ℝ) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) \in V$
243	16 17	ifex	$⊢ if (t \in D, \|f (t) + i g (t)\|, 0) \in V$
244	243	a1i	$⊢ (φ \land t \in ℝ) \to if (t \in D, \|f (t) + i g (t)\|, 0) \in V$
245		eqidd	$⊢ φ \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) = (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))$
246		eqidd	$⊢ φ \to (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) = (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))$
247	241 242 244 245 246	ofrfval2	$⊢ φ \to ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \leq_{f} (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) \leftrightarrow \forall t \in ℝ if (t \in (u, w), \|f (t) + i g (t)\|, 0) \leq if (t \in D, \|f (t) + i g (t)\|, 0))$
248	247	ad2antrr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \leq_{f} (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) \leftrightarrow \forall t \in ℝ if (t \in (u, w), \|f (t) + i g (t)\|, 0) \leq if (t \in D, \|f (t) + i g (t)\|, 0))$
249	240 248	mpbird	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \leq_{f} (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))$
250		itg2le	$⊢ ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞] \land (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞] \land (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \leq_{f} (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)))$
251	86 202 249 250	syl3anc	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)))$
252		itg2lecl	$⊢ ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞] \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) \in ℝ \land \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)))) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \in ℝ$
253	86 201 251 252	syl3anc	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \in ℝ$
254	8	ffvelcdmda	$⊢ (φ \land t \in D) \to F (t) \in ℂ$
255	254	adantlr	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land t \in D) \to F (t) \in ℂ$
256	224 255	syldan	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to F (t) \in ℂ$
257	256	adantllr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to F (t) \in ℂ$
258	205 39	sylan2	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in (u, w)) \to f (t) + i g (t) \in ℂ$
259	258	adantll	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in (u, w)) \to f (t) + i g (t) \in ℂ$
260	259	adantlr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to f (t) + i g (t) \in ℂ$
261	257 260	subcld	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to F (t) - (f (t) + i g (t)) \in ℂ$
262	261	abscld	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to \|F (t) - (f (t) + i g (t))\| \in ℝ$
263	261	absge0d	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to 0 \leq \|F (t) - (f (t) + i g (t))\|$
264		elrege0	$⊢ \|F (t) - (f (t) + i g (t))\| \in [0, +∞) \leftrightarrow (\|F (t) - (f (t) + i g (t))\| \in ℝ \land 0 \leq \|F (t) - (f (t) + i g (t))\|)$
265	262 263 264	sylanbrc	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to \|F (t) - (f (t) + i g (t))\| \in [0, +∞)$
266	74	a1i	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land \neg t \in (u, w)) \to 0 \in [0, +∞)$
267	265 266	ifclda	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \in [0, +∞)$
268	267	adantr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in ℝ) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \in [0, +∞)$
269	268	fmpttd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) : ℝ ⟶ [0, +∞)$
270	262	rexrd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to \|F (t) - (f (t) + i g (t))\| \in ℝ^{*}$
271		elxrge0	$⊢ \|F (t) - (f (t) + i g (t))\| \in [0, +∞] \leftrightarrow (\|F (t) - (f (t) + i g (t))\| \in ℝ^{*} \land 0 \leq \|F (t) - (f (t) + i g (t))\|)$
272	270 263 271	sylanbrc	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to \|F (t) - (f (t) + i g (t))\| \in [0, +∞]$
273	82	a1i	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land \neg t \in (u, w)) \to 0 \in [0, +∞]$
274	272 273	ifclda	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \in [0, +∞]$
275	274	adantr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in ℝ) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \in [0, +∞]$
276	275	fmpttd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) : ℝ ⟶ [0, +∞]$
277		recncf	$⊢ ℜ : ℂ \underset{cn}{⟶} ℝ$
278		prid1g	$⊢ ℜ : ℂ \underset{cn}{⟶} ℝ \to ℜ \in \{ℜ, ℑ\}$
279	277 278	ax-mp	$⊢ ℜ \in \{ℜ, ℑ\}$
280		ftc1anclem2	$⊢ (F : D ⟶ ℂ \land F \in 𝐿^{1} \land ℜ \in \{ℜ, ℑ\}) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))) \in ℝ$
281	279 280	mp3an3	$⊢ (F : D ⟶ ℂ \land F \in 𝐿^{1}) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))) \in ℝ$
282	8 7 281	syl2anc	$⊢ φ \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))) \in ℝ$
283		imcncf	$⊢ ℑ : ℂ \underset{cn}{⟶} ℝ$
284		prid2g	$⊢ ℑ : ℂ \underset{cn}{⟶} ℝ \to ℑ \in \{ℜ, ℑ\}$
285	283 284	ax-mp	$⊢ ℑ \in \{ℜ, ℑ\}$
286		ftc1anclem2	$⊢ (F : D ⟶ ℂ \land F \in 𝐿^{1} \land ℑ \in \{ℜ, ℑ\}) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) \in ℝ$
287	285 286	mp3an3	$⊢ (F : D ⟶ ℂ \land F \in 𝐿^{1}) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) \in ℝ$
288	8 7 287	syl2anc	$⊢ φ \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) \in ℝ$
289	282 288	readdcld	$⊢ φ \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) \in ℝ$
290	289	ad2antrr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) \in ℝ$
291	201 290	readdcld	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) \in ℝ$
292		ge0addcl	$⊢ (x \in [0, +∞) \land y \in [0, +∞)) \to x + y \in [0, +∞)$
293	292	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, +∞)$
294		ifcl	$⊢ (\|f (t) + i g (t)\| \in [0, +∞) \land 0 \in [0, +∞)) \to if (t \in D, \|f (t) + i g (t)\|, 0) \in [0, +∞)$
295	73 74 294	sylancl	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to if (t \in D, \|f (t) + i g (t)\|, 0) \in [0, +∞)$
296	295	fmpttd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞)$
297	296	adantl	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞)$
298	292	adantl	$⊢ (φ \land (x \in [0, +∞) \land y \in [0, +∞))) \to x + y \in [0, +∞)$
299	254	recld	$⊢ (φ \land t \in D) \to ℜ (F (t)) \in ℝ$
300	299	recnd	$⊢ (φ \land t \in D) \to ℜ (F (t)) \in ℂ$
301	300	abscld	$⊢ (φ \land t \in D) \to \|ℜ (F (t))\| \in ℝ$
302	300	absge0d	$⊢ (φ \land t \in D) \to 0 \leq \|ℜ (F (t))\|$
303		elrege0	$⊢ \|ℜ (F (t))\| \in [0, +∞) \leftrightarrow (\|ℜ (F (t))\| \in ℝ \land 0 \leq \|ℜ (F (t))\|)$
304	301 302 303	sylanbrc	$⊢ (φ \land t \in D) \to \|ℜ (F (t))\| \in [0, +∞)$
305	74	a1i	$⊢ (φ \land \neg t \in D) \to 0 \in [0, +∞)$
306	304 305	ifclda	$⊢ φ \to if (t \in D, \|ℜ (F (t))\|, 0) \in [0, +∞)$
307	306	adantr	$⊢ (φ \land t \in ℝ) \to if (t \in D, \|ℜ (F (t))\|, 0) \in [0, +∞)$
308	307	fmpttd	$⊢ φ \to (t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) : ℝ ⟶ [0, +∞)$
309	254	imcld	$⊢ (φ \land t \in D) \to ℑ (F (t)) \in ℝ$
310	309	recnd	$⊢ (φ \land t \in D) \to ℑ (F (t)) \in ℂ$
311	310	abscld	$⊢ (φ \land t \in D) \to \|ℑ (F (t))\| \in ℝ$
312	310	absge0d	$⊢ (φ \land t \in D) \to 0 \leq \|ℑ (F (t))\|$
313		elrege0	$⊢ \|ℑ (F (t))\| \in [0, +∞) \leftrightarrow (\|ℑ (F (t))\| \in ℝ \land 0 \leq \|ℑ (F (t))\|)$
314	311 312 313	sylanbrc	$⊢ (φ \land t \in D) \to \|ℑ (F (t))\| \in [0, +∞)$
315	314 305	ifclda	$⊢ φ \to if (t \in D, \|ℑ (F (t))\|, 0) \in [0, +∞)$
316	315	adantr	$⊢ (φ \land t \in ℝ) \to if (t \in D, \|ℑ (F (t))\|, 0) \in [0, +∞)$
317	316	fmpttd	$⊢ φ \to (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)) : ℝ ⟶ [0, +∞)$
318	298 308 317 241 241 109	off	$⊢ φ \to ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) : ℝ ⟶ [0, +∞)$
319	318	adantr	$⊢ (φ \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 ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) : ℝ ⟶ [0, +∞)$
320	40	a1i	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to ℝ \in V$
321	293 297 319 320 320 109	off	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))) : ℝ ⟶ [0, +∞)$
322		fss	$⊢ (((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))) : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))) : ℝ ⟶ [0, +∞]$
323	321 163 322	sylancl	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))) : ℝ ⟶ [0, +∞]$
324	323	adantr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))) : ℝ ⟶ [0, +∞]$
325		0xr	$⊢ 0 \in ℝ^{*}$
326	325	a1i	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land \neg t \in (u, w)) \to 0 \in ℝ^{*}$
327	270 326	ifclda	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \in ℝ^{*}$
328	254	adantlr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to F (t) \in ℂ$
329	39	adantll	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to f (t) + i g (t) \in ℂ$
330	232 329	syldan	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to f (t) + i g (t) \in ℂ$
331	328 330	subcld	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to F (t) - (f (t) + i g (t)) \in ℂ$
332	331	abscld	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|F (t) - (f (t) + i g (t))\| \in ℝ$
333	332	rexrd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|F (t) - (f (t) + i g (t))\| \in ℝ^{*}$
334	325	a1i	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \neg t \in D) \to 0 \in ℝ^{*}$
335	333 334	ifclda	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) \in ℝ^{*}$
336	335	adantr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) \in ℝ^{*}$
337	330	abscld	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|f (t) + i g (t)\| \in ℝ$
338		0red	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \neg t \in D) \to 0 \in ℝ$
339	337 338	ifclda	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to if (t \in D, \|f (t) + i g (t)\|, 0) \in ℝ$
340		0red	$⊢ (φ \land \neg t \in D) \to 0 \in ℝ$
341	301 340	ifclda	$⊢ φ \to if (t \in D, \|ℜ (F (t))\|, 0) \in ℝ$
342	311 340	ifclda	$⊢ φ \to if (t \in D, \|ℑ (F (t))\|, 0) \in ℝ$
343	341 342	readdcld	$⊢ φ \to if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0) \in ℝ$
344	343	adantr	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0) \in ℝ$
345	339 344	readdcld	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0) \in ℝ$
346	345	rexrd	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0) \in ℝ^{*}$
347	346	adantr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0) \in ℝ^{*}$
348		breq1	$⊢ \|F (t) - (f (t) + i g (t))\| = if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \to (\|F (t) - (f (t) + i g (t))\| \leq if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) \leftrightarrow if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \leq if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0))$
349		breq1	$⊢ 0 = if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \to (0 \leq if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) \leftrightarrow if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \leq if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0))$
350	224	adantllr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to t \in D$
351	332	leidd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|F (t) - (f (t) + i g (t))\| \leq \|F (t) - (f (t) + i g (t))\|$
352	351	adantlr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in D) \to \|F (t) - (f (t) + i g (t))\| \leq \|F (t) - (f (t) + i g (t))\|$
353		iftrue	$⊢ t \in D \to if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) = \|F (t) - (f (t) + i g (t))\|$
354	353	adantl	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in D) \to if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) = \|F (t) - (f (t) + i g (t))\|$
355	352 354	breqtrrd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in D) \to \|F (t) - (f (t) + i g (t))\| \leq if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0)$
356	350 355	syldan	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to \|F (t) - (f (t) + i g (t))\| \leq if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0)$
357		breq2	$⊢ \|F (t) - (f (t) + i g (t))\| = if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) \to (0 \leq \|F (t) - (f (t) + i g (t))\| \leftrightarrow 0 \leq if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0))$
358		breq2	$⊢ 0 = if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) \to (0 \leq 0 \leftrightarrow 0 \leq if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0))$
359	331	absge0d	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to 0 \leq \|F (t) - (f (t) + i g (t))\|$
360	357 358 359 236	ifbothda	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to 0 \leq if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0)$
361	360	ad2antrr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land \neg t \in (u, w)) \to 0 \leq if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0)$
362	348 349 356 361	ifbothda	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \leq if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0)$
363	254	negcld	$⊢ (φ \land t \in D) \to - F (t) \in ℂ$
364	363	adantlr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to - F (t) \in ℂ$
365	330 364	addcld	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to f (t) + i g (t) + (- F (t)) \in ℂ$
366	365	abscld	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|f (t) + i g (t) + (- F (t))\| \in ℝ$
367	363	abscld	$⊢ (φ \land t \in D) \to \|- F (t)\| \in ℝ$
368	367	adantlr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|- F (t)\| \in ℝ$
369	337 368	readdcld	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|f (t) + i g (t)\| + \|- F (t)\| \in ℝ$
370	301 311	readdcld	$⊢ (φ \land t \in D) \to \|ℜ (F (t))\| + \|ℑ (F (t))\| \in ℝ$
371	370	adantlr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|ℜ (F (t))\| + \|ℑ (F (t))\| \in ℝ$
372	337 371	readdcld	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\| \in ℝ$
373	330 364	abstrid	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|f (t) + i g (t) + (- F (t))\| \leq \|f (t) + i g (t)\| + \|- F (t)\|$
374		mulcl	$⊢ (i \in ℂ \land ℑ (F (t)) \in ℂ) \to i ℑ (F (t)) \in ℂ$
375	31 310 374	sylancr	$⊢ (φ \land t \in D) \to i ℑ (F (t)) \in ℂ$
376	300 375	abstrid	$⊢ (φ \land t \in D) \to \|ℜ (F (t)) + i ℑ (F (t))\| \leq \|ℜ (F (t))\| + \|i ℑ (F (t))\|$
377	254	absnegd	$⊢ (φ \land t \in D) \to \|- F (t)\| = \|F (t)\|$
378	254	replimd	$⊢ (φ \land t \in D) \to F (t) = ℜ (F (t)) + i ℑ (F (t))$
379	378	fveq2d	$⊢ (φ \land t \in D) \to \|F (t)\| = \|ℜ (F (t)) + i ℑ (F (t))\|$
380	377 379	eqtrd	$⊢ (φ \land t \in D) \to \|- F (t)\| = \|ℜ (F (t)) + i ℑ (F (t))\|$
381		absmul	$⊢ (i \in ℂ \land ℑ (F (t)) \in ℂ) \to \|i ℑ (F (t))\| = \|i\| \|ℑ (F (t))\|$
382	31 310 381	sylancr	$⊢ (φ \land t \in D) \to \|i ℑ (F (t))\| = \|i\| \|ℑ (F (t))\|$
383	182	oveq1i	$⊢ \|i\| \|ℑ (F (t))\| = 1 \|ℑ (F (t))\|$
384	382 383	eqtrdi	$⊢ (φ \land t \in D) \to \|i ℑ (F (t))\| = 1 \|ℑ (F (t))\|$
385	311	recnd	$⊢ (φ \land t \in D) \to \|ℑ (F (t))\| \in ℂ$
386	385	mullidd	$⊢ (φ \land t \in D) \to 1 \|ℑ (F (t))\| = \|ℑ (F (t))\|$
387	384 386	eqtr2d	$⊢ (φ \land t \in D) \to \|ℑ (F (t))\| = \|i ℑ (F (t))\|$
388	387	oveq2d	$⊢ (φ \land t \in D) \to \|ℜ (F (t))\| + \|ℑ (F (t))\| = \|ℜ (F (t))\| + \|i ℑ (F (t))\|$
389	376 380 388	3brtr4d	$⊢ (φ \land t \in D) \to \|- F (t)\| \leq \|ℜ (F (t))\| + \|ℑ (F (t))\|$
390	389	adantlr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|- F (t)\| \leq \|ℜ (F (t))\| + \|ℑ (F (t))\|$
391	368 371 337 390	leadd2dd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|f (t) + i g (t)\| + \|- F (t)\| \leq \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|$
392	366 369 372 373 391	letrd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|f (t) + i g (t) + (- F (t))\| \leq \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|$
393	328 330	abssubd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|F (t) - (f (t) + i g (t))\| = \|f (t) + i g (t) - F (t)\|$
394	353	adantl	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) = \|F (t) - (f (t) + i g (t))\|$
395	330 328	negsubd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to f (t) + i g (t) + (- F (t)) = f (t) + i g (t) - F (t)$
396	395	fveq2d	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|f (t) + i g (t) + (- F (t))\| = \|f (t) + i g (t) - F (t)\|$
397	393 394 396	3eqtr4d	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) = \|f (t) + i g (t) + (- F (t))\|$
398		iftrue	$⊢ t \in D \to if (t \in D, \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|, 0) = \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|$
399	398	adantl	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to if (t \in D, \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|, 0) = \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|$
400	392 397 399	3brtr4d	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) \leq if (t \in D, \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|, 0)$
401	400	ex	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in D \to if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) \leq if (t \in D, \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|, 0))$
402	235	a1i	$⊢ \neg t \in D \to 0 \leq 0$
403		iffalse	$⊢ \neg t \in D \to if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) = 0$
404		iffalse	$⊢ \neg t \in D \to if (t \in D, \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|, 0) = 0$
405	402 403 404	3brtr4d	$⊢ \neg t \in D \to if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) \leq if (t \in D, \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|, 0)$
406	401 405	pm2.61d1	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) \leq if (t \in D, \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|, 0)$
407		iftrue	$⊢ t \in D \to if (t \in D, \|ℜ (F (t))\|, 0) = \|ℜ (F (t))\|$
408		iftrue	$⊢ t \in D \to if (t \in D, \|ℑ (F (t))\|, 0) = \|ℑ (F (t))\|$
409	407 408	oveq12d	$⊢ t \in D \to if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0) = \|ℜ (F (t))\| + \|ℑ (F (t))\|$
410	225 409	oveq12d	$⊢ t \in D \to if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0) = \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|$
411	410 398	eqtr4d	$⊢ t \in D \to if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0) = if (t \in D, \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|, 0)$
412		00id	$⊢ 0 + 0 = 0$
413	412	oveq2i	$⊢ 0 + 0 + 0 = 0 + 0$
414	413 412	eqtri	$⊢ 0 + 0 + 0 = 0$
415		iffalse	$⊢ \neg t \in D \to if (t \in D, \|f (t) + i g (t)\|, 0) = 0$
416		iffalse	$⊢ \neg t \in D \to if (t \in D, \|ℜ (F (t))\|, 0) = 0$
417		iffalse	$⊢ \neg t \in D \to if (t \in D, \|ℑ (F (t))\|, 0) = 0$
418	416 417	oveq12d	$⊢ \neg t \in D \to if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0) = 0 + 0$
419	415 418	oveq12d	$⊢ \neg t \in D \to if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0) = 0 + 0 + 0$
420	414 419 404	3eqtr4a	$⊢ \neg t \in D \to if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0) = if (t \in D, \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|, 0)$
421	411 420	pm2.61i	$⊢ if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0) = if (t \in D, \|f (t) + i g (t)\| + \|ℜ (F (t))\| + \|ℑ (F (t))\|, 0)$
422	406 421	breqtrrdi	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) \leq if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0)$
423	422	adantr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to if (t \in D, \|F (t) - (f (t) + i g (t))\|, 0) \leq if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0)$
424	327 336 347 362 423	xrletrd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \leq if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0)$
425	424	ralrimivw	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to \forall t \in ℝ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \leq if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0)$
426		fvex	$⊢ \|F (t) - (f (t) + i g (t))\| \in V$
427	426 17	ifex	$⊢ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \in V$
428	427	a1i	$⊢ (φ \land t \in ℝ) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \in V$
429		ovexd	$⊢ (φ \land t \in ℝ) \to if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0) \in V$
430		eqidd	$⊢ φ \to (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) = (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))$
431		ovexd	$⊢ (φ \land t \in ℝ) \to if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0) \in V$
432	341	adantr	$⊢ (φ \land t \in ℝ) \to if (t \in D, \|ℜ (F (t))\|, 0) \in ℝ$
433	342	adantr	$⊢ (φ \land t \in ℝ) \to if (t \in D, \|ℑ (F (t))\|, 0) \in ℝ$
434		eqidd	$⊢ φ \to (t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) = (t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))$
435		eqidd	$⊢ φ \to (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)) = (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))$
436	241 432 433 434 435	offval2	$⊢ φ \to (t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)) = (t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0))$
437	241 244 431 246 436	offval2	$⊢ φ \to (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) = (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0))$
438	241 428 429 430 437	ofrfval2	$⊢ φ \to ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) \leq_{f} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))) \leftrightarrow \forall t \in ℝ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \leq if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0))$
439	438	ad2antrr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) \leq_{f} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))) \leftrightarrow \forall t \in ℝ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \leq if (t \in D, \|f (t) + i g (t)\|, 0) + if (t \in D, \|ℜ (F (t))\|, 0) + if (t \in D, \|ℑ (F (t))\|, 0))$
440	425 439	mpbird	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) \leq_{f} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))))$
441		itg2le	$⊢ ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) : ℝ ⟶ [0, +∞] \land ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))) : ℝ ⟶ [0, +∞] \land (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) \leq_{f} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))))) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))))$
442	276 324 440 441	syl3anc	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))))$
443	6	adantr	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to D \subseteq ℝ$
444	243	a1i	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to if (t \in D, \|f (t) + i g (t)\|, 0) \in V$
445		eldifn	$⊢ t \in (ℝ ∖ D) \to \neg t \in D$
446	445	iffalsed	$⊢ t \in (ℝ ∖ D) \to if (t \in D, \|f (t) + i g (t)\|, 0) = 0$
447	446	adantl	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in (ℝ ∖ D)) \to if (t \in D, \|f (t) + i g (t)\|, 0) = 0$
448		ovexd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to i g (t) \in V$
449	41 42 448 45 52	offval2	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to f +_{f} ((ℝ \times \{i\}) \times_{f} g) = (t \in ℝ ⟼ f (t) + i g (t))$
450	39 449 56 57	fmptco	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} g)) = (t \in ℝ ⟼ \|f (t) + i g (t)\|)$
451	450	reseq1d	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to {(abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} g))) ↾}_{D} = {(t \in ℝ ⟼ \|f (t) + i g (t)\|) ↾}_{D}$
452	6	resmptd	$⊢ φ \to {(t \in ℝ ⟼ \|f (t) + i g (t)\|) ↾}_{D} = (t \in D ⟼ \|f (t) + i g (t)\|)$
453	451 452	sylan9eqr	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to {(abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} g))) ↾}_{D} = (t \in D ⟼ \|f (t) + i g (t)\|)$
454	225	mpteq2ia	$⊢ (t \in D ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) = (t \in D ⟼ \|f (t) + i g (t)\|)$
455	453 454	eqtr4di	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to {(abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} g))) ↾}_{D} = (t \in D ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))$
456		i1fmbf	$⊢ abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} g)) \in dom \int^{1} \to abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} g)) \in MblFn$
457	59 456	syl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} g)) \in MblFn$
458	8	fdmd	$⊢ φ \to dom F = D$
459		iblmbf	$⊢ F \in 𝐿^{1} \to F \in MblFn$
460		mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$
461	7 459 460	3syl	$⊢ φ \to dom F \in dom vol$
462	458 461	eqeltrrd	$⊢ φ \to D \in dom vol$
463		mbfres	$⊢ (abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} g)) \in MblFn \land D \in dom vol) \to {(abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} g))) ↾}_{D} \in MblFn$
464	457 462 463	syl2anr	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to {(abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} g))) ↾}_{D} \in MblFn$
465	455 464	eqeltrrd	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in D ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) \in MblFn$
466	443 15 444 447 465	mbfss	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) \in MblFn$
467	200	adantl	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) \in ℝ$
468		0cnd	$⊢ (φ \land \neg t \in D) \to 0 \in ℂ$
469	300 468	ifclda	$⊢ φ \to if (t \in D, ℜ (F (t)), 0) \in ℂ$
470	469	adantr	$⊢ (φ \land t \in ℝ) \to if (t \in D, ℜ (F (t)), 0) \in ℂ$
471		eqidd	$⊢ φ \to (t \in ℝ ⟼ if (t \in D, ℜ (F (t)), 0)) = (t \in ℝ ⟼ if (t \in D, ℜ (F (t)), 0))$
472	54	a1i	$⊢ φ \to abs : ℂ ⟶ ℝ$
473	472	feqmptd	$⊢ φ \to abs = (x \in ℂ ⟼ \|x\|)$
474		fveq2	$⊢ x = if (t \in D, ℜ (F (t)), 0) \to \|x\| = \|if (t \in D, ℜ (F (t)), 0)\|$
475		fvif	$⊢ \|if (t \in D, ℜ (F (t)), 0)\| = if (t \in D, \|ℜ (F (t))\|, \|0\|)$
476		abs0	$⊢ \|0\| = 0$
477		ifeq2	$⊢ \|0\| = 0 \to if (t \in D, \|ℜ (F (t))\|, \|0\|) = if (t \in D, \|ℜ (F (t))\|, 0)$
478	476 477	ax-mp	$⊢ if (t \in D, \|ℜ (F (t))\|, \|0\|) = if (t \in D, \|ℜ (F (t))\|, 0)$
479	475 478	eqtri	$⊢ \|if (t \in D, ℜ (F (t)), 0)\| = if (t \in D, \|ℜ (F (t))\|, 0)$
480	474 479	eqtrdi	$⊢ x = if (t \in D, ℜ (F (t)), 0) \to \|x\| = if (t \in D, \|ℜ (F (t))\|, 0)$
481	470 471 473 480	fmptco	$⊢ φ \to abs \circ (t \in ℝ ⟼ if (t \in D, ℜ (F (t)), 0)) = (t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))$
482	299 340	ifclda	$⊢ φ \to if (t \in D, ℜ (F (t)), 0) \in ℝ$
483	482	adantr	$⊢ (φ \land t \in ℝ) \to if (t \in D, ℜ (F (t)), 0) \in ℝ$
484	483	fmpttd	$⊢ φ \to (t \in ℝ ⟼ if (t \in D, ℜ (F (t)), 0)) : ℝ ⟶ ℝ$
485	14	a1i	$⊢ φ \to ℝ \in dom vol$
486	482	adantr	$⊢ (φ \land t \in D) \to if (t \in D, ℜ (F (t)), 0) \in ℝ$
487	445	adantl	$⊢ (φ \land t \in (ℝ ∖ D)) \to \neg t \in D$
488	487	iffalsed	$⊢ (φ \land t \in (ℝ ∖ D)) \to if (t \in D, ℜ (F (t)), 0) = 0$
489		iftrue	$⊢ t \in D \to if (t \in D, ℜ (F (t)), 0) = ℜ (F (t))$
490	489	mpteq2ia	$⊢ (t \in D ⟼ if (t \in D, ℜ (F (t)), 0)) = (t \in D ⟼ ℜ (F (t)))$
491	8	feqmptd	$⊢ φ \to F = (t \in D ⟼ F (t))$
492	7 459	syl	$⊢ φ \to F \in MblFn$
493	491 492	eqeltrrd	$⊢ φ \to (t \in D ⟼ F (t)) \in MblFn$
494	254	ismbfcn2	$⊢ φ \to ((t \in D ⟼ F (t)) \in MblFn \leftrightarrow ((t \in D ⟼ ℜ (F (t))) \in MblFn \land (t \in D ⟼ ℑ (F (t))) \in MblFn))$
495	493 494	mpbid	$⊢ φ \to ((t \in D ⟼ ℜ (F (t))) \in MblFn \land (t \in D ⟼ ℑ (F (t))) \in MblFn)$
496	495	simpld	$⊢ φ \to (t \in D ⟼ ℜ (F (t))) \in MblFn$
497	490 496	eqeltrid	$⊢ φ \to (t \in D ⟼ if (t \in D, ℜ (F (t)), 0)) \in MblFn$
498	6 485 486 488 497	mbfss	$⊢ φ \to (t \in ℝ ⟼ if (t \in D, ℜ (F (t)), 0)) \in MblFn$
499		ftc1anclem1	$⊢ ((t \in ℝ ⟼ if (t \in D, ℜ (F (t)), 0)) : ℝ ⟶ ℝ \land (t \in ℝ ⟼ if (t \in D, ℜ (F (t)), 0)) \in MblFn) \to abs \circ (t \in ℝ ⟼ if (t \in D, ℜ (F (t)), 0)) \in MblFn$
500	484 498 499	syl2anc	$⊢ φ \to abs \circ (t \in ℝ ⟼ if (t \in D, ℜ (F (t)), 0)) \in MblFn$
501	481 500	eqeltrrd	$⊢ φ \to (t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) \in MblFn$
502	501 308 282 317 288	itg2addnc	$⊢ φ \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) = \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))$
503	502 289	eqeltrd	$⊢ φ \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) \in ℝ$
504	503	adantr	$⊢ (φ \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 ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) \in ℝ$
505	466 297 467 319 504	itg2addnc	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))) = \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))$
506	502	adantr	$⊢ (φ \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 ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) = \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))$
507	506	oveq2d	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) = \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))$
508	505 507	eqtrd	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))) = \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))$
509	508	adantr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0)) +_{f} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))) = \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))$
510	442 509	breqtrd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))$
511		itg2lecl	$⊢ ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) : ℝ ⟶ [0, +∞] \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0))) \in ℝ \land \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|f (t) + i g (t)\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℜ (F (t))\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in D, \|ℑ (F (t))\|, 0)))) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) \in ℝ$
512	276 291 510 511	syl3anc	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) \in ℝ$
513	69 78 253 269 512	itg2addnc	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) = \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)))$
514	241 242 428 245 430	offval2	$⊢ φ \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) = (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0) + if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))$
515		eqeq2	$⊢ \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\| = if (t \in (u, w), \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\|, 0) \to (if (t \in (u, w), \|f (t) + i g (t)\|, 0) + if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) = \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\| \leftrightarrow if (t \in (u, w), \|f (t) + i g (t)\|, 0) + if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) = if (t \in (u, w), \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\|, 0))$
516		eqeq2	$⊢ 0 = if (t \in (u, w), \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\|, 0) \to (if (t \in (u, w), \|f (t) + i g (t)\|, 0) + if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) = 0 \leftrightarrow if (t \in (u, w), \|f (t) + i g (t)\|, 0) + if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) = if (t \in (u, w), \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\|, 0))$
517		iftrue	$⊢ t \in (u, w) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) = \|F (t) - (f (t) + i g (t))\|$
518	23 517	oveq12d	$⊢ t \in (u, w) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) + if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) = \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\|$
519	518	adantl	$⊢ (φ \land t \in (u, w)) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) + if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) = \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\|$
520		iffalse	$⊢ \neg t \in (u, w) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) = 0$
521		iffalse	$⊢ \neg t \in (u, w) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) = 0$
522	520 521	oveq12d	$⊢ \neg t \in (u, w) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) + if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) = 0 + 0$
523	522 412	eqtrdi	$⊢ \neg t \in (u, w) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) + if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) = 0$
524	523	adantl	$⊢ (φ \land \neg t \in (u, w)) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) + if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) = 0$
525	515 516 519 524	ifbothda	$⊢ φ \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) + if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) = if (t \in (u, w), \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\|, 0)$
526	525	mpteq2dv	$⊢ φ \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0) + if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) = (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\|, 0))$
527	514 526	eqtrd	$⊢ φ \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) = (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\|, 0))$
528	527	ad2antrr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) = (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\|, 0))$
529		simplr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to (f \in dom \int^{1} \land g \in dom \int^{1})$
530	258	abscld	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in (u, w)) \to \|f (t) + i g (t)\| \in ℝ$
531	530	recnd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in (u, w)) \to \|f (t) + i g (t)\| \in ℂ$
532	529 531	sylan	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to \|f (t) + i g (t)\| \in ℂ$
533	262	recnd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to \|F (t) - (f (t) + i g (t))\| \in ℂ$
534	532 533	addcomd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\| = \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|$
535	534	ifeq1da	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to if (t \in (u, w), \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\|, 0) = if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)$
536	535	mpteq2dv	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\| + \|F (t) - (f (t) + i g (t))\|, 0)) = (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0))$
537	528 536	eqtrd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) = (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0))$
538	537	fveq2d	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) +_{f} (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) = \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)))$
539	513 538	eqtr3d	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) = \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)))$
540	10 11 539	syl2an	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2}) \land \exists r \in (ran f \cup ran g) r \neq 0) \land y \in ℝ^{+}) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) = \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)))$
541	540	adantr	$⊢ ((((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2}) \land \exists r \in (ran f \cup ran g) r \neq 0) \land y \in ℝ^{+}) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land \|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)}) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) + \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) = \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)))$
542		rpcn	$⊢ y \in ℝ^{+} \to y \in ℂ$
543	542	2halvesd	$⊢ y \in ℝ^{+} \to (\frac{y}{2}) + (\frac{y}{2}) = y$
544	543	ad3antlr	$⊢ ((((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2}) \land \exists r \in (ran f \cup ran g) r \neq 0) \land y \in ℝ^{+}) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land \|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)}) \to (\frac{y}{2}) + (\frac{y}{2}) = y$
545	9 541 544	3brtr3d	$⊢ ((((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2}) \land \exists r \in (ran f \cup ran g) r \neq 0) \land y \in ℝ^{+}) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land \|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)}) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0))) < y$

Metamath Proof Explorer

Theorem ftc1anclem8

Proof