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 25979

Description: Lemma for ibladd 25980. (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 4541	. . . 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 11233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℝ)
6	2, 5	eqeltrd 2863	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ ℝ)
7		0re 11205	. . . . . . . . 9 ⊢ 0 ∈ ℝ
8		ifcl 4533	. . . . . . . . 9 ⊢ ((𝐷 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ)
9	6, 7, 8	sylancl 597	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ)
10	9	rexrd 11254	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ^*)
11		max1 13206	. . . . . . . 8 ⊢ ((0 ∈ ℝ ∧ 𝐷 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐷, 𝐷, 0))
12	7, 6, 11	sylancr 598	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐷, 𝐷, 0))
13		elxrge0 13479	. . . . . . 7 ⊢ (if(0 ≤ 𝐷, 𝐷, 0) ∈ (0[,]+∞) ↔ (if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ^* ∧ 0 ≤ if(0 ≤ 𝐷, 𝐷, 0)))
14	10, 12, 13	sylanbrc 594	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈ (0[,]+∞))
15		0e0iccpnf 13481	. . . . . . 7 ⊢ 0 ∈ (0[,]+∞)
16	15	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ (0[,]+∞))
17	14, 16	ifclda 4523	. . . . 5 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ∈ (0[,]+∞))
18	17	adantr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ∈ (0[,]+∞))
19	1, 18	eqeltrid 2867	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ∈ (0[,]+∞))
20	19	fmpttd 7110	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)):ℝ⟶(0[,]+∞))
21		reex 11186	. . . . . . . 8 ⊢ ℝ ∈ V
22	21	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ V)
23		ifan 4541	. . . . . . . . 9 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0)
24		ifcl 4533	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
25	3, 7, 24	sylancl 597	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
26	7	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ ℝ)
27	25, 26	ifclda 4523	. . . . . . . . 9 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) ∈ ℝ)
28	23, 27	eqeltrid 2867	. . . . . . . 8 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ)
29	28	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ)
30		ifan 4541	. . . . . . . . 9 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0)
31		ifcl 4533	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
32	4, 7, 31	sylancl 597	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
33	32, 26	ifclda 4523	. . . . . . . . 9 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) ∈ ℝ)
34	30, 33	eqeltrid 2867	. . . . . . . 8 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ)
35	34	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ)
36		eqidd 2764	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)))
37		eqidd 2764	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))
38	22, 29, 35, 36, 37	offval2 7694	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘_f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))))
39		iftrue 4493	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
40		ibar 537	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (0 ≤ 𝐵 ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵)))
41	40	ifbid 4511	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → if(0 ≤ 𝐵, 𝐵, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))
42		ibar 537	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (0 ≤ 𝐶 ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
43	42	ifbid 4511	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → if(0 ≤ 𝐶, 𝐶, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))
44	41, 43	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))
45	39, 44	eqtr2d 2799	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
46		00id 11380	. . . . . . . . 9 ⊢ (0 + 0) = 0
47		simpl 487	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) → 𝑥 ∈ 𝐴)
48	47	con3i 155	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵))
49	48	iffalsed 4498	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = 0)
50		simpl 487	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶) → 𝑥 ∈ 𝐴)
51	50	con3i 155	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶))
52	51	iffalsed 4498	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = 0)
53	49, 52	oveq12d 7428	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = (0 + 0))
54		iffalse 4496	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = 0)
55	46, 53, 54	3eqtr4a 2824	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
56	45, 55	pm2.61i 184	. . . . . . 7 ⊢ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)
57	56	mpteq2i 5207	. . . . . 6 ⊢ (𝑥 ∈ ℝ ↦ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
58	38, 57	eqtrdi 2814	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘_f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))
59	58	fveq2d 6885	. . . 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 25796	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ dom vol)
62		mblss 25690	. . . . . . 7 ⊢ (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
63	61, 62	syl 18	. . . . . 6 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
64		rembl 25699	. . . . . . 7 ⊢ ℝ ∈ dom vol
65	64	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ ∈ dom vol)
66	28	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ)
67		eldifn 4086	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℝ ∖ 𝐴) → ¬ 𝑥 ∈ 𝐴)
68	67	adantl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ 𝑥 ∈ 𝐴)
69	68	intnanrd 494	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵))
70	69	iffalsed 4498	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = 0)
71	41	mpteq2ia 5206	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))
72	3, 60	mbfpos 25810	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn)
73	71, 72	eqeltrrid 2868	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∈ MblFn)
74	63, 65, 66, 70, 73	mbfss 25805	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∈ MblFn)
75		max1 13206	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0))
76	7, 3, 75	sylancr 598	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0))
77		elrege0 13476	. . . . . . . . . 10 ⊢ (if(0 ≤ 𝐵, 𝐵, 0) ∈ (0[,)+∞) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ 𝐵, 𝐵, 0)))
78	25, 76, 77	sylanbrc 594	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ (0[,)+∞))
79		0e0icopnf 13480	. . . . . . . . . 10 ⊢ 0 ∈ (0[,)+∞)
80	79	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ (0[,)+∞))
81	78, 80	ifclda 4523	. . . . . . . 8 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) ∈ (0[,)+∞))
82	23, 81	eqeltrid 2867	. . . . . . 7 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ (0[,)+∞))
83	82	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ (0[,)+∞))
84	83	fmpttd 7110	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)):ℝ⟶(0[,)+∞))
85		ibladd.6	. . . . 5 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ)
86	34	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ)
87	68, 52	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = 0)
88	43	mpteq2ia 5206	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))
89		ibladd.5	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
90	4, 89	mbfpos 25810	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) ∈ MblFn)
91	88, 90	eqeltrrid 2868	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) ∈ MblFn)
92	63, 65, 86, 87, 91	mbfss 25805	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) ∈ MblFn)
93		max1 13206	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0))
94	7, 4, 93	sylancr 598	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0))
95		elrege0 13476	. . . . . . . . . 10 ⊢ (if(0 ≤ 𝐶, 𝐶, 0) ∈ (0[,)+∞) ↔ (if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ 𝐶, 𝐶, 0)))
96	32, 94, 95	sylanbrc 594	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ (0[,)+∞))
97	96, 80	ifclda 4523	. . . . . . . 8 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) ∈ (0[,)+∞))
98	30, 97	eqeltrid 2867	. . . . . . 7 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ (0[,)+∞))
99	98	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ (0[,)+∞))
100	99	fmpttd 7110	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)):ℝ⟶(0[,)+∞))
101		ibladd.7	. . . . 5 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ)
102	74, 84, 85, 92, 100, 101	itg2add 25918	. . . 4 ⊢ (𝜑 → (∫₂‘((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘_f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))))
103	59, 102	eqtr3d 2800	. . 3 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))))
104	85, 101	readdcld 11233	. . 3 ⊢ (𝜑 → ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) ∈ ℝ)
105	103, 104	eqeltrd 2863	. 2 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) ∈ ℝ)
106	25, 32	readdcld 11233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ)
107	106	rexrd 11254	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ^*)
108	25, 32, 76, 94	addge0d 11785	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
109		elxrge0 13479	. . . . . . 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 594	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ (0[,]+∞))
111	110, 16	ifclda 4523	. . . . 5 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) ∈ (0[,]+∞))
112	111	adantr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) ∈ (0[,]+∞))
113	112	fmpttd 7110	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)):ℝ⟶(0[,]+∞))
114		max2 13208	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ if(0 ≤ 𝐵, 𝐵, 0))
115	7, 3, 114	sylancr 598	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ if(0 ≤ 𝐵, 𝐵, 0))
116		max2 13208	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ≤ if(0 ≤ 𝐶, 𝐶, 0))
117	7, 4, 116	sylancr 598	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≤ if(0 ≤ 𝐶, 𝐶, 0))
118	3, 4, 25, 32, 115, 117	le2addd 11828	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
119	2, 118	eqbrtrd 5133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
120		breq1 5112	. . . . . . . . . . 11 ⊢ (𝐷 = if(0 ≤ 𝐷, 𝐷, 0) → (𝐷 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ↔ if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
121		breq1 5112	. . . . . . . . . . 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 4527	. . . . . . . . . 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 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
124		iftrue 4493	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = if(0 ≤ 𝐷, 𝐷, 0))
125	124	adantl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = if(0 ≤ 𝐷, 𝐷, 0))
126	39	adantl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
127	123, 125, 126	3brtr4d 5143	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
128	127	ex 417	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))
129		0le0 12337	. . . . . . . . 9 ⊢ 0 ≤ 0
130	129	a1i 11	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → 0 ≤ 0)
131		iffalse 4496	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = 0)
132	130, 131, 54	3brtr4d 5143	. . . . . . 7 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
133	128, 132	pm2.61d1 182	. . . . . 6 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
134	1, 133	eqbrtrid 5146	. . . . 5 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
135	134	ralrimivw 3161	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
136		eqidd 2764	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)))
137		eqidd 2764	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))
138	22, 19, 112, 136, 137	ofrfval2 7695	. . . 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 260	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))
140		itg2le 25898	. . 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 1398	. 2 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))))
142		itg2lecl 25897	. 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 1398	1 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 = wceq 1570 ∈ wcel 2143 ∀wral 3079 Vcvv 3455 ∖ cdif 3902 ⊆ wss 3905 ifcif 4487 class class class wbr 5109 ↦ cmpt 5192 dom cdm 5661 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ∘_f cof 7672 ∘_r cofr 7673 ℝcr 11094 0cc0 11095 + caddc 11098 +∞cpnf 11235 ℝ^*cxr 11237 ≤ cle 11239 [,)cico 13369 [,]cicc 13370 volcvol 25622 MblFncmbf 25773 ∫₂citg2 25775

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-inf2 9606 ax-cc 10414 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172 ax-pre-sup 11173 ax-addf 11174

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-disj 5077 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-ofr 7675 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-2o 8450 df-oadd 8453 df-omul 8454 df-er 8690 df-map 8822 df-pm 8823 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fi 9367 df-sup 9398 df-inf 9399 df-oi 9468 df-dju 9883 df-card 9921 df-acn 9924 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-div 11867 df-nn 12229 df-2 12298 df-3 12299 df-n0 12500 df-z 12587 df-uz 12858 df-q 12968 df-rp 13012 df-xneg 13132 df-xadd 13133 df-xmul 13134 df-ioo 13371 df-ioc 13372 df-ico 13373 df-icc 13374 df-fz 13531 df-fzo 13679 df-fl 13821 df-seq 14034 df-exp 14094 df-hash 14363 df-cj 15146 df-re 15147 df-im 15148 df-sqrt 15282 df-abs 15283 df-clim 15535 df-rlim 15536 df-sum 15734 df-rest 17470 df-topgen 17491 df-psmet 21514 df-xmet 21515 df-met 21516 df-bl 21517 df-mopn 21518 df-top 23051 df-topon 23068 df-bases 23103 df-cmp 23544 df-ovol 25623 df-vol 25624 df-mbf 25778 df-itg1 25779 df-itg2 25780 df-0p 25829

This theorem is referenced by: ibladd 25980

W3C validator