itg2const2

Description: When the base set of a constant function has infinite volume, the integral is also infinite and vice-versa. (Contributed by Mario Carneiro, 30-Aug-2014)

		Ref	Expression
	Assertion	itg2const2	$⊢ (A \in dom vol \land B \in ℝ^{+}) \to (vol (A) \in ℝ \leftrightarrow \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ)$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land vol (A) \in ℝ) \to A \in dom vol$
2		simpr	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land vol (A) \in ℝ) \to vol (A) \in ℝ$
3		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
4	3	ad2antlr	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land vol (A) \in ℝ) \to B \in ℝ$
5		rpge0	$⊢ B \in ℝ^{+} \to 0 \leq B$
6	5	ad2antlr	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land vol (A) \in ℝ) \to 0 \leq B$
7		elrege0	$⊢ B \in [0, +∞) \leftrightarrow (B \in ℝ \land 0 \leq B)$
8	4 6 7	sylanbrc	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land vol (A) \in ℝ) \to B \in [0, +∞)$
9		itg2const	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) = B vol (A)$
10	1 2 8 9	syl3anc	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land vol (A) \in ℝ) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) = B vol (A)$
11	4 2	remulcld	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land vol (A) \in ℝ) \to B vol (A) \in ℝ$
12	10 11	eqeltrd	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land vol (A) \in ℝ) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ$
13		mblvol	$⊢ A \in dom vol \to vol (A) = {vol}^{*} (A)$
14	13	ad2antrr	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to vol (A) = {vol}^{*} (A)$
15		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
16	15	ad3antrrr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land {vol}^{*} (A) \leq \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}) \to A \subseteq ℝ$
17		peano2re	$⊢ \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1 \in ℝ$
18	17	adantl	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1 \in ℝ$
19		simplr	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to B \in ℝ^{+}$
20	18 19	rerpdivcld	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in ℝ$
21	20	adantr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land {vol}^{*} (A) \leq \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}) \to \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in ℝ$
22		simpr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land {vol}^{} (A) \leq \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}) \to {vol}^{} (A) \leq \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}$
23		ovollecl	$⊢ (A \subseteq ℝ \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in ℝ \land {vol}^{} (A) \leq \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}) \to {vol}^{} (A) \in ℝ$
24	16 21 22 23	syl3anc	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land {vol}^{} (A) \leq \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}) \to {vol}^{} (A) \in ℝ$
25		simplll	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{*} (A)) \to A \in dom vol$
26	20	adantr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{*} (A)) \to \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in ℝ$
27	26	rexrd	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{} (A)) \to \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in ℝ^{}$
28		simpr	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ$
29	3	ad2antlr	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land x \in ℝ) \to B \in ℝ$
30	29	rexrd	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land x \in ℝ) \to B \in ℝ^{*}$
31	5	ad2antlr	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land x \in ℝ) \to 0 \leq B$
32		elxrge0	$⊢ B \in [0, +∞] \leftrightarrow (B \in ℝ^{*} \land 0 \leq B)$
33	30 31 32	sylanbrc	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land x \in ℝ) \to B \in [0, +∞]$
34		0e0iccpnf	$⊢ 0 \in [0, +∞]$
35		ifcl	$⊢ (B \in [0, +∞] \land 0 \in [0, +∞]) \to if (x \in A, B, 0) \in [0, +∞]$
36	33 34 35	sylancl	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land x \in ℝ) \to if (x \in A, B, 0) \in [0, +∞]$
37	36	fmpttd	$⊢ (A \in dom vol \land B \in ℝ^{+}) \to (x \in ℝ ⟼ if (x \in A, B, 0)) : ℝ ⟶ [0, +∞]$
38	37	adantr	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to (x \in ℝ ⟼ if (x \in A, B, 0)) : ℝ ⟶ [0, +∞]$
39		itg2ge0	$⊢ (x \in ℝ ⟼ if (x \in A, B, 0)) : ℝ ⟶ [0, +∞] \to 0 \leq \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0)))$
40	38 39	syl	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to 0 \leq \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0)))$
41	28 40	ge0p1rpd	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1 \in ℝ^{+}$
42	41 19	rpdivcld	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in ℝ^{+}$
43	42	rpge0d	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to 0 \leq \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}$
44	43	adantr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{*} (A)) \to 0 \leq \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}$
45	14	breq2d	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to (\frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq vol (A) \leftrightarrow \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{*} (A))$
46	45	biimpar	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{*} (A)) \to \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq vol (A)$
47		0xr	$⊢ 0 \in ℝ^{*}$
48		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
49		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
50	49	ffvelcdmi	$⊢ A \in dom vol \to vol (A) \in [0, +∞]$
51	48 50	sselid	$⊢ A \in dom vol \to vol (A) \in ℝ^{*}$
52	25 51	syl	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{} (A)) \to vol (A) \in ℝ^{}$
53		elicc1	$⊢ (0 \in ℝ^{} \land vol (A) \in ℝ^{}) \to (\frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in [0, vol (A)] \leftrightarrow (\frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in ℝ^{*} \land 0 \leq \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq vol (A)))$
54	47 52 53	sylancr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{} (A)) \to (\frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in [0, vol (A)] \leftrightarrow (\frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in ℝ^{} \land 0 \leq \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq vol (A)))$
55	27 44 46 54	mpbir3and	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{*} (A)) \to \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in [0, vol (A)]$
56		volivth	$⊢ (A \in dom vol \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in [0, vol (A)]) \to \exists z \in dom vol (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B})$
57	25 55 56	syl2anc	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{*} (A)) \to \exists z \in dom vol (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B})$
58	57	ex	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to (\frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{*} (A) \to \exists z \in dom vol (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))$
59		simprl	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to z \in dom vol$
60		simprrr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}$
61	20	adantr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in ℝ$
62	60 61	eqeltrd	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to vol (z) \in ℝ$
63	3	ad2antlr	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to B \in ℝ$
64	63	adantr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to B \in ℝ$
65	19	adantr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to B \in ℝ^{+}$
66	65	rpge0d	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to 0 \leq B$
67	64 66 7	sylanbrc	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to B \in [0, +∞)$
68		itg2const	$⊢ (z \in dom vol \land vol (z) \in ℝ \land B \in [0, +∞)) \to \int^{2} ((x \in ℝ ⟼ if (x \in z, B, 0))) = B vol (z)$
69	59 62 67 68	syl3anc	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to \int^{2} ((x \in ℝ ⟼ if (x \in z, B, 0))) = B vol (z)$
70	60	oveq2d	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to B vol (z) = B (\frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B})$
71	18	recnd	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1 \in ℂ$
72	63	recnd	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to B \in ℂ$
73		rpne0	$⊢ B \in ℝ^{+} \to B \neq 0$
74	73	ad2antlr	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to B \neq 0$
75	71 72 74	divcan2d	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to B (\frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}) = \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1$
76	75	adantr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to B (\frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}) = \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1$
77	69 70 76	3eqtrd	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to \int^{2} ((x \in ℝ ⟼ if (x \in z, B, 0))) = \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1$
78	3	adantl	$⊢ (A \in dom vol \land B \in ℝ^{+}) \to B \in ℝ$
79	78	rexrd	$⊢ (A \in dom vol \land B \in ℝ^{+}) \to B \in ℝ^{*}$
80	5	adantl	$⊢ (A \in dom vol \land B \in ℝ^{+}) \to 0 \leq B$
81	79 80 32	sylanbrc	$⊢ (A \in dom vol \land B \in ℝ^{+}) \to B \in [0, +∞]$
82		ifcl	$⊢ (B \in [0, +∞] \land 0 \in [0, +∞]) \to if (x \in z, B, 0) \in [0, +∞]$
83	81 34 82	sylancl	$⊢ (A \in dom vol \land B \in ℝ^{+}) \to if (x \in z, B, 0) \in [0, +∞]$
84	83	adantr	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land x \in ℝ) \to if (x \in z, B, 0) \in [0, +∞]$
85	84	fmpttd	$⊢ (A \in dom vol \land B \in ℝ^{+}) \to (x \in ℝ ⟼ if (x \in z, B, 0)) : ℝ ⟶ [0, +∞]$
86	85	ad2antrr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to (x \in ℝ ⟼ if (x \in z, B, 0)) : ℝ ⟶ [0, +∞]$
87	38	adantr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to (x \in ℝ ⟼ if (x \in A, B, 0)) : ℝ ⟶ [0, +∞]$
88		simpl	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to (A \in dom vol \land B \in ℝ^{+})$
89		simprl	$⊢ (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B})) \to z \subseteq A$
90	78	ad3antrrr	$⊢ ((((A \in dom vol \land B \in ℝ^{+}) \land z \subseteq A) \land x \in ℝ) \land x \in z) \to B \in ℝ$
91	90	leidd	$⊢ ((((A \in dom vol \land B \in ℝ^{+}) \land z \subseteq A) \land x \in ℝ) \land x \in z) \to B \leq B$
92		iftrue	$⊢ x \in z \to if (x \in z, B, 0) = B$
93	92	adantl	$⊢ ((((A \in dom vol \land B \in ℝ^{+}) \land z \subseteq A) \land x \in ℝ) \land x \in z) \to if (x \in z, B, 0) = B$
94		simplr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land z \subseteq A) \land x \in ℝ) \to z \subseteq A$
95	94	sselda	$⊢ ((((A \in dom vol \land B \in ℝ^{+}) \land z \subseteq A) \land x \in ℝ) \land x \in z) \to x \in A$
96	95	iftrued	$⊢ ((((A \in dom vol \land B \in ℝ^{+}) \land z \subseteq A) \land x \in ℝ) \land x \in z) \to if (x \in A, B, 0) = B$
97	91 93 96	3brtr4d	$⊢ ((((A \in dom vol \land B \in ℝ^{+}) \land z \subseteq A) \land x \in ℝ) \land x \in z) \to if (x \in z, B, 0) \leq if (x \in A, B, 0)$
98		iffalse	$⊢ \neg x \in z \to if (x \in z, B, 0) = 0$
99	98	adantl	$⊢ ((((A \in dom vol \land B \in ℝ^{+}) \land z \subseteq A) \land x \in ℝ) \land \neg x \in z) \to if (x \in z, B, 0) = 0$
100		0le0	$⊢ 0 \leq 0$
101		breq2	$⊢ B = if (x \in A, B, 0) \to (0 \leq B \leftrightarrow 0 \leq if (x \in A, B, 0))$
102		breq2	$⊢ 0 = if (x \in A, B, 0) \to (0 \leq 0 \leftrightarrow 0 \leq if (x \in A, B, 0))$
103	101 102	ifboth	$⊢ (0 \leq B \land 0 \leq 0) \to 0 \leq if (x \in A, B, 0)$
104	80 100 103	sylancl	$⊢ (A \in dom vol \land B \in ℝ^{+}) \to 0 \leq if (x \in A, B, 0)$
105	104	ad3antrrr	$⊢ ((((A \in dom vol \land B \in ℝ^{+}) \land z \subseteq A) \land x \in ℝ) \land \neg x \in z) \to 0 \leq if (x \in A, B, 0)$
106	99 105	eqbrtrd	$⊢ ((((A \in dom vol \land B \in ℝ^{+}) \land z \subseteq A) \land x \in ℝ) \land \neg x \in z) \to if (x \in z, B, 0) \leq if (x \in A, B, 0)$
107	97 106	pm2.61dan	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land z \subseteq A) \land x \in ℝ) \to if (x \in z, B, 0) \leq if (x \in A, B, 0)$
108	107	ralrimiva	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land z \subseteq A) \to \forall x \in ℝ if (x \in z, B, 0) \leq if (x \in A, B, 0)$
109		reex	$⊢ ℝ \in V$
110	109	a1i	$⊢ (A \in dom vol \land B \in ℝ^{+}) \to ℝ \in V$
111		eqidd	$⊢ (A \in dom vol \land B \in ℝ^{+}) \to (x \in ℝ ⟼ if (x \in z, B, 0)) = (x \in ℝ ⟼ if (x \in z, B, 0))$
112		eqidd	$⊢ (A \in dom vol \land B \in ℝ^{+}) \to (x \in ℝ ⟼ if (x \in A, B, 0)) = (x \in ℝ ⟼ if (x \in A, B, 0))$
113	110 84 36 111 112	ofrfval2	$⊢ (A \in dom vol \land B \in ℝ^{+}) \to ((x \in ℝ ⟼ if (x \in z, B, 0)) \leq_{f} (x \in ℝ ⟼ if (x \in A, B, 0)) \leftrightarrow \forall x \in ℝ if (x \in z, B, 0) \leq if (x \in A, B, 0))$
114	113	biimpar	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \forall x \in ℝ if (x \in z, B, 0) \leq if (x \in A, B, 0)) \to (x \in ℝ ⟼ if (x \in z, B, 0)) \leq_{f} (x \in ℝ ⟼ if (x \in A, B, 0))$
115	108 114	syldan	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land z \subseteq A) \to (x \in ℝ ⟼ if (x \in z, B, 0)) \leq_{f} (x \in ℝ ⟼ if (x \in A, B, 0))$
116	88 89 115	syl2an	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to (x \in ℝ ⟼ if (x \in z, B, 0)) \leq_{f} (x \in ℝ ⟼ if (x \in A, B, 0))$
117		itg2le	$⊢ ((x \in ℝ ⟼ if (x \in z, B, 0)) : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in A, B, 0)) : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in z, B, 0)) \leq_{f} (x \in ℝ ⟼ if (x \in A, B, 0))) \to \int^{2} ((x \in ℝ ⟼ if (x \in z, B, 0))) \leq \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0)))$
118	86 87 116 117	syl3anc	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to \int^{2} ((x \in ℝ ⟼ if (x \in z, B, 0))) \leq \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0)))$
119	77 118	eqbrtrrd	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1 \leq \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0)))$
120		ltp1	$⊢ \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) < \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1$
121	120	ad2antlr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) < \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1$
122		simplr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ$
123	17	ad2antlr	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1 \in ℝ$
124	122 123	ltnled	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to (\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) < \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1 \leftrightarrow \neg \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1 \leq \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))))$
125	121 124	mpbid	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to \neg \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1 \leq \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0)))$
126	119 125	pm2.21dd	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land (z \in dom vol \land (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}))) \to {vol}^{*} (A) \in ℝ$
127	126	rexlimdvaa	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to (\exists z \in dom vol (z \subseteq A \land vol (z) = \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B}) \to {vol}^{*} (A) \in ℝ)$
128	58 127	syld	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to (\frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{} (A) \to {vol}^{} (A) \in ℝ)$
129	128	imp	$⊢ (((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{} (A)) \to {vol}^{} (A) \in ℝ$
130	51	ad2antrr	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to vol (A) \in ℝ^{*}$
131	14 130	eqeltrrd	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to {vol}^{} (A) \in ℝ^{}$
132	20	rexrd	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in ℝ^{*}$
133		xrletri	$⊢ ({vol}^{} (A) \in ℝ^{} \land \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \in ℝ^{}) \to ({vol}^{} (A) \leq \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \lor \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{*} (A))$
134	131 132 133	syl2anc	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to ({vol}^{} (A) \leq \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \lor \frac{\int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) + 1}{B} \leq {vol}^{} (A))$
135	24 129 134	mpjaodan	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to {vol}^{*} (A) \in ℝ$
136	14 135	eqeltrd	$⊢ ((A \in dom vol \land B \in ℝ^{+}) \land \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ) \to vol (A) \in ℝ$
137	12 136	impbida	$⊢ (A \in dom vol \land B \in ℝ^{+}) \to (vol (A) \in ℝ \leftrightarrow \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) \in ℝ)$

Metamath Proof Explorer

Theorem itg2const2

Proof