Theorem ftc1anclem5 37055

Description: Lemma for ftc1anc 37059, 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 4526	. . . . . . . . 9 ⊢ (𝑡 ∈ ℝ → if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
2	1	mpteq2ia 5241	. . . . . . . 8 ⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0)) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
3	2	fveq2i 6884	. . . . . . 7 ⊢ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
4		ftc1anc.f	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)
5	4	ffvelcdmda 7076	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
6		0cnd 11204	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ)
7	5, 6	ifclda 4555	. . . . . . . . . . . 12 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
8	7	recld 15138	. . . . . . . . . . 11 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
9	8	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
10		ftc1anc.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
11		rembl 25391	. . . . . . . . . . . 12 ⊢ ℝ ∈ dom vol
12	11	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ∈ dom vol)
13	8	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
14		eldifn 4119	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷)
15	14	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷)
16		iffalse 4529	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = 0)
17	16	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ (¬ 𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘0))
18		re0 15096	. . . . . . . . . . . . 13 ⊢ (ℜ‘0) = 0
19	17, 18	eqtrdi 2780	. . . . . . . . . . . 12 ⊢ (¬ 𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = 0)
20	15, 19	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = 0)
21		iftrue 4526	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = (𝐹‘𝑡))
22	21	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(𝐹‘𝑡)))
23	22	mpteq2ia 5241	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡)))
24	4	feqmptd 6950	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
25		ftc1anc.i	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ 𝐿1)
26	24, 25	eqeltrrd 2826	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
27	5	iblcn 25650	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1 ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ 𝐿1)))
28	26, 27	mpbid 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ 𝐿1))
29	28	simpld 494	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1)
30	23, 29	eqeltrid 2829	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ 𝐿1)
31	10, 12, 13, 20, 30	iblss2 25657	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ 𝐿1)
32	8	recnd 11239	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ)
33	32	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ)
34		eqidd 2725	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
35		absf 15281	. . . . . . . . . . . . . 14 ⊢ abs:ℂ⟶ℝ
36	35	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → abs:ℂ⟶ℝ)
37	36	feqmptd 6950	. . . . . . . . . . . 12 ⊢ (𝜑 → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
38		fveq2 6881	. . . . . . . . . . . 12 ⊢ (𝑥 = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (abs‘𝑥) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
39	33, 34, 37, 38	fmptco 7119	. . . . . . . . . . 11 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
40	9	fmpttd 7106	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ)
41		iblmbf 25619	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)
42	25, 41	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ MblFn)
43	24, 42	eqeltrrd 2826	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn)
44	5	ismbfcn2 25489	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)))
45	43, 44	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn))
46	45	simpld 494	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn)
47	23, 46	eqeltrid 2829	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)
48	10, 12, 13, 20, 47	mbfss 25497	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)
49		ftc1anclem1 37051	. . . . . . . . . . . 12 ⊢ (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn)
50	40, 48, 49	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn)
51	39, 50	eqeltrrd 2826	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn)
52	9, 31, 51	iblabsnc 37042	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ 𝐿1)
53	32	abscld 15380	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ)
54	53	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ)
55	32	absge0d 15388	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
56	55	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
57	54, 56	iblpos 25644	. . . . . . . . 9 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ 𝐿1 ↔ ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈ ℝ)))
58	52, 57	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈ ℝ))
59	58	simprd 495	. . . . . . 7 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈ ℝ)
60	3, 59	eqeltrrid 2830	. . . . . 6 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ)
61		ltsubrp 13007	. . . . . 6 ⊢ (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))))
62	60, 61	sylan 579	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))))
63		rpre 12979	. . . . . . 7 ⊢ (𝑌 ∈ ℝ+ → 𝑌 ∈ ℝ)
64		resubcl 11521	. . . . . . 7 ⊢ (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ)
65	60, 63, 64	syl2an 595	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ)
66	60	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ)
67	65, 66	ltnled 11358	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ↔ ¬ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
68	62, 67	mpbid 231	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ¬ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))
69	53	rexrd 11261	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ*)
70		elxrge0 13431	. . . . . . . . 9 ⊢ ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ (0[,]+∞) ↔ ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ* ∧ 0 ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
71	69, 55, 70	sylanbrc 582	. . . . . . . 8 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ (0[,]+∞))
72	71	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ (0[,]+∞))
73	72	fmpttd 7106	. . . . . 6 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))):ℝ⟶(0[,]+∞))
74	73	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))):ℝ⟶(0[,]+∞))
75	65	rexrd 11261	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ*)
76		itg2leub 25586	. . . . 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 583	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))))
78	68, 77	mtbid 324	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ¬ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
79		rexanali 3094	. . 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 233	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
81	65	ad2antrr 723	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ)
82		itg1cl 25536	. . . . . . . . 9 ⊢ (𝑔 ∈ dom ∫1 → (∫1‘𝑔) ∈ ℝ)
83	82	ad2antlr 724	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫1‘𝑔) ∈ ℝ)
84		eqid 2724	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
85	84	i1fpos 25558	. . . . . . . . . . 11 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1)
86		0re 11213	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
87		i1ff 25527	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
88	87	ffvelcdmda 7076	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℝ)
89		max1 13161	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (𝑔‘𝑡) ∈ ℝ) → 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
90	86, 88, 89	sylancr 586	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
91	90	ralrimiva 3138	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
92		ax-resscn 11163	. . . . . . . . . . . . . . 15 ⊢ ℝ ⊆ ℂ
93	92	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → ℝ ⊆ ℂ)
94		fvex 6894	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔‘𝑡) ∈ V
95		c0ex 11205	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
96	94, 95	ifex 4570	. . . . . . . . . . . . . . . 16 ⊢ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V
97	96, 84	fnmpti 6683	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ
98	97	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ)
99	93, 98	0pledm 25524	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → (0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ (ℝ × {0}) ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
100		reex 11197	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ V
101	100	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → ℝ ∈ V)
102	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ∈ V)
103		ifcl 4565	. . . . . . . . . . . . . . 15 ⊢ (((𝑔‘𝑡) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ)
104	88, 86, 103	sylancl 585	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ)
105		fconstmpt 5728	. . . . . . . . . . . . . . 15 ⊢ (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)
106	105	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0))
107		eqidd 2725	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
108	101, 102, 104, 106, 107	ofrfval2 7684	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → ((ℝ × {0}) ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
109	99, 108	bitrd 279	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → (0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
110	91, 109	mpbird 257	. . . . . . . . . . 11 ⊢ (𝑔 ∈ dom ∫1 → 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
111		itg2itg1 25588	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
112	85, 110, 111	syl2anc 583	. . . . . . . . . 10 ⊢ (𝑔 ∈ dom ∫1 → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
113		itg1cl 25536	. . . . . . . . . . 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 2825	. . . . . . . . 9 ⊢ (𝑔 ∈ dom ∫1 → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
116	115	ad2antlr 724	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
117		ltnle 11290	. . . . . . . . . 10 ⊢ ((((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ ∧ (∫1‘𝑔) ∈ ℝ) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔) ↔ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
118	65, 82, 117	syl2an 595	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔) ↔ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
119	118	biimpar 477	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔))
120		max2 13163	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (𝑔‘𝑡) ∈ ℝ) → (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
121	86, 88, 120	sylancr 586	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
122	121	ralrimiva 3138	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → ∀𝑡 ∈ ℝ (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
123	87	feqmptd 6950	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 = (𝑡 ∈ ℝ ↦ (𝑔‘𝑡)))
124	101, 88, 104, 123, 107	ofrfval2 7684	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → (𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
125	122, 124	mpbird 257	. . . . . . . . . . 11 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
126		itg1le 25565	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ dom ∫1 ∧ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) → (∫1‘𝑔) ≤ (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
127	85, 125, 126	mpd3an23 1459	. . . . . . . . . 10 ⊢ (𝑔 ∈ dom ∫1 → (∫1‘𝑔) ≤ (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
128	127, 112	breqtrrd 5166	. . . . . . . . 9 ⊢ (𝑔 ∈ dom ∫1 → (∫1‘𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
129	128	ad2antlr 724	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫1‘𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
130	81, 83, 116, 119, 129	ltletrd 11371	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
131	130	adantrl 713	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ (𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
132		i1fmbf 25526	. . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ MblFn)
135		elrege0 13428	. . . . . . . . . . . . . . . . 17 ⊢ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
136	104, 90, 135	sylanbrc 582	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ (0[,)+∞))
137	136	fmpttd 7106	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)):ℝ⟶(0[,)+∞))
138	137	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)):ℝ⟶(0[,)+∞))
139	115	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
140	104	recnd 11239	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ)
141	140	negcld 11555	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ)
142	140, 141	ifcld 4566	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℂ)
143		subcl 11456	. . . . . . . . . . . . . . . . . . 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 595	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℂ)
145	144	anassrs 467	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℂ)
146	145	abscld 15380	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈ ℝ)
147	145	absge0d 15388	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))
148		elrege0 13428	. . . . . . . . . . . . . . . 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 582	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈ (0[,)+∞))
150	149	fmpttd 7106	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))):ℝ⟶(0[,)+∞))
151		eleq1w 2808	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑡 → (𝑥 ∈ 𝐷 ↔ 𝑡 ∈ 𝐷))
152		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑡 → (𝐹‘𝑥) = (𝐹‘𝑡))
153	151, 152	ifbieq1d 4544	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
154	153	fveq2d 6885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑡 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
155		eqid 2724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))
156		fvex 6894	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V
157	154, 155, 156	fvmpt 6988	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
158	154	breq2d 5150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
159		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡))
160	159	breq2d 5150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑡 → (0 ≤ (𝑔‘𝑥) ↔ 0 ≤ (𝑔‘𝑡)))
161	160, 159	ifbieq1d 4544	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
162	161	negeqd 11451	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
163	158, 161, 162	ifbieq12d 4548	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑡 → if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
164		eqid 2724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
165		negex 11455	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V
166	96, 165	ifex 4570	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ V
167	163, 164, 166	fvmpt 6988	. . . . . . . . . . . . . . . . . . 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 7419	. . . . . . . . . . . . . . . . . 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 6885	. . . . . . . . . . . . . . . . 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 5241	. . . . . . . . . . . . . . . 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 6884	. . . . . . . . . . . . . . 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 6894	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔‘𝑥) ∈ V
174	173, 95	ifex 4570	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ V
175	174, 95	ifex 4570	. . . . . . . . . . . . . . . . . . . 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 7434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) ∈ V
178	95, 177	ifex 4570	. . . . . . . . . . . . . . . . . . . 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 6707	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹:𝐷⟶ℂ → 𝐹 Fn 𝐷)
181		frn 6714	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹:𝐷⟶ℂ → ran 𝐹 ⊆ ℂ)
182		ref 15056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ℜ:ℂ⟶ℝ
183		ffn 6707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ℜ:ℂ⟶ℝ → ℜ Fn ℂ)
184	182, 183	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℜ Fn ℂ
185		fnco 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℜ Fn ℂ ∧ 𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘ 𝐹) Fn 𝐷)
186	184, 185	mp3an1 1444	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘ 𝐹) Fn 𝐷)
187	180, 181, 186	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹:𝐷⟶ℂ → (ℜ ∘ 𝐹) Fn 𝐷)
188		elpreima 7049	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℜ ∘ 𝐹) Fn 𝐷 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))))
189	4, 187, 188	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))))
190		fco 6731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((ℜ:ℂ⟶ℝ ∧ 𝐹:𝐷⟶ℂ) → (ℜ ∘ 𝐹):𝐷⟶ℝ)
191	182, 4, 190	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (ℜ ∘ 𝐹):𝐷⟶ℝ)
192	191	ffvelcdmda 7076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ)
193	192	biantrurd 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ ∘ 𝐹)‘𝑥))))
194		elrege0 13428	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ ∘ 𝐹)‘𝑥)))
195	193, 194	bitr4di 289	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)))
196		fvco3 6980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹‘𝑥)))
197	4, 196	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹‘𝑥)))
198	197	breq2d 5150	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥))))
199	195, 198	bitr3d 281	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥))))
200	199	pm5.32da 578	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥)))))
201	189, 200	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥)))))
202	201	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥)))))
203		eldif 3950	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝐷))
204	203	baibr 536	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ → (¬ 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (ℝ ∖ 𝐷)))
205		0le0 12310	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ≤ 0
206	205, 18	breqtrri 5165	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 ≤ (ℜ‘0)
207	206	biantru 529	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑥 ∈ 𝐷 ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0)))
208	204, 207	bitr3di 286	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0))))
209	208	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0))))
210	202, 209	orbi12d 915	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)) ↔ ((𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))) ∨ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0)))))
211		elun 4140	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)))
212		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥) → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘(𝐹‘𝑥)))
213	212	breq2d 5150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥) → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥))))
214		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘0))
215	214	breq2d 5150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0 → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘0)))
216	213, 215	elimif 4557	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ ((𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))) ∨ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0))))
217	210, 211, 216	3bitr4g 314	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ 0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))))
218	217	ifbid 4543	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0))
219	218	mpteq2dva 5238	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)))
220	217	ifbid 4543	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))
221	220	mpteq2dva 5238	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))))
222	172, 176, 179, 219, 221	offval2 7683	. . . . . . . . . . . . . . . . . 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 7500	. . . . . . . . . . . . . . . . . . . 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 7076	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ∈ ℝ)
225	224	recnd 11239	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ∈ ℂ)
226		0cn 11203	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℂ
227		ifcl 4565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔‘𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ)
228	225, 226, 227	sylancl 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ)
229	228	addridd 11411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) + 0) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
230	228	mulm1d 11663	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
231	230	oveq2d 7417	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (0 + (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = (0 + -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
232	228	negcld 11555	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ)
233	232	addlidd 11412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (0 + -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
234	231, 233	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (0 + (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
235	229, 234	ifeq12d 4541	. . . . . . . . . . . . . . . . . . . 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 2776	. . . . . . . . . . . . . . . . . . 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 5238	. . . . . . . . . . . . . . . . . 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 2784	. . . . . . . . . . . . . . . . 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 11258	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ*
240		pnfxr 11265	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ +∞ ∈ ℝ*
241		0ltpnf 13099	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 < +∞
242		snunioo 13452	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞) → ({0} ∪ (0(,)+∞)) = (0[,)+∞))
243	239, 240, 241, 242	mp3an 1457	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({0} ∪ (0(,)+∞)) = (0[,)+∞)
244	243	imaeq2i 6047	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) = (◡(ℜ ∘ 𝐹) “ (0[,)+∞))
245		imaundi 6139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) = ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞)))
246	244, 245	eqtr3i 2754	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) = ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞)))
247		ismbfcn 25480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝐷⟶ℂ → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
248	4, 247	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
249	42, 248	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn))
250	249	simpld 494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℜ ∘ 𝐹) ∈ MblFn)
251		mbfimasn 25483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ ∧ 0 ∈ ℝ) → (◡(ℜ ∘ 𝐹) “ {0}) ∈ dom vol)
252	86, 251	mp3an3 1446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (◡(ℜ ∘ 𝐹) “ {0}) ∈ dom vol)
253		mbfima 25481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (◡(ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom vol)
254		unmbl 25388	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((◡(ℜ ∘ 𝐹) “ {0}) ∈ dom vol ∧ (◡(ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
255	252, 253, 254	syl2anc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
256	250, 191, 255	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
257	246, 256	eqeltrid 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol)
258	4	fdmd 6718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom 𝐹 = 𝐷)
259		mbfdm 25477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
260	42, 259	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom 𝐹 ∈ dom vol)
261	258, 260	eqeltrrd 2826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐷 ∈ dom vol)
262		difmbl 25394	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℝ ∈ dom vol ∧ 𝐷 ∈ dom vol) → (ℝ ∖ 𝐷) ∈ dom vol)
263	11, 261, 262	sylancr 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℝ ∖ 𝐷) ∈ dom vol)
264		unmbl 25388	. . . . . . . . . . . . . . . . . . 19 ⊢ (((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol ∧ (ℝ ∖ 𝐷) ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol)
265	257, 263, 264	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol)
266		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑥 → (𝑔‘𝑡) = (𝑔‘𝑥))
267	266	breq2d 5150	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑥 → (0 ≤ (𝑔‘𝑡) ↔ 0 ≤ (𝑔‘𝑥)))
268	267, 266	ifbieq1d 4544	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑥 → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
269	268, 84, 174	fvmpt 6988	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
270	269	eqcomd 2730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥))
271	270	ifeq1d 4539	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) = if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥), 0))
272	271	mpteq2ia 5241	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥), 0))
273	272	i1fres 25557	. . . . . . . . . . . . . . . . . . 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 12324	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -1 ∈ ℝ
276	275	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → -1 ∈ ℝ)
277	274, 276	i1fmulc 25555	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → ((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ dom ∫1)
278		cmmbl 25385	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol → (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ∈ dom vol)
279		ifnot 4572	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)), 0) = if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
280		eldif 3950	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))))
281	280	baibr 536	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ 𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)))))
282		tru 1537	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ⊤
283		negex 11455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ -1 ∈ V
284	283	fconst 6767	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℝ × {-1}):ℝ⟶{-1}
285		ffn 6707	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4210	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℝ ∩ ℝ) = ℝ
290	283	fvconst2 7197	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ ℝ → ((ℝ × {-1})‘𝑥) = -1)
291	290	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → ((ℝ × {-1})‘𝑥) = -1)
292	269	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
293	286, 287, 288, 288, 289, 291, 292	ofval 7674	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
294	282, 293	mpan 687	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ → (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
295	294	eqcomd 2730	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥))
296	281, 295	ifbieq1d 4544	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → if(¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)), 0) = if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0))
297	279, 296	eqtr3id 2778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0))
298	297	mpteq2ia 5241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0))
299	298	i1fres 25557	. . . . . . . . . . . . . . . . . . . 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 595	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) ∈ dom ∫1)
301	273, 300	i1fadd 25546	. . . . . . . . . . . . . . . . . 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 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) ∈ dom ∫1)
303	238, 302	eqeltrrd 2826	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ dom ∫1)
304	154	cbvmptv 5251	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
305	304, 31	eqeltrid 2829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1)
306	9, 304	fmptd 7105	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)
307	305, 306	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ))
308	307	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ))
309		ftc1anclem4 37054	. . . . . . . . . . . . . . . . 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 1117	. . . . . . . . . . . . . . . 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 583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))))) ∈ ℝ)
312	171, 311	eqeltrrid 2830	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) ∈ ℝ)
313	134, 138, 139, 150, 312	itg2addnc 37032	. . . . . . . . . . . . 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 2725	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
317		eqidd 2725	. . . . . . . . . . . . . . 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 7683	. . . . . . . . . . . . . 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 6885	. . . . . . . . . . . . 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 2766	. . . . . . . . . . . 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 480	. . . . . . . . . . 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 1909	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑔 ∈ dom ∫1)
323		nfcv 2895	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡𝑔
324		nfcv 2895	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡 ∘r ≤
325		nfmpt1 5246	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
326	323, 324, 325	nfbr 5185	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
327	322, 326	nfan 1894	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
328		anass 468	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ↔ (𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)))
329	87	ffnd 6708	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 Fn ℝ)
330		fvex 6894	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ V
331		eqid 2724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
332	330, 331	fnmpti 6683	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) Fn ℝ
333	332	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) Fn ℝ)
334		eqidd 2725	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) = (𝑔‘𝑡))
335	331	fvmpt2 6999	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ V) → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
336	330, 335	mpan2 688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ℝ → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
337	336	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
338	329, 333, 101, 101, 289, 334, 337	ofrval 7675	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
339	338	3com23 1123	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
340	339	3expa 1115	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
341	340	adantll 711	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
342		resubcl 11521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
343	8, 104, 342	syl2an 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
344	343	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
345		absid 15240	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
346	8, 345	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
347	346	breq2d 5150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
348	347	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
349	348	an32s 649	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
350	349	adantllr 716	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
351		breq1 5141	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
352		breq1 5141	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
353	351, 352	ifboth 4559	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
354	350, 353	sylancom 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
355		subge0 11724	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → (0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
356	8, 104, 355	syl2an 595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
357	356	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
358	354, 357	mpbird 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → 0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
359	344, 358	absidd 15366	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
360		iftrue 4526	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
361	360	oveq2d 7417	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
362	361	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . 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 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))))
364	8	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
365	345	oveq1d 7416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
366	364, 365	sylan 579	. . . . . . . . . . . . . . . . . . . 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 2774	. . . . . . . . . . . . . . . . . . 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 11638	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ)
369		resubcl 11521	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
370	8, 368, 369	syl2an 595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
371	370	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
372	88	ad3antlr 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ∈ ℝ)
373	8	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
374	8	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
375		ltnle 11290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
376	86, 375	mpan2 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
377		ltle 11299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
378	86, 377	mpan2 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
379	376, 378	sylbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ → (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
380	379	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)
381		absnid 15242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
382	380, 381	syldan 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
383	382	breq2d 5150	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
384	383	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
385	384	an32s 649	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
386	374, 385	sylanl1 677	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
387	372, 373, 386	lenegcon2d 11794	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡))
388		simpll 764	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → 𝜑)
389	86	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 0 ∈ ℝ)
390	8, 389	ltnled 11358	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
391	8, 86, 377	sylancl 585	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
392	390, 391	sylbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
393	392	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)
394	388, 393	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)
395		negeq 11449	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → -(𝑔‘𝑡) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
396	395	breq2d 5150	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
397		neg0 11503	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ -0 = 0
398		negeq 11449	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → -0 = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
399	397, 398	eqtr3id 2778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → 0 = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
400	399	breq2d 5150	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
401	396, 400	ifboth 4559	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡) ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
402	387, 394, 401	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
403		suble0 11725	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
404	8, 368, 403	syl2an 595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
405	404	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
406	402, 405	mpbird 257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0)
407	371, 406	absnidd 15357	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
408		subneg 11506	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
409	408	negeqd 11451	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
410		negdi2 11515	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
411	409, 410	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
412	32, 140, 411	syl2an 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
413	412	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
414	407, 413	eqtrd 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
415		iffalse 4529	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
416	415	oveq2d 7417	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
417	416	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . 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 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))))
419	8, 381	sylan 579	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
420	393, 419	syldan 590	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
421	420	oveq1d 7416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
422	388, 421	sylan 579	. . . . . . . . . . . . . . . . . . . 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 2774	. . . . . . . . . . . . . . . . . . 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 810	. . . . . . . . . . . . . . . . . 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 7417	. . . . . . . . . . . . . . . . 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 11239	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ)
427		pncan3 11465	. . . . . . . . . . . . . . . . . . 19 ⊢ ((if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ ∧ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
428	140, 426, 427	syl2anr 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
429	428	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
430	425, 429	eqtrd 2764	. . . . . . . . . . . . . . . 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 590	. . . . . . . . . . . . . . 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 580	. . . . . . . . . . . . . 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 649	. . . . . . . . . . . . 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 5236	. . . . . . . . . . . 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 6885	. . . . . . . . . . 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 2764	. . . . . . . . . 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 5148	. . . . . . . . 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 716	. . . . . . . 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 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) ∈ ℝ)
440	63	ad2antlr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → 𝑌 ∈ ℝ)
441	115	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
442	439, 440, 441	ltadd2d 11367	. . . . . . . . 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 480	. . . . . . . 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 11681	. . . . . . . . . . 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 1157	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+ ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌)))
446	445	3expa 1115	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌)))
447	446	adantr 480	. . . . . . . 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 311	. . . . . . 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 714	. . . . . 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 257	. . . . 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 412	. . . 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 3160	. . 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 6880	. . . . . . . . . . . . . 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 2784	. . . . . . . . . . . . 13 ⊢ ((𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
455	454	oveq2d 7417	. . . . . . . . . . . 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 6885	. . . . . . . . . . 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 5238	. . . . . . . . . 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 6885	. . . . . . . . 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 5148	. . . . . . . 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 3604	. . . . . . 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 412	. . . . . 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 3147	. . . 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 480	. . 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 205   ∧ wa 395   ∨ wo 844   = wceq 1533  ⊤wtru 1534   ∈ wcel 2098  ∀wral 3053  ∃wrex 3062  Vcvv 3466   ∖ cdif 3937   ∪ cun 3938   ⊆ wss 3940  ifcif 4520  {csn 4620   class class class wbr 5138   ↦ cmpt 5221   × cxp 5664  ^◡ccnv 5665  dom cdm 5666  ran crn 5667   “ cima 5669   ∘ ccom 5670   Fn wfn 6528  ⟶wf 6529  ‘cfv 6533  (class class class)co 7401   ∘_f cof 7661   ∘_r cofr 7662  ℂcc 11104  ℝcr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111  +∞cpnf 11242  ℝ^*cxr 11244   < clt 11245   ≤ cle 11246   − cmin 11441  -cneg 11442  ℝ⁺crp 12971  (,)cioo 13321  [,)cico 13323  [,]cicc 13324  ℜcre 15041  ℑcim 15042  abscabs 15178  volcvol 25314  MblFncmbf 25465  ∫₁citg1 25466  ∫₂citg2 25467  𝐿¹cibl 25468  ∫citg 25469  0_𝑝c0p 25520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-disj 5104  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-ofr 7664  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8699  df-map 8818  df-pm 8819  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-n0 12470  df-z 12556  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-sum 15630  df-rest 17367  df-topgen 17388  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-top 22718  df-topon 22735  df-bases 22771  df-cmp 23213  df-ovol 25315  df-vol 25316  df-mbf 25470  df-itg1 25471  df-itg2 25472  df-ibl 25473  df-0p 25521

This theorem is referenced by:  ftc1anclem6  37056