vitalilem4

	Ref	Expression
Hypotheses	vitali.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in [0, 1] \land y \in [0, 1]) \land x - y \in ℚ)\}$
	vitali.2	$⊢ S = [0, 1] / \underset{˙}{\sim}$
	vitali.3	$⊢ φ \to F Fn S$
	vitali.4	$⊢ φ \to \forall z \in S (z \neq \emptyset \to F (z) \in z)$
	vitali.5	$⊢ φ \to G : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1]$
	vitali.6	$⊢ T = (n \in ℕ ⟼ \{s \in ℝ \| s - G (n) \in ran F\})$
	vitali.7	$⊢ φ \to \neg ran F \in (𝒫 ℝ ∖ dom vol)$
Assertion	vitalilem4	$⊢ (φ \land m \in ℕ) \to {vol}^{*} (T (m)) = 0$

Proof

Step	Hyp	Ref	Expression
1		vitali.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in [0, 1] \land y \in [0, 1]) \land x - y \in ℚ)\}$
2		vitali.2	$⊢ S = [0, 1] / \underset{˙}{\sim}$
3		vitali.3	$⊢ φ \to F Fn S$
4		vitali.4	$⊢ φ \to \forall z \in S (z \neq \emptyset \to F (z) \in z)$
5		vitali.5	$⊢ φ \to G : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1]$
6		vitali.6	$⊢ T = (n \in ℕ ⟼ \{s \in ℝ \| s - G (n) \in ran F\})$
7		vitali.7	$⊢ φ \to \neg ran F \in (𝒫 ℝ ∖ dom vol)$
8		fveq2	$⊢ n = m \to G (n) = G (m)$
9	8	oveq2d	$⊢ n = m \to s - G (n) = s - G (m)$
10	9	eleq1d	$⊢ n = m \to (s - G (n) \in ran F \leftrightarrow s - G (m) \in ran F)$
11	10	rabbidv	$⊢ n = m \to \{s \in ℝ \| s - G (n) \in ran F\} = \{s \in ℝ \| s - G (m) \in ran F\}$
12		reex	$⊢ ℝ \in V$
13	12	rabex	$⊢ \{s \in ℝ \| s - G (m) \in ran F\} \in V$
14	11 6 13	fvmpt	$⊢ m \in ℕ \to T (m) = \{s \in ℝ \| s - G (m) \in ran F\}$
15	14	adantl	$⊢ (φ \land m \in ℕ) \to T (m) = \{s \in ℝ \| s - G (m) \in ran F\}$
16	15	fveq2d	$⊢ (φ \land m \in ℕ) \to {vol}^{} (T (m)) = {vol}^{} (\{s \in ℝ \| s - G (m) \in ran F\})$
17	1 2 3 4 5 6 7	vitalilem2	$⊢ φ \to (ran F \subseteq [0, 1] \land [0, 1] \subseteq ⋃_{m \in ℕ} T (m) \land ⋃_{m \in ℕ} T (m) \subseteq [- 1, 2])$
18	17	simp1d	$⊢ φ \to ran F \subseteq [0, 1]$
19		unitssre	$⊢ [0, 1] \subseteq ℝ$
20	18 19	sstrdi	$⊢ φ \to ran F \subseteq ℝ$
21	20	adantr	$⊢ (φ \land m \in ℕ) \to ran F \subseteq ℝ$
22		neg1rr	$⊢ - 1 \in ℝ$
23		1re	$⊢ 1 \in ℝ$
24		iccssre	$⊢ (- 1 \in ℝ \land 1 \in ℝ) \to [- 1, 1] \subseteq ℝ$
25	22 23 24	mp2an	$⊢ [- 1, 1] \subseteq ℝ$
26		f1of	$⊢ G : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \to G : ℕ ⟶ ℚ \cap [- 1, 1]$
27	5 26	syl	$⊢ φ \to G : ℕ ⟶ ℚ \cap [- 1, 1]$
28	27	ffvelrnda	$⊢ (φ \land m \in ℕ) \to G (m) \in (ℚ \cap [- 1, 1])$
29	28	elin2d	$⊢ (φ \land m \in ℕ) \to G (m) \in [- 1, 1]$
30	25 29	sseldi	$⊢ (φ \land m \in ℕ) \to G (m) \in ℝ$
31		eqidd	$⊢ (φ \land m \in ℕ) \to \{s \in ℝ \| s - G (m) \in ran F\} = \{s \in ℝ \| s - G (m) \in ran F\}$
32	21 30 31	ovolshft	$⊢ (φ \land m \in ℕ) \to {vol}^{} (ran F) = {vol}^{} (\{s \in ℝ \| s - G (m) \in ran F\})$
33	16 32	eqtr4d	$⊢ (φ \land m \in ℕ) \to {vol}^{} (T (m)) = {vol}^{} (ran F)$
34		3re	$⊢ 3 \in ℝ$
35	34	rexri	$⊢ 3 \in ℝ^{*}$
36	35	a1i	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to 3 \in ℝ^{}$
37		3rp	$⊢ 3 \in ℝ^{+}$
38		0re	$⊢ 0 \in ℝ$
39		0le1	$⊢ 0 \leq 1$
40		ovolicc	$⊢ (0 \in ℝ \land 1 \in ℝ \land 0 \leq 1) \to {vol}^{*} ([0, 1]) = 1 - 0$
41	38 23 39 40	mp3an	$⊢ {vol}^{*} ([0, 1]) = 1 - 0$
42		1m0e1	$⊢ 1 - 0 = 1$
43	41 42	eqtri	$⊢ {vol}^{*} ([0, 1]) = 1$
44	43 23	eqeltri	$⊢ {vol}^{*} ([0, 1]) \in ℝ$
45		ovolsscl	$⊢ (ran F \subseteq [0, 1] \land [0, 1] \subseteq ℝ \land {vol}^{} ([0, 1]) \in ℝ) \to {vol}^{} (ran F) \in ℝ$
46	19 44 45	mp3an23	$⊢ ran F \subseteq [0, 1] \to {vol}^{*} (ran F) \in ℝ$
47	18 46	syl	$⊢ φ \to {vol}^{*} (ran F) \in ℝ$
48	47	adantr	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to {vol}^{} (ran F) \in ℝ$
49		simpr	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to 0 < {vol}^{} (ran F)$
50	48 49	elrpd	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to {vol}^{} (ran F) \in ℝ^{+}$
51		rpdivcl	$⊢ (3 \in ℝ^{+} \land {vol}^{} (ran F) \in ℝ^{+}) \to \frac{3}{{vol}^{} (ran F)} \in ℝ^{+}$
52	37 50 51	sylancr	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to \frac{3}{{vol}^{} (ran F)} \in ℝ^{+}$
53	52	rpred	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to \frac{3}{{vol}^{} (ran F)} \in ℝ$
54	52	rpge0d	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to 0 \leq \frac{3}{{vol}^{} (ran F)}$
55		flge0nn0	$⊢ (\frac{3}{{vol}^{} (ran F)} \in ℝ \land 0 \leq \frac{3}{{vol}^{} (ran F)}) \to ⌊\frac{3}{{vol}^{*} (ran F)}⌋ \in ℕ_{0}$
56	53 54 55	syl2anc	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to ⌊\frac{3}{{vol}^{} (ran F)}⌋ \in ℕ_{0}$
57		nn0p1nn	$⊢ ⌊\frac{3}{{vol}^{} (ran F)}⌋ \in ℕ_{0} \to ⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1 \in ℕ$
58	56 57	syl	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to ⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1 \in ℕ$
59	58	nnred	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to ⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1 \in ℝ$
60	59 48	remulcld	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) {vol}^{*} (ran F) \in ℝ$
61	60	rexrd	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) {vol}^{} (ran F) \in ℝ^{}$
62	12	elpw2	$⊢ ran F \in 𝒫 ℝ \leftrightarrow ran F \subseteq ℝ$
63	20 62	sylibr	$⊢ φ \to ran F \in 𝒫 ℝ$
64	63	anim1i	$⊢ (φ \land \neg ran F \in dom vol) \to (ran F \in 𝒫 ℝ \land \neg ran F \in dom vol)$
65		eldif	$⊢ ran F \in (𝒫 ℝ ∖ dom vol) \leftrightarrow (ran F \in 𝒫 ℝ \land \neg ran F \in dom vol)$
66	64 65	sylibr	$⊢ (φ \land \neg ran F \in dom vol) \to ran F \in (𝒫 ℝ ∖ dom vol)$
67	66	ex	$⊢ φ \to (\neg ran F \in dom vol \to ran F \in (𝒫 ℝ ∖ dom vol))$
68	7 67	mt3d	$⊢ φ \to ran F \in dom vol$
69		inss1	$⊢ ℚ \cap [- 1, 1] \subseteq ℚ$
70		qssre	$⊢ ℚ \subseteq ℝ$
71	69 70	sstri	$⊢ ℚ \cap [- 1, 1] \subseteq ℝ$
72		fss	$⊢ (G : ℕ ⟶ ℚ \cap [- 1, 1] \land ℚ \cap [- 1, 1] \subseteq ℝ) \to G : ℕ ⟶ ℝ$
73	27 71 72	sylancl	$⊢ φ \to G : ℕ ⟶ ℝ$
74	73	ffvelrnda	$⊢ (φ \land n \in ℕ) \to G (n) \in ℝ$
75		shftmbl	$⊢ (ran F \in dom vol \land G (n) \in ℝ) \to \{s \in ℝ \| s - G (n) \in ran F\} \in dom vol$
76	68 74 75	syl2an2r	$⊢ (φ \land n \in ℕ) \to \{s \in ℝ \| s - G (n) \in ran F\} \in dom vol$
77	76 6	fmptd	$⊢ φ \to T : ℕ ⟶ dom vol$
78	77	ffvelrnda	$⊢ (φ \land m \in ℕ) \to T (m) \in dom vol$
79	78	ralrimiva	$⊢ φ \to \forall m \in ℕ T (m) \in dom vol$
80		iunmbl	$⊢ \forall m \in ℕ T (m) \in dom vol \to ⋃_{m \in ℕ} T (m) \in dom vol$
81	79 80	syl	$⊢ φ \to ⋃_{m \in ℕ} T (m) \in dom vol$
82		mblss	$⊢ ⋃_{m \in ℕ} T (m) \in dom vol \to ⋃_{m \in ℕ} T (m) \subseteq ℝ$
83		ovolcl	$⊢ ⋃_{m \in ℕ} T (m) \subseteq ℝ \to {vol}^{} (⋃_{m \in ℕ} T (m)) \in ℝ^{}$
84	81 82 83	3syl	$⊢ φ \to {vol}^{} (⋃_{m \in ℕ} T (m)) \in ℝ^{}$
85	84	adantr	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to {vol}^{} (⋃_{m \in ℕ} T (m)) \in ℝ^{*}$
86		flltp1	$⊢ \frac{3}{{vol}^{} (ran F)} \in ℝ \to \frac{3}{{vol}^{} (ran F)} < ⌊\frac{3}{{vol}^{*} (ran F)}⌋ + 1$
87	53 86	syl	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to \frac{3}{{vol}^{} (ran F)} < ⌊\frac{3}{{vol}^{*} (ran F)}⌋ + 1$
88	34	a1i	$⊢ (φ \land 0 < {vol}^{*} (ran F)) \to 3 \in ℝ$
89	88 59 50	ltdivmul2d	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to (\frac{3}{{vol}^{} (ran F)} < ⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1 \leftrightarrow 3 < (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) {vol}^{*} (ran F))$
90	87 89	mpbid	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to 3 < (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) {vol}^{*} (ran F)$
91		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
92		1zzd	$⊢ (φ \land 0 < {vol}^{*} (ran F)) \to 1 \in ℤ$
93		mblvol	$⊢ T (m) \in dom vol \to vol (T (m)) = {vol}^{*} (T (m))$
94	78 93	syl	$⊢ (φ \land m \in ℕ) \to vol (T (m)) = {vol}^{*} (T (m))$
95	94 33	eqtrd	$⊢ (φ \land m \in ℕ) \to vol (T (m)) = {vol}^{*} (ran F)$
96	47	adantr	$⊢ (φ \land m \in ℕ) \to {vol}^{*} (ran F) \in ℝ$
97	95 96	eqeltrd	$⊢ (φ \land m \in ℕ) \to vol (T (m)) \in ℝ$
98	97	adantlr	$⊢ ((φ \land 0 < {vol}^{*} (ran F)) \land m \in ℕ) \to vol (T (m)) \in ℝ$
99		eqid	$⊢ (m \in ℕ ⟼ vol (T (m))) = (m \in ℕ ⟼ vol (T (m)))$
100	98 99	fmptd	$⊢ (φ \land 0 < {vol}^{*} (ran F)) \to (m \in ℕ ⟼ vol (T (m))) : ℕ ⟶ ℝ$
101	100	ffvelrnda	$⊢ ((φ \land 0 < {vol}^{*} (ran F)) \land k \in ℕ) \to (m \in ℕ ⟼ vol (T (m))) (k) \in ℝ$
102	91 92 101	serfre	$⊢ (φ \land 0 < {vol}^{*} (ran F)) \to seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) : ℕ ⟶ ℝ$
103	102	frnd	$⊢ (φ \land 0 < {vol}^{*} (ran F)) \to ran seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) \subseteq ℝ$
104		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
105	103 104	sstrdi	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to ran seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) \subseteq ℝ^{}$
106	95	adantlr	$⊢ ((φ \land 0 < {vol}^{} (ran F)) \land m \in ℕ) \to vol (T (m)) = {vol}^{} (ran F)$
107	106	mpteq2dva	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to (m \in ℕ ⟼ vol (T (m))) = (m \in ℕ ⟼ {vol}^{} (ran F))$
108		fconstmpt	$⊢ ℕ \times \{{vol}^{} (ran F)\} = (m \in ℕ ⟼ {vol}^{} (ran F))$
109	107 108	eqtr4di	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to (m \in ℕ ⟼ vol (T (m))) = ℕ \times \{{vol}^{} (ran F)\}$
110	109	seqeq3d	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) = seq 1 (+ (ℕ \times \{{vol}^{} (ran F)\}))$
111	110	fveq1d	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) = seq 1 (+ (ℕ \times \{{vol}^{} (ran F)\})) (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1)$
112	48	recnd	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to {vol}^{} (ran F) \in ℂ$
113		ser1const	$⊢ ({vol}^{} (ran F) \in ℂ \land ⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1 \in ℕ) \to seq 1 (+ (ℕ \times \{{vol}^{} (ran F)\})) (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) = (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) {vol}^{} (ran F)$
114	112 58 113	syl2anc	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to seq 1 (+ (ℕ \times \{{vol}^{} (ran F)\})) (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) = (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) {vol}^{*} (ran F)$
115	111 114	eqtrd	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) = (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) {vol}^{} (ran F)$
116	102	ffnd	$⊢ (φ \land 0 < {vol}^{*} (ran F)) \to seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) Fn ℕ$
117		fnfvelrn	$⊢ (seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) Fn ℕ \land ⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1 \in ℕ) \to seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) \in ran seq 1 (+ (m \in ℕ ⟼ vol (T (m))))$
118	116 58 117	syl2anc	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) \in ran seq 1 (+ (m \in ℕ ⟼ vol (T (m))))$
119	115 118	eqeltrrd	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) {vol}^{*} (ran F) \in ran seq 1 (+ (m \in ℕ ⟼ vol (T (m))))$
120		supxrub	$⊢ (ran seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) \subseteq ℝ^{} \land (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) {vol}^{} (ran F) \in ran seq 1 (+ (m \in ℕ ⟼ vol (T (m))))) \to (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) {vol}^{} (ran F) \leq sup (ran seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) ℝ^{} <)$
121	105 119 120	syl2anc	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) {vol}^{} (ran F) \leq sup (ran seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) ℝ^{} <)$
122	81	adantr	$⊢ (φ \land 0 < {vol}^{*} (ran F)) \to ⋃_{m \in ℕ} T (m) \in dom vol$
123		mblvol	$⊢ ⋃_{m \in ℕ} T (m) \in dom vol \to vol (⋃_{m \in ℕ} T (m)) = {vol}^{*} (⋃_{m \in ℕ} T (m))$
124	122 123	syl	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to vol (⋃_{m \in ℕ} T (m)) = {vol}^{} (⋃_{m \in ℕ} T (m))$
125	78 97	jca	$⊢ (φ \land m \in ℕ) \to (T (m) \in dom vol \land vol (T (m)) \in ℝ)$
126	125	ralrimiva	$⊢ φ \to \forall m \in ℕ (T (m) \in dom vol \land vol (T (m)) \in ℝ)$
127	1 2 3 4 5 6 7	vitalilem3	$⊢ φ \to \underset{m \in ℕ}{Disj} T (m)$
128	127	adantr	$⊢ (φ \land 0 < {vol}^{*} (ran F)) \to \underset{m \in ℕ}{Disj} T (m)$
129		eqid	$⊢ seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) = seq 1 (+ (m \in ℕ ⟼ vol (T (m))))$
130	129 99	voliun	$⊢ (\forall m \in ℕ (T (m) \in dom vol \land vol (T (m)) \in ℝ) \land \underset{m \in ℕ}{Disj} T (m)) \to vol (⋃_{m \in ℕ} T (m)) = sup (ran seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) ℝ^{*} <)$
131	126 128 130	syl2an2r	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to vol (⋃_{m \in ℕ} T (m)) = sup (ran seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) ℝ^{} <)$
132	124 131	eqtr3d	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to {vol}^{} (⋃_{m \in ℕ} T (m)) = sup (ran seq 1 (+ (m \in ℕ ⟼ vol (T (m)))) ℝ^{*} <)$
133	121 132	breqtrrd	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to (⌊\frac{3}{{vol}^{} (ran F)}⌋ + 1) {vol}^{} (ran F) \leq {vol}^{} (⋃_{m \in ℕ} T (m))$
134	36 61 85 90 133	xrltletrd	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to 3 < {vol}^{} (⋃_{m \in ℕ} T (m))$
135	17	simp3d	$⊢ φ \to ⋃_{m \in ℕ} T (m) \subseteq [- 1, 2]$
136	135	adantr	$⊢ (φ \land 0 < {vol}^{*} (ran F)) \to ⋃_{m \in ℕ} T (m) \subseteq [- 1, 2]$
137		2re	$⊢ 2 \in ℝ$
138		iccssre	$⊢ (- 1 \in ℝ \land 2 \in ℝ) \to [- 1, 2] \subseteq ℝ$
139	22 137 138	mp2an	$⊢ [- 1, 2] \subseteq ℝ$
140		ovolss	$⊢ (⋃_{m \in ℕ} T (m) \subseteq [- 1, 2] \land [- 1, 2] \subseteq ℝ) \to {vol}^{} (⋃_{m \in ℕ} T (m)) \leq {vol}^{} ([- 1, 2])$
141	136 139 140	sylancl	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to {vol}^{} (⋃_{m \in ℕ} T (m)) \leq {vol}^{*} ([- 1, 2])$
142		2cn	$⊢ 2 \in ℂ$
143		ax-1cn	$⊢ 1 \in ℂ$
144	142 143	subnegi	$⊢ 2 - -1 = 2 + 1$
145		neg1lt0	$⊢ - 1 < 0$
146		2pos	$⊢ 0 < 2$
147	22 38 137	lttri	$⊢ (- 1 < 0 \land 0 < 2) \to - 1 < 2$
148	145 146 147	mp2an	$⊢ - 1 < 2$
149	22 137 148	ltleii	$⊢ - 1 \leq 2$
150		ovolicc	$⊢ (- 1 \in ℝ \land 2 \in ℝ \land - 1 \leq 2) \to {vol}^{*} ([- 1, 2]) = 2 - -1$
151	22 137 149 150	mp3an	$⊢ {vol}^{*} ([- 1, 2]) = 2 - -1$
152		df-3	$⊢ 3 = 2 + 1$
153	144 151 152	3eqtr4i	$⊢ {vol}^{*} ([- 1, 2]) = 3$
154	141 153	breqtrdi	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to {vol}^{} (⋃_{m \in ℕ} T (m)) \leq 3$
155		xrlenlt	$⊢ ({vol}^{} (⋃_{m \in ℕ} T (m)) \in ℝ^{} \land 3 \in ℝ^{}) \to ({vol}^{} (⋃_{m \in ℕ} T (m)) \leq 3 \leftrightarrow \neg 3 < {vol}^{*} (⋃_{m \in ℕ} T (m)))$
156	85 35 155	sylancl	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to ({vol}^{} (⋃_{m \in ℕ} T (m)) \leq 3 \leftrightarrow \neg 3 < {vol}^{*} (⋃_{m \in ℕ} T (m)))$
157	154 156	mpbid	$⊢ (φ \land 0 < {vol}^{} (ran F)) \to \neg 3 < {vol}^{} (⋃_{m \in ℕ} T (m))$
158	134 157	pm2.65da	$⊢ φ \to \neg 0 < {vol}^{*} (ran F)$
159		ovolge0	$⊢ ran F \subseteq ℝ \to 0 \leq {vol}^{*} (ran F)$
160	20 159	syl	$⊢ φ \to 0 \leq {vol}^{*} (ran F)$
161		0xr	$⊢ 0 \in ℝ^{*}$
162		ovolcl	$⊢ ran F \subseteq ℝ \to {vol}^{} (ran F) \in ℝ^{}$
163	20 162	syl	$⊢ φ \to {vol}^{} (ran F) \in ℝ^{}$
164		xrleloe	$⊢ (0 \in ℝ^{} \land {vol}^{} (ran F) \in ℝ^{}) \to (0 \leq {vol}^{} (ran F) \leftrightarrow (0 < {vol}^{} (ran F) \lor 0 = {vol}^{} (ran F)))$
165	161 163 164	sylancr	$⊢ φ \to (0 \leq {vol}^{} (ran F) \leftrightarrow (0 < {vol}^{} (ran F) \lor 0 = {vol}^{*} (ran F)))$
166	160 165	mpbid	$⊢ φ \to (0 < {vol}^{} (ran F) \lor 0 = {vol}^{} (ran F))$
167	166	ord	$⊢ φ \to (\neg 0 < {vol}^{} (ran F) \to 0 = {vol}^{} (ran F))$
168	158 167	mpd	$⊢ φ \to 0 = {vol}^{*} (ran F)$
169	168	adantr	$⊢ (φ \land m \in ℕ) \to 0 = {vol}^{*} (ran F)$
170	33 169	eqtr4d	$⊢ (φ \land m \in ℕ) \to {vol}^{*} (T (m)) = 0$

Metamath Proof Explorer

Theorem vitalilem4

Proof