Theorem ftc1anclem5 38157

Description: Lemma for ftc1anc 38161, 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 4483	. . . . . . . . 9 ⊢ (𝑡 ∈ ℝ → if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
2	1	mpteq2ia 5192	. . . . . . . 8 ⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0)) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
3	2	fveq2i 6865	. . . . . . 7 ⊢ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
4		ftc1anc.f	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)
5	4	ffvelcdmda 7060	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
6		0cnd 11166	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ)
7	5, 6	ifclda 4513	. . . . . . . . . . . 12 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
8	7	recld 15212	. . . . . . . . . . 11 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
9	8	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
10		ftc1anc.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
11		rembl 25590	. . . . . . . . . . . 12 ⊢ ℝ ∈ dom vol
12	11	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ∈ dom vol)
13	8	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
14		eldifn 4083	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷)
15	14	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷)
16		iffalse 4486	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = 0)
17	16	fveq2d 6866	. . . . . . . . . . . . 13 ⊢ (¬ 𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘0))
18		re0 15170	. . . . . . . . . . . . 13 ⊢ (ℜ‘0) = 0
19	17, 18	eqtrdi 2812	. . . . . . . . . . . 12 ⊢ (¬ 𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = 0)
20	15, 19	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = 0)
21		iftrue 4483	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = (𝐹‘𝑡))
22	21	fveq2d 6866	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(𝐹‘𝑡)))
23	22	mpteq2ia 5192	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡)))
24	4	feqmptd 6930	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
25		ftc1anc.i	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ 𝐿1)
26	24, 25	eqeltrrd 2862	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
27	5	iblcn 25849	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1 ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ 𝐿1)))
28	26, 27	mpbid 234	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ 𝐿1))
29	28	simpld 498	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1)
30	23, 29	eqeltrid 2865	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ 𝐿1)
31	10, 12, 13, 20, 30	iblss2 25856	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ 𝐿1)
32	8	recnd 11204	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ)
33	32	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ)
34		eqidd 2762	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
35		absf 15356	. . . . . . . . . . . . . 14 ⊢ abs:ℂ⟶ℝ
36	35	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → abs:ℂ⟶ℝ)
37	36	feqmptd 6930	. . . . . . . . . . . 12 ⊢ (𝜑 → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
38		fveq2 6862	. . . . . . . . . . . 12 ⊢ (𝑥 = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (abs‘𝑥) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
39	33, 34, 37, 38	fmptco 7106	. . . . . . . . . . 11 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
40	9	fmpttd 7091	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ)
41		iblmbf 25817	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)
42	25, 41	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ MblFn)
43	24, 42	eqeltrrd 2862	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn)
44	5	ismbfcn2 25688	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)))
45	43, 44	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn))
46	45	simpld 498	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn)
47	23, 46	eqeltrid 2865	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)
48	10, 12, 13, 20, 47	mbfss 25696	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)
49		ftc1anclem1 38153	. . . . . . . . . . . 12 ⊢ (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn)
50	40, 48, 49	syl2anc 593	. . . . . . . . . . 11 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn)
51	39, 50	eqeltrrd 2862	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn)
52	9, 31, 51	iblabsnc 38144	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ 𝐿1)
53	32	abscld 15457	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ)
54	53	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ)
55	32	absge0d 15465	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
56	55	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
57	54, 56	iblpos 25843	. . . . . . . . 9 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ 𝐿1 ↔ ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈ ℝ)))
58	52, 57	mpbid 234	. . . . . . . 8 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈ ℝ))
59	58	simprd 499	. . . . . . 7 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈ ℝ)
60	3, 59	eqeltrrid 2866	. . . . . 6 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ)
61		ltsubrp 13025	. . . . . 6 ⊢ (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))))
62	60, 61	sylan 589	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))))
63		rpre 12996	. . . . . . 7 ⊢ (𝑌 ∈ ℝ+ → 𝑌 ∈ ℝ)
64		resubcl 11489	. . . . . . 7 ⊢ (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ)
65	60, 63, 64	syl2an 605	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ)
66	60	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ)
67	65, 66	ltnled 11324	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ↔ ¬ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
68	62, 67	mpbid 234	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ¬ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))
69	53	rexrd 11226	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ*)
70		elxrge0 13455	. . . . . . . . 9 ⊢ ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ (0[,]+∞) ↔ ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ* ∧ 0 ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
71	69, 55, 70	sylanbrc 592	. . . . . . . 8 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ (0[,]+∞))
72	71	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ (0[,]+∞))
73	72	fmpttd 7091	. . . . . 6 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))):ℝ⟶(0[,]+∞))
74	73	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))):ℝ⟶(0[,]+∞))
75	65	rexrd 11226	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ*)
76		itg2leub 25784	. . . . 5 ⊢ (((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))):ℝ⟶(0[,]+∞) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ*) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))))
77	74, 75, 76	syl2anc 593	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))))
78	68, 77	mtbid 326	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ¬ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
79		rexanali 3115	. . 3 ⊢ (∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) ↔ ¬ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
80	78, 79	sylibr 236	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
81	65	ad2antrr 736	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ)
82		itg1cl 25735	. . . . . . . . 9 ⊢ (𝑔 ∈ dom ∫1 → (∫1‘𝑔) ∈ ℝ)
83	82	ad2antlr 737	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫1‘𝑔) ∈ ℝ)
84		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
85	84	i1fpos 25756	. . . . . . . . . . 11 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1)
86		0re 11177	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
87		i1ff 25726	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
88	87	ffvelcdmda 7060	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℝ)
89		max1 13182	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (𝑔‘𝑡) ∈ ℝ) → 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
90	86, 88, 89	sylancr 596	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
91	90	ralrimiva 3153	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
92		ax-resscn 11124	. . . . . . . . . . . . . . 15 ⊢ ℝ ⊆ ℂ
93	92	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → ℝ ⊆ ℂ)
94		fvex 6875	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔‘𝑡) ∈ V
95		c0ex 11167	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
96	94, 95	ifex 4528	. . . . . . . . . . . . . . . 16 ⊢ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V
97	96, 84	fnmpti 6659	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ
98	97	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ)
99	93, 98	0pledm 25723	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → (0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ (ℝ × {0}) ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
100		reex 11158	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ V
101	100	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → ℝ ∈ V)
102	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ∈ V)
103		ifcl 4523	. . . . . . . . . . . . . . 15 ⊢ (((𝑔‘𝑡) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ)
104	88, 86, 103	sylancl 595	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ)
105		fconstmpt 5705	. . . . . . . . . . . . . . 15 ⊢ (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)
106	105	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0))
107		eqidd 2762	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
108	101, 102, 104, 106, 107	ofrfval2 7676	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → ((ℝ × {0}) ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
109	99, 108	bitrd 281	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → (0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
110	91, 109	mpbird 259	. . . . . . . . . . 11 ⊢ (𝑔 ∈ dom ∫1 → 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
111		itg2itg1 25786	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
112	85, 110, 111	syl2anc 593	. . . . . . . . . 10 ⊢ (𝑔 ∈ dom ∫1 → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
113		itg1cl 25735	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
114	85, 113	syl 17	. . . . . . . . . 10 ⊢ (𝑔 ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
115	112, 114	eqeltrd 2861	. . . . . . . . 9 ⊢ (𝑔 ∈ dom ∫1 → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
116	115	ad2antlr 737	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
117		ltnle 11256	. . . . . . . . . 10 ⊢ ((((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ ∧ (∫1‘𝑔) ∈ ℝ) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔) ↔ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
118	65, 82, 117	syl2an 605	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔) ↔ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
119	118	biimpar 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔))
120		max2 13184	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (𝑔‘𝑡) ∈ ℝ) → (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
121	86, 88, 120	sylancr 596	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
122	121	ralrimiva 3153	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → ∀𝑡 ∈ ℝ (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
123	87	feqmptd 6930	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 = (𝑡 ∈ ℝ ↦ (𝑔‘𝑡)))
124	101, 88, 104, 123, 107	ofrfval2 7676	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → (𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
125	122, 124	mpbird 259	. . . . . . . . . . 11 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
126		itg1le 25763	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ dom ∫1 ∧ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) → (∫1‘𝑔) ≤ (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
127	85, 125, 126	mpd3an23 1483	. . . . . . . . . 10 ⊢ (𝑔 ∈ dom ∫1 → (∫1‘𝑔) ≤ (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
128	127, 112	breqtrrd 5125	. . . . . . . . 9 ⊢ (𝑔 ∈ dom ∫1 → (∫1‘𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
129	128	ad2antlr 737	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫1‘𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
130	81, 83, 116, 119, 129	ltletrd 11337	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
131	130	adantrl 726	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ (𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
132		i1fmbf 25725	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ MblFn)
133	85, 132	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ MblFn)
134	133	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ MblFn)
135		elrege0 13452	. . . . . . . . . . . . . . . . 17 ⊢ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
136	104, 90, 135	sylanbrc 592	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ (0[,)+∞))
137	136	fmpttd 7091	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)):ℝ⟶(0[,)+∞))
138	137	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)):ℝ⟶(0[,)+∞))
139	115	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
140	104	recnd 11204	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ)
141	140	negcld 11523	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ)
142	140, 141	ifcld 4524	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℂ)
143		subcl 11423	. . . . . . . . . . . . . . . . . . 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))) ∈ ℂ)
144	32, 142, 143	syl2an 605	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℂ)
145	144	anassrs 471	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℂ)
146	145	abscld 15457	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈ ℝ)
147	145	absge0d 15465	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))
148		elrege0 13452	. . . . . . . . . . . . . . . 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))))))
149	146, 147, 148	sylanbrc 592	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈ (0[,)+∞))
150	149	fmpttd 7091	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))):ℝ⟶(0[,)+∞))
151		eleq1w 2844	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑡 → (𝑥 ∈ 𝐷 ↔ 𝑡 ∈ 𝐷))
152		fveq2 6862	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑡 → (𝐹‘𝑥) = (𝐹‘𝑡))
153	151, 152	ifbieq1d 4502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
154	153	fveq2d 6866	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑡 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
155		eqid 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))
156		fvex 6875	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V
157	154, 155, 156	fvmpt 6970	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
158	154	breq2d 5109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
159		fveq2 6862	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡))
160	159	breq2d 5109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑡 → (0 ≤ (𝑔‘𝑥) ↔ 0 ≤ (𝑔‘𝑡)))
161	160, 159	ifbieq1d 4502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
162	161	negeqd 11418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
163	158, 161, 162	ifbieq12d 4506	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑡 → if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
164		eqid 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
165		negex 11422	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V
166	96, 165	ifex 4528	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ V
167	163, 164, 166	fvmpt 6970	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
168	157, 167	oveq12d 7409	. . . . . . . . . . . . . . . . . 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))))
169	168	fveq2d 6866	. . . . . . . . . . . . . . . . 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)))))
170	169	mpteq2ia 5192	. . . . . . . . . . . . . . . 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)))))
171	170	fveq2i 6865	. . . . . . . . . . . . . . 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))))))
172	100	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℝ ∈ V)
173		fvex 6875	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔‘𝑥) ∈ V
174	173, 95	ifex 4528	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ V
175	174, 95	ifex 4528	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) ∈ V
176	175	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) ∈ V)
177		ovex 7424	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) ∈ V
178	95, 177	ifex 4528	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ V
179	178	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ V)
180		ffn 6686	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹:𝐷⟶ℂ → 𝐹 Fn 𝐷)
181		frn 6694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹:𝐷⟶ℂ → ran 𝐹 ⊆ ℂ)
182		ref 15130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ℜ:ℂ⟶ℝ
183		ffn 6686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ℜ:ℂ⟶ℝ → ℜ Fn ℂ)
184	182, 183	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℜ Fn ℂ
185		fnco 6634	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℜ Fn ℂ ∧ 𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘ 𝐹) Fn 𝐷)
186	184, 185	mp3an1 1468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘ 𝐹) Fn 𝐷)
187	180, 181, 186	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹:𝐷⟶ℂ → (ℜ ∘ 𝐹) Fn 𝐷)
188		elpreima 7034	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℜ ∘ 𝐹) Fn 𝐷 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))))
189	4, 187, 188	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))))
190		fco 6711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((ℜ:ℂ⟶ℝ ∧ 𝐹:𝐷⟶ℂ) → (ℜ ∘ 𝐹):𝐷⟶ℝ)
191	182, 4, 190	sylancr 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (ℜ ∘ 𝐹):𝐷⟶ℝ)
192	191	ffvelcdmda 7060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ)
193	192	biantrurd 540	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ ∘ 𝐹)‘𝑥))))
194		elrege0 13452	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ ∘ 𝐹)‘𝑥)))
195	193, 194	bitr4di 291	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)))
196		fvco3 6962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹‘𝑥)))
197	4, 196	sylan 589	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹‘𝑥)))
198	197	breq2d 5109	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥))))
199	195, 198	bitr3d 283	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥))))
200	199	pm5.32da 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥)))))
201	189, 200	bitrd 281	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥)))))
202	201	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥)))))
203		eldif 3912	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝐷))
204	203	baibr 544	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ → (¬ 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (ℝ ∖ 𝐷)))
205		0le0 12313	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ≤ 0
206	205, 18	breqtrri 5124	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 ≤ (ℜ‘0)
207	206	biantru 537	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑥 ∈ 𝐷 ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0)))
208	204, 207	bitr3di 288	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0))))
209	208	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0))))
210	202, 209	orbi12d 929	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)) ↔ ((𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))) ∨ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0)))))
211		elun 4104	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)))
212		fveq2 6862	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥) → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘(𝐹‘𝑥)))
213	212	breq2d 5109	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥) → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥))))
214		fveq2 6862	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘0))
215	214	breq2d 5109	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0 → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘0)))
216	213, 215	elimif 4515	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ ((𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))) ∨ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0))))
217	210, 211, 216	3bitr4g 316	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ 0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))))
218	217	ifbid 4501	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0))
219	218	mpteq2dva 5190	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)))
220	217	ifbid 4501	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))
221	220	mpteq2dva 5190	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))))
222	172, 176, 179, 219, 221	offval2 7675	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) = (𝑥 ∈ ℝ ↦ (if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) + if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))))
223		ovif12 7491	. . . . . . . . . . . . . . . . . . . 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))))
224	87	ffvelcdmda 7060	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ∈ ℝ)
225	224	recnd 11204	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ∈ ℂ)
226		0cn 11165	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℂ
227		ifcl 4523	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔‘𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ)
228	225, 226, 227	sylancl 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ)
229	228	addridd 11377	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) + 0) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
230	228	mulm1d 11633	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
231	230	oveq2d 7407	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (0 + (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = (0 + -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
232	228	negcld 11523	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ)
233	232	addlidd 11378	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (0 + -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
234	231, 233	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (0 + (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
235	229, 234	ifeq12d 4499	. . . . . . . . . . . . . . . . . . . 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)))
236	223, 235	eqtrid 2808	. . . . . . . . . . . . . . . . . . 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)))
237	236	mpteq2dva 5190	. . . . . . . . . . . . . . . . . 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))))
238	222, 237	sylan9eq 2816	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))
239		0xr 11223	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ*
240		pnfxr 11230	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ +∞ ∈ ℝ*
241		0ltpnf 13118	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 < +∞
242		snunioo 13476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞) → ({0} ∪ (0(,)+∞)) = (0[,)+∞))
243	239, 240, 241, 242	mp3an 1481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({0} ∪ (0(,)+∞)) = (0[,)+∞)
244	243	imaeq2i 6043	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) = (◡(ℜ ∘ 𝐹) “ (0[,)+∞))
245		imaundi 6130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) = ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞)))
246	244, 245	eqtr3i 2786	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) = ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞)))
247		ismbfcn 25679	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝐷⟶ℂ → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
248	4, 247	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
249	42, 248	mpbid 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn))
250	249	simpld 498	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℜ ∘ 𝐹) ∈ MblFn)
251		mbfimasn 25682	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ ∧ 0 ∈ ℝ) → (◡(ℜ ∘ 𝐹) “ {0}) ∈ dom vol)
252	86, 251	mp3an3 1470	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (◡(ℜ ∘ 𝐹) “ {0}) ∈ dom vol)
253		mbfima 25680	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (◡(ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom vol)
254		unmbl 25587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((◡(ℜ ∘ 𝐹) “ {0}) ∈ dom vol ∧ (◡(ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
255	252, 253, 254	syl2anc 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
256	250, 191, 255	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
257	246, 256	eqeltrid 2865	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol)
258	4	fdmd 6697	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom 𝐹 = 𝐷)
259		mbfdm 25676	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
260	42, 259	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom 𝐹 ∈ dom vol)
261	258, 260	eqeltrrd 2862	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐷 ∈ dom vol)
262		difmbl 25593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℝ ∈ dom vol ∧ 𝐷 ∈ dom vol) → (ℝ ∖ 𝐷) ∈ dom vol)
263	11, 261, 262	sylancr 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℝ ∖ 𝐷) ∈ dom vol)
264		unmbl 25587	. . . . . . . . . . . . . . . . . . 19 ⊢ (((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol ∧ (ℝ ∖ 𝐷) ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol)
265	257, 263, 264	syl2anc 593	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol)
266		fveq2 6862	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑥 → (𝑔‘𝑡) = (𝑔‘𝑥))
267	266	breq2d 5109	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑥 → (0 ≤ (𝑔‘𝑡) ↔ 0 ≤ (𝑔‘𝑥)))
268	267, 266	ifbieq1d 4502	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑥 → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
269	268, 84, 174	fvmpt 6970	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
270	269	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥))
271	270	ifeq1d 4497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) = if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥), 0))
272	271	mpteq2ia 5192	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥), 0))
273	272	i1fres 25755	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∈ dom ∫1)
274		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1)
275		neg1rr 12175	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -1 ∈ ℝ
276	275	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → -1 ∈ ℝ)
277	274, 276	i1fmulc 25753	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → ((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ dom ∫1)
278		cmmbl 25584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol → (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ∈ dom vol)
279		ifnot 4530	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)), 0) = if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
280		eldif 3912	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))))
281	280	baibr 544	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ 𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)))))
282		tru 1563	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ⊤
283		negex 11422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ -1 ∈ V
284	283	fconst 6745	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℝ × {-1}):ℝ⟶{-1}
285		ffn 6686	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℝ × {-1}):ℝ⟶{-1} → (ℝ × {-1}) Fn ℝ)
286	284, 285	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⊤ → (ℝ × {-1}) Fn ℝ)
287	97	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⊤ → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ)
288	100	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⊤ → ℝ ∈ V)
289		inidm 4176	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℝ ∩ ℝ) = ℝ
290	283	fvconst2 7183	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ ℝ → ((ℝ × {-1})‘𝑥) = -1)
291	290	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → ((ℝ × {-1})‘𝑥) = -1)
292	269	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
293	286, 287, 288, 288, 289, 291, 292	ofval 7666	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
294	282, 293	mpan 700	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ → (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
295	294	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥))
296	281, 295	ifbieq1d 4502	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → if(¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)), 0) = if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0))
297	279, 296	eqtr3id 2810	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0))
298	297	mpteq2ia 5192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0))
299	298	i1fres 25755	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ dom ∫1 ∧ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) ∈ dom ∫1)
300	277, 278, 299	syl2an 605	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) ∈ dom ∫1)
301	273, 300	i1fadd 25745	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) ∈ dom ∫1)
302	85, 265, 301	syl2anr 606	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) ∈ dom ∫1)
303	238, 302	eqeltrrd 2862	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ dom ∫1)
304	154	cbvmptv 5201	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
305	304, 31	eqeltrid 2865	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1)
306	9, 304	fmptd 7090	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)
307	305, 306	jca 519	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ))
308	307	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ))
309		ftc1anclem4 38156	. . . . . . . . . . . . . . . . 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)))‘𝑡))))) ∈ ℝ)
310	309	3expb 1132	. . . . . . . . . . . . . . . 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)))‘𝑡))))) ∈ ℝ)
311	303, 308, 310	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))))) ∈ ℝ)
312	171, 311	eqeltrrid 2866	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) ∈ ℝ)
313	134, 138, 139, 150, 312	itg2addnc 38134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∘f + (𝑡 ∈ ℝ ↦ (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))))))))
314	100	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ℝ ∈ V)
315	96	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V)
316		eqidd 2762	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
317		eqidd 2762	. . . . . . . . . . . . . . 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))))))
318	314, 315, 146, 316, 317	offval2 7675	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∘f + (𝑡 ∈ ℝ ↦ (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)))))))
319	318	fveq2d 6866	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∘f + (𝑡 ∈ ℝ ↦ (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))))))))
320	313, 319	eqtr3d 2798	. . . . . . . . . . . 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))))))))
321	320	adantr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (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))))))))
322		nfv 1933	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑔 ∈ dom ∫1)
323		nfcv 2923	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡𝑔
324		nfcv 2923	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡 ∘r ≤
325		nfmpt1 5196	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
326	323, 324, 325	nfbr 5144	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
327	322, 326	nfan 1918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
328		anass 472	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ↔ (𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)))
329	87	ffnd 6687	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 Fn ℝ)
330		fvex 6875	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ V
331		eqid 2761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
332	330, 331	fnmpti 6659	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) Fn ℝ
333	332	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) Fn ℝ)
334		eqidd 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) = (𝑔‘𝑡))
335	331	fvmpt2 6982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ V) → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
336	330, 335	mpan2 701	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ℝ → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
337	336	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
338	329, 333, 101, 101, 289, 334, 337	ofrval 7667	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
339	338	3com23 1138	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
340	339	3expa 1130	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
341	340	adantll 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
342		resubcl 11489	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
343	8, 104, 342	syl2an 605	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
344	343	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
345		absid 15314	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
346	8, 345	sylan 589	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
347	346	breq2d 5109	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
348	347	biimpa 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
349	348	an32s 662	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
350	349	adantllr 729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
351		breq1 5100	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
352		breq1 5100	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
353	351, 352	ifboth 4517	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
354	350, 353	sylancom 597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
355		subge0 11694	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → (0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
356	8, 104, 355	syl2an 605	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
357	356	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
358	354, 357	mpbird 259	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → 0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
359	344, 358	absidd 15441	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
360		iftrue 4483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
361	360	oveq2d 7407	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
362	361	fveq2d 6866	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
363	362	adantl 485	. . . . . . . . . . . . . . . . . . . 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))))
364	8	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
365	345	oveq1d 7406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
366	364, 365	sylan 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
367	359, 363, 366	3eqtr4d 2806	. . . . . . . . . . . . . . . . . . 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)))
368	104	renegcld 11608	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ)
369		resubcl 11489	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
370	8, 368, 369	syl2an 605	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
371	370	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
372	88	ad3antlr 741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ∈ ℝ)
373	8	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
374	8	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
375		ltnle 11256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
376	86, 375	mpan2 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
377		ltle 11265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
378	86, 377	mpan2 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
379	376, 378	sylbird 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ → (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
380	379	imp 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)
381		absnid 15316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
382	380, 381	syldan 600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
383	382	breq2d 5109	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
384	383	biimpa 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
385	384	an32s 662	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
386	374, 385	sylanl1 690	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
387	372, 373, 386	lenegcon2d 11764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡))
388		simpll 776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → 𝜑)
389	86	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 0 ∈ ℝ)
390	8, 389	ltnled 11324	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
391	8, 86, 377	sylancl 595	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
392	390, 391	sylbird 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
393	392	imp 410	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)
394	388, 393	sylan 589	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)
395		negeq 11416	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → -(𝑔‘𝑡) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
396	395	breq2d 5109	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
397		neg0 11471	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ -0 = 0
398		negeq 11416	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → -0 = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
399	397, 398	eqtr3id 2810	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → 0 = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
400	399	breq2d 5109	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
401	396, 400	ifboth 4517	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡) ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
402	387, 394, 401	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
403		suble0 11695	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
404	8, 368, 403	syl2an 605	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
405	404	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
406	402, 405	mpbird 259	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0)
407	371, 406	absnidd 15432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
408		subneg 11474	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
409	408	negeqd 11418	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
410		negdi2 11483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
411	409, 410	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
412	32, 140, 411	syl2an 605	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
413	412	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
414	407, 413	eqtrd 2796	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
415		iffalse 4486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
416	415	oveq2d 7407	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
417	416	fveq2d 6866	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
418	417	adantl 485	. . . . . . . . . . . . . . . . . . . 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))))
419	8, 381	sylan 589	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
420	393, 419	syldan 600	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
421	420	oveq1d 7406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
422	388, 421	sylan 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
423	414, 418, 422	3eqtr4d 2806	. . . . . . . . . . . . . . . . . . 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)))
424	367, 423	pm2.61dan 822	. . . . . . . . . . . . . . . . . 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)))
425	424	oveq2d 7407	. . . . . . . . . . . . . . . . 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))))
426	53	recnd 11204	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ)
427		pncan3 11432	. . . . . . . . . . . . . . . . . . 19 ⊢ ((if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ ∧ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
428	140, 426, 427	syl2anr 606	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
429	428	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
430	425, 429	eqtrd 2796	. . . . . . . . . . . . . . . 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))))
431	341, 430	syldan 600	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
432	328, 431	sylanb 590	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
433	432	an32s 662	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∧ 𝑡 ∈ ℝ) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
434	327, 433	mpteq2da 5189	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑡 ∈ ℝ ↦ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
435	434	fveq2d 6866	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (∫2‘(𝑡 ∈ ℝ ↦ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))))
436	321, 435	eqtrd 2796	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (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))))))
437	436	breq1d 5107	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (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))) + 𝑌)))
438	437	adantllr 729	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (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))) + 𝑌)))
439	312	adantlr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) ∈ ℝ)
440	63	ad2antlr 737	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → 𝑌 ∈ ℝ)
441	115	adantl 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
442	439, 440, 441	ltadd2d 11333	. . . . . . . . 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))) + 𝑌)))
443	442	adantr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (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))) + 𝑌)))
444		ltsubadd 11651	. . . . . . . . . . 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))) + 𝑌)))
445	60, 63, 115, 444	syl3an 1172	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+ ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌)))
446	445	3expa 1130	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌)))
447	446	adantr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌)))
448	438, 443, 447	3bitr4d 313	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (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)))))
449	448	adantrr 727	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ (𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (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)))))
450	131, 449	mpbird 259	. . . . 5 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ (𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌)
451	450	ex 416	. . . 4 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → ((𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌))
452	451	reximdva 3174	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌))
453		fveq1 6861	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) → (𝑓‘𝑡) = ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))
454	453, 167	sylan9eq 2816	. . . . . . . . . . . . 13 ⊢ ((𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
455	454	oveq2d 7407	. . . . . . . . . . . 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))))
456	455	fveq2d 6866	. . . . . . . . . . 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)))))
457	456	mpteq2dva 5190	. . . . . . . . . 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))))))
458	457	fveq2d 6866	. . . . . . . . 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)))))))
459	458	breq1d 5107	. . . . . . . 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)))))) < 𝑌))
460	459	rspcev 3580	. . . . . . 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)) − (𝑓‘𝑡))))) < 𝑌)
461	460	ex 416	. . . . . 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)) − (𝑓‘𝑡))))) < 𝑌))
462	303, 461	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)) − (𝑓‘𝑡))))) < 𝑌))
463	462	rexlimdva 3162	. . . 4 ⊢ (𝜑 → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌))
464	463	adantr 484	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌))
465	452, 464	syld 47	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌))
466	80, 465	mpd 15	1 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   = wceq 1559  ⊤wtru 1560   ∈ wcel 2141  ∀wral 3075  ∃wrex 3085  Vcvv 3453   ∖ cdif 3899   ∪ cun 3900   ⊆ wss 3902  ifcif 4477  {csn 4579   class class class wbr 5097   ↦ cmpt 5178   × cxp 5641  ^◡ccnv 5642  dom cdm 5643  ran crn 5644   “ cima 5646   ∘ ccom 5647   Fn wfn 6511  ⟶wf 6512  ‘cfv 6516  (class class class)co 7391   ∘_f cof 7653   ∘_r cofr 7654  ℂcc 11065  ℝcr 11066  0cc0 11067  1c1 11068   + caddc 11070   · cmul 11072  +∞cpnf 11207  ℝ^*cxr 11209   < clt 11210   ≤ cle 11211   − cmin 11408  -cneg 11409  ℝ⁺crp 12987  (,)cioo 13343  [,)cico 13345  [,]cicc 13346  ℜcre 15115  ℑcim 15116  abscabs 15252  volcvol 25513  MblFncmbf 25664  ∫₁citg1 25665  ∫₂citg2 25666  𝐿¹cibl 25667  ∫citg 25668  0_𝑝c0p 25719

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-inf2 9590  ax-cnex 11123  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143  ax-pre-mulgt0 11144  ax-pre-sup 11145  ax-addf 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-int 4903  df-iun 4948  df-disj 5065  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-se 5597  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-isom 6525  df-riota 7348  df-ov 7394  df-oprab 7395  df-mpo 7396  df-of 7655  df-ofr 7656  df-om 7842  df-1st 7965  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-1o 8431  df-2o 8432  df-er 8672  df-map 8804  df-pm 8805  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-fi 9351  df-sup 9382  df-inf 9383  df-oi 9452  df-dju 9853  df-card 9891  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-sub 11410  df-neg 11411  df-div 11839  df-nn 12205  df-2 12274  df-3 12275  df-4 12276  df-n0 12476  df-z 12563  df-uz 12834  df-q 12944  df-rp 12988  df-xneg 13108  df-xadd 13109  df-xmul 13110  df-ioo 13347  df-ico 13349  df-icc 13350  df-fz 13507  df-fzo 13654  df-fl 13796  df-mod 13874  df-seq 14009  df-exp 14069  df-hash 14338  df-cj 15117  df-re 15118  df-im 15119  df-sqrt 15253  df-abs 15254  df-clim 15506  df-sum 15705  df-rest 17442  df-topgen 17463  df-psmet 21404  df-xmet 21405  df-met 21406  df-bl 21407  df-mopn 21408  df-top 22942  df-topon 22959  df-bases 22994  df-cmp 23435  df-ovol 25514  df-vol 25515  df-mbf 25669  df-itg1 25670  df-itg2 25671  df-ibl 25672  df-0p 25720

This theorem is referenced by:  ftc1anclem6  38158