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 25806

Description: Lemma for ibladd 25807. (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 4509	. . . 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 11166	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℝ)
6	2, 5	eqeltrd 2839	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ ℝ)
7		0re 11138	. . . . . . . . 9 ⊢ 0 ∈ ℝ
8		ifcl 4501	. . . . . . . . 9 ⊢ ((𝐷 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ)
9	6, 7, 8	sylancl 592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ)
10	9	rexrd 11187	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ^*)
11		max1 13129	. . . . . . . 8 ⊢ ((0 ∈ ℝ ∧ 𝐷 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐷, 𝐷, 0))
12	7, 6, 11	sylancr 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐷, 𝐷, 0))
13		elxrge0 13402	. . . . . . 7 ⊢ (if(0 ≤ 𝐷, 𝐷, 0) ∈ (0[,]+∞) ↔ (if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ^* ∧ 0 ≤ if(0 ≤ 𝐷, 𝐷, 0)))
14	10, 12, 13	sylanbrc 589	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈ (0[,]+∞))
15		0e0iccpnf 13404	. . . . . . 7 ⊢ 0 ∈ (0[,]+∞)
16	15	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ (0[,]+∞))
17	14, 16	ifclda 4491	. . . . 5 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ∈ (0[,]+∞))
18	17	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ∈ (0[,]+∞))
19	1, 18	eqeltrid 2843	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ∈ (0[,]+∞))
20	19	fmpttd 7057	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)):ℝ⟶(0[,]+∞))
21		reex 11121	. . . . . . . 8 ⊢ ℝ ∈ V
22	21	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ V)
23		ifan 4509	. . . . . . . . 9 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0)
24		ifcl 4501	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
25	3, 7, 24	sylancl 592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
26	7	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ ℝ)
27	25, 26	ifclda 4491	. . . . . . . . 9 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) ∈ ℝ)
28	23, 27	eqeltrid 2843	. . . . . . . 8 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ)
29	28	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ)
30		ifan 4509	. . . . . . . . 9 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0)
31		ifcl 4501	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
32	4, 7, 31	sylancl 592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
33	32, 26	ifclda 4491	. . . . . . . . 9 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) ∈ ℝ)
34	30, 33	eqeltrid 2843	. . . . . . . 8 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ)
35	34	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ)
36		eqidd 2740	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)))
37		eqidd 2740	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))
38	22, 29, 35, 36, 37	offval2 7641	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘_f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))))
39		iftrue 4461	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
40		ibar 533	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (0 ≤ 𝐵 ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵)))
41	40	ifbid 4479	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → if(0 ≤ 𝐵, 𝐵, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))
42		ibar 533	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (0 ≤ 𝐶 ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
43	42	ifbid 4479	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → if(0 ≤ 𝐶, 𝐶, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))
44	41, 43	oveq12d 7375	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))
45	39, 44	eqtr2d 2775	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
46		00id 11313	. . . . . . . . 9 ⊢ (0 + 0) = 0
47		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) → 𝑥 ∈ 𝐴)
48	47	con3i 154	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵))
49	48	iffalsed 4466	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = 0)
50		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶) → 𝑥 ∈ 𝐴)
51	50	con3i 154	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶))
52	51	iffalsed 4466	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = 0)
53	49, 52	oveq12d 7375	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = (0 + 0))
54		iffalse 4464	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = 0)
55	46, 53, 54	3eqtr4a 2800	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
56	45, 55	pm2.61i 183	. . . . . . 7 ⊢ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)
57	56	mpteq2i 5169	. . . . . 6 ⊢ (𝑥 ∈ ℝ ↦ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
58	38, 57	eqtrdi 2790	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘_f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))
59	58	fveq2d 6832	. . . 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 25623	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ dom vol)
62		mblss 25517	. . . . . . 7 ⊢ (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
63	61, 62	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
64		rembl 25526	. . . . . . 7 ⊢ ℝ ∈ dom vol
65	64	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ ∈ dom vol)
66	28	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ)
67		eldifn 4063	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℝ ∖ 𝐴) → ¬ 𝑥 ∈ 𝐴)
68	67	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ 𝑥 ∈ 𝐴)
69	68	intnanrd 490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵))
70	69	iffalsed 4466	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = 0)
71	41	mpteq2ia 5168	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))
72	3, 60	mbfpos 25637	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn)
73	71, 72	eqeltrrid 2844	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∈ MblFn)
74	63, 65, 66, 70, 73	mbfss 25632	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∈ MblFn)
75		max1 13129	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0))
76	7, 3, 75	sylancr 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0))
77		elrege0 13399	. . . . . . . . . 10 ⊢ (if(0 ≤ 𝐵, 𝐵, 0) ∈ (0[,)+∞) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ 𝐵, 𝐵, 0)))
78	25, 76, 77	sylanbrc 589	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ (0[,)+∞))
79		0e0icopnf 13403	. . . . . . . . . 10 ⊢ 0 ∈ (0[,)+∞)
80	79	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ (0[,)+∞))
81	78, 80	ifclda 4491	. . . . . . . 8 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) ∈ (0[,)+∞))
82	23, 81	eqeltrid 2843	. . . . . . 7 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ (0[,)+∞))
83	82	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ (0[,)+∞))
84	83	fmpttd 7057	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)):ℝ⟶(0[,)+∞))
85		ibladd.6	. . . . 5 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ)
86	34	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ)
87	68, 52	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = 0)
88	43	mpteq2ia 5168	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))
89		ibladd.5	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
90	4, 89	mbfpos 25637	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) ∈ MblFn)
91	88, 90	eqeltrrid 2844	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) ∈ MblFn)
92	63, 65, 86, 87, 91	mbfss 25632	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) ∈ MblFn)
93		max1 13129	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0))
94	7, 4, 93	sylancr 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0))
95		elrege0 13399	. . . . . . . . . 10 ⊢ (if(0 ≤ 𝐶, 𝐶, 0) ∈ (0[,)+∞) ↔ (if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ 𝐶, 𝐶, 0)))
96	32, 94, 95	sylanbrc 589	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ (0[,)+∞))
97	96, 80	ifclda 4491	. . . . . . . 8 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) ∈ (0[,)+∞))
98	30, 97	eqeltrid 2843	. . . . . . 7 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ (0[,)+∞))
99	98	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ (0[,)+∞))
100	99	fmpttd 7057	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)):ℝ⟶(0[,)+∞))
101		ibladd.7	. . . . 5 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ)
102	74, 84, 85, 92, 100, 101	itg2add 25745	. . . 4 ⊢ (𝜑 → (∫₂‘((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘_f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))))
103	59, 102	eqtr3d 2776	. . 3 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))))
104	85, 101	readdcld 11166	. . 3 ⊢ (𝜑 → ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) ∈ ℝ)
105	103, 104	eqeltrd 2839	. 2 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) ∈ ℝ)
106	25, 32	readdcld 11166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ)
107	106	rexrd 11187	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ^*)
108	25, 32, 76, 94	addge0d 11718	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
109		elxrge0 13402	. . . . . . 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 589	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ (0[,]+∞))
111	110, 16	ifclda 4491	. . . . 5 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) ∈ (0[,]+∞))
112	111	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) ∈ (0[,]+∞))
113	112	fmpttd 7057	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)):ℝ⟶(0[,]+∞))
114		max2 13131	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ if(0 ≤ 𝐵, 𝐵, 0))
115	7, 3, 114	sylancr 593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ if(0 ≤ 𝐵, 𝐵, 0))
116		max2 13131	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ≤ if(0 ≤ 𝐶, 𝐶, 0))
117	7, 4, 116	sylancr 593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≤ if(0 ≤ 𝐶, 𝐶, 0))
118	3, 4, 25, 32, 115, 117	le2addd 11761	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
119	2, 118	eqbrtrd 5095	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
120		breq1 5076	. . . . . . . . . . 11 ⊢ (𝐷 = if(0 ≤ 𝐷, 𝐷, 0) → (𝐷 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ↔ if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
121		breq1 5076	. . . . . . . . . . 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 4495	. . . . . . . . . 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 590	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
124		iftrue 4461	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = if(0 ≤ 𝐷, 𝐷, 0))
125	124	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = if(0 ≤ 𝐷, 𝐷, 0))
126	39	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
127	123, 125, 126	3brtr4d 5105	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
128	127	ex 413	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))
129		0le0 12274	. . . . . . . . 9 ⊢ 0 ≤ 0
130	129	a1i 11	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → 0 ≤ 0)
131		iffalse 4464	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = 0)
132	130, 131, 54	3brtr4d 5105	. . . . . . 7 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
133	128, 132	pm2.61d1 181	. . . . . 6 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
134	1, 133	eqbrtrid 5108	. . . . 5 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
135	134	ralrimivw 3135	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))
136		eqidd 2740	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)))
137		eqidd 2740	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))
138	22, 19, 112, 136, 137	ofrfval2 7642	. . . 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 258	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))
140		itg2le 25725	. . 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 1379	. 2 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))))
142		itg2lecl 25724	. 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 1379	1 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1547 ∈ wcel 2119 ∀wral 3053 Vcvv 3431 ∖ cdif 3880 ⊆ wss 3883 ifcif 4455 class class class wbr 5073 ↦ cmpt 5154 dom cdm 5619 ⟶wf 6482 ‘cfv 6486 (class class class)co 7357 ∘_f cof 7619 ∘_r cofr 7620 ℝcr 11029 0cc0 11030 + caddc 11033 +∞cpnf 11168 ℝ^*cxr 11170 ≤ cle 11172 [,)cico 13292 [,]cicc 13293 volcvol 25449 MblFncmbf 25600 ∫₂citg2 25602

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5200 ax-sep 5219 ax-nul 5229 ax-pow 5295 ax-pr 5363 ax-un 7679 ax-inf2 9554 ax-cc 10349 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107 ax-pre-sup 11108 ax-addf 11109

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4263 df-if 4456 df-pw 4532 df-sn 4557 df-pr 4559 df-op 4563 df-uni 4840 df-int 4879 df-iun 4924 df-disj 5041 df-br 5074 df-opab 5136 df-mpt 5155 df-tr 5181 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7314 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7621 df-ofr 7622 df-om 7808 df-1st 7932 df-2nd 7933 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-2o 8397 df-oadd 8400 df-omul 8401 df-er 8634 df-map 8766 df-pm 8767 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-fi 9315 df-sup 9346 df-inf 9347 df-oi 9416 df-dju 9817 df-card 9855 df-acn 9858 df-pnf 11173 df-mnf 11174 df-xr 11175 df-ltxr 11176 df-le 11177 df-sub 11371 df-neg 11372 df-div 11800 df-nn 12167 df-2 12236 df-3 12237 df-n0 12430 df-z 12517 df-uz 12781 df-q 12891 df-rp 12935 df-xneg 13055 df-xadd 13056 df-xmul 13057 df-ioo 13294 df-ioc 13295 df-ico 13296 df-icc 13297 df-fz 13454 df-fzo 13601 df-fl 13743 df-seq 13956 df-exp 14016 df-hash 14285 df-cj 15053 df-re 15054 df-im 15055 df-sqrt 15189 df-abs 15190 df-clim 15442 df-rlim 15443 df-sum 15641 df-rest 17377 df-topgen 17398 df-psmet 21340 df-xmet 21341 df-met 21342 df-bl 21343 df-mopn 21344 df-top 22878 df-topon 22895 df-bases 22930 df-cmp 23371 df-ovol 25450 df-vol 25451 df-mbf 25605 df-itg1 25606 df-itg2 25607 df-0p 25656

This theorem is referenced by: ibladd 25807

W3C validator