Theorem ftc1anclem5 37301

Description: Lemma for ftc1anc 37305, 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 4536	. . . . . . . . 9 ⊢ (𝑡 ∈ ℝ → if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
2	1	mpteq2ia 5252	. . . . . . . 8 ⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0)) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
3	2	fveq2i 6899	. . . . . . 7 ⊢ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
4		ftc1anc.f	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)
5	4	ffvelcdmda 7093	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
6		0cnd 11239	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ)
7	5, 6	ifclda 4565	. . . . . . . . . . . 12 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
8	7	recld 15177	. . . . . . . . . . 11 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
9	8	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
10		ftc1anc.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
11		rembl 25513	. . . . . . . . . . . 12 ⊢ ℝ ∈ dom vol
12	11	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ∈ dom vol)
13	8	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
14		eldifn 4124	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷)
15	14	adantl 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷)
16		iffalse 4539	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = 0)
17	16	fveq2d 6900	. . . . . . . . . . . . 13 ⊢ (¬ 𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘0))
18		re0 15135	. . . . . . . . . . . . 13 ⊢ (ℜ‘0) = 0
19	17, 18	eqtrdi 2781	. . . . . . . . . . . 12 ⊢ (¬ 𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = 0)
20	15, 19	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = 0)
21		iftrue 4536	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = (𝐹‘𝑡))
22	21	fveq2d 6900	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(𝐹‘𝑡)))
23	22	mpteq2ia 5252	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡)))
24	4	feqmptd 6966	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
25		ftc1anc.i	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ 𝐿1)
26	24, 25	eqeltrrd 2826	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
27	5	iblcn 25772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1 ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ 𝐿1)))
28	26, 27	mpbid 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ 𝐿1))
29	28	simpld 493	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1)
30	23, 29	eqeltrid 2829	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ 𝐿1)
31	10, 12, 13, 20, 30	iblss2 25779	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ 𝐿1)
32	8	recnd 11274	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ)
33	32	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ)
34		eqidd 2726	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
35		absf 15320	. . . . . . . . . . . . . 14 ⊢ abs:ℂ⟶ℝ
36	35	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → abs:ℂ⟶ℝ)
37	36	feqmptd 6966	. . . . . . . . . . . 12 ⊢ (𝜑 → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
38		fveq2 6896	. . . . . . . . . . . 12 ⊢ (𝑥 = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (abs‘𝑥) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
39	33, 34, 37, 38	fmptco 7138	. . . . . . . . . . 11 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
40	9	fmpttd 7124	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ)
41		iblmbf 25741	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)
42	25, 41	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ MblFn)
43	24, 42	eqeltrrd 2826	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn)
44	5	ismbfcn2 25611	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)))
45	43, 44	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn))
46	45	simpld 493	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn)
47	23, 46	eqeltrid 2829	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)
48	10, 12, 13, 20, 47	mbfss 25619	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)
49		ftc1anclem1 37297	. . . . . . . . . . . 12 ⊢ (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn)
50	40, 48, 49	syl2anc 582	. . . . . . . . . . 11 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn)
51	39, 50	eqeltrrd 2826	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn)
52	9, 31, 51	iblabsnc 37288	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ 𝐿1)
53	32	abscld 15419	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ)
54	53	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ)
55	32	absge0d 15427	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
56	55	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
57	54, 56	iblpos 25766	. . . . . . . . 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 494	. . . . . . 7 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈ ℝ)
60	3, 59	eqeltrrid 2830	. . . . . 6 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ)
61		ltsubrp 13045	. . . . . 6 ⊢ (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))))
62	60, 61	sylan 578	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))))
63		rpre 13017	. . . . . . 7 ⊢ (𝑌 ∈ ℝ+ → 𝑌 ∈ ℝ)
64		resubcl 11556	. . . . . . 7 ⊢ (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ)
65	60, 63, 64	syl2an 594	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ)
66	60	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ)
67	65, 66	ltnled 11393	. . . . 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 11296	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ*)
70		elxrge0 13469	. . . . . . . . 9 ⊢ ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ (0[,]+∞) ↔ ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ* ∧ 0 ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
71	69, 55, 70	sylanbrc 581	. . . . . . . 8 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ (0[,]+∞))
72	71	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ (0[,]+∞))
73	72	fmpttd 7124	. . . . . 6 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))):ℝ⟶(0[,]+∞))
74	73	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))):ℝ⟶(0[,]+∞))
75	65	rexrd 11296	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ*)
76		itg2leub 25708	. . . . 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 582	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))))
78	68, 77	mtbid 323	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ¬ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
79		rexanali 3091	. . 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 724	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ)
82		itg1cl 25658	. . . . . . . . 9 ⊢ (𝑔 ∈ dom ∫1 → (∫1‘𝑔) ∈ ℝ)
83	82	ad2antlr 725	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫1‘𝑔) ∈ ℝ)
84		eqid 2725	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
85	84	i1fpos 25680	. . . . . . . . . . 11 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1)
86		0re 11248	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
87		i1ff 25649	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
88	87	ffvelcdmda 7093	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℝ)
89		max1 13199	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (𝑔‘𝑡) ∈ ℝ) → 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
90	86, 88, 89	sylancr 585	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
91	90	ralrimiva 3135	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
92		ax-resscn 11197	. . . . . . . . . . . . . . 15 ⊢ ℝ ⊆ ℂ
93	92	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → ℝ ⊆ ℂ)
94		fvex 6909	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔‘𝑡) ∈ V
95		c0ex 11240	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
96	94, 95	ifex 4580	. . . . . . . . . . . . . . . 16 ⊢ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V
97	96, 84	fnmpti 6699	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ
98	97	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ)
99	93, 98	0pledm 25646	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → (0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ (ℝ × {0}) ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
100		reex 11231	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ V
101	100	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → ℝ ∈ V)
102	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ∈ V)
103		ifcl 4575	. . . . . . . . . . . . . . 15 ⊢ (((𝑔‘𝑡) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ)
104	88, 86, 103	sylancl 584	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ)
105		fconstmpt 5740	. . . . . . . . . . . . . . 15 ⊢ (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)
106	105	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0))
107		eqidd 2726	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
108	101, 102, 104, 106, 107	ofrfval2 7706	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → ((ℝ × {0}) ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
109	99, 108	bitrd 278	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → (0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
110	91, 109	mpbird 256	. . . . . . . . . . 11 ⊢ (𝑔 ∈ dom ∫1 → 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
111		itg2itg1 25710	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
112	85, 110, 111	syl2anc 582	. . . . . . . . . 10 ⊢ (𝑔 ∈ dom ∫1 → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
113		itg1cl 25658	. . . . . . . . . . 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 725	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
117		ltnle 11325	. . . . . . . . . 10 ⊢ ((((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ ∧ (∫1‘𝑔) ∈ ℝ) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔) ↔ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
118	65, 82, 117	syl2an 594	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔) ↔ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))
119	118	biimpar 476	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔))
120		max2 13201	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (𝑔‘𝑡) ∈ ℝ) → (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
121	86, 88, 120	sylancr 585	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
122	121	ralrimiva 3135	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → ∀𝑡 ∈ ℝ (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
123	87	feqmptd 6966	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 = (𝑡 ∈ ℝ ↦ (𝑔‘𝑡)))
124	101, 88, 104, 123, 107	ofrfval2 7706	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ dom ∫1 → (𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
125	122, 124	mpbird 256	. . . . . . . . . . 11 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
126		itg1le 25687	. . . . . . . . . . 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 5177	. . . . . . . . 9 ⊢ (𝑔 ∈ dom ∫1 → (∫1‘𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
129	128	ad2antlr 725	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫1‘𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
130	81, 83, 116, 119, 129	ltletrd 11406	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
131	130	adantrl 714	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ (𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))
132		i1fmbf 25648	. . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ MblFn)
135		elrege0 13466	. . . . . . . . . . . . . . . . 17 ⊢ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
136	104, 90, 135	sylanbrc 581	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ (0[,)+∞))
137	136	fmpttd 7124	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)):ℝ⟶(0[,)+∞))
138	137	adantl 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)):ℝ⟶(0[,)+∞))
139	115	adantl 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
140	104	recnd 11274	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ)
141	140	negcld 11590	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ)
142	140, 141	ifcld 4576	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℂ)
143		subcl 11491	. . . . . . . . . . . . . . . . . . 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 594	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℂ)
145	144	anassrs 466	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℂ)
146	145	abscld 15419	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈ ℝ)
147	145	absge0d 15427	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))
148		elrege0 13466	. . . . . . . . . . . . . . . 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 581	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈ (0[,)+∞))
150	149	fmpttd 7124	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))):ℝ⟶(0[,)+∞))
151		eleq1w 2808	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑡 → (𝑥 ∈ 𝐷 ↔ 𝑡 ∈ 𝐷))
152		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑡 → (𝐹‘𝑥) = (𝐹‘𝑡))
153	151, 152	ifbieq1d 4554	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
154	153	fveq2d 6900	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑡 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
155		eqid 2725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))
156		fvex 6909	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V
157	154, 155, 156	fvmpt 7004	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
158	154	breq2d 5161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
159		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡))
160	159	breq2d 5161	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑡 → (0 ≤ (𝑔‘𝑥) ↔ 0 ≤ (𝑔‘𝑡)))
161	160, 159	ifbieq1d 4554	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
162	161	negeqd 11486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑡 → -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
163	158, 161, 162	ifbieq12d 4558	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑡 → if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
164		eqid 2725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
165		negex 11490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V
166	96, 165	ifex 4580	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ V
167	163, 164, 166	fvmpt 7004	. . . . . . . . . . . . . . . . . . 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 7437	. . . . . . . . . . . . . . . . . 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 6900	. . . . . . . . . . . . . . . . 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 5252	. . . . . . . . . . . . . . . 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 6899	. . . . . . . . . . . . . . 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 6909	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔‘𝑥) ∈ V
174	173, 95	ifex 4580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ V
175	174, 95	ifex 4580	. . . . . . . . . . . . . . . . . . . 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 7452	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) ∈ V
178	95, 177	ifex 4580	. . . . . . . . . . . . . . . . . . . 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 6723	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹:𝐷⟶ℂ → 𝐹 Fn 𝐷)
181		frn 6730	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹:𝐷⟶ℂ → ran 𝐹 ⊆ ℂ)
182		ref 15095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ℜ:ℂ⟶ℝ
183		ffn 6723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ℜ:ℂ⟶ℝ → ℜ Fn ℂ)
184	182, 183	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℜ Fn ℂ
185		fnco 6673	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℜ Fn ℂ ∧ 𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘ 𝐹) Fn 𝐷)
186	184, 185	mp3an1 1444	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘ 𝐹) Fn 𝐷)
187	180, 181, 186	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹:𝐷⟶ℂ → (ℜ ∘ 𝐹) Fn 𝐷)
188		elpreima 7066	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℜ ∘ 𝐹) Fn 𝐷 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))))
189	4, 187, 188	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))))
190		fco 6747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((ℜ:ℂ⟶ℝ ∧ 𝐹:𝐷⟶ℂ) → (ℜ ∘ 𝐹):𝐷⟶ℝ)
191	182, 4, 190	sylancr 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (ℜ ∘ 𝐹):𝐷⟶ℝ)
192	191	ffvelcdmda 7093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ)
193	192	biantrurd 531	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ ∘ 𝐹)‘𝑥))))
194		elrege0 13466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ ∘ 𝐹)‘𝑥)))
195	193, 194	bitr4di 288	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)))
196		fvco3 6996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹‘𝑥)))
197	4, 196	sylan 578	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹‘𝑥)))
198	197	breq2d 5161	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥))))
199	195, 198	bitr3d 280	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥))))
200	199	pm5.32da 577	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥)))))
201	189, 200	bitrd 278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥)))))
202	201	adantr 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥)))))
203		eldif 3954	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝐷))
204	203	baibr 535	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ → (¬ 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (ℝ ∖ 𝐷)))
205		0le0 12346	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ≤ 0
206	205, 18	breqtrri 5176	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 ≤ (ℜ‘0)
207	206	biantru 528	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑥 ∈ 𝐷 ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0)))
208	204, 207	bitr3di 285	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0))))
209	208	adantl 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0))))
210	202, 209	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)) ↔ ((𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))) ∨ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0)))))
211		elun 4145	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)))
212		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥) → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘(𝐹‘𝑥)))
213	212	breq2d 5161	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥) → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥))))
214		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘0))
215	214	breq2d 5161	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0 → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘0)))
216	213, 215	elimif 4567	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ ((𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))) ∨ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘0))))
217	210, 211, 216	3bitr4g 313	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ 0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))))
218	217	ifbid 4553	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0))
219	218	mpteq2dva 5249	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)))
220	217	ifbid 4553	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))
221	220	mpteq2dva 5249	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))))
222	172, 176, 179, 219, 221	offval2 7705	. . . . . . . . . . . . . . . . . 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 7520	. . . . . . . . . . . . . . . . . . . 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 7093	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ∈ ℝ)
225	224	recnd 11274	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ∈ ℂ)
226		0cn 11238	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℂ
227		ifcl 4575	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔‘𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ)
228	225, 226, 227	sylancl 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ)
229	228	addridd 11446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) + 0) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
230	228	mulm1d 11698	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
231	230	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (0 + (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = (0 + -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
232	228	negcld 11590	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ)
233	232	addlidd 11447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (0 + -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
234	231, 233	eqtrd 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (0 + (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
235	229, 234	ifeq12d 4551	. . . . . . . . . . . . . . . . . . . 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 2777	. . . . . . . . . . . . . . . . . . 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 5249	. . . . . . . . . . . . . . . . . 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 2785	. . . . . . . . . . . . . . . . 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 11293	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ*
240		pnfxr 11300	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ +∞ ∈ ℝ*
241		0ltpnf 13137	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 < +∞
242		snunioo 13490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞) → ({0} ∪ (0(,)+∞)) = (0[,)+∞))
243	239, 240, 241, 242	mp3an 1457	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({0} ∪ (0(,)+∞)) = (0[,)+∞)
244	243	imaeq2i 6062	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) = (◡(ℜ ∘ 𝐹) “ (0[,)+∞))
245		imaundi 6156	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) = ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞)))
246	244, 245	eqtr3i 2755	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) = ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞)))
247		ismbfcn 25602	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝐷⟶ℂ → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
248	4, 247	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
249	42, 248	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn))
250	249	simpld 493	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℜ ∘ 𝐹) ∈ MblFn)
251		mbfimasn 25605	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ ∧ 0 ∈ ℝ) → (◡(ℜ ∘ 𝐹) “ {0}) ∈ dom vol)
252	86, 251	mp3an3 1446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (◡(ℜ ∘ 𝐹) “ {0}) ∈ dom vol)
253		mbfima 25603	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (◡(ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom vol)
254		unmbl 25510	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((◡(ℜ ∘ 𝐹) “ {0}) ∈ dom vol ∧ (◡(ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
255	252, 253, 254	syl2anc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
256	250, 191, 255	syl2anc 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
257	246, 256	eqeltrid 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol)
258	4	fdmd 6733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom 𝐹 = 𝐷)
259		mbfdm 25599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
260	42, 259	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom 𝐹 ∈ dom vol)
261	258, 260	eqeltrrd 2826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐷 ∈ dom vol)
262		difmbl 25516	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℝ ∈ dom vol ∧ 𝐷 ∈ dom vol) → (ℝ ∖ 𝐷) ∈ dom vol)
263	11, 261, 262	sylancr 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℝ ∖ 𝐷) ∈ dom vol)
264		unmbl 25510	. . . . . . . . . . . . . . . . . . 19 ⊢ (((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol ∧ (ℝ ∖ 𝐷) ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol)
265	257, 263, 264	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol)
266		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑥 → (𝑔‘𝑡) = (𝑔‘𝑥))
267	266	breq2d 5161	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑥 → (0 ≤ (𝑔‘𝑡) ↔ 0 ≤ (𝑔‘𝑥)))
268	267, 266	ifbieq1d 4554	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑥 → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
269	268, 84, 174	fvmpt 7004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
270	269	eqcomd 2731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥))
271	270	ifeq1d 4549	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) = if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥), 0))
272	271	mpteq2ia 5252	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥), 0))
273	272	i1fres 25679	. . . . . . . . . . . . . . . . . . 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 12360	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -1 ∈ ℝ
276	275	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → -1 ∈ ℝ)
277	274, 276	i1fmulc 25677	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → ((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ dom ∫1)
278		cmmbl 25507	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol → (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ∈ dom vol)
279		ifnot 4582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)), 0) = if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
280		eldif 3954	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))))
281	280	baibr 535	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ 𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)))))
282		tru 1537	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ⊤
283		negex 11490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ -1 ∈ V
284	283	fconst 6783	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℝ × {-1}):ℝ⟶{-1}
285		ffn 6723	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℝ ∩ ℝ) = ℝ
290	283	fvconst2 7216	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ ℝ → ((ℝ × {-1})‘𝑥) = -1)
291	290	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → ((ℝ × {-1})‘𝑥) = -1)
292	269	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))
293	286, 287, 288, 288, 289, 291, 292	ofval 7696	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
294	282, 293	mpan 688	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ → (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))
295	294	eqcomd 2731	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥))
296	281, 295	ifbieq1d 4554	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → if(¬ 𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)), 0) = if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0))
297	279, 296	eqtr3id 2779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0))
298	297	mpteq2ia 5252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0))
299	298	i1fres 25679	. . . . . . . . . . . . . . . . . . . 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 594	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) ∈ dom ∫1)
301	273, 300	i1fadd 25668	. . . . . . . . . . . . . . . . . 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 595	. . . . . . . . . . . . . . . . 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 5262	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
305	304, 31	eqeltrid 2829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1)
306	9, 304	fmptd 7123	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)
307	305, 306	jca 510	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ))
308	307	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ))
309		ftc1anclem4 37300	. . . . . . . . . . . . . . . . 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 582	. . . . . . . . . . . . . . 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 37278	. . . . . . . . . . . . 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 2726	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
317		eqidd 2726	. . . . . . . . . . . . . . 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 7705	. . . . . . . . . . . . . 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 6900	. . . . . . . . . . . . 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 2767	. . . . . . . . . . . 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 479	. . . . . . . . . . 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 2891	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡𝑔
324		nfcv 2891	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡 ∘r ≤
325		nfmpt1 5257	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
326	323, 324, 325	nfbr 5196	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
327	322, 326	nfan 1894	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
328		anass 467	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ↔ (𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)))
329	87	ffnd 6724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 Fn ℝ)
330		fvex 6909	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ V
331		eqid 2725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
332	330, 331	fnmpti 6699	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) Fn ℝ
333	332	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) Fn ℝ)
334		eqidd 2726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) = (𝑔‘𝑡))
335	331	fvmpt2 7015	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ V) → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
336	330, 335	mpan2 689	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ℝ → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
337	336	adantl 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
338	329, 333, 101, 101, 289, 334, 337	ofrval 7697	. . . . . . . . . . . . . . . . . . 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 712	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
342		resubcl 11556	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
343	8, 104, 342	syl2an 594	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
344	343	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
345		absid 15279	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
346	8, 345	sylan 578	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
347	346	breq2d 5161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
348	347	biimpa 475	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
349	348	an32s 650	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
350	349	adantllr 717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
351		breq1 5152	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
352		breq1 5152	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
353	351, 352	ifboth 4569	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
354	350, 353	sylancom 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
355		subge0 11759	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → (0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
356	8, 104, 355	syl2an 594	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
357	356	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
358	354, 357	mpbird 256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → 0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
359	344, 358	absidd 15405	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
360		iftrue 4536	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
361	360	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
362	361	fveq2d 6900	. . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
365	345	oveq1d 7434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
366	364, 365	sylan 578	. . . . . . . . . . . . . . . . . . . 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 2775	. . . . . . . . . . . . . . . . . . 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 11673	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ)
369		resubcl 11556	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
370	8, 368, 369	syl2an 594	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
371	370	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ)
372	88	ad3antlr 729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ∈ ℝ)
373	8	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
374	8	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
375		ltnle 11325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
376	86, 375	mpan2 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
377		ltle 11334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
378	86, 377	mpan2 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
379	376, 378	sylbird 259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ → (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
380	379	imp 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)
381		absnid 15281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
382	380, 381	syldan 589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
383	382	breq2d 5161	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
384	383	biimpa 475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
385	384	an32s 650	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
386	374, 385	sylanl1 678	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
387	372, 373, 386	lenegcon2d 11829	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡))
388		simpll 765	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → 𝜑)
389	86	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 0 ∈ ℝ)
390	8, 389	ltnled 11393	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
391	8, 86, 377	sylancl 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
392	390, 391	sylbird 259	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0))
393	392	imp 405	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)
394	388, 393	sylan 578	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)
395		negeq 11484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → -(𝑔‘𝑡) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
396	395	breq2d 5161	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
397		neg0 11538	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ -0 = 0
398		negeq 11484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → -0 = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
399	397, 398	eqtr3id 2779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → 0 = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
400	399	breq2d 5161	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
401	396, 400	ifboth 4569	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡) ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
402	387, 394, 401	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
403		suble0 11760	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
404	8, 368, 403	syl2an 594	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
405	404	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
406	402, 405	mpbird 256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0)
407	371, 406	absnidd 15396	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
408		subneg 11541	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
409	408	negeqd 11486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
410		negdi2 11550	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
411	409, 410	eqtrd 2765	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
412	32, 140, 411	syl2an 594	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
413	412	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
414	407, 413	eqtrd 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
415		iffalse 4539	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))
416	415	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
417	416	fveq2d 6900	. . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . 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 578	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
420	393, 419	syldan 589	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
421	420	oveq1d 7434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
422	388, 421	sylan 578	. . . . . . . . . . . . . . . . . . . 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 2775	. . . . . . . . . . . . . . . . . . 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 811	. . . . . . . . . . . . . . . . . 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 7435	. . . . . . . . . . . . . . . . 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 11274	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ)
427		pncan3 11500	. . . . . . . . . . . . . . . . . . 19 ⊢ ((if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ ∧ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
428	140, 426, 427	syl2anr 595	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
429	428	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))
430	425, 429	eqtrd 2765	. . . . . . . . . . . . . . . 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 589	. . . . . . . . . . . . . . 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 579	. . . . . . . . . . . . . 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 650	. . . . . . . . . . . . 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 5247	. . . . . . . . . . . 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 6900	. . . . . . . . . . 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 2765	. . . . . . . . . 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 5159	. . . . . . . . 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 717	. . . . . . . 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 713	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) ∈ ℝ)
440	63	ad2antlr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → 𝑌 ∈ ℝ)
441	115	adantl 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ)
442	439, 440, 441	ltadd2d 11402	. . . . . . . . 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 479	. . . . . . . 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 11716	. . . . . . . . . . 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 479	. . . . . . . 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 310	. . . . . . 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 715	. . . . . 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 256	. . . . 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 411	. . . 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 3157	. . 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 6895	. . . . . . . . . . . . . 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 2785	. . . . . . . . . . . . 13 ⊢ ((𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))
455	454	oveq2d 7435	. . . . . . . . . . . 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 6900	. . . . . . . . . . 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 5249	. . . . . . . . . 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 6900	. . . . . . . . 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 5159	. . . . . . . 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 3606	. . . . . . 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 411	. . . . . 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 3144	. . . 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 479	. . 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 394   ∨ wo 845   = wceq 1533  ⊤wtru 1534   ∈ wcel 2098  ∀wral 3050  ∃wrex 3059  Vcvv 3461   ∖ cdif 3941   ∪ cun 3942   ⊆ wss 3944  ifcif 4530  {csn 4630   class class class wbr 5149   ↦ cmpt 5232   × cxp 5676  ^◡ccnv 5677  dom cdm 5678  ran crn 5679   “ cima 5681   ∘ ccom 5682   Fn wfn 6544  ⟶wf 6545  ‘cfv 6549  (class class class)co 7419   ∘_f cof 7683   ∘_r cofr 7684  ℂcc 11138  ℝcr 11139  0cc0 11140  1c1 11141   + caddc 11143   · cmul 11145  +∞cpnf 11277  ℝ^*cxr 11279   < clt 11280   ≤ cle 11281   − cmin 11476  -cneg 11477  ℝ⁺crp 13009  (,)cioo 13359  [,)cico 13361  [,]cicc 13362  ℜcre 15080  ℑcim 15081  abscabs 15217  volcvol 25436  MblFncmbf 25587  ∫₁citg1 25588  ∫₂citg2 25589  𝐿¹cibl 25590  ∫citg 25591  0_𝑝c0p 25642

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 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-inf2 9666  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217  ax-pre-sup 11218  ax-addf 11219

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-disj 5115  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-ofr 7686  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-er 8725  df-map 8847  df-pm 8848  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fi 9436  df-sup 9467  df-inf 9468  df-oi 9535  df-dju 9926  df-card 9964  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-div 11904  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-n0 12506  df-z 12592  df-uz 12856  df-q 12966  df-rp 13010  df-xneg 13127  df-xadd 13128  df-xmul 13129  df-ioo 13363  df-ico 13365  df-icc 13366  df-fz 13520  df-fzo 13663  df-fl 13793  df-mod 13871  df-seq 14003  df-exp 14063  df-hash 14326  df-cj 15082  df-re 15083  df-im 15084  df-sqrt 15218  df-abs 15219  df-clim 15468  df-sum 15669  df-rest 17407  df-topgen 17428  df-psmet 21288  df-xmet 21289  df-met 21290  df-bl 21291  df-mopn 21292  df-top 22840  df-topon 22857  df-bases 22893  df-cmp 23335  df-ovol 25437  df-vol 25438  df-mbf 25592  df-itg1 25593  df-itg2 25594  df-ibl 25595  df-0p 25643

This theorem is referenced by:  ftc1anclem6  37302