Step | Hyp | Ref
| Expression |
1 | | r19.26 3111 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ↔ (∀𝑛
∈ ℕ 𝐴 ∈ dom
vol ∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ)) |
2 | | eqid 2733 |
. . . . . 6
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘𝐴))) = seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘𝐴))) |
3 | | eqid 2733 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦
(vol‘𝐴)) = (𝑛 ∈ ℕ ↦
(vol‘𝐴)) |
4 | 2, 3 | voliun 24941 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, <
)) |
5 | 1, 4 | sylanbr 583 |
. . . 4
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, <
)) |
6 | 5 | an32s 651 |
. . 3
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦
(vol‘𝐴))),
ℝ*, < )) |
7 | | nfra1 3266 |
. . . . . . 7
⊢
Ⅎ𝑛∀𝑛 ∈ ℕ 𝐴 ∈ dom vol |
8 | | nfra1 3266 |
. . . . . . 7
⊢
Ⅎ𝑛∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ |
9 | 7, 8 | nfan 1903 |
. . . . . 6
⊢
Ⅎ𝑛(∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈
ℝ) |
10 | | simpr 486 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑛 ∈ ℕ)
→ 𝑛 ∈
ℕ) |
11 | | rspa 3230 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑛 ∈ ℕ)
→ 𝐴 ∈ dom
vol) |
12 | | volf 24916 |
. . . . . . . . . . . 12
⊢ vol:dom
vol⟶(0[,]+∞) |
13 | 12 | ffvelcdmi 7038 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
(0[,]+∞)) |
14 | 11, 13 | syl 17 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑛 ∈ ℕ)
→ (vol‘𝐴) ∈
(0[,]+∞)) |
15 | 3 | fvmpt2 6963 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧
(vol‘𝐴) ∈
(0[,]+∞)) → ((𝑛
∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴)) |
16 | 10, 14, 15 | syl2anc 585 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑛 ∈ ℕ)
→ ((𝑛 ∈ ℕ
↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴)) |
17 | 16 | adantlr 714 |
. . . . . . . 8
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → ((𝑛
∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴)) |
18 | 17 | ex 414 |
. . . . . . 7
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → (𝑛
∈ ℕ → ((𝑛
∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴))) |
19 | 9, 18 | ralrimi 3239 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → ∀𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴)) |
20 | 9, 19 | esumeq2d 32700 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → Σ*𝑛 ∈ ℕ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = Σ*𝑛 ∈ ℕ(vol‘𝐴)) |
21 | | simpr 486 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) |
22 | 21 | r19.21bi 3233 |
. . . . . . . 8
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → (vol‘𝐴) ∈ ℝ) |
23 | 14 | adantlr 714 |
. . . . . . . . 9
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → (vol‘𝐴) ∈ (0[,]+∞)) |
24 | | 0xr 11210 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
25 | | pnfxr 11217 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
26 | | elicc1 13317 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
((vol‘𝐴) ∈
(0[,]+∞) ↔ ((vol‘𝐴) ∈ ℝ* ∧ 0 ≤
(vol‘𝐴) ∧
(vol‘𝐴) ≤
+∞))) |
27 | 24, 25, 26 | mp2an 691 |
. . . . . . . . . 10
⊢
((vol‘𝐴)
∈ (0[,]+∞) ↔ ((vol‘𝐴) ∈ ℝ* ∧ 0 ≤
(vol‘𝐴) ∧
(vol‘𝐴) ≤
+∞)) |
28 | 27 | simp2bi 1147 |
. . . . . . . . 9
⊢
((vol‘𝐴)
∈ (0[,]+∞) → 0 ≤ (vol‘𝐴)) |
29 | 23, 28 | syl 17 |
. . . . . . . 8
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → 0 ≤ (vol‘𝐴)) |
30 | | ltpnf 13049 |
. . . . . . . . 9
⊢
((vol‘𝐴)
∈ ℝ → (vol‘𝐴) < +∞) |
31 | 22, 30 | syl 17 |
. . . . . . . 8
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → (vol‘𝐴) < +∞) |
32 | | 0re 11165 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
33 | | elico2 13337 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) →
((vol‘𝐴) ∈
(0[,)+∞) ↔ ((vol‘𝐴) ∈ ℝ ∧ 0 ≤
(vol‘𝐴) ∧
(vol‘𝐴) <
+∞))) |
34 | 32, 25, 33 | mp2an 691 |
. . . . . . . 8
⊢
((vol‘𝐴)
∈ (0[,)+∞) ↔ ((vol‘𝐴) ∈ ℝ ∧ 0 ≤
(vol‘𝐴) ∧
(vol‘𝐴) <
+∞)) |
35 | 22, 29, 31, 34 | syl3anbrc 1344 |
. . . . . . 7
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → (vol‘𝐴) ∈ (0[,)+∞)) |
36 | 9, 35, 3 | fmptdf 7069 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → (𝑛
∈ ℕ ↦ (vol‘𝐴)):ℕ⟶(0[,)+∞)) |
37 | | nfmpt1 5217 |
. . . . . . 7
⊢
Ⅎ𝑛(𝑛 ∈ ℕ ↦ (vol‘𝐴)) |
38 | 37 | esumfsupre 32734 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ↦
(vol‘𝐴)):ℕ⟶(0[,)+∞) →
Σ*𝑛 ∈
ℕ((𝑛 ∈ ℕ
↦ (vol‘𝐴))‘𝑛) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, <
)) |
39 | 36, 38 | syl 17 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → Σ*𝑛 ∈ ℕ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, <
)) |
40 | 20, 39 | eqtr3d 2775 |
. . . 4
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → Σ*𝑛 ∈ ℕ(vol‘𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, <
)) |
41 | 40 | adantlr 714 |
. . 3
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ) → Σ*𝑛 ∈ ℕ(vol‘𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, <
)) |
42 | 6, 41 | eqtr4d 2776 |
. 2
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴)) |
43 | | simpr 486 |
. . . . . . . 8
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ∃𝑛 ∈
ℕ (vol‘𝐴) =
+∞) |
44 | | nfv 1918 |
. . . . . . . . 9
⊢
Ⅎ𝑘(vol‘𝐴) = +∞ |
45 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛vol |
46 | | nfcsb1v 3884 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐴 |
47 | 45, 46 | nffv 6856 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐴) |
48 | 47 | nfeq1 2919 |
. . . . . . . . 9
⊢
Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ |
49 | | csbeq1a 3873 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → 𝐴 = ⦋𝑘 / 𝑛⦌𝐴) |
50 | 49 | fveqeq2d 6854 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((vol‘𝐴) = +∞ ↔
(vol‘⦋𝑘
/ 𝑛⦌𝐴) = +∞)) |
51 | 44, 48, 50 | cbvrexw 3289 |
. . . . . . . 8
⊢
(∃𝑛 ∈
ℕ (vol‘𝐴) =
+∞ ↔ ∃𝑘
∈ ℕ (vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞) |
52 | 43, 51 | sylib 217 |
. . . . . . 7
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ∃𝑘 ∈
ℕ (vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞) |
53 | 46 | nfel1 2920 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol |
54 | 49 | eleq1d 2819 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (𝐴 ∈ dom vol ↔ ⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol)) |
55 | 53, 54 | rspc 3571 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ →
(∀𝑛 ∈ ℕ
𝐴 ∈ dom vol →
⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol)) |
56 | 55 | impcom 409 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ⦋𝑘 /
𝑛⦌𝐴 ∈ dom
vol) |
57 | | iunmbl 24940 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol) |
58 | 57 | adantr 482 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol) |
59 | | nfcv 2904 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛ℕ |
60 | | nfcv 2904 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛𝑘 |
61 | 59, 60, 46, 49 | ssiun2sf 31531 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ →
⦋𝑘 / 𝑛⦌𝐴 ⊆ ∪
𝑛 ∈ ℕ 𝐴) |
62 | 61 | adantl 483 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ⦋𝑘 /
𝑛⦌𝐴 ⊆ ∪ 𝑛 ∈ ℕ 𝐴) |
63 | | volss 24920 |
. . . . . . . . . . 11
⊢
((⦋𝑘 /
𝑛⦌𝐴 ∈ dom vol ∧ ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ⦋𝑘 / 𝑛⦌𝐴 ⊆ ∪
𝑛 ∈ ℕ 𝐴) →
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
64 | 56, 58, 62, 63 | syl3anc 1372 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ (vol‘⦋𝑘 / 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
65 | 64 | adantlr 714 |
. . . . . . . . 9
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧ 𝑘 ∈ ℕ) →
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
66 | 65 | adantlr 714 |
. . . . . . . 8
⊢
((((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
∧ 𝑘 ∈ ℕ)
→ (vol‘⦋𝑘 / 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
67 | 66 | ralrimiva 3140 |
. . . . . . 7
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ∀𝑘 ∈
ℕ (vol‘⦋𝑘 / 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
68 | | r19.29r 3116 |
. . . . . . 7
⊢
((∃𝑘 ∈
ℕ (vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ ∧ ∀𝑘 ∈ ℕ
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) → ∃𝑘 ∈ ℕ
((vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴))) |
69 | 52, 67, 68 | syl2anc 585 |
. . . . . 6
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ∃𝑘 ∈
ℕ ((vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴))) |
70 | | breq1 5112 |
. . . . . . . 8
⊢
((vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ →
((vol‘⦋𝑘 / 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ +∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴))) |
71 | 70 | biimpa 478 |
. . . . . . 7
⊢
(((vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) → +∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
72 | 71 | reximi 3084 |
. . . . . 6
⊢
(∃𝑘 ∈
ℕ ((vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) → ∃𝑘 ∈ ℕ +∞ ≤
(vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
73 | 69, 72 | syl 17 |
. . . . 5
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ∃𝑘 ∈
ℕ +∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
74 | | 1nn 12172 |
. . . . . 6
⊢ 1 ∈
ℕ |
75 | | ne0i 4298 |
. . . . . 6
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
76 | | r19.9rzv 4461 |
. . . . . 6
⊢ (ℕ
≠ ∅ → (+∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ ∃𝑘 ∈ ℕ +∞ ≤
(vol‘∪ 𝑛 ∈ ℕ 𝐴))) |
77 | 74, 75, 76 | mp2b 10 |
. . . . 5
⊢ (+∞
≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ ∃𝑘 ∈ ℕ +∞ ≤
(vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
78 | 73, 77 | sylibr 233 |
. . . 4
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ +∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
79 | | iccssxr 13356 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
80 | 12 | ffvelcdmi 7038 |
. . . . . . . 8
⊢ (∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → (vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈ (0[,]+∞)) |
81 | 79, 80 | sselid 3946 |
. . . . . . 7
⊢ (∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → (vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
82 | 57, 81 | syl 17 |
. . . . . 6
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
83 | 82 | ad2antrr 725 |
. . . . 5
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
84 | | xgepnf 13093 |
. . . . 5
⊢
((vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈ ℝ* →
(+∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ (vol‘∪ 𝑛 ∈ ℕ 𝐴) = +∞)) |
85 | 83, 84 | syl 17 |
. . . 4
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ (+∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ (vol‘∪ 𝑛 ∈ ℕ 𝐴) = +∞)) |
86 | 78, 85 | mpbid 231 |
. . 3
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ (vol‘∪ 𝑛 ∈ ℕ 𝐴) = +∞) |
87 | | nfdisj1 5088 |
. . . . . 6
⊢
Ⅎ𝑛Disj
𝑛 ∈ ℕ 𝐴 |
88 | 7, 87 | nfan 1903 |
. . . . 5
⊢
Ⅎ𝑛(∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) |
89 | | nfre1 3267 |
. . . . 5
⊢
Ⅎ𝑛∃𝑛 ∈ ℕ (vol‘𝐴) = +∞ |
90 | 88, 89 | nfan 1903 |
. . . 4
⊢
Ⅎ𝑛((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) |
91 | | nnex 12167 |
. . . . 5
⊢ ℕ
∈ V |
92 | 91 | a1i 11 |
. . . 4
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ℕ ∈ V) |
93 | 14 | 3ad2antr3 1191 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ (Disj 𝑛 ∈
ℕ 𝐴 ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞
∧ 𝑛 ∈ ℕ))
→ (vol‘𝐴) ∈
(0[,]+∞)) |
94 | 93 | 3anassrs 1361 |
. . . 4
⊢
((((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
∧ 𝑛 ∈ ℕ)
→ (vol‘𝐴) ∈
(0[,]+∞)) |
95 | 90, 92, 94, 43 | esumpinfval 32736 |
. . 3
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ Σ*𝑛
∈ ℕ(vol‘𝐴)
= +∞) |
96 | 86, 95 | eqtr4d 2776 |
. 2
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ (vol‘∪ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴)) |
97 | | exmid 894 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ¬ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) |
98 | | rexnal 3100 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ ¬ (vol‘𝐴)
∈ ℝ ↔ ¬ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) |
99 | 98 | orbi2i 912 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈ ℝ) ↔
(∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ ∨ ¬ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ)) |
100 | 97, 99 | mpbir 230 |
. . . 4
⊢
(∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈
ℝ) |
101 | | r19.29 3114 |
. . . . . . 7
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∃𝑛 ∈
ℕ ¬ (vol‘𝐴)
∈ ℝ) → ∃𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ ¬ (vol‘𝐴) ∈
ℝ)) |
102 | | xrge0nre 13379 |
. . . . . . . . 9
⊢
(((vol‘𝐴)
∈ (0[,]+∞) ∧ ¬ (vol‘𝐴) ∈ ℝ) → (vol‘𝐴) = +∞) |
103 | 13, 102 | sylan 581 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧ ¬
(vol‘𝐴) ∈
ℝ) → (vol‘𝐴) = +∞) |
104 | 103 | reximi 3084 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ ¬ (vol‘𝐴)
∈ ℝ) → ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) |
105 | 101, 104 | syl 17 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∃𝑛 ∈
ℕ ¬ (vol‘𝐴)
∈ ℝ) → ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) |
106 | 105 | ex 414 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ (∃𝑛 ∈
ℕ ¬ (vol‘𝐴)
∈ ℝ → ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞)) |
107 | 106 | orim2d 966 |
. . . 4
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ((∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈ ℝ) →
(∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ ∨ ∃𝑛
∈ ℕ (vol‘𝐴) = +∞))) |
108 | 100, 107 | mpi 20 |
. . 3
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ (∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞)) |
109 | 108 | adantr 482 |
. 2
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) →
(∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ ∨ ∃𝑛
∈ ℕ (vol‘𝐴) = +∞)) |
110 | 42, 96, 109 | mpjaodan 958 |
1
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) →
(vol‘∪ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴)) |