ftc1anclem5

Description: Lemma for ftc1anc , the existence of a simple function the integral of whose pointwise difference from the function is less than a given positive real. (Contributed by Brendan Leahy, 17-Jun-2018)

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

Proof

Step	Hyp	Ref	Expression
1		ftc1anc.g	$⊢ G = (x \in [A, B] ⟼ \int_{(A, x)} F (t) d t)$
2		ftc1anc.a	$⊢ φ \to A \in ℝ$
3		ftc1anc.b	$⊢ φ \to B \in ℝ$
4		ftc1anc.le	$⊢ φ \to A \leq B$
5		ftc1anc.s	$⊢ φ \to (A, B) \subseteq D$
6		ftc1anc.d	$⊢ φ \to D \subseteq ℝ$
7		ftc1anc.i	$⊢ φ \to F \in 𝐿^{1}$
8		ftc1anc.f	$⊢ φ \to F : D ⟶ ℂ$
9		iftrue	$⊢ t \in ℝ \to if (t \in ℝ, \|ℜ (if (t \in D, F (t), 0))\|, 0) = \|ℜ (if (t \in D, F (t), 0))\|$
10	9	mpteq2ia	$⊢ (t \in ℝ ⟼ if (t \in ℝ, \|ℜ (if (t \in D, F (t), 0))\|, 0)) = (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)$
11	10	fveq2i	$⊢ \int^{2} ((t \in ℝ ⟼ if (t \in ℝ, \|ℜ (if (t \in D, F (t), 0))\|, 0))) = \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|))$
12	8	ffvelrnda	$⊢ (φ \land t \in D) \to F (t) \in ℂ$
13		0cnd	$⊢ (φ \land \neg t \in D) \to 0 \in ℂ$
14	12 13	ifclda	$⊢ φ \to if (t \in D, F (t), 0) \in ℂ$
15	14	recld	$⊢ φ \to ℜ (if (t \in D, F (t), 0)) \in ℝ$
16	15	adantr	$⊢ (φ \land t \in ℝ) \to ℜ (if (t \in D, F (t), 0)) \in ℝ$
17		rembl	$⊢ ℝ \in dom vol$
18	17	a1i	$⊢ φ \to ℝ \in dom vol$
19	15	adantr	$⊢ (φ \land t \in D) \to ℜ (if (t \in D, F (t), 0)) \in ℝ$
20		eldifn	$⊢ t \in (ℝ ∖ D) \to \neg t \in D$
21	20	adantl	$⊢ (φ \land t \in (ℝ ∖ D)) \to \neg t \in D$
22		iffalse	$⊢ \neg t \in D \to if (t \in D, F (t), 0) = 0$
23	22	fveq2d	$⊢ \neg t \in D \to ℜ (if (t \in D, F (t), 0)) = ℜ (0)$
24		re0	$⊢ ℜ (0) = 0$
25	23 24	eqtrdi	$⊢ \neg t \in D \to ℜ (if (t \in D, F (t), 0)) = 0$
26	21 25	syl	$⊢ (φ \land t \in (ℝ ∖ D)) \to ℜ (if (t \in D, F (t), 0)) = 0$
27		iftrue	$⊢ t \in D \to if (t \in D, F (t), 0) = F (t)$
28	27	fveq2d	$⊢ t \in D \to ℜ (if (t \in D, F (t), 0)) = ℜ (F (t))$
29	28	mpteq2ia	$⊢ (t \in D ⟼ ℜ (if (t \in D, F (t), 0))) = (t \in D ⟼ ℜ (F (t)))$
30	8	feqmptd	$⊢ φ \to F = (t \in D ⟼ F (t))$
31	30 7	eqeltrrd	$⊢ φ \to (t \in D ⟼ F (t)) \in 𝐿^{1}$
32	12	iblcn	$⊢ φ \to ((t \in D ⟼ F (t)) \in 𝐿^{1} \leftrightarrow ((t \in D ⟼ ℜ (F (t))) \in 𝐿^{1} \land (t \in D ⟼ ℑ (F (t))) \in 𝐿^{1}))$
33	31 32	mpbid	$⊢ φ \to ((t \in D ⟼ ℜ (F (t))) \in 𝐿^{1} \land (t \in D ⟼ ℑ (F (t))) \in 𝐿^{1})$
34	33	simpld	$⊢ φ \to (t \in D ⟼ ℜ (F (t))) \in 𝐿^{1}$
35	29 34	eqeltrid	$⊢ φ \to (t \in D ⟼ ℜ (if (t \in D, F (t), 0))) \in 𝐿^{1}$
36	6 18 19 26 35	iblss2	$⊢ φ \to (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) \in 𝐿^{1}$
37	15	recnd	$⊢ φ \to ℜ (if (t \in D, F (t), 0)) \in ℂ$
38	37	adantr	$⊢ (φ \land t \in ℝ) \to ℜ (if (t \in D, F (t), 0)) \in ℂ$
39		eqidd	$⊢ φ \to (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) = (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))$
40		absf	$⊢ abs : ℂ ⟶ ℝ$
41	40	a1i	$⊢ φ \to abs : ℂ ⟶ ℝ$
42	41	feqmptd	$⊢ φ \to abs = (x \in ℂ ⟼ \|x\|)$
43		fveq2	$⊢ x = ℜ (if (t \in D, F (t), 0)) \to \|x\| = \|ℜ (if (t \in D, F (t), 0))\|$
44	38 39 42 43	fmptco	$⊢ φ \to abs \circ (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) = (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)$
45	16	fmpttd	$⊢ φ \to (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) : ℝ ⟶ ℝ$
46		iblmbf	$⊢ F \in 𝐿^{1} \to F \in MblFn$
47	7 46	syl	$⊢ φ \to F \in MblFn$
48	30 47	eqeltrrd	$⊢ φ \to (t \in D ⟼ F (t)) \in MblFn$
49	12	ismbfcn2	$⊢ φ \to ((t \in D ⟼ F (t)) \in MblFn \leftrightarrow ((t \in D ⟼ ℜ (F (t))) \in MblFn \land (t \in D ⟼ ℑ (F (t))) \in MblFn))$
50	48 49	mpbid	$⊢ φ \to ((t \in D ⟼ ℜ (F (t))) \in MblFn \land (t \in D ⟼ ℑ (F (t))) \in MblFn)$
51	50	simpld	$⊢ φ \to (t \in D ⟼ ℜ (F (t))) \in MblFn$
52	29 51	eqeltrid	$⊢ φ \to (t \in D ⟼ ℜ (if (t \in D, F (t), 0))) \in MblFn$
53	6 18 19 26 52	mbfss	$⊢ φ \to (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) \in MblFn$
54		ftc1anclem1	$⊢ ((t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) : ℝ ⟶ ℝ \land (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) \in MblFn) \to abs \circ (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) \in MblFn$
55	45 53 54	syl2anc	$⊢ φ \to abs \circ (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0))) \in MblFn$
56	44 55	eqeltrrd	$⊢ φ \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \in MblFn$
57	16 36 56	iblabsnc	$⊢ φ \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \in 𝐿^{1}$
58	37	abscld	$⊢ φ \to \|ℜ (if (t \in D, F (t), 0))\| \in ℝ$
59	58	adantr	$⊢ (φ \land t \in ℝ) \to \|ℜ (if (t \in D, F (t), 0))\| \in ℝ$
60	37	absge0d	$⊢ φ \to 0 \leq \|ℜ (if (t \in D, F (t), 0))\|$
61	60	adantr	$⊢ (φ \land t \in ℝ) \to 0 \leq \|ℜ (if (t \in D, F (t), 0))\|$
62	59 61	iblpos	$⊢ φ \to ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \in 𝐿^{1} \leftrightarrow ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \in MblFn \land \int^{2} ((t \in ℝ ⟼ if (t \in ℝ, \|ℜ (if (t \in D, F (t), 0))\|, 0))) \in ℝ))$
63	57 62	mpbid	$⊢ φ \to ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \in MblFn \land \int^{2} ((t \in ℝ ⟼ if (t \in ℝ, \|ℜ (if (t \in D, F (t), 0))\|, 0))) \in ℝ)$
64	63	simprd	$⊢ φ \to \int^{2} ((t \in ℝ ⟼ if (t \in ℝ, \|ℜ (if (t \in D, F (t), 0))\|, 0))) \in ℝ$
65	11 64	eqeltrrid	$⊢ φ \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \in ℝ$
66		ltsubrp	$⊢ (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \in ℝ \land Y \in ℝ^{+}) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y < \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|))$
67	65 66	sylan	$⊢ (φ \land Y \in ℝ^{+}) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y < \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|))$
68		rpre	$⊢ Y \in ℝ^{+} \to Y \in ℝ$
69		resubcl	$⊢ (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \in ℝ \land Y \in ℝ) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y \in ℝ$
70	65 68 69	syl2an	$⊢ (φ \land Y \in ℝ^{+}) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y \in ℝ$
71	65	adantr	$⊢ (φ \land Y \in ℝ^{+}) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \in ℝ$
72	70 71	ltnled	$⊢ (φ \land Y \in ℝ^{+}) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y < \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \leftrightarrow \neg \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y)$
73	67 72	mpbid	$⊢ (φ \land Y \in ℝ^{+}) \to \neg \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y$
74	58	rexrd	$⊢ φ \to \|ℜ (if (t \in D, F (t), 0))\| \in ℝ^{*}$
75		elxrge0	$⊢ \|ℜ (if (t \in D, F (t), 0))\| \in [0, +∞] \leftrightarrow (\|ℜ (if (t \in D, F (t), 0))\| \in ℝ^{*} \land 0 \leq \|ℜ (if (t \in D, F (t), 0))\|)$
76	74 60 75	sylanbrc	$⊢ φ \to \|ℜ (if (t \in D, F (t), 0))\| \in [0, +∞]$
77	76	adantr	$⊢ (φ \land t \in ℝ) \to \|ℜ (if (t \in D, F (t), 0))\| \in [0, +∞]$
78	77	fmpttd	$⊢ φ \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) : ℝ ⟶ [0, +∞]$
79	78	adantr	$⊢ (φ \land Y \in ℝ^{+}) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) : ℝ ⟶ [0, +∞]$
80	70	rexrd	$⊢ (φ \land Y \in ℝ^{+}) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y \in ℝ^{*}$
81		itg2leub	$⊢ ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) : ℝ ⟶ [0, +∞] \land \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y \in ℝ^{*}) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y \leftrightarrow \forall g \in dom \int^{1} (g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \to \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y))$
82	79 80 81	syl2anc	$⊢ (φ \land Y \in ℝ^{+}) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y \leftrightarrow \forall g \in dom \int^{1} (g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \to \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y))$
83	73 82	mtbid	$⊢ (φ \land Y \in ℝ^{+}) \to \neg \forall g \in dom \int^{1} (g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \to \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y)$
84		rexanali	$⊢ \exists g \in dom \int^{1} (g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \land \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y) \leftrightarrow \neg \forall g \in dom \int^{1} (g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \to \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y)$
85	83 84	sylibr	$⊢ (φ \land Y \in ℝ^{+}) \to \exists g \in dom \int^{1} (g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \land \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y)$
86	70	ad2antrr	$⊢ (((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \land \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y \in ℝ$
87		itg1cl	$⊢ g \in dom \int^{1} \to \int^{1} (g) \in ℝ$
88	87	ad2antlr	$⊢ (((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \land \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y) \to \int^{1} (g) \in ℝ$
89		eqid	$⊢ (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) = (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))$
90	89	i1fpos	$⊢ g \in dom \int^{1} \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in dom \int^{1}$
91		0re	$⊢ 0 \in ℝ$
92		i1ff	$⊢ g \in dom \int^{1} \to g : ℝ ⟶ ℝ$
93	92	ffvelrnda	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) \in ℝ$
94		max1	$⊢ (0 \in ℝ \land g (t) \in ℝ) \to 0 \leq if (0 \leq g (t), g (t), 0)$
95	91 93 94	sylancr	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to 0 \leq if (0 \leq g (t), g (t), 0)$
96	95	ralrimiva	$⊢ g \in dom \int^{1} \to \forall t \in ℝ 0 \leq if (0 \leq g (t), g (t), 0)$
97		ax-resscn	$⊢ ℝ \subseteq ℂ$
98	97	a1i	$⊢ g \in dom \int^{1} \to ℝ \subseteq ℂ$
99		fvex	$⊢ g (t) \in V$
100		c0ex	$⊢ 0 \in V$
101	99 100	ifex	$⊢ if (0 \leq g (t), g (t), 0) \in V$
102	101 89	fnmpti	$⊢ (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) Fn ℝ$
103	102	a1i	$⊢ g \in dom \int^{1} \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) Fn ℝ$
104	98 103	0pledm	$⊢ g \in dom \int^{1} \to (0_{𝑝} \leq_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \leftrightarrow (ℝ \times \{0\}) \leq_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)))$
105		reex	$⊢ ℝ \in V$
106	105	a1i	$⊢ g \in dom \int^{1} \to ℝ \in V$
107	100	a1i	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to 0 \in V$
108		ifcl	$⊢ (g (t) \in ℝ \land 0 \in ℝ) \to if (0 \leq g (t), g (t), 0) \in ℝ$
109	93 91 108	sylancl	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to if (0 \leq g (t), g (t), 0) \in ℝ$
110		fconstmpt	$⊢ ℝ \times \{0\} = (t \in ℝ ⟼ 0)$
111	110	a1i	$⊢ g \in dom \int^{1} \to ℝ \times \{0\} = (t \in ℝ ⟼ 0)$
112		eqidd	$⊢ g \in dom \int^{1} \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) = (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))$
113	106 107 109 111 112	ofrfval2	$⊢ g \in dom \int^{1} \to ((ℝ \times \{0\}) \leq_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \leftrightarrow \forall t \in ℝ 0 \leq if (0 \leq g (t), g (t), 0))$
114	104 113	bitrd	$⊢ g \in dom \int^{1} \to (0_{𝑝} \leq_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \leftrightarrow \forall t \in ℝ 0 \leq if (0 \leq g (t), g (t), 0))$
115	96 114	mpbird	$⊢ g \in dom \int^{1} \to 0_{𝑝} \leq_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))$
116		itg2itg1	$⊢ ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in dom \int^{1} \land 0_{𝑝} \leq_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) \to \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) = \int^{1} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)))$
117	90 115 116	syl2anc	$⊢ g \in dom \int^{1} \to \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) = \int^{1} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)))$
118		itg1cl	$⊢ (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in dom \int^{1} \to \int^{1} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) \in ℝ$
119	90 118	syl	$⊢ g \in dom \int^{1} \to \int^{1} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) \in ℝ$
120	117 119	eqeltrd	$⊢ g \in dom \int^{1} \to \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) \in ℝ$
121	120	ad2antlr	$⊢ (((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \land \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y) \to \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) \in ℝ$
122		ltnle	$⊢ (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y \in ℝ \land \int^{1} (g) \in ℝ) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y < \int^{1} (g) \leftrightarrow \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y)$
123	70 87 122	syl2an	$⊢ ((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y < \int^{1} (g) \leftrightarrow \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y)$
124	123	biimpar	$⊢ (((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \land \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y < \int^{1} (g)$
125		max2	$⊢ (0 \in ℝ \land g (t) \in ℝ) \to g (t) \leq if (0 \leq g (t), g (t), 0)$
126	91 93 125	sylancr	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) \leq if (0 \leq g (t), g (t), 0)$
127	126	ralrimiva	$⊢ g \in dom \int^{1} \to \forall t \in ℝ g (t) \leq if (0 \leq g (t), g (t), 0)$
128	92	feqmptd	$⊢ g \in dom \int^{1} \to g = (t \in ℝ ⟼ g (t))$
129	106 93 109 128 112	ofrfval2	$⊢ g \in dom \int^{1} \to (g \leq_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \leftrightarrow \forall t \in ℝ g (t) \leq if (0 \leq g (t), g (t), 0))$
130	127 129	mpbird	$⊢ g \in dom \int^{1} \to g \leq_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))$
131		itg1le	$⊢ (g \in dom \int^{1} \land (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in dom \int^{1} \land g \leq_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) \to \int^{1} (g) \leq \int^{1} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)))$
132	90 130 131	mpd3an23	$⊢ g \in dom \int^{1} \to \int^{1} (g) \leq \int^{1} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)))$
133	132 117	breqtrrd	$⊢ g \in dom \int^{1} \to \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)))$
134	133	ad2antlr	$⊢ (((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \land \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y) \to \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)))$
135	86 88 121 124 134	ltletrd	$⊢ (((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \land \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)))$
136	135	adantrl	$⊢ (((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \land (g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \land \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y)) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)))$
137		i1fmbf	$⊢ (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in dom \int^{1} \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in MblFn$
138	90 137	syl	$⊢ g \in dom \int^{1} \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in MblFn$
139	138	adantl	$⊢ (φ \land g \in dom \int^{1}) \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in MblFn$
140		elrege0	$⊢ if (0 \leq g (t), g (t), 0) \in [0, +∞) \leftrightarrow (if (0 \leq g (t), g (t), 0) \in ℝ \land 0 \leq if (0 \leq g (t), g (t), 0))$
141	109 95 140	sylanbrc	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to if (0 \leq g (t), g (t), 0) \in [0, +∞)$
142	141	fmpttd	$⊢ g \in dom \int^{1} \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) : ℝ ⟶ [0, +∞)$
143	142	adantl	$⊢ (φ \land g \in dom \int^{1}) \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) : ℝ ⟶ [0, +∞)$
144	120	adantl	$⊢ (φ \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) \in ℝ$
145	109	recnd	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to if (0 \leq g (t), g (t), 0) \in ℂ$
146	145	negcld	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to - if (0 \leq g (t), g (t), 0) \in ℂ$
147	145 146	ifcld	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0)) \in ℂ$
148		subcl	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℂ \land if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0)) \in ℂ) \to ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0)) \in ℂ$
149	37 147 148	syl2an	$⊢ (φ \land (g \in dom \int^{1} \land t \in ℝ)) \to ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0)) \in ℂ$
150	149	anassrs	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0)) \in ℂ$
151	150	abscld	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| \in ℝ$
152	150	absge0d	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to 0 \leq \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|$
153		elrege0	$⊢ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| \in [0, +∞) \leftrightarrow (\|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| \in ℝ \land 0 \leq \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)$
154	151 152 153	sylanbrc	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| \in [0, +∞)$
155	154	fmpttd	$⊢ (φ \land g \in dom \int^{1}) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|) : ℝ ⟶ [0, +∞)$
156		eleq1w	$⊢ x = t \to (x \in D \leftrightarrow t \in D)$
157		fveq2	$⊢ x = t \to F (x) = F (t)$
158	156 157	ifbieq1d	$⊢ x = t \to if (x \in D, F (x), 0) = if (t \in D, F (t), 0)$
159	158	fveq2d	$⊢ x = t \to ℜ (if (x \in D, F (x), 0)) = ℜ (if (t \in D, F (t), 0))$
160		eqid	$⊢ (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) = (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0)))$
161		fvex	$⊢ ℜ (if (t \in D, F (t), 0)) \in V$
162	159 160 161	fvmpt	$⊢ t \in ℝ \to (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) = ℜ (if (t \in D, F (t), 0))$
163	159	breq2d	$⊢ x = t \to (0 \leq ℜ (if (x \in D, F (x), 0)) \leftrightarrow 0 \leq ℜ (if (t \in D, F (t), 0)))$
164		fveq2	$⊢ x = t \to g (x) = g (t)$
165	164	breq2d	$⊢ x = t \to (0 \leq g (x) \leftrightarrow 0 \leq g (t))$
166	165 164	ifbieq1d	$⊢ x = t \to if (0 \leq g (x), g (x), 0) = if (0 \leq g (t), g (t), 0)$
167	166	negeqd	$⊢ x = t \to - if (0 \leq g (x), g (x), 0) = - if (0 \leq g (t), g (t), 0)$
168	163 166 167	ifbieq12d	$⊢ x = t \to if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0)) = if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))$
169		eqid	$⊢ (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) = (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0)))$
170		negex	$⊢ - if (0 \leq g (t), g (t), 0) \in V$
171	101 170	ifex	$⊢ if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0)) \in V$
172	168 169 171	fvmpt	$⊢ t \in ℝ \to (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) (t) = if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))$
173	162 172	oveq12d	$⊢ t \in ℝ \to (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) - (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) (t) = ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))$
174	173	fveq2d	$⊢ t \in ℝ \to \|(x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) - (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) (t)\| = \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|$
175	174	mpteq2ia	$⊢ (t \in ℝ ⟼ \|(x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) - (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) (t)\|) = (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)$
176	175	fveq2i	$⊢ \int^{2} ((t \in ℝ ⟼ \|(x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) - (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) (t)\|)) = \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|))$
177	105	a1i	$⊢ φ \to ℝ \in V$
178		fvex	$⊢ g (x) \in V$
179	178 100	ifex	$⊢ if (0 \leq g (x), g (x), 0) \in V$
180	179 100	ifex	$⊢ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), 0) \in V$
181	180	a1i	$⊢ (φ \land x \in ℝ) \to if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), 0) \in V$
182		ovex	$⊢ -1 if (0 \leq g (x), g (x), 0) \in V$
183	100 182	ifex	$⊢ if (0 \leq ℜ (if (x \in D, F (x), 0)), 0, -1 if (0 \leq g (x), g (x), 0)) \in V$
184	183	a1i	$⊢ (φ \land x \in ℝ) \to if (0 \leq ℜ (if (x \in D, F (x), 0)), 0, -1 if (0 \leq g (x), g (x), 0)) \in V$
185		ffn	$⊢ F : D ⟶ ℂ \to F Fn D$
186		frn	$⊢ F : D ⟶ ℂ \to ran F \subseteq ℂ$
187		ref	$⊢ ℜ : ℂ ⟶ ℝ$
188		ffn	$⊢ ℜ : ℂ ⟶ ℝ \to ℜ Fn ℂ$
189	187 188	ax-mp	$⊢ ℜ Fn ℂ$
190		fnco	$⊢ (ℜ Fn ℂ \land F Fn D \land ran F \subseteq ℂ) \to (ℜ \circ F) Fn D$
191	189 190	mp3an1	$⊢ (F Fn D \land ran F \subseteq ℂ) \to (ℜ \circ F) Fn D$
192	185 186 191	syl2anc	$⊢ F : D ⟶ ℂ \to (ℜ \circ F) Fn D$
193		elpreima	$⊢ (ℜ \circ F) Fn D \to (x \in {(ℜ \circ F)}^{-1} [[0, +∞)] \leftrightarrow (x \in D \land (ℜ \circ F) (x) \in [0, +∞)))$
194	8 192 193	3syl	$⊢ φ \to (x \in {(ℜ \circ F)}^{-1} [[0, +∞)] \leftrightarrow (x \in D \land (ℜ \circ F) (x) \in [0, +∞)))$
195		fco	$⊢ (ℜ : ℂ ⟶ ℝ \land F : D ⟶ ℂ) \to (ℜ \circ F) : D ⟶ ℝ$
196	187 8 195	sylancr	$⊢ φ \to (ℜ \circ F) : D ⟶ ℝ$
197	196	ffvelrnda	$⊢ (φ \land x \in D) \to (ℜ \circ F) (x) \in ℝ$
198	197	biantrurd	$⊢ (φ \land x \in D) \to (0 \leq (ℜ \circ F) (x) \leftrightarrow ((ℜ \circ F) (x) \in ℝ \land 0 \leq (ℜ \circ F) (x)))$
199		elrege0	$⊢ (ℜ \circ F) (x) \in [0, +∞) \leftrightarrow ((ℜ \circ F) (x) \in ℝ \land 0 \leq (ℜ \circ F) (x))$
200	198 199	bitr4di	$⊢ (φ \land x \in D) \to (0 \leq (ℜ \circ F) (x) \leftrightarrow (ℜ \circ F) (x) \in [0, +∞))$
201		fvco3	$⊢ (F : D ⟶ ℂ \land x \in D) \to (ℜ \circ F) (x) = ℜ (F (x))$
202	8 201	sylan	$⊢ (φ \land x \in D) \to (ℜ \circ F) (x) = ℜ (F (x))$
203	202	breq2d	$⊢ (φ \land x \in D) \to (0 \leq (ℜ \circ F) (x) \leftrightarrow 0 \leq ℜ (F (x)))$
204	200 203	bitr3d	$⊢ (φ \land x \in D) \to ((ℜ \circ F) (x) \in [0, +∞) \leftrightarrow 0 \leq ℜ (F (x)))$
205	204	pm5.32da	$⊢ φ \to ((x \in D \land (ℜ \circ F) (x) \in [0, +∞)) \leftrightarrow (x \in D \land 0 \leq ℜ (F (x))))$
206	194 205	bitrd	$⊢ φ \to (x \in {(ℜ \circ F)}^{-1} [[0, +∞)] \leftrightarrow (x \in D \land 0 \leq ℜ (F (x))))$
207	206	adantr	$⊢ (φ \land x \in ℝ) \to (x \in {(ℜ \circ F)}^{-1} [[0, +∞)] \leftrightarrow (x \in D \land 0 \leq ℜ (F (x))))$
208		eldif	$⊢ x \in (ℝ ∖ D) \leftrightarrow (x \in ℝ \land \neg x \in D)$
209	208	baibr	$⊢ x \in ℝ \to (\neg x \in D \leftrightarrow x \in (ℝ ∖ D))$
210		0le0	$⊢ 0 \leq 0$
211	210 24	breqtrri	$⊢ 0 \leq ℜ (0)$
212	211	biantru	$⊢ \neg x \in D \leftrightarrow (\neg x \in D \land 0 \leq ℜ (0))$
213	209 212	bitr3di	$⊢ x \in ℝ \to (x \in (ℝ ∖ D) \leftrightarrow (\neg x \in D \land 0 \leq ℜ (0)))$
214	213	adantl	$⊢ (φ \land x \in ℝ) \to (x \in (ℝ ∖ D) \leftrightarrow (\neg x \in D \land 0 \leq ℜ (0)))$
215	207 214	orbi12d	$⊢ (φ \land x \in ℝ) \to ((x \in {(ℜ \circ F)}^{-1} [[0, +∞)] \lor x \in (ℝ ∖ D)) \leftrightarrow ((x \in D \land 0 \leq ℜ (F (x))) \lor (\neg x \in D \land 0 \leq ℜ (0))))$
216		elun	$⊢ x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)) \leftrightarrow (x \in {(ℜ \circ F)}^{-1} [[0, +∞)] \lor x \in (ℝ ∖ D))$
217		fveq2	$⊢ if (x \in D, F (x), 0) = F (x) \to ℜ (if (x \in D, F (x), 0)) = ℜ (F (x))$
218	217	breq2d	$⊢ if (x \in D, F (x), 0) = F (x) \to (0 \leq ℜ (if (x \in D, F (x), 0)) \leftrightarrow 0 \leq ℜ (F (x)))$
219		fveq2	$⊢ if (x \in D, F (x), 0) = 0 \to ℜ (if (x \in D, F (x), 0)) = ℜ (0)$
220	219	breq2d	$⊢ if (x \in D, F (x), 0) = 0 \to (0 \leq ℜ (if (x \in D, F (x), 0)) \leftrightarrow 0 \leq ℜ (0))$
221	218 220	elimif	$⊢ 0 \leq ℜ (if (x \in D, F (x), 0)) \leftrightarrow ((x \in D \land 0 \leq ℜ (F (x))) \lor (\neg x \in D \land 0 \leq ℜ (0)))$
222	215 216 221	3bitr4g	$⊢ (φ \land x \in ℝ) \to (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)) \leftrightarrow 0 \leq ℜ (if (x \in D, F (x), 0)))$
223	222	ifbid	$⊢ (φ \land x \in ℝ) \to if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), if (0 \leq g (x), g (x), 0), 0) = if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), 0)$
224	223	mpteq2dva	$⊢ φ \to (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), if (0 \leq g (x), g (x), 0), 0)) = (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), 0))$
225	222	ifbid	$⊢ (φ \land x \in ℝ) \to if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), 0, -1 if (0 \leq g (x), g (x), 0)) = if (0 \leq ℜ (if (x \in D, F (x), 0)), 0, -1 if (0 \leq g (x), g (x), 0))$
226	225	mpteq2dva	$⊢ φ \to (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), 0, -1 if (0 \leq g (x), g (x), 0))) = (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), 0, -1 if (0 \leq g (x), g (x), 0)))$
227	177 181 184 224 226	offval2	$⊢ φ \to (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), if (0 \leq g (x), g (x), 0), 0)) +_{f} (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), 0, -1 if (0 \leq g (x), g (x), 0))) = (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), 0) + if (0 \leq ℜ (if (x \in D, F (x), 0)), 0, -1 if (0 \leq g (x), g (x), 0)))$
228		ovif12	$⊢ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), 0) + if (0 \leq ℜ (if (x \in D, F (x), 0)), 0, -1 if (0 \leq g (x), g (x), 0)) = if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0) + 0, 0 + -1 if (0 \leq g (x), g (x), 0))$
229	92	ffvelrnda	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to g (x) \in ℝ$
230	229	recnd	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to g (x) \in ℂ$
231		0cn	$⊢ 0 \in ℂ$
232		ifcl	$⊢ (g (x) \in ℂ \land 0 \in ℂ) \to if (0 \leq g (x), g (x), 0) \in ℂ$
233	230 231 232	sylancl	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to if (0 \leq g (x), g (x), 0) \in ℂ$
234	233	addid1d	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to if (0 \leq g (x), g (x), 0) + 0 = if (0 \leq g (x), g (x), 0)$
235	233	mulm1d	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to -1 if (0 \leq g (x), g (x), 0) = - if (0 \leq g (x), g (x), 0)$
236	235	oveq2d	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to 0 + -1 if (0 \leq g (x), g (x), 0) = 0 + (- if (0 \leq g (x), g (x), 0))$
237	233	negcld	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to - if (0 \leq g (x), g (x), 0) \in ℂ$
238	237	addid2d	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to 0 + (- if (0 \leq g (x), g (x), 0)) = - if (0 \leq g (x), g (x), 0)$
239	236 238	eqtrd	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to 0 + -1 if (0 \leq g (x), g (x), 0) = - if (0 \leq g (x), g (x), 0)$
240	234 239	ifeq12d	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0) + 0, 0 + -1 if (0 \leq g (x), g (x), 0)) = if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))$
241	228 240	eqtrid	$⊢ (g \in dom \int^{1} \land x \in ℝ) \to if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), 0) + if (0 \leq ℜ (if (x \in D, F (x), 0)), 0, -1 if (0 \leq g (x), g (x), 0)) = if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))$
242	241	mpteq2dva	$⊢ g \in dom \int^{1} \to (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), 0) + if (0 \leq ℜ (if (x \in D, F (x), 0)), 0, -1 if (0 \leq g (x), g (x), 0))) = (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0)))$
243	227 242	sylan9eq	$⊢ (φ \land g \in dom \int^{1}) \to (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), if (0 \leq g (x), g (x), 0), 0)) +_{f} (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), 0, -1 if (0 \leq g (x), g (x), 0))) = (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0)))$
244		0xr	$⊢ 0 \in ℝ^{*}$
245		pnfxr	$⊢ +∞ \in ℝ^{*}$
246		0ltpnf	$⊢ 0 < +∞$
247		snunioo	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land 0 < +∞) \to \{0\} \cup (0, +∞) = [0, +∞)$
248	244 245 246 247	mp3an	$⊢ \{0\} \cup (0, +∞) = [0, +∞)$
249	248	imaeq2i	$⊢ {(ℜ \circ F)}^{-1} [\{0\} \cup (0, +∞)] = {(ℜ \circ F)}^{-1} [[0, +∞)]$
250		imaundi	$⊢ {(ℜ \circ F)}^{-1} [\{0\} \cup (0, +∞)] = {(ℜ \circ F)}^{-1} [\{0\}] \cup {(ℜ \circ F)}^{-1} [(0, +∞)]$
251	249 250	eqtr3i	$⊢ {(ℜ \circ F)}^{-1} [[0, +∞)] = {(ℜ \circ F)}^{-1} [\{0\}] \cup {(ℜ \circ F)}^{-1} [(0, +∞)]$
252		ismbfcn	$⊢ F : D ⟶ ℂ \to (F \in MblFn \leftrightarrow (ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn))$
253	8 252	syl	$⊢ φ \to (F \in MblFn \leftrightarrow (ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn))$
254	47 253	mpbid	$⊢ φ \to (ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn)$
255	254	simpld	$⊢ φ \to ℜ \circ F \in MblFn$
256		mbfimasn	$⊢ (ℜ \circ F \in MblFn \land (ℜ \circ F) : D ⟶ ℝ \land 0 \in ℝ) \to {(ℜ \circ F)}^{-1} [\{0\}] \in dom vol$
257	91 256	mp3an3	$⊢ (ℜ \circ F \in MblFn \land (ℜ \circ F) : D ⟶ ℝ) \to {(ℜ \circ F)}^{-1} [\{0\}] \in dom vol$
258		mbfima	$⊢ (ℜ \circ F \in MblFn \land (ℜ \circ F) : D ⟶ ℝ) \to {(ℜ \circ F)}^{-1} [(0, +∞)] \in dom vol$
259		unmbl	$⊢ ({(ℜ \circ F)}^{-1} [\{0\}] \in dom vol \land {(ℜ \circ F)}^{-1} [(0, +∞)] \in dom vol) \to {(ℜ \circ F)}^{-1} [\{0\}] \cup {(ℜ \circ F)}^{-1} [(0, +∞)] \in dom vol$
260	257 258 259	syl2anc	$⊢ (ℜ \circ F \in MblFn \land (ℜ \circ F) : D ⟶ ℝ) \to {(ℜ \circ F)}^{-1} [\{0\}] \cup {(ℜ \circ F)}^{-1} [(0, +∞)] \in dom vol$
261	255 196 260	syl2anc	$⊢ φ \to {(ℜ \circ F)}^{-1} [\{0\}] \cup {(ℜ \circ F)}^{-1} [(0, +∞)] \in dom vol$
262	251 261	eqeltrid	$⊢ φ \to {(ℜ \circ F)}^{-1} [[0, +∞)] \in dom vol$
263	8	fdmd	$⊢ φ \to dom F = D$
264		mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$
265	47 264	syl	$⊢ φ \to dom F \in dom vol$
266	263 265	eqeltrrd	$⊢ φ \to D \in dom vol$
267		difmbl	$⊢ (ℝ \in dom vol \land D \in dom vol) \to ℝ ∖ D \in dom vol$
268	17 266 267	sylancr	$⊢ φ \to ℝ ∖ D \in dom vol$
269		unmbl	$⊢ ({(ℜ \circ F)}^{-1} [[0, +∞)] \in dom vol \land ℝ ∖ D \in dom vol) \to {(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D) \in dom vol$
270	262 268 269	syl2anc	$⊢ φ \to {(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D) \in dom vol$
271		fveq2	$⊢ t = x \to g (t) = g (x)$
272	271	breq2d	$⊢ t = x \to (0 \leq g (t) \leftrightarrow 0 \leq g (x))$
273	272 271	ifbieq1d	$⊢ t = x \to if (0 \leq g (t), g (t), 0) = if (0 \leq g (x), g (x), 0)$
274	273 89 179	fvmpt	$⊢ x \in ℝ \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) (x) = if (0 \leq g (x), g (x), 0)$
275	274	eqcomd	$⊢ x \in ℝ \to if (0 \leq g (x), g (x), 0) = (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) (x)$
276	275	ifeq1d	$⊢ x \in ℝ \to if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), if (0 \leq g (x), g (x), 0), 0) = if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) (x), 0)$
277	276	mpteq2ia	$⊢ (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), if (0 \leq g (x), g (x), 0), 0)) = (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) (x), 0))$
278	277	i1fres	$⊢ ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in dom \int^{1} \land {(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D) \in dom vol) \to (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), if (0 \leq g (x), g (x), 0), 0)) \in dom \int^{1}$
279		id	$⊢ (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in dom \int^{1} \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in dom \int^{1}$
280		neg1rr	$⊢ - 1 \in ℝ$
281	280	a1i	$⊢ (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in dom \int^{1} \to - 1 \in ℝ$
282	279 281	i1fmulc	$⊢ (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in dom \int^{1} \to (ℝ \times \{- 1\}) \times_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in dom \int^{1}$
283		cmmbl	$⊢ {(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D) \in dom vol \to ℝ ∖ ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)) \in dom vol$
284		ifnot	$⊢ if (\neg x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), -1 if (0 \leq g (x), g (x), 0), 0) = if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), 0, -1 if (0 \leq g (x), g (x), 0))$
285		eldif	$⊢ x \in (ℝ ∖ ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D))) \leftrightarrow (x \in ℝ \land \neg x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)))$
286	285	baibr	$⊢ x \in ℝ \to (\neg x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)) \leftrightarrow x \in (ℝ ∖ ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D))))$
287		tru	$⊢ ⊤$
288		negex	$⊢ - 1 \in V$
289	288	fconst	$⊢ (ℝ \times \{- 1\}) : ℝ ⟶ \{- 1\}$
290		ffn	$⊢ (ℝ \times \{- 1\}) : ℝ ⟶ \{- 1\} \to (ℝ \times \{- 1\}) Fn ℝ$
291	289 290	mp1i	$⊢ ⊤ \to (ℝ \times \{- 1\}) Fn ℝ$
292	102	a1i	$⊢ ⊤ \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) Fn ℝ$
293	105	a1i	$⊢ ⊤ \to ℝ \in V$
294		inidm	$⊢ ℝ \cap ℝ = ℝ$
295	288	fvconst2	$⊢ x \in ℝ \to (ℝ \times \{- 1\}) (x) = - 1$
296	295	adantl	$⊢ (⊤ \land x \in ℝ) \to (ℝ \times \{- 1\}) (x) = - 1$
297	274	adantl	$⊢ (⊤ \land x \in ℝ) \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) (x) = if (0 \leq g (x), g (x), 0)$
298	291 292 293 293 294 296 297	ofval	$⊢ (⊤ \land x \in ℝ) \to ((ℝ \times \{- 1\}) \times_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) (x) = -1 if (0 \leq g (x), g (x), 0)$
299	287 298	mpan	$⊢ x \in ℝ \to ((ℝ \times \{- 1\}) \times_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) (x) = -1 if (0 \leq g (x), g (x), 0)$
300	299	eqcomd	$⊢ x \in ℝ \to -1 if (0 \leq g (x), g (x), 0) = ((ℝ \times \{- 1\}) \times_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) (x)$
301	286 300	ifbieq1d	$⊢ x \in ℝ \to if (\neg x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), -1 if (0 \leq g (x), g (x), 0), 0) = if (x \in (ℝ ∖ ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D))), ((ℝ \times \{- 1\}) \times_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) (x), 0)$
302	284 301	eqtr3id	$⊢ x \in ℝ \to if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), 0, -1 if (0 \leq g (x), g (x), 0)) = if (x \in (ℝ ∖ ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D))), ((ℝ \times \{- 1\}) \times_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) (x), 0)$
303	302	mpteq2ia	$⊢ (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), 0, -1 if (0 \leq g (x), g (x), 0))) = (x \in ℝ ⟼ if (x \in (ℝ ∖ ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D))), ((ℝ \times \{- 1\}) \times_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) (x), 0))$
304	303	i1fres	$⊢ ((ℝ \times \{- 1\}) \times_{f} (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in dom \int^{1} \land ℝ ∖ ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)) \in dom vol) \to (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), 0, -1 if (0 \leq g (x), g (x), 0))) \in dom \int^{1}$
305	282 283 304	syl2an	$⊢ ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in dom \int^{1} \land {(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D) \in dom vol) \to (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), 0, -1 if (0 \leq g (x), g (x), 0))) \in dom \int^{1}$
306	278 305	i1fadd	$⊢ ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) \in dom \int^{1} \land {(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D) \in dom vol) \to (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), if (0 \leq g (x), g (x), 0), 0)) +_{f} (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), 0, -1 if (0 \leq g (x), g (x), 0))) \in dom \int^{1}$
307	90 270 306	syl2anr	$⊢ (φ \land g \in dom \int^{1}) \to (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), if (0 \leq g (x), g (x), 0), 0)) +_{f} (x \in ℝ ⟼ if (x \in ({(ℜ \circ F)}^{-1} [[0, +∞)] \cup (ℝ ∖ D)), 0, -1 if (0 \leq g (x), g (x), 0))) \in dom \int^{1}$
308	243 307	eqeltrrd	$⊢ (φ \land g \in dom \int^{1}) \to (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) \in dom \int^{1}$
309	159	cbvmptv	$⊢ (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) = (t \in ℝ ⟼ ℜ (if (t \in D, F (t), 0)))$
310	309 36	eqeltrid	$⊢ φ \to (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) \in 𝐿^{1}$
311	16 309	fmptd	$⊢ φ \to (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) : ℝ ⟶ ℝ$
312	310 311	jca	$⊢ φ \to ((x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) \in 𝐿^{1} \land (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) : ℝ ⟶ ℝ)$
313	312	adantr	$⊢ (φ \land g \in dom \int^{1}) \to ((x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) \in 𝐿^{1} \land (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) : ℝ ⟶ ℝ)$
314		ftc1anclem4	$⊢ ((x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) \in dom \int^{1} \land (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) \in 𝐿^{1} \land (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ \|(x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) - (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) (t)\|)) \in ℝ$
315	314	3expb	$⊢ ((x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) \in dom \int^{1} \land ((x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) \in 𝐿^{1} \land (x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) : ℝ ⟶ ℝ)) \to \int^{2} ((t \in ℝ ⟼ \|(x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) - (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) (t)\|)) \in ℝ$
316	308 313 315	syl2anc	$⊢ (φ \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ \|(x \in ℝ ⟼ ℜ (if (x \in D, F (x), 0))) (t) - (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) (t)\|)) \in ℝ$
317	176 316	eqeltrrid	$⊢ (φ \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) \in ℝ$
318	139 143 144 155 317	itg2addnc	$⊢ (φ \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) +_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) = \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|))$
319	105	a1i	$⊢ (φ \land g \in dom \int^{1}) \to ℝ \in V$
320	101	a1i	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \to if (0 \leq g (t), g (t), 0) \in V$
321		eqidd	$⊢ (φ \land g \in dom \int^{1}) \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) = (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))$
322		eqidd	$⊢ (φ \land g \in dom \int^{1}) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|) = (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)$
323	319 320 151 321 322	offval2	$⊢ (φ \land g \in dom \int^{1}) \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) +_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|) = (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)$
324	323	fveq2d	$⊢ (φ \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0)) +_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) = \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|))$
325	318 324	eqtr3d	$⊢ (φ \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) = \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|))$
326	325	adantr	$⊢ ((φ \land g \in dom \int^{1}) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \to \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) = \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|))$
327		nfv	$⊢ Ⅎ t (φ \land g \in dom \int^{1})$
328		nfcv	$⊢ \underline{Ⅎ} t g$
329		nfcv	$⊢ \underline{Ⅎ} t \circ_{r} \leq$
330		nfmpt1	$⊢ \underline{Ⅎ} t (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)$
331	328 329 330	nfbr	$⊢ Ⅎ t g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)$
332	327 331	nfan	$⊢ Ⅎ t ((φ \land g \in dom \int^{1}) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|))$
333		anass	$⊢ ((φ \land g \in dom \int^{1}) \land t \in ℝ) \leftrightarrow (φ \land (g \in dom \int^{1} \land t \in ℝ))$
334	92	ffnd	$⊢ g \in dom \int^{1} \to g Fn ℝ$
335		fvex	$⊢ \|ℜ (if (t \in D, F (t), 0))\| \in V$
336		eqid	$⊢ (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) = (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)$
337	335 336	fnmpti	$⊢ (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) Fn ℝ$
338	337	a1i	$⊢ g \in dom \int^{1} \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) Fn ℝ$
339		eqidd	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to g (t) = g (t)$
340	336	fvmpt2	$⊢ (t \in ℝ \land \|ℜ (if (t \in D, F (t), 0))\| \in V) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) (t) = \|ℜ (if (t \in D, F (t), 0))\|$
341	335 340	mpan2	$⊢ t \in ℝ \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) (t) = \|ℜ (if (t \in D, F (t), 0))\|$
342	341	adantl	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) (t) = \|ℜ (if (t \in D, F (t), 0))\|$
343	334 338 106 106 294 339 342	ofrval	$⊢ (g \in dom \int^{1} \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \land t \in ℝ) \to g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|$
344	343	3com23	$⊢ (g \in dom \int^{1} \land t \in ℝ \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \to g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|$
345	344	3expa	$⊢ ((g \in dom \int^{1} \land t \in ℝ) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \to g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|$
346	345	adantll	$⊢ ((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \to g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|$
347		resubcl	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land if (0 \leq g (t), g (t), 0) \in ℝ) \to ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0) \in ℝ$
348	15 109 347	syl2an	$⊢ (φ \land (g \in dom \int^{1} \land t \in ℝ)) \to ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0) \in ℝ$
349	348	ad2antrr	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0) \in ℝ$
350		absid	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0))\| = ℜ (if (t \in D, F (t), 0))$
351	15 350	sylan	$⊢ (φ \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0))\| = ℜ (if (t \in D, F (t), 0))$
352	351	breq2d	$⊢ (φ \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to (g (t) \leq \|ℜ (if (t \in D, F (t), 0))\| \leftrightarrow g (t) \leq ℜ (if (t \in D, F (t), 0)))$
353	352	biimpa	$⊢ ((φ \land 0 \leq ℜ (if (t \in D, F (t), 0))) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \to g (t) \leq ℜ (if (t \in D, F (t), 0))$
354	353	an32s	$⊢ ((φ \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to g (t) \leq ℜ (if (t \in D, F (t), 0))$
355	354	adantllr	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to g (t) \leq ℜ (if (t \in D, F (t), 0))$
356		breq1	$⊢ g (t) = if (0 \leq g (t), g (t), 0) \to (g (t) \leq ℜ (if (t \in D, F (t), 0)) \leftrightarrow if (0 \leq g (t), g (t), 0) \leq ℜ (if (t \in D, F (t), 0)))$
357		breq1	$⊢ 0 = if (0 \leq g (t), g (t), 0) \to (0 \leq ℜ (if (t \in D, F (t), 0)) \leftrightarrow if (0 \leq g (t), g (t), 0) \leq ℜ (if (t \in D, F (t), 0)))$
358	356 357	ifboth	$⊢ (g (t) \leq ℜ (if (t \in D, F (t), 0)) \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to if (0 \leq g (t), g (t), 0) \leq ℜ (if (t \in D, F (t), 0))$
359	355 358	sylancom	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to if (0 \leq g (t), g (t), 0) \leq ℜ (if (t \in D, F (t), 0))$
360		subge0	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land if (0 \leq g (t), g (t), 0) \in ℝ) \to (0 \leq ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0) \leftrightarrow if (0 \leq g (t), g (t), 0) \leq ℜ (if (t \in D, F (t), 0)))$
361	15 109 360	syl2an	$⊢ (φ \land (g \in dom \int^{1} \land t \in ℝ)) \to (0 \leq ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0) \leftrightarrow if (0 \leq g (t), g (t), 0) \leq ℜ (if (t \in D, F (t), 0)))$
362	361	ad2antrr	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to (0 \leq ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0) \leftrightarrow if (0 \leq g (t), g (t), 0) \leq ℜ (if (t \in D, F (t), 0)))$
363	359 362	mpbird	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to 0 \leq ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)$
364	349 363	absidd	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)\| = ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)$
365		iftrue	$⊢ 0 \leq ℜ (if (t \in D, F (t), 0)) \to if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0)) = if (0 \leq g (t), g (t), 0)$
366	365	oveq2d	$⊢ 0 \leq ℜ (if (t \in D, F (t), 0)) \to ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0)) = ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)$
367	366	fveq2d	$⊢ 0 \leq ℜ (if (t \in D, F (t), 0)) \to \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| = \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)\|$
368	367	adantl	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| = \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)\|$
369	15	ad2antrr	$⊢ ((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \to ℜ (if (t \in D, F (t), 0)) \in ℝ$
370	350	oveq1d	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0))\| - if (0 \leq g (t), g (t), 0) = ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)$
371	369 370	sylan	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0))\| - if (0 \leq g (t), g (t), 0) = ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)$
372	364 368 371	3eqtr4d	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| = \|ℜ (if (t \in D, F (t), 0))\| - if (0 \leq g (t), g (t), 0)$
373	109	renegcld	$⊢ (g \in dom \int^{1} \land t \in ℝ) \to - if (0 \leq g (t), g (t), 0) \in ℝ$
374		resubcl	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land - if (0 \leq g (t), g (t), 0) \in ℝ) \to ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0)) \in ℝ$
375	15 373 374	syl2an	$⊢ (φ \land (g \in dom \int^{1} \land t \in ℝ)) \to ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0)) \in ℝ$
376	375	ad2antrr	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0)) \in ℝ$
377	93	ad3antlr	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to g (t) \in ℝ$
378	15	ad3antrrr	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to ℜ (if (t \in D, F (t), 0)) \in ℝ$
379	15	adantr	$⊢ (φ \land (g \in dom \int^{1} \land t \in ℝ)) \to ℜ (if (t \in D, F (t), 0)) \in ℝ$
380		ltnle	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land 0 \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) < 0 \leftrightarrow \neg 0 \leq ℜ (if (t \in D, F (t), 0)))$
381	91 380	mpan2	$⊢ ℜ (if (t \in D, F (t), 0)) \in ℝ \to (ℜ (if (t \in D, F (t), 0)) < 0 \leftrightarrow \neg 0 \leq ℜ (if (t \in D, F (t), 0)))$
382		ltle	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land 0 \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) < 0 \to ℜ (if (t \in D, F (t), 0)) \leq 0)$
383	91 382	mpan2	$⊢ ℜ (if (t \in D, F (t), 0)) \in ℝ \to (ℜ (if (t \in D, F (t), 0)) < 0 \to ℜ (if (t \in D, F (t), 0)) \leq 0)$
384	381 383	sylbird	$⊢ ℜ (if (t \in D, F (t), 0)) \in ℝ \to (\neg 0 \leq ℜ (if (t \in D, F (t), 0)) \to ℜ (if (t \in D, F (t), 0)) \leq 0)$
385	384	imp	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to ℜ (if (t \in D, F (t), 0)) \leq 0$
386		absnid	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land ℜ (if (t \in D, F (t), 0)) \leq 0) \to \|ℜ (if (t \in D, F (t), 0))\| = - ℜ (if (t \in D, F (t), 0))$
387	385 386	syldan	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0))\| = - ℜ (if (t \in D, F (t), 0))$
388	387	breq2d	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to (g (t) \leq \|ℜ (if (t \in D, F (t), 0))\| \leftrightarrow g (t) \leq - ℜ (if (t \in D, F (t), 0)))$
389	388	biimpa	$⊢ ((ℜ (if (t \in D, F (t), 0)) \in ℝ \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \to g (t) \leq - ℜ (if (t \in D, F (t), 0))$
390	389	an32s	$⊢ ((ℜ (if (t \in D, F (t), 0)) \in ℝ \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to g (t) \leq - ℜ (if (t \in D, F (t), 0))$
391	379 390	sylanl1	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to g (t) \leq - ℜ (if (t \in D, F (t), 0))$
392	377 378 391	lenegcon2d	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to ℜ (if (t \in D, F (t), 0)) \leq - g (t)$
393		simpll	$⊢ ((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \to φ$
394	91	a1i	$⊢ φ \to 0 \in ℝ$
395	15 394	ltnled	$⊢ φ \to (ℜ (if (t \in D, F (t), 0)) < 0 \leftrightarrow \neg 0 \leq ℜ (if (t \in D, F (t), 0)))$
396	15 91 382	sylancl	$⊢ φ \to (ℜ (if (t \in D, F (t), 0)) < 0 \to ℜ (if (t \in D, F (t), 0)) \leq 0)$
397	395 396	sylbird	$⊢ φ \to (\neg 0 \leq ℜ (if (t \in D, F (t), 0)) \to ℜ (if (t \in D, F (t), 0)) \leq 0)$
398	397	imp	$⊢ (φ \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to ℜ (if (t \in D, F (t), 0)) \leq 0$
399	393 398	sylan	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to ℜ (if (t \in D, F (t), 0)) \leq 0$
400		negeq	$⊢ g (t) = if (0 \leq g (t), g (t), 0) \to - g (t) = - if (0 \leq g (t), g (t), 0)$
401	400	breq2d	$⊢ g (t) = if (0 \leq g (t), g (t), 0) \to (ℜ (if (t \in D, F (t), 0)) \leq - g (t) \leftrightarrow ℜ (if (t \in D, F (t), 0)) \leq - if (0 \leq g (t), g (t), 0))$
402		neg0	$⊢ - 0 = 0$
403		negeq	$⊢ 0 = if (0 \leq g (t), g (t), 0) \to - 0 = - if (0 \leq g (t), g (t), 0)$
404	402 403	eqtr3id	$⊢ 0 = if (0 \leq g (t), g (t), 0) \to 0 = - if (0 \leq g (t), g (t), 0)$
405	404	breq2d	$⊢ 0 = if (0 \leq g (t), g (t), 0) \to (ℜ (if (t \in D, F (t), 0)) \leq 0 \leftrightarrow ℜ (if (t \in D, F (t), 0)) \leq - if (0 \leq g (t), g (t), 0))$
406	401 405	ifboth	$⊢ (ℜ (if (t \in D, F (t), 0)) \leq - g (t) \land ℜ (if (t \in D, F (t), 0)) \leq 0) \to ℜ (if (t \in D, F (t), 0)) \leq - if (0 \leq g (t), g (t), 0)$
407	392 399 406	syl2anc	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to ℜ (if (t \in D, F (t), 0)) \leq - if (0 \leq g (t), g (t), 0)$
408		suble0	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℝ \land - if (0 \leq g (t), g (t), 0) \in ℝ) \to (ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0)) \leq 0 \leftrightarrow ℜ (if (t \in D, F (t), 0)) \leq - if (0 \leq g (t), g (t), 0))$
409	15 373 408	syl2an	$⊢ (φ \land (g \in dom \int^{1} \land t \in ℝ)) \to (ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0)) \leq 0 \leftrightarrow ℜ (if (t \in D, F (t), 0)) \leq - if (0 \leq g (t), g (t), 0))$
410	409	ad2antrr	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to (ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0)) \leq 0 \leftrightarrow ℜ (if (t \in D, F (t), 0)) \leq - if (0 \leq g (t), g (t), 0))$
411	407 410	mpbird	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0)) \leq 0$
412	376 411	absnidd	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0))\| = - (ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0)))$
413		subneg	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℂ \land if (0 \leq g (t), g (t), 0) \in ℂ) \to ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0)) = ℜ (if (t \in D, F (t), 0)) + if (0 \leq g (t), g (t), 0)$
414	413	negeqd	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℂ \land if (0 \leq g (t), g (t), 0) \in ℂ) \to - (ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0))) = - (ℜ (if (t \in D, F (t), 0)) + if (0 \leq g (t), g (t), 0))$
415		negdi2	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℂ \land if (0 \leq g (t), g (t), 0) \in ℂ) \to - (ℜ (if (t \in D, F (t), 0)) + if (0 \leq g (t), g (t), 0)) = - ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)$
416	414 415	eqtrd	$⊢ (ℜ (if (t \in D, F (t), 0)) \in ℂ \land if (0 \leq g (t), g (t), 0) \in ℂ) \to - (ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0))) = - ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)$
417	37 145 416	syl2an	$⊢ (φ \land (g \in dom \int^{1} \land t \in ℝ)) \to - (ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0))) = - ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)$
418	417	ad2antrr	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to - (ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0))) = - ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)$
419	412 418	eqtrd	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0))\| = - ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)$
420		iffalse	$⊢ \neg 0 \leq ℜ (if (t \in D, F (t), 0)) \to if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0)) = - if (0 \leq g (t), g (t), 0)$
421	420	oveq2d	$⊢ \neg 0 \leq ℜ (if (t \in D, F (t), 0)) \to ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0)) = ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0))$
422	421	fveq2d	$⊢ \neg 0 \leq ℜ (if (t \in D, F (t), 0)) \to \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| = \|ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0))\|$
423	422	adantl	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| = \|ℜ (if (t \in D, F (t), 0)) - (- if (0 \leq g (t), g (t), 0))\|$
424	15 386	sylan	$⊢ (φ \land ℜ (if (t \in D, F (t), 0)) \leq 0) \to \|ℜ (if (t \in D, F (t), 0))\| = - ℜ (if (t \in D, F (t), 0))$
425	398 424	syldan	$⊢ (φ \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0))\| = - ℜ (if (t \in D, F (t), 0))$
426	425	oveq1d	$⊢ (φ \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0))\| - if (0 \leq g (t), g (t), 0) = - ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)$
427	393 426	sylan	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0))\| - if (0 \leq g (t), g (t), 0) = - ℜ (if (t \in D, F (t), 0)) - if (0 \leq g (t), g (t), 0)$
428	419 423 427	3eqtr4d	$⊢ (((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \land \neg 0 \leq ℜ (if (t \in D, F (t), 0))) \to \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| = \|ℜ (if (t \in D, F (t), 0))\| - if (0 \leq g (t), g (t), 0)$
429	372 428	pm2.61dan	$⊢ ((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \to \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| = \|ℜ (if (t \in D, F (t), 0))\| - if (0 \leq g (t), g (t), 0)$
430	429	oveq2d	$⊢ ((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \to if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| = if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0))\| - if (0 \leq g (t), g (t), 0)$
431	58	recnd	$⊢ φ \to \|ℜ (if (t \in D, F (t), 0))\| \in ℂ$
432		pncan3	$⊢ (if (0 \leq g (t), g (t), 0) \in ℂ \land \|ℜ (if (t \in D, F (t), 0))\| \in ℂ) \to if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0))\| - if (0 \leq g (t), g (t), 0) = \|ℜ (if (t \in D, F (t), 0))\|$
433	145 431 432	syl2anr	$⊢ (φ \land (g \in dom \int^{1} \land t \in ℝ)) \to if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0))\| - if (0 \leq g (t), g (t), 0) = \|ℜ (if (t \in D, F (t), 0))\|$
434	433	adantr	$⊢ ((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \to if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0))\| - if (0 \leq g (t), g (t), 0) = \|ℜ (if (t \in D, F (t), 0))\|$
435	430 434	eqtrd	$⊢ ((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g (t) \leq \|ℜ (if (t \in D, F (t), 0))\|) \to if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| = \|ℜ (if (t \in D, F (t), 0))\|$
436	346 435	syldan	$⊢ ((φ \land (g \in dom \int^{1} \land t \in ℝ)) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \to if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| = \|ℜ (if (t \in D, F (t), 0))\|$
437	333 436	sylanb	$⊢ (((φ \land g \in dom \int^{1}) \land t \in ℝ) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \to if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| = \|ℜ (if (t \in D, F (t), 0))\|$
438	437	an32s	$⊢ (((φ \land g \in dom \int^{1}) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \land t \in ℝ) \to if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\| = \|ℜ (if (t \in D, F (t), 0))\|$
439	332 438	mpteq2da	$⊢ ((φ \land g \in dom \int^{1}) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \to (t \in ℝ ⟼ if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|) = (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)$
440	439	fveq2d	$⊢ ((φ \land g \in dom \int^{1}) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \to \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0) + \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) = \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|))$
441	326 440	eqtrd	$⊢ ((φ \land g \in dom \int^{1}) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \to \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) = \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|))$
442	441	breq1d	$⊢ ((φ \land g \in dom \int^{1}) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \to (\int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + Y \leftrightarrow \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + Y)$
443	442	adantllr	$⊢ (((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \to (\int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + Y \leftrightarrow \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + Y)$
444	317	adantlr	$⊢ ((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) \in ℝ$
445	68	ad2antlr	$⊢ ((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \to Y \in ℝ$
446	120	adantl	$⊢ ((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \to \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) \in ℝ$
447	444 445 446	ltadd2d	$⊢ ((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < Y \leftrightarrow \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + Y)$
448	447	adantr	$⊢ (((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < Y \leftrightarrow \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + Y)$
449		ltsubadd	$⊢ (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \in ℝ \land Y \in ℝ \land \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) \in ℝ) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) \leftrightarrow \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + Y)$
450	65 68 120 449	syl3an	$⊢ (φ \land Y \in ℝ^{+} \land g \in dom \int^{1}) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) \leftrightarrow \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + Y)$
451	450	3expa	$⊢ ((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) \leftrightarrow \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + Y)$
452	451	adantr	$⊢ (((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) \leftrightarrow \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))) + Y)$
453	443 448 452	3bitr4d	$⊢ (((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \land g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < Y \leftrightarrow \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))))$
454	453	adantrr	$⊢ (((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \land (g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \land \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y)) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < Y \leftrightarrow \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y < \int^{2} ((t \in ℝ ⟼ if (0 \leq g (t), g (t), 0))))$
455	136 454	mpbird	$⊢ (((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \land (g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \land \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y)) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < Y$
456	455	ex	$⊢ ((φ \land Y \in ℝ^{+}) \land g \in dom \int^{1}) \to ((g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \land \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < Y)$
457	456	reximdva	$⊢ (φ \land Y \in ℝ^{+}) \to (\exists g \in dom \int^{1} (g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \land \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y) \to \exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < Y)$
458		fveq1	$⊢ f = (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) \to f (t) = (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) (t)$
459	458 172	sylan9eq	$⊢ (f = (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) \land t \in ℝ) \to f (t) = if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))$
460	459	oveq2d	$⊢ (f = (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) \land t \in ℝ) \to ℜ (if (t \in D, F (t), 0)) - f (t) = ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))$
461	460	fveq2d	$⊢ (f = (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) \land t \in ℝ) \to \|ℜ (if (t \in D, F (t), 0)) - f (t)\| = \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|$
462	461	mpteq2dva	$⊢ f = (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) \to (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|) = (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)$
463	462	fveq2d	$⊢ f = (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) \to \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) = \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|))$
464	463	breq1d	$⊢ f = (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < Y \leftrightarrow \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < Y)$
465	464	rspcev	$⊢ ((x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) \in dom \int^{1} \land \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < Y) \to \exists f \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < Y$
466	465	ex	$⊢ (x \in ℝ ⟼ if (0 \leq ℜ (if (x \in D, F (x), 0)), if (0 \leq g (x), g (x), 0), - if (0 \leq g (x), g (x), 0))) \in dom \int^{1} \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < Y \to \exists f \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < Y)$
467	308 466	syl	$⊢ (φ \land g \in dom \int^{1}) \to (\int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < Y \to \exists f \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < Y)$
468	467	rexlimdva	$⊢ φ \to (\exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < Y \to \exists f \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < Y)$
469	468	adantr	$⊢ (φ \land Y \in ℝ^{+}) \to (\exists g \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - if (0 \leq ℜ (if (t \in D, F (t), 0)), if (0 \leq g (t), g (t), 0), - if (0 \leq g (t), g (t), 0))\|)) < Y \to \exists f \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < Y)$
470	457 469	syld	$⊢ (φ \land Y \in ℝ^{+}) \to (\exists g \in dom \int^{1} (g \leq_{f} (t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|) \land \neg \int^{1} (g) \leq \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0))\|)) - Y) \to \exists f \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < Y)$
471	85 470	mpd	$⊢ (φ \land Y \in ℝ^{+}) \to \exists f \in dom \int^{1} \int^{2} ((t \in ℝ ⟼ \|ℜ (if (t \in D, F (t), 0)) - f (t)\|)) < Y$

Metamath Proof Explorer

Theorem ftc1anclem5

Proof