| Step | Hyp | Ref
| Expression |
| 1 | | r19.26 3111 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ↔ (∀𝑛
∈ ℕ 𝐴 ∈ dom
vol ∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ)) |
| 2 | | eqid 2737 |
. . . . . 6
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘𝐴))) = seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘𝐴))) |
| 3 | | eqid 2737 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦
(vol‘𝐴)) = (𝑛 ∈ ℕ ↦
(vol‘𝐴)) |
| 4 | 2, 3 | voliun 25589 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ (𝐴 ∈ dom vol
∧ (vol‘𝐴) ∈
ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, <
)) |
| 5 | 1, 4 | sylanbr 582 |
. . . 4
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, <
)) |
| 6 | 5 | an32s 652 |
. . 3
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦
(vol‘𝐴))),
ℝ*, < )) |
| 7 | | nfra1 3284 |
. . . . . . 7
⊢
Ⅎ𝑛∀𝑛 ∈ ℕ 𝐴 ∈ dom vol |
| 8 | | nfra1 3284 |
. . . . . . 7
⊢
Ⅎ𝑛∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ |
| 9 | 7, 8 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑛(∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈
ℝ) |
| 10 | | simpr 484 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑛 ∈ ℕ)
→ 𝑛 ∈
ℕ) |
| 11 | | rspa 3248 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑛 ∈ ℕ)
→ 𝐴 ∈ dom
vol) |
| 12 | | volf 25564 |
. . . . . . . . . . . 12
⊢ vol:dom
vol⟶(0[,]+∞) |
| 13 | 12 | ffvelcdmi 7103 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
(0[,]+∞)) |
| 14 | 11, 13 | syl 17 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑛 ∈ ℕ)
→ (vol‘𝐴) ∈
(0[,]+∞)) |
| 15 | 3 | fvmpt2 7027 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧
(vol‘𝐴) ∈
(0[,]+∞)) → ((𝑛
∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴)) |
| 16 | 10, 14, 15 | syl2anc 584 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑛 ∈ ℕ)
→ ((𝑛 ∈ ℕ
↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴)) |
| 17 | 16 | adantlr 715 |
. . . . . . . 8
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → ((𝑛
∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴)) |
| 18 | 17 | ex 412 |
. . . . . . 7
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → (𝑛
∈ ℕ → ((𝑛
∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴))) |
| 19 | 9, 18 | ralrimi 3257 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → ∀𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴)) |
| 20 | 9, 19 | esumeq2d 34038 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → Σ*𝑛 ∈ ℕ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = Σ*𝑛 ∈ ℕ(vol‘𝐴)) |
| 21 | | simpr 484 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) |
| 22 | 21 | r19.21bi 3251 |
. . . . . . . 8
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → (vol‘𝐴) ∈ ℝ) |
| 23 | 14 | adantlr 715 |
. . . . . . . . 9
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → (vol‘𝐴) ∈ (0[,]+∞)) |
| 24 | | 0xr 11308 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
| 25 | | pnfxr 11315 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
| 26 | | elicc1 13431 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
((vol‘𝐴) ∈
(0[,]+∞) ↔ ((vol‘𝐴) ∈ ℝ* ∧ 0 ≤
(vol‘𝐴) ∧
(vol‘𝐴) ≤
+∞))) |
| 27 | 24, 25, 26 | mp2an 692 |
. . . . . . . . . 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 13162 |
. . . . . . . . 9
⊢
((vol‘𝐴)
∈ ℝ → (vol‘𝐴) < +∞) |
| 31 | 22, 30 | syl 17 |
. . . . . . . 8
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) ∧ 𝑛
∈ ℕ) → (vol‘𝐴) < +∞) |
| 32 | | 0re 11263 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
| 33 | | elico2 13451 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) →
((vol‘𝐴) ∈
(0[,)+∞) ↔ ((vol‘𝐴) ∈ ℝ ∧ 0 ≤
(vol‘𝐴) ∧
(vol‘𝐴) <
+∞))) |
| 34 | 32, 25, 33 | mp2an 692 |
. . . . . . . 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 7137 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → (𝑛
∈ ℕ ↦ (vol‘𝐴)):ℕ⟶(0[,)+∞)) |
| 37 | | nfmpt1 5250 |
. . . . . . 7
⊢
Ⅎ𝑛(𝑛 ∈ ℕ ↦ (vol‘𝐴)) |
| 38 | 37 | esumfsupre 34072 |
. . . . . 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 2779 |
. . . 4
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ) → Σ*𝑛 ∈ ℕ(vol‘𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, <
)) |
| 41 | 40 | adantlr 715 |
. . 3
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ) → Σ*𝑛 ∈ ℕ(vol‘𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, <
)) |
| 42 | 6, 41 | eqtr4d 2780 |
. 2
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴)) |
| 43 | | simpr 484 |
. . . . . . . 8
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ∃𝑛 ∈
ℕ (vol‘𝐴) =
+∞) |
| 44 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑘(vol‘𝐴) = +∞ |
| 45 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛vol |
| 46 | | nfcsb1v 3923 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐴 |
| 47 | 45, 46 | nffv 6916 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐴) |
| 48 | 47 | nfeq1 2921 |
. . . . . . . . 9
⊢
Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ |
| 49 | | csbeq1a 3913 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → 𝐴 = ⦋𝑘 / 𝑛⦌𝐴) |
| 50 | 49 | fveqeq2d 6914 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((vol‘𝐴) = +∞ ↔
(vol‘⦋𝑘
/ 𝑛⦌𝐴) = +∞)) |
| 51 | 44, 48, 50 | cbvrexw 3307 |
. . . . . . . 8
⊢
(∃𝑛 ∈
ℕ (vol‘𝐴) =
+∞ ↔ ∃𝑘
∈ ℕ (vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞) |
| 52 | 43, 51 | sylib 218 |
. . . . . . 7
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ∃𝑘 ∈
ℕ (vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞) |
| 53 | 46 | nfel1 2922 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol |
| 54 | 49 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (𝐴 ∈ dom vol ↔ ⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol)) |
| 55 | 53, 54 | rspc 3610 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ →
(∀𝑛 ∈ ℕ
𝐴 ∈ dom vol →
⦋𝑘 / 𝑛⦌𝐴 ∈ dom vol)) |
| 56 | 55 | impcom 407 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ⦋𝑘 /
𝑛⦌𝐴 ∈ dom
vol) |
| 57 | | iunmbl 25588 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol) |
| 58 | 57 | adantr 480 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol) |
| 59 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛ℕ |
| 60 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛𝑘 |
| 61 | 59, 60, 46, 49 | ssiun2sf 32572 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ →
⦋𝑘 / 𝑛⦌𝐴 ⊆ ∪
𝑛 ∈ ℕ 𝐴) |
| 62 | 61 | adantl 481 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ ⦋𝑘 /
𝑛⦌𝐴 ⊆ ∪ 𝑛 ∈ ℕ 𝐴) |
| 63 | | volss 25568 |
. . . . . . . . . . 11
⊢
((⦋𝑘 /
𝑛⦌𝐴 ∈ dom vol ∧ ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ⦋𝑘 / 𝑛⦌𝐴 ⊆ ∪
𝑛 ∈ ℕ 𝐴) →
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
| 64 | 56, 58, 62, 63 | syl3anc 1373 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ 𝑘 ∈ ℕ)
→ (vol‘⦋𝑘 / 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
| 65 | 64 | adantlr 715 |
. . . . . . . . 9
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧ 𝑘 ∈ ℕ) →
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
| 66 | 65 | adantlr 715 |
. . . . . . . 8
⊢
((((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
∧ 𝑘 ∈ ℕ)
→ (vol‘⦋𝑘 / 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
| 67 | 66 | ralrimiva 3146 |
. . . . . . 7
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ∀𝑘 ∈
ℕ (vol‘⦋𝑘 / 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
| 68 | | r19.29r 3116 |
. . . . . . 7
⊢
((∃𝑘 ∈
ℕ (vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ ∧ ∀𝑘 ∈ ℕ
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) → ∃𝑘 ∈ ℕ
((vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴))) |
| 69 | 52, 67, 68 | syl2anc 584 |
. . . . . 6
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ ∃𝑘 ∈
ℕ ((vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴))) |
| 70 | | breq1 5146 |
. . . . . . . 8
⊢
((vol‘⦋𝑘 / 𝑛⦌𝐴) = +∞ →
((vol‘⦋𝑘 / 𝑛⦌𝐴) ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ +∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴))) |
| 71 | 70 | biimpa 476 |
. . . . . . 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 12277 |
. . . . . 6
⊢ 1 ∈
ℕ |
| 75 | | ne0i 4341 |
. . . . . 6
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
| 76 | | r19.9rzv 4500 |
. . . . . 6
⊢ (ℕ
≠ ∅ → (+∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ ∃𝑘 ∈ ℕ +∞ ≤
(vol‘∪ 𝑛 ∈ ℕ 𝐴))) |
| 77 | 74, 75, 76 | mp2b 10 |
. . . . 5
⊢ (+∞
≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ ∃𝑘 ∈ ℕ +∞ ≤
(vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
| 78 | 73, 77 | sylibr 234 |
. . . 4
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ +∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴)) |
| 79 | | iccssxr 13470 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
| 80 | 12 | ffvelcdmi 7103 |
. . . . . . . 8
⊢ (∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → (vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈ (0[,]+∞)) |
| 81 | 79, 80 | sselid 3981 |
. . . . . . 7
⊢ (∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → (vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
| 82 | 57, 81 | syl 17 |
. . . . . 6
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
| 83 | 82 | ad2antrr 726 |
. . . . 5
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
| 84 | | xgepnf 13207 |
. . . . 5
⊢
((vol‘∪ 𝑛 ∈ ℕ 𝐴) ∈ ℝ* →
(+∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ (vol‘∪ 𝑛 ∈ ℕ 𝐴) = +∞)) |
| 85 | 83, 84 | syl 17 |
. . . 4
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ (+∞ ≤ (vol‘∪ 𝑛 ∈ ℕ 𝐴) ↔ (vol‘∪ 𝑛 ∈ ℕ 𝐴) = +∞)) |
| 86 | 78, 85 | mpbid 232 |
. . 3
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ (vol‘∪ 𝑛 ∈ ℕ 𝐴) = +∞) |
| 87 | | nfdisj1 5124 |
. . . . . 6
⊢
Ⅎ𝑛Disj
𝑛 ∈ ℕ 𝐴 |
| 88 | 7, 87 | nfan 1899 |
. . . . 5
⊢
Ⅎ𝑛(∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) |
| 89 | | nfre1 3285 |
. . . . 5
⊢
Ⅎ𝑛∃𝑛 ∈ ℕ (vol‘𝐴) = +∞ |
| 90 | 88, 89 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑛((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) |
| 91 | | nnex 12272 |
. . . . 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 34074 |
. . 3
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ Σ*𝑛
∈ ℕ(vol‘𝐴)
= +∞) |
| 96 | 86, 95 | eqtr4d 2780 |
. 2
⊢
(((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) ∧
∃𝑛 ∈ ℕ
(vol‘𝐴) = +∞)
→ (vol‘∪ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴)) |
| 97 | | exmid 895 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ¬ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) |
| 98 | | rexnal 3100 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ ¬ (vol‘𝐴)
∈ ℝ ↔ ¬ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) |
| 99 | 98 | orbi2i 913 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈ ℝ) ↔
(∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ ∨ ¬ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ)) |
| 100 | 97, 99 | mpbir 231 |
. . . 4
⊢
(∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈
ℝ) |
| 101 | | r19.29 3114 |
. . . . . . 7
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ ∃𝑛 ∈
ℕ ¬ (vol‘𝐴)
∈ ℝ) → ∃𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ ¬ (vol‘𝐴) ∈
ℝ)) |
| 102 | | xrge0nre 13493 |
. . . . . . . . 9
⊢
(((vol‘𝐴)
∈ (0[,]+∞) ∧ ¬ (vol‘𝐴) ∈ ℝ) → (vol‘𝐴) = +∞) |
| 103 | 13, 102 | sylan 580 |
. . . . . . . 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 412 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ (∃𝑛 ∈
ℕ ¬ (vol‘𝐴)
∈ ℝ → ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞)) |
| 107 | 106 | orim2d 969 |
. . . 4
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ ((∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈ ℝ) →
(∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ ∨ ∃𝑛
∈ ℕ (vol‘𝐴) = +∞))) |
| 108 | 100, 107 | mpi 20 |
. . 3
⊢
(∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
→ (∀𝑛 ∈
ℕ (vol‘𝐴)
∈ ℝ ∨ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞)) |
| 109 | 108 | adantr 480 |
. 2
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) →
(∀𝑛 ∈ ℕ
(vol‘𝐴) ∈
ℝ ∨ ∃𝑛
∈ ℕ (vol‘𝐴) = +∞)) |
| 110 | 42, 96, 109 | mpjaodan 961 |
1
⊢
((∀𝑛 ∈
ℕ 𝐴 ∈ dom vol
∧ Disj 𝑛 ∈
ℕ 𝐴) →
(vol‘∪ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴)) |