Theorem ftc1anclem6 38406

Description: Lemma for ftc1anc 38409- 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 13061	. . 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 38405	. . 3 ⊢ ((𝜑 ∧ (𝑌 / 2) ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2))
11	1, 10	sylan2 605	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2))
12		eqid 2765	. . . . 5 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) d𝑡) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) d𝑡)
13		ax-icn 11174	. . . . . . . 8 ⊢ i ∈ ℂ
14		ine0 11664	. . . . . . . 8 ⊢ i ≠ 0
15	13, 14	reccli 11960	. . . . . . 7 ⊢ (1 / i) ∈ ℂ
16	15	a1i 11	. . . . . 6 ⊢ (𝜑 → (1 / i) ∈ ℂ)
17	9	ffvelcdmda 7083	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐹‘𝑦) ∈ ℂ)
18	9	feqmptd 6953	. . . . . . 7 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)))
19	18, 8	eqeltrrd 2866	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ 𝐿1)
20		divrec2 11904	. . . . . . . . . 10 ⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦)))
21	13, 14, 20	mp3an23 1482	. . . . . . . . 9 ⊢ ((𝐹‘𝑦) ∈ ℂ → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦)))
22	17, 21	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦)))
23	22	mpteq2dva 5206	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) = (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))))
24		iblmbf 25977	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ 𝐿1 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn)
25	19, 24	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn)
26		2fveq3 6890	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (ℜ‘(𝐹‘𝑦)) = (ℜ‘(𝐹‘𝑥)))
27	26	cbvmptv 5217	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) = (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥)))
28	27	eleq1i 2856	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn)
29	17	recld 15269	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℝ)
30	29	recnd 11252	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℂ)
31	30	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℂ)
32	28	bilanri 512	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn)
33	31, 32	mbfneg 25860	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn)
34	28, 33	sylan2b 606	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn)
35	9	ffvelcdmda 7083	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐹‘𝑥) ∈ ℂ)
36	35	recld 15269	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (ℜ‘(𝐹‘𝑥)) ∈ ℝ)
37	36	recnd 11252	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (ℜ‘(𝐹‘𝑥)) ∈ ℂ)
38	37	negnegd 11575	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → --(ℜ‘(𝐹‘𝑥)) = (ℜ‘(𝐹‘𝑥)))
39	38	mpteq2dva 5206	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))))
40	39, 27	eqtr4di 2818	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))))
41	40	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))))
42		negex 11470	. . . . . . . . . . . . . . . 16 ⊢ -(ℜ‘(𝐹‘𝑥)) ∈ V
43	42	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) ∧ 𝑥 ∈ 𝐷) → -(ℜ‘(𝐹‘𝑥)) ∈ V)
44	26	negeqd 11466	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → -(ℜ‘(𝐹‘𝑦)) = -(ℜ‘(𝐹‘𝑥)))
45	44	cbvmptv 5217	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) = (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥)))
46	45	eleq1i 2856	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) ∈ MblFn)
47	46	bilani 510	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) ∈ MblFn)
48	43, 47	mbfneg 25860	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) ∈ MblFn)
49	41, 48	eqeltrrd 2866	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn)
50	34, 49	impbida 813	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn))
51		divcl 11893	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹‘𝑦) / i) ∈ ℂ)
52		imre 15183	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑦) / i) ∈ ℂ → (ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i))))
53	51, 52	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → (ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i))))
54	13, 14, 53	mp3an23 1482	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i))))
55	13, 14, 51	mp3an23 1482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑦) ∈ ℂ → ((𝐹‘𝑦) / i) ∈ ℂ)
56		mulneg1 11665	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i ∈ ℂ ∧ ((𝐹‘𝑦) / i) ∈ ℂ) → (-i · ((𝐹‘𝑦) / i)) = -(i · ((𝐹‘𝑦) / i)))
57	13, 55, 56	sylancr 599	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) ∈ ℂ → (-i · ((𝐹‘𝑦) / i)) = -(i · ((𝐹‘𝑦) / i)))
58		divcan2 11895	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → (i · ((𝐹‘𝑦) / i)) = (𝐹‘𝑦))
59	13, 14, 58	mp3an23 1482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑦) ∈ ℂ → (i · ((𝐹‘𝑦) / i)) = (𝐹‘𝑦))
60	59	negeqd 11466	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) ∈ ℂ → -(i · ((𝐹‘𝑦) / i)) = -(𝐹‘𝑦))
61	57, 60	eqtrd 2800	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑦) ∈ ℂ → (-i · ((𝐹‘𝑦) / i)) = -(𝐹‘𝑦))
62	61	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℜ‘(-i · ((𝐹‘𝑦) / i))) = (ℜ‘-(𝐹‘𝑦)))
63		reneg 15200	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℜ‘-(𝐹‘𝑦)) = -(ℜ‘(𝐹‘𝑦)))
64	54, 62, 63	3eqtrd 2804	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℑ‘((𝐹‘𝑦) / i)) = -(ℜ‘(𝐹‘𝑦)))
65	17, 64	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℑ‘((𝐹‘𝑦) / i)) = -(ℜ‘(𝐹‘𝑦)))
66	65	mpteq2dva 5206	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) = (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))))
67	66	eleq1d 2850	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn))
68	50, 67	bitr4d 285	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn))
69		imval 15182	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑦) ∈ ℂ → (ℑ‘(𝐹‘𝑦)) = (ℜ‘((𝐹‘𝑦) / i)))
70	17, 69	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℑ‘(𝐹‘𝑦)) = (ℜ‘((𝐹‘𝑦) / i)))
71	70	mpteq2dva 5206	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))))
72	71	eleq1d 2850	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn))
73	68, 72	anbi12d 644	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn)))
74		ancom 466	. . . . . . . . . 10 ⊢ (((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn))
75	73, 74	bitrdi 290	. . . . . . . . 9 ⊢ (𝜑 → (((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn)))
76	17	ismbfcn2 25848	. . . . . . . . 9 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn)))
77	17, 55	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑦) / i) ∈ ℂ)
78	77	ismbfcn2 25848	. . . . . . . . 9 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn)))
79	75, 76, 78	3bitr4d 314	. . . . . . . 8 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn))
80	25, 79	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn)
81	23, 80	eqeltrrd 2866	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) ∈ MblFn)
82	16, 17, 19, 81	iblmulc2nc 38393	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) ∈ 𝐿1)
83		mulcl 11199	. . . . . . 7 ⊢ (((1 / i) ∈ ℂ ∧ (𝐹‘𝑦) ∈ ℂ) → ((1 / i) · (𝐹‘𝑦)) ∈ ℂ)
84	15, 17, 83	sylancr 599	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((1 / i) · (𝐹‘𝑦)) ∈ ℂ)
85	84	fmpttd 7114	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))):𝐷⟶ℂ)
86	12, 3, 4, 5, 6, 7, 82, 85	ftc1anclem5 38405	. . . 4 ⊢ ((𝜑 ∧ (𝑌 / 2) ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))
87	1, 86	sylan2 605	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))
88	9	ffvelcdmda 7083	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
89		0cnd 11214	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ)
90	88, 89	ifclda 4525	. . . . . . . . . . 11 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
91		imval 15182	. . . . . . . . . . 11 ⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i)))
92	90, 91	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i)))
93		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑡 → (𝐹‘𝑦) = (𝐹‘𝑡))
94	93	oveq2d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑡 → ((1 / i) · (𝐹‘𝑦)) = ((1 / i) · (𝐹‘𝑡)))
95		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) = (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))
96		ovex 7452	. . . . . . . . . . . . . . . 16 ⊢ ((1 / i) · (𝐹‘𝑡)) ∈ V
97	94, 95, 96	fvmpt 6993	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝐷 → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((1 / i) · (𝐹‘𝑡)))
98	97	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((1 / i) · (𝐹‘𝑡)))
99		divrec2 11904	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑡) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡)))
100	13, 14, 99	mp3an23 1482	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑡) ∈ ℂ → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡)))
101	88, 100	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡)))
102	98, 101	eqtr4d 2803	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((𝐹‘𝑡) / i))
103	102	ifeq1da 4521	. . . . . . . . . . . 12 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0))
104		ovif 7517	. . . . . . . . . . . . 13 ⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), (0 / i))
105	13, 14	div0i 11964	. . . . . . . . . . . . . 14 ⊢ (0 / i) = 0
106		ifeq2 4494	. . . . . . . . . . . . . 14 ⊢ ((0 / i) = 0 → if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), (0 / i)) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0))
107	105, 106	ax-mp 5	. . . . . . . . . . . . 13 ⊢ if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), (0 / i)) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0)
108	104, 107	eqtri 2788	. . . . . . . . . . . 12 ⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0)
109	103, 108	eqtr4di 2818	. . . . . . . . . . 11 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i))
110	109	fveq2d 6889	. . . . . . . . . 10 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i)))
111	92, 110	eqtr4d 2803	. . . . . . . . 9 ⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)))
112	111	fvoveq1d 7441	. . . . . . . 8 ⊢ (𝜑 → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))
113	112	mpteq2dv 5207	. . . . . . 7 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡)))))
114	113	fveq2d 6889	. . . . . 6 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))))
115	114	breq1d 5121	. . . . 5 ⊢ (𝜑 → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)))
116	115	rexbidv 3191	. . . 4 ⊢ (𝜑 → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)))
117	116	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)))
118	87, 117	mpbird 260	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))
119		reeanv 3239	. . 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)))
120		eleq1w 2848	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (𝑥 ∈ 𝐷 ↔ 𝑡 ∈ 𝐷))
121		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (𝐹‘𝑥) = (𝐹‘𝑡))
122	120, 121	ifbieq1d 4514	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑡 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
123	122	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑡 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
124		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))
125		fvex 6898	. . . . . . . . . . . . . 14 ⊢ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V
126	123, 124, 125	fvmpt 6993	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
127	126	fvoveq1d 7441	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℝ → (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))
128	127	mpteq2ia 5208	. . . . . . . . . . 11 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))
129	128	fveq2i 6888	. . . . . . . . . 10 ⊢ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))))
130		rembl 25750	. . . . . . . . . . . . . . . . 17 ⊢ ℝ ∈ dom vol
131	130	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℝ ∈ dom vol)
132		0cnd 11214	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐷) → 0 ∈ ℂ)
133	35, 132	ifclda 4525	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ)
134	133	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ)
135		eldifn 4086	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (ℝ ∖ 𝐷) → ¬ 𝑥 ∈ 𝐷)
136	135	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑥 ∈ 𝐷)
137	136	iffalsed 4500	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐷)) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0)
138	9	feqmptd 6953	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)))
139		iftrue 4495	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐷 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥))
140	139	mpteq2ia 5208	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥))
141	138, 140	eqtr4di 2818	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))
142	141, 8	eqeltrrd 2866	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ 𝐿1)
143	7, 131, 134, 137, 142	iblss2 26016	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ 𝐿1)
144	133	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ)
145	144	iblcn 26009	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ 𝐿1 ↔ ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1)))
146	143, 145	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1))
147	146	simpld 500	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1)
148	144	recld 15269	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ ℝ)
149	148	fmpttd 7114	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)
150	147, 149	jca 521	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ))
151		ftc1anclem4 38404	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ)
152	151	3expb 1138	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ)
153	150, 152	sylan2 605	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝜑) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ)
154	153	ancoms 464	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ)
155	129, 154	eqeltrrid 2870	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ)
156	122	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑡 → (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
157		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))
158		fvex 6898	. . . . . . . . . . . . . 14 ⊢ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V
159	156, 157, 158	fvmpt 6993	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
160	159	fvoveq1d 7441	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℝ → (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
161	160	mpteq2ia 5208	. . . . . . . . . . 11 ⊢ (𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
162	161	fveq2i 6888	. . . . . . . . . 10 ⊢ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
163	146	simprd 501	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1)
164	133	imcld 15270	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ ℝ)
165	164	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ ℝ)
166	165	fmpttd 7114	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)
167	163, 166	jca 521	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ))
168		ftc1anclem4 38404	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ)
169	168	3expb 1138	. . . . . . . . . . . 12 ⊢ ((𝑔 ∈ dom ∫1 ∧ ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ)
170	167, 169	sylan2 605	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝜑) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ)
171	170	ancoms 464	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ)
172	162, 171	eqeltrrid 2870	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ)
173	155, 172	anim12dan 631	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ))
174	1	rpred 13076	. . . . . . . . 9 ⊢ (𝑌 ∈ ℝ+ → (𝑌 / 2) ∈ ℝ)
175	174, 174	jca 521	. . . . . . . 8 ⊢ (𝑌 ∈ ℝ+ → ((𝑌 / 2) ∈ ℝ ∧ (𝑌 / 2) ∈ ℝ))
176		lt2add 11714	. . . . . . . 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))))
177	173, 175, 176	syl2an 608	. . . . . . 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))))
178	177	an32s 665	. . . . . 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))))
179	90	recld 15269	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
180	179	recnd 11252	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ)
181		i1ff 25886	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → 𝑓:ℝ⟶ℝ)
182	181	ffvelcdmda 7083	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℝ)
183	182	recnd 11252	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℂ)
184		subcl 11471	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑓‘𝑡) ∈ ℂ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ)
185	180, 183, 184	syl2an 608	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ)
186	185	anassrs 473	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ)
187	186	adantlrr 734	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ)
188	90	imcld 15270	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
189	188	recnd 11252	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ)
190		i1ff 25886	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
191	190	ffvelcdmda 7083	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℝ)
192	191	recnd 11252	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℂ)
193		subcl 11471	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ)
194	189, 192, 193	syl2an 608	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ)
195	194	anassrs 473	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ)
196		mulcl 11199	. . . . . . . . . . . . . . . . 17 ⊢ ((i ∈ ℂ ∧ ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ)
197	13, 195, 196	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ)
198	197	adantlrl 733	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ)
199	187, 198	addcld 11243	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) ∈ ℂ)
200	199	abscld 15514	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ)
201	200	rexrd 11274	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ*)
202	199	absge0d 15522	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
203		elxrge0 13500	. . . . . . . . . . . 12 ⊢ ((abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ (0[,]+∞) ↔ ((abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ* ∧ 0 ≤ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))))
204	201, 202, 203	sylanbrc 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ (0[,]+∞))
205	204	fmpttd 7114	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))):ℝ⟶(0[,]+∞))
206		icossicc 13479	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
207		ge0addcl 13503	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,)+∞))
208	206, 207	sselid 3936	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,]+∞))
209	208	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,]+∞))
210	186	abscld 15514	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ ℝ)
211	186	absge0d 15522	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))
212		elrege0 13497	. . . . . . . . . . . . . 14 ⊢ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ (0[,)+∞) ↔ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))))
213	210, 211, 212	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ (0[,)+∞))
214	213	fmpttd 7114	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))):ℝ⟶(0[,)+∞))
215	214	adantrr 730	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))):ℝ⟶(0[,)+∞))
216	195	abscld 15514	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℝ)
217	195	absge0d 15522	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
218		elrege0 13497	. . . . . . . . . . . . . 14 ⊢ ((abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ (0[,)+∞) ↔ ((abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
219	216, 217, 218	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ (0[,)+∞))
220	219	fmpttd 7114	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))):ℝ⟶(0[,)+∞))
221	220	adantrl 729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))):ℝ⟶(0[,)+∞))
222		reex 11206	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
223	222	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ℝ ∈ V)
224		inidm 4179	. . . . . . . . . . 11 ⊢ (ℝ ∩ ℝ) = ℝ
225	209, 215, 221, 223, 223, 224	off 7702	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))):ℝ⟶(0[,]+∞))
226	187, 198	abstrid 15534	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ≤ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
227	226	ralrimiva 3159	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ∀𝑡 ∈ ℝ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ≤ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
228		ovexd 7454	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ V)
229		eqidd 2766	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))))
230		fvexd 6900	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ V)
231		fvexd 6900	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) ∈ V)
232		eqidd 2766	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))))
233		absmul 15369	. . . . . . . . . . . . . . . . 17 ⊢ ((i ∈ ℂ ∧ ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) → (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = ((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
234	13, 195, 233	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = ((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
235		absi 15361	. . . . . . . . . . . . . . . . . 18 ⊢ (abs‘i) = 1
236	235	oveq1i 7429	. . . . . . . . . . . . . . . . 17 ⊢ ((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (1 · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
237	216	recnd 11252	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ)
238	237	mullidd 11242	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (1 · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
239	236, 238	eqtrid 2812	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))
240	234, 239	eqtr2d 2801	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))
241	240	mpteq2dva 5206	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
242	241	adantrl 729	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
243	223, 230, 231, 232, 242	offval2 7704	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) = (𝑡 ∈ ℝ ↦ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))))
244	223, 200, 228, 229, 243	ofrfval2 7705	. . . . . . . . . . 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)) − (𝑔‘𝑡)))))))
245	227, 244	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∘r ≤ ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))
246		itg2le 25949	. . . . . . . . . 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)) − (𝑔‘𝑡)))))))
247	205, 225, 245, 246	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ (∫2‘((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))))
248		absf 15413	. . . . . . . . . . . . . 14 ⊢ abs:ℂ⟶ℝ
249	248	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → abs:ℂ⟶ℝ)
250	249, 186	cofmpt 7132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))))
251		resubcl 11537	. . . . . . . . . . . . . . . 16 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑓‘𝑡) ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ)
252	179, 182, 251	syl2an 608	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ)
253	252	anassrs 473	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ)
254	253	fmpttd 7114	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))):ℝ⟶ℝ)
255	130	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ℝ ∈ dom vol)
256		iunin2 5037	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦}))
257		imaiun 7248	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝑓 “ ∪ 𝑦 ∈ ran 𝑓{𝑦}) = ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})
258		iunid 5027	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑦 ∈ ran 𝑓{𝑦} = ran 𝑓
259	258	imaeq2i 6062	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝑓 “ ∪ 𝑦 ∈ ran 𝑓{𝑦}) = (◡𝑓 “ ran 𝑓)
260	257, 259	eqtr3i 2790	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦}) = (◡𝑓 “ ran 𝑓)
261	260	ineq2i 4170	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓))
262	256, 261	eqtri 2788	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓))
263		cnvimass 6086	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))
264		ovex 7452	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ V
265		eqid 2765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) = (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))
266	264, 265	dmmpti 6683	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) = ℝ
267	263, 266	sseqtri 3986	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ ℝ
268		cnvimarndm 6087	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝑓 “ ran 𝑓) = dom 𝑓
269	181	fdmd 6720	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ dom ∫1 → dom 𝑓 = ℝ)
270	268, 269	eqtrid 2812	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → (◡𝑓 “ ran 𝑓) = ℝ)
271	267, 270	sseqtrrid 3981	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ (◡𝑓 “ ran 𝑓))
272		dfss2 3924	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ (◡𝑓 “ ran 𝑓) ↔ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)))
273	271, 272	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)))
274	262, 273	eqtrid 2812	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ dom ∫1 → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)))
275	274	ad2antlr 740	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)))
276	181	frnd 6718	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ)
277	276	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ran 𝑓 ⊆ ℝ)
278	277	sselda 3938	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → 𝑦 ∈ ℝ)
279	179	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
280		resubcl 11537	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ)
281	179, 280	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ)
282	281	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ)
283	279, 282	2thd 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ))
284		ltaddsub 11703	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))
285	179, 284	syl3an3 1183	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝜑) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))
286	285	3comr 1143	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))
287	286	3expa 1136	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))
288	283, 287	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))))
289		readdcl 11198	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
290	289	rexrd 11274	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ*)
291	290	adantll 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ*)
292		elioopnf 13486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 + 𝑦) ∈ ℝ* → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
293	291, 292	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
294		rexr 11270	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
295	294	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℝ*)
296		elioopnf 13486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ* → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))))
297	295, 296	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))))
298	288, 293, 297	3bitr4rd 315	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)))
299		oveq2 7427	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓‘𝑡) = 𝑦 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))
300	299	eleq1d 2850	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞)))
301	300	bibi1d 346	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓‘𝑡) = 𝑦 → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞))))
302	298, 301	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞))))
303	302	pm5.32rd 589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)))
304	303	adantllr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)))
305	278, 304	syldan 603	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)))
306	305	rabbidv 3425	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)} = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
307	181	feqmptd 6953	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ dom ∫1 → 𝑓 = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)))
308	307	cnveqd 5863	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ∈ dom ∫1 → ◡𝑓 = ◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)))
309	308	imaeq1d 6063	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ dom ∫1 → (◡𝑓 “ {𝑦}) = (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}))
310	309	ineq2d 4173	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})))
311	265	mptpreima 6241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)}
312		vex 3461	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑦 ∈ V
313		eqid 2765	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡))
314	313	mptiniseg 6242	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ V → (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}) = {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
315	312, 314	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}) = {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}
316	311, 315	ineq12i 4171	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
317		inrab 4269	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}
318	316, 317	eqtri 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}
319	310, 318	eqtrdi 2816	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
320	319	ad3antlr 744	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
321	309	ineq2d 4173	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})))
322		eqid 2765	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
323	322	mptpreima 6241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) = {𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)}
324	323, 315	ineq12i 4171	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
325		inrab 4269	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}
326	324, 325	eqtri 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}
327	321, 326	eqtrdi 2816	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
328	327	ad3antlr 744	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)})
329	306, 320, 328	3eqtr4d 2810	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})))
330	329	iuneq2dv 4983	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})))
331	275, 330	eqtr3d 2802	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) = ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})))
332		i1frn 25887	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin)
333	332	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ran 𝑓 ∈ Fin)
334	90	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
335		eldifn 4086	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷)
336	335	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷)
337	336	iffalsed 4500	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = 0)
338	9	feqmptd 6953	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
339		iftrue 4495	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = (𝐹‘𝑡))
340	339	mpteq2ia 5208	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡))
341	338, 340	eqtr4di 2818	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
342		iblmbf 25977	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)
343	8, 342	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹 ∈ MblFn)
344	341, 343	eqeltrrd 2866	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn)
345	7, 131, 334, 337, 344	mbfss 25856	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn)
346	90	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
347	346	ismbfcn2 25848	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn ↔ ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)))
348	345, 347	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn))
349	348	simpld 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)
350	179	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)
351	350	fmpttd 7114	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ)
352		mbfima 25840	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ) → (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol)
353	349, 351, 352	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol)
354		i1fima 25888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (◡𝑓 “ {𝑦}) ∈ dom vol)
355		inmbl 25752	. . . . . . . . . . . . . . . . . . 19 ⊢ (((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol ∧ (◡𝑓 “ {𝑦}) ∈ dom vol) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
356	353, 354, 355	syl2an 608	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
357	356	ralrimivw 3163	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
358		finiunmbl 25754	. . . . . . . . . . . . . . . . 17 ⊢ ((ran 𝑓 ∈ Fin ∧ ∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
359	333, 357, 358	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
360	359	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
361	331, 360	eqeltrd 2865	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∈ dom vol)
362		iunin2 5037	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦}))
363	260	ineq2i 4170	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓))
364	362, 363	eqtri 2788	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓))
365		cnvimass 6086	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))
366	365, 266	sseqtri 3986	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ ℝ
367	366, 270	sseqtrrid 3981	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ (◡𝑓 “ ran 𝑓))
368		dfss2 3924	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ (◡𝑓 “ ran 𝑓) ↔ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)))
369	367, 368	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)))
370	364, 369	eqtrid 2812	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ dom ∫1 → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)))
371	370	ad2antlr 740	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)))
372	282, 279	2thd 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ))
373		ltsubadd 11699	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))
374	179, 373	syl3an1 1181	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))
375	374	3expa 1136	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))
376	375	an32s 665	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))
377	372, 376	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))))
378		elioomnf 13487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ* → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥)))
379	295, 378	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥)))
380		elioomnf 13487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 + 𝑦) ∈ ℝ* → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))))
381	291, 380	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))))
382	377, 379, 381	3bitr4d 314	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))))
383	299	eleq1d 2850	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥)))
384	383	bibi1d 346	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓‘𝑡) = 𝑦 → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)))))
385	382, 384	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)))))
386	385	pm5.32rd 589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)))
387	386	adantllr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)))
388	278, 387	syldan 603	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)))
389	388	rabbidv 3425	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)} = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)})
390	309	ineq2d 4173	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})))
391	265	mptpreima 6241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)}
392	391, 315	ineq12i 4171	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
393		inrab 4269	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)}
394	392, 393	eqtri 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)}
395	390, 394	eqtrdi 2816	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)})
396	395	ad3antlr 744	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)})
397	309	ineq2d 4173	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})))
398	322	mptpreima 6241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) = {𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))}
399	398, 315	ineq12i 4171	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦})
400		inrab 4269	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)}
401	399, 400	eqtri 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)}
402	397, 401	eqtrdi 2816	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)})
403	402	ad3antlr 744	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)})
404	389, 396, 403	3eqtr4d 2810	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})))
405	404	iuneq2dv 4983	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})))
406	371, 405	eqtr3d 2802	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) = ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})))
407		mbfima 25840	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ) → (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol)
408	349, 351, 407	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol)
409		inmbl 25752	. . . . . . . . . . . . . . . . . . 19 ⊢ (((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol ∧ (◡𝑓 “ {𝑦}) ∈ dom vol) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
410	408, 354, 409	syl2an 608	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
411	410	ralrimivw 3163	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
412		finiunmbl 25754	. . . . . . . . . . . . . . . . 17 ⊢ ((ran 𝑓 ∈ Fin ∧ ∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
413	333, 411, 412	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
414	413	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol)
415	406, 414	eqeltrd 2865	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∈ dom vol)
416	254, 255, 361, 415	ismbf2d 25850	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ MblFn)
417		ftc1anclem1 38401	. . . . . . . . . . . . 13 ⊢ (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn)
418	254, 416, 417	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn)
419	250, 418	eqeltrrd 2866	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn)
420	419	adantrr 730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn)
421	155	adantrr 730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ)
422	172	adantrl 729	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ)
423	420, 215, 421, 221, 422	itg2addnc 38382	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))))
424	247, 423	breqtrd 5139	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))))
425	424	adantlr 728	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))))
426		itg2cl 25942	. . . . . . . . . 10 ⊢ ((𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ∈ ℝ*)
427	205, 426	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ∈ ℝ*)
428	427	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ∈ ℝ*)
429		readdcl 11198	. . . . . . . . . . . 12 ⊢ (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ)
430	155, 172, 429	syl2an 608	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ (𝜑 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ)
431	430	anandis 691	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ)
432	431	rexrd 11274	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ*)
433	432	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ*)
434	1, 1	rpaddcld 13091	. . . . . . . . . 10 ⊢ (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ+)
435	434	rpxrd 13077	. . . . . . . . 9 ⊢ (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ*)
436	435	ad2antlr 740	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ*)
437		xrlelttr 13197	. . . . . . . 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))))
438	428, 433, 436, 437	syl3anc 1398	. . . . . . 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))))
439	425, 438	mpand 708	. . . . . 6 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2))))
440	178, 439	syld 48	. . . . 5 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2))))
441		mulcl 11199	. . . . . . . . . . . . . . 15 ⊢ ((i ∈ ℂ ∧ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ) → (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ)
442	13, 189, 441	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ)
443	180, 442	jca 521	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ))
444		mulcl 11199	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ)
445	13, 192, 444	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ)
446	183, 445	anim12i 625	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ))
447	446	anandirs 692	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ))
448		addsub4 11516	. . . . . . . . . . . . 13 ⊢ ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) ∧ ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ)) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))))
449	443, 447, 448	syl2an 608	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ)) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))))
450	449	anassrs 473	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))))
451	90	replimd 15272	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
452	451	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))
453	452	oveq1d 7434	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
454	192	adantll 727	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℂ)
455		subdi 11662	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))
456	13, 189, 454, 455	mp3an3an 1496	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ)) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))
457	456	anassrs 473	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))
458	457	oveq2d 7435	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))))
459	450, 453, 458	3eqtr4rd 2811	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
460	459	fveq2d 6889	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) = (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
461	460	mpteq2dva 5206	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
462	461	fveq2d 6889	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))))
463	462	adantlr 728	. . . . . 6 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))))
464		rpcn 13043	. . . . . . . 8 ⊢ (𝑌 ∈ ℝ+ → 𝑌 ∈ ℂ)
465	464	2halvesd 12505	. . . . . . 7 ⊢ (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) = 𝑌)
466	465	ad2antlr 740	. . . . . 6 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑌 / 2) + (𝑌 / 2)) = 𝑌)
467	463, 466	breq12d 5124	. . . . 5 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2)) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌))
468	440, 467	sylibd 242	. . . 4 ⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌))
469	468	reximdvva 3215	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌))
470	119, 469	biimtrrid 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 · (𝑔‘𝑡))))))) < 𝑌))
471	11, 118, 470	mp2and 712	1 ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∀wral 3081  ∃wrex 3091  {crab 3418  Vcvv 3457   ∖ cdif 3903   ∩ cin 3905   ⊆ wss 3906  ifcif 4489  {csn 4591  ∪ ciun 4958   class class class wbr 5111   ↦ cmpt 5194  ^◡ccnv 5662  dom cdm 5663  ran crn 5664   “ cima 5666   ∘ ccom 5667  ⟶wf 6536  ‘cfv 6540  (class class class)co 7419   ∘_f cof 7682   ∘_r cofr 7683  Fincfn 8949  ℂcc 11113  ℝcr 11114  0cc0 11115  1c1 11116  ici 11117   + caddc 11118   · cmul 11120  +∞cpnf 11255  -∞cmnf 11256  ℝ^*cxr 11257   < clt 11258   ≤ cle 11259   − cmin 11456  -cneg 11457   / cdiv 11886  2c2 12310  ℝ⁺crp 13032  (,)cioo 13388  [,)cico 13390  [,]cicc 13391  ℜcre 15172  ℑcim 15173  abscabs 15309  volcvol 25673  MblFncmbf 25824  ∫₁citg1 25825  ∫₂citg2 25826  𝐿¹cibl 25827  ∫citg 25828

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-inf2 9617  ax-cnex 11171  ax-resscn 11172  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-mulcom 11179  ax-addass 11180  ax-mulass 11181  ax-distr 11182  ax-i2m1 11183  ax-1ne0 11184  ax-1rid 11185  ax-rnegex 11186  ax-rrecex 11187  ax-cnre 11188  ax-pre-lttri 11189  ax-pre-lttrn 11190  ax-pre-ltadd 11191  ax-pre-mulgt0 11192  ax-pre-sup 11193  ax-addf 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-disj 5079  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7684  df-ofr 7685  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-2o 8460  df-er 8700  df-map 8832  df-pm 8833  df-en 8950  df-dom 8951  df-sdom 8952  df-fin 8953  df-fi 9378  df-sup 9409  df-inf 9410  df-oi 9479  df-dju 9903  df-card 9941  df-pnf 11260  df-mnf 11261  df-xr 11262  df-ltxr 11263  df-le 11264  df-sub 11458  df-neg 11459  df-div 11887  df-nn 12249  df-2 12318  df-3 12319  df-4 12320  df-n0 12520  df-z 12607  df-uz 12879  df-q 12989  df-rp 13033  df-xneg 13153  df-xadd 13154  df-xmul 13155  df-ioo 13392  df-ico 13394  df-icc 13395  df-fz 13552  df-fzo 13700  df-fl 13843  df-mod 13921  df-seq 14056  df-exp 14116  df-hash 14385  df-cj 15174  df-re 15175  df-im 15176  df-sqrt 15310  df-abs 15311  df-clim 15563  df-sum 15762  df-rest 17497  df-topgen 17518  df-psmet 21564  df-xmet 21565  df-met 21566  df-bl 21567  df-mopn 21568  df-top 23101  df-topon 23118  df-bases 23153  df-cmp 23594  df-ovol 25674  df-vol 25675  df-mbf 25829  df-itg1 25830  df-itg2 25831  df-ibl 25832  df-0p 25880

This theorem is used by:  ftc1anc  38409