volsup2

Description: The volume of A is the supremum of the sequence vol*( A i^i ( -u n , n ) ) of volumes of bounded sets. (Contributed by Mario Carneiro, 30-Aug-2014)

		Ref	Expression
	Assertion	volsup2	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to \exists n \in ℕ B < vol (A \cap [- n, n])$

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to B < vol (A)$
2		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
3	2	3ad2ant2	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to B \in ℝ^{*}$
4		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
5		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
6	5	ffvelrni	$⊢ A \in dom vol \to vol (A) \in [0, +∞]$
7	4 6	sselid	$⊢ A \in dom vol \to vol (A) \in ℝ^{*}$
8	7	3ad2ant1	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to vol (A) \in ℝ^{*}$
9		xrltnle	$⊢ (B \in ℝ^{} \land vol (A) \in ℝ^{}) \to (B < vol (A) \leftrightarrow \neg vol (A) \leq B)$
10	3 8 9	syl2anc	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to (B < vol (A) \leftrightarrow \neg vol (A) \leq B)$
11	1 10	mpbid	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to \neg vol (A) \leq B$
12		negeq	$⊢ m = n \to - m = - n$
13		id	$⊢ m = n \to m = n$
14	12 13	oveq12d	$⊢ m = n \to [- m, m] = [- n, n]$
15	14	ineq2d	$⊢ m = n \to A \cap [- m, m] = A \cap [- n, n]$
16		eqid	$⊢ (m \in ℕ ⟼ A \cap [- m, m]) = (m \in ℕ ⟼ A \cap [- m, m])$
17		ovex	$⊢ [- n, n] \in V$
18	17	inex2	$⊢ A \cap [- n, n] \in V$
19	15 16 18	fvmpt	$⊢ n \in ℕ \to (m \in ℕ ⟼ A \cap [- m, m]) (n) = A \cap [- n, n]$
20	19	iuneq2i	$⊢ ⋃_{n \in ℕ} (m \in ℕ ⟼ A \cap [- m, m]) (n) = ⋃_{n \in ℕ} (A \cap [- n, n])$
21		iunin2	$⊢ ⋃_{n \in ℕ} (A \cap [- n, n]) = A \cap ⋃_{n \in ℕ} [- n, n]$
22	20 21	eqtri	$⊢ ⋃_{n \in ℕ} (m \in ℕ ⟼ A \cap [- m, m]) (n) = A \cap ⋃_{n \in ℕ} [- n, n]$
23		simpl1	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to A \in dom vol$
24		nnre	$⊢ n \in ℕ \to n \in ℝ$
25	24	adantl	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to n \in ℝ$
26	25	renegcld	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to - n \in ℝ$
27		iccmbl	$⊢ (- n \in ℝ \land n \in ℝ) \to [- n, n] \in dom vol$
28	26 25 27	syl2anc	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to [- n, n] \in dom vol$
29		inmbl	$⊢ (A \in dom vol \land [- n, n] \in dom vol) \to A \cap [- n, n] \in dom vol$
30	23 28 29	syl2anc	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to A \cap [- n, n] \in dom vol$
31	15	cbvmptv	$⊢ (m \in ℕ ⟼ A \cap [- m, m]) = (n \in ℕ ⟼ A \cap [- n, n])$
32	30 31	fmptd	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to (m \in ℕ ⟼ A \cap [- m, m]) : ℕ ⟶ dom vol$
33	32	ffnd	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to (m \in ℕ ⟼ A \cap [- m, m]) Fn ℕ$
34		fniunfv	$⊢ (m \in ℕ ⟼ A \cap [- m, m]) Fn ℕ \to ⋃_{n \in ℕ} (m \in ℕ ⟼ A \cap [- m, m]) (n) = ⋃ ran (m \in ℕ ⟼ A \cap [- m, m])$
35	33 34	syl	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to ⋃_{n \in ℕ} (m \in ℕ ⟼ A \cap [- m, m]) (n) = ⋃ ran (m \in ℕ ⟼ A \cap [- m, m])$
36		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
37	36	3ad2ant1	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to A \subseteq ℝ$
38	37	sselda	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land x \in A) \to x \in ℝ$
39		recn	$⊢ x \in ℝ \to x \in ℂ$
40	39	abscld	$⊢ x \in ℝ \to \|x\| \in ℝ$
41		arch	$⊢ \|x\| \in ℝ \to \exists n \in ℕ \|x\| < n$
42	40 41	syl	$⊢ x \in ℝ \to \exists n \in ℕ \|x\| < n$
43		ltle	$⊢ (\|x\| \in ℝ \land n \in ℝ) \to (\|x\| < n \to \|x\| \leq n)$
44	40 24 43	syl2an	$⊢ (x \in ℝ \land n \in ℕ) \to (\|x\| < n \to \|x\| \leq n)$
45		id	$⊢ (x \in ℝ \land - n \leq x \land x \leq n) \to (x \in ℝ \land - n \leq x \land x \leq n)$
46	45	3expib	$⊢ x \in ℝ \to ((- n \leq x \land x \leq n) \to (x \in ℝ \land - n \leq x \land x \leq n))$
47	46	adantr	$⊢ (x \in ℝ \land n \in ℕ) \to ((- n \leq x \land x \leq n) \to (x \in ℝ \land - n \leq x \land x \leq n))$
48		absle	$⊢ (x \in ℝ \land n \in ℝ) \to (\|x\| \leq n \leftrightarrow (- n \leq x \land x \leq n))$
49	24 48	sylan2	$⊢ (x \in ℝ \land n \in ℕ) \to (\|x\| \leq n \leftrightarrow (- n \leq x \land x \leq n))$
50	24	adantl	$⊢ (x \in ℝ \land n \in ℕ) \to n \in ℝ$
51	50	renegcld	$⊢ (x \in ℝ \land n \in ℕ) \to - n \in ℝ$
52		elicc2	$⊢ (- n \in ℝ \land n \in ℝ) \to (x \in [- n, n] \leftrightarrow (x \in ℝ \land - n \leq x \land x \leq n))$
53	51 50 52	syl2anc	$⊢ (x \in ℝ \land n \in ℕ) \to (x \in [- n, n] \leftrightarrow (x \in ℝ \land - n \leq x \land x \leq n))$
54	47 49 53	3imtr4d	$⊢ (x \in ℝ \land n \in ℕ) \to (\|x\| \leq n \to x \in [- n, n])$
55	44 54	syld	$⊢ (x \in ℝ \land n \in ℕ) \to (\|x\| < n \to x \in [- n, n])$
56	55	reximdva	$⊢ x \in ℝ \to (\exists n \in ℕ \|x\| < n \to \exists n \in ℕ x \in [- n, n])$
57	42 56	mpd	$⊢ x \in ℝ \to \exists n \in ℕ x \in [- n, n]$
58	38 57	syl	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land x \in A) \to \exists n \in ℕ x \in [- n, n]$
59	58	ex	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to (x \in A \to \exists n \in ℕ x \in [- n, n])$
60		eliun	$⊢ x \in ⋃_{n \in ℕ} [- n, n] \leftrightarrow \exists n \in ℕ x \in [- n, n]$
61	59 60	syl6ibr	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to (x \in A \to x \in ⋃_{n \in ℕ} [- n, n])$
62	61	ssrdv	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to A \subseteq ⋃_{n \in ℕ} [- n, n]$
63		df-ss	$⊢ A \subseteq ⋃_{n \in ℕ} [- n, n] \leftrightarrow A \cap ⋃_{n \in ℕ} [- n, n] = A$
64	62 63	sylib	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to A \cap ⋃_{n \in ℕ} [- n, n] = A$
65	22 35 64	3eqtr3a	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to ⋃ ran (m \in ℕ ⟼ A \cap [- m, m]) = A$
66	65	fveq2d	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to vol (⋃ ran (m \in ℕ ⟼ A \cap [- m, m])) = vol (A)$
67		peano2re	$⊢ n \in ℝ \to n + 1 \in ℝ$
68	25 67	syl	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to n + 1 \in ℝ$
69	68	renegcld	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to - (n + 1) \in ℝ$
70	25	lep1d	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to n \leq n + 1$
71	25 68	lenegd	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to (n \leq n + 1 \leftrightarrow - (n + 1) \leq - n)$
72	70 71	mpbid	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to - (n + 1) \leq - n$
73		iccss	$⊢ ((- (n + 1) \in ℝ \land n + 1 \in ℝ) \land (- (n + 1) \leq - n \land n \leq n + 1)) \to [- n, n] \subseteq [- (n + 1), n + 1]$
74	69 68 72 70 73	syl22anc	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to [- n, n] \subseteq [- (n + 1), n + 1]$
75		sslin	$⊢ [- n, n] \subseteq [- (n + 1), n + 1] \to A \cap [- n, n] \subseteq A \cap [- (n + 1), n + 1]$
76	74 75	syl	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to A \cap [- n, n] \subseteq A \cap [- (n + 1), n + 1]$
77	19	adantl	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to (m \in ℕ ⟼ A \cap [- m, m]) (n) = A \cap [- n, n]$
78		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
79	78	adantl	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to n + 1 \in ℕ$
80		negeq	$⊢ m = n + 1 \to - m = - (n + 1)$
81		id	$⊢ m = n + 1 \to m = n + 1$
82	80 81	oveq12d	$⊢ m = n + 1 \to [- m, m] = [- (n + 1), n + 1]$
83	82	ineq2d	$⊢ m = n + 1 \to A \cap [- m, m] = A \cap [- (n + 1), n + 1]$
84		ovex	$⊢ [- (n + 1), n + 1] \in V$
85	84	inex2	$⊢ A \cap [- (n + 1), n + 1] \in V$
86	83 16 85	fvmpt	$⊢ n + 1 \in ℕ \to (m \in ℕ ⟼ A \cap [- m, m]) (n + 1) = A \cap [- (n + 1), n + 1]$
87	79 86	syl	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to (m \in ℕ ⟼ A \cap [- m, m]) (n + 1) = A \cap [- (n + 1), n + 1]$
88	76 77 87	3sstr4d	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to (m \in ℕ ⟼ A \cap [- m, m]) (n) \subseteq (m \in ℕ ⟼ A \cap [- m, m]) (n + 1)$
89	88	ralrimiva	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to \forall n \in ℕ (m \in ℕ ⟼ A \cap [- m, m]) (n) \subseteq (m \in ℕ ⟼ A \cap [- m, m]) (n + 1)$
90		volsup	$⊢ ((m \in ℕ ⟼ A \cap [- m, m]) : ℕ ⟶ dom vol \land \forall n \in ℕ (m \in ℕ ⟼ A \cap [- m, m]) (n) \subseteq (m \in ℕ ⟼ A \cap [- m, m]) (n + 1)) \to vol (⋃ ran (m \in ℕ ⟼ A \cap [- m, m])) = sup (vol [ran (m \in ℕ ⟼ A \cap [- m, m])] ℝ^{*} <)$
91	32 89 90	syl2anc	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to vol (⋃ ran (m \in ℕ ⟼ A \cap [- m, m])) = sup (vol [ran (m \in ℕ ⟼ A \cap [- m, m])] ℝ^{*} <)$
92	66 91	eqtr3d	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to vol (A) = sup (vol [ran (m \in ℕ ⟼ A \cap [- m, m])] ℝ^{*} <)$
93	92	breq1d	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to (vol (A) \leq B \leftrightarrow sup (vol [ran (m \in ℕ ⟼ A \cap [- m, m])] ℝ^{*} <) \leq B)$
94		imassrn	$⊢ vol [ran (m \in ℕ ⟼ A \cap [- m, m])] \subseteq ran vol$
95		frn	$⊢ vol : dom vol ⟶ [0, +∞] \to ran vol \subseteq [0, +∞]$
96	5 95	ax-mp	$⊢ ran vol \subseteq [0, +∞]$
97	96 4	sstri	$⊢ ran vol \subseteq ℝ^{*}$
98	94 97	sstri	$⊢ vol [ran (m \in ℕ ⟼ A \cap [- m, m])] \subseteq ℝ^{*}$
99		supxrleub	$⊢ (vol [ran (m \in ℕ ⟼ A \cap [- m, m])] \subseteq ℝ^{} \land B \in ℝ^{}) \to (sup (vol [ran (m \in ℕ ⟼ A \cap [- m, m])] ℝ^{*} <) \leq B \leftrightarrow \forall n \in vol [ran (m \in ℕ ⟼ A \cap [- m, m])] n \leq B)$
100	98 3 99	sylancr	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to (sup (vol [ran (m \in ℕ ⟼ A \cap [- m, m])] ℝ^{*} <) \leq B \leftrightarrow \forall n \in vol [ran (m \in ℕ ⟼ A \cap [- m, m])] n \leq B)$
101		ffn	$⊢ vol : dom vol ⟶ [0, +∞] \to vol Fn dom vol$
102	5 101	ax-mp	$⊢ vol Fn dom vol$
103	32	frnd	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to ran (m \in ℕ ⟼ A \cap [- m, m]) \subseteq dom vol$
104		breq1	$⊢ n = vol (z) \to (n \leq B \leftrightarrow vol (z) \leq B)$
105	104	ralima	$⊢ (vol Fn dom vol \land ran (m \in ℕ ⟼ A \cap [- m, m]) \subseteq dom vol) \to (\forall n \in vol [ran (m \in ℕ ⟼ A \cap [- m, m])] n \leq B \leftrightarrow \forall z \in ran (m \in ℕ ⟼ A \cap [- m, m]) vol (z) \leq B)$
106	102 103 105	sylancr	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to (\forall n \in vol [ran (m \in ℕ ⟼ A \cap [- m, m])] n \leq B \leftrightarrow \forall z \in ran (m \in ℕ ⟼ A \cap [- m, m]) vol (z) \leq B)$
107		fveq2	$⊢ z = (m \in ℕ ⟼ A \cap [- m, m]) (n) \to vol (z) = vol ((m \in ℕ ⟼ A \cap [- m, m]) (n))$
108	107	breq1d	$⊢ z = (m \in ℕ ⟼ A \cap [- m, m]) (n) \to (vol (z) \leq B \leftrightarrow vol ((m \in ℕ ⟼ A \cap [- m, m]) (n)) \leq B)$
109	108	ralrn	$⊢ (m \in ℕ ⟼ A \cap [- m, m]) Fn ℕ \to (\forall z \in ran (m \in ℕ ⟼ A \cap [- m, m]) vol (z) \leq B \leftrightarrow \forall n \in ℕ vol ((m \in ℕ ⟼ A \cap [- m, m]) (n)) \leq B)$
110	33 109	syl	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to (\forall z \in ran (m \in ℕ ⟼ A \cap [- m, m]) vol (z) \leq B \leftrightarrow \forall n \in ℕ vol ((m \in ℕ ⟼ A \cap [- m, m]) (n)) \leq B)$
111	19	fveq2d	$⊢ n \in ℕ \to vol ((m \in ℕ ⟼ A \cap [- m, m]) (n)) = vol (A \cap [- n, n])$
112	111	breq1d	$⊢ n \in ℕ \to (vol ((m \in ℕ ⟼ A \cap [- m, m]) (n)) \leq B \leftrightarrow vol (A \cap [- n, n]) \leq B)$
113	112	ralbiia	$⊢ \forall n \in ℕ vol ((m \in ℕ ⟼ A \cap [- m, m]) (n)) \leq B \leftrightarrow \forall n \in ℕ vol (A \cap [- n, n]) \leq B$
114	110 113	bitrdi	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to (\forall z \in ran (m \in ℕ ⟼ A \cap [- m, m]) vol (z) \leq B \leftrightarrow \forall n \in ℕ vol (A \cap [- n, n]) \leq B)$
115	106 114	bitrd	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to (\forall n \in vol [ran (m \in ℕ ⟼ A \cap [- m, m])] n \leq B \leftrightarrow \forall n \in ℕ vol (A \cap [- n, n]) \leq B)$
116	93 100 115	3bitrd	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to (vol (A) \leq B \leftrightarrow \forall n \in ℕ vol (A \cap [- n, n]) \leq B)$
117	11 116	mtbid	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to \neg \forall n \in ℕ vol (A \cap [- n, n]) \leq B$
118		rexnal	$⊢ \exists n \in ℕ \neg vol (A \cap [- n, n]) \leq B \leftrightarrow \neg \forall n \in ℕ vol (A \cap [- n, n]) \leq B$
119	117 118	sylibr	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to \exists n \in ℕ \neg vol (A \cap [- n, n]) \leq B$
120	3	adantr	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to B \in ℝ^{*}$
121	5	ffvelrni	$⊢ A \cap [- n, n] \in dom vol \to vol (A \cap [- n, n]) \in [0, +∞]$
122	4 121	sselid	$⊢ A \cap [- n, n] \in dom vol \to vol (A \cap [- n, n]) \in ℝ^{*}$
123	30 122	syl	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to vol (A \cap [- n, n]) \in ℝ^{*}$
124		xrltnle	$⊢ (B \in ℝ^{} \land vol (A \cap [- n, n]) \in ℝ^{}) \to (B < vol (A \cap [- n, n]) \leftrightarrow \neg vol (A \cap [- n, n]) \leq B)$
125	120 123 124	syl2anc	$⊢ ((A \in dom vol \land B \in ℝ \land B < vol (A)) \land n \in ℕ) \to (B < vol (A \cap [- n, n]) \leftrightarrow \neg vol (A \cap [- n, n]) \leq B)$
126	125	rexbidva	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to (\exists n \in ℕ B < vol (A \cap [- n, n]) \leftrightarrow \exists n \in ℕ \neg vol (A \cap [- n, n]) \leq B)$
127	119 126	mpbird	$⊢ (A \in dom vol \land B \in ℝ \land B < vol (A)) \to \exists n \in ℕ B < vol (A \cap [- n, n])$

Metamath Proof Explorer

Theorem volsup2

Proof