Step | Hyp | Ref
| Expression |
1 | | 0lt1 11243 |
. . . 4
⊢ 0 <
1 |
2 | | 0re 10724 |
. . . . . 6
⊢ 0 ∈
ℝ |
3 | | 1re 10722 |
. . . . . 6
⊢ 1 ∈
ℝ |
4 | | 0le1 11244 |
. . . . . 6
⊢ 0 ≤
1 |
5 | | ovolicc 24278 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ≤ 1) →
(vol*‘(0[,]1)) = (1 − 0)) |
6 | 2, 3, 4, 5 | mp3an 1462 |
. . . . 5
⊢
(vol*‘(0[,]1)) = (1 − 0) |
7 | | 1m0e1 11840 |
. . . . 5
⊢ (1
− 0) = 1 |
8 | 6, 7 | eqtri 2762 |
. . . 4
⊢
(vol*‘(0[,]1)) = 1 |
9 | 1, 8 | breqtrri 5058 |
. . 3
⊢ 0 <
(vol*‘(0[,]1)) |
10 | 8, 3 | eqeltri 2830 |
. . . 4
⊢
(vol*‘(0[,]1)) ∈ ℝ |
11 | 2, 10 | ltnlei 10842 |
. . 3
⊢ (0 <
(vol*‘(0[,]1)) ↔ ¬ (vol*‘(0[,]1)) ≤ 0) |
12 | 9, 11 | mpbi 233 |
. 2
⊢ ¬
(vol*‘(0[,]1)) ≤ 0 |
13 | | vitali.1 |
. . . . . 6
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)} |
14 | | vitali.2 |
. . . . . 6
⊢ 𝑆 = ((0[,]1) / ∼
) |
15 | | vitali.3 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn 𝑆) |
16 | | vitali.4 |
. . . . . 6
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧)) |
17 | | vitali.5 |
. . . . . 6
⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) |
18 | | vitali.6 |
. . . . . 6
⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹}) |
19 | | vitali.7 |
. . . . . 6
⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ
∖ dom vol)) |
20 | 13, 14, 15, 16, 17, 18, 19 | vitalilem2 24364 |
. . . . 5
⊢ (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆
∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪
𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2))) |
21 | 20 | simp2d 1144 |
. . . 4
⊢ (𝜑 → (0[,]1) ⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) |
22 | 13 | vitalilem1 24363 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∼ Er
(0[,]1) |
23 | | erdm 8333 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ( ∼ Er
(0[,]1) → dom ∼ =
(0[,]1)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ dom ∼ =
(0[,]1) |
25 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
26 | 25, 14 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((0[,]1) / ∼ )) |
27 | | elqsn0 8400 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((dom
∼
= (0[,]1) ∧ 𝑧 ∈
((0[,]1) / ∼ )) → 𝑧 ≠ ∅) |
28 | 24, 26, 27 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ≠ ∅) |
29 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∼ Er
(0[,]1)) |
30 | 29 | qsss 8392 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((0[,]1) / ∼ )
⊆ 𝒫 (0[,]1)) |
31 | 14, 30 | eqsstrid 3926 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑆 ⊆ 𝒫 (0[,]1)) |
32 | 31 | sselda 3878 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝒫 (0[,]1)) |
33 | 32 | elpwid 4500 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ⊆ (0[,]1)) |
34 | 33 | sseld 3877 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑧) ∈ 𝑧 → (𝐹‘𝑧) ∈ (0[,]1))) |
35 | 28, 34 | embantd 59 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) → (𝐹‘𝑧) ∈ (0[,]1))) |
36 | 35 | ralimdva 3092 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1))) |
37 | 16, 36 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1)) |
38 | | ffnfv 6895 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝑆⟶(0[,]1) ↔ (𝐹 Fn 𝑆 ∧ ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1))) |
39 | 15, 37, 38 | sylanbrc 586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝑆⟶(0[,]1)) |
40 | 39 | frnd 6513 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ran 𝐹 ⊆ (0[,]1)) |
41 | | unitssre 12976 |
. . . . . . . . . . . . . . . 16
⊢ (0[,]1)
⊆ ℝ |
42 | 40, 41 | sstrdi 3890 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
43 | | reex 10709 |
. . . . . . . . . . . . . . . 16
⊢ ℝ
∈ V |
44 | 43 | elpw2 5214 |
. . . . . . . . . . . . . . 15
⊢ (ran
𝐹 ∈ 𝒫 ℝ
↔ ran 𝐹 ⊆
ℝ) |
45 | 42, 44 | sylibr 237 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐹 ∈ 𝒫 ℝ) |
46 | 45 | anim1i 618 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ ran 𝐹 ∈ dom vol) → (ran 𝐹 ∈ 𝒫 ℝ ∧
¬ ran 𝐹 ∈ dom
vol)) |
47 | | eldif 3854 |
. . . . . . . . . . . . 13
⊢ (ran
𝐹 ∈ (𝒫 ℝ
∖ dom vol) ↔ (ran 𝐹 ∈ 𝒫 ℝ ∧ ¬ ran
𝐹 ∈ dom
vol)) |
48 | 46, 47 | sylibr 237 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ ran 𝐹 ∈ dom vol) → ran 𝐹 ∈ (𝒫 ℝ
∖ dom vol)) |
49 | 48 | ex 416 |
. . . . . . . . . . 11
⊢ (𝜑 → (¬ ran 𝐹 ∈ dom vol → ran 𝐹 ∈ (𝒫 ℝ
∖ dom vol))) |
50 | 19, 49 | mt3d 150 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝐹 ∈ dom vol) |
51 | | f1of 6621 |
. . . . . . . . . . . . 13
⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ⟶(ℚ ∩
(-1[,]1))) |
52 | 17, 51 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:ℕ⟶(ℚ ∩
(-1[,]1))) |
53 | | inss1 4120 |
. . . . . . . . . . . . 13
⊢ (ℚ
∩ (-1[,]1)) ⊆ ℚ |
54 | | qssre 12444 |
. . . . . . . . . . . . 13
⊢ ℚ
⊆ ℝ |
55 | 53, 54 | sstri 3887 |
. . . . . . . . . . . 12
⊢ (ℚ
∩ (-1[,]1)) ⊆ ℝ |
56 | | fss 6522 |
. . . . . . . . . . . 12
⊢ ((𝐺:ℕ⟶(ℚ ∩
(-1[,]1)) ∧ (ℚ ∩ (-1[,]1)) ⊆ ℝ) → 𝐺:ℕ⟶ℝ) |
57 | 52, 55, 56 | sylancl 589 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:ℕ⟶ℝ) |
58 | 57 | ffvelrnda 6864 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℝ) |
59 | | shftmbl 24293 |
. . . . . . . . . 10
⊢ ((ran
𝐹 ∈ dom vol ∧
(𝐺‘𝑛) ∈ ℝ) → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} ∈ dom vol) |
60 | 50, 58, 59 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} ∈ dom vol) |
61 | 60, 18 | fmptd 6891 |
. . . . . . . 8
⊢ (𝜑 → 𝑇:ℕ⟶dom vol) |
62 | 61 | ffvelrnda 6864 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑇‘𝑚) ∈ dom vol) |
63 | 62 | ralrimiva 3097 |
. . . . . 6
⊢ (𝜑 → ∀𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol) |
64 | | iunmbl 24308 |
. . . . . 6
⊢
(∀𝑚 ∈
ℕ (𝑇‘𝑚) ∈ dom vol → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol) |
65 | 63, 64 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol) |
66 | | mblss 24286 |
. . . . 5
⊢ (∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ) |
67 | 65, 66 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ) |
68 | | ovolss 24240 |
. . . 4
⊢ (((0[,]1)
⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪
𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ) →
(vol*‘(0[,]1)) ≤ (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚))) |
69 | 21, 67, 68 | syl2anc 587 |
. . 3
⊢ (𝜑 → (vol*‘(0[,]1)) ≤
(vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚))) |
70 | | eqid 2739 |
. . . . . 6
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) = seq1( + , (𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) |
71 | | eqid 2739 |
. . . . . 6
⊢ (𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚))) = (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚))) |
72 | | mblss 24286 |
. . . . . . 7
⊢ ((𝑇‘𝑚) ∈ dom vol → (𝑇‘𝑚) ⊆ ℝ) |
73 | 62, 72 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑇‘𝑚) ⊆ ℝ) |
74 | 13, 14, 15, 16, 17, 18, 19 | vitalilem4 24366 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol*‘(𝑇‘𝑚)) = 0) |
75 | 74, 2 | eqeltrdi 2842 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol*‘(𝑇‘𝑚)) ∈ ℝ) |
76 | 74 | mpteq2dva 5126 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚))) = (𝑚 ∈ ℕ ↦ 0)) |
77 | | fconstmpt 5586 |
. . . . . . . . . . 11
⊢ (ℕ
× {0}) = (𝑚 ∈
ℕ ↦ 0) |
78 | | nnuz 12366 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
79 | 78 | xpeq1i 5552 |
. . . . . . . . . . 11
⊢ (ℕ
× {0}) = ((ℤ≥‘1) × {0}) |
80 | 77, 79 | eqtr3i 2764 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ ↦ 0) =
((ℤ≥‘1) × {0}) |
81 | 76, 80 | eqtrdi 2790 |
. . . . . . . . 9
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚))) = ((ℤ≥‘1)
× {0})) |
82 | 81 | seqeq3d 13471 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) = seq1( + ,
((ℤ≥‘1) × {0}))) |
83 | | 1z 12096 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
84 | | serclim0 15027 |
. . . . . . . . 9
⊢ (1 ∈
ℤ → seq1( + , ((ℤ≥‘1) × {0}))
⇝ 0) |
85 | 83, 84 | ax-mp 5 |
. . . . . . . 8
⊢ seq1( + ,
((ℤ≥‘1) × {0})) ⇝ 0 |
86 | 82, 85 | eqbrtrdi 5070 |
. . . . . . 7
⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) ⇝ 0) |
87 | | seqex 13465 |
. . . . . . . 8
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) ∈ V |
88 | | c0ex 10716 |
. . . . . . . 8
⊢ 0 ∈
V |
89 | 87, 88 | breldm 5752 |
. . . . . . 7
⊢ (seq1( +
, (𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) ⇝ 0 → seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) ∈ dom ⇝
) |
90 | 86, 89 | syl 17 |
. . . . . 6
⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) ∈ dom ⇝
) |
91 | 70, 71, 73, 75, 90 | ovoliun2 24261 |
. . . . 5
⊢ (𝜑 → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ Σ𝑚 ∈ ℕ (vol*‘(𝑇‘𝑚))) |
92 | 74 | sumeq2dv 15156 |
. . . . . 6
⊢ (𝜑 → Σ𝑚 ∈ ℕ (vol*‘(𝑇‘𝑚)) = Σ𝑚 ∈ ℕ 0) |
93 | 78 | eqimssi 3936 |
. . . . . . . 8
⊢ ℕ
⊆ (ℤ≥‘1) |
94 | 93 | orci 864 |
. . . . . . 7
⊢ (ℕ
⊆ (ℤ≥‘1) ∨ ℕ ∈
Fin) |
95 | | sumz 15175 |
. . . . . . 7
⊢ ((ℕ
⊆ (ℤ≥‘1) ∨ ℕ ∈ Fin) →
Σ𝑚 ∈ ℕ 0 =
0) |
96 | 94, 95 | ax-mp 5 |
. . . . . 6
⊢
Σ𝑚 ∈
ℕ 0 = 0 |
97 | 92, 96 | eqtrdi 2790 |
. . . . 5
⊢ (𝜑 → Σ𝑚 ∈ ℕ (vol*‘(𝑇‘𝑚)) = 0) |
98 | 91, 97 | breqtrd 5057 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ 0) |
99 | | ovolge0 24236 |
. . . . 5
⊢ (∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ → 0 ≤
(vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚))) |
100 | 67, 99 | syl 17 |
. . . 4
⊢ (𝜑 → 0 ≤
(vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚))) |
101 | | ovolcl 24233 |
. . . . . 6
⊢ (∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ∈
ℝ*) |
102 | 67, 101 | syl 17 |
. . . . 5
⊢ (𝜑 → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ∈
ℝ*) |
103 | | 0xr 10769 |
. . . . 5
⊢ 0 ∈
ℝ* |
104 | | xrletri3 12633 |
. . . . 5
⊢
(((vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ∈ ℝ* ∧ 0 ∈
ℝ*) → ((vol*‘∪
𝑚 ∈ ℕ (𝑇‘𝑚)) = 0 ↔ ((vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚))))) |
105 | 102, 103,
104 | sylancl 589 |
. . . 4
⊢ (𝜑 → ((vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) = 0 ↔ ((vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚))))) |
106 | 98, 100, 105 | mpbir2and 713 |
. . 3
⊢ (𝜑 → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) = 0) |
107 | 69, 106 | breqtrd 5057 |
. 2
⊢ (𝜑 → (vol*‘(0[,]1)) ≤
0) |
108 | 12, 107 | mto 200 |
1
⊢ ¬
𝜑 |