Theorem ftc1anclem5

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

	Ref	Expression
Hypotheses	ftc1anc.g	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
	ftc1anc.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ftc1anc.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ftc1anc.le	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	ftc1anc.s	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
	ftc1anc.d	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
	ftc1anc.i	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
	ftc1anc.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
Assertion	ftc1anclem5	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ∃ 𝑓 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < 𝑌 )

Proof

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