Theorem ftc1anclem5 32659

Description: Lemma for ftc1anc 32663, 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.)

Hypotheses

Ref	Expression
ftc1anc.g	⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)
ftc1anc.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
ftc1anc.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
ftc1anc.le	⊢ (𝜑 → 𝐴 ≤ 𝐵)
ftc1anc.s	⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
ftc1anc.d	⊢ (𝜑 → 𝐷 ⊆ ℝ)
ftc1anc.i	⊢ (𝜑 → 𝐹 ∈ 𝐿1)
ftc1anc.f	⊢ (𝜑 → 𝐹:𝐷⟶ℂ)

Assertion

Ref	Expression
ftc1anclem5	⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌)

Distinct variable groups:   𝑡,𝑓,𝑥,𝐴   𝐵,𝑓,𝑡,𝑥   𝐷,𝑓,𝑡,𝑥   𝑓,𝐹,𝑡,𝑥   𝜑,𝑓,𝑡,𝑥   𝑓,𝐺   𝑓,𝑌,𝑡,𝑥

Allowed substitution hints:   𝐺(𝑥,𝑡)

Proof of Theorem ftc1anclem5

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iftrue 4042	. . . . . . . . 9 ⊢ (𝑡 ∈ ℝ → if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
2	1	mpteq2ia 4668	. . . . . . . 8 ⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0)) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
3	2	fveq2i 6106	. . . . . . 7 ⊢ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
4		ftc1anc.f	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)
5	4	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
6		0cnd 9912	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ)
7	5, 6	ifclda 4070	. . . . . . . . . . . 12 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
8	7	recld 13782	. . . . . . . . . . 11 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
9	8	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
10		ftc1anc.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
11		rembl 23115	. . . . . . . . . . . 12 ⊢ ℝ ∈ dom vol
12	11	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ∈ dom vol)
13	8	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
14		eldifn 3695	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷)
15	14	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷)
16		iffalse 4045	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = 0)
17	16	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ (¬ 𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘0))
18		re0 13740	. . . . . . . . . . . . 13 ⊢ (ℜ‘0) = 0
19	17, 18	syl6eq 2660	. . . . . . . . . . . 12 ⊢ (¬ 𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = 0)
20	15, 19	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = 0)
21		iftrue 4042	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = (𝐹‘𝑡))
22	21	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(𝐹‘𝑡)))
23	22	mpteq2ia 4668	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡)))
24	4	feqmptd 6159	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
25		ftc1anc.i	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ 𝐿1)
26	24, 25	eqeltrrd 2689	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
27	5	iblcn 23371	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1 ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ 𝐿1)))
28	26, 27	mpbid 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ 𝐿1))
29	28	simpld 474	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1)
30	23, 29	syl5eqel 2692	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ 𝐿1)
31	10, 12, 13, 20, 30	iblss2 23378	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ 𝐿1)
32	8	recnd 9947	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ)
33	32	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ)
34		eqidd 2611	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
35		absf 13925	. . . . . . . . . . . . . 14 ⊢ abs:ℂ⟶ℝ
36	35	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → abs:ℂ⟶ℝ)
37	36	feqmptd 6159	. . . . . . . . . . . 12 ⊢ (𝜑 → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
38		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑥 = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (abs‘𝑥) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
39	33, 34, 37, 38	fmptco 6303	. . . . . . . . . . 11 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
40		eqid 2610	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
41	9, 40	fmptd 6292	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ)
42		iblmbf 23340	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)
43	25, 42	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ MblFn)
44	24, 43	eqeltrrd 2689	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn)
45	5	ismbfcn2 23212	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)))
46	44, 45	mpbid 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn))
47	46	simpld 474	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn)
48	23, 47	syl5eqel 2692	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)
49	10, 12, 13, 20, 48	mbfss 23219	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)
50		ftc1anclem1 32655	. . . . . . . . . . . 12 ⊢ (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn)
51	41, 49, 50	syl2anc 691	. . . . . . . . . . 11 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn)
52	39, 51	eqeltrrd 2689	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn)
53	9, 31, 52	iblabsnc 32644	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ 𝐿1)
54	32	abscld 14023	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ)
55	54	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ)
56	32	absge0d 14031	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
57	56	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
58	55, 57	iblpos 23365	. . . . . . . . 9 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ 𝐿1 ↔ ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈ ℝ)))
59	53, 58	mpbid 221	. . . . . . . 8 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈ ℝ))
60	59	simprd 478	. . . . . . 7 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈ ℝ)
61	3, 60	syl5eqelr 2693	. . . . . 6 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ)
62		ltsubrp 11742	. . . . . 6 ⊢ (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))))
63	61, 62	sylan 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))))
64		rpre 11715	. . . . . . 7 ⊢ (𝑌 ∈ ℝ+ → 𝑌 ∈ ℝ)
65		resubcl 10224	. . . . . . 7 ⊢ (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ)
66	61, 64, 65	syl2an 493	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ)
67	61	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ)
68	66, 67	ltnled 10063	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ↔ ¬ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
69	63, 68	mpbid 221	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ¬ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))
70	54	rexrd 9968	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ*)
71		elxrge0 12152	. . . . . . . . 9 ⊢ ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ (0[,]+∞) ↔ ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ* ∧ 0 ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
72	70, 56, 71	sylanbrc 695	. . . . . . . 8 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ (0[,]+∞))
73	72	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ (0[,]+∞))
74		eqid 2610	. . . . . . 7 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
75	73, 74	fmptd 6292	. . . . . 6 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))):ℝ⟶(0[,]+∞))
76	75	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))):ℝ⟶(0[,]+∞))
77	66	rexrd 9968	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ*)
78		itg2leub 23307	. . . . 5 ⊢ (((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))):ℝ⟶(0[,]+∞) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ*) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))))
79	76, 77, 78	syl2anc 691	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))))
80	69, 79	mtbid 313	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ¬ ∀𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
81		rexanali 2981	. . 3 ⊢ (∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) ↔ ¬ ∀𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
82	80, 81	sylibr 223	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
83	66	ad2antrr 758	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ)
84		itg1cl 23258	. . . . . . . . 9 ⊢ (𝑔 ∈ dom ∫1 → (∫1‘𝑔) ∈ ℝ)
85	84	ad2antlr 759	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫1‘𝑔) ∈ ℝ)
86		eqid 2610	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
87	86	i1fpos 23279	. . . . . . . . . . 11 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1)
88		0re 9919	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
89		i1ff 23249	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
90	89	ffvelrnda 6267	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℝ)
91		max1 11890	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (𝑔‘𝑡) ∈ ℝ) → 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
92	88, 90, 91	sylancr 694	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
93	92	ralrimiva 2949	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
94		ax-resscn 9872	. . . . . . . . . . . . . . 15 ⊢ ℝ ⊆ ℂ
95	94	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → ℝ ⊆ ℂ)
96		fvex 6113	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔‘𝑡) ∈ V
97		c0ex 9913	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
98	96, 97	ifex 4106	. . . . . . . . . . . . . . . 16 ⊢ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V
99	98, 86	fnmpti 5935	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ
100	99	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ)
101	95, 100	0pledm 23246	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → (0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ (ℝ × {0}) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
102		reex 9906	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ V
103	102	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → ℝ ∈ V)
104	97	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ∈ V)
105		ifcl 4080	. . . . . . . . . . . . . . 15 ⊢ (((𝑔‘𝑡) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ)
106	90, 88, 105	sylancl 693	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ)
107		fconstmpt 5085	. . . . . . . . . . . . . . 15 ⊢ (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)
108	107	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0))
109		eqidd 2611	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
110	103, 104, 106, 108, 109	ofrfval2 6813	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → ((ℝ × {0}) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
111	101, 110	bitrd 267	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → (0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
112	93, 111	mpbird 246	. . . . . . . . . . 11 ⊢ (𝑔 ∈ dom ∫1 → 0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
113		itg2itg1 23309	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ 0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
114	87, 112, 113	syl2anc 691	. . . . . . . . . 10 ⊢ (𝑔 ∈ dom ∫1 → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
115		itg1cl 23258	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
116	87, 115	syl 17	. . . . . . . . . 10 ⊢ (𝑔 ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
117	114, 116	eqeltrd 2688	. . . . . . . . 9 ⊢ (𝑔 ∈ dom ∫1 → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
118	117	ad2antlr 759	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
119		ltnle 9996	. . . . . . . . . 10 ⊢ ((((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ ∧ (∫1‘𝑔) ∈ ℝ) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔) ↔ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
120	66, 84, 119	syl2an 493	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔) ↔ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
121	120	biimpar 501	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔))
122		max2 11892	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (𝑔‘𝑡) ∈ ℝ) → (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
123	88, 90, 122	sylancr 694	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
124	123	ralrimiva 2949	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → ∀𝑡 ∈ ℝ (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
125	89	feqmptd 6159	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 = (𝑡 ∈ ℝ ↦ (𝑔‘𝑡)))
126	103, 90, 106, 125, 109	ofrfval2 6813	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → (𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
127	124, 126	mpbird 246	. . . . . . . . . . 11 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
128		itg1le 23286	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ dom ∫1 ∧ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) → (∫1‘𝑔) ≤ (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
129	87, 127, 128	mpd3an23 1418	. . . . . . . . . 10 ⊢ (𝑔 ∈ dom ∫1 → (∫1‘𝑔) ≤ (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
130	129, 114	breqtrrd 4611	. . . . . . . . 9 ⊢ (𝑔 ∈ dom ∫1 → (∫1‘𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
131	130	ad2antlr 759	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫1‘𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
132	83, 85, 118, 121, 131	ltletrd 10076	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
133	132	adantrl 748	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ (𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
134		i1fmbf 23248	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ MblFn)
135	87, 134	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ MblFn)
136	135	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ MblFn)
137		elrege0 12149	. . . . . . . . . . . . . . . . 17 ⊢ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
138	106, 92, 137	sylanbrc 695	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ (0[,)+∞))
139	138, 86	fmptd 6292	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)):ℝ⟶(0[,)+∞))
140	139	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)):ℝ⟶(0[,)+∞))
141	117	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
142	106	recnd 9947	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ)
143	142	negcld 10258	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ)
144	142, 143	ifcld 4081	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℂ)
145		subcl 10159	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℂ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℂ)
146	32, 144, 145	syl2an 493	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℂ)
147	146	anassrs 678	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℂ)
148	147	abscld 14023	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈ ℝ)
149	147	absge0d 14031	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))
150		elrege0 12149	. . . . . . . . . . . . . . . 16 ⊢ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈ (0[,)+∞) ↔ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈ ℝ ∧ 0 ≤ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))
151	148, 149, 150	sylanbrc 695	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈ (0[,)+∞))
152		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))
153	151, 152	fmptd 6292	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))):ℝ⟶(0[,)+∞))
154		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑡 → (𝑥 ∈ 𝐷 ↔ 𝑡 ∈ 𝐷))
155		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑡 → (𝐹‘𝑥) = (𝐹‘𝑡))
156	154, 155	ifbieq1d 4059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
157	156	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑡 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
158		eqid 2610	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))
159		fvex 6113	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V
160	157, 158, 159	fvmpt 6191	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
161	157	breq2d 4595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
162		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡))
163	162	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑡 → (0 ≤ (𝑔‘𝑥) ↔ 0 ≤ (𝑔‘𝑡)))
164	163, 162	ifbieq1d 4059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
165	164	negeqd 10154	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
166	161, 164, 165	ifbieq12d 4063	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑡 → if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
167		eqid 2610	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
168		negex 10158	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V
169	98, 168	ifex 4106	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ V
170	166, 167, 169	fvmpt 6191	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
171	160, 170	oveq12d 6567	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ ℝ → (((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
172	171	fveq2d 6107	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ ℝ → (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))
173	172	mpteq2ia 4668	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))
174	173	fveq2i 6106	. . . . . . . . . . . . . . 15 ⊢ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))
175	102	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℝ ∈ V)
176		fvex 6113	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔‘𝑥) ∈ V
177	176, 97	ifex 4106	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ V
178	177, 97	ifex 4106	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) ∈ V
179	178	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) ∈ V)
180		ovex 6577	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) ∈ V
181	97, 180	ifex 4106	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ V
182	181	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ V)
183		ffn 5958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹:𝐷⟶ℂ → 𝐹 Fn 𝐷)
184		frn 5966	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹:𝐷⟶ℂ → ran 𝐹 ⊆ ℂ)
185		ref 13700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ℜ:ℂ⟶ℝ
186		ffn 5958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ℜ:ℂ⟶ℝ → ℜ Fn ℂ)
187	185, 186	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℜ Fn ℂ
188		fnco 5913	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℜ Fn ℂ ∧ 𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘ 𝐹) Fn 𝐷)
189	187, 188	mp3an1 1403	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘ 𝐹) Fn 𝐷)
190	183, 184, 189	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹:𝐷⟶ℂ → (ℜ ∘ 𝐹) Fn 𝐷)
191		elpreima 6245	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℜ ∘ 𝐹) Fn 𝐷 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))))
192	4, 190, 191	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))))
193		fco 5971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((ℜ:ℂ⟶ℝ ∧ 𝐹:𝐷⟶ℂ) → (ℜ ∘ 𝐹):𝐷⟶ℝ)
194	185, 4, 193	sylancr 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (ℜ ∘ 𝐹):𝐷⟶ℝ)
195	194	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ)
196	195	biantrurd 528	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ ∘ 𝐹)‘𝑥))))
197		elrege0 12149	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ ∘ 𝐹)‘𝑥)))
198	196, 197	syl6bbr 277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)))
199		fvco3 6185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹‘𝑥)))
200	4, 199	sylan 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹‘𝑥)))
201	200	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥))))
202	198, 201	bitr3d 269	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥))))
203	202	pm5.32da 671	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥)))))
204	192, 203	bitrd 267	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥)))))
205	204	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥)))))
206		0le0 10987	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ≤ 0
207	206, 18	breqtrri 4610	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 ≤ (ℜ‘0)
208	207	biantru 525	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑥 ∈ 𝐷 ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0)))
209		eldif 3550	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝐷))
210	209	baibr 943	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ → (¬ 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (ℝ ∖ 𝐷)))
211	208, 210	syl5rbbr 274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0))))
212	211	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0))))
213	205, 212	orbi12d 742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)) ↔ ((𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))) ∨ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0)))))
214		elun 3715	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)))
215		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥) → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘(𝐹‘𝑥)))
216	215	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥) → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥))))
217		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘0))
218	217	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0 → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘0)))
219	216, 218	elimif 4072	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ ((𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))) ∨ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0))))
220	213, 214, 219	3bitr4g 302	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ 0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))))
221	220	ifbid 4058	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0))
222	221	mpteq2dva 4672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)))
223	220	ifbid 4058	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))
224	223	mpteq2dva 4672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))))
225	175, 179, 182, 222, 224	offval2 6812	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) = (𝑥 ∈ ℝ ↦ (if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) + if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))))
226		ovif12 6637	. . . . . . . . . . . . . . . . . . . 20 ⊢ (if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) + if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), (if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) + 0), (0 + (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))
227	89	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ∈ ℝ)
228	227	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ∈ ℂ)
229		0cn 9911	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℂ
230		ifcl 4080	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔‘𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ)
231	228, 229, 230	sylancl 693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ)
232	231	addid1d 10115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) + 0) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
233	231	mulm1d 10361	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
234	233	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (0 + (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = (0 + -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
235	231	negcld 10258	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ)
236	235	addid2d 10116	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (0 + -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
237	234, 236	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (0 + (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
238	232, 237	ifeq12d 4056	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), (if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) + 0), (0 + (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
239	226, 238	syl5eq 2656	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) + if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
240	239	mpteq2dva 4672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ dom ∫1 → (𝑥 ∈ ℝ ↦ (if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) + if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))
241	225, 240	sylan9eq 2664	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))
242		0xr 9965	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ*
243		pnfxr 9971	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ +∞ ∈ ℝ*
244		0ltpnf 11832	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 < +∞
245		snunioo 12169	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞) → ({0} ∪ (0(,)+∞)) = (0[,)+∞))
246	242, 243, 244, 245	mp3an 1416	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({0} ∪ (0(,)+∞)) = (0[,)+∞)
247	246	imaeq2i 5383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) = (◡(ℜ ∘ 𝐹) “ (0[,)+∞))
248		imaundi 5464	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) = ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞)))
249	247, 248	eqtr3i 2634	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) = ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞)))
250		ismbfcn 23204	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝐷⟶ℂ → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
251	4, 250	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
252	43, 251	mpbid 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn))
253	252	simpld 474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℜ ∘ 𝐹) ∈ MblFn)
254		mbfimasn 23207	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ ∧ 0 ∈ ℝ) → (◡(ℜ ∘ 𝐹) “ {0}) ∈ dom vol)
255	88, 254	mp3an3 1405	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (◡(ℜ ∘ 𝐹) “ {0}) ∈ dom vol)
256		mbfima 23205	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (◡(ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom vol)
257		unmbl 23112	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((◡(ℜ ∘ 𝐹) “ {0}) ∈ dom vol ∧ (◡(ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
258	255, 256, 257	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
259	253, 194, 258	syl2anc 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
260	249, 259	syl5eqel 2692	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol)
261		fdm 5964	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹:𝐷⟶ℂ → dom 𝐹 = 𝐷)
262	4, 261	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom 𝐹 = 𝐷)
263		mbfdm 23201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
264	43, 263	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom 𝐹 ∈ dom vol)
265	262, 264	eqeltrrd 2689	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐷 ∈ dom vol)
266		difmbl 23118	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℝ ∈ dom vol ∧ 𝐷 ∈ dom vol) → (ℝ ∖ 𝐷) ∈ dom vol)
267	11, 265, 266	sylancr 694	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℝ ∖ 𝐷) ∈ dom vol)
268		unmbl 23112	. . . . . . . . . . . . . . . . . . 19 ⊢ (((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol ∧ (ℝ ∖ 𝐷) ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol)
269	260, 267, 268	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol)
270		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑥 → (𝑔‘𝑡) = (𝑔‘𝑥))
271	270	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑥 → (0 ≤ (𝑔‘𝑡) ↔ 0 ≤ (𝑔‘𝑥)))
272	271, 270	ifbieq1d 4059	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑥 → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
273	272, 86, 177	fvmpt 6191	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
274	273	eqcomd 2616	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥))
275	274	ifeq1d 4054	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) = if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥), 0))
276	275	mpteq2ia 4668	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥), 0))
277	276	i1fres 23278	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∈ dom ∫1)
278		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1)
279		neg1rr 11002	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -1 ∈ ℝ
280	279	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → -1 ∈ ℝ)
281	278, 280	i1fmulc 23276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → ((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ dom ∫1)
282		cmmbl 23109	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol → (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ∈ dom vol)
283		ifnot 4083	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)), 0) = if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
284		eldif 3550	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))))
285	284	baibr 943	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ 𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)))))
286		tru 1479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ⊤
287		negex 10158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ -1 ∈ V
288	287	fconst 6004	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℝ × {-1}):ℝ⟶{-1}
289		ffn 5958	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℝ × {-1}):ℝ⟶{-1} → (ℝ × {-1}) Fn ℝ)
290	288, 289	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⊤ → (ℝ × {-1}) Fn ℝ)
291	99	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⊤ → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ)
292	102	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⊤ → ℝ ∈ V)
293		inidm 3784	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℝ ∩ ℝ) = ℝ
294	287	fvconst2 6374	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ ℝ → ((ℝ × {-1})‘𝑥) = -1)
295	294	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → ((ℝ × {-1})‘𝑥) = -1)
296	273	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
297	290, 291, 292, 292, 293, 295, 296	ofval 6804	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → (((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
298	286, 297	mpan 702	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ → (((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
299	298	eqcomd 2616	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = (((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥))
300	285, 299	ifbieq1d 4059	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → if(¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)), 0) = if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0))
301	283, 300	syl5eqr 2658	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0))
302	301	mpteq2ia 4668	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0))
303	302	i1fres 23278	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ dom ∫1 ∧ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) ∈ dom ∫1)
304	281, 282, 303	syl2an 493	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) ∈ dom ∫1)
305	277, 304	i1fadd 23268	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) ∈ dom ∫1)
306	87, 269, 305	syl2anr 494	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) ∈ dom ∫1)
307	241, 306	eqeltrrd 2689	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ dom ∫1)
308	157	cbvmptv 4678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
309	308, 31	syl5eqel 2692	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1)
310	9, 308	fmptd 6292	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)
311	309, 310	jca 553	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ))
312	311	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ))
313		ftc1anclem4 32658	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))))) ∈ ℝ)
314	313	3expb 1258	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ dom ∫1 ∧ ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))))) ∈ ℝ)
315	307, 312, 314	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))))) ∈ ℝ)
316	174, 315	syl5eqelr 2693	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) ∈ ℝ)
317	136, 140, 141, 153, 316	itg2addnc 32634	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))))
318	102	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ℝ ∈ V)
319	98	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V)
320		eqidd 2611	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
321		eqidd 2611	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))
322	318, 319, 148, 320, 321	offval2 6812	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) = (𝑡 ∈ ℝ ↦ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))))
323	322	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))))
324	317, 323	eqtr3d 2646	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))))
325	324	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))))
326		nfv 1830	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑔 ∈ dom ∫1)
327		nfcv 2751	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡𝑔
328		nfcv 2751	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡 ∘𝑟 ≤
329		nfmpt1 4675	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
330	327, 328, 329	nfbr 4629	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
331	326, 330	nfan 1816	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
332		anass 679	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ↔ (𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)))
333		ffn 5958	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔:ℝ⟶ℝ → 𝑔 Fn ℝ)
334	89, 333	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 Fn ℝ)
335		fvex 6113	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ V
336	335, 74	fnmpti 5935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) Fn ℝ
337	336	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) Fn ℝ)
338		eqidd 2611	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) = (𝑔‘𝑡))
339	74	fvmpt2 6200	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ V) → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
340	335, 339	mpan2 703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ℝ → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
341	340	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
342	334, 337, 103, 103, 293, 338, 341	ofrval 6805	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
343	342	3com23 1263	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
344	343	3expa 1257	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
345	344	adantll 746	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
346		resubcl 10224	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
347	8, 106, 346	syl2an 493	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
348	347	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
349		absid 13884	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
350	8, 349	sylan 487	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
351	350	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
352	351	biimpa 500	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
353	352	an32s 842	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
354	353	adantllr 751	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
355		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
356		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
357	355, 356	ifboth 4074	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
358	354, 357	sylancom 698	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
359		subge0 10420	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → (0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
360	8, 106, 359	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
361	360	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
362	358, 361	mpbird 246	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → 0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
363	348, 362	absidd 14009	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
364		iftrue 4042	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
365	364	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
366	365	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
367	366	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
368	8	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
369	349	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
370	368, 369	sylan 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
371	363, 367, 370	3eqtr4d 2654	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
372	106	renegcld 10336	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ)
373		resubcl 10224	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
374	8, 372, 373	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
375	374	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
376	90	ad3antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ∈ ℝ)
377	8	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
378	8	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
379		ltnle 9996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
380	88, 379	mpan2 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
381		ltle 10005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
382	88, 381	mpan2 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
383	380, 382	sylbird 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ → (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
384	383	imp 444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)
385		absnid 13886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
386	384, 385	syldan 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
387	386	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
388	387	biimpa 500	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
389	388	an32s 842	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
390	378, 389	sylanl1 680	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
391	376, 377, 390	lenegcon2d 10489	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡))
392		simpll 786	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → 𝜑)
393	88	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 0 ∈ ℝ)
394	8, 393	ltnled 10063	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
395	8, 88, 381	sylancl 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
396	394, 395	sylbird 249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
397	396	imp 444	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)
398	392, 397	sylan 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)
399		negeq 10152	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → -(𝑔‘𝑡) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
400	399	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
401		neg0 10206	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ -0 = 0
402		negeq 10152	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → -0 = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
403	401, 402	syl5eqr 2658	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → 0 = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
404	403	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
405	400, 404	ifboth 4074	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡) ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
406	391, 398, 405	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
407		suble0 10421	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
408	8, 372, 407	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
409	408	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
410	406, 409	mpbird 246	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0)
411	375, 410	absnidd 14000	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
412		subneg 10209	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
413	412	negeqd 10154	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
414		negdi2 10218	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
415	413, 414	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
416	32, 142, 415	syl2an 493	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
417	416	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
418	411, 417	eqtrd 2644	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
419		iffalse 4045	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
420	419	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
421	420	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
422	421	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
423	8, 385	sylan 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
424	397, 423	syldan 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
425	424	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
426	392, 425	sylan 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
427	418, 422, 426	3eqtr4d 2654	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
428	371, 427	pm2.61dan 828	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
429	428	oveq2d 6565	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
430	54	recnd 9947	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ)
431		pncan3 10168	. . . . . . . . . . . . . . . . . . 19 ⊢ ((if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ ∧ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
432	142, 430, 431	syl2anr 494	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
433	432	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
434	429, 433	eqtrd 2644	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
435	345, 434	syldan 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
436	332, 435	sylanb 488	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
437	436	an32s 842	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∧ 𝑡 ∈ ℝ) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
438	331, 437	mpteq2da 4671	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑡 ∈ ℝ ↦ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
439	438	fveq2d 6107	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (∫2‘(𝑡 ∈ ℝ ↦ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))))
440	325, 439	eqtrd 2644	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))))
441	440	breq1d 4593	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌)))
442	441	adantllr 751	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌)))
443	316	adantlr 747	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) ∈ ℝ)
444	64	ad2antlr 759	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → 𝑌 ∈ ℝ)
445	117	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
446	443, 444, 445	ltadd2d 10072	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 ↔ ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌)))
447	446	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 ↔ ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌)))
448		ltsubadd 10377	. . . . . . . . . . 11 ⊢ (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌)))
449	61, 64, 117, 448	syl3an 1360	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+ ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌)))
450	449	3expa 1257	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌)))
451	450	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌)))
452	442, 447, 451	3bitr4d 299	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 ↔ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))
453	452	adantrr 749	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ (𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 ↔ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))
454	133, 453	mpbird 246	. . . . 5 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ (𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌)
455	454	ex 449	. . . 4 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → ((𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌))
456	455	reximdva 3000	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌))
457		fveq1 6102	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) → (𝑓‘𝑡) = ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))
458	457, 170	sylan9eq 2664	. . . . . . . . . . . . 13 ⊢ ((𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
459	458	oveq2d 6565	. . . . . . . . . . . 12 ⊢ ((𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
460	459	fveq2d 6107	. . . . . . . . . . 11 ⊢ ((𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))
461	460	mpteq2dva 4672	. . . . . . . . . 10 ⊢ (𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))
462	461	fveq2d 6107	. . . . . . . . 9 ⊢ (𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))))
463	462	breq1d 4593	. . . . . . . 8 ⊢ (𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌 ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌))
464	463	rspcev 3282	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ dom ∫1 ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌)
465	464	ex 449	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ dom ∫1 → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌))
466	307, 465	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌))
467	466	rexlimdva 3013	. . . 4 ⊢ (𝜑 → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌))
468	467	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌))
469	456, 468	syld 46	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌))
470	82, 469	mpd 15	1 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475  ⊤wtru 1476   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ⊆ wss 3540  ifcif 4036  {csn 4125   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  ^◡ccnv 5037  dom cdm 5038  ran crn 5039   “ cima 5041   ∘ ccom 5042   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ∘_𝑓 cof 6793   ∘_𝑟 cofr 6794  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  +∞cpnf 9950  ℝ^*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145  -cneg 10146  ℝ⁺crp 11708  (,)cioo 12046  [,)cico 12048  [,]cicc 12049  ℜcre 13685  ℑcim 13686  abscabs 13822  volcvol 23039  MblFncmbf 23189  ∫₁citg1 23190  ∫₂citg2 23191  𝐿¹cibl 23192  ∫citg 23193  0_𝑝c0p 23242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-ofr 6796  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-rest 15906  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-cmp 21000  df-ovol 23040  df-vol 23041  df-mbf 23194  df-itg1 23195  df-itg2 23196  df-ibl 23197  df-0p 23243

This theorem is referenced by:  ftc1anclem6  32660