ftc1anclem7

	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	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})$

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		i1ff	$⊢ f \in dom \int^{1} \to f : ℝ ⟶ ℝ$
10	9	ffvelcdmda	$⊢ (f \in dom \int^{1} \land x \in ℝ) \to f (x) \in ℝ$
11	10	recnd	$⊢ (f \in dom \int^{1} \land x \in ℝ) \to f (x) \in ℂ$
12		ax-icn	$⊢ i \in ℂ$
13		i1ff	$⊢ g \in dom \int^{1} \to g : ℝ ⟶ ℝ$
14	13	ffvelcdmda	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to g (x) \in ℝ$
15	14	recnd	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to g (x) \in ℂ$
16		mulcl	$⊢ (i \in ℂ \land g (x) \in ℂ) \to i g (x) \in ℂ$
17	12 15 16	sylancr	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to i g (x) \in ℂ$
18		addcl	$⊢ (f (x) \in ℂ \land i g (x) \in ℂ) \to f (x) + i g (x) \in ℂ$
19	11 17 18	syl2an	$⊢ ((f \in dom \int^{1} \land x \in ℝ) \land (g \in dom \int^{1} \land x \in ℝ)) \to f (x) + i g (x) \in ℂ$
20	19	anandirs	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land x \in ℝ) \to f (x) + i g (x) \in ℂ$
21		reex	$⊢ ℝ \in V$
22	21	a1i	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ℝ \in V$
23	10	adantlr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land x \in ℝ) \to f (x) \in ℝ$
24		ovexd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land x \in ℝ) \to i g (x) \in V$
25	9	feqmptd	$⊢ f \in dom \int^{1} \to f = (x \in ℝ ⟼ f (x))$
26	25	adantr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to f = (x \in ℝ ⟼ f (x))$
27	21	a1i	$⊢ g \in dom \int^{1} \to ℝ \in V$
28	12	a1i	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to i \in ℂ$
29		fconstmpt	$⊢ ℝ \times \{i\} = (x \in ℝ ⟼ i)$
30	29	a1i	$⊢ g \in dom \int^{1} \to ℝ \times \{i\} = (x \in ℝ ⟼ i)$
31	13	feqmptd	$⊢ g \in dom \int^{1} \to g = (x \in ℝ ⟼ g (x))$
32	27 28 14 30 31	offval2	$⊢ g \in dom \int^{1} \to (ℝ \times \{i\}) \times_{f} g = (x \in ℝ ⟼ i g (x))$
33	32	adantl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (ℝ \times \{i\}) \times_{f} g = (x \in ℝ ⟼ i g (x))$
34	22 23 24 26 33	offval2	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to f +_{f} ((ℝ \times \{i\}) \times_{f} g) = (x \in ℝ ⟼ f (x) + i g (x))$
35		absf	$⊢ abs : ℂ ⟶ ℝ$
36	35	a1i	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs : ℂ ⟶ ℝ$
37	36	feqmptd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs = (t \in ℂ ⟼ \|t\|)$
38		fveq2	$⊢ t = f (x) + i g (x) \to \|t\| = \|f (x) + i g (x)\|$
39	20 34 37 38	fmptco	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs \circ (f +_{f} ((ℝ \times \{i\}) \times_{f} g)) = (x \in ℝ ⟼ \|f (x) + i g (x)\|)$
40		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}$
41	39 40	eqeltrrd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (x \in ℝ ⟼ \|f (x) + i g (x)\|) \in dom \int^{1}$
42		ioombl	$⊢ (u, w) \in dom vol$
43		fveq2	$⊢ x = t \to f (x) = f (t)$
44		fveq2	$⊢ x = t \to g (x) = g (t)$
45	44	oveq2d	$⊢ x = t \to i g (x) = i g (t)$
46	43 45	oveq12d	$⊢ x = t \to f (x) + i g (x) = f (t) + i g (t)$
47	46	fveq2d	$⊢ x = t \to \|f (x) + i g (x)\| = \|f (t) + i g (t)\|$
48		eqid	$⊢ (x \in ℝ ⟼ \|f (x) + i g (x)\|) = (x \in ℝ ⟼ \|f (x) + i g (x)\|)$
49		fvex	$⊢ \|f (t) + i g (t)\| \in V$
50	47 48 49	fvmpt	$⊢ t \in ℝ \to (x \in ℝ ⟼ \|f (x) + i g (x)\|) (t) = \|f (t) + i g (t)\|$
51	50	eqcomd	$⊢ t \in ℝ \to \|f (t) + i g (t)\| = (x \in ℝ ⟼ \|f (x) + i g (x)\|) (t)$
52	51	ifeq1d	$⊢ t \in ℝ \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) = if (t \in (u, w), (x \in ℝ ⟼ \|f (x) + i g (x)\|) (t), 0)$
53	52	mpteq2ia	$⊢ (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) = (t \in ℝ ⟼ if (t \in (u, w), (x \in ℝ ⟼ \|f (x) + i g (x)\|) (t), 0))$
54	53	i1fres	$⊢ ((x \in ℝ ⟼ \|f (x) + i g (x)\|) \in dom \int^{1} \land (u, w) \in dom vol) \to (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \in dom \int^{1}$
55	41 42 54	sylancl	$⊢ (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 dom \int^{1}$
56		breq2	$⊢ \|f (t) + i g (t)\| = if (t \in (u, w), \|f (t) + i g (t)\|, 0) \to (0 \leq \|f (t) + i g (t)\| \leftrightarrow 0 \leq if (t \in (u, w), \|f (t) + i g (t)\|, 0))$
57		breq2	$⊢ 0 = if (t \in (u, w), \|f (t) + i g (t)\|, 0) \to (0 \leq 0 \leftrightarrow 0 \leq if (t \in (u, w), \|f (t) + i g (t)\|, 0))$
58		elioore	$⊢ t \in (u, w) \to t \in ℝ$
59		eleq1w	$⊢ x = t \to (x \in ℝ \leftrightarrow t \in ℝ)$
60	59	anbi2d	$⊢ x = t \to (((f \in dom \int^{1} \land g \in dom \int^{1}) \land x \in ℝ) \leftrightarrow ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ))$
61	46	eleq1d	$⊢ x = t \to (f (x) + i g (x) \in ℂ \leftrightarrow f (t) + i g (t) \in ℂ)$
62	60 61	imbi12d	$⊢ x = t \to ((((f \in dom \int^{1} \land g \in dom \int^{1}) \land x \in ℝ) \to f (x) + i g (x) \in ℂ) \leftrightarrow (((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to f (t) + i g (t) \in ℂ))$
63	62 20	chvarvv	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to f (t) + i g (t) \in ℂ$
64	63	absge0d	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to 0 \leq \|f (t) + i g (t)\|$
65	58 64	sylan2	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in (u, w)) \to 0 \leq \|f (t) + i g (t)\|$
66		0le0	$⊢ 0 \leq 0$
67	66	a1i	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land \neg t \in (u, w)) \to 0 \leq 0$
68	56 57 65 67	ifbothda	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to 0 \leq if (t \in (u, w), \|f (t) + i g (t)\|, 0)$
69	68	ralrimivw	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to \forall t \in ℝ 0 \leq if (t \in (u, w), \|f (t) + i g (t)\|, 0)$
70		ax-resscn	$⊢ ℝ \subseteq ℂ$
71	70	a1i	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ℝ \subseteq ℂ$
72		c0ex	$⊢ 0 \in V$
73	49 72	ifex	$⊢ if (t \in (u, w), \|f (t) + i g (t)\|, 0) \in V$
74		eqid	$⊢ (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))$
75	73 74	fnmpti	$⊢ (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) Fn ℝ$
76	75	a1i	$⊢ (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)) Fn ℝ$
77	71 76	0pledm	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (0_{𝑝} \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \leftrightarrow (ℝ \times \{0\}) \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))$
78	72	a1i	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to 0 \in V$
79	73	a1i	$⊢ ((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 V$
80		fconstmpt	$⊢ ℝ \times \{0\} = (t \in ℝ ⟼ 0)$
81	80	a1i	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ℝ \times \{0\} = (t \in ℝ ⟼ 0)$
82		eqidd	$⊢ (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)) = (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))$
83	22 78 79 81 82	ofrfval2	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ((ℝ \times \{0\}) \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \leftrightarrow \forall t \in ℝ 0 \leq if (t \in (u, w), \|f (t) + i g (t)\|, 0))$
84	77 83	bitrd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (0_{𝑝} \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \leftrightarrow \forall t \in ℝ 0 \leq if (t \in (u, w), \|f (t) + i g (t)\|, 0))$
85	69 84	mpbird	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to 0_{𝑝} \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))$
86		itg2itg1	$⊢ ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \in dom \int^{1} \land 0_{𝑝} \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) = \int^{1} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))$
87		itg1cl	$⊢ (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \in dom \int^{1} \to \int^{1} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \in ℝ$
88	87	adantr	$⊢ ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \in dom \int^{1} \land 0_{𝑝} \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \to \int^{1} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \in ℝ$
89	86 88	eqeltrd	$⊢ ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \in dom \int^{1} \land 0_{𝑝} \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \in ℝ$
90	55 85 89	syl2anc	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \in ℝ$
91	90	ad6antlr	$⊢ ((((((φ \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))) \in ℝ$
92		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}))$
93	2	rexrd	$⊢ φ \to A \in ℝ^{*}$
94	3	rexrd	$⊢ φ \to B \in ℝ^{*}$
95	93 94	jca	$⊢ φ \to (A \in ℝ^{} \land B \in ℝ^{})$
96		df-icc	$⊢ [.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{t \in ℝ^{*} \| (x \leq t \land t \leq y)\})$
97	96	elixx3g	$⊢ u \in [A, B] \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land u \in ℝ^{*}) \land (A \leq u \land u \leq B))$
98	97	simprbi	$⊢ u \in [A, B] \to (A \leq u \land u \leq B)$
99	98	simpld	$⊢ u \in [A, B] \to A \leq u$
100	96	elixx3g	$⊢ w \in [A, B] \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land w \in ℝ^{*}) \land (A \leq w \land w \leq B))$
101	100	simprbi	$⊢ w \in [A, B] \to (A \leq w \land w \leq B)$
102	101	simprd	$⊢ w \in [A, B] \to w \leq B$
103	99 102	anim12i	$⊢ (u \in [A, B] \land w \in [A, B]) \to (A \leq u \land w \leq B)$
104		ioossioo	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A \leq u \land w \leq B)) \to (u, w) \subseteq (A, B)$
105	95 103 104	syl2an	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (u, w) \subseteq (A, B)$
106	5	adantr	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (A, B) \subseteq D$
107	105 106	sstrd	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (u, w) \subseteq D$
108	107	3adantr3	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to (u, w) \subseteq D$
109	108	sselda	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land t \in (u, w)) \to t \in D$
110	8	ffvelcdmda	$⊢ (φ \land t \in D) \to F (t) \in ℂ$
111	110	adantlr	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land t \in D) \to F (t) \in ℂ$
112	109 111	syldan	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land t \in (u, w)) \to F (t) \in ℂ$
113	112	adantllr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land t \in (u, w)) \to F (t) \in ℂ$
114	63	adantll	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in ℝ) \to f (t) + i g (t) \in ℂ$
115	58 114	sylan2	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in (u, w)) \to f (t) + i g (t) \in ℂ$
116	115	adantlr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land t \in (u, w)) \to f (t) + i g (t) \in ℂ$
117	113 116	subcld	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land t \in (u, w)) \to F (t) - (f (t) + i g (t)) \in ℂ$
118	117	abscld	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land t \in (u, w)) \to \|F (t) - (f (t) + i g (t))\| \in ℝ$
119	118	rexrd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land t \in (u, w)) \to \|F (t) - (f (t) + i g (t))\| \in ℝ^{*}$
120	117	absge0d	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land t \in (u, w)) \to 0 \leq \|F (t) - (f (t) + i g (t))\|$
121		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))\|)$
122	119 120 121	sylanbrc	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land t \in (u, w)) \to \|F (t) - (f (t) + i g (t))\| \in [0, +∞]$
123		0e0iccpnf	$⊢ 0 \in [0, +∞]$
124	123	a1i	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land \neg t \in (u, w)) \to 0 \in [0, +∞]$
125	122 124	ifclda	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \in [0, +∞]$
126	125	adantr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land t \in ℝ) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \in [0, +∞]$
127	126	fmpttd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) : ℝ ⟶ [0, +∞]$
128	92 127	sylan	$⊢ (((((φ \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 (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) : ℝ ⟶ [0, +∞]$
129		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
130	129	rehalfcld	$⊢ y \in ℝ^{+} \to \frac{y}{2} \in ℝ$
131	130	ad2antlr	$⊢ (((((φ \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 \frac{y}{2} \in ℝ$
132		simpll	$⊢ (((φ \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 y \in ℝ^{+}) \to (φ \land (f \in dom \int^{1} \land g \in dom \int^{1}))$
133	107	sselda	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to t \in D$
134	133	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$
135	110	adantlr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to F (t) \in ℂ$
136	6	sselda	$⊢ (φ \land t \in D) \to t \in ℝ$
137	136	adantlr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to t \in ℝ$
138	137 114	syldan	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to f (t) + i g (t) \in ℂ$
139	135 138	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 ℂ$
140	139	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 ℝ$
141	140	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 ℝ^{*}$
142	141	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))\| \in ℝ^{*}$
143	134 142	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))\| \in ℝ^{*}$
144	139	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))\|$
145	144	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 0 \leq \|F (t) - (f (t) + i g (t))\|$
146	134 145	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 0 \leq \|F (t) - (f (t) + i g (t))\|$
147	143 146 121	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, +∞]$
148	123	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, +∞]$
149	147 148	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, +∞]$
150	149	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, +∞]$
151	150	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, +∞]$
152		itg2cl	$⊢ (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) : ℝ ⟶ [0, +∞] \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) \in ℝ^{*}$
153	151 152	syl	$⊢ ((φ \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 ℝ^{*}$
154	132 153	sylan	$⊢ ((((φ \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 y \in ℝ^{+}) \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 ℝ^{*}$
155		rphalfcl	$⊢ y \in ℝ^{+} \to \frac{y}{2} \in ℝ^{+}$
156	155	rpxrd	$⊢ y \in ℝ^{+} \to \frac{y}{2} \in ℝ^{*}$
157	156	ad2antlr	$⊢ ((((φ \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 y \in ℝ^{+}) \land (u \in [A, B] \land w \in [A, B])) \to \frac{y}{2} \in ℝ^{*}$
158		0cnd	$⊢ (φ \land \neg t \in D) \to 0 \in ℂ$
159	110 158	ifclda	$⊢ φ \to if (t \in D, F (t), 0) \in ℂ$
160		subcl	$⊢ (if (t \in D, F (t), 0) \in ℂ \land f (t) + i g (t) \in ℂ) \to if (t \in D, F (t), 0) - (f (t) + i g (t)) \in ℂ$
161	159 63 160	syl2an	$⊢ (φ \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)) \in ℂ$
162	161	anassrs	$⊢ ((φ \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)) \in ℂ$
163	162	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 g (t))\| \in ℝ$
164	163	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 g (t))\| \in ℝ^{*}$
165	162	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 g (t))\|$
166		elxrge0	$⊢ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\| \in [0, +∞] \leftrightarrow (\|if (t \in D, F (t), 0) - (f (t) + i g (t))\| \in ℝ^{*} \land 0 \leq \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)$
167	164 165 166	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 g (t))\| \in [0, +∞]$
168	167	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 g (t))\|) : ℝ ⟶ [0, +∞]$
169		itg2cl	$⊢ (t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|) : ℝ ⟶ [0, +∞] \to \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) \in ℝ^{*}$
170	168 169	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 g (t))\|)) \in ℝ^{*}$
171	170	ad3antrrr	$⊢ ((((φ \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 y \in ℝ^{+}) \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) \in ℝ^{*}$
172	168	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), 0) - (f (t) + i g (t))\|) : ℝ ⟶ [0, +∞]$
173		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), 0) - (f (t) + i g (t))\| \leftrightarrow if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \leq \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)$
174		breq1	$⊢ 0 = if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \to (0 \leq \|if (t \in D, F (t), 0) - (f (t) + i g (t))\| \leftrightarrow if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \leq \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)$
175	140	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))\|$
176		iftrue	$⊢ t \in D \to if (t \in D, F (t), 0) = F (t)$
177	176	fvoveq1d	$⊢ t \in D \to \|if (t \in D, F (t), 0) - (f (t) + i g (t))\| = \|F (t) - (f (t) + i g (t))\|$
178	177	adantl	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in D) \to \|if (t \in D, F (t), 0) - (f (t) + i g (t))\| = \|F (t) - (f (t) + i g (t))\|$
179	175 178	breqtrrd	$⊢ ((φ \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 \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|$
180	179	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 \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|$
181	134 180	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), 0) - (f (t) + i g (t))\|$
182	181	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 ℝ) \land t \in (u, w)) \to \|F (t) - (f (t) + i g (t))\| \leq \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|$
183	165	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 ℝ) \to 0 \leq \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|$
184	183	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 ℝ) \land \neg t \in (u, w)) \to 0 \leq \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|$
185	173 174 182 184	ifbothda	$⊢ (((φ \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) \leq \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|$
186	185	ralrimiva	$⊢ ((φ \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), 0) - (f (t) + i g (t))\|$
187	21	a1i	$⊢ φ \to ℝ \in V$
188		fvex	$⊢ \|F (t) - (f (t) + i g (t))\| \in V$
189	188 72	ifex	$⊢ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \in V$
190	189	a1i	$⊢ (φ \land t \in ℝ) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \in V$
191		fvexd	$⊢ (φ \land t \in ℝ) \to \|if (t \in D, F (t), 0) - (f (t) + i g (t))\| \in V$
192		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))$
193		eqidd	$⊢ φ \to (t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|) = (t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)$
194	187 190 191 192 193	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), 0) - (f (t) + i g (t))\|) \leftrightarrow \forall t \in ℝ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \leq \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)$
195	194	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), 0) - (f (t) + i g (t))\|) \leftrightarrow \forall t \in ℝ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0) \leq \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)$
196	186 195	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), 0) - (f (t) + i g (t))\|)$
197		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), 0) - (f (t) + i g (t))\|) : ℝ ⟶ [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), 0) - (f (t) + i g (t))\|)) \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), 0) - (f (t) + i g (t))\|))$
198	151 172 196 197	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), 0) - (f (t) + i g (t))\|))$
199	132 198	sylan	$⊢ ((((φ \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 y \in ℝ^{+}) \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), 0) - (f (t) + i g (t))\|))$
200		simpllr	$⊢ ((((φ \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 y \in ℝ^{+}) \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2}$
201	154 171 157 199 200	xrlelttrd	$⊢ ((((φ \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 y \in ℝ^{+}) \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))) < \frac{y}{2}$
202	154 157 201	xrltled	$⊢ ((((φ \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 y \in ℝ^{+}) \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 \frac{y}{2}$
203	202	adantllr	$⊢ (((((φ \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])) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) \leq \frac{y}{2}$
204	203	3adantr3	$⊢ (((((φ \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) - (f (t) + i g (t))\|, 0))) \leq \frac{y}{2}$
205		itg2lecl	$⊢ ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0)) : ℝ ⟶ [0, +∞] \land \frac{y}{2} \in ℝ \land \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) \leq \frac{y}{2}) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) \in ℝ$
206	128 131 204 205	syl3anc	$⊢ (((((φ \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) - (f (t) + i g (t))\|, 0))) \in ℝ$
207	206	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) - (f (t) + i g (t))\|, 0))) \in ℝ$
208	130	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} \in ℝ$
209	90	adantr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land \exists r \in (ran f \cup ran g) r \neq 0) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \in ℝ$
210		2rp	$⊢ 2 \in ℝ^{+}$
211		imassrn	$⊢ abs [ran f \cup ran g] \subseteq ran abs$
212		frn	$⊢ abs : ℂ ⟶ ℝ \to ran abs \subseteq ℝ$
213	35 212	ax-mp	$⊢ ran abs \subseteq ℝ$
214	211 213	sstri	$⊢ abs [ran f \cup ran g] \subseteq ℝ$
215	214	a1i	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs [ran f \cup ran g] \subseteq ℝ$
216	9	frnd	$⊢ f \in dom \int^{1} \to ran f \subseteq ℝ$
217	216	adantr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ran f \subseteq ℝ$
218	13	frnd	$⊢ g \in dom \int^{1} \to ran g \subseteq ℝ$
219	218	adantl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ran g \subseteq ℝ$
220	217 219	unssd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ran f \cup ran g \subseteq ℝ$
221	220 70	sstrdi	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ran f \cup ran g \subseteq ℂ$
222		i1f0rn	$⊢ f \in dom \int^{1} \to 0 \in ran f$
223		elun1	$⊢ 0 \in ran f \to 0 \in (ran f \cup ran g)$
224	222 223	syl	$⊢ f \in dom \int^{1} \to 0 \in (ran f \cup ran g)$
225	224	adantr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to 0 \in (ran f \cup ran g)$
226		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
227	35 226	ax-mp	$⊢ abs Fn ℂ$
228		fnfvima	$⊢ (abs Fn ℂ \land ran f \cup ran g \subseteq ℂ \land 0 \in (ran f \cup ran g)) \to \|0\| \in abs [ran f \cup ran g]$
229	227 228	mp3an1	$⊢ (ran f \cup ran g \subseteq ℂ \land 0 \in (ran f \cup ran g)) \to \|0\| \in abs [ran f \cup ran g]$
230	221 225 229	syl2anc	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to \|0\| \in abs [ran f \cup ran g]$
231	230	ne0d	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs [ran f \cup ran g] \neq \emptyset$
232		ffun	$⊢ abs : ℂ ⟶ ℝ \to Fun abs$
233	35 232	ax-mp	$⊢ Fun abs$
234		i1frn	$⊢ f \in dom \int^{1} \to ran f \in Fin$
235		i1frn	$⊢ g \in dom \int^{1} \to ran g \in Fin$
236		unfi	$⊢ (ran f \in Fin \land ran g \in Fin) \to ran f \cup ran g \in Fin$
237	234 235 236	syl2an	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ran f \cup ran g \in Fin$
238		imafi	$⊢ (Fun abs \land ran f \cup ran g \in Fin) \to abs [ran f \cup ran g] \in Fin$
239	233 237 238	sylancr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs [ran f \cup ran g] \in Fin$
240		fimaxre2	$⊢ (abs [ran f \cup ran g] \subseteq ℝ \land abs [ran f \cup ran g] \in Fin) \to \exists x \in ℝ \forall y \in abs [ran f \cup ran g] y \leq x$
241	214 239 240	sylancr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to \exists x \in ℝ \forall y \in abs [ran f \cup ran g] y \leq x$
242		suprcl	$⊢ (abs [ran f \cup ran g] \subseteq ℝ \land abs [ran f \cup ran g] \neq \emptyset \land \exists x \in ℝ \forall y \in abs [ran f \cup ran g] y \leq x) \to sup (abs [ran f \cup ran g] ℝ <) \in ℝ$
243	215 231 241 242	syl3anc	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to sup (abs [ran f \cup ran g] ℝ <) \in ℝ$
244	243	adantr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land (r \in (ran f \cup ran g) \land r \neq 0)) \to sup (abs [ran f \cup ran g] ℝ <) \in ℝ$
245		0red	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land (r \in (ran f \cup ran g) \land r \neq 0)) \to 0 \in ℝ$
246	221	sselda	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land r \in (ran f \cup ran g)) \to r \in ℂ$
247	246	abscld	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land r \in (ran f \cup ran g)) \to \|r\| \in ℝ$
248	247	adantrr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land (r \in (ran f \cup ran g) \land r \neq 0)) \to \|r\| \in ℝ$
249		absgt0	$⊢ r \in ℂ \to (r \neq 0 \leftrightarrow 0 < \|r\|)$
250	246 249	syl	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land r \in (ran f \cup ran g)) \to (r \neq 0 \leftrightarrow 0 < \|r\|)$
251	250	biimpa	$⊢ (((f \in dom \int^{1} \land g \in dom \int^{1}) \land r \in (ran f \cup ran g)) \land r \neq 0) \to 0 < \|r\|$
252	251	anasss	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land (r \in (ran f \cup ran g) \land r \neq 0)) \to 0 < \|r\|$
253	215 231 241	3jca	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (abs [ran f \cup ran g] \subseteq ℝ \land abs [ran f \cup ran g] \neq \emptyset \land \exists x \in ℝ \forall y \in abs [ran f \cup ran g] y \leq x)$
254	253	adantr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land r \in (ran f \cup ran g)) \to (abs [ran f \cup ran g] \subseteq ℝ \land abs [ran f \cup ran g] \neq \emptyset \land \exists x \in ℝ \forall y \in abs [ran f \cup ran g] y \leq x)$
255		fnfvima	$⊢ (abs Fn ℂ \land ran f \cup ran g \subseteq ℂ \land r \in (ran f \cup ran g)) \to \|r\| \in abs [ran f \cup ran g]$
256	227 255	mp3an1	$⊢ (ran f \cup ran g \subseteq ℂ \land r \in (ran f \cup ran g)) \to \|r\| \in abs [ran f \cup ran g]$
257	221 256	sylan	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land r \in (ran f \cup ran g)) \to \|r\| \in abs [ran f \cup ran g]$
258		suprub	$⊢ ((abs [ran f \cup ran g] \subseteq ℝ \land abs [ran f \cup ran g] \neq \emptyset \land \exists x \in ℝ \forall y \in abs [ran f \cup ran g] y \leq x) \land \|r\| \in abs [ran f \cup ran g]) \to \|r\| \leq sup (abs [ran f \cup ran g] ℝ <)$
259	254 257 258	syl2anc	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land r \in (ran f \cup ran g)) \to \|r\| \leq sup (abs [ran f \cup ran g] ℝ <)$
260	259	adantrr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land (r \in (ran f \cup ran g) \land r \neq 0)) \to \|r\| \leq sup (abs [ran f \cup ran g] ℝ <)$
261	245 248 244 252 260	ltletrd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land (r \in (ran f \cup ran g) \land r \neq 0)) \to 0 < sup (abs [ran f \cup ran g] ℝ <)$
262	244 261	elrpd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land (r \in (ran f \cup ran g) \land r \neq 0)) \to sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{+}$
263	262	rexlimdvaa	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (\exists r \in (ran f \cup ran g) r \neq 0 \to sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{+})$
264	263	imp	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land \exists r \in (ran f \cup ran g) r \neq 0) \to sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{+}$
265		rpmulcl	$⊢ (2 \in ℝ^{+} \land sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{+}) \to 2 sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{+}$
266	210 264 265	sylancr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land \exists r \in (ran f \cup ran g) r \neq 0) \to 2 sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{+}$
267	209 266	rerpdivcld	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land \exists r \in (ran f \cup ran g) r \neq 0) \to \frac{\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))}{2 sup (abs [ran f \cup ran g] ℝ <)} \in ℝ$
268	267	adantll	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \exists r \in (ran f \cup ran g) r \neq 0) \to \frac{\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))}{2 sup (abs [ran f \cup ran g] ℝ <)} \in ℝ$
269	268	adantlr	$⊢ (((φ \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) \to \frac{\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))}{2 sup (abs [ran f \cup ran g] ℝ <)} \in ℝ$
270	269	ad3antrrr	$⊢ ((((((φ \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{\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))}{2 sup (abs [ran f \cup ran g] ℝ <)} \in ℝ$
271		simp-4l	$⊢ ((((φ \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 φ$
272		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
273	2 3 272	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
274	273 70	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
275	274	sselda	$⊢ (φ \land w \in [A, B]) \to w \in ℂ$
276	274	sselda	$⊢ (φ \land u \in [A, B]) \to u \in ℂ$
277		subcl	$⊢ (w \in ℂ \land u \in ℂ) \to w - u \in ℂ$
278	275 276 277	syl2anr	$⊢ ((φ \land u \in [A, B]) \land (φ \land w \in [A, B])) \to w - u \in ℂ$
279	278	anandis	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to w - u \in ℂ$
280	279	abscld	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \|w - u\| \in ℝ$
281	280	3adantr3	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to \|w - u\| \in ℝ$
282	271 281	sylan	$⊢ (((((φ \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 \|w - u\| \in ℝ$
283	282	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 \|w - u\| \in ℝ$
284		rpdivcl	$⊢ (\frac{y}{2} \in ℝ^{+} \land 2 sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{+}) \to \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \in ℝ^{+}$
285	155 266 284	syl2anr	$⊢ (((f \in dom \int^{1} \land g \in dom \int^{1}) \land \exists r \in (ran f \cup ran g) r \neq 0) \land y \in ℝ^{+}) \to \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \in ℝ^{+}$
286	285	rpred	$⊢ (((f \in dom \int^{1} \land g \in dom \int^{1}) \land \exists r \in (ran f \cup ran g) r \neq 0) \land y \in ℝ^{+}) \to \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \in ℝ$
287	286	adantlll	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \exists r \in (ran f \cup ran g) r \neq 0) \land y \in ℝ^{+}) \to \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \in ℝ$
288	287	adantllr	$⊢ ((((φ \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 \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \in ℝ$
289	288	ad2antrr	$⊢ ((((((φ \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{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \in ℝ$
290	273	sseld	$⊢ φ \to (u \in [A, B] \to u \in ℝ)$
291	273	sseld	$⊢ φ \to (w \in [A, B] \to w \in ℝ)$
292		idd	$⊢ φ \to (u \leq w \to u \leq w)$
293	290 291 292	3anim123d	$⊢ φ \to ((u \in [A, B] \land w \in [A, B] \land u \leq w) \to (u \in ℝ \land w \in ℝ \land u \leq w))$
294	293	ad2antrr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \exists r \in (ran f \cup ran g) r \neq 0) \to ((u \in [A, B] \land w \in [A, B] \land u \leq w) \to (u \in ℝ \land w \in ℝ \land u \leq w))$
295	294	imp	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \exists r \in (ran f \cup ran g) r \neq 0) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to (u \in ℝ \land w \in ℝ \land u \leq w)$
296	63	abscld	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t) + i g (t)\| \in ℝ$
297	296	rexrd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t) + i g (t)\| \in ℝ^{*}$
298		elxrge0	$⊢ \|f (t) + i g (t)\| \in [0, +∞] \leftrightarrow (\|f (t) + i g (t)\| \in ℝ^{*} \land 0 \leq \|f (t) + i g (t)\|)$
299	297 64 298	sylanbrc	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t) + i g (t)\| \in [0, +∞]$
300		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, +∞]$
301	299 123 300	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, +∞]$
302	301	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, +∞]$
303	243	recnd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to sup (abs [ran f \cup ran g] ℝ <) \in ℂ$
304	303	2timesd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to 2 sup (abs [ran f \cup ran g] ℝ <) = sup (abs [ran f \cup ran g] ℝ <) + sup (abs [ran f \cup ran g] ℝ <)$
305	243 243	readdcld	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to sup (abs [ran f \cup ran g] ℝ <) + sup (abs [ran f \cup ran g] ℝ <) \in ℝ$
306	305	rexrd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to sup (abs [ran f \cup ran g] ℝ <) + sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{*}$
307		abs0	$⊢ \|0\| = 0$
308	307 230	eqeltrrid	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to 0 \in abs [ran f \cup ran g]$
309		suprub	$⊢ ((abs [ran f \cup ran g] \subseteq ℝ \land abs [ran f \cup ran g] \neq \emptyset \land \exists x \in ℝ \forall y \in abs [ran f \cup ran g] y \leq x) \land 0 \in abs [ran f \cup ran g]) \to 0 \leq sup (abs [ran f \cup ran g] ℝ <)$
310	253 308 309	syl2anc	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to 0 \leq sup (abs [ran f \cup ran g] ℝ <)$
311	243 243 310 310	addge0d	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to 0 \leq sup (abs [ran f \cup ran g] ℝ <) + sup (abs [ran f \cup ran g] ℝ <)$
312		elxrge0	$⊢ sup (abs [ran f \cup ran g] ℝ <) + sup (abs [ran f \cup ran g] ℝ <) \in [0, +∞] \leftrightarrow (sup (abs [ran f \cup ran g] ℝ <) + sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{*} \land 0 \leq sup (abs [ran f \cup ran g] ℝ <) + sup (abs [ran f \cup ran g] ℝ <))$
313	306 311 312	sylanbrc	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to sup (abs [ran f \cup ran g] ℝ <) + sup (abs [ran f \cup ran g] ℝ <) \in [0, +∞]$
314	304 313	eqeltrd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to 2 sup (abs [ran f \cup ran g] ℝ <) \in [0, +∞]$
315		ifcl	$⊢ (2 sup (abs [ran f \cup ran g] ℝ <) \in [0, +∞] \land 0 \in [0, +∞]) \to if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0) \in [0, +∞]$
316	314 123 315	sylancl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0) \in [0, +∞]$
317	316	adantr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0) \in [0, +∞]$
318	317	fmpttd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in ℝ ⟼ if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0)) : ℝ ⟶ [0, +∞]$
319	9	ffvelcdmda	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to f (t) \in ℝ$
320	319	recnd	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to f (t) \in ℂ$
321	320	abscld	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to \|f (t)\| \in ℝ$
322	13	ffvelcdmda	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) \in ℝ$
323	322	recnd	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) \in ℂ$
324	323	abscld	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to \|g (t)\| \in ℝ$
325		readdcl	$⊢ (\|f (t)\| \in ℝ \land \|g (t)\| \in ℝ) \to \|f (t)\| + \|g (t)\| \in ℝ$
326	321 324 325	syl2an	$⊢ ((f \in dom \int^{1} \land t \in ℝ) \land (g \in dom \int^{1} \land t \in ℝ)) \to \|f (t)\| + \|g (t)\| \in ℝ$
327	326	anandirs	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t)\| + \|g (t)\| \in ℝ$
328	305	adantr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to sup (abs [ran f \cup ran g] ℝ <) + sup (abs [ran f \cup ran g] ℝ <) \in ℝ$
329		mulcl	$⊢ (i \in ℂ \land g (t) \in ℂ) \to i g (t) \in ℂ$
330	12 323 329	sylancr	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to i g (t) \in ℂ$
331		abstri	$⊢ (f (t) \in ℂ \land i g (t) \in ℂ) \to \|f (t) + i g (t)\| \leq \|f (t)\| + \|i g (t)\|$
332	320 330 331	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)\|$
333	332	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)\|$
334		absmul	$⊢ (i \in ℂ \land g (t) \in ℂ) \to \|i g (t)\| = \|i\| \|g (t)\|$
335	12 323 334	sylancr	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to \|i g (t)\| = \|i\| \|g (t)\|$
336		absi	$⊢ \|i\| = 1$
337	336	oveq1i	$⊢ \|i\| \|g (t)\| = 1 \|g (t)\|$
338	335 337	eqtrdi	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to \|i g (t)\| = 1 \|g (t)\|$
339	324	recnd	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to \|g (t)\| \in ℂ$
340	339	mullidd	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to 1 \|g (t)\| = \|g (t)\|$
341	338 340	eqtrd	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to \|i g (t)\| = \|g (t)\|$
342	341	adantll	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|i g (t)\| = \|g (t)\|$
343	342	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)\|$
344	333 343	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)\|$
345	321	adantlr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t)\| \in ℝ$
346	324	adantll	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|g (t)\| \in ℝ$
347	243	adantr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to sup (abs [ran f \cup ran g] ℝ <) \in ℝ$
348	253	adantr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to (abs [ran f \cup ran g] \subseteq ℝ \land abs [ran f \cup ran g] \neq \emptyset \land \exists x \in ℝ \forall y \in abs [ran f \cup ran g] y \leq x)$
349	221	adantr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to ran f \cup ran g \subseteq ℂ$
350	9	ffnd	$⊢ f \in dom \int^{1} \to f Fn ℝ$
351		fnfvelrn	$⊢ (f Fn ℝ \land t \in ℝ) \to f (t) \in ran f$
352	350 351	sylan	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to f (t) \in ran f$
353		elun1	$⊢ f (t) \in ran f \to f (t) \in (ran f \cup ran g)$
354	352 353	syl	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to f (t) \in (ran f \cup ran g)$
355	354	adantlr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to f (t) \in (ran f \cup ran g)$
356		fnfvima	$⊢ (abs Fn ℂ \land ran f \cup ran g \subseteq ℂ \land f (t) \in (ran f \cup ran g)) \to \|f (t)\| \in abs [ran f \cup ran g]$
357	227 356	mp3an1	$⊢ (ran f \cup ran g \subseteq ℂ \land f (t) \in (ran f \cup ran g)) \to \|f (t)\| \in abs [ran f \cup ran g]$
358	349 355 357	syl2anc	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t)\| \in abs [ran f \cup ran g]$
359		suprub	$⊢ ((abs [ran f \cup ran g] \subseteq ℝ \land abs [ran f \cup ran g] \neq \emptyset \land \exists x \in ℝ \forall y \in abs [ran f \cup ran g] y \leq x) \land \|f (t)\| \in abs [ran f \cup ran g]) \to \|f (t)\| \leq sup (abs [ran f \cup ran g] ℝ <)$
360	348 358 359	syl2anc	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t)\| \leq sup (abs [ran f \cup ran g] ℝ <)$
361	13	ffnd	$⊢ g \in dom \int^{1} \to g Fn ℝ$
362		fnfvelrn	$⊢ (g Fn ℝ \land t \in ℝ) \to g (t) \in ran g$
363	361 362	sylan	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) \in ran g$
364		elun2	$⊢ g (t) \in ran g \to g (t) \in (ran f \cup ran g)$
365	363 364	syl	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) \in (ran f \cup ran g)$
366	365	adantll	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to g (t) \in (ran f \cup ran g)$
367		fnfvima	$⊢ (abs Fn ℂ \land ran f \cup ran g \subseteq ℂ \land g (t) \in (ran f \cup ran g)) \to \|g (t)\| \in abs [ran f \cup ran g]$
368	227 367	mp3an1	$⊢ (ran f \cup ran g \subseteq ℂ \land g (t) \in (ran f \cup ran g)) \to \|g (t)\| \in abs [ran f \cup ran g]$
369	349 366 368	syl2anc	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|g (t)\| \in abs [ran f \cup ran g]$
370		suprub	$⊢ ((abs [ran f \cup ran g] \subseteq ℝ \land abs [ran f \cup ran g] \neq \emptyset \land \exists x \in ℝ \forall y \in abs [ran f \cup ran g] y \leq x) \land \|g (t)\| \in abs [ran f \cup ran g]) \to \|g (t)\| \leq sup (abs [ran f \cup ran g] ℝ <)$
371	348 369 370	syl2anc	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|g (t)\| \leq sup (abs [ran f \cup ran g] ℝ <)$
372	345 346 347 347 360 371	le2addd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t)\| + \|g (t)\| \leq sup (abs [ran f \cup ran g] ℝ <) + sup (abs [ran f \cup ran g] ℝ <)$
373	296 327 328 344 372	letrd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t) + i g (t)\| \leq sup (abs [ran f \cup ran g] ℝ <) + sup (abs [ran f \cup ran g] ℝ <)$
374	304	adantr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to 2 sup (abs [ran f \cup ran g] ℝ <) = sup (abs [ran f \cup ran g] ℝ <) + sup (abs [ran f \cup ran g] ℝ <)$
375	373 374	breqtrrd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to \|f (t) + i g (t)\| \leq 2 sup (abs [ran f \cup ran g] ℝ <)$
376	58 375	sylan2	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in (u, w)) \to \|f (t) + i g (t)\| \leq 2 sup (abs [ran f \cup ran g] ℝ <)$
377		iftrue	$⊢ t \in (u, w) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) = \|f (t) + i g (t)\|$
378	377	adantl	$⊢ ((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) = \|f (t) + i g (t)\|$
379		iftrue	$⊢ t \in (u, w) \to if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0) = 2 sup (abs [ran f \cup ran g] ℝ <)$
380	379	adantl	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in (u, w)) \to if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0) = 2 sup (abs [ran f \cup ran g] ℝ <)$
381	376 378 380	3brtr4d	$⊢ ((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) \leq if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0)$
382	381	ex	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in (u, w) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) \leq if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0))$
383	66	a1i	$⊢ \neg t \in (u, w) \to 0 \leq 0$
384		iffalse	$⊢ \neg t \in (u, w) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) = 0$
385		iffalse	$⊢ \neg t \in (u, w) \to if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0) = 0$
386	383 384 385	3brtr4d	$⊢ \neg t \in (u, w) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) \leq if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0)$
387	382 386	pm2.61d1	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to if (t \in (u, w), \|f (t) + i g (t)\|, 0) \leq if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0)$
388	387	ralrimivw	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to \forall t \in ℝ if (t \in (u, w), \|f (t) + i g (t)\|, 0) \leq if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0)$
389		ovex	$⊢ 2 sup (abs [ran f \cup ran g] ℝ <) \in V$
390	389 72	ifex	$⊢ if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0) \in V$
391	390	a1i	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0) \in V$
392		eqidd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to (t \in ℝ ⟼ if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0)) = (t \in ℝ ⟼ if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0))$
393	22 79 391 82 392	ofrfval2	$⊢ (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)) \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0)) \leftrightarrow \forall t \in ℝ if (t \in (u, w), \|f (t) + i g (t)\|, 0) \leq if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0))$
394	388 393	mpbird	$⊢ (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)) \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0))$
395		itg2le	$⊢ ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞] \land (t \in ℝ ⟼ if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0)) : ℝ ⟶ [0, +∞] \land (t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)) \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 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 (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0)))$
396	302 318 394 395	syl3anc	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0)))$
397	396	adantr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land (u \in ℝ \land w \in ℝ \land u \leq w)) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0)))$
398		mblvol	$⊢ (u, w) \in dom vol \to vol ((u, w)) = {vol}^{*} ((u, w))$
399	42 398	ax-mp	$⊢ vol ((u, w)) = {vol}^{*} ((u, w))$
400		ovolioo	$⊢ (u \in ℝ \land w \in ℝ \land u \leq w) \to {vol}^{*} ((u, w)) = w - u$
401	399 400	eqtrid	$⊢ (u \in ℝ \land w \in ℝ \land u \leq w) \to vol ((u, w)) = w - u$
402		resubcl	$⊢ (w \in ℝ \land u \in ℝ) \to w - u \in ℝ$
403	402	ancoms	$⊢ (u \in ℝ \land w \in ℝ) \to w - u \in ℝ$
404	403	3adant3	$⊢ (u \in ℝ \land w \in ℝ \land u \leq w) \to w - u \in ℝ$
405	401 404	eqeltrd	$⊢ (u \in ℝ \land w \in ℝ \land u \leq w) \to vol ((u, w)) \in ℝ$
406		elrege0	$⊢ sup (abs [ran f \cup ran g] ℝ <) \in [0, +∞) \leftrightarrow (sup (abs [ran f \cup ran g] ℝ <) \in ℝ \land 0 \leq sup (abs [ran f \cup ran g] ℝ <))$
407	243 310 406	sylanbrc	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to sup (abs [ran f \cup ran g] ℝ <) \in [0, +∞)$
408		ge0addcl	$⊢ (sup (abs [ran f \cup ran g] ℝ <) \in [0, +∞) \land sup (abs [ran f \cup ran g] ℝ <) \in [0, +∞)) \to sup (abs [ran f \cup ran g] ℝ <) + sup (abs [ran f \cup ran g] ℝ <) \in [0, +∞)$
409	407 407 408	syl2anc	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to sup (abs [ran f \cup ran g] ℝ <) + sup (abs [ran f \cup ran g] ℝ <) \in [0, +∞)$
410	304 409	eqeltrd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to 2 sup (abs [ran f \cup ran g] ℝ <) \in [0, +∞)$
411		itg2const	$⊢ ((u, w) \in dom vol \land vol ((u, w)) \in ℝ \land 2 sup (abs [ran f \cup ran g] ℝ <) \in [0, +∞)) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0))) = 2 sup (abs [ran f \cup ran g] ℝ <) vol ((u, w))$
412	42 411	mp3an1	$⊢ (vol ((u, w)) \in ℝ \land 2 sup (abs [ran f \cup ran g] ℝ <) \in [0, +∞)) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0))) = 2 sup (abs [ran f \cup ran g] ℝ <) vol ((u, w))$
413	405 410 412	syl2anr	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land (u \in ℝ \land w \in ℝ \land u \leq w)) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), 2 sup (abs [ran f \cup ran g] ℝ <), 0))) = 2 sup (abs [ran f \cup ran g] ℝ <) vol ((u, w))$
414	397 413	breqtrd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land (u \in ℝ \land w \in ℝ \land u \leq w)) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \leq 2 sup (abs [ran f \cup ran g] ℝ <) vol ((u, w))$
415	414	adantll	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in ℝ \land w \in ℝ \land u \leq w)) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \leq 2 sup (abs [ran f \cup ran g] ℝ <) vol ((u, w))$
416	415	adantlr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \exists r \in (ran f \cup ran g) r \neq 0) \land (u \in ℝ \land w \in ℝ \land u \leq w)) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \leq 2 sup (abs [ran f \cup ran g] ℝ <) vol ((u, w))$
417	90	ad3antlr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \exists r \in (ran f \cup ran g) r \neq 0) \land (u \in ℝ \land w \in ℝ \land u \leq w)) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \in ℝ$
418	405	adantl	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \exists r \in (ran f \cup ran g) r \neq 0) \land (u \in ℝ \land w \in ℝ \land u \leq w)) \to vol ((u, w)) \in ℝ$
419	266	adantll	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \exists r \in (ran f \cup ran g) r \neq 0) \to 2 sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{+}$
420	419	adantr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \exists r \in (ran f \cup ran g) r \neq 0) \land (u \in ℝ \land w \in ℝ \land u \leq w)) \to 2 sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{+}$
421	417 418 420	ledivmuld	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \exists r \in (ran f \cup ran g) r \neq 0) \land (u \in ℝ \land w \in ℝ \land u \leq w)) \to (\frac{\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))}{2 sup (abs [ran f \cup ran g] ℝ <)} \leq vol ((u, w)) \leftrightarrow \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \leq 2 sup (abs [ran f \cup ran g] ℝ <) vol ((u, w)))$
422	416 421	mpbird	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \exists r \in (ran f \cup ran g) r \neq 0) \land (u \in ℝ \land w \in ℝ \land u \leq w)) \to \frac{\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))}{2 sup (abs [ran f \cup ran g] ℝ <)} \leq vol ((u, w))$
423		abssubge0	$⊢ (u \in ℝ \land w \in ℝ \land u \leq w) \to \|w - u\| = w - u$
424	400 423	eqtr4d	$⊢ (u \in ℝ \land w \in ℝ \land u \leq w) \to {vol}^{*} ((u, w)) = \|w - u\|$
425	399 424	eqtrid	$⊢ (u \in ℝ \land w \in ℝ \land u \leq w) \to vol ((u, w)) = \|w - u\|$
426	425	adantl	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \exists r \in (ran f \cup ran g) r \neq 0) \land (u \in ℝ \land w \in ℝ \land u \leq w)) \to vol ((u, w)) = \|w - u\|$
427	422 426	breqtrd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \exists r \in (ran f \cup ran g) r \neq 0) \land (u \in ℝ \land w \in ℝ \land u \leq w)) \to \frac{\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))}{2 sup (abs [ran f \cup ran g] ℝ <)} \leq \|w - u\|$
428	295 427	syldan	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \exists r \in (ran f \cup ran g) r \neq 0) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to \frac{\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))}{2 sup (abs [ran f \cup ran g] ℝ <)} \leq \|w - u\|$
429	428	adantllr	$⊢ ((((φ \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 (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to \frac{\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))}{2 sup (abs [ran f \cup ran g] ℝ <)} \leq \|w - u\|$
430	429	adantlr	$⊢ (((((φ \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 \frac{\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))}{2 sup (abs [ran f \cup ran g] ℝ <)} \leq \|w - u\|$
431	430	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 \frac{\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))}{2 sup (abs [ran f \cup ran g] ℝ <)} \leq \|w - u\|$
432		simpr	$⊢ ((((((φ \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 \|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)}$
433	270 283 289 431 432	lelttrd	$⊢ ((((((φ \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{\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))}{2 sup (abs [ran f \cup ran g] ℝ <)} < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)}$
434	90	adantl	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \in ℝ$
435	434	ad3antrrr	$⊢ ((((φ \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 \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) \in ℝ$
436	130	adantl	$⊢ ((((φ \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 \frac{y}{2} \in ℝ$
437	419	adantlr	$⊢ (((φ \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) \to 2 sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{+}$
438	437	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 ℝ^{+}) \to 2 sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{+}$
439	435 436 438	ltdiv1d	$⊢ ((((φ \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 (\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0))) < \frac{y}{2} \leftrightarrow \frac{\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))}{2 sup (abs [ran f \cup ran g] ℝ <)} < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)})$
440	439	ad2antrr	$⊢ ((((((φ \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))) < \frac{y}{2} \leftrightarrow \frac{\int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|f (t) + i g (t)\|, 0)))}{2 sup (abs [ran f \cup ran g] ℝ <)} < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)})$
441	433 440	mpbird	$⊢ ((((((φ \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))) < \frac{y}{2}$
442	201	adantllr	$⊢ (((((φ \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])) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\|, 0))) < \frac{y}{2}$
443	442	3adantr3	$⊢ (((((φ \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) - (f (t) + i g (t))\|, 0))) < \frac{y}{2}$
444	443	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) - (f (t) + i g (t))\|, 0))) < \frac{y}{2}$
445	91 207 208 208 441 444	lt2addd	$⊢ ((((((φ \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})$

Metamath Proof Explorer

Theorem ftc1anclem7

Proof