Theorem ftc1anclem6

Description: Lemma for ftc1anc - construction of simple functions within an arbitrary absolute distance of the given function. Similar to Lemma 565Ib of Fremlin5 p. 218, but without Fremlin's additional step of converting the simple function into a continuous one, which is unnecessary to this lemma's use; also, two simple functions are used to allow for complex-valued F . (Contributed by Brendan Leahy, 31-May-2018)

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

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		rphalfcl	⊢ ( 𝑌 ∈ ℝ+ → ( 𝑌 / 2 ) ∈ ℝ+ )
10	1 2 3 4 5 6 7 8	ftc1anclem5	⊢ ( ( 𝜑 ∧ ( 𝑌 / 2 ) ∈ ℝ+ ) → ∃ 𝑓 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) )
11	9 10	sylan2	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ∃ 𝑓 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) )
12		eqid	⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) d 𝑡 ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) d 𝑡 )
13		ax-icn	⊢ i ∈ ℂ
14		ine0	⊢ i ≠ 0
15	13 14	reccli	⊢ ( 1 / i ) ∈ ℂ
16	15	a1i	⊢ ( 𝜑 → ( 1 / i ) ∈ ℂ )
17	8	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
18	8	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑦 ) ) )
19	18 7	eqeltrrd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝐿1 )
20		divrec2	⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ( 𝐹 ‘ 𝑦 ) / i ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) )
21	13 14 20	mp3an23	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( ( 𝐹 ‘ 𝑦 ) / i ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) )
22	17 21	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑦 ) / i ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) )
23	22	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑦 ) / i ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) )
24		iblmbf	⊢ ( ( 𝑦 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝐿1 → ( 𝑦 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ MblFn )
25	19 24	syl	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ MblFn )
26		2fveq3	⊢ ( 𝑦 = 𝑥 → ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) = ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) )
27	26	cbvmptv	⊢ ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) )
28	27	eleq1i	⊢ ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ↔ ( 𝑥 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
29	17	recld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ )
30	29	recnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℂ )
31	30	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ) ∧ 𝑦 ∈ 𝐷 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℂ )
32	28	biimpri	⊢ ( ( 𝑥 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn → ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn )
33	32	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ) → ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn )
34	31 33	mbfneg	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ) → ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn )
35	28 34	sylan2b	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) → ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn )
36	8	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
37	36	recld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
38	37	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
39	38	negnegd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → - - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) )
40	39	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ - - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
41	40 27	eqtr4di	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ - - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
42	41	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) → ( 𝑥 ∈ 𝐷 ↦ - - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
43		negex	⊢ - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ V
44	43	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) ∧ 𝑥 ∈ 𝐷 ) → - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ V )
45	26	negeqd	⊢ ( 𝑦 = 𝑥 → - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) = - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) )
46	45	cbvmptv	⊢ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) )
47	46	eleq1i	⊢ ( ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ↔ ( 𝑥 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
48	47	biimpi	⊢ ( ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn → ( 𝑥 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
49	48	adantl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) → ( 𝑥 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
50	44 49	mbfneg	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) → ( 𝑥 ∈ 𝐷 ↦ - - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
51	42 50	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) → ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn )
52	35 51	impbida	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ↔ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) )
53		divcl	⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ( 𝐹 ‘ 𝑦 ) / i ) ∈ ℂ )
54		imre	⊢ ( ( ( 𝐹 ‘ 𝑦 ) / i ) ∈ ℂ → ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) = ( ℜ ‘ ( - i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) )
55	53 54	syl	⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) = ( ℜ ‘ ( - i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) )
56	13 14 55	mp3an23	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) = ( ℜ ‘ ( - i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) )
57	13 14 53	mp3an23	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( ( 𝐹 ‘ 𝑦 ) / i ) ∈ ℂ )
58		mulneg1	⊢ ( ( i ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑦 ) / i ) ∈ ℂ ) → ( - i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) = - ( i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) )
59	13 57 58	sylancr	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( - i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) = - ( i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) )
60		divcan2	⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) = ( 𝐹 ‘ 𝑦 ) )
61	13 14 60	mp3an23	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) = ( 𝐹 ‘ 𝑦 ) )
62	61	negeqd	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → - ( i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) = - ( 𝐹 ‘ 𝑦 ) )
63	59 62	eqtrd	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( - i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) = - ( 𝐹 ‘ 𝑦 ) )
64	63	fveq2d	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( ℜ ‘ ( - i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) = ( ℜ ‘ - ( 𝐹 ‘ 𝑦 ) ) )
65		reneg	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( ℜ ‘ - ( 𝐹 ‘ 𝑦 ) ) = - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) )
66	56 64 65	3eqtrd	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) = - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) )
67	17 66	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) = - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) )
68	67	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) = ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
69	68	eleq1d	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ↔ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) )
70	52 69	bitr4d	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ↔ ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ) )
71		imval	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( ℑ ‘ ( 𝐹 ‘ 𝑦 ) ) = ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) )
72	17 71	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ℑ ‘ ( 𝐹 ‘ 𝑦 ) ) = ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) )
73	72	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) )
74	73	eleq1d	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ↔ ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ) )
75	70 74	anbi12d	⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) ↔ ( ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ) ) )
76		ancom	⊢ ( ( ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ) ↔ ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ) )
77	75 76	bitrdi	⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) ↔ ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ) ) )
78	17	ismbfcn2	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ MblFn ↔ ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) ) )
79	17 57	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑦 ) / i ) ∈ ℂ )
80	79	ismbfcn2	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ∈ MblFn ↔ ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ) ) )
81	77 78 80	3bitr4d	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ MblFn ↔ ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ∈ MblFn ) )
82	25 81	mpbid	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ∈ MblFn )
83	23 82	eqeltrrd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn )
84	16 17 19 83	iblmulc2nc	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ∈ 𝐿1 )
85		mulcl	⊢ ( ( ( 1 / i ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑦 ) ∈ ℂ ) → ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ∈ ℂ )
86	15 17 85	sylancr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ∈ ℂ )
87	86	fmpttd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) : 𝐷 ⟶ ℂ )
88	12 2 3 4 5 6 84 87	ftc1anclem5	⊢ ( ( 𝜑 ∧ ( 𝑌 / 2 ) ∈ ℝ+ ) → ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) )
89	9 88	sylan2	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) )
90	8	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
91		0cnd	⊢ ( ( 𝜑 ∧ ¬ 𝑡 ∈ 𝐷 ) → 0 ∈ ℂ )
92	90 91	ifclda	⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ∈ ℂ )
93		imval	⊢ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ∈ ℂ → ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) = ( ℜ ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) / i ) ) )
94	92 93	syl	⊢ ( 𝜑 → ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) = ( ℜ ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) / i ) ) )
95		fveq2	⊢ ( 𝑦 = 𝑡 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑡 ) )
96	95	oveq2d	⊢ ( 𝑦 = 𝑡 → ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑡 ) ) )
97		eqid	⊢ ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) )
98		ovex	⊢ ( ( 1 / i ) · ( 𝐹 ‘ 𝑡 ) ) ∈ V
99	96 97 98	fvmpt	⊢ ( 𝑡 ∈ 𝐷 → ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑡 ) ) )
100	99	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑡 ) ) )
101		divrec2	⊢ ( ( ( 𝐹 ‘ 𝑡 ) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ( 𝐹 ‘ 𝑡 ) / i ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑡 ) ) )
102	13 14 101	mp3an23	⊢ ( ( 𝐹 ‘ 𝑡 ) ∈ ℂ → ( ( 𝐹 ‘ 𝑡 ) / i ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑡 ) ) )
103	90 102	syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑡 ) / i ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑡 ) ) )
104	100 103	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) = ( ( 𝐹 ‘ 𝑡 ) / i ) )
105	104	ifeq1da	⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) = if ( 𝑡 ∈ 𝐷 , ( ( 𝐹 ‘ 𝑡 ) / i ) , 0 ) )
106		ovif	⊢ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) / i ) = if ( 𝑡 ∈ 𝐷 , ( ( 𝐹 ‘ 𝑡 ) / i ) , ( 0 / i ) )
107	13 14	div0i	⊢ ( 0 / i ) = 0
108		ifeq2	⊢ ( ( 0 / i ) = 0 → if ( 𝑡 ∈ 𝐷 , ( ( 𝐹 ‘ 𝑡 ) / i ) , ( 0 / i ) ) = if ( 𝑡 ∈ 𝐷 , ( ( 𝐹 ‘ 𝑡 ) / i ) , 0 ) )
109	107 108	ax-mp	⊢ if ( 𝑡 ∈ 𝐷 , ( ( 𝐹 ‘ 𝑡 ) / i ) , ( 0 / i ) ) = if ( 𝑡 ∈ 𝐷 , ( ( 𝐹 ‘ 𝑡 ) / i ) , 0 )
110	106 109	eqtri	⊢ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) / i ) = if ( 𝑡 ∈ 𝐷 , ( ( 𝐹 ‘ 𝑡 ) / i ) , 0 )
111	105 110	eqtr4di	⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) = ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) / i ) )
112	111	fveq2d	⊢ ( 𝜑 → ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) = ( ℜ ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) / i ) ) )
113	94 112	eqtr4d	⊢ ( 𝜑 → ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) = ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) )
114	113	fvoveq1d	⊢ ( 𝜑 → ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) = ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) )
115	114	mpteq2dv	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) )
116	115	fveq2d	⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
117	116	breq1d	⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ↔ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) )
118	117	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ↔ ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) )
119	118	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ( ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ↔ ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) )
120	89 119	mpbird	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) )
121		reeanv	⊢ ( ∃ 𝑓 ∈ dom ∫1 ∃ 𝑔 ∈ dom ∫1 ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) ↔ ( ∃ 𝑓 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ∧ ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) )
122		eleq1w	⊢ ( 𝑥 = 𝑡 → ( 𝑥 ∈ 𝐷 ↔ 𝑡 ∈ 𝐷 ) )
123		fveq2	⊢ ( 𝑥 = 𝑡 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑡 ) )
124	122 123	ifbieq1d	⊢ ( 𝑥 = 𝑡 → if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) )
125	124	fveq2d	⊢ ( 𝑥 = 𝑡 → ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) )
126		eqid	⊢ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
127		fvex	⊢ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ V
128	125 126 127	fvmpt	⊢ ( 𝑡 ∈ ℝ → ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) = ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) )
129	128	fvoveq1d	⊢ ( 𝑡 ∈ ℝ → ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑓 ‘ 𝑡 ) ) ) = ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) )
130	129	mpteq2ia	⊢ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑓 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) )
131	130	fveq2i	⊢ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) )
132		rembl	⊢ ℝ ∈ dom vol
133	132	a1i	⊢ ( 𝜑 → ℝ ∈ dom vol )
134		0cnd	⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐷 ) → 0 ∈ ℂ )
135	36 134	ifclda	⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℂ )
136	135	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℂ )
137		eldifn	⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐷 ) → ¬ 𝑥 ∈ 𝐷 )
138	137	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐷 ) ) → ¬ 𝑥 ∈ 𝐷 )
139	138	iffalsed	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐷 ) ) → if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) = 0 )
140	8	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) )
141		iftrue	⊢ ( 𝑥 ∈ 𝐷 → if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) )
142	141	mpteq2ia	⊢ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) )
143	140 142	eqtr4di	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
144	143 7	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐿1 )
145	6 133 136 139 144	iblss2	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐿1 )
146	135	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℂ )
147	146	iblcn	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ) ) )
148	145 147	mpbid	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ) )
149	148	simpld	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 )
150	146	recld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ ℝ )
151	150	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ )
152	149 151	jca	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ ) )
153		ftc1anclem4	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
154	153	3expb	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
155	152 154	sylan2	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝜑 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
156	155	ancoms	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
157	131 156	eqeltrrid	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
158	124	fveq2d	⊢ ( 𝑥 = 𝑡 → ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) )
159		eqid	⊢ ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
160		fvex	⊢ ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ V
161	158 159 160	fvmpt	⊢ ( 𝑡 ∈ ℝ → ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) = ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) )
162	161	fvoveq1d	⊢ ( 𝑡 ∈ ℝ → ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑔 ‘ 𝑡 ) ) ) = ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) )
163	162	mpteq2ia	⊢ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) )
164	163	fveq2i	⊢ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) )
165	148	simprd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 )
166	135	imcld	⊢ ( 𝜑 → ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ ℝ )
167	166	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ ℝ )
168	167	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ )
169	165 168	jca	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ ) )
170		ftc1anclem4	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
171	170	3expb	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
172	169 171	sylan2	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝜑 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
173	172	ancoms	⊢ ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
174	164 173	eqeltrrid	⊢ ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
175	157 174	anim12dan	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ ) )
176	9	rpred	⊢ ( 𝑌 ∈ ℝ+ → ( 𝑌 / 2 ) ∈ ℝ )
177	176 176	jca	⊢ ( 𝑌 ∈ ℝ+ → ( ( 𝑌 / 2 ) ∈ ℝ ∧ ( 𝑌 / 2 ) ∈ ℝ ) )
178		lt2add	⊢ ( ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ ) ∧ ( ( 𝑌 / 2 ) ∈ ℝ ∧ ( 𝑌 / 2 ) ∈ ℝ ) ) → ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ) )
179	175 177 178	syl2an	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑌 ∈ ℝ+ ) → ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ) )
180	179	an32s	⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ) )
181	92	recld	⊢ ( 𝜑 → ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ )
182	181	recnd	⊢ ( 𝜑 → ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ )
183		i1ff	⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 : ℝ ⟶ ℝ )
184	183	ffvelcdmda	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ℝ )
185	184	recnd	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ℂ )
186		subcl	⊢ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ ∧ ( 𝑓 ‘ 𝑡 ) ∈ ℂ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ℂ )
187	182 185 186	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ℂ )
188	187	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ℂ )
189	188	adantlrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ℂ )
190	92	imcld	⊢ ( 𝜑 → ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ )
191	190	recnd	⊢ ( 𝜑 → ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ )
192		i1ff	⊢ ( 𝑔 ∈ dom ∫1 → 𝑔 : ℝ ⟶ ℝ )
193	192	ffvelcdmda	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ℝ )
194	193	recnd	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ℂ )
195		subcl	⊢ ( ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℂ ) → ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
196	191 194 195	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
197	196	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
198		mulcl	⊢ ( ( i ∈ ℂ ∧ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) → ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
199	13 197 198	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
200	199	adantlrl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
201	189 200	addcld	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℂ )
202	201	abscld	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
203	202	rexrd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* )
204	201	absge0d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
205		elxrge0	⊢ ( ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
206	203 204 205	sylanbrc	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) )
207	206	fmpttd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
208		icossicc	⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
209		ge0addcl	⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
210	208 209	sselid	⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,] +∞ ) )
211	210	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,] +∞ ) )
212	188	abscld	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ∈ ℝ )
213	188	absge0d	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) )
214		elrege0	⊢ ( ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) )
215	212 213 214	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) )
216	215	fmpttd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
217	216	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
218	197	abscld	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℝ )
219	197	absge0d	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) )
220		elrege0	⊢ ( ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) )
221	218 219 220	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) )
222	221	fmpttd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
223	222	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
224		reex	⊢ ℝ ∈ V
225	224	a1i	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ℝ ∈ V )
226		inidm	⊢ ( ℝ ∩ ℝ ) = ℝ
227	211 217 223 225 225 226	off	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
228	189 200	abstrid	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ ( ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) + ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
229	228	ralrimiva	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ∀ 𝑡 ∈ ℝ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ ( ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) + ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
230		ovexd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) + ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ V )
231		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
232		fvexd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ∈ V )
233		fvexd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ V )
234		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) )
235		absmul	⊢ ( ( i ∈ ℂ ∧ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) → ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( abs ‘ i ) · ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) )
236	13 197 235	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( abs ‘ i ) · ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) )
237		absi	⊢ ( abs ‘ i ) = 1
238	237	oveq1i	⊢ ( ( abs ‘ i ) · ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( 1 · ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) )
239	218	recnd	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
240	239	mullidd	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( 1 · ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) )
241	238 240	eqtrid	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ i ) · ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) )
242	236 241	eqtr2d	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) = ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) )
243	242	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
244	243	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
245	225 232 233 234 244	offval2	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) + ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
246	225 202 230 231 245	ofrfval2	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∘r ≤ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ↔ ∀ 𝑡 ∈ ℝ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ ( ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) + ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
247	229 246	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∘r ≤ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
248		itg2le	⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∘r ≤ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ≤ ( ∫2 ‘ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
249	207 227 247 248	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ≤ ( ∫2 ‘ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
250		absf	⊢ abs : ℂ ⟶ ℝ
251	250	a1i	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → abs : ℂ ⟶ ℝ )
252	251 188	cofmpt	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( abs ∘ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) )
253		resubcl	⊢ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ ( 𝑓 ‘ 𝑡 ) ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ℝ )
254	181 184 253	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ℝ )
255	254	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ℝ )
256	255	fmpttd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) : ℝ ⟶ ℝ )
257	132	a1i	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ℝ ∈ dom vol )
258		iunin2	⊢ ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ∪ 𝑦 ∈ ran 𝑓 ( ◡ 𝑓 “ { 𝑦 } ) )
259		imaiun	⊢ ( ◡ 𝑓 “ ∪ 𝑦 ∈ ran 𝑓 { 𝑦 } ) = ∪ 𝑦 ∈ ran 𝑓 ( ◡ 𝑓 “ { 𝑦 } )
260		iunid	⊢ ∪ 𝑦 ∈ ran 𝑓 { 𝑦 } = ran 𝑓
261	260	imaeq2i	⊢ ( ◡ 𝑓 “ ∪ 𝑦 ∈ ran 𝑓 { 𝑦 } ) = ( ◡ 𝑓 “ ran 𝑓 )
262	259 261	eqtr3i	⊢ ∪ 𝑦 ∈ ran 𝑓 ( ◡ 𝑓 “ { 𝑦 } ) = ( ◡ 𝑓 “ ran 𝑓 )
263	262	ineq2i	⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ∪ 𝑦 ∈ ran 𝑓 ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) )
264	258 263	eqtri	⊢ ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) )
265		cnvimass	⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ⊆ dom ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) )
266		ovex	⊢ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ V
267		eqid	⊢ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) )
268	266 267	dmmpti	⊢ dom ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) = ℝ
269	265 268	sseqtri	⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ⊆ ℝ
270		cnvimarndm	⊢ ( ◡ 𝑓 “ ran 𝑓 ) = dom 𝑓
271	183	fdmd	⊢ ( 𝑓 ∈ dom ∫1 → dom 𝑓 = ℝ )
272	270 271	eqtrid	⊢ ( 𝑓 ∈ dom ∫1 → ( ◡ 𝑓 “ ran 𝑓 ) = ℝ )
273	269 272	sseqtrrid	⊢ ( 𝑓 ∈ dom ∫1 → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ⊆ ( ◡ 𝑓 “ ran 𝑓 ) )
274		df-ss	⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ⊆ ( ◡ 𝑓 “ ran 𝑓 ) ↔ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) )
275	273 274	sylib	⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) )
276	264 275	eqtrid	⊢ ( 𝑓 ∈ dom ∫1 → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) )
277	276	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) )
278	183	frnd	⊢ ( 𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ )
279	278	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ran 𝑓 ⊆ ℝ )
280	279	sselda	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → 𝑦 ∈ ℝ )
281	181	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ )
282		resubcl	⊢ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ )
283	181 282	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ )
284	283	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ )
285	281 284	2thd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ) )
286		ltaddsub	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ) → ( ( 𝑥 + 𝑦 ) < ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ↔ 𝑥 < ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ) )
287	181 286	syl3an3	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝜑 ) → ( ( 𝑥 + 𝑦 ) < ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ↔ 𝑥 < ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ) )
288	287	3comr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + 𝑦 ) < ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ↔ 𝑥 < ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ) )
289	288	3expa	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + 𝑦 ) < ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ↔ 𝑥 < ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ) )
290	285 289	anbi12d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ ( 𝑥 + 𝑦 ) < ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ↔ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ∧ 𝑥 < ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ) ) )
291		readdcl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
292	291	rexrd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ* )
293	292	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ* )
294		elioopnf	⊢ ( ( 𝑥 + 𝑦 ) ∈ ℝ* → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ ( 𝑥 + 𝑦 ) < ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) )
295	293 294	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ ( 𝑥 + 𝑦 ) < ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) )
296		rexr	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
297	296	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℝ* )
298		elioopnf	⊢ ( 𝑥 ∈ ℝ* → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ∧ 𝑥 < ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ) ) )
299	297 298	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ∧ 𝑥 < ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ) ) )
300	290 295 299	3bitr4rd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) )
301		oveq2	⊢ ( ( 𝑓 ‘ 𝑡 ) = 𝑦 → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) = ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) )
302	301	eleq1d	⊢ ( ( 𝑓 ‘ 𝑡 ) = 𝑦 → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( 𝑥 (,) +∞ ) ) )
303	302	bibi1d	⊢ ( ( 𝑓 ‘ 𝑡 ) = 𝑦 → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ↔ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ) )
304	300 303	syl5ibrcom	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) = 𝑦 → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ) )
305	304	pm5.32rd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ) )
306	305	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ) )
307	280 306	syldan	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ) )
308	307	rabbidv	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
309	183	feqmptd	⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 = ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) )
310	309	cnveqd	⊢ ( 𝑓 ∈ dom ∫1 → ◡ 𝑓 = ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) )
311	310	imaeq1d	⊢ ( 𝑓 ∈ dom ∫1 → ( ◡ 𝑓 “ { 𝑦 } ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) )
312	311	ineq2d	⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) )
313	267	mptpreima	⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) }
314		vex	⊢ 𝑦 ∈ V
315		eqid	⊢ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) = ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) )
316	315	mptiniseg	⊢ ( 𝑦 ∈ V → ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) = { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } )
317	314 316	ax-mp	⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) = { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 }
318	313 317	ineq12i	⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = ( { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } )
319		inrab	⊢ ( { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
320	318 319	eqtri	⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
321	312 320	eqtrdi	⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
322	321	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
323	311	ineq2d	⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) )
324		eqid	⊢ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) )
325	324	mptpreima	⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) = { 𝑡 ∈ ℝ ∣ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) }
326	325 317	ineq12i	⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = ( { 𝑡 ∈ ℝ ∣ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } )
327		inrab	⊢ ( { 𝑡 ∈ ℝ ∣ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
328	326 327	eqtri	⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
329	323 328	eqtrdi	⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
330	329	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
331	308 322 330	3eqtr4d	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) )
332	331	iuneq2dv	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) )
333	277 332	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) = ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) )
334		i1frn	⊢ ( 𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin )
335	334	adantl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ran 𝑓 ∈ Fin )
336	92	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ∈ ℂ )
337		eldifn	⊢ ( 𝑡 ∈ ( ℝ ∖ 𝐷 ) → ¬ 𝑡 ∈ 𝐷 )
338	337	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ℝ ∖ 𝐷 ) ) → ¬ 𝑡 ∈ 𝐷 )
339	338	iffalsed	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ℝ ∖ 𝐷 ) ) → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) = 0 )
340	8	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) )
341		iftrue	⊢ ( 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) = ( 𝐹 ‘ 𝑡 ) )
342	341	mpteq2ia	⊢ ( 𝑡 ∈ 𝐷 ↦ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) = ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) )
343	340 342	eqtr4di	⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ 𝐷 ↦ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) )
344		iblmbf	⊢ ( 𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn )
345	7 344	syl	⊢ ( 𝜑 → 𝐹 ∈ MblFn )
346	343 345	eqeltrrd	⊢ ( 𝜑 → ( 𝑡 ∈ 𝐷 ↦ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ MblFn )
347	6 133 336 339 346	mbfss	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ MblFn )
348	92	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ∈ ℂ )
349	348	ismbfcn2	⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ MblFn ↔ ( ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ MblFn ∧ ( 𝑡 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ MblFn ) ) )
350	347 349	mpbid	⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ MblFn ∧ ( 𝑡 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ MblFn ) )
351	350	simpld	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ MblFn )
352	181	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ )
353	352	fmpttd	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) : ℝ ⟶ ℝ )
354		mbfima	⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ MblFn ∧ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) : ℝ ⟶ ℝ ) → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∈ dom vol )
355	351 353 354	syl2anc	⊢ ( 𝜑 → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∈ dom vol )
356		i1fima	⊢ ( 𝑓 ∈ dom ∫1 → ( ◡ 𝑓 “ { 𝑦 } ) ∈ dom vol )
357		inmbl	⊢ ( ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∈ dom vol ∧ ( ◡ 𝑓 “ { 𝑦 } ) ∈ dom vol ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
358	355 356 357	syl2an	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
359	358	ralrimivw	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ∀ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
360		finiunmbl	⊢ ( ( ran 𝑓 ∈ Fin ∧ ∀ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
361	335 359 360	syl2anc	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
362	361	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
363	333 362	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
364		iunin2	⊢ ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ∪ 𝑦 ∈ ran 𝑓 ( ◡ 𝑓 “ { 𝑦 } ) )
365	262	ineq2i	⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ∪ 𝑦 ∈ ran 𝑓 ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) )
366	364 365	eqtri	⊢ ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) )
367		cnvimass	⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ⊆ dom ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) )
368	367 268	sseqtri	⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ⊆ ℝ
369	368 272	sseqtrrid	⊢ ( 𝑓 ∈ dom ∫1 → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ⊆ ( ◡ 𝑓 “ ran 𝑓 ) )
370		df-ss	⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ⊆ ( ◡ 𝑓 “ ran 𝑓 ) ↔ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) )
371	369 370	sylib	⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) )
372	366 371	eqtrid	⊢ ( 𝑓 ∈ dom ∫1 → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) )
373	372	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) )
374	284 281	2thd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ) )
375		ltsubadd	⊢ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) < 𝑥 ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) < ( 𝑥 + 𝑦 ) ) )
376	181 375	syl3an1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) < 𝑥 ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) < ( 𝑥 + 𝑦 ) ) )
377	376	3expa	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) < 𝑥 ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) < ( 𝑥 + 𝑦 ) ) )
378	377	an32s	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) < 𝑥 ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) < ( 𝑥 + 𝑦 ) ) )
379	374 378	anbi12d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ∧ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) < 𝑥 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) < ( 𝑥 + 𝑦 ) ) ) )
380		elioomnf	⊢ ( 𝑥 ∈ ℝ* → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ∧ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) < 𝑥 ) ) )
381	297 380	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ∧ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) < 𝑥 ) ) )
382		elioomnf	⊢ ( ( 𝑥 + 𝑦 ) ∈ ℝ* → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) < ( 𝑥 + 𝑦 ) ) ) )
383	293 382	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) < ( 𝑥 + 𝑦 ) ) ) )
384	379 381 383	3bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) )
385	301	eleq1d	⊢ ( ( 𝑓 ‘ 𝑡 ) = 𝑦 → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( -∞ (,) 𝑥 ) ) )
386	385	bibi1d	⊢ ( ( 𝑓 ‘ 𝑡 ) = 𝑦 → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ↔ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ) )
387	384 386	syl5ibrcom	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) = 𝑦 → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ) )
388	387	pm5.32rd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ) )
389	388	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ) )
390	280 389	syldan	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ) )
391	390	rabbidv	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
392	311	ineq2d	⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) )
393	267	mptpreima	⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) }
394	393 317	ineq12i	⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = ( { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } )
395		inrab	⊢ ( { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
396	394 395	eqtri	⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
397	392 396	eqtrdi	⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
398	397	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
399	311	ineq2d	⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) )
400	324	mptpreima	⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) = { 𝑡 ∈ ℝ ∣ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) }
401	400 317	ineq12i	⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = ( { 𝑡 ∈ ℝ ∣ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } )
402		inrab	⊢ ( { 𝑡 ∈ ℝ ∣ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
403	401 402	eqtri	⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
404	399 403	eqtrdi	⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
405	404	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
406	391 398 405	3eqtr4d	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) )
407	406	iuneq2dv	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) )
408	373 407	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) = ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) )
409		mbfima	⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ MblFn ∧ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) : ℝ ⟶ ℝ ) → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∈ dom vol )
410	351 353 409	syl2anc	⊢ ( 𝜑 → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∈ dom vol )
411		inmbl	⊢ ( ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∈ dom vol ∧ ( ◡ 𝑓 “ { 𝑦 } ) ∈ dom vol ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
412	410 356 411	syl2an	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
413	412	ralrimivw	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ∀ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
414		finiunmbl	⊢ ( ( ran 𝑓 ∈ Fin ∧ ∀ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
415	335 413 414	syl2anc	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
416	415	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
417	408 416	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
418	256 257 363 417	ismbf2d	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ∈ MblFn )
419		ftc1anclem1	⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) : ℝ ⟶ ℝ ∧ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ∈ MblFn ) → ( abs ∘ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∈ MblFn )
420	256 418 419	syl2anc	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( abs ∘ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∈ MblFn )
421	252 420	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∈ MblFn )
422	421	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∈ MblFn )
423	157	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
424	174	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
425	422 217 423 223 424	itg2addnc	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) = ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
426	249 425	breqtrd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ≤ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
427	426	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ≤ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
428		itg2cl	⊢ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ∈ ℝ* )
429	207 428	syl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ∈ ℝ* )
430	429	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ∈ ℝ* )
431		readdcl	⊢ ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∈ ℝ )
432	157 174 431	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∈ ℝ )
433	432	anandis	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∈ ℝ )
434	433	rexrd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∈ ℝ* )
435	434	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∈ ℝ* )
436	9 9	rpaddcld	⊢ ( 𝑌 ∈ ℝ+ → ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ∈ ℝ+ )
437	436	rpxrd	⊢ ( 𝑌 ∈ ℝ+ → ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ∈ ℝ* )
438	437	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ∈ ℝ* )
439		xrlelttr	⊢ ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ∈ ℝ* ∧ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∈ ℝ* ∧ ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ∈ ℝ* ) → ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ≤ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∧ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ) )
440	430 435 438 439	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ≤ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∧ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ) )
441	427 440	mpand	⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ) )
442	180 441	syld	⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ) )
443		mulcl	⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ ) → ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ ℂ )
444	13 191 443	sylancr	⊢ ( 𝜑 → ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ ℂ )
445	182 444	jca	⊢ ( 𝜑 → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ ∧ ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ ℂ ) )
446		mulcl	⊢ ( ( i ∈ ℂ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℂ ) → ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
447	13 194 446	sylancr	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
448	185 447	anim12i	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( ( 𝑓 ‘ 𝑡 ) ∈ ℂ ∧ ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) )
449	448	anandirs	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) ∈ ℂ ∧ ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) )
450		addsub4	⊢ ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ ∧ ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ ℂ ) ∧ ( ( 𝑓 ‘ 𝑡 ) ∈ ℂ ∧ ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) + ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) − ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
451	445 449 450	syl2an	⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) + ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) − ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
452	451	anassrs	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) + ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) − ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
453	92	replimd	⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) = ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) + ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) )
454	453	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) = ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) + ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) )
455	454	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) + ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
456	194	adantll	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ℂ )
457		subdi	⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℂ ) → ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) = ( ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) − ( i · ( 𝑔 ‘ 𝑡 ) ) ) )
458	13 191 456 457	mp3an3an	⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) ) → ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) = ( ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) − ( i · ( 𝑔 ‘ 𝑡 ) ) ) )
459	458	anassrs	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) = ( ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) − ( i · ( 𝑔 ‘ 𝑡 ) ) ) )
460	459	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) − ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
461	452 455 460	3eqtr4rd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
462	461	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) = ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
463	462	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
464	463	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) )
465	464	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) )
466		rpcn	⊢ ( 𝑌 ∈ ℝ+ → 𝑌 ∈ ℂ )
467	466	2halvesd	⊢ ( 𝑌 ∈ ℝ+ → ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) = 𝑌 )
468	467	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) = 𝑌 )
469	465 468	breq12d	⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ↔ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < 𝑌 ) )
470	442 469	sylibd	⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < 𝑌 ) )
471	470	reximdvva	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ( ∃ 𝑓 ∈ dom ∫1 ∃ 𝑔 ∈ dom ∫1 ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) → ∃ 𝑓 ∈ dom ∫1 ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < 𝑌 ) )
472	121 471	biimtrrid	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ( ( ∃ 𝑓 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ∧ ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) → ∃ 𝑓 ∈ dom ∫1 ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < 𝑌 ) )
473	11 120 472	mp2and	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ∃ 𝑓 ∈ dom ∫1 ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < 𝑌 )