Theorem ftc1anclem6 37706

Description: Lemma for ftc1anc 37709- 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 𝐹. (Contributed by Brendan Leahy, 31-May-2018.)

Hypotheses

Ref	Expression
ftc1anc.g	⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)
ftc1anc.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
ftc1anc.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
ftc1anc.le	⊢ (𝜑 → 𝐴 ≤ 𝐵)
ftc1anc.s	⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
ftc1anc.d	⊢ (𝜑 → 𝐷 ⊆ ℝ)
ftc1anc.i	⊢ (𝜑 → 𝐹 ∈ 𝐿1)
ftc1anc.f	⊢ (𝜑 → 𝐹:𝐷⟶ℂ)

Assertion

Ref	Expression
ftc1anclem6	⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌)

Distinct variable groups:   𝑓,𝑔,𝑡,𝑥,𝐴   𝐵,𝑓,𝑔,𝑡,𝑥   𝐷,𝑓,𝑔,𝑡,𝑥   𝑓,𝐹,𝑔,𝑡,𝑥   𝜑,𝑓,𝑔,𝑡,𝑥   𝑓,𝐺,𝑔   𝑓,𝑌,𝑔,𝑡,𝑥

Allowed substitution hints:   𝐺(𝑥,𝑡)

Proof of Theorem ftc1anclem6

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rphalfcl 13063	. . 3 ⊢ (𝑌 ∈ ℝ+ → (𝑌 / 2) ∈ ℝ+)
2		ftc1anc.g	. . . 4 ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)
3		ftc1anc.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		ftc1anc.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		ftc1anc.le	. . . 4 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
6		ftc1anc.s	. . . 4 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
7		ftc1anc.d	. . . 4 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
8		ftc1anc.i	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝐿1)
9		ftc1anc.f	. . . 4 ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)
10	2, 3, 4, 5, 6, 7, 8, 9	ftc1anclem5 37705	. . 3 ⊢ ((𝜑 ∧ (𝑌 / 2) ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2))
11	1, 10	sylan2 593	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2))
12		eqid 2736	. . . . 5 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) d𝑡) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) d𝑡)
13		ax-icn 11215	. . . . . . . 8 ⊢ i ∈ ℂ
14		ine0 11699	. . . . . . . 8 ⊢ i ≠ 0
15	13, 14	reccli 11998	. . . . . . 7 ⊢ (1 / i) ∈ ℂ
16	15	a1i 11	. . . . . 6 ⊢ (𝜑 → (1 / i) ∈ ℂ)
17	9	ffvelcdmda 7103	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐹‘𝑦) ∈ ℂ)
18	9	feqmptd 6976	. . . . . . 7 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)))
19	18, 8	eqeltrrd 2841	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ 𝐿1)
20		divrec2 11940	. . . . . . . . . 10 ⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦)))
21	13, 14, 20	mp3an23 1454	. . . . . . . . 9 ⊢ ((𝐹‘𝑦) ∈ ℂ → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦)))
22	17, 21	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦)))
23	22	mpteq2dva 5241	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) = (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))))
24		iblmbf 25803	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ 𝐿1 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn)
25	19, 24	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn)
26		2fveq3 6910	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (ℜ‘(𝐹‘𝑦)) = (ℜ‘(𝐹‘𝑥)))
27	26	cbvmptv 5254	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) = (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥)))
28	27	eleq1i 2831	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn)
29	17	recld 15234	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℝ)
30	29	recnd 11290	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℂ)
31	30	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℂ)
32	28	biimpri 228	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn → (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn)
33	32	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn)
34	31, 33	mbfneg 25686	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn)
35	28, 34	sylan2b 594	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn)
36	9	ffvelcdmda 7103	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐹‘𝑥) ∈ ℂ)
37	36	recld 15234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (ℜ‘(𝐹‘𝑥)) ∈ ℝ)
38	37	recnd 11290	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (ℜ‘(𝐹‘𝑥)) ∈ ℂ)
39	38	negnegd 11612	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → --(ℜ‘(𝐹‘𝑥)) = (ℜ‘(𝐹‘𝑥)))
40	39	mpteq2dva 5241	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))))
41	40, 27	eqtr4di 2794	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))))
42	41	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))))
43		negex 11507	. . . . . . . . . . . . . . . 16 ⊢ -(ℜ‘(𝐹‘𝑥)) ∈ V
44	43	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) ∧ 𝑥 ∈ 𝐷) → -(ℜ‘(𝐹‘𝑥)) ∈ V)
45	26	negeqd 11503	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → -(ℜ‘(𝐹‘𝑦)) = -(ℜ‘(𝐹‘𝑥)))
46	45	cbvmptv 5254	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) = (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥)))
47	46	eleq1i 2831	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) ∈ MblFn)
48	47	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn → (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) ∈ MblFn)
49	48	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) ∈ MblFn)
50	44, 49	mbfneg 25686	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) ∈ MblFn)
51	42, 50	eqeltrrd 2841	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn)
52	35, 51	impbida 800	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn))
53		divcl 11929	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹‘𝑦) / i) ∈ ℂ)
54		imre 15148	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑦) / i) ∈ ℂ → (ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i))))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → (ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i))))
56	13, 14, 55	mp3an23 1454	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i))))
57	13, 14, 53	mp3an23 1454	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑦) ∈ ℂ → ((𝐹‘𝑦) / i) ∈ ℂ)
58		mulneg1 11700	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i ∈ ℂ ∧ ((𝐹‘𝑦) / i) ∈ ℂ) → (-i · ((𝐹‘𝑦) / i)) = -(i · ((𝐹‘𝑦) / i)))
59	13, 57, 58	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) ∈ ℂ → (-i · ((𝐹‘𝑦) / i)) = -(i · ((𝐹‘𝑦) / i)))
60		divcan2 11931	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → (i · ((𝐹‘𝑦) / i)) = (𝐹‘𝑦))
61	13, 14, 60	mp3an23 1454	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑦) ∈ ℂ → (i · ((𝐹‘𝑦) / i)) = (𝐹‘𝑦))
62	61	negeqd 11503	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) ∈ ℂ → -(i · ((𝐹‘𝑦) / i)) = -(𝐹‘𝑦))
63	59, 62	eqtrd 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑦) ∈ ℂ → (-i · ((𝐹‘𝑦) / i)) = -(𝐹‘𝑦))
64	63	fveq2d 6909	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℜ‘(-i · ((𝐹‘𝑦) / i))) = (ℜ‘-(𝐹‘𝑦)))
65		reneg 15165	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℜ‘-(𝐹‘𝑦)) = -(ℜ‘(𝐹‘𝑦)))
66	56, 64, 65	3eqtrd 2780	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℑ‘((𝐹‘𝑦) / i)) = -(ℜ‘(𝐹‘𝑦)))
67	17, 66	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℑ‘((𝐹‘𝑦) / i)) = -(ℜ‘(𝐹‘𝑦)))
68	67	mpteq2dva 5241	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) = (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))))
69	68	eleq1d 2825	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn))
70	52, 69	bitr4d 282	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn))
71		imval 15147	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℑ‘(𝐹‘𝑦)) = (ℜ‘((𝐹‘𝑦) / i)))
72	17, 71	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℑ‘(𝐹‘𝑦)) = (ℜ‘((𝐹‘𝑦) / i)))
73	72	mpteq2dva 5241	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))))
74	73	eleq1d 2825	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn))
75	70, 74	anbi12d 632	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn)))
76		ancom 460	. . . . . . . . . 10 ⊢ (((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn))
77	75, 76	bitrdi 287	. . . . . . . . 9 ⊢ (𝜑 → (((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn)))
78	17	ismbfcn2 25674	. . . . . . . . 9 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn)))
79	17, 57	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑦) / i) ∈ ℂ)
80	79	ismbfcn2 25674	. . . . . . . . 9 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn)))
81	77, 78, 80	3bitr4d 311	. . . . . . . 8 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn))
82	25, 81	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn)
83	23, 82	eqeltrrd 2841	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) ∈ MblFn)
84	16, 17, 19, 83	iblmulc2nc 37693	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) ∈ 𝐿1)
85		mulcl 11240	. . . . . . 7 ⊢ (((1 / i) ∈ ℂ ∧ (𝐹‘𝑦) ∈ ℂ) → ((1 / i) · (𝐹‘𝑦)) ∈ ℂ)
86	15, 17, 85	sylancr 587	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((1 / i) · (𝐹‘𝑦)) ∈ ℂ)
87	86	fmpttd 7134	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))):𝐷⟶ℂ)
88	12, 3, 4, 5, 6, 7, 84, 87	ftc1anclem5 37705	. . . 4 ⊢ ((𝜑 ∧ (𝑌 / 2) ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))
89	1, 88	sylan2 593	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))
90	9	ffvelcdmda 7103	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
91		0cnd 11255	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ)
92	90, 91	ifclda 4560	. . . . . . . . . . 11 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
93		imval 15147	. . . . . . . . . . 11 ⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i)))
94	92, 93	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i)))
95		fveq2 6905	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑡 → (𝐹‘𝑦) = (𝐹‘𝑡))
96	95	oveq2d 7448	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑡 → ((1 / i) · (𝐹‘𝑦)) = ((1 / i) · (𝐹‘𝑡)))
97		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) = (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))
98		ovex 7465	. . . . . . . . . . . . . . . 16 ⊢ ((1 / i) · (𝐹‘𝑡)) ∈ V
99	96, 97, 98	fvmpt 7015	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝐷 → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((1 / i) · (𝐹‘𝑡)))
100	99	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((1 / i) · (𝐹‘𝑡)))
101		divrec2 11940	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑡) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡)))
102	13, 14, 101	mp3an23 1454	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑡) ∈ ℂ → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡)))
103	90, 102	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡)))
104	100, 103	eqtr4d 2779	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((𝐹‘𝑡) / i))
105	104	ifeq1da 4556	. . . . . . . . . . . 12 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0))
106		ovif 7532	. . . . . . . . . . . . 13 ⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), (0 / i))
107	13, 14	div0i 12002	. . . . . . . . . . . . . 14 ⊢ (0 / i) = 0
108		ifeq2 4529	. . . . . . . . . . . . . 14 ⊢ ((0 / i) = 0 → if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), (0 / i)) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0))
109	107, 108	ax-mp 5	. . . . . . . . . . . . 13 ⊢ if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), (0 / i)) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0)
110	106, 109	eqtri 2764	. . . . . . . . . . . 12 ⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0)
111	105, 110	eqtr4di 2794	. . . . . . . . . . 11 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i))
112	111	fveq2d 6909	. . . . . . . . . 10 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i)))
113	94, 112	eqtr4d 2779	. . . . . . . . 9 ⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)))
114	113	fvoveq1d 7454	. . . . . . . 8 ⊢ (𝜑 → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))
115	114	mpteq2dv 5243	. . . . . . 7 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡)))))
116	115	fveq2d 6909	. . . . . 6 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))))
117	116	breq1d 5152	. . . . 5 ⊢ (𝜑 → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)))
118	117	rexbidv 3178	. . . 4 ⊢ (𝜑 → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)))
119	118	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)))
120	89, 119	mpbird 257	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))
121		reeanv 3228	. . 3 ⊢ (∃𝑓 ∈ 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 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (𝑥 ∈ 𝐷 ↔ 𝑡 ∈ 𝐷))
123		fveq2 6905	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (𝐹‘𝑥) = (𝐹‘𝑡))
124	122, 123	ifbieq1d 4549	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑡 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
125	124	fveq2d 6909	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑡 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
126		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))
127		fvex 6918	. . . . . . . . . . . . . 14 ⊢ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V
128	125, 126, 127	fvmpt 7015	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
129	128	fvoveq1d 7454	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℝ → (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))
130	129	mpteq2ia 5244	. . . . . . . . . . 11 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))
131	130	fveq2i 6908	. . . . . . . . . 10 ⊢ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))))
132		rembl 25576	. . . . . . . . . . . . . . . . 17 ⊢ ℝ ∈ dom vol
133	132	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℝ ∈ dom vol)
134		0cnd 11255	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐷) → 0 ∈ ℂ)
135	36, 134	ifclda 4560	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ)
136	135	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ)
137		eldifn 4131	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (ℝ ∖ 𝐷) → ¬ 𝑥 ∈ 𝐷)
138	137	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑥 ∈ 𝐷)
139	138	iffalsed 4535	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐷)) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0)
140	9	feqmptd 6976	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)))
141		iftrue 4530	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐷 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥))
142	141	mpteq2ia 5244	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥))
143	140, 142	eqtr4di 2794	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))
144	143, 8	eqeltrrd 2841	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ 𝐿1)
145	7, 133, 136, 139, 144	iblss2 25842	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ 𝐿1)
146	135	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ)
147	146	iblcn 25835	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ 𝐿1 ↔ ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1)))
148	145, 147	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1))
149	148	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1)
150	146	recld 15234	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ ℝ)
151	150	fmpttd 7134	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)
152	149, 151	jca 511	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ))
153		ftc1anclem4 37704	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ)
154	153	3expb 1120	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ)
155	152, 154	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝜑) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ)
156	155	ancoms 458	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ)
157	131, 156	eqeltrrid 2845	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ)
158	124	fveq2d 6909	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑡 → (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
159		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))
160		fvex 6918	. . . . . . . . . . . . . 14 ⊢ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V
161	158, 159, 160	fvmpt 7015	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
162	161	fvoveq1d 7454	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℝ → (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
163	162	mpteq2ia 5244	. . . . . . . . . . 11 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
164	163	fveq2i 6908	. . . . . . . . . 10 ⊢ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
165	148	simprd 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1)
166	135	imcld 15235	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ ℝ)
167	166	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ ℝ)
168	167	fmpttd 7134	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)
169	165, 168	jca 511	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ))
170		ftc1anclem4 37704	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ)
171	170	3expb 1120	. . . . . . . . . . . 12 ⊢ ((𝑔 ∈ dom ∫1 ∧ ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ)
172	169, 171	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝜑) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ)
173	172	ancoms 458	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ)
174	164, 173	eqeltrrid 2845	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ)
175	157, 174	anim12dan 619	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ))
176	1	rpred 13078	. . . . . . . . 9 ⊢ (𝑌 ∈ ℝ+ → (𝑌 / 2) ∈ ℝ)
177	176, 176	jca 511	. . . . . . . 8 ⊢ (𝑌 ∈ ℝ+ → ((𝑌 / 2) ∈ ℝ ∧ (𝑌 / 2) ∈ ℝ))
178		lt2add 11749	. . . . . . . 8 ⊢ ((((∫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 596	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ 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 652	. . . . . 6 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ 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 15234	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
182	181	recnd 11290	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ)
183		i1ff 25712	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → 𝑓:ℝ⟶ℝ)
184	183	ffvelcdmda 7103	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℝ)
185	184	recnd 11290	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℂ)
186		subcl 11508	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑓‘𝑡) ∈ ℂ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ)
187	182, 185, 186	syl2an 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ)
188	187	anassrs 467	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ)
189	188	adantlrr 721	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ)
190	92	imcld 15235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
191	190	recnd 11290	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ)
192		i1ff 25712	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
193	192	ffvelcdmda 7103	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℝ)
194	193	recnd 11290	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℂ)
195		subcl 11508	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ)
196	191, 194, 195	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ)
197	196	anassrs 467	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ)
198		mulcl 11240	. . . . . . . . . . . . . . . . 17 ⊢ ((i ∈ ℂ ∧ ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ)
199	13, 197, 198	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ)
200	199	adantlrl 720	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ)
201	189, 200	addcld 11281	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) ∈ ℂ)
202	201	abscld 15476	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ)
203	202	rexrd 11312	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ*)
204	201	absge0d 15484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
205		elxrge0 13498	. . . . . . . . . . . 12 ⊢ ((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 583	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ (0[,]+∞))
207	206	fmpttd 7134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))):ℝ⟶(0[,]+∞))
208		icossicc 13477	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
209		ge0addcl 13501	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,)+∞))
210	208, 209	sselid 3980	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,]+∞))
211	210	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,]+∞))
212	188	abscld 15476	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ ℝ)
213	188	absge0d 15484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))
214		elrege0 13495	. . . . . . . . . . . . . 14 ⊢ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ (0[,)+∞) ↔ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))))
215	212, 213, 214	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ (0[,)+∞))
216	215	fmpttd 7134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))):ℝ⟶(0[,)+∞))
217	216	adantrr 717	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))):ℝ⟶(0[,)+∞))
218	197	abscld 15476	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℝ)
219	197	absge0d 15484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
220		elrege0 13495	. . . . . . . . . . . . . 14 ⊢ ((abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ (0[,)+∞) ↔ ((abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
221	218, 219, 220	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ (0[,)+∞))
222	221	fmpttd 7134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))):ℝ⟶(0[,)+∞))
223	222	adantrl 716	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))):ℝ⟶(0[,)+∞))
224		reex 11247	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
225	224	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ℝ ∈ V)
226		inidm 4226	. . . . . . . . . . 11 ⊢ (ℝ ∩ ℝ) = ℝ
227	211, 217, 223, 225, 225, 226	off 7716	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))):ℝ⟶(0[,]+∞))
228	189, 200	abstrid 15496	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ≤ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
229	228	ralrimiva 3145	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ∀𝑡 ∈ ℝ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ≤ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
230		ovexd 7467	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ V)
231		eqidd 2737	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))))
232		fvexd 6920	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ V)
233		fvexd 6920	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) ∈ V)
234		eqidd 2737	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))))
235		absmul 15334	. . . . . . . . . . . . . . . . 17 ⊢ ((i ∈ ℂ ∧ ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) → (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = ((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
236	13, 197, 235	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = ((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
237		absi 15326	. . . . . . . . . . . . . . . . . 18 ⊢ (abs‘i) = 1
238	237	oveq1i 7442	. . . . . . . . . . . . . . . . 17 ⊢ ((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (1 · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
239	218	recnd 11290	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ)
240	239	mullidd 11280	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (1 · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
241	238, 240	eqtrid 2788	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
242	236, 241	eqtr2d 2777	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
243	242	mpteq2dva 5241	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
244	243	adantrl 716	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
245	225, 232, 233, 234, 244	offval2 7718	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ 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 7719	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ 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 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∘r ≤ ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
248		itg2le 25775	. . . . . . . . . 10 ⊢ (((𝑡 ∈ ℝ ↦ (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 1372	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ (∫2‘((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))))
250		absf 15377	. . . . . . . . . . . . . 14 ⊢ abs:ℂ⟶ℝ
251	250	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → abs:ℂ⟶ℝ)
252	251, 188	cofmpt 7151	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))))
253		resubcl 11574	. . . . . . . . . . . . . . . 16 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑓‘𝑡) ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ)
254	181, 184, 253	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ)
255	254	anassrs 467	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ)
256	255	fmpttd 7134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))):ℝ⟶ℝ)
257	132	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ℝ ∈ dom vol)
258		iunin2 5070	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦}))
259		imaiun 7266	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝑓 “ ∪ 𝑦 ∈ ran 𝑓{𝑦}) = ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})
260		iunid 5059	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑦 ∈ ran 𝑓{𝑦} = ran 𝑓
261	260	imaeq2i 6075	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝑓 “ ∪ 𝑦 ∈ ran 𝑓{𝑦}) = (◡𝑓 “ ran 𝑓)
262	259, 261	eqtr3i 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦}) = (◡𝑓 “ ran 𝑓)
263	262	ineq2i 4216	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓))
264	258, 263	eqtri 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓))
265		cnvimass 6099	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))
266		ovex 7465	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ V
267		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) = (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))
268	266, 267	dmmpti 6711	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) = ℝ
269	265, 268	sseqtri 4031	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ ℝ
270		cnvimarndm 6100	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝑓 “ ran 𝑓) = dom 𝑓
271	183	fdmd 6745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ dom ∫1 → dom 𝑓 = ℝ)
272	270, 271	eqtrid 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → (◡𝑓 “ ran 𝑓) = ℝ)
273	269, 272	sseqtrrid 4026	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ (◡𝑓 “ ran 𝑓))
274		dfss2 3968	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ (◡𝑓 “ ran 𝑓) ↔ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)))
275	273, 274	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)))
276	264, 275	eqtrid 2788	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ dom ∫1 → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)))
277	276	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)))
278	183	frnd 6743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ)
279	278	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ran 𝑓 ⊆ ℝ)
280	279	sselda 3982	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → 𝑦 ∈ ℝ)
281	181	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
282		resubcl 11574	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ)
283	181, 282	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ)
284	283	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ)
285	281, 284	2thd 265	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ))
286		ltaddsub 11738	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))
287	181, 286	syl3an3 1165	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝜑) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))
288	287	3comr 1125	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))
289	288	3expa 1118	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))
290	285, 289	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))))
291		readdcl 11239	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
292	291	rexrd 11312	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ*)
293	292	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ*)
294		elioopnf 13484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 + 𝑦) ∈ ℝ* → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
295	293, 294	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
296		rexr 11308	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
297	296	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℝ*)
298		elioopnf 13484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ* → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))))
299	297, 298	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))))
300	290, 295, 299	3bitr4rd 312	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)))
301		oveq2 7440	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓‘𝑡) = 𝑦 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))
302	301	eleq1d 2825	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞)))
303	302	bibi1d 343	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓‘𝑡) = 𝑦 → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞))))
304	300, 303	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞))))
305	304	pm5.32rd 578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)))
306	305	adantllr 719	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)))
307	280, 306	syldan 591	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)))
308	307	rabbidv 3443	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)} = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
309	183	feqmptd 6976	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ dom ∫1 → 𝑓 = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)))
310	309	cnveqd 5885	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ∈ dom ∫1 → ◡𝑓 = ◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)))
311	310	imaeq1d 6076	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ dom ∫1 → (◡𝑓 “ {𝑦}) = (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}))
312	311	ineq2d 4219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})))
313	267	mptpreima 6257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)}
314		vex 3483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑦 ∈ V
315		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡))
316	315	mptiniseg 6258	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ V → (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}) = {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
317	314, 316	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}) = {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}
318	313, 317	ineq12i 4217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
319		inrab 4315	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}
320	318, 319	eqtri 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}
321	312, 320	eqtrdi 2792	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
322	321	ad3antlr 731	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
323	311	ineq2d 4219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})))
324		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
325	324	mptpreima 6257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) = {𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)}
326	325, 317	ineq12i 4217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
327		inrab 4315	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}
328	326, 327	eqtri 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}
329	323, 328	eqtrdi 2792	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
330	329	ad3antlr 731	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
331	308, 322, 330	3eqtr4d 2786	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})))
332	331	iuneq2dv 5015	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})))
333	277, 332	eqtr3d 2778	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) = ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})))
334		i1frn 25713	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin)
335	334	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ran 𝑓 ∈ Fin)
336	92	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
337		eldifn 4131	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷)
338	337	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷)
339	338	iffalsed 4535	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = 0)
340	9	feqmptd 6976	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
341		iftrue 4530	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = (𝐹‘𝑡))
342	341	mpteq2ia 5244	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡))
343	340, 342	eqtr4di 2794	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
344		iblmbf 25803	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)
345	8, 344	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹 ∈ MblFn)
346	343, 345	eqeltrrd 2841	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn)
347	7, 133, 336, 339, 346	mbfss 25682	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn)
348	92	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
349	348	ismbfcn2 25674	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn ↔ ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)))
350	347, 349	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn))
351	350	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)
352	181	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
353	352	fmpttd 7134	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ)
354		mbfima 25666	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ) → (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol)
355	351, 353, 354	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol)
356		i1fima 25714	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (◡𝑓 “ {𝑦}) ∈ dom vol)
357		inmbl 25578	. . . . . . . . . . . . . . . . . . 19 ⊢ (((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol ∧ (◡𝑓 “ {𝑦}) ∈ dom vol) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
358	355, 356, 357	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
359	358	ralrimivw 3149	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
360		finiunmbl 25580	. . . . . . . . . . . . . . . . 17 ⊢ ((ran 𝑓 ∈ Fin ∧ ∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
361	335, 359, 360	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
362	361	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
363	333, 362	eqeltrd 2840	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∈ dom vol)
364		iunin2 5070	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦}))
365	262	ineq2i 4216	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓))
366	364, 365	eqtri 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓))
367		cnvimass 6099	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))
368	367, 268	sseqtri 4031	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ ℝ
369	368, 272	sseqtrrid 4026	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ (◡𝑓 “ ran 𝑓))
370		dfss2 3968	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ (◡𝑓 “ ran 𝑓) ↔ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)))
371	369, 370	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)))
372	366, 371	eqtrid 2788	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ dom ∫1 → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)))
373	372	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)))
374	284, 281	2thd 265	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ))
375		ltsubadd 11734	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))
376	181, 375	syl3an1 1163	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))
377	376	3expa 1118	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))
378	377	an32s 652	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))
379	374, 378	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))))
380		elioomnf 13485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ* → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥)))
381	297, 380	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥)))
382		elioomnf 13485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 + 𝑦) ∈ ℝ* → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))))
383	293, 382	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))))
384	379, 381, 383	3bitr4d 311	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))))
385	301	eleq1d 2825	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥)))
386	385	bibi1d 343	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓‘𝑡) = 𝑦 → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)))))
387	384, 386	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)))))
388	387	pm5.32rd 578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)))
389	388	adantllr 719	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)))
390	280, 389	syldan 591	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)))
391	390	rabbidv 3443	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)} = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)})
392	311	ineq2d 4219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})))
393	267	mptpreima 6257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)}
394	393, 317	ineq12i 4217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
395		inrab 4315	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)}
396	394, 395	eqtri 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)}
397	392, 396	eqtrdi 2792	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)})
398	397	ad3antlr 731	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)})
399	311	ineq2d 4219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})))
400	324	mptpreima 6257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) = {𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))}
401	400, 317	ineq12i 4217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
402		inrab 4315	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)}
403	401, 402	eqtri 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)}
404	399, 403	eqtrdi 2792	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)})
405	404	ad3antlr 731	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)})
406	391, 398, 405	3eqtr4d 2786	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})))
407	406	iuneq2dv 5015	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})))
408	373, 407	eqtr3d 2778	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) = ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})))
409		mbfima 25666	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ) → (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol)
410	351, 353, 409	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol)
411		inmbl 25578	. . . . . . . . . . . . . . . . . . 19 ⊢ (((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol ∧ (◡𝑓 “ {𝑦}) ∈ dom vol) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
412	410, 356, 411	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
413	412	ralrimivw 3149	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
414		finiunmbl 25580	. . . . . . . . . . . . . . . . 17 ⊢ ((ran 𝑓 ∈ Fin ∧ ∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
415	335, 413, 414	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
416	415	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
417	408, 416	eqeltrd 2840	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∈ dom vol)
418	256, 257, 363, 417	ismbf2d 25676	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ MblFn)
419		ftc1anclem1 37701	. . . . . . . . . . . . 13 ⊢ (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn)
420	256, 418, 419	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn)
421	252, 420	eqeltrrd 2841	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn)
422	421	adantrr 717	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn)
423	157	adantrr 717	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ)
424	174	adantrl 716	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ)
425	422, 217, 423, 223, 424	itg2addnc 37682	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))))
426	249, 425	breqtrd 5168	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))))
427	426	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))))
428		itg2cl 25768	. . . . . . . . . 10 ⊢ ((𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ∈ ℝ*)
429	207, 428	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ∈ ℝ*)
430	429	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ∈ ℝ*)
431		readdcl 11239	. . . . . . . . . . . 12 ⊢ (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ)
432	157, 174, 431	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ (𝜑 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ)
433	432	anandis 678	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ)
434	433	rexrd 11312	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ*)
435	434	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ*)
436	1, 1	rpaddcld 13093	. . . . . . . . . 10 ⊢ (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ+)
437	436	rpxrd 13079	. . . . . . . . 9 ⊢ (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ*)
438	437	ad2antlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ*)
439		xrlelttr 13199	. . . . . . . 8 ⊢ (((∫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 1372	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ 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 695	. . . . . 6 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ 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 47	. . . . 5 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ 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 11240	. . . . . . . . . . . . . . 15 ⊢ ((i ∈ ℂ ∧ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ) → (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ)
444	13, 191, 443	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ)
445	182, 444	jca 511	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ))
446		mulcl 11240	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ)
447	13, 194, 446	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ)
448	185, 447	anim12i 613	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ))
449	448	anandirs 679	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ))
450		addsub4 11553	. . . . . . . . . . . . 13 ⊢ ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) ∧ ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ)) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))))
451	445, 449, 450	syl2an 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ)) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))))
452	451	anassrs 467	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))))
453	92	replimd 15237	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
454	453	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
455	454	oveq1d 7447	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
456	194	adantll 714	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℂ)
457		subdi 11697	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))
458	13, 191, 456, 457	mp3an3an 1468	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ)) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))
459	458	anassrs 467	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))
460	459	oveq2d 7448	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))))
461	452, 455, 460	3eqtr4rd 2787	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
462	461	fveq2d 6909	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) = (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
463	462	mpteq2dva 5241	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
464	463	fveq2d 6909	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))))
465	464	adantlr 715	. . . . . 6 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))))
466		rpcn 13046	. . . . . . . 8 ⊢ (𝑌 ∈ ℝ+ → 𝑌 ∈ ℂ)
467	466	2halvesd 12514	. . . . . . 7 ⊢ (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) = 𝑌)
468	467	ad2antlr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑌 / 2) + (𝑌 / 2)) = 𝑌)
469	465, 468	breq12d 5155	. . . . 5 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2)) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌))
470	442, 469	sylibd 239	. . . 4 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌))
471	470	reximdvva 3206	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∃𝑓 ∈ 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 243	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ((∃𝑓 ∈ 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 699	1 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   ≠ wne 2939  ∀wral 3060  ∃wrex 3069  {crab 3435  Vcvv 3479   ∖ cdif 3947   ∩ cin 3949   ⊆ wss 3950  ifcif 4524  {csn 4625  ∪ ciun 4990   class class class wbr 5142   ↦ cmpt 5224  ^◡ccnv 5683  dom cdm 5684  ran crn 5685   “ cima 5687   ∘ ccom 5688  ⟶wf 6556  ‘cfv 6560  (class class class)co 7432   ∘_f cof 7696   ∘_r cofr 7697  Fincfn 8986  ℂcc 11154  ℝcr 11155  0cc0 11156  1c1 11157  ici 11158   + caddc 11159   · cmul 11161  +∞cpnf 11293  -∞cmnf 11294  ℝ^*cxr 11295   < clt 11296   ≤ cle 11297   − cmin 11493  -cneg 11494   / cdiv 11921  2c2 12322  ℝ⁺crp 13035  (,)cioo 13388  [,)cico 13390  [,]cicc 13391  ℜcre 15137  ℑcim 15138  abscabs 15274  volcvol 25499  MblFncmbf 25650  ∫₁citg1 25651  ∫₂citg2 25652  𝐿¹cibl 25653  ∫citg 25654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-inf2 9682  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233  ax-pre-sup 11234  ax-addf 11235

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-disj 5110  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-of 7698  df-ofr 7699  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-er 8746  df-map 8869  df-pm 8870  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-fi 9452  df-sup 9483  df-inf 9484  df-oi 9551  df-dju 9942  df-card 9980  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-div 11922  df-nn 12268  df-2 12330  df-3 12331  df-4 12332  df-n0 12529  df-z 12616  df-uz 12880  df-q 12992  df-rp 13036  df-xneg 13155  df-xadd 13156  df-xmul 13157  df-ioo 13392  df-ico 13394  df-icc 13395  df-fz 13549  df-fzo 13696  df-fl 13833  df-mod 13911  df-seq 14044  df-exp 14104  df-hash 14371  df-cj 15139  df-re 15140  df-im 15141  df-sqrt 15275  df-abs 15276  df-clim 15525  df-sum 15724  df-rest 17468  df-topgen 17489  df-psmet 21357  df-xmet 21358  df-met 21359  df-bl 21360  df-mopn 21361  df-top 22901  df-topon 22918  df-bases 22954  df-cmp 23396  df-ovol 25500  df-vol 25501  df-mbf 25655  df-itg1 25656  df-itg2 25657  df-ibl 25658  df-0p 25706

This theorem is referenced by:  ftc1anc  37709