ibladdlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ibladdlem		Structured version Visualization version GIF version

Theorem ibladdlem 25775

Description: Lemma for ibladd 25776. (Contributed by Mario Carneiro, 17-Aug-2014.)

**Hypotheses**
Ref	Expression
ibladd.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
ibladd.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)
ibladd.3	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 = (𝐵 + 𝐶))
ibladd.4	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
ibladd.5	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
ibladd.6	⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ)
ibladd.7	⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ)

**Assertion**
Ref	Expression
ibladdlem	⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ)

Distinct variable groups: 𝑥,𝐴 𝜑,𝑥 Allowed substitution hints: 𝐵(𝑥) 𝐶(𝑥) 𝐷(𝑥)

**Proof of Theorem ibladdlem**
Step	Hyp	Ref	Expression
1		ifan 4531	. . . 4 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0)
2		ibladd.3	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 = (𝐵 + 𝐶))
3		ibladd.1	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
4		ibladd.2	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)
5	3, 4	readdcld 11159	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℝ)
6	2, 5	eqeltrd 2834	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ ℝ)
7		0re 11132	. . . . . . . . 9 ⊢ 0 ∈ ℝ
8		ifcl 4523	. . . . . . . . 9 ⊢ ((𝐷 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ)
9	6, 7, 8	sylancl 586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ)
10	9	rexrd 11180	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ^*)
11		max1 13098	. . . . . . . 8 ⊢ ((0 ∈ ℝ ∧ 𝐷 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐷, 𝐷, 0))
12	7, 6, 11	sylancr 587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐷, 𝐷, 0))
13		elxrge0 13371	. . . . . . 7 ⊢ (if(0 ≤ 𝐷, 𝐷, 0) ∈ (0[,]+∞) ↔ (if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ^* ∧ 0 ≤ if(0 ≤ 𝐷, 𝐷, 0)))
14	10, 12, 13	sylanbrc 583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈ (0[,]+∞))
15		0e0iccpnf 13373	. . . . . . 7 ⊢ 0 ∈ (0[,]+∞)
16	15	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ (0[,]+∞))
17	14, 16	ifclda 4513	. . . . 5 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ∈ (0[,]+∞))
18	17	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ∈ (0[,]+∞))
19	1, 18	eqeltrid 2838	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ∈ (0[,]+∞))
20	19	fmpttd 7058	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)):ℝ⟶(0[,]+∞))
21		reex 11115	. . . . . . . 8 ⊢ ℝ ∈ V
22	21	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ V)
23		ifan 4531	. . . . . . . . 9 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0)
24		ifcl 4523	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
25	3, 7, 24	sylancl 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
26	7	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ ℝ)
27	25, 26	ifclda 4513	. . . . . . . . 9 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) ∈ ℝ)
28	23, 27	eqeltrid 2838	. . . . . . . 8 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ)
29	28	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ)
30		ifan 4531	. . . . . . . . 9 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0)
31		ifcl 4523	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
32	4, 7, 31	sylancl 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
33	32, 26	ifclda 4513	. . . . . . . . 9 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) ∈ ℝ)
34	30, 33	eqeltrid 2838	. . . . . . . 8 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ)
35	34	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ)
36		eqidd 2735	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)))
37		eqidd 2735	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))
38	22, 29, 35, 36, 37	offval2 7640	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘_f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))))
39		iftrue 4483	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
40		ibar 528	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (0 ≤ 𝐵 ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵)))
41	40	ifbid 4501	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → if(0 ≤ 𝐵, 𝐵, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))
42		ibar 528	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (0 ≤ 𝐶 ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
43	42	ifbid 4501	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → if(0 ≤ 𝐶, 𝐶, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))
44	41, 43	oveq12d 7374	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))
45	39, 44	eqtr2d 2770	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
46		00id 11306	. . . . . . . . 9 ⊢ (0 + 0) = 0
47		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) → 𝑥 ∈ 𝐴)
48	47	con3i 154	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵))
49	48	iffalsed 4488	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = 0)
50		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶) → 𝑥 ∈ 𝐴)
51	50	con3i 154	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶))
52	51	iffalsed 4488	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = 0)
53	49, 52	oveq12d 7374	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = (0 + 0))
54		iffalse 4486	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = 0)
55	46, 53, 54	3eqtr4a 2795	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
56	45, 55	pm2.61i 182	. . . . . . 7 ⊢ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)
57	56	mpteq2i 5192	. . . . . 6 ⊢ (𝑥 ∈ ℝ ↦ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
58	38, 57	eqtrdi 2785	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘_f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))
59	58	fveq2d 6836	. . . 4 ⊢ (𝜑 → (∫₂‘((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘_f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) = (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))))
60		ibladd.4	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
61	60, 3	mbfdm2 25592	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ dom vol)
62		mblss 25486	. . . . . . 7 ⊢ (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
63	61, 62	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
64		rembl 25495	. . . . . . 7 ⊢ ℝ ∈ dom vol
65	64	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ ∈ dom vol)
66	28	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ)
67		eldifn 4082	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℝ ∖ 𝐴) → ¬ 𝑥 ∈ 𝐴)
68	67	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ 𝑥 ∈ 𝐴)
69	68	intnanrd 489	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵))
70	69	iffalsed 4488	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = 0)
71	41	mpteq2ia 5191	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))
72	3, 60	mbfpos 25606	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn)
73	71, 72	eqeltrrid 2839	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∈ MblFn)
74	63, 65, 66, 70, 73	mbfss 25601	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∈ MblFn)
75		max1 13098	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0))
76	7, 3, 75	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0))
77		elrege0 13368	. . . . . . . . . 10 ⊢ (if(0 ≤ 𝐵, 𝐵, 0) ∈ (0[,)+∞) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ 𝐵, 𝐵, 0)))
78	25, 76, 77	sylanbrc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ (0[,)+∞))
79		0e0icopnf 13372	. . . . . . . . . 10 ⊢ 0 ∈ (0[,)+∞)
80	79	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ (0[,)+∞))
81	78, 80	ifclda 4513	. . . . . . . 8 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) ∈ (0[,)+∞))
82	23, 81	eqeltrid 2838	. . . . . . 7 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ (0[,)+∞))
83	82	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ (0[,)+∞))
84	83	fmpttd 7058	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)):ℝ⟶(0[,)+∞))
85		ibladd.6	. . . . 5 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ)
86	34	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ)
87	68, 52	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = 0)
88	43	mpteq2ia 5191	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))
89		ibladd.5	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
90	4, 89	mbfpos 25606	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) ∈ MblFn)
91	88, 90	eqeltrrid 2839	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) ∈ MblFn)
92	63, 65, 86, 87, 91	mbfss 25601	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) ∈ MblFn)
93		max1 13098	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0))
94	7, 4, 93	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0))
95		elrege0 13368	. . . . . . . . . 10 ⊢ (if(0 ≤ 𝐶, 𝐶, 0) ∈ (0[,)+∞) ↔ (if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ 𝐶, 𝐶, 0)))
96	32, 94, 95	sylanbrc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ (0[,)+∞))
97	96, 80	ifclda 4513	. . . . . . . 8 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) ∈ (0[,)+∞))
98	30, 97	eqeltrid 2838	. . . . . . 7 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ (0[,)+∞))
99	98	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ (0[,)+∞))
100	99	fmpttd 7058	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)):ℝ⟶(0[,)+∞))
101		ibladd.7	. . . . 5 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ)
102	74, 84, 85, 92, 100, 101	itg2add 25714	. . . 4 ⊢ (𝜑 → (∫₂‘((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘_f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))))
103	59, 102	eqtr3d 2771	. . 3 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))))
104	85, 101	readdcld 11159	. . 3 ⊢ (𝜑 → ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) ∈ ℝ)
105	103, 104	eqeltrd 2834	. 2 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) ∈ ℝ)
106	25, 32	readdcld 11159	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ)
107	106	rexrd 11180	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ^*)
108	25, 32, 76, 94	addge0d 11711	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
109		elxrge0 13371	. . . . . . 7 ⊢ ((if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ (0[,]+∞) ↔ ((if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ^* ∧ 0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
110	107, 108, 109	sylanbrc 583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ (0[,]+∞))
111	110, 16	ifclda 4513	. . . . 5 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) ∈ (0[,]+∞))
112	111	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) ∈ (0[,]+∞))
113	112	fmpttd 7058	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)):ℝ⟶(0[,]+∞))
114		max2 13100	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ if(0 ≤ 𝐵, 𝐵, 0))
115	7, 3, 114	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ if(0 ≤ 𝐵, 𝐵, 0))
116		max2 13100	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ≤ if(0 ≤ 𝐶, 𝐶, 0))
117	7, 4, 116	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≤ if(0 ≤ 𝐶, 𝐶, 0))
118	3, 4, 25, 32, 115, 117	le2addd 11754	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
119	2, 118	eqbrtrd 5118	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
120		breq1 5099	. . . . . . . . . . 11 ⊢ (𝐷 = if(0 ≤ 𝐷, 𝐷, 0) → (𝐷 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ↔ if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
121		breq1 5099	. . . . . . . . . . 11 ⊢ (0 = if(0 ≤ 𝐷, 𝐷, 0) → (0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ↔ if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
122	120, 121	ifboth 4517	. . . . . . . . . 10 ⊢ ((𝐷 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∧ 0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) → if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
123	119, 108, 122	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
124		iftrue 4483	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = if(0 ≤ 𝐷, 𝐷, 0))
125	124	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = if(0 ≤ 𝐷, 𝐷, 0))
126	39	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
127	123, 125, 126	3brtr4d 5128	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
128	127	ex 412	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))
129		0le0 12244	. . . . . . . . 9 ⊢ 0 ≤ 0
130	129	a1i 11	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → 0 ≤ 0)
131		iffalse 4486	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = 0)
132	130, 131, 54	3brtr4d 5128	. . . . . . 7 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
133	128, 132	pm2.61d1 180	. . . . . 6 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
134	1, 133	eqbrtrid 5131	. . . . 5 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
135	134	ralrimivw 3130	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
136		eqidd 2735	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)))
137		eqidd 2735	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))
138	22, 19, 112, 136, 137	ofrfval2 7641	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) ↔ ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))
139	135, 138	mpbird 257	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))
140		itg2le 25694	. . 3 ⊢ (((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))))
141	20, 113, 139, 140	syl3anc 1373	. 2 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))))
142		itg2lecl 25693	. 2 ⊢ (((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ)
143	20, 105, 141, 142	syl3anc 1373	1 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ∀wral 3049 Vcvv 3438 ∖ cdif 3896 ⊆ wss 3899 ifcif 4477 class class class wbr 5096 ↦ cmpt 5177 dom cdm 5622 ⟶wf 6486 ‘cfv 6490 (class class class)co 7356 ∘_f cof 7618 ∘_r cofr 7619 ℝcr 11023 0cc0 11024 + caddc 11027 +∞cpnf 11161 ℝ^*cxr 11163 ≤ cle 11165 [,)cico 13261 [,]cicc 13262 volcvol 25418 MblFncmbf 25569 ∫₂citg2 25571

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678 ax-inf2 9548 ax-cc 10343 ax-cnex 11080 ax-resscn 11081 ax-1cn 11082 ax-icn 11083 ax-addcl 11084 ax-addrcl 11085 ax-mulcl 11086 ax-mulrcl 11087 ax-mulcom 11088 ax-addass 11089 ax-mulass 11090 ax-distr 11091 ax-i2m1 11092 ax-1ne0 11093 ax-1rid 11094 ax-rnegex 11095 ax-rrecex 11096 ax-cnre 11097 ax-pre-lttri 11098 ax-pre-lttrn 11099 ax-pre-ltadd 11100 ax-pre-mulgt0 11101 ax-pre-sup 11102 ax-addf 11103

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-rmo 3348 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4862 df-int 4901 df-iun 4946 df-disj 5064 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-se 5576 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-isom 6499 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-of 7620 df-ofr 7621 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-oadd 8399 df-omul 8400 df-er 8633 df-map 8763 df-pm 8764 df-en 8882 df-dom 8883 df-sdom 8884 df-fin 8885 df-fi 9312 df-sup 9343 df-inf 9344 df-oi 9413 df-dju 9811 df-card 9849 df-acn 9852 df-pnf 11166 df-mnf 11167 df-xr 11168 df-ltxr 11169 df-le 11170 df-sub 11364 df-neg 11365 df-div 11793 df-nn 12144 df-2 12206 df-3 12207 df-n0 12400 df-z 12487 df-uz 12750 df-q 12860 df-rp 12904 df-xneg 13024 df-xadd 13025 df-xmul 13026 df-ioo 13263 df-ioc 13264 df-ico 13265 df-icc 13266 df-fz 13422 df-fzo 13569 df-fl 13710 df-seq 13923 df-exp 13983 df-hash 14252 df-cj 15020 df-re 15021 df-im 15022 df-sqrt 15156 df-abs 15157 df-clim 15409 df-rlim 15410 df-sum 15608 df-rest 17340 df-topgen 17361 df-psmet 21299 df-xmet 21300 df-met 21301 df-bl 21302 df-mopn 21303 df-top 22836 df-topon 22853 df-bases 22888 df-cmp 23329 df-ovol 25419 df-vol 25420 df-mbf 25574 df-itg1 25575 df-itg2 25576 df-0p 25625

This theorem is referenced by: ibladd 25776

W3C validator