ftc1anc

Description: ftc1a holds for functions that obey the triangle inequality in the absence of ax-cc . Theorem 565Ma of Fremlin5 p. 220. (Contributed by Brendan Leahy, 11-May-2018)

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

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		ftc1anc.t	$⊢ φ \to \forall s \in (.) [[A, B] \times [A, B]] \|\int_{s} F (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in s, \|F (t)\|, 0)))$
10	1 2 3 4 5 6 7 8	ftc1lem2	$⊢ φ \to G : [A, B] ⟶ ℂ$
11		rphalfcl	$⊢ y \in ℝ^{+} \to \frac{y}{2} \in ℝ^{+}$
12	1 2 3 4 5 6 7 8	ftc1anclem6	$⊢ (φ \land \frac{y}{2} \in ℝ^{+}) \to \exists f \in dom \int^{1} \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2}$
13	11 12	sylan2	$⊢ (φ \land y \in ℝ^{+}) \to \exists f \in dom \int^{1} \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2}$
14	13	adantrl	$⊢ (φ \land (u \in [A, B] \land y \in ℝ^{+})) \to \exists f \in dom \int^{1} \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2}$
15	11	ad2antll	$⊢ (φ \land (u \in [A, B] \land y \in ℝ^{+})) \to \frac{y}{2} \in ℝ^{+}$
16		2rp	$⊢ 2 \in ℝ^{+}$
17		i1ff	$⊢ f \in dom \int^{1} \to f : ℝ ⟶ ℝ$
18	17	frnd	$⊢ f \in dom \int^{1} \to ran f \subseteq ℝ$
19	18	adantr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ran f \subseteq ℝ$
20		i1ff	$⊢ g \in dom \int^{1} \to g : ℝ ⟶ ℝ$
21	20	frnd	$⊢ g \in dom \int^{1} \to ran g \subseteq ℝ$
22	21	adantl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ran g \subseteq ℝ$
23	19 22	unssd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ran f \cup ran g \subseteq ℝ$
24		ax-resscn	$⊢ ℝ \subseteq ℂ$
25	23 24	sstrdi	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ran f \cup ran g \subseteq ℂ$
26		i1f0rn	$⊢ f \in dom \int^{1} \to 0 \in ran f$
27		elun1	$⊢ 0 \in ran f \to 0 \in (ran f \cup ran g)$
28	26 27	syl	$⊢ f \in dom \int^{1} \to 0 \in (ran f \cup ran g)$
29	28	adantr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to 0 \in (ran f \cup ran g)$
30		absf	$⊢ abs : ℂ ⟶ ℝ$
31		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
32	30 31	ax-mp	$⊢ abs Fn ℂ$
33		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]$
34	32 33	mp3an1	$⊢ (ran f \cup ran g \subseteq ℂ \land 0 \in (ran f \cup ran g)) \to \|0\| \in abs [ran f \cup ran g]$
35	25 29 34	syl2anc	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to \|0\| \in abs [ran f \cup ran g]$
36	35	ne0d	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs [ran f \cup ran g] \neq \emptyset$
37		imassrn	$⊢ abs [ran f \cup ran g] \subseteq ran abs$
38		frn	$⊢ abs : ℂ ⟶ ℝ \to ran abs \subseteq ℝ$
39	30 38	ax-mp	$⊢ ran abs \subseteq ℝ$
40	37 39	sstri	$⊢ abs [ran f \cup ran g] \subseteq ℝ$
41		ffun	$⊢ abs : ℂ ⟶ ℝ \to Fun abs$
42	30 41	ax-mp	$⊢ Fun abs$
43		i1frn	$⊢ f \in dom \int^{1} \to ran f \in Fin$
44		i1frn	$⊢ g \in dom \int^{1} \to ran g \in Fin$
45		unfi	$⊢ (ran f \in Fin \land ran g \in Fin) \to ran f \cup ran g \in Fin$
46	43 44 45	syl2an	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to ran f \cup ran g \in Fin$
47		imafi	$⊢ (Fun abs \land ran f \cup ran g \in Fin) \to abs [ran f \cup ran g] \in Fin$
48	42 46 47	sylancr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs [ran f \cup ran g] \in Fin$
49		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$
50	40 48 49	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$
51		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 ℝ$
52	40 51	mp3an1	$⊢ (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 ℝ$
53	36 50 52	syl2anc	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to sup (abs [ran f \cup ran g] ℝ <) \in ℝ$
54	53	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 sup (abs [ran f \cup ran g] ℝ <) \in ℝ$
55		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 ℝ$
56	25	sselda	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land r \in (ran f \cup ran g)) \to r \in ℂ$
57	56	abscld	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land r \in (ran f \cup ran g)) \to \|r\| \in ℝ$
58	57	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 ℝ$
59	53	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 ℝ$
60		absgt0	$⊢ r \in ℂ \to (r \neq 0 \leftrightarrow 0 < \|r\|)$
61	56 60	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\|)$
62	61	biimpd	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land r \in (ran f \cup ran g)) \to (r \neq 0 \to 0 < \|r\|)$
63	62	impr	$⊢ ((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\|$
64	40	a1i	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to abs [ran f \cup ran g] \subseteq ℝ$
65	64 36 50	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)$
66	65	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)$
67		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]$
68	32 67	mp3an1	$⊢ (ran f \cup ran g \subseteq ℂ \land r \in (ran f \cup ran g)) \to \|r\| \in abs [ran f \cup ran g]$
69	25 68	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]$
70		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] ℝ <)$
71	66 69 70	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] ℝ <)$
72	71	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] ℝ <)$
73	55 58 59 63 72	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] ℝ <)$
74	73	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 0 < sup (abs [ran f \cup ran g] ℝ <))$
75	74	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 0 < sup (abs [ran f \cup ran g] ℝ <)$
76	54 75	elrpd	$⊢ ((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 ℝ^{+}$
77		rpmulcl	$⊢ (2 \in ℝ^{+} \land sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{+}) \to 2 sup (abs [ran f \cup ran g] ℝ <) \in ℝ^{+}$
78	16 76 77	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 ℝ^{+}$
79		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 ℝ^{+}$
80	15 78 79	syl2an	$⊢ ((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \in ℝ^{+}$
81	80	anassrs	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \in ℝ^{+}$
82	81	adantlr	$⊢ ((((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \in ℝ^{+}$
83		ancom	$⊢ (u \in [A, B] \land y \in ℝ^{+}) \leftrightarrow (y \in ℝ^{+} \land u \in [A, B])$
84	83	anbi2i	$⊢ ((((φ \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 y \in ℝ^{+})) \leftrightarrow ((((φ \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]))$
85		an32	$⊢ ((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land (f \in dom \int^{1} \land g \in dom \int^{1})) \leftrightarrow ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land y \in ℝ^{+}))$
86	85	anbi1i	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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}) \leftrightarrow (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2})$
87		an32	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2}) \leftrightarrow (((φ \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 (u \in [A, B] \land y \in ℝ^{+}))$
88	86 87	bitri	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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}) \leftrightarrow (((φ \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 (u \in [A, B] \land y \in ℝ^{+}))$
89	88	anbi1i	$⊢ ((((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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) \leftrightarrow ((((φ \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 (u \in [A, B] \land y \in ℝ^{+})) \land \exists r \in (ran f \cup ran g) r \neq 0)$
90		an32	$⊢ ((((φ \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 (u \in [A, B] \land y \in ℝ^{+})) \land \exists r \in (ran f \cup ran g) r \neq 0) \leftrightarrow ((((φ \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 y \in ℝ^{+}))$
91	89 90	bitri	$⊢ ((((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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) \leftrightarrow ((((φ \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 y \in ℝ^{+}))$
92		anass	$⊢ (((((φ \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]) \leftrightarrow ((((φ \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]))$
93	84 91 92	3bitr4i	$⊢ ((((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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) \leftrightarrow (((((φ \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])$
94		oveq12	$⊢ (b = w \land a = u) \to b - a = w - u$
95	94	ancoms	$⊢ (a = u \land b = w) \to b - a = w - u$
96	95	fveq2d	$⊢ (a = u \land b = w) \to \|b - a\| = \|w - u\|$
97	96	breq1d	$⊢ (a = u \land b = w) \to (\|b - a\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \leftrightarrow \|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)})$
98		fveq2	$⊢ b = w \to G (b) = G (w)$
99		fveq2	$⊢ a = u \to G (a) = G (u)$
100	98 99	oveqan12rd	$⊢ (a = u \land b = w) \to G (b) - G (a) = G (w) - G (u)$
101	100	fveq2d	$⊢ (a = u \land b = w) \to \|G (b) - G (a)\| = \|G (w) - G (u)\|$
102	101	breq1d	$⊢ (a = u \land b = w) \to (\|G (b) - G (a)\| < y \leftrightarrow \|G (w) - G (u)\| < y)$
103	97 102	imbi12d	$⊢ (a = u \land b = w) \to ((\|b - a\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to \|G (b) - G (a)\| < y) \leftrightarrow (\|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to \|G (w) - G (u)\| < y))$
104		oveq12	$⊢ (b = u \land a = w) \to b - a = u - w$
105	104	ancoms	$⊢ (a = w \land b = u) \to b - a = u - w$
106	105	fveq2d	$⊢ (a = w \land b = u) \to \|b - a\| = \|u - w\|$
107	106	breq1d	$⊢ (a = w \land b = u) \to (\|b - a\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \leftrightarrow \|u - w\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)})$
108		fveq2	$⊢ b = u \to G (b) = G (u)$
109		fveq2	$⊢ a = w \to G (a) = G (w)$
110	108 109	oveqan12rd	$⊢ (a = w \land b = u) \to G (b) - G (a) = G (u) - G (w)$
111	110	fveq2d	$⊢ (a = w \land b = u) \to \|G (b) - G (a)\| = \|G (u) - G (w)\|$
112	111	breq1d	$⊢ (a = w \land b = u) \to (\|G (b) - G (a)\| < y \leftrightarrow \|G (u) - G (w)\| < y)$
113	107 112	imbi12d	$⊢ (a = w \land b = u) \to ((\|b - a\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to \|G (b) - G (a)\| < y) \leftrightarrow (\|u - w\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to \|G (u) - G (w)\| < y))$
114		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
115	2 3 114	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
116	115	ad4antr	$⊢ ((((φ \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 [A, B] \subseteq ℝ$
117		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 φ$
118	115 24	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
119	118	sselda	$⊢ (φ \land w \in [A, B]) \to w \in ℂ$
120	118	sselda	$⊢ (φ \land u \in [A, B]) \to u \in ℂ$
121		abssub	$⊢ (w \in ℂ \land u \in ℂ) \to \|w - u\| = \|u - w\|$
122	119 120 121	syl2anr	$⊢ ((φ \land u \in [A, B]) \land (φ \land w \in [A, B])) \to \|w - u\| = \|u - w\|$
123	122	anandis	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \|w - u\| = \|u - w\|$
124	123	breq1d	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (\|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \leftrightarrow \|u - w\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)})$
125	10	ffvelcdmda	$⊢ (φ \land w \in [A, B]) \to G (w) \in ℂ$
126	10	ffvelcdmda	$⊢ (φ \land u \in [A, B]) \to G (u) \in ℂ$
127		abssub	$⊢ (G (w) \in ℂ \land G (u) \in ℂ) \to \|G (w) - G (u)\| = \|G (u) - G (w)\|$
128	125 126 127	syl2anr	$⊢ ((φ \land u \in [A, B]) \land (φ \land w \in [A, B])) \to \|G (w) - G (u)\| = \|G (u) - G (w)\|$
129	128	anandis	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \|G (w) - G (u)\| = \|G (u) - G (w)\|$
130	129	breq1d	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (\|G (w) - G (u)\| < y \leftrightarrow \|G (u) - G (w)\| < y)$
131	124 130	imbi12d	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to ((\|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to \|G (w) - G (u)\| < y) \leftrightarrow (\|u - w\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to \|G (u) - G (w)\| < y))$
132	117 131	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])) \to ((\|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to \|G (w) - G (u)\| < y) \leftrightarrow (\|u - w\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to \|G (u) - G (w)\| < y))$
133	2	rexrd	$⊢ φ \to A \in ℝ^{*}$
134	3	rexrd	$⊢ φ \to B \in ℝ^{*}$
135	133 134	jca	$⊢ φ \to (A \in ℝ^{} \land B \in ℝ^{})$
136		df-icc	$⊢ [.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{t \in ℝ^{*} \| (x \leq t \land t \leq y)\})$
137	136	elixx3g	$⊢ u \in [A, B] \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land u \in ℝ^{*}) \land (A \leq u \land u \leq B))$
138	137	simprbi	$⊢ u \in [A, B] \to (A \leq u \land u \leq B)$
139	138	simpld	$⊢ u \in [A, B] \to A \leq u$
140	136	elixx3g	$⊢ w \in [A, B] \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land w \in ℝ^{*}) \land (A \leq w \land w \leq B))$
141	140	simprbi	$⊢ w \in [A, B] \to (A \leq w \land w \leq B)$
142	141	simprd	$⊢ w \in [A, B] \to w \leq B$
143	139 142	anim12i	$⊢ (u \in [A, B] \land w \in [A, B]) \to (A \leq u \land w \leq B)$
144		ioossioo	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A \leq u \land w \leq B)) \to (u, w) \subseteq (A, B)$
145	135 143 144	syl2an	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (u, w) \subseteq (A, B)$
146	5	adantr	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (A, B) \subseteq D$
147	145 146	sstrd	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (u, w) \subseteq D$
148	147	sselda	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to t \in D$
149	8	ffvelcdmda	$⊢ (φ \land t \in D) \to F (t) \in ℂ$
150	149	abscld	$⊢ (φ \land t \in D) \to \|F (t)\| \in ℝ$
151	150	rexrd	$⊢ (φ \land t \in D) \to \|F (t)\| \in ℝ^{*}$
152	149	absge0d	$⊢ (φ \land t \in D) \to 0 \leq \|F (t)\|$
153		elxrge0	$⊢ \|F (t)\| \in [0, +∞] \leftrightarrow (\|F (t)\| \in ℝ^{*} \land 0 \leq \|F (t)\|)$
154	151 152 153	sylanbrc	$⊢ (φ \land t \in D) \to \|F (t)\| \in [0, +∞]$
155	154	adantlr	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land t \in D) \to \|F (t)\| \in [0, +∞]$
156	148 155	syldan	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to \|F (t)\| \in [0, +∞]$
157		0e0iccpnf	$⊢ 0 \in [0, +∞]$
158	157	a1i	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land \neg t \in (u, w)) \to 0 \in [0, +∞]$
159	156 158	ifclda	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to if (t \in (u, w), \|F (t)\|, 0) \in [0, +∞]$
160	159	adantr	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land t \in ℝ) \to if (t \in (u, w), \|F (t)\|, 0) \in [0, +∞]$
161	160	fmpttd	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)) : ℝ ⟶ [0, +∞]$
162		itg2cl	$⊢ (t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)) : ℝ ⟶ [0, +∞] \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))) \in ℝ^{*}$
163	161 162	syl	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))) \in ℝ^{*}$
164	163	3adantr3	$⊢ (φ \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)\|, 0))) \in ℝ^{*}$
165	117 164	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 \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))) \in ℝ^{*}$
166	165	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)\|, 0))) \in ℝ^{*}$
167		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}))$
168	149	adantlr	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land t \in D) \to F (t) \in ℂ$
169	148 168	syldan	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to F (t) \in ℂ$
170	169	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 ℂ$
171		elioore	$⊢ t \in (u, w) \to t \in ℝ$
172	17	ffvelcdmda	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to f (t) \in ℝ$
173	172	recnd	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to f (t) \in ℂ$
174		ax-icn	$⊢ i \in ℂ$
175	20	ffvelcdmda	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) \in ℝ$
176	175	recnd	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) \in ℂ$
177		mulcl	$⊢ (i \in ℂ \land g (t) \in ℂ) \to i g (t) \in ℂ$
178	174 176 177	sylancr	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to i g (t) \in ℂ$
179		addcl	$⊢ (f (t) \in ℂ \land i g (t) \in ℂ) \to f (t) + i g (t) \in ℂ$
180	173 178 179	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 ℂ$
181	180	anandirs	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to f (t) + i g (t) \in ℂ$
182	171 181	sylan2	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in (u, w)) \to f (t) + i g (t) \in ℂ$
183	182	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 ℂ$
184	183	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 ℂ$
185	170 184	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 ℂ$
186	185	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 ℝ$
187	182	abscld	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in (u, w)) \to \|f (t) + i g (t)\| \in ℝ$
188	187	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 ℝ$
189	188	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 ℝ$
190	186 189	readdcld	$⊢ (((φ \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))\| + \|f (t) + i g (t)\| \in ℝ$
191	190	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))\| + \|f (t) + i g (t)\| \in ℝ^{*}$
192	185	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))\|$
193	181	absge0d	$⊢ ((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \to 0 \leq \|f (t) + i g (t)\|$
194	171 193	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)\|$
195	194	adantll	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land t \in (u, w)) \to 0 \leq \|f (t) + i g (t)\|$
196	195	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 0 \leq \|f (t) + i g (t)\|$
197	186 189 192 196	addge0d	$⊢ (((φ \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))\| + \|f (t) + i g (t)\|$
198		elxrge0	$⊢ \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\| \in [0, +∞] \leftrightarrow (\|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\| \in ℝ^{*} \land 0 \leq \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|)$
199	191 197 198	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))\| + \|f (t) + i g (t)\| \in [0, +∞]$
200	157	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, +∞]$
201	199 200	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))\| + \|f (t) + i g (t)\|, 0) \in [0, +∞]$
202	201	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))\| + \|f (t) + i g (t)\|, 0) \in [0, +∞]$
203	202	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))\| + \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞]$
204		itg2cl	$⊢ (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (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))\| + \|f (t) + i g (t)\|, 0))) \in ℝ^{*}$
205	203 204	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))\| + \|f (t) + i g (t)\|, 0))) \in ℝ^{*}$
206	205	3adantr3	$⊢ ((φ \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 \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0))) \in ℝ^{*}$
207	167 206	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 \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0))) \in ℝ^{*}$
208	207	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))\| + \|f (t) + i g (t)\|, 0))) \in ℝ^{*}$
209		rpxr	$⊢ y \in ℝ^{+} \to y \in ℝ^{*}$
210	209	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 y \in ℝ^{*}$
211	159	adantlr	$⊢ ((φ \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)\|, 0) \in [0, +∞]$
212	211	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)\|, 0) \in [0, +∞]$
213	212	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)\|, 0)) : ℝ ⟶ [0, +∞]$
214	170 184	npcand	$⊢ (((φ \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))) + f (t) + i g (t) = F (t)$
215	214	fveq2d	$⊢ (((φ \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))) + f (t) + i g (t)\| = \|F (t)\|$
216	185 184	abstrid	$⊢ (((φ \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))) + f (t) + i g (t)\| \leq \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|$
217	215 216	eqbrtrrd	$⊢ (((φ \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)\| \leq \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|$
218		iftrue	$⊢ t \in (u, w) \to if (t \in (u, w), \|F (t)\|, 0) = \|F (t)\|$
219	218	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 (u, w)) \to if (t \in (u, w), \|F (t)\|, 0) = \|F (t)\|$
220		iftrue	$⊢ t \in (u, w) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0) = \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|$
221	220	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 (u, w)) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0) = \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|$
222	217 219 221	3brtr4d	$⊢ (((φ \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 (u, w), \|F (t)\|, 0) \leq if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)$
223	222	ex	$⊢ ((φ \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 (u, w) \to if (t \in (u, w), \|F (t)\|, 0) \leq if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0))$
224		0le0	$⊢ 0 \leq 0$
225	224	a1i	$⊢ \neg t \in (u, w) \to 0 \leq 0$
226		iffalse	$⊢ \neg t \in (u, w) \to if (t \in (u, w), \|F (t)\|, 0) = 0$
227		iffalse	$⊢ \neg t \in (u, w) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0) = 0$
228	225 226 227	3brtr4d	$⊢ \neg t \in (u, w) \to if (t \in (u, w), \|F (t)\|, 0) \leq if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)$
229	223 228	pm2.61d1	$⊢ ((φ \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)\|, 0) \leq if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)$
230	229	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)\|, 0) \leq if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)$
231		reex	$⊢ ℝ \in V$
232	231	a1i	$⊢ φ \to ℝ \in V$
233		fvex	$⊢ \|F (t)\| \in V$
234		c0ex	$⊢ 0 \in V$
235	233 234	ifex	$⊢ if (t \in (u, w), \|F (t)\|, 0) \in V$
236	235	a1i	$⊢ (φ \land t \in ℝ) \to if (t \in (u, w), \|F (t)\|, 0) \in V$
237		ovex	$⊢ \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\| \in V$
238	237 234	ifex	$⊢ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0) \in V$
239	238	a1i	$⊢ (φ \land t \in ℝ) \to if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0) \in V$
240		eqidd	$⊢ φ \to (t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)) = (t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))$
241		eqidd	$⊢ φ \to (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (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))$
242	232 236 239 240 241	ofrfval2	$⊢ φ \to ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)) \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)) \leftrightarrow \forall t \in ℝ if (t \in (u, w), \|F (t)\|, 0) \leq if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0))$
243	242	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)\|, 0)) \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)) \leftrightarrow \forall t \in ℝ if (t \in (u, w), \|F (t)\|, 0) \leq if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0))$
244	230 243	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)\|, 0)) \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0))$
245		itg2le	$⊢ ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)) : ℝ ⟶ [0, +∞] \land (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)) : ℝ ⟶ [0, +∞] \land (t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)) \leq_{f} (t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0))) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)))$
246	213 203 244 245	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)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)))$
247	246	3adantr3	$⊢ ((φ \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 \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)))$
248	167 247	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 \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)))$
249	248	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)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t) - (f (t) + i g (t))\| + \|f (t) + i g (t)\|, 0)))$
250	1 2 3 4 5 6 7 8	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$
251	166 208 210 249 250	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 \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)\|, 0))) < y$
252		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) \to φ$
253		simpr2	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to w \in [A, B]$
254		oveq2	$⊢ x = w \to (A, x) = (A, w)$
255		itgeq1	$⊢ (A, x) = (A, w) \to \int_{(A, x)} F (t) d t = \int_{(A, w)} F (t) d t$
256	254 255	syl	$⊢ x = w \to \int_{(A, x)} F (t) d t = \int_{(A, w)} F (t) d t$
257		itgex	$⊢ \int_{(A, w)} F (t) d t \in V$
258	256 1 257	fvmpt	$⊢ w \in [A, B] \to G (w) = \int_{(A, w)} F (t) d t$
259	253 258	syl	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to G (w) = \int_{(A, w)} F (t) d t$
260	2	adantr	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to A \in ℝ$
261	115	sselda	$⊢ (φ \land w \in [A, B]) \to w \in ℝ$
262	261	3ad2antr2	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to w \in ℝ$
263	115	sselda	$⊢ (φ \land u \in [A, B]) \to u \in ℝ$
264	263	rexrd	$⊢ (φ \land u \in [A, B]) \to u \in ℝ^{*}$
265	264	3ad2antr1	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to u \in ℝ^{*}$
266		elicc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (u \in [A, B] \leftrightarrow (u \in ℝ^{*} \land A \leq u \land u \leq B))$
267	133 134 266	syl2anc	$⊢ φ \to (u \in [A, B] \leftrightarrow (u \in ℝ^{*} \land A \leq u \land u \leq B))$
268	267	biimpa	$⊢ (φ \land u \in [A, B]) \to (u \in ℝ^{*} \land A \leq u \land u \leq B)$
269	268	simp2d	$⊢ (φ \land u \in [A, B]) \to A \leq u$
270	269	3ad2antr1	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to A \leq u$
271		simpr3	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to u \leq w$
272	133	adantr	$⊢ (φ \land w \in [A, B]) \to A \in ℝ^{*}$
273	261	rexrd	$⊢ (φ \land w \in [A, B]) \to w \in ℝ^{*}$
274		elicc1	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (u \in [A, w] \leftrightarrow (u \in ℝ^{*} \land A \leq u \land u \leq w))$
275	272 273 274	syl2anc	$⊢ (φ \land w \in [A, B]) \to (u \in [A, w] \leftrightarrow (u \in ℝ^{*} \land A \leq u \land u \leq w))$
276	275	3ad2antr2	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to (u \in [A, w] \leftrightarrow (u \in ℝ^{*} \land A \leq u \land u \leq w))$
277	265 270 271 276	mpbir3and	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to u \in [A, w]$
278		iooss2	$⊢ (B \in ℝ^{*} \land w \leq B) \to (A, w) \subseteq (A, B)$
279	134 142 278	syl2an	$⊢ (φ \land w \in [A, B]) \to (A, w) \subseteq (A, B)$
280	5	adantr	$⊢ (φ \land w \in [A, B]) \to (A, B) \subseteq D$
281	279 280	sstrd	$⊢ (φ \land w \in [A, B]) \to (A, w) \subseteq D$
282	281	3ad2antr2	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to (A, w) \subseteq D$
283	282	sselda	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land t \in (A, w)) \to t \in D$
284	149	adantlr	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land t \in D) \to F (t) \in ℂ$
285	283 284	syldan	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \land t \in (A, w)) \to F (t) \in ℂ$
286		eleq1w	$⊢ w = u \to (w \in [A, B] \leftrightarrow u \in [A, B])$
287	286	anbi2d	$⊢ w = u \to ((φ \land w \in [A, B]) \leftrightarrow (φ \land u \in [A, B]))$
288		oveq2	$⊢ w = u \to (A, w) = (A, u)$
289	288	mpteq1d	$⊢ w = u \to (t \in (A, w) ⟼ F (t)) = (t \in (A, u) ⟼ F (t))$
290	289	eleq1d	$⊢ w = u \to ((t \in (A, w) ⟼ F (t)) \in 𝐿^{1} \leftrightarrow (t \in (A, u) ⟼ F (t)) \in 𝐿^{1})$
291	287 290	imbi12d	$⊢ w = u \to (((φ \land w \in [A, B]) \to (t \in (A, w) ⟼ F (t)) \in 𝐿^{1}) \leftrightarrow ((φ \land u \in [A, B]) \to (t \in (A, u) ⟼ F (t)) \in 𝐿^{1}))$
292		ioombl	$⊢ (A, w) \in dom vol$
293	292	a1i	$⊢ (φ \land w \in [A, B]) \to (A, w) \in dom vol$
294	149	adantlr	$⊢ ((φ \land w \in [A, B]) \land t \in D) \to F (t) \in ℂ$
295	8	feqmptd	$⊢ φ \to F = (t \in D ⟼ F (t))$
296	295 7	eqeltrrd	$⊢ φ \to (t \in D ⟼ F (t)) \in 𝐿^{1}$
297	296	adantr	$⊢ (φ \land w \in [A, B]) \to (t \in D ⟼ F (t)) \in 𝐿^{1}$
298	281 293 294 297	iblss	$⊢ (φ \land w \in [A, B]) \to (t \in (A, w) ⟼ F (t)) \in 𝐿^{1}$
299	291 298	chvarvv	$⊢ (φ \land u \in [A, B]) \to (t \in (A, u) ⟼ F (t)) \in 𝐿^{1}$
300	299	3ad2antr1	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to (t \in (A, u) ⟼ F (t)) \in 𝐿^{1}$
301		ioombl	$⊢ (u, w) \in dom vol$
302	301	a1i	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (u, w) \in dom vol$
303		fvexd	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land t \in D) \to F (t) \in V$
304	296	adantr	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (t \in D ⟼ F (t)) \in 𝐿^{1}$
305	147 302 303 304	iblss	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (t \in (u, w) ⟼ F (t)) \in 𝐿^{1}$
306	305	3adantr3	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to (t \in (u, w) ⟼ F (t)) \in 𝐿^{1}$
307	260 262 277 285 300 306	itgsplitioo	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to \int_{(A, w)} F (t) d t = \int_{(A, u)} F (t) d t + \int_{(u, w)} F (t) d t$
308	259 307	eqtrd	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to G (w) = \int_{(A, u)} F (t) d t + \int_{(u, w)} F (t) d t$
309		simpr1	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to u \in [A, B]$
310		oveq2	$⊢ x = u \to (A, x) = (A, u)$
311		itgeq1	$⊢ (A, x) = (A, u) \to \int_{(A, x)} F (t) d t = \int_{(A, u)} F (t) d t$
312	310 311	syl	$⊢ x = u \to \int_{(A, x)} F (t) d t = \int_{(A, u)} F (t) d t$
313		itgex	$⊢ \int_{(A, u)} F (t) d t \in V$
314	312 1 313	fvmpt	$⊢ u \in [A, B] \to G (u) = \int_{(A, u)} F (t) d t$
315	309 314	syl	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to G (u) = \int_{(A, u)} F (t) d t$
316	308 315	oveq12d	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to G (w) - G (u) = \int_{(A, u)} F (t) d t + \int_{(u, w)} F (t) d t - \int_{(A, u)} F (t) d t$
317		fvexd	$⊢ ((φ \land u \in [A, B]) \land t \in (A, u)) \to F (t) \in V$
318	317 299	itgcl	$⊢ (φ \land u \in [A, B]) \to \int_{(A, u)} F (t) d t \in ℂ$
319	318	adantrr	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \int_{(A, u)} F (t) d t \in ℂ$
320		fvexd	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land t \in (u, w)) \to F (t) \in V$
321	320 305	itgcl	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \int_{(u, w)} F (t) d t \in ℂ$
322	319 321	pncan2d	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \int_{(A, u)} F (t) d t + \int_{(u, w)} F (t) d t - \int_{(A, u)} F (t) d t = \int_{(u, w)} F (t) d t$
323	322	3adantr3	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to \int_{(A, u)} F (t) d t + \int_{(u, w)} F (t) d t - \int_{(A, u)} F (t) d t = \int_{(u, w)} F (t) d t$
324	316 323	eqtrd	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to G (w) - G (u) = \int_{(u, w)} F (t) d t$
325	324	fveq2d	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to \|G (w) - G (u)\| = \|\int_{(u, w)} F (t) d t\|$
326		df-ov	$⊢ (u, w) = (.) (⟨u, w⟩)$
327		opelxpi	$⊢ (u \in [A, B] \land w \in [A, B]) \to ⟨u, w⟩ \in ([A, B] \times [A, B])$
328		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
329		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
330	328 329	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
331		iccssxr	$⊢ [A, B] \subseteq ℝ^{*}$
332		xpss12	$⊢ ([A, B] \subseteq ℝ^{} \land [A, B] \subseteq ℝ^{}) \to [A, B] \times [A, B] \subseteq ℝ^{} \times ℝ^{}$
333	331 331 332	mp2an	$⊢ [A, B] \times [A, B] \subseteq ℝ^{} \times ℝ^{}$
334		fnfvima	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land [A, B] \times [A, B] \subseteq ℝ^{} \times ℝ^{} \land ⟨u, w⟩ \in ([A, B] \times [A, B])) \to (.) (⟨u, w⟩) \in (.) [[A, B] \times [A, B]]$
335	330 333 334	mp3an12	$⊢ ⟨u, w⟩ \in ([A, B] \times [A, B]) \to (.) (⟨u, w⟩) \in (.) [[A, B] \times [A, B]]$
336	327 335	syl	$⊢ (u \in [A, B] \land w \in [A, B]) \to (.) (⟨u, w⟩) \in (.) [[A, B] \times [A, B]]$
337	326 336	eqeltrid	$⊢ (u \in [A, B] \land w \in [A, B]) \to (u, w) \in (.) [[A, B] \times [A, B]]$
338		itgeq1	$⊢ s = (u, w) \to \int_{s} F (t) d t = \int_{(u, w)} F (t) d t$
339	338	fveq2d	$⊢ s = (u, w) \to \|\int_{s} F (t) d t\| = \|\int_{(u, w)} F (t) d t\|$
340		eleq2	$⊢ s = (u, w) \to (t \in s \leftrightarrow t \in (u, w))$
341	340	ifbid	$⊢ s = (u, w) \to if (t \in s, \|F (t)\|, 0) = if (t \in (u, w), \|F (t)\|, 0)$
342	341	mpteq2dv	$⊢ s = (u, w) \to (t \in ℝ ⟼ if (t \in s, \|F (t)\|, 0)) = (t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))$
343	342	fveq2d	$⊢ s = (u, w) \to \int^{2} ((t \in ℝ ⟼ if (t \in s, \|F (t)\|, 0))) = \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)))$
344	339 343	breq12d	$⊢ s = (u, w) \to (\|\int_{s} F (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in s, \|F (t)\|, 0))) \leftrightarrow \|\int_{(u, w)} F (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))))$
345	344	rspccva	$⊢ (\forall s \in (.) [[A, B] \times [A, B]] \|\int_{s} F (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in s, \|F (t)\|, 0))) \land (u, w) \in (.) [[A, B] \times [A, B]]) \to \|\int_{(u, w)} F (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)))$
346	9 337 345	syl2an	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \|\int_{(u, w)} F (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)))$
347	346	3adantr3	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to \|\int_{(u, w)} F (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)))$
348	325 347	eqbrtrd	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to \|G (w) - G (u)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)))$
349	348	adantlr	$⊢ ((φ \land y \in ℝ^{+}) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to \|G (w) - G (u)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)))$
350		subcl	$⊢ (G (w) \in ℂ \land G (u) \in ℂ) \to G (w) - G (u) \in ℂ$
351	125 126 350	syl2anr	$⊢ ((φ \land u \in [A, B]) \land (φ \land w \in [A, B])) \to G (w) - G (u) \in ℂ$
352	351	anandis	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to G (w) - G (u) \in ℂ$
353	352	abscld	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \|G (w) - G (u)\| \in ℝ$
354	353	rexrd	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \|G (w) - G (u)\| \in ℝ^{*}$
355	354	3adantr3	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to \|G (w) - G (u)\| \in ℝ^{*}$
356	355	adantlr	$⊢ ((φ \land y \in ℝ^{+}) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to \|G (w) - G (u)\| \in ℝ^{*}$
357	164	adantlr	$⊢ ((φ \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)\|, 0))) \in ℝ^{*}$
358	209	ad2antlr	$⊢ ((φ \land y \in ℝ^{+}) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to y \in ℝ^{*}$
359		xrlelttr	$⊢ (\|G (w) - G (u)\| \in ℝ^{} \land \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))) \in ℝ^{} \land y \in ℝ^{*}) \to ((\|G (w) - G (u)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))) \land \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))) < y) \to \|G (w) - G (u)\| < y)$
360	356 357 358 359	syl3anc	$⊢ ((φ \land y \in ℝ^{+}) \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to ((\|G (w) - G (u)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))) \land \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))) < y) \to \|G (w) - G (u)\| < y)$
361	349 360	mpand	$⊢ ((φ \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)\|, 0))) < y \to \|G (w) - G (u)\| < y)$
362	252 361	sylanl1	$⊢ (((((φ \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)\|, 0))) < y \to \|G (w) - G (u)\| < y)$
363	362	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)\|, 0))) < y \to \|G (w) - G (u)\| < y)$
364	251 363	mpd	$⊢ ((((((φ \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 \|G (w) - G (u)\| < y$
365	364	ex	$⊢ (((((φ \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\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to \|G (w) - G (u)\| < y)$
366	103 113 116 132 365	wlogle	$⊢ (((((φ \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 (\|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to \|G (w) - G (u)\| < y)$
367	366	anassrs	$⊢ ((((((φ \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 (\|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to \|G (w) - G (u)\| < y)$
368	93 367	sylanb	$⊢ (((((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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 w \in [A, B]) \to (\|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to \|G (w) - G (u)\| < y)$
369	368	ralrimiva	$⊢ ((((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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 \forall w \in [A, B] (\|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to \|G (w) - G (u)\| < y)$
370		breq2	$⊢ z = \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to (\|w - u\| < z \leftrightarrow \|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)})$
371	370	rspceaimv	$⊢ (\frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \in ℝ^{+} \land \forall w \in [A, B] (\|w - u\| < \frac{\frac{y}{2}}{2 sup (abs [ran f \cup ran g] ℝ <)} \to \|G (w) - G (u)\| < y)) \to \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)$
372	82 369 371	syl2anc	$⊢ ((((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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 \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)$
373		ralnex	$⊢ \forall r \in (ran f \cup ran g) \neg r \neq 0 \leftrightarrow \neg \exists r \in (ran f \cup ran g) r \neq 0$
374		nne	$⊢ \neg r \neq 0 \leftrightarrow r = 0$
375	374	ralbii	$⊢ \forall r \in (ran f \cup ran g) \neg r \neq 0 \leftrightarrow \forall r \in (ran f \cup ran g) r = 0$
376	373 375	bitr3i	$⊢ \neg \exists r \in (ran f \cup ran g) r \neq 0 \leftrightarrow \forall r \in (ran f \cup ran g) r = 0$
377	17	ffnd	$⊢ f \in dom \int^{1} \to f Fn ℝ$
378		fnfvelrn	$⊢ (f Fn ℝ \land t \in ℝ) \to f (t) \in ran f$
379	377 378	sylan	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to f (t) \in ran f$
380		elun1	$⊢ f (t) \in ran f \to f (t) \in (ran f \cup ran g)$
381	379 380	syl	$⊢ (f \in dom \int^{1} \land t \in ℝ) \to f (t) \in (ran f \cup ran g)$
382		eqeq1	$⊢ r = f (t) \to (r = 0 \leftrightarrow f (t) = 0)$
383	382	rspcva	$⊢ (f (t) \in (ran f \cup ran g) \land \forall r \in (ran f \cup ran g) r = 0) \to f (t) = 0$
384	381 383	sylan	$⊢ ((f \in dom \int^{1} \land t \in ℝ) \land \forall r \in (ran f \cup ran g) r = 0) \to f (t) = 0$
385	384	adantllr	$⊢ (((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \land \forall r \in (ran f \cup ran g) r = 0) \to f (t) = 0$
386	20	ffnd	$⊢ g \in dom \int^{1} \to g Fn ℝ$
387		fnfvelrn	$⊢ (g Fn ℝ \land t \in ℝ) \to g (t) \in ran g$
388	386 387	sylan	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) \in ran g$
389		elun2	$⊢ g (t) \in ran g \to g (t) \in (ran f \cup ran g)$
390	388 389	syl	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) \in (ran f \cup ran g)$
391		eqeq1	$⊢ r = g (t) \to (r = 0 \leftrightarrow g (t) = 0)$
392	391	rspcva	$⊢ (g (t) \in (ran f \cup ran g) \land \forall r \in (ran f \cup ran g) r = 0) \to g (t) = 0$
393	392	oveq2d	$⊢ (g (t) \in (ran f \cup ran g) \land \forall r \in (ran f \cup ran g) r = 0) \to i g (t) = i \cdot 0$
394		it0e0	$⊢ i \cdot 0 = 0$
395	393 394	eqtrdi	$⊢ (g (t) \in (ran f \cup ran g) \land \forall r \in (ran f \cup ran g) r = 0) \to i g (t) = 0$
396	390 395	sylan	$⊢ ((g \in dom \int^{1} \land t \in ℝ) \land \forall r \in (ran f \cup ran g) r = 0) \to i g (t) = 0$
397	396	adantlll	$⊢ (((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \land \forall r \in (ran f \cup ran g) r = 0) \to i g (t) = 0$
398	385 397	oveq12d	$⊢ (((f \in dom \int^{1} \land g \in dom \int^{1}) \land t \in ℝ) \land \forall r \in (ran f \cup ran g) r = 0) \to f (t) + i g (t) = 0 + 0$
399	398	an32s	$⊢ (((f \in dom \int^{1} \land g \in dom \int^{1}) \land \forall r \in (ran f \cup ran g) r = 0) \land t \in ℝ) \to f (t) + i g (t) = 0 + 0$
400		00id	$⊢ 0 + 0 = 0$
401	399 400	eqtrdi	$⊢ (((f \in dom \int^{1} \land g \in dom \int^{1}) \land \forall r \in (ran f \cup ran g) r = 0) \land t \in ℝ) \to f (t) + i g (t) = 0$
402	401	adantlll	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \forall r \in (ran f \cup ran g) r = 0) \land t \in ℝ) \to f (t) + i g (t) = 0$
403	402	oveq2d	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \forall r \in (ran f \cup ran g) r = 0) \land t \in ℝ) \to if (t \in D, F (t), 0) - (f (t) + i g (t)) = if (t \in D, F (t), 0) - 0$
404		0cnd	$⊢ (φ \land \neg t \in D) \to 0 \in ℂ$
405	149 404	ifclda	$⊢ φ \to if (t \in D, F (t), 0) \in ℂ$
406	405	subid1d	$⊢ φ \to if (t \in D, F (t), 0) - 0 = if (t \in D, F (t), 0)$
407	406	ad3antrrr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \forall r \in (ran f \cup ran g) r = 0) \land t \in ℝ) \to if (t \in D, F (t), 0) - 0 = if (t \in D, F (t), 0)$
408	403 407	eqtrd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \forall r \in (ran f \cup ran g) r = 0) \land t \in ℝ) \to if (t \in D, F (t), 0) - (f (t) + i g (t)) = if (t \in D, F (t), 0)$
409	408	fveq2d	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \forall r \in (ran f \cup ran g) r = 0) \land t \in ℝ) \to \|if (t \in D, F (t), 0) - (f (t) + i g (t))\| = \|if (t \in D, F (t), 0)\|$
410		fvif	$⊢ \|if (t \in D, F (t), 0)\| = if (t \in D, \|F (t)\|, \|0\|)$
411		abs0	$⊢ \|0\| = 0$
412		ifeq2	$⊢ \|0\| = 0 \to if (t \in D, \|F (t)\|, \|0\|) = if (t \in D, \|F (t)\|, 0)$
413	411 412	ax-mp	$⊢ if (t \in D, \|F (t)\|, \|0\|) = if (t \in D, \|F (t)\|, 0)$
414	410 413	eqtri	$⊢ \|if (t \in D, F (t), 0)\| = if (t \in D, \|F (t)\|, 0)$
415	409 414	eqtrdi	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \forall r \in (ran f \cup ran g) r = 0) \land t \in ℝ) \to \|if (t \in D, F (t), 0) - (f (t) + i g (t))\| = if (t \in D, \|F (t)\|, 0)$
416	415	mpteq2dva	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \forall r \in (ran f \cup ran g) r = 0) \to (t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|) = (t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))$
417	416	fveq2d	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \forall r \in (ran f \cup ran g) r = 0) \to \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) = \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)))$
418	417	breq1d	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \forall r \in (ran f \cup ran g) r = 0) \to (\int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2} \leftrightarrow \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2})$
419	418	biimpd	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land \forall r \in (ran f \cup ran g) r = 0) \to (\int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2} \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2})$
420	419	ex	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (\forall r \in (ran f \cup ran g) r = 0 \to (\int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2} \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}))$
421	420	com23	$⊢ (φ \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))\|)) < \frac{y}{2} \to (\forall r \in (ran f \cup ran g) r = 0 \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}))$
422	421	imp32	$⊢ ((φ \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 \forall r \in (ran f \cup ran g) r = 0)) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}$
423	422	anasss	$⊢ (φ \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 \forall r \in (ran f \cup ran g) r = 0))) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}$
424	423	adantlr	$⊢ ((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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 \forall r \in (ran f \cup ran g) r = 0))) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}$
425		1rp	$⊢ 1 \in ℝ^{+}$
426	425	ne0ii	$⊢ ℝ^{+} \neq \emptyset$
427	352	anassrs	$⊢ ((φ \land u \in [A, B]) \land w \in [A, B]) \to G (w) - G (u) \in ℂ$
428	427	abscld	$⊢ ((φ \land u \in [A, B]) \land w \in [A, B]) \to \|G (w) - G (u)\| \in ℝ$
429	428	adantlrr	$⊢ ((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land w \in [A, B]) \to \|G (w) - G (u)\| \in ℝ$
430	429	adantlr	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \land w \in [A, B]) \to \|G (w) - G (u)\| \in ℝ$
431		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
432	431	rehalfcld	$⊢ y \in ℝ^{+} \to \frac{y}{2} \in ℝ$
433	432	adantl	$⊢ (u \in [A, B] \land y \in ℝ^{+}) \to \frac{y}{2} \in ℝ$
434	433	ad3antlr	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \land w \in [A, B]) \to \frac{y}{2} \in ℝ$
435	431	adantl	$⊢ (u \in [A, B] \land y \in ℝ^{+}) \to y \in ℝ$
436	435	ad3antlr	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \land w \in [A, B]) \to y \in ℝ$
437	430	rexrd	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \land w \in [A, B]) \to \|G (w) - G (u)\| \in ℝ^{*}$
438	157	a1i	$⊢ (φ \land \neg t \in D) \to 0 \in [0, +∞]$
439	154 438	ifclda	$⊢ φ \to if (t \in D, \|F (t)\|, 0) \in [0, +∞]$
440	439	adantr	$⊢ (φ \land t \in ℝ) \to if (t \in D, \|F (t)\|, 0) \in [0, +∞]$
441	440	fmpttd	$⊢ φ \to (t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)) : ℝ ⟶ [0, +∞]$
442		itg2cl	$⊢ (t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)) : ℝ ⟶ [0, +∞] \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) \in ℝ^{*}$
443	441 442	syl	$⊢ φ \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) \in ℝ^{*}$
444	443	ad3antrrr	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \land w \in [A, B]) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) \in ℝ^{*}$
445	434	rexrd	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \land w \in [A, B]) \to \frac{y}{2} \in ℝ^{*}$
446	109 108	oveqan12rd	$⊢ (b = u \land a = w) \to G (a) - G (b) = G (w) - G (u)$
447	446	fveq2d	$⊢ (b = u \land a = w) \to \|G (a) - G (b)\| = \|G (w) - G (u)\|$
448	447	breq1d	$⊢ (b = u \land a = w) \to (\|G (a) - G (b)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) \leftrightarrow \|G (w) - G (u)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))))$
449	99 98	oveqan12rd	$⊢ (b = w \land a = u) \to G (a) - G (b) = G (u) - G (w)$
450	449	fveq2d	$⊢ (b = w \land a = u) \to \|G (a) - G (b)\| = \|G (u) - G (w)\|$
451	450	breq1d	$⊢ (b = w \land a = u) \to (\|G (a) - G (b)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) \leftrightarrow \|G (u) - G (w)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))))$
452	129	breq1d	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (\|G (w) - G (u)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) \leftrightarrow \|G (u) - G (w)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))))$
453	321	abscld	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \|\int_{(u, w)} F (t) d t\| \in ℝ$
454	453	rexrd	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \|\int_{(u, w)} F (t) d t\| \in ℝ^{*}$
455	443	adantr	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) \in ℝ^{*}$
456	441	adantr	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)) : ℝ ⟶ [0, +∞]$
457		breq2	$⊢ \|F (t)\| = if (t \in D, \|F (t)\|, 0) \to (if (t \in (u, w), \|F (t)\|, 0) \leq \|F (t)\| \leftrightarrow if (t \in (u, w), \|F (t)\|, 0) \leq if (t \in D, \|F (t)\|, 0))$
458		breq2	$⊢ 0 = if (t \in D, \|F (t)\|, 0) \to (if (t \in (u, w), \|F (t)\|, 0) \leq 0 \leftrightarrow if (t \in (u, w), \|F (t)\|, 0) \leq if (t \in D, \|F (t)\|, 0))$
459	150	leidd	$⊢ (φ \land t \in D) \to \|F (t)\| \leq \|F (t)\|$
460		breq1	$⊢ \|F (t)\| = if (t \in (u, w), \|F (t)\|, 0) \to (\|F (t)\| \leq \|F (t)\| \leftrightarrow if (t \in (u, w), \|F (t)\|, 0) \leq \|F (t)\|)$
461		breq1	$⊢ 0 = if (t \in (u, w), \|F (t)\|, 0) \to (0 \leq \|F (t)\| \leftrightarrow if (t \in (u, w), \|F (t)\|, 0) \leq \|F (t)\|)$
462	460 461	ifboth	$⊢ (\|F (t)\| \leq \|F (t)\| \land 0 \leq \|F (t)\|) \to if (t \in (u, w), \|F (t)\|, 0) \leq \|F (t)\|$
463	459 152 462	syl2anc	$⊢ (φ \land t \in D) \to if (t \in (u, w), \|F (t)\|, 0) \leq \|F (t)\|$
464	463	adantlr	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land t \in D) \to if (t \in (u, w), \|F (t)\|, 0) \leq \|F (t)\|$
465	147	ssneld	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (\neg t \in D \to \neg t \in (u, w))$
466	465	imp	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land \neg t \in D) \to \neg t \in (u, w)$
467	226 224	eqbrtrdi	$⊢ \neg t \in (u, w) \to if (t \in (u, w), \|F (t)\|, 0) \leq 0$
468	466 467	syl	$⊢ ((φ \land (u \in [A, B] \land w \in [A, B])) \land \neg t \in D) \to if (t \in (u, w), \|F (t)\|, 0) \leq 0$
469	457 458 464 468	ifbothda	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to if (t \in (u, w), \|F (t)\|, 0) \leq if (t \in D, \|F (t)\|, 0)$
470	469	ralrimivw	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \forall t \in ℝ if (t \in (u, w), \|F (t)\|, 0) \leq if (t \in D, \|F (t)\|, 0)$
471	233 234	ifex	$⊢ if (t \in D, \|F (t)\|, 0) \in V$
472	471	a1i	$⊢ (φ \land t \in ℝ) \to if (t \in D, \|F (t)\|, 0) \in V$
473		eqidd	$⊢ φ \to (t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)) = (t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))$
474	232 236 472 240 473	ofrfval2	$⊢ φ \to ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)) \leq_{f} (t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)) \leftrightarrow \forall t \in ℝ if (t \in (u, w), \|F (t)\|, 0) \leq if (t \in D, \|F (t)\|, 0))$
475	474	adantr	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)) \leq_{f} (t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)) \leftrightarrow \forall t \in ℝ if (t \in (u, w), \|F (t)\|, 0) \leq if (t \in D, \|F (t)\|, 0))$
476	470 475	mpbird	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to (t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)) \leq_{f} (t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))$
477		itg2le	$⊢ ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)) : ℝ ⟶ [0, +∞] \land (t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)) : ℝ ⟶ [0, +∞] \land (t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0)) \leq_{f} (t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)))$
478	161 456 476 477	syl3anc	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \int^{2} ((t \in ℝ ⟼ if (t \in (u, w), \|F (t)\|, 0))) \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)))$
479	454 163 455 346 478	xrletrd	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \|\int_{(u, w)} F (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)))$
480	479	3adantr3	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to \|\int_{(u, w)} F (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)))$
481	325 480	eqbrtrd	$⊢ (φ \land (u \in [A, B] \land w \in [A, B] \land u \leq w)) \to \|G (w) - G (u)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)))$
482	448 451 115 452 481	wlogle	$⊢ (φ \land (u \in [A, B] \land w \in [A, B])) \to \|G (w) - G (u)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)))$
483	482	anassrs	$⊢ ((φ \land u \in [A, B]) \land w \in [A, B]) \to \|G (w) - G (u)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)))$
484	483	adantlrr	$⊢ ((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land w \in [A, B]) \to \|G (w) - G (u)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)))$
485	484	adantlr	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \land w \in [A, B]) \to \|G (w) - G (u)\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0)))$
486		simplr	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \land w \in [A, B]) \to \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}$
487	437 444 445 485 486	xrlelttrd	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \land w \in [A, B]) \to \|G (w) - G (u)\| < \frac{y}{2}$
488		rphalflt	$⊢ y \in ℝ^{+} \to \frac{y}{2} < y$
489	488	adantl	$⊢ (u \in [A, B] \land y \in ℝ^{+}) \to \frac{y}{2} < y$
490	489	ad3antlr	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \land w \in [A, B]) \to \frac{y}{2} < y$
491	430 434 436 487 490	lttrd	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \land w \in [A, B]) \to \|G (w) - G (u)\| < y$
492	491	a1d	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \land w \in [A, B]) \to (\|w - u\| < z \to \|G (w) - G (u)\| < y)$
493	492	ralrimiva	$⊢ ((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \to \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)$
494	493	ralrimivw	$⊢ ((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \to \forall z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)$
495		r19.2z	$⊢ (ℝ^{+} \neq \emptyset \land \forall z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)) \to \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)$
496	426 494 495	sylancr	$⊢ ((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land \int^{2} ((t \in ℝ ⟼ if (t \in D, \|F (t)\|, 0))) < \frac{y}{2}) \to \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)$
497	424 496	syldan	$⊢ ((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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 \forall r \in (ran f \cup ran g) r = 0))) \to \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)$
498	497	anassrs	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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 \forall r \in (ran f \cup ran g) r = 0)) \to \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)$
499	498	anassrs	$⊢ ((((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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 \forall r \in (ran f \cup ran g) r = 0) \to \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)$
500	376 499	sylan2b	$⊢ ((((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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 \neg \exists r \in (ran f \cup ran g) r \neq 0) \to \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)$
501	372 500	pm2.61dan	$⊢ (((φ \land (u \in [A, B] \land y \in ℝ^{+})) \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}) \to \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)$
502	501	ex	$⊢ ((φ \land (u \in [A, B] \land y \in ℝ^{+})) \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (\int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2} \to \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y))$
503	502	rexlimdvva	$⊢ (φ \land (u \in [A, B] \land y \in ℝ^{+})) \to (\exists f \in dom \int^{1} \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|if (t \in D, F (t), 0) - (f (t) + i g (t))\|)) < \frac{y}{2} \to \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y))$
504	14 503	mpd	$⊢ (φ \land (u \in [A, B] \land y \in ℝ^{+})) \to \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)$
505	504	ralrimivva	$⊢ φ \to \forall u \in [A, B] \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)$
506		ssid	$⊢ ℂ \subseteq ℂ$
507		elcncf2	$⊢ ([A, B] \subseteq ℂ \land ℂ \subseteq ℂ) \to (G : [A, B] \underset{cn}{⟶} ℂ \leftrightarrow (G : [A, B] ⟶ ℂ \land \forall u \in [A, B] \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)))$
508	118 506 507	sylancl	$⊢ φ \to (G : [A, B] \underset{cn}{⟶} ℂ \leftrightarrow (G : [A, B] ⟶ ℂ \land \forall u \in [A, B] \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in [A, B] (\|w - u\| < z \to \|G (w) - G (u)\| < y)))$
509	10 505 508	mpbir2and	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem ftc1anc

Proof