Theorem ismbf3d 23821

Description: Simplified form of ismbfd 23806. (Contributed by Mario Carneiro, 18-Jun-2014.)

Hypotheses

Ref	Expression
ismbf3d.1	⊢ (𝜑 → 𝐹:𝐴⟶ℝ)
ismbf3d.2	⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol)

Assertion

Ref	Expression
ismbf3d	⊢ (𝜑 → 𝐹 ∈ MblFn)

Distinct variable groups:   𝑥,𝐹   𝜑,𝑥

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem ismbf3d

Dummy variables 𝑣 𝑢 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ismbf3d.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)
2		fimacnv 6597	. . . 4 ⊢ (𝐹:𝐴⟶ℝ → (◡𝐹 “ ℝ) = 𝐴)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → (◡𝐹 “ ℝ) = 𝐴)
4		imaiun 6759	. . . . 5 ⊢ (◡𝐹 “ ∪ 𝑦 ∈ ℕ (-𝑦(,)+∞)) = ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-𝑦(,)+∞))
5		ioossre 12524	. . . . . . . . 9 ⊢ (-𝑦(,)+∞) ⊆ ℝ
6	5	rgenw 3134	. . . . . . . 8 ⊢ ∀𝑦 ∈ ℕ (-𝑦(,)+∞) ⊆ ℝ
7		iunss 4782	. . . . . . . 8 ⊢ (∪ 𝑦 ∈ ℕ (-𝑦(,)+∞) ⊆ ℝ ↔ ∀𝑦 ∈ ℕ (-𝑦(,)+∞) ⊆ ℝ)
8	6, 7	mpbir 223	. . . . . . 7 ⊢ ∪ 𝑦 ∈ ℕ (-𝑦(,)+∞) ⊆ ℝ
9		renegcl 10666	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℝ → -𝑧 ∈ ℝ)
10		arch 11616	. . . . . . . . . . 11 ⊢ (-𝑧 ∈ ℝ → ∃𝑦 ∈ ℕ -𝑧 < 𝑦)
11	9, 10	syl 17	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℝ → ∃𝑦 ∈ ℕ -𝑧 < 𝑦)
12		simpl 476	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → 𝑧 ∈ ℝ)
13	12	biantrurd 530	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → (-𝑦 < 𝑧 ↔ (𝑧 ∈ ℝ ∧ -𝑦 < 𝑧)))
14		nnre 11359	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
15		ltnegcon1 10854	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (-𝑧 < 𝑦 ↔ -𝑦 < 𝑧))
16	14, 15	sylan2 588	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → (-𝑧 < 𝑦 ↔ -𝑦 < 𝑧))
17	14	adantl 475	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
18	17	renegcld 10782	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → -𝑦 ∈ ℝ)
19	18	rexrd 10407	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → -𝑦 ∈ ℝ*)
20		elioopnf 12557	. . . . . . . . . . . . 13 ⊢ (-𝑦 ∈ ℝ* → (𝑧 ∈ (-𝑦(,)+∞) ↔ (𝑧 ∈ ℝ ∧ -𝑦 < 𝑧)))
21	19, 20	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → (𝑧 ∈ (-𝑦(,)+∞) ↔ (𝑧 ∈ ℝ ∧ -𝑦 < 𝑧)))
22	13, 16, 21	3bitr4d 303	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → (-𝑧 < 𝑦 ↔ 𝑧 ∈ (-𝑦(,)+∞)))
23	22	rexbidva 3260	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℝ → (∃𝑦 ∈ ℕ -𝑧 < 𝑦 ↔ ∃𝑦 ∈ ℕ 𝑧 ∈ (-𝑦(,)+∞)))
24	11, 23	mpbid 224	. . . . . . . . 9 ⊢ (𝑧 ∈ ℝ → ∃𝑦 ∈ ℕ 𝑧 ∈ (-𝑦(,)+∞))
25		eliun 4745	. . . . . . . . 9 ⊢ (𝑧 ∈ ∪ 𝑦 ∈ ℕ (-𝑦(,)+∞) ↔ ∃𝑦 ∈ ℕ 𝑧 ∈ (-𝑦(,)+∞))
26	24, 25	sylibr 226	. . . . . . . 8 ⊢ (𝑧 ∈ ℝ → 𝑧 ∈ ∪ 𝑦 ∈ ℕ (-𝑦(,)+∞))
27	26	ssriv 3832	. . . . . . 7 ⊢ ℝ ⊆ ∪ 𝑦 ∈ ℕ (-𝑦(,)+∞)
28	8, 27	eqssi 3844	. . . . . 6 ⊢ ∪ 𝑦 ∈ ℕ (-𝑦(,)+∞) = ℝ
29	28	imaeq2i 5706	. . . . 5 ⊢ (◡𝐹 “ ∪ 𝑦 ∈ ℕ (-𝑦(,)+∞)) = (◡𝐹 “ ℝ)
30	4, 29	eqtr3i 2852	. . . 4 ⊢ ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-𝑦(,)+∞)) = (◡𝐹 “ ℝ)
31		ismbf3d.2	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol)
32	31	ralrimiva 3176	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ ℝ (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol)
33	14	renegcld 10782	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → -𝑦 ∈ ℝ)
34		oveq1 6913	. . . . . . . . . 10 ⊢ (𝑥 = -𝑦 → (𝑥(,)+∞) = (-𝑦(,)+∞))
35	34	imaeq2d 5708	. . . . . . . . 9 ⊢ (𝑥 = -𝑦 → (◡𝐹 “ (𝑥(,)+∞)) = (◡𝐹 “ (-𝑦(,)+∞)))
36	35	eleq1d 2892	. . . . . . . 8 ⊢ (𝑥 = -𝑦 → ((◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol ↔ (◡𝐹 “ (-𝑦(,)+∞)) ∈ dom vol))
37	36	rspccva 3526	. . . . . . 7 ⊢ ((∀𝑥 ∈ ℝ (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol ∧ -𝑦 ∈ ℝ) → (◡𝐹 “ (-𝑦(,)+∞)) ∈ dom vol)
38	32, 33, 37	syl2an 591	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (◡𝐹 “ (-𝑦(,)+∞)) ∈ dom vol)
39	38	ralrimiva 3176	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ ℕ (◡𝐹 “ (-𝑦(,)+∞)) ∈ dom vol)
40		iunmbl 23720	. . . . 5 ⊢ (∀𝑦 ∈ ℕ (◡𝐹 “ (-𝑦(,)+∞)) ∈ dom vol → ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-𝑦(,)+∞)) ∈ dom vol)
41	39, 40	syl 17	. . . 4 ⊢ (𝜑 → ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-𝑦(,)+∞)) ∈ dom vol)
42	30, 41	syl5eqelr 2912	. . 3 ⊢ (𝜑 → (◡𝐹 “ ℝ) ∈ dom vol)
43	3, 42	eqeltrrd 2908	. 2 ⊢ (𝜑 → 𝐴 ∈ dom vol)
44		imaiun 6759	. . . . . . 7 ⊢ (◡𝐹 “ ∪ 𝑦 ∈ ℕ (-∞(,](𝑧 − (1 / 𝑦)))) = ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦))))
45		eliun 4745	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ 𝑦 ∈ ℕ (-∞(,](𝑧 − (1 / 𝑦))) ↔ ∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))))
46		3simpb 1186	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦))) → (𝑥 ∈ ℝ ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦))))
47		simplr 787	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → 𝑧 ∈ ℝ)
48		nnrp 12126	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
49	48	ad2antrl 721	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → 𝑦 ∈ ℝ+)
50	49	rpreccld 12167	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → (1 / 𝑦) ∈ ℝ+)
51	47, 50	ltsubrpd 12189	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → (𝑧 − (1 / 𝑦)) < 𝑧)
52		simprr 791	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → 𝑥 ∈ ℝ)
53		simpr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → 𝑧 ∈ ℝ)
54		nnrecre 11394	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℕ → (1 / 𝑦) ∈ ℝ)
55		resubcl 10667	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ ℝ ∧ (1 / 𝑦) ∈ ℝ) → (𝑧 − (1 / 𝑦)) ∈ ℝ)
56	53, 54, 55	syl2an 591	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑧 − (1 / 𝑦)) ∈ ℝ)
57	56	adantrr 710	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → (𝑧 − (1 / 𝑦)) ∈ ℝ)
58		lelttr 10448	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℝ ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 ≤ (𝑧 − (1 / 𝑦)) ∧ (𝑧 − (1 / 𝑦)) < 𝑧) → 𝑥 < 𝑧))
59	52, 57, 47, 58	syl3anc 1496	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → ((𝑥 ≤ (𝑧 − (1 / 𝑦)) ∧ (𝑧 − (1 / 𝑦)) < 𝑧) → 𝑥 < 𝑧))
60	51, 59	mpan2d 687	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → (𝑥 ≤ (𝑧 − (1 / 𝑦)) → 𝑥 < 𝑧))
61	60	anassrs 461	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ≤ (𝑧 − (1 / 𝑦)) → 𝑥 < 𝑧))
62	61	imdistanda 569	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((𝑥 ∈ ℝ ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦))) → (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)))
63	46, 62	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦))) → (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)))
64		mnfxr 10415	. . . . . . . . . . . . . . . 16 ⊢ -∞ ∈ ℝ*
65		elioc2 12525	. . . . . . . . . . . . . . . 16 ⊢ ((-∞ ∈ ℝ* ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ) → (𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦)))))
66	64, 56, 65	sylancr 583	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦)))))
67		rexr 10403	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℝ → 𝑧 ∈ ℝ*)
68	67	adantl 475	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → 𝑧 ∈ ℝ*)
69		elioomnf 12558	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℝ* → (𝑥 ∈ (-∞(,)𝑧) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)))
70	68, 69	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝑥 ∈ (-∞(,)𝑧) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)))
71	70	adantr 474	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑥 ∈ (-∞(,)𝑧) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)))
72	63, 66, 71	3imtr4d 286	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) → 𝑥 ∈ (-∞(,)𝑧)))
73	72	rexlimdva 3241	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) → 𝑥 ∈ (-∞(,)𝑧)))
74	73, 70	sylibd 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) → (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)))
75		simprl 789	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → 𝑥 ∈ ℝ)
76	75	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → 𝑥 ∈ ℝ)
77		mnflt 12244	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → -∞ < 𝑥)
78	76, 77	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → -∞ < 𝑥)
79	56	ad2ant2r 755	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → (𝑧 − (1 / 𝑦)) ∈ ℝ)
80	54	ad2antrl 721	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → (1 / 𝑦) ∈ ℝ)
81		simplr 787	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → 𝑧 ∈ ℝ)
82	81	adantr 474	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → 𝑧 ∈ ℝ)
83		simprr 791	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → (1 / 𝑦) < (𝑧 − 𝑥))
84	80, 82, 76, 83	ltsub13d 10959	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → 𝑥 < (𝑧 − (1 / 𝑦)))
85	76, 79, 84	ltled 10505	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → 𝑥 ≤ (𝑧 − (1 / 𝑦)))
86	66	ad2ant2r 755	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → (𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦)))))
87	76, 78, 85, 86	mpbir3and 1448	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))))
88	81, 75	resubcld 10783	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → (𝑧 − 𝑥) ∈ ℝ)
89		simprr 791	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → 𝑥 < 𝑧)
90	75, 81	posdifd 10940	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → (𝑥 < 𝑧 ↔ 0 < (𝑧 − 𝑥)))
91	89, 90	mpbid 224	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → 0 < (𝑧 − 𝑥))
92		nnrecl 11617	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 − 𝑥) ∈ ℝ ∧ 0 < (𝑧 − 𝑥)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝑧 − 𝑥))
93	88, 91, 92	syl2anc 581	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝑧 − 𝑥))
94	87, 93	reximddv 3227	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → ∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))))
95	94	ex 403	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ((𝑥 ∈ ℝ ∧ 𝑥 < 𝑧) → ∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦)))))
96	74, 95	impbid 204	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)))
97	96, 70	bitr4d 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ 𝑥 ∈ (-∞(,)𝑧)))
98	45, 97	syl5bb 275	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝑥 ∈ ∪ 𝑦 ∈ ℕ (-∞(,](𝑧 − (1 / 𝑦))) ↔ 𝑥 ∈ (-∞(,)𝑧)))
99	98	eqrdv 2824	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∪ 𝑦 ∈ ℕ (-∞(,](𝑧 − (1 / 𝑦))) = (-∞(,)𝑧))
100	99	imaeq2d 5708	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (◡𝐹 “ ∪ 𝑦 ∈ ℕ (-∞(,](𝑧 − (1 / 𝑦)))) = (◡𝐹 “ (-∞(,)𝑧)))
101	44, 100	syl5eqr 2876	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) = (◡𝐹 “ (-∞(,)𝑧)))
102	1	ad2antrr 719	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → 𝐹:𝐴⟶ℝ)
103		ffun 6282	. . . . . . . . . . 11 ⊢ (𝐹:𝐴⟶ℝ → Fun 𝐹)
104		funcnvcnv 6190	. . . . . . . . . . 11 ⊢ (Fun 𝐹 → Fun ◡◡𝐹)
105		imadif 6207	. . . . . . . . . . 11 ⊢ (Fun ◡◡𝐹 → (◡𝐹 “ (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞))))
106	102, 103, 104, 105	4syl 19	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (◡𝐹 “ (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞))))
107	64	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → -∞ ∈ ℝ*)
108	56	rexrd 10407	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑧 − (1 / 𝑦)) ∈ ℝ*)
109		pnfxr 10411	. . . . . . . . . . . . . . 15 ⊢ +∞ ∈ ℝ*
110	109	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → +∞ ∈ ℝ*)
111		mnflt 12244	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 − (1 / 𝑦)) ∈ ℝ → -∞ < (𝑧 − (1 / 𝑦)))
112	56, 111	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → -∞ < (𝑧 − (1 / 𝑦)))
113		ltpnf 12241	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 − (1 / 𝑦)) ∈ ℝ → (𝑧 − (1 / 𝑦)) < +∞)
114	56, 113	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑧 − (1 / 𝑦)) < +∞)
115		df-ioc 12469	. . . . . . . . . . . . . . 15 ⊢ (,] = (𝑢 ∈ ℝ*, 𝑣 ∈ ℝ* ↦ {𝑤 ∈ ℝ* ∣ (𝑢 < 𝑤 ∧ 𝑤 ≤ 𝑣)})
116		df-ioo 12468	. . . . . . . . . . . . . . 15 ⊢ (,) = (𝑢 ∈ ℝ*, 𝑣 ∈ ℝ* ↦ {𝑤 ∈ ℝ* ∣ (𝑢 < 𝑤 ∧ 𝑤 < 𝑣)})
117		xrltnle 10425	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 − (1 / 𝑦)) ∈ ℝ* ∧ 𝑥 ∈ ℝ*) → ((𝑧 − (1 / 𝑦)) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑧 − (1 / 𝑦))))
118		xrlelttr 12276	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ* ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝑥 ≤ (𝑧 − (1 / 𝑦)) ∧ (𝑧 − (1 / 𝑦)) < +∞) → 𝑥 < +∞))
119		xrlttr 12260	. . . . . . . . . . . . . . 15 ⊢ ((-∞ ∈ ℝ* ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ* ∧ 𝑥 ∈ ℝ*) → ((-∞ < (𝑧 − (1 / 𝑦)) ∧ (𝑧 − (1 / 𝑦)) < 𝑥) → -∞ < 𝑥))
120	115, 116, 117, 116, 118, 119	ixxun 12480	. . . . . . . . . . . . . 14 ⊢ (((-∞ ∈ ℝ* ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞ < (𝑧 − (1 / 𝑦)) ∧ (𝑧 − (1 / 𝑦)) < +∞)) → ((-∞(,](𝑧 − (1 / 𝑦))) ∪ ((𝑧 − (1 / 𝑦))(,)+∞)) = (-∞(,)+∞))
121	107, 108, 110, 112, 114, 120	syl32anc 1503	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((-∞(,](𝑧 − (1 / 𝑦))) ∪ ((𝑧 − (1 / 𝑦))(,)+∞)) = (-∞(,)+∞))
122		uncom 3985	. . . . . . . . . . . . 13 ⊢ ((-∞(,](𝑧 − (1 / 𝑦))) ∪ ((𝑧 − (1 / 𝑦))(,)+∞)) = (((𝑧 − (1 / 𝑦))(,)+∞) ∪ (-∞(,](𝑧 − (1 / 𝑦))))
123		ioomax 12537	. . . . . . . . . . . . 13 ⊢ (-∞(,)+∞) = ℝ
124	121, 122, 123	3eqtr3g 2885	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (((𝑧 − (1 / 𝑦))(,)+∞) ∪ (-∞(,](𝑧 − (1 / 𝑦)))) = ℝ)
125		ioossre 12524	. . . . . . . . . . . . 13 ⊢ ((𝑧 − (1 / 𝑦))(,)+∞) ⊆ ℝ
126		incom 4033	. . . . . . . . . . . . . 14 ⊢ (((𝑧 − (1 / 𝑦))(,)+∞) ∩ (-∞(,](𝑧 − (1 / 𝑦)))) = ((-∞(,](𝑧 − (1 / 𝑦))) ∩ ((𝑧 − (1 / 𝑦))(,)+∞))
127	115, 116, 117	ixxdisj 12479	. . . . . . . . . . . . . . . 16 ⊢ ((-∞ ∈ ℝ* ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((-∞(,](𝑧 − (1 / 𝑦))) ∩ ((𝑧 − (1 / 𝑦))(,)+∞)) = ∅)
128	64, 109, 127	mp3an13 1582	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 − (1 / 𝑦)) ∈ ℝ* → ((-∞(,](𝑧 − (1 / 𝑦))) ∩ ((𝑧 − (1 / 𝑦))(,)+∞)) = ∅)
129	108, 128	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((-∞(,](𝑧 − (1 / 𝑦))) ∩ ((𝑧 − (1 / 𝑦))(,)+∞)) = ∅)
130	126, 129	syl5eq 2874	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (((𝑧 − (1 / 𝑦))(,)+∞) ∩ (-∞(,](𝑧 − (1 / 𝑦)))) = ∅)
131		uneqdifeq 4281	. . . . . . . . . . . . 13 ⊢ ((((𝑧 − (1 / 𝑦))(,)+∞) ⊆ ℝ ∧ (((𝑧 − (1 / 𝑦))(,)+∞) ∩ (-∞(,](𝑧 − (1 / 𝑦)))) = ∅) → ((((𝑧 − (1 / 𝑦))(,)+∞) ∪ (-∞(,](𝑧 − (1 / 𝑦)))) = ℝ ↔ (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞)) = (-∞(,](𝑧 − (1 / 𝑦)))))
132	125, 130, 131	sylancr 583	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((((𝑧 − (1 / 𝑦))(,)+∞) ∪ (-∞(,](𝑧 − (1 / 𝑦)))) = ℝ ↔ (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞)) = (-∞(,](𝑧 − (1 / 𝑦)))))
133	124, 132	mpbid 224	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞)) = (-∞(,](𝑧 − (1 / 𝑦))))
134	133	imaeq2d 5708	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (◡𝐹 “ (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞))) = (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))))
135	106, 134	eqtr3d 2864	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞))) = (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))))
136	42	ad2antrr 719	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (◡𝐹 “ ℝ) ∈ dom vol)
137		oveq1 6913	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑧 − (1 / 𝑦)) → (𝑥(,)+∞) = ((𝑧 − (1 / 𝑦))(,)+∞))
138	137	imaeq2d 5708	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑧 − (1 / 𝑦)) → (◡𝐹 “ (𝑥(,)+∞)) = (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞)))
139	138	eleq1d 2892	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 − (1 / 𝑦)) → ((◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol ↔ (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞)) ∈ dom vol))
140	32	ad2antrr 719	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ∀𝑥 ∈ ℝ (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol)
141	139, 140, 56	rspcdva 3533	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞)) ∈ dom vol)
142		difmbl 23710	. . . . . . . . . 10 ⊢ (((◡𝐹 “ ℝ) ∈ dom vol ∧ (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞)) ∈ dom vol) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞))) ∈ dom vol)
143	136, 141, 142	syl2anc 581	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞))) ∈ dom vol)
144	135, 143	eqeltrrd 2908	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol)
145	144	ralrimiva 3176	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∀𝑦 ∈ ℕ (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol)
146		iunmbl 23720	. . . . . . 7 ⊢ (∀𝑦 ∈ ℕ (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol → ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol)
147	145, 146	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol)
148	101, 147	eqeltrrd 2908	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑧)) ∈ dom vol)
149	148	ralrimiva 3176	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ ℝ (◡𝐹 “ (-∞(,)𝑧)) ∈ dom vol)
150		oveq2 6914	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (-∞(,)𝑧) = (-∞(,)𝑥))
151	150	imaeq2d 5708	. . . . . 6 ⊢ (𝑧 = 𝑥 → (◡𝐹 “ (-∞(,)𝑧)) = (◡𝐹 “ (-∞(,)𝑥)))
152	151	eleq1d 2892	. . . . 5 ⊢ (𝑧 = 𝑥 → ((◡𝐹 “ (-∞(,)𝑧)) ∈ dom vol ↔ (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol))
153	152	cbvralv 3384	. . . 4 ⊢ (∀𝑧 ∈ ℝ (◡𝐹 “ (-∞(,)𝑧)) ∈ dom vol ↔ ∀𝑥 ∈ ℝ (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol)
154	149, 153	sylib 210	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ℝ (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol)
155	154	r19.21bi 3142	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol)
156	1, 43, 31, 155	ismbf2d 23807	1 ⊢ (𝜑 → 𝐹 ∈ MblFn)

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1113   = wceq 1658   ∈ wcel 2166  ∀wral 3118  ∃wrex 3119   ∖ cdif 3796   ∪ cun 3797   ∩ cin 3798   ⊆ wss 3799  ∅c0 4145  ∪ ciun 4741   class class class wbr 4874  ^◡ccnv 5342  dom cdm 5343   “ cima 5346  Fun wfun 6118  ⟶wf 6120  (class class class)co 6906  ℝcr 10252  0cc0 10253  1c1 10254  +∞cpnf 10389  -∞cmnf 10390  ℝ^*cxr 10391   < clt 10392   ≤ cle 10393   − cmin 10586  -cneg 10587   / cdiv 11010  ℕcn 11351  ℝ⁺crp 12113  (,)cioo 12464  (,]cioc 12465  volcvol 23630  MblFncmbf 23781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-rep 4995  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210  ax-inf2 8816  ax-cc 9573  ax-cnex 10309  ax-resscn 10310  ax-1cn 10311  ax-icn 10312  ax-addcl 10313  ax-addrcl 10314  ax-mulcl 10315  ax-mulrcl 10316  ax-mulcom 10317  ax-addass 10318  ax-mulass 10319  ax-distr 10320  ax-i2m1 10321  ax-1ne0 10322  ax-1rid 10323  ax-rnegex 10324  ax-rrecex 10325  ax-cnre 10326  ax-pre-lttri 10327  ax-pre-lttrn 10328  ax-pre-ltadd 10329  ax-pre-mulgt0 10330  ax-pre-sup 10331

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-fal 1672  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-nel 3104  df-ral 3123  df-rex 3124  df-reu 3125  df-rmo 3126  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-pss 3815  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4660  df-int 4699  df-iun 4743  df-disj 4843  df-br 4875  df-opab 4937  df-mpt 4954  df-tr 4977  df-id 5251  df-eprel 5256  df-po 5264  df-so 5265  df-fr 5302  df-se 5303  df-we 5304  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-pred 5921  df-ord 5967  df-on 5968  df-lim 5969  df-suc 5970  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-isom 6133  df-riota 6867  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-of 7158  df-om 7328  df-1st 7429  df-2nd 7430  df-wrecs 7673  df-recs 7735  df-rdg 7773  df-1o 7827  df-2o 7828  df-oadd 7831  df-er 8010  df-map 8125  df-pm 8126  df-en 8224  df-dom 8225  df-sdom 8226  df-fin 8227  df-sup 8618  df-inf 8619  df-oi 8685  df-card 9079  df-cda 9306  df-pnf 10394  df-mnf 10395  df-xr 10396  df-ltxr 10397  df-le 10398  df-sub 10588  df-neg 10589  df-div 11011  df-nn 11352  df-2 11415  df-3 11416  df-n0 11620  df-z 11706  df-uz 11970  df-q 12073  df-rp 12114  df-xadd 12234  df-ioo 12468  df-ioc 12469  df-ico 12470  df-icc 12471  df-fz 12621  df-fzo 12762  df-fl 12889  df-seq 13097  df-exp 13156  df-hash 13412  df-cj 14217  df-re 14218  df-im 14219  df-sqrt 14353  df-abs 14354  df-clim 14597  df-rlim 14598  df-sum 14795  df-xmet 20100  df-met 20101  df-ovol 23631  df-vol 23632  df-mbf 23786

This theorem is referenced by:  mbfaddlem  23827  mbfsup  23831