Theorem ftc1anclem6 35549

Description: Lemma for ftc1anc 35552- 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 12596	. . 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 35548	. . 3 ⊢ ((𝜑 ∧ (𝑌 / 2) ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2))
11	1, 10	sylan2 596	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2))
12		eqid 2734	. . . . 5 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) d𝑡) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) d𝑡)
13		ax-icn 10771	. . . . . . . 8 ⊢ i ∈ ℂ
14		ine0 11250	. . . . . . . 8 ⊢ i ≠ 0
15	13, 14	reccli 11545	. . . . . . 7 ⊢ (1 / i) ∈ ℂ
16	15	a1i 11	. . . . . 6 ⊢ (𝜑 → (1 / i) ∈ ℂ)
17	9	ffvelrnda 6893	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐹‘𝑦) ∈ ℂ)
18	9	feqmptd 6769	. . . . . . 7 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)))
19	18, 8	eqeltrrd 2835	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ 𝐿1)
20		divrec2 11490	. . . . . . . . . 10 ⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦)))
21	13, 14, 20	mp3an23 1455	. . . . . . . . 9 ⊢ ((𝐹‘𝑦) ∈ ℂ → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦)))
22	17, 21	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦)))
23	22	mpteq2dva 5139	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) = (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))))
24		iblmbf 24637	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ 𝐿1 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn)
25	19, 24	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn)
26		2fveq3 6711	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (ℜ‘(𝐹‘𝑦)) = (ℜ‘(𝐹‘𝑥)))
27	26	cbvmptv 5147	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) = (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥)))
28	27	eleq1i 2824	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn)
29	17	recld 14740	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℝ)
30	29	recnd 10844	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℂ)
31	30	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℂ)
32	28	biimpri 231	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn → (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn)
33	32	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn)
34	31, 33	mbfneg 24519	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn)
35	28, 34	sylan2b 597	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn)
36	9	ffvelrnda 6893	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐹‘𝑥) ∈ ℂ)
37	36	recld 14740	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (ℜ‘(𝐹‘𝑥)) ∈ ℝ)
38	37	recnd 10844	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (ℜ‘(𝐹‘𝑥)) ∈ ℂ)
39	38	negnegd 11163	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → --(ℜ‘(𝐹‘𝑥)) = (ℜ‘(𝐹‘𝑥)))
40	39	mpteq2dva 5139	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))))
41	40, 27	eqtr4di 2792	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))))
42	41	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))))
43		negex 11059	. . . . . . . . . . . . . . . 16 ⊢ -(ℜ‘(𝐹‘𝑥)) ∈ V
44	43	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) ∧ 𝑥 ∈ 𝐷) → -(ℜ‘(𝐹‘𝑥)) ∈ V)
45	26	negeqd 11055	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → -(ℜ‘(𝐹‘𝑦)) = -(ℜ‘(𝐹‘𝑥)))
46	45	cbvmptv 5147	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) = (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥)))
47	46	eleq1i 2824	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) ∈ MblFn)
48	47	biimpi 219	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn → (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) ∈ MblFn)
49	48	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) ∈ MblFn)
50	44, 49	mbfneg 24519	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) ∈ MblFn)
51	42, 50	eqeltrrd 2835	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn)
52	35, 51	impbida 801	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn))
53		divcl 11479	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹‘𝑦) / i) ∈ ℂ)
54		imre 14654	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑦) / i) ∈ ℂ → (ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i))))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → (ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i))))
56	13, 14, 55	mp3an23 1455	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i))))
57	13, 14, 53	mp3an23 1455	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑦) ∈ ℂ → ((𝐹‘𝑦) / i) ∈ ℂ)
58		mulneg1 11251	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i ∈ ℂ ∧ ((𝐹‘𝑦) / i) ∈ ℂ) → (-i · ((𝐹‘𝑦) / i)) = -(i · ((𝐹‘𝑦) / i)))
59	13, 57, 58	sylancr 590	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) ∈ ℂ → (-i · ((𝐹‘𝑦) / i)) = -(i · ((𝐹‘𝑦) / i)))
60		divcan2 11481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → (i · ((𝐹‘𝑦) / i)) = (𝐹‘𝑦))
61	13, 14, 60	mp3an23 1455	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑦) ∈ ℂ → (i · ((𝐹‘𝑦) / i)) = (𝐹‘𝑦))
62	61	negeqd 11055	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) ∈ ℂ → -(i · ((𝐹‘𝑦) / i)) = -(𝐹‘𝑦))
63	59, 62	eqtrd 2774	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑦) ∈ ℂ → (-i · ((𝐹‘𝑦) / i)) = -(𝐹‘𝑦))
64	63	fveq2d 6710	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℜ‘(-i · ((𝐹‘𝑦) / i))) = (ℜ‘-(𝐹‘𝑦)))
65		reneg 14671	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℜ‘-(𝐹‘𝑦)) = -(ℜ‘(𝐹‘𝑦)))
66	56, 64, 65	3eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℑ‘((𝐹‘𝑦) / i)) = -(ℜ‘(𝐹‘𝑦)))
67	17, 66	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℑ‘((𝐹‘𝑦) / i)) = -(ℜ‘(𝐹‘𝑦)))
68	67	mpteq2dva 5139	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) = (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))))
69	68	eleq1d 2818	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn))
70	52, 69	bitr4d 285	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn))
71		imval 14653	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℑ‘(𝐹‘𝑦)) = (ℜ‘((𝐹‘𝑦) / i)))
72	17, 71	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℑ‘(𝐹‘𝑦)) = (ℜ‘((𝐹‘𝑦) / i)))
73	72	mpteq2dva 5139	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))))
74	73	eleq1d 2818	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn))
75	70, 74	anbi12d 634	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn)))
76		ancom 464	. . . . . . . . . 10 ⊢ (((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn))
77	75, 76	bitrdi 290	. . . . . . . . 9 ⊢ (𝜑 → (((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn)))
78	17	ismbfcn2 24507	. . . . . . . . 9 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn)))
79	17, 57	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑦) / i) ∈ ℂ)
80	79	ismbfcn2 24507	. . . . . . . . 9 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn)))
81	77, 78, 80	3bitr4d 314	. . . . . . . 8 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn))
82	25, 81	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn)
83	23, 82	eqeltrrd 2835	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) ∈ MblFn)
84	16, 17, 19, 83	iblmulc2nc 35536	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) ∈ 𝐿1)
85		mulcl 10796	. . . . . . 7 ⊢ (((1 / i) ∈ ℂ ∧ (𝐹‘𝑦) ∈ ℂ) → ((1 / i) · (𝐹‘𝑦)) ∈ ℂ)
86	15, 17, 85	sylancr 590	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((1 / i) · (𝐹‘𝑦)) ∈ ℂ)
87	86	fmpttd 6921	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))):𝐷⟶ℂ)
88	12, 3, 4, 5, 6, 7, 84, 87	ftc1anclem5 35548	. . . 4 ⊢ ((𝜑 ∧ (𝑌 / 2) ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))
89	1, 88	sylan2 596	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))
90	9	ffvelrnda 6893	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
91		0cnd 10809	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ)
92	90, 91	ifclda 4464	. . . . . . . . . . 11 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
93		imval 14653	. . . . . . . . . . 11 ⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i)))
94	92, 93	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i)))
95		fveq2 6706	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑡 → (𝐹‘𝑦) = (𝐹‘𝑡))
96	95	oveq2d 7218	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑡 → ((1 / i) · (𝐹‘𝑦)) = ((1 / i) · (𝐹‘𝑡)))
97		eqid 2734	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) = (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))
98		ovex 7235	. . . . . . . . . . . . . . . 16 ⊢ ((1 / i) · (𝐹‘𝑡)) ∈ V
99	96, 97, 98	fvmpt 6807	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝐷 → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((1 / i) · (𝐹‘𝑡)))
100	99	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((1 / i) · (𝐹‘𝑡)))
101		divrec2 11490	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑡) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡)))
102	13, 14, 101	mp3an23 1455	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑡) ∈ ℂ → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡)))
103	90, 102	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡)))
104	100, 103	eqtr4d 2777	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((𝐹‘𝑡) / i))
105	104	ifeq1da 4460	. . . . . . . . . . . 12 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0))
106		ovif 7297	. . . . . . . . . . . . 13 ⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), (0 / i))
107	13, 14	div0i 11549	. . . . . . . . . . . . . 14 ⊢ (0 / i) = 0
108		ifeq2 4434	. . . . . . . . . . . . . 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 2762	. . . . . . . . . . . 12 ⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0)
111	105, 110	eqtr4di 2792	. . . . . . . . . . 11 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i))
112	111	fveq2d 6710	. . . . . . . . . 10 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i)))
113	94, 112	eqtr4d 2777	. . . . . . . . 9 ⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)))
114	113	fvoveq1d 7224	. . . . . . . 8 ⊢ (𝜑 → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))
115	114	mpteq2dv 5140	. . . . . . 7 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡)))))
116	115	fveq2d 6710	. . . . . 6 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))))
117	116	breq1d 5053	. . . . 5 ⊢ (𝜑 → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)))
118	117	rexbidv 3209	. . . 4 ⊢ (𝜑 → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)))
119	118	adantr 484	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)))
120	89, 119	mpbird 260	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))
121		reeanv 3272	. . 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 2816	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (𝑥 ∈ 𝐷 ↔ 𝑡 ∈ 𝐷))
123		fveq2 6706	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (𝐹‘𝑥) = (𝐹‘𝑡))
124	122, 123	ifbieq1d 4453	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑡 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
125	124	fveq2d 6710	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑡 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
126		eqid 2734	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))
127		fvex 6719	. . . . . . . . . . . . . 14 ⊢ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V
128	125, 126, 127	fvmpt 6807	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
129	128	fvoveq1d 7224	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℝ → (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))
130	129	mpteq2ia 5135	. . . . . . . . . . 11 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))
131	130	fveq2i 6709	. . . . . . . . . 10 ⊢ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))))
132		rembl 24409	. . . . . . . . . . . . . . . . 17 ⊢ ℝ ∈ dom vol
133	132	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℝ ∈ dom vol)
134		0cnd 10809	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐷) → 0 ∈ ℂ)
135	36, 134	ifclda 4464	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ)
136	135	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ)
137		eldifn 4032	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (ℝ ∖ 𝐷) → ¬ 𝑥 ∈ 𝐷)
138	137	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑥 ∈ 𝐷)
139	138	iffalsed 4440	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐷)) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0)
140	9	feqmptd 6769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)))
141		iftrue 4435	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐷 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥))
142	141	mpteq2ia 5135	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥))
143	140, 142	eqtr4di 2792	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))
144	143, 8	eqeltrrd 2835	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ 𝐿1)
145	7, 133, 136, 139, 144	iblss2 24675	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ 𝐿1)
146	135	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ)
147	146	iblcn 24668	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ 𝐿1 ↔ ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1)))
148	145, 147	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1))
149	148	simpld 498	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1)
150	146	recld 14740	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ ℝ)
151	150	fmpttd 6921	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)
152	149, 151	jca 515	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ))
153		ftc1anclem4 35547	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ)
154	153	3expb 1122	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ)
155	152, 154	sylan2 596	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝜑) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ)
156	155	ancoms 462	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ)
157	131, 156	eqeltrrid 2839	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ)
158	124	fveq2d 6710	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑡 → (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
159		eqid 2734	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))
160		fvex 6719	. . . . . . . . . . . . . 14 ⊢ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V
161	158, 159, 160	fvmpt 6807	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
162	161	fvoveq1d 7224	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℝ → (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
163	162	mpteq2ia 5135	. . . . . . . . . . 11 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
164	163	fveq2i 6709	. . . . . . . . . 10 ⊢ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
165	148	simprd 499	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1)
166	135	imcld 14741	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ ℝ)
167	166	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ ℝ)
168	167	fmpttd 6921	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)
169	165, 168	jca 515	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ))
170		ftc1anclem4 35547	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ)
171	170	3expb 1122	. . . . . . . . . . . 12 ⊢ ((𝑔 ∈ dom ∫1 ∧ ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ)
172	169, 171	sylan2 596	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝜑) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ)
173	172	ancoms 462	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ)
174	164, 173	eqeltrrid 2839	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ)
175	157, 174	anim12dan 622	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ))
176	1	rpred 12611	. . . . . . . . 9 ⊢ (𝑌 ∈ ℝ+ → (𝑌 / 2) ∈ ℝ)
177	176, 176	jca 515	. . . . . . . 8 ⊢ (𝑌 ∈ ℝ+ → ((𝑌 / 2) ∈ ℝ ∧ (𝑌 / 2) ∈ ℝ))
178		lt2add 11300	. . . . . . . 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 599	. . . . . . 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 14740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
182	181	recnd 10844	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ)
183		i1ff 24545	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → 𝑓:ℝ⟶ℝ)
184	183	ffvelrnda 6893	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℝ)
185	184	recnd 10844	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℂ)
186		subcl 11060	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑓‘𝑡) ∈ ℂ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ)
187	182, 185, 186	syl2an 599	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ)
188	187	anassrs 471	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ)
189	188	adantlrr 721	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ)
190	92	imcld 14741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
191	190	recnd 10844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ)
192		i1ff 24545	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
193	192	ffvelrnda 6893	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℝ)
194	193	recnd 10844	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℂ)
195		subcl 11060	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ)
196	191, 194, 195	syl2an 599	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ)
197	196	anassrs 471	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ)
198		mulcl 10796	. . . . . . . . . . . . . . . . 17 ⊢ ((i ∈ ℂ ∧ ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ)
199	13, 197, 198	sylancr 590	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ)
200	199	adantlrl 720	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ)
201	189, 200	addcld 10835	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) ∈ ℂ)
202	201	abscld 14983	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ)
203	202	rexrd 10866	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ*)
204	201	absge0d 14991	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
205		elxrge0 13028	. . . . . . . . . . . 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 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ (0[,]+∞))
207	206	fmpttd 6921	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))):ℝ⟶(0[,]+∞))
208		icossicc 13007	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
209		ge0addcl 13031	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,)+∞))
210	208, 209	sseldi 3889	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,]+∞))
211	210	adantl 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,]+∞))
212	188	abscld 14983	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ ℝ)
213	188	absge0d 14991	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))
214		elrege0 13025	. . . . . . . . . . . . . 14 ⊢ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ (0[,)+∞) ↔ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))))
215	212, 213, 214	sylanbrc 586	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ (0[,)+∞))
216	215	fmpttd 6921	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))):ℝ⟶(0[,)+∞))
217	216	adantrr 717	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))):ℝ⟶(0[,)+∞))
218	197	abscld 14983	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℝ)
219	197	absge0d 14991	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
220		elrege0 13025	. . . . . . . . . . . . . 14 ⊢ ((abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ (0[,)+∞) ↔ ((abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
221	218, 219, 220	sylanbrc 586	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ (0[,)+∞))
222	221	fmpttd 6921	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))):ℝ⟶(0[,)+∞))
223	222	adantrl 716	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))):ℝ⟶(0[,)+∞))
224		reex 10803	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
225	224	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ℝ ∈ V)
226		inidm 4123	. . . . . . . . . . 11 ⊢ (ℝ ∩ ℝ) = ℝ
227	211, 217, 223, 225, 225, 226	off 7475	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))):ℝ⟶(0[,]+∞))
228	189, 200	abstrid 15003	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ≤ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
229	228	ralrimiva 3098	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ∀𝑡 ∈ ℝ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ≤ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
230		ovexd 7237	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ V)
231		eqidd 2735	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))))
232		fvexd 6721	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ V)
233		fvexd 6721	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) ∈ V)
234		eqidd 2735	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))))
235		absmul 14841	. . . . . . . . . . . . . . . . 17 ⊢ ((i ∈ ℂ ∧ ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) → (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = ((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
236	13, 197, 235	sylancr 590	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = ((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
237		absi 14833	. . . . . . . . . . . . . . . . . 18 ⊢ (abs‘i) = 1
238	237	oveq1i 7212	. . . . . . . . . . . . . . . . 17 ⊢ ((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (1 · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
239	218	recnd 10844	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ)
240	239	mulid2d 10834	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (1 · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
241	238, 240	syl5eq 2786	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
242	236, 241	eqtr2d 2775	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
243	242	mpteq2dva 5139	. . . . . . . . . . . . . 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 7477	. . . . . . . . . . . 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 7478	. . . . . . . . . . 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 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∘r ≤ ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
248		itg2le 24609	. . . . . . . . . 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 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ (∫2‘((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))))
250		absf 14884	. . . . . . . . . . . . . 14 ⊢ abs:ℂ⟶ℝ
251	250	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → abs:ℂ⟶ℝ)
252	251, 188	cofmpt 6936	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))))
253		resubcl 11125	. . . . . . . . . . . . . . . 16 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑓‘𝑡) ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ)
254	181, 184, 253	syl2an 599	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ)
255	254	anassrs 471	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ)
256	255	fmpttd 6921	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))):ℝ⟶ℝ)
257	132	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ℝ ∈ dom vol)
258		iunin2 4969	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦}))
259		imaiun 7047	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝑓 “ ∪ 𝑦 ∈ ran 𝑓{𝑦}) = ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})
260		iunid 4959	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑦 ∈ ran 𝑓{𝑦} = ran 𝑓
261	260	imaeq2i 5916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝑓 “ ∪ 𝑦 ∈ ran 𝑓{𝑦}) = (◡𝑓 “ ran 𝑓)
262	259, 261	eqtr3i 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦}) = (◡𝑓 “ ran 𝑓)
263	262	ineq2i 4114	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓))
264	258, 263	eqtri 2762	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓))
265		cnvimass 5938	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))
266		ovex 7235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ V
267		eqid 2734	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) = (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))
268	266, 267	dmmpti 6511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) = ℝ
269	265, 268	sseqtri 3927	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ ℝ
270		cnvimarndm 5939	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝑓 “ ran 𝑓) = dom 𝑓
271	183	fdmd 6545	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ dom ∫1 → dom 𝑓 = ℝ)
272	270, 271	syl5eq 2786	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → (◡𝑓 “ ran 𝑓) = ℝ)
273	269, 272	sseqtrrid 3944	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ (◡𝑓 “ ran 𝑓))
274		df-ss 3874	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ (◡𝑓 “ ran 𝑓) ↔ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)))
275	273, 274	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)))
276	264, 275	syl5eq 2786	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ dom ∫1 → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)))
277	276	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)))
278	183	frnd 6542	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ)
279	278	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ran 𝑓 ⊆ ℝ)
280	279	sselda 3891	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → 𝑦 ∈ ℝ)
281	181	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
282		resubcl 11125	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ)
283	181, 282	sylan 583	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ)
284	283	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ)
285	281, 284	2thd 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ))
286		ltaddsub 11289	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))
287	181, 286	syl3an3 1167	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝜑) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))
288	287	3comr 1127	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))
289	288	3expa 1120	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))
290	285, 289	anbi12d 634	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))))
291		readdcl 10795	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
292	291	rexrd 10866	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ*)
293	292	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ*)
294		elioopnf 13014	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 + 𝑦) ∈ ℝ* → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
295	293, 294	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
296		rexr 10862	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
297	296	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℝ*)
298		elioopnf 13014	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ* → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))))
299	297, 298	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))))
300	290, 295, 299	3bitr4rd 315	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)))
301		oveq2 7210	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓‘𝑡) = 𝑦 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))
302	301	eleq1d 2818	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞)))
303	302	bibi1d 347	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓‘𝑡) = 𝑦 → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞))))
304	300, 303	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞))))
305	304	pm5.32rd 581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)))
306	305	adantllr 719	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)))
307	280, 306	syldan 594	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)))
308	307	rabbidv 3383	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)} = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
309	183	feqmptd 6769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ dom ∫1 → 𝑓 = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)))
310	309	cnveqd 5733	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ∈ dom ∫1 → ◡𝑓 = ◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)))
311	310	imaeq1d 5917	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ dom ∫1 → (◡𝑓 “ {𝑦}) = (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}))
312	311	ineq2d 4117	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})))
313	267	mptpreima 6090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)}
314		vex 3405	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑦 ∈ V
315		eqid 2734	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡))
316	315	mptiniseg 6091	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ V → (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}) = {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
317	314, 316	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}) = {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}
318	313, 317	ineq12i 4115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
319		inrab 4211	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}
320	318, 319	eqtri 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}
321	312, 320	eqtrdi 2790	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
322	321	ad3antlr 731	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
323	311	ineq2d 4117	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})))
324		eqid 2734	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
325	324	mptpreima 6090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) = {𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)}
326	325, 317	ineq12i 4115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
327		inrab 4211	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}
328	326, 327	eqtri 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}
329	323, 328	eqtrdi 2790	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
330	329	ad3antlr 731	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
331	308, 322, 330	3eqtr4d 2784	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})))
332	331	iuneq2dv 4918	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})))
333	277, 332	eqtr3d 2776	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) = ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})))
334		i1frn 24546	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin)
335	334	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ran 𝑓 ∈ Fin)
336	92	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
337		eldifn 4032	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷)
338	337	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷)
339	338	iffalsed 4440	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = 0)
340	9	feqmptd 6769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
341		iftrue 4435	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = (𝐹‘𝑡))
342	341	mpteq2ia 5135	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡))
343	340, 342	eqtr4di 2792	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
344		iblmbf 24637	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)
345	8, 344	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹 ∈ MblFn)
346	343, 345	eqeltrrd 2835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn)
347	7, 133, 336, 339, 346	mbfss 24515	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn)
348	92	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
349	348	ismbfcn2 24507	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn ↔ ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)))
350	347, 349	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn))
351	350	simpld 498	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)
352	181	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
353	352	fmpttd 6921	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ)
354		mbfima 24499	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ) → (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol)
355	351, 353, 354	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol)
356		i1fima 24547	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (◡𝑓 “ {𝑦}) ∈ dom vol)
357		inmbl 24411	. . . . . . . . . . . . . . . . . . 19 ⊢ (((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol ∧ (◡𝑓 “ {𝑦}) ∈ dom vol) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
358	355, 356, 357	syl2an 599	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
359	358	ralrimivw 3099	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
360		finiunmbl 24413	. . . . . . . . . . . . . . . . 17 ⊢ ((ran 𝑓 ∈ Fin ∧ ∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
361	335, 359, 360	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
362	361	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
363	333, 362	eqeltrd 2834	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∈ dom vol)
364		iunin2 4969	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦}))
365	262	ineq2i 4114	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓))
366	364, 365	eqtri 2762	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓))
367		cnvimass 5938	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))
368	367, 268	sseqtri 3927	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ ℝ
369	368, 272	sseqtrrid 3944	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ (◡𝑓 “ ran 𝑓))
370		df-ss 3874	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ (◡𝑓 “ ran 𝑓) ↔ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)))
371	369, 370	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)))
372	366, 371	syl5eq 2786	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ dom ∫1 → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)))
373	372	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)))
374	284, 281	2thd 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ))
375		ltsubadd 11285	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))
376	181, 375	syl3an1 1165	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))
377	376	3expa 1120	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))
378	377	an32s 652	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))
379	374, 378	anbi12d 634	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))))
380		elioomnf 13015	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ* → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥)))
381	297, 380	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥)))
382		elioomnf 13015	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 + 𝑦) ∈ ℝ* → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))))
383	293, 382	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))))
384	379, 381, 383	3bitr4d 314	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))))
385	301	eleq1d 2818	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥)))
386	385	bibi1d 347	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓‘𝑡) = 𝑦 → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)))))
387	384, 386	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)))))
388	387	pm5.32rd 581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)))
389	388	adantllr 719	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)))
390	280, 389	syldan 594	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)))
391	390	rabbidv 3383	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)} = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)})
392	311	ineq2d 4117	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})))
393	267	mptpreima 6090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)}
394	393, 317	ineq12i 4115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
395		inrab 4211	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)}
396	394, 395	eqtri 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)}
397	392, 396	eqtrdi 2790	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)})
398	397	ad3antlr 731	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)})
399	311	ineq2d 4117	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})))
400	324	mptpreima 6090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) = {𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))}
401	400, 317	ineq12i 4115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
402		inrab 4211	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)}
403	401, 402	eqtri 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)}
404	399, 403	eqtrdi 2790	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)})
405	404	ad3antlr 731	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)})
406	391, 398, 405	3eqtr4d 2784	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})))
407	406	iuneq2dv 4918	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})))
408	373, 407	eqtr3d 2776	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) = ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})))
409		mbfima 24499	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ) → (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol)
410	351, 353, 409	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol)
411		inmbl 24411	. . . . . . . . . . . . . . . . . . 19 ⊢ (((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol ∧ (◡𝑓 “ {𝑦}) ∈ dom vol) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
412	410, 356, 411	syl2an 599	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
413	412	ralrimivw 3099	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
414		finiunmbl 24413	. . . . . . . . . . . . . . . . 17 ⊢ ((ran 𝑓 ∈ Fin ∧ ∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
415	335, 413, 414	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
416	415	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
417	408, 416	eqeltrd 2834	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∈ dom vol)
418	256, 257, 363, 417	ismbf2d 24509	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ MblFn)
419		ftc1anclem1 35544	. . . . . . . . . . . . 13 ⊢ (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn)
420	256, 418, 419	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn)
421	252, 420	eqeltrrd 2835	. . . . . . . . . . 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 35525	. . . . . . . . 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 5069	. . . . . . . 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 24602	. . . . . . . . . 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 10795	. . . . . . . . . . . 12 ⊢ (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ)
432	157, 174, 431	syl2an 599	. . . . . . . . . . 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 10866	. . . . . . . . 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 12626	. . . . . . . . . 10 ⊢ (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ+)
437	436	rpxrd 12612	. . . . . . . . 9 ⊢ (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ*)
438	437	ad2antlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ*)
439		xrlelttr 12729	. . . . . . . 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 1373	. . . . . . 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 10796	. . . . . . . . . . . . . . 15 ⊢ ((i ∈ ℂ ∧ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ) → (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ)
444	13, 191, 443	sylancr 590	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ)
445	182, 444	jca 515	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ))
446		mulcl 10796	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ)
447	13, 194, 446	sylancr 590	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ)
448	185, 447	anim12i 616	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ))
449	448	anandirs 679	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ))
450		addsub4 11104	. . . . . . . . . . . . 13 ⊢ ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) ∧ ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ)) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))))
451	445, 449, 450	syl2an 599	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ)) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))))
452	451	anassrs 471	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))))
453	92	replimd 14743	. . . . . . . . . . . . 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 7217	. . . . . . . . . . 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 11248	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))
458	13, 191, 456, 457	mp3an3an 1469	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ)) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))
459	458	anassrs 471	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))
460	459	oveq2d 7218	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))))
461	452, 455, 460	3eqtr4rd 2785	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
462	461	fveq2d 6710	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) = (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
463	462	mpteq2dva 5139	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
464	463	fveq2d 6710	. . . . . . 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 12579	. . . . . . . 8 ⊢ (𝑌 ∈ ℝ+ → 𝑌 ∈ ℂ)
467	466	2halvesd 12059	. . . . . . 7 ⊢ (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) = 𝑌)
468	467	ad2antlr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑌 / 2) + (𝑌 / 2)) = 𝑌)
469	465, 468	breq12d 5056	. . . . 5 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2)) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌))
470	442, 469	sylibd 242	. . . 4 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌))
471	470	reximdvva 3189	. . 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	syl5bir 246	. 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 209   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2110   ≠ wne 2935  ∀wral 3054  ∃wrex 3055  {crab 3058  Vcvv 3401   ∖ cdif 3854   ∩ cin 3856   ⊆ wss 3857  ifcif 4429  {csn 4531  ∪ ciun 4894   class class class wbr 5043   ↦ cmpt 5124  ^◡ccnv 5539  dom cdm 5540  ran crn 5541   “ cima 5543   ∘ ccom 5544  ⟶wf 6365  ‘cfv 6369  (class class class)co 7202   ∘_f cof 7456   ∘_r cofr 7457  Fincfn 8615  ℂcc 10710  ℝcr 10711  0cc0 10712  1c1 10713  ici 10714   + caddc 10715   · cmul 10717  +∞cpnf 10847  -∞cmnf 10848  ℝ^*cxr 10849   < clt 10850   ≤ cle 10851   − cmin 11045  -cneg 11046   / cdiv 11472  2c2 11868  ℝ⁺crp 12569  (,)cioo 12918  [,)cico 12920  [,]cicc 12921  ℜcre 14643  ℑcim 14644  abscabs 14780  volcvol 24332  MblFncmbf 24483  ∫₁citg1 24484  ∫₂citg2 24485  𝐿¹cibl 24486  ∫citg 24487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-rep 5168  ax-sep 5181  ax-nul 5188  ax-pow 5247  ax-pr 5311  ax-un 7512  ax-inf2 9245  ax-cnex 10768  ax-resscn 10769  ax-1cn 10770  ax-icn 10771  ax-addcl 10772  ax-addrcl 10773  ax-mulcl 10774  ax-mulrcl 10775  ax-mulcom 10776  ax-addass 10777  ax-mulass 10778  ax-distr 10779  ax-i2m1 10780  ax-1ne0 10781  ax-1rid 10782  ax-rnegex 10783  ax-rrecex 10784  ax-cnre 10785  ax-pre-lttri 10786  ax-pre-lttrn 10787  ax-pre-ltadd 10788  ax-pre-mulgt0 10789  ax-pre-sup 10790  ax-addf 10791

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3403  df-sbc 3688  df-csb 3803  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-pss 3876  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-tp 4536  df-op 4538  df-uni 4810  df-int 4850  df-iun 4896  df-disj 5009  df-br 5044  df-opab 5106  df-mpt 5125  df-tr 5151  df-id 5444  df-eprel 5449  df-po 5457  df-so 5458  df-fr 5498  df-se 5499  df-we 5500  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-pred 6149  df-ord 6205  df-on 6206  df-lim 6207  df-suc 6208  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-f1 6374  df-fo 6375  df-f1o 6376  df-fv 6377  df-isom 6378  df-riota 7159  df-ov 7205  df-oprab 7206  df-mpo 7207  df-of 7458  df-ofr 7459  df-om 7634  df-1st 7750  df-2nd 7751  df-wrecs 8036  df-recs 8097  df-rdg 8135  df-1o 8191  df-2o 8192  df-er 8380  df-map 8499  df-pm 8500  df-en 8616  df-dom 8617  df-sdom 8618  df-fin 8619  df-fi 9016  df-sup 9047  df-inf 9048  df-oi 9115  df-dju 9500  df-card 9538  df-pnf 10852  df-mnf 10853  df-xr 10854  df-ltxr 10855  df-le 10856  df-sub 11047  df-neg 11048  df-div 11473  df-nn 11814  df-2 11876  df-3 11877  df-4 11878  df-n0 12074  df-z 12160  df-uz 12422  df-q 12528  df-rp 12570  df-xneg 12687  df-xadd 12688  df-xmul 12689  df-ioo 12922  df-ico 12924  df-icc 12925  df-fz 13079  df-fzo 13222  df-fl 13350  df-mod 13426  df-seq 13558  df-exp 13619  df-hash 13880  df-cj 14645  df-re 14646  df-im 14647  df-sqrt 14781  df-abs 14782  df-clim 15032  df-sum 15233  df-rest 16899  df-topgen 16920  df-psmet 20327  df-xmet 20328  df-met 20329  df-bl 20330  df-mopn 20331  df-top 21763  df-topon 21780  df-bases 21815  df-cmp 22256  df-ovol 24333  df-vol 24334  df-mbf 24488  df-itg1 24489  df-itg2 24490  df-ibl 24491  df-0p 24539

This theorem is referenced by:  ftc1anc  35552