Step | Hyp | Ref
| Expression |
1 | | r19.26 3046 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ↔ (∀𝑛
∈ ℕ 𝐴 ∈ dom
vol ∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ)) |
2 | | eqid 2610 |
. . . . . 6
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘𝐴))) = seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘𝐴))) |
3 | | eqid 2610 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦
(vol‘𝐴)) = (𝑛 ∈ ℕ ↦
(vol‘𝐴)) |
4 | 2, 3 | voliun 23129 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, <
)) |
5 | 1, 4 | sylanbr 489 |
. . . 4
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, <
)) |
6 | 5 | an32s 842 |
. . 3
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦
(vol‘𝐴))),
ℝ*, < )) |
7 | | nfra1 2925 |
. . . . . . 7
⊢
Ⅎ𝑛∀𝑛 ∈ ℕ 𝐴 ∈ dom vol |
8 | | nfra1 2925 |
. . . . . . 7
⊢
Ⅎ𝑛∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ |
9 | 7, 8 | nfan 1816 |
. . . . . 6
⊢
Ⅎ𝑛(∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈
ℝ) |
10 | | simpr 476 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑛 ∈ ℕ)
→ 𝑛 ∈
ℕ) |
11 | | rspa 2914 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑛 ∈ ℕ)
→ 𝐴 ∈ dom
vol) |
12 | | volf 23104 |
. . . . . . . . . . . 12
⊢ vol:dom
vol⟶(0[,]+∞) |
13 | 12 | ffvelrni 6266 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
(0[,]+∞)) |
14 | 11, 13 | syl 17 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑛 ∈ ℕ)
→ (vol‘𝐴) ∈
(0[,]+∞)) |
15 | 3 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧
(vol‘𝐴) ∈
(0[,]+∞)) → ((𝑛
∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴)) |
16 | 10, 14, 15 | syl2anc 691 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑛 ∈ ℕ)
→ ((𝑛 ∈ ℕ
↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴)) |
17 | 16 | adantlr 747 |
. . . . . . . 8
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → ((𝑛
∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴)) |
18 | 17 | ex 449 |
. . . . . . 7
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → (𝑛
∈ ℕ → ((𝑛
∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴))) |
19 | 9, 18 | ralrimi 2940 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → ∀𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴)) |
20 | 9, 19 | esumeq2d 29426 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → Σ*𝑛 ∈ ℕ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = Σ*𝑛 ∈ ℕ(vol‘𝐴)) |
21 | | simpr 476 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) |
22 | 21 | r19.21bi 2916 |
. . . . . . . 8
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → (vol‘𝐴) ∈ ℝ) |
23 | 14 | adantlr 747 |
. . . . . . . . 9
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → (vol‘𝐴) ∈ (0[,]+∞)) |
24 | | 0xr 9965 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
25 | | pnfxr 9971 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
26 | | elicc1 12090 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
((vol‘𝐴) ∈
(0[,]+∞) ↔ ((vol‘𝐴) ∈ ℝ* ∧ 0 ≤
(vol‘𝐴) ∧
(vol‘𝐴) ≤
+∞))) |
27 | 24, 25, 26 | mp2an 704 |
. . . . . . . . . 10
⊢
((vol‘𝐴)
∈ (0[,]+∞) ↔ ((vol‘𝐴) ∈ ℝ* ∧ 0 ≤
(vol‘𝐴) ∧
(vol‘𝐴) ≤
+∞)) |
28 | 27 | simp2bi 1070 |
. . . . . . . . 9
⊢
((vol‘𝐴)
∈ (0[,]+∞) → 0 ≤ (vol‘𝐴)) |
29 | 23, 28 | syl 17 |
. . . . . . . 8
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → 0 ≤ (vol‘𝐴)) |
30 | | ltpnf 11830 |
. . . . . . . . 9
⊢
((vol‘𝐴)
∈ ℝ → (vol‘𝐴) < +∞) |
31 | 22, 30 | syl 17 |
. . . . . . . 8
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → (vol‘𝐴) < +∞) |
32 | | 0re 9919 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
33 | | elico2 12108 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) →
((vol‘𝐴) ∈
(0[,)+∞) ↔ ((vol‘𝐴) ∈ ℝ ∧ 0 ≤
(vol‘𝐴) ∧
(vol‘𝐴) <
+∞))) |
34 | 32, 25, 33 | mp2an 704 |
. . . . . . . 8
⊢
((vol‘𝐴)
∈ (0[,)+∞) ↔ ((vol‘𝐴) ∈ ℝ ∧ 0 ≤
(vol‘𝐴) ∧
(vol‘𝐴) <
+∞)) |
35 | 22, 29, 31, 34 | syl3anbrc 1239 |
. . . . . . 7
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → (vol‘𝐴) ∈ (0[,)+∞)) |
36 | 9, 35, 3 | fmptdf 6294 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → (𝑛
∈ ℕ ↦ (vol‘𝐴)):ℕ⟶(0[,)+∞)) |
37 | | nfmpt1 4675 |
. . . . . . 7
⊢
Ⅎ𝑛(𝑛 ∈ ℕ ↦ (vol‘𝐴)) |
38 | 37 | esumfsupre 29460 |
. . . . . 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 2646 |
. . . 4
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → Σ*𝑛 ∈ ℕ(vol‘𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, <
)) |
41 | 40 | adantlr 747 |
. . 3
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ) → Σ*𝑛 ∈ ℕ(vol‘𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, <
)) |
42 | 6, 41 | eqtr4d 2647 |
. 2
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴)) |
43 | | simpr 476 |
. . . . . . . 8
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ∃𝑛 ∈
ℕ (vol‘𝐴) =
+∞) |
44 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑘(vol‘𝐴) = +∞ |
45 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛vol |
46 | | nfcsb1v 3515 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐴 |
47 | 45, 46 | nffv 6110 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐴) |
48 | 47 | nfeq1 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ |
49 | | csbeq1a 3508 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → 𝐴 = ⦋𝑘 / 𝑛⦌𝐴) |
50 | 49 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (vol‘𝐴) = (vol‘⦋𝑘 / 𝑛⦌𝐴)) |
51 | 50 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((vol‘𝐴) = +∞ ↔
(vol‘⦋𝑘
/ 𝑛⦌𝐴) = +∞)) |
52 | 44, 48, 51 | cbvrex 3144 |
. . . . . . . 8
⊢
(∃𝑛 ∈
ℕ (vol‘𝐴) =
+∞ ↔ ∃𝑘
∈ ℕ (vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞) |
53 | 43, 52 | sylib 207 |
. . . . . . 7
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ∃𝑘 ∈
ℕ (vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞) |
54 | 46 | nfel1 2765 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol |
55 | 49 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (𝐴 ∈ dom vol ↔ ⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol)) |
56 | 54, 55 | rspc 3276 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ →
(∀𝑛 ∈ ℕ
𝐴 ∈ dom vol →
⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol)) |
57 | 56 | impcom 445 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ⦋𝑘 /
𝑛⦌𝐴 ∈ dom
vol) |
58 | | iunmbl 23128 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol) |
59 | 58 | adantr 480 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol) |
60 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛ℕ |
61 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛𝑘 |
62 | 60, 61, 46, 49 | ssiun2sf 28760 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ →
⦋𝑘 / 𝑛⦌𝐴 ⊆ ∪
𝑛 ∈ ℕ 𝐴) |
63 | 62 | adantl 481 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ⦋𝑘 /
𝑛⦌𝐴 ⊆ ∪ 𝑛 ∈ ℕ 𝐴) |
64 | | volss 23108 |
. . . . . . . . . . 11
⊢
((⦋𝑘 /
𝑛⦌𝐴 ∈ dom vol ∧ ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ⦋𝑘 / 𝑛⦌𝐴 ⊆ ∪
𝑛 ∈ ℕ 𝐴) →
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
65 | 57, 59, 63, 64 | syl3anc 1318 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ (vol‘⦋𝑘 / 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
66 | 65 | adantlr 747 |
. . . . . . . . 9
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧ 𝑘 ∈ ℕ) →
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
67 | 66 | adantlr 747 |
. . . . . . . 8
⊢
((((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
∧ 𝑘 ∈ ℕ)
→ (vol‘⦋𝑘 / 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
68 | 67 | ralrimiva 2949 |
. . . . . . 7
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ∀𝑘 ∈
ℕ (vol‘⦋𝑘 / 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
69 | | r19.29r 3055 |
. . . . . . 7
⊢
((∃𝑘 ∈
ℕ (vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ ∧ ∀𝑘 ∈ ℕ
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) → ∃𝑘 ∈ ℕ
((vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴))) |
70 | 53, 68, 69 | syl2anc 691 |
. . . . . 6
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ∃𝑘 ∈
ℕ ((vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴))) |
71 | | breq1 4586 |
. . . . . . . 8
⊢
((vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ →
((vol‘⦋𝑘 / 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ +∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴))) |
72 | 71 | biimpa 500 |
. . . . . . 7
⊢
(((vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) → +∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
73 | 72 | reximi 2994 |
. . . . . 6
⊢
(∃𝑘 ∈
ℕ ((vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) → ∃𝑘 ∈ ℕ +∞ ≤
(vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
74 | 70, 73 | syl 17 |
. . . . 5
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ∃𝑘 ∈
ℕ +∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
75 | | 1nn 10908 |
. . . . . 6
⊢ 1 ∈
ℕ |
76 | | ne0i 3880 |
. . . . . 6
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
77 | | r19.9rzv 4017 |
. . . . . 6
⊢ (ℕ
≠ ∅ → (+∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ ∃𝑘 ∈ ℕ +∞ ≤
(vol‘∪ 𝑛 ∈ ℕ 𝐴))) |
78 | 75, 76, 77 | mp2b 10 |
. . . . 5
⊢ (+∞
≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ ∃𝑘 ∈ ℕ +∞ ≤
(vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
79 | 74, 78 | sylibr 223 |
. . . 4
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ +∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
80 | | iccssxr 12127 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
81 | 12 | ffvelrni 6266 |
. . . . . . . 8
⊢ (∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → (vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈ (0[,]+∞)) |
82 | 80, 81 | sseldi 3566 |
. . . . . . 7
⊢ (∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → (vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
83 | 58, 82 | syl 17 |
. . . . . 6
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
84 | 83 | ad2antrr 758 |
. . . . 5
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
85 | | xgepnf 28904 |
. . . . 5
⊢
((vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈ ℝ* →
(+∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ (vol‘∪ 𝑛 ∈ ℕ 𝐴) = +∞)) |
86 | 84, 85 | syl 17 |
. . . 4
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ (+∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ (vol‘∪ 𝑛 ∈ ℕ 𝐴) = +∞)) |
87 | 79, 86 | mpbid 221 |
. . 3
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ (vol‘∪ 𝑛 ∈ ℕ 𝐴) = +∞) |
88 | | nfdisj1 4566 |
. . . . . 6
⊢
Ⅎ𝑛Disj
𝑛 ∈ ℕ 𝐴 |
89 | 7, 88 | nfan 1816 |
. . . . 5
⊢
Ⅎ𝑛(∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) |
90 | | nfre1 2988 |
. . . . 5
⊢
Ⅎ𝑛∃𝑛 ∈ ℕ (vol‘𝐴) = +∞ |
91 | 89, 90 | nfan 1816 |
. . . 4
⊢
Ⅎ𝑛((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) |
92 | | nnex 10903 |
. . . . 5
⊢ ℕ
∈ V |
93 | 92 | a1i 11 |
. . . 4
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ℕ ∈ V) |
94 | 14 | 3ad2antr3 1221 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ (Disj 𝑛 ∈
ℕ 𝐴 ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞
∧ 𝑛 ∈ ℕ))
→ (vol‘𝐴) ∈
(0[,]+∞)) |
95 | 94 | 3anassrs 1282 |
. . . 4
⊢
((((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
∧ 𝑛 ∈ ℕ)
→ (vol‘𝐴) ∈
(0[,]+∞)) |
96 | 91, 93, 95, 43 | esumpinfval 29462 |
. . 3
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ Σ*𝑛
∈ ℕ(vol‘𝐴)
= +∞) |
97 | 87, 96 | eqtr4d 2647 |
. 2
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ (vol‘∪ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴)) |
98 | | exmid 430 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ¬ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) |
99 | | rexnal 2978 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ ¬ (vol‘𝐴)
∈ ℝ ↔ ¬ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) |
100 | 99 | orbi2i 540 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈ ℝ) ↔
(∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ ∨ ¬ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ)) |
101 | 98, 100 | mpbir 220 |
. . . 4
⊢
(∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈
ℝ) |
102 | | r19.29 3054 |
. . . . . . 7
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∃𝑛 ∈
ℕ ¬ (vol‘𝐴)
∈ ℝ) → ∃𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ ¬ (vol‘𝐴) ∈
ℝ)) |
103 | | xrge0nre 12148 |
. . . . . . . . 9
⊢
(((vol‘𝐴)
∈ (0[,]+∞) ∧ ¬ (vol‘𝐴) ∈ ℝ) → (vol‘𝐴) = +∞) |
104 | 13, 103 | sylan 487 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧ ¬
(vol‘𝐴) ∈
ℝ) → (vol‘𝐴) = +∞) |
105 | 104 | reximi 2994 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ ¬ (vol‘𝐴)
∈ ℝ) → ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) |
106 | 102, 105 | syl 17 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∃𝑛 ∈
ℕ ¬ (vol‘𝐴)
∈ ℝ) → ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) |
107 | 106 | ex 449 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ (∃𝑛 ∈
ℕ ¬ (vol‘𝐴)
∈ ℝ → ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞)) |
108 | 107 | orim2d 881 |
. . . 4
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ((∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈ ℝ) →
(∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ ∨ ∃𝑛
∈ ℕ (vol‘𝐴) = +∞))) |
109 | 101, 108 | mpi 20 |
. . 3
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ (∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞)) |
110 | 109 | adantr 480 |
. 2
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) →
(∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ ∨ ∃𝑛
∈ ℕ (vol‘𝐴) = +∞)) |
111 | 42, 97, 110 | mpjaodan 823 |
1
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) →
(vol‘∪ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴)) |