Step | Hyp | Ref
| Expression |
1 | | 0lt1 10429 |
. . . 4
⊢ 0 <
1 |
2 | | 0re 9919 |
. . . . . 6
⊢ 0 ∈
ℝ |
3 | | 1re 9918 |
. . . . . 6
⊢ 1 ∈
ℝ |
4 | | 0le1 10430 |
. . . . . 6
⊢ 0 ≤
1 |
5 | | ovolicc 23098 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ≤ 1) →
(vol*‘(0[,]1)) = (1 − 0)) |
6 | 2, 3, 4, 5 | mp3an 1416 |
. . . . 5
⊢
(vol*‘(0[,]1)) = (1 − 0) |
7 | | 1m0e1 11008 |
. . . . 5
⊢ (1
− 0) = 1 |
8 | 6, 7 | eqtri 2632 |
. . . 4
⊢
(vol*‘(0[,]1)) = 1 |
9 | 1, 8 | breqtrri 4610 |
. . 3
⊢ 0 <
(vol*‘(0[,]1)) |
10 | 8, 3 | eqeltri 2684 |
. . . 4
⊢
(vol*‘(0[,]1)) ∈ ℝ |
11 | 2, 10 | ltnlei 10037 |
. . 3
⊢ (0 <
(vol*‘(0[,]1)) ↔ ¬ (vol*‘(0[,]1)) ≤ 0) |
12 | 9, 11 | mpbi 219 |
. 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 23184 |
. . . . 5
⊢ (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆
∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪
𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2))) |
21 | 20 | simp2d 1067 |
. . . 4
⊢ (𝜑 → (0[,]1) ⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) |
22 | 13 | vitalilem1 23182 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∼ Er
(0[,]1) |
23 | | erdm 7639 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ( ∼ Er
(0[,]1) → dom ∼ =
(0[,]1)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ dom ∼ =
(0[,]1) |
25 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
26 | 25, 14 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((0[,]1) / ∼ )) |
27 | | elqsn0 7703 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((dom
∼
= (0[,]1) ∧ 𝑧 ∈
((0[,]1) / ∼ )) → 𝑧 ≠ ∅) |
28 | 24, 26, 27 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ≠ ∅) |
29 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ∼ Er
(0[,]1)) |
30 | 29 | qsss 7695 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((0[,]1) / ∼ )
⊆ 𝒫 (0[,]1)) |
31 | 14, 30 | syl5eqss 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑆 ⊆ 𝒫 (0[,]1)) |
32 | 31 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝒫 (0[,]1)) |
33 | 32 | elpwid 4118 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ⊆ (0[,]1)) |
34 | 33 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑧) ∈ 𝑧 → (𝐹‘𝑧) ∈ (0[,]1))) |
35 | 28, 34 | embantd 57 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) → (𝐹‘𝑧) ∈ (0[,]1))) |
36 | 35 | ralimdva 2945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1))) |
37 | 16, 36 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1)) |
38 | | ffnfv 6295 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝑆⟶(0[,]1) ↔ (𝐹 Fn 𝑆 ∧ ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1))) |
39 | 15, 37, 38 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:𝑆⟶(0[,]1)) |
40 | | frn 5966 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝑆⟶(0[,]1) → ran 𝐹 ⊆ (0[,]1)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran 𝐹 ⊆ (0[,]1)) |
42 | | unitssre 12190 |
. . . . . . . . . . . . . . . . 17
⊢ (0[,]1)
⊆ ℝ |
43 | 41, 42 | syl6ss 3580 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
44 | | reex 9906 |
. . . . . . . . . . . . . . . . 17
⊢ ℝ
∈ V |
45 | 44 | elpw2 4755 |
. . . . . . . . . . . . . . . 16
⊢ (ran
𝐹 ∈ 𝒫 ℝ
↔ ran 𝐹 ⊆
ℝ) |
46 | 43, 45 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐹 ∈ 𝒫 ℝ) |
47 | 46 | anim1i 590 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ ran 𝐹 ∈ dom vol) → (ran 𝐹 ∈ 𝒫 ℝ ∧
¬ ran 𝐹 ∈ dom
vol)) |
48 | | eldif 3550 |
. . . . . . . . . . . . . 14
⊢ (ran
𝐹 ∈ (𝒫 ℝ
∖ dom vol) ↔ (ran 𝐹 ∈ 𝒫 ℝ ∧ ¬ ran
𝐹 ∈ dom
vol)) |
49 | 47, 48 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ ran 𝐹 ∈ dom vol) → ran 𝐹 ∈ (𝒫 ℝ
∖ dom vol)) |
50 | 49 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝜑 → (¬ ran 𝐹 ∈ dom vol → ran 𝐹 ∈ (𝒫 ℝ
∖ dom vol))) |
51 | 19, 50 | mt3d 139 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐹 ∈ dom vol) |
52 | 51 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran 𝐹 ∈ dom vol) |
53 | | f1of 6050 |
. . . . . . . . . . . . 13
⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ⟶(ℚ ∩
(-1[,]1))) |
54 | 17, 53 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:ℕ⟶(ℚ ∩
(-1[,]1))) |
55 | | inss1 3795 |
. . . . . . . . . . . . 13
⊢ (ℚ
∩ (-1[,]1)) ⊆ ℚ |
56 | | qssre 11674 |
. . . . . . . . . . . . 13
⊢ ℚ
⊆ ℝ |
57 | 55, 56 | sstri 3577 |
. . . . . . . . . . . 12
⊢ (ℚ
∩ (-1[,]1)) ⊆ ℝ |
58 | | fss 5969 |
. . . . . . . . . . . 12
⊢ ((𝐺:ℕ⟶(ℚ ∩
(-1[,]1)) ∧ (ℚ ∩ (-1[,]1)) ⊆ ℝ) → 𝐺:ℕ⟶ℝ) |
59 | 54, 57, 58 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:ℕ⟶ℝ) |
60 | 59 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℝ) |
61 | | shftmbl 23113 |
. . . . . . . . . 10
⊢ ((ran
𝐹 ∈ dom vol ∧
(𝐺‘𝑛) ∈ ℝ) → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} ∈ dom vol) |
62 | 52, 60, 61 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} ∈ dom vol) |
63 | 62, 18 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → 𝑇:ℕ⟶dom vol) |
64 | 63 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑇‘𝑚) ∈ dom vol) |
65 | 64 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol) |
66 | | iunmbl 23128 |
. . . . . 6
⊢
(∀𝑚 ∈
ℕ (𝑇‘𝑚) ∈ dom vol → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol) |
67 | 65, 66 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol) |
68 | | mblss 23106 |
. . . . 5
⊢ (∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ) |
69 | 67, 68 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ) |
70 | | ovolss 23060 |
. . . 4
⊢ (((0[,]1)
⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪
𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ) →
(vol*‘(0[,]1)) ≤ (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚))) |
71 | 21, 69, 70 | syl2anc 691 |
. . 3
⊢ (𝜑 → (vol*‘(0[,]1)) ≤
(vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚))) |
72 | | eqid 2610 |
. . . . . 6
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) = seq1( + , (𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) |
73 | | eqid 2610 |
. . . . . 6
⊢ (𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚))) = (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚))) |
74 | | mblss 23106 |
. . . . . . 7
⊢ ((𝑇‘𝑚) ∈ dom vol → (𝑇‘𝑚) ⊆ ℝ) |
75 | 64, 74 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑇‘𝑚) ⊆ ℝ) |
76 | 13, 14, 15, 16, 17, 18, 19 | vitalilem4 23186 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol*‘(𝑇‘𝑚)) = 0) |
77 | 76, 2 | syl6eqel 2696 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol*‘(𝑇‘𝑚)) ∈ ℝ) |
78 | 76 | mpteq2dva 4672 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚))) = (𝑚 ∈ ℕ ↦ 0)) |
79 | | fconstmpt 5085 |
. . . . . . . . . . 11
⊢ (ℕ
× {0}) = (𝑚 ∈
ℕ ↦ 0) |
80 | | nnuz 11599 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
81 | 80 | xpeq1i 5059 |
. . . . . . . . . . 11
⊢ (ℕ
× {0}) = ((ℤ≥‘1) × {0}) |
82 | 79, 81 | eqtr3i 2634 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ ↦ 0) =
((ℤ≥‘1) × {0}) |
83 | 78, 82 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚))) = ((ℤ≥‘1)
× {0})) |
84 | 83 | seqeq3d 12671 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) = seq1( + ,
((ℤ≥‘1) × {0}))) |
85 | | 1z 11284 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
86 | | serclim0 14156 |
. . . . . . . . 9
⊢ (1 ∈
ℤ → seq1( + , ((ℤ≥‘1) × {0}))
⇝ 0) |
87 | 85, 86 | ax-mp 5 |
. . . . . . . 8
⊢ seq1( + ,
((ℤ≥‘1) × {0})) ⇝ 0 |
88 | 84, 87 | syl6eqbr 4622 |
. . . . . . 7
⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) ⇝ 0) |
89 | | seqex 12665 |
. . . . . . . 8
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) ∈ V |
90 | | c0ex 9913 |
. . . . . . . 8
⊢ 0 ∈
V |
91 | 89, 90 | breldm 5251 |
. . . . . . 7
⊢ (seq1( +
, (𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) ⇝ 0 → seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) ∈ dom ⇝
) |
92 | 88, 91 | syl 17 |
. . . . . 6
⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦
(vol*‘(𝑇‘𝑚)))) ∈ dom ⇝
) |
93 | 72, 73, 75, 77, 92 | ovoliun2 23081 |
. . . . 5
⊢ (𝜑 → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ Σ𝑚 ∈ ℕ (vol*‘(𝑇‘𝑚))) |
94 | 76 | sumeq2dv 14281 |
. . . . . 6
⊢ (𝜑 → Σ𝑚 ∈ ℕ (vol*‘(𝑇‘𝑚)) = Σ𝑚 ∈ ℕ 0) |
95 | 80 | eqimssi 3622 |
. . . . . . . 8
⊢ ℕ
⊆ (ℤ≥‘1) |
96 | 95 | orci 404 |
. . . . . . 7
⊢ (ℕ
⊆ (ℤ≥‘1) ∨ ℕ ∈
Fin) |
97 | | sumz 14300 |
. . . . . . 7
⊢ ((ℕ
⊆ (ℤ≥‘1) ∨ ℕ ∈ Fin) →
Σ𝑚 ∈ ℕ 0 =
0) |
98 | 96, 97 | ax-mp 5 |
. . . . . 6
⊢
Σ𝑚 ∈
ℕ 0 = 0 |
99 | 94, 98 | syl6eq 2660 |
. . . . 5
⊢ (𝜑 → Σ𝑚 ∈ ℕ (vol*‘(𝑇‘𝑚)) = 0) |
100 | 93, 99 | breqtrd 4609 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ 0) |
101 | | ovolge0 23056 |
. . . . 5
⊢ (∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ → 0 ≤
(vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚))) |
102 | 69, 101 | syl 17 |
. . . 4
⊢ (𝜑 → 0 ≤
(vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚))) |
103 | | ovolcl 23053 |
. . . . . 6
⊢ (∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ∈
ℝ*) |
104 | 69, 103 | syl 17 |
. . . . 5
⊢ (𝜑 → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ∈
ℝ*) |
105 | | 0xr 9965 |
. . . . 5
⊢ 0 ∈
ℝ* |
106 | | xrletri3 11861 |
. . . . 5
⊢
(((vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ∈ ℝ* ∧ 0 ∈
ℝ*) → ((vol*‘∪
𝑚 ∈ ℕ (𝑇‘𝑚)) = 0 ↔ ((vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚))))) |
107 | 104, 105,
106 | sylancl 693 |
. . . 4
⊢ (𝜑 → ((vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) = 0 ↔ ((vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚))))) |
108 | 100, 102,
107 | mpbir2and 959 |
. . 3
⊢ (𝜑 → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) = 0) |
109 | 71, 108 | breqtrd 4609 |
. 2
⊢ (𝜑 → (vol*‘(0[,]1)) ≤
0) |
110 | 12, 109 | mto 187 |
1
⊢ ¬
𝜑 |