| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑛𝜑 |
| 2 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑛vol |
| 3 | | nfiu1 5027 |
. . . . . . 7
⊢
Ⅎ𝑛∪ 𝑛 ∈ ℕ (𝐸‘𝑛) |
| 4 | 2, 3 | nffv 6916 |
. . . . . 6
⊢
Ⅎ𝑛(vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) |
| 5 | 4 | nfeq1 2921 |
. . . . 5
⊢
Ⅎ𝑛(vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = +∞ |
| 6 | | iccssxr 13470 |
. . . . . . . . . 10
⊢
(0[,]+∞) ⊆ ℝ* |
| 7 | | volf 25564 |
. . . . . . . . . . . 12
⊢ vol:dom
vol⟶(0[,]+∞) |
| 8 | 7 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → vol:dom
vol⟶(0[,]+∞)) |
| 9 | | voliunsge0lem.e |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸:ℕ⟶dom vol) |
| 10 | 9 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸‘𝑛) ∈ dom vol) |
| 11 | 10 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐸‘𝑛) ∈ dom vol) |
| 12 | | iunmbl 25588 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ℕ (𝐸‘𝑛) ∈ dom vol → ∪ 𝑛 ∈ ℕ (𝐸‘𝑛) ∈ dom vol) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐸‘𝑛) ∈ dom vol) |
| 14 | 8, 13 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ (𝜑 → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) ∈ (0[,]+∞)) |
| 15 | 6, 14 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) ∈
ℝ*) |
| 16 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) ∈
ℝ*) |
| 17 | 16 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ (vol‘(𝐸‘𝑛)) = +∞) → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) ∈
ℝ*) |
| 18 | | id 22 |
. . . . . . . . . 10
⊢
((vol‘(𝐸‘𝑛)) = +∞ → (vol‘(𝐸‘𝑛)) = +∞) |
| 19 | 18 | eqcomd 2743 |
. . . . . . . . 9
⊢
((vol‘(𝐸‘𝑛)) = +∞ → +∞ =
(vol‘(𝐸‘𝑛))) |
| 20 | 19 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ (vol‘(𝐸‘𝑛)) = +∞) → +∞ =
(vol‘(𝐸‘𝑛))) |
| 21 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑛 ∈ ℕ (𝐸‘𝑛) ∈ dom vol) |
| 22 | | ssiun2 5047 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝐸‘𝑛) ⊆ ∪
𝑛 ∈ ℕ (𝐸‘𝑛)) |
| 23 | 22 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸‘𝑛) ⊆ ∪
𝑛 ∈ ℕ (𝐸‘𝑛)) |
| 24 | | volss 25568 |
. . . . . . . . . 10
⊢ (((𝐸‘𝑛) ∈ dom vol ∧ ∪ 𝑛 ∈ ℕ (𝐸‘𝑛) ∈ dom vol ∧ (𝐸‘𝑛) ⊆ ∪
𝑛 ∈ ℕ (𝐸‘𝑛)) → (vol‘(𝐸‘𝑛)) ≤ (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛))) |
| 25 | 10, 21, 23, 24 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐸‘𝑛)) ≤ (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛))) |
| 26 | 25 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ (vol‘(𝐸‘𝑛)) = +∞) → (vol‘(𝐸‘𝑛)) ≤ (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛))) |
| 27 | 20, 26 | eqbrtrd 5165 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ (vol‘(𝐸‘𝑛)) = +∞) → +∞ ≤
(vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛))) |
| 28 | 17, 27 | xrgepnfd 45342 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ (vol‘(𝐸‘𝑛)) = +∞) → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = +∞) |
| 29 | 28 | 3exp 1120 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ → ((vol‘(𝐸‘𝑛)) = +∞ → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = +∞))) |
| 30 | 1, 5, 29 | rexlimd 3266 |
. . . 4
⊢ (𝜑 → (∃𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) = +∞ → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = +∞)) |
| 31 | 30 | imp 406 |
. . 3
⊢ ((𝜑 ∧ ∃𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) = +∞) → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = +∞) |
| 32 | | nfre1 3285 |
. . . . 5
⊢
Ⅎ𝑛∃𝑛 ∈ ℕ
(vol‘(𝐸‘𝑛)) = +∞ |
| 33 | 1, 32 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑛(𝜑 ∧ ∃𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) = +∞) |
| 34 | | nnex 12272 |
. . . . 5
⊢ ℕ
∈ V |
| 35 | 34 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) = +∞) → ℕ ∈
V) |
| 36 | 7 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → vol:dom
vol⟶(0[,]+∞)) |
| 37 | 36, 10 | ffvelcdmd 7105 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐸‘𝑛)) ∈ (0[,]+∞)) |
| 38 | 37 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ ∃𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) = +∞) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐸‘𝑛)) ∈ (0[,]+∞)) |
| 39 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) = +∞) → ∃𝑛 ∈ ℕ
(vol‘(𝐸‘𝑛)) = +∞) |
| 40 | 33, 35, 38, 39 | sge0pnfmpt 46460 |
. . 3
⊢ ((𝜑 ∧ ∃𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) = +∞) →
(Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛)))) = +∞) |
| 41 | 31, 40 | eqtr4d 2780 |
. 2
⊢ ((𝜑 ∧ ∃𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) = +∞) → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) =
(Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛))))) |
| 42 | | ralnex 3072 |
. . . . . 6
⊢
(∀𝑛 ∈
ℕ ¬ (vol‘(𝐸‘𝑛)) = +∞ ↔ ¬ ∃𝑛 ∈ ℕ
(vol‘(𝐸‘𝑛)) = +∞) |
| 43 | 42 | biimpri 228 |
. . . . 5
⊢ (¬
∃𝑛 ∈ ℕ
(vol‘(𝐸‘𝑛)) = +∞ →
∀𝑛 ∈ ℕ
¬ (vol‘(𝐸‘𝑛)) = +∞) |
| 44 | 43 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ ¬ ∃𝑛 ∈ ℕ
(vol‘(𝐸‘𝑛)) = +∞) →
∀𝑛 ∈ ℕ
¬ (vol‘(𝐸‘𝑛)) = +∞) |
| 45 | 37 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬
(vol‘(𝐸‘𝑛)) = +∞) →
(vol‘(𝐸‘𝑛)) ∈
(0[,]+∞)) |
| 46 | 18 | necon3bi 2967 |
. . . . . . . . . 10
⊢ (¬
(vol‘(𝐸‘𝑛)) = +∞ →
(vol‘(𝐸‘𝑛)) ≠
+∞) |
| 47 | 46 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬
(vol‘(𝐸‘𝑛)) = +∞) →
(vol‘(𝐸‘𝑛)) ≠
+∞) |
| 48 | | ge0xrre 45544 |
. . . . . . . . 9
⊢
(((vol‘(𝐸‘𝑛)) ∈ (0[,]+∞) ∧
(vol‘(𝐸‘𝑛)) ≠ +∞) →
(vol‘(𝐸‘𝑛)) ∈
ℝ) |
| 49 | 45, 47, 48 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬
(vol‘(𝐸‘𝑛)) = +∞) →
(vol‘(𝐸‘𝑛)) ∈
ℝ) |
| 50 | 49 | ex 412 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (¬
(vol‘(𝐸‘𝑛)) = +∞ →
(vol‘(𝐸‘𝑛)) ∈
ℝ)) |
| 51 | | renepnf 11309 |
. . . . . . . . 9
⊢
((vol‘(𝐸‘𝑛)) ∈ ℝ → (vol‘(𝐸‘𝑛)) ≠ +∞) |
| 52 | 51 | neneqd 2945 |
. . . . . . . 8
⊢
((vol‘(𝐸‘𝑛)) ∈ ℝ → ¬
(vol‘(𝐸‘𝑛)) = +∞) |
| 53 | 52 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐸‘𝑛)) ∈ ℝ → ¬
(vol‘(𝐸‘𝑛)) = +∞)) |
| 54 | 50, 53 | impbid 212 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (¬
(vol‘(𝐸‘𝑛)) = +∞ ↔
(vol‘(𝐸‘𝑛)) ∈
ℝ)) |
| 55 | 54 | ralbidva 3176 |
. . . . 5
⊢ (𝜑 → (∀𝑛 ∈ ℕ ¬
(vol‘(𝐸‘𝑛)) = +∞ ↔
∀𝑛 ∈ ℕ
(vol‘(𝐸‘𝑛)) ∈
ℝ)) |
| 56 | 55 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ ∃𝑛 ∈ ℕ
(vol‘(𝐸‘𝑛)) = +∞) →
(∀𝑛 ∈ ℕ
¬ (vol‘(𝐸‘𝑛)) = +∞ ↔ ∀𝑛 ∈ ℕ
(vol‘(𝐸‘𝑛)) ∈
ℝ)) |
| 57 | 44, 56 | mpbid 232 |
. . 3
⊢ ((𝜑 ∧ ¬ ∃𝑛 ∈ ℕ
(vol‘(𝐸‘𝑛)) = +∞) →
∀𝑛 ∈ ℕ
(vol‘(𝐸‘𝑛)) ∈
ℝ) |
| 58 | | nfra1 3284 |
. . . . . . 7
⊢
Ⅎ𝑛∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ |
| 59 | 1, 58 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑛(𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) |
| 60 | 10 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (𝐸‘𝑛) ∈ dom vol) |
| 61 | | rspa 3248 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ ∧ 𝑛 ∈ ℕ) → (vol‘(𝐸‘𝑛)) ∈ ℝ) |
| 62 | 61 | adantll 714 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐸‘𝑛)) ∈ ℝ) |
| 63 | 60, 62 | jca 511 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝐸‘𝑛) ∈ dom vol ∧ (vol‘(𝐸‘𝑛)) ∈ ℝ)) |
| 64 | 63 | ex 412 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) → (𝑛 ∈ ℕ → ((𝐸‘𝑛) ∈ dom vol ∧ (vol‘(𝐸‘𝑛)) ∈ ℝ))) |
| 65 | 59, 64 | ralrimi 3257 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) → ∀𝑛 ∈ ℕ ((𝐸‘𝑛) ∈ dom vol ∧ (vol‘(𝐸‘𝑛)) ∈ ℝ)) |
| 66 | | voliunsge0lem.d |
. . . . . 6
⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐸‘𝑛)) |
| 67 | 66 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) → Disj 𝑛 ∈ ℕ (𝐸‘𝑛)) |
| 68 | | voliunsge0lem.s |
. . . . . 6
⊢ 𝑆 = seq1( + , 𝐺) |
| 69 | | voliunsge0lem.g |
. . . . . 6
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛))) |
| 70 | 68, 69 | voliun 25589 |
. . . . 5
⊢
((∀𝑛 ∈
ℕ ((𝐸‘𝑛) ∈ dom vol ∧
(vol‘(𝐸‘𝑛)) ∈ ℝ) ∧
Disj 𝑛 ∈
ℕ (𝐸‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = sup(ran 𝑆, ℝ*, <
)) |
| 71 | 65, 67, 70 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = sup(ran 𝑆, ℝ*, <
)) |
| 72 | | 1zzd 12648 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) → 1 ∈
ℤ) |
| 73 | | nnuz 12921 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
| 74 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑛 𝑚 ∈ ℕ |
| 75 | 59, 74 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑛((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑚 ∈ ℕ) |
| 76 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑛(vol‘(𝐸‘𝑚)) ∈ (0[,)+∞) |
| 77 | 75, 76 | nfim 1896 |
. . . . . . 7
⊢
Ⅎ𝑛(((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (vol‘(𝐸‘𝑚)) ∈ (0[,)+∞)) |
| 78 | | eleq1w 2824 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑛 ∈ ℕ ↔ 𝑚 ∈ ℕ)) |
| 79 | 78 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑛 ∈ ℕ) ↔ ((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑚 ∈ ℕ))) |
| 80 | | 2fveq3 6911 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (vol‘(𝐸‘𝑛)) = (vol‘(𝐸‘𝑚))) |
| 81 | 80 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → ((vol‘(𝐸‘𝑛)) ∈ (0[,)+∞) ↔
(vol‘(𝐸‘𝑚)) ∈
(0[,)+∞))) |
| 82 | 79, 81 | imbi12d 344 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → ((((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐸‘𝑛)) ∈ (0[,)+∞)) ↔ (((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (vol‘(𝐸‘𝑚)) ∈ (0[,)+∞)))) |
| 83 | | 0xr 11308 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
| 84 | 83 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → 0 ∈
ℝ*) |
| 85 | | pnfxr 11315 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
| 86 | 85 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → +∞ ∈
ℝ*) |
| 87 | 62 | rexrd 11311 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐸‘𝑛)) ∈
ℝ*) |
| 88 | | volge0 45976 |
. . . . . . . . . 10
⊢ ((𝐸‘𝑛) ∈ dom vol → 0 ≤
(vol‘(𝐸‘𝑛))) |
| 89 | 10, 88 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤
(vol‘(𝐸‘𝑛))) |
| 90 | 89 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → 0 ≤
(vol‘(𝐸‘𝑛))) |
| 91 | 62 | ltpnfd 13163 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐸‘𝑛)) < +∞) |
| 92 | 84, 86, 87, 90, 91 | elicod 13437 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐸‘𝑛)) ∈ (0[,)+∞)) |
| 93 | 77, 82, 92 | chvarfv 2240 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (vol‘(𝐸‘𝑚)) ∈ (0[,)+∞)) |
| 94 | 80 | cbvmptv 5255 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦
(vol‘(𝐸‘𝑛))) = (𝑚 ∈ ℕ ↦ (vol‘(𝐸‘𝑚))) |
| 95 | 93, 94 | fmptd 7134 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) → (𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛))):ℕ⟶(0[,)+∞)) |
| 96 | | seqeq3 14047 |
. . . . . . 7
⊢ (𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛))) → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛))))) |
| 97 | 69, 96 | ax-mp 5 |
. . . . . 6
⊢ seq1( + ,
𝐺) = seq1( + , (𝑛 ∈ ℕ ↦
(vol‘(𝐸‘𝑛)))) |
| 98 | 68, 97 | eqtri 2765 |
. . . . 5
⊢ 𝑆 = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛)))) |
| 99 | 72, 73, 95, 98 | sge0seq 46461 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) →
(Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛)))) = sup(ran 𝑆, ℝ*, <
)) |
| 100 | 71, 99 | eqtr4d 2780 |
. . 3
⊢ ((𝜑 ∧ ∀𝑛 ∈ ℕ (vol‘(𝐸‘𝑛)) ∈ ℝ) → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) =
(Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛))))) |
| 101 | 57, 100 | syldan 591 |
. 2
⊢ ((𝜑 ∧ ¬ ∃𝑛 ∈ ℕ
(vol‘(𝐸‘𝑛)) = +∞) →
(vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) =
(Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛))))) |
| 102 | 41, 101 | pm2.61dan 813 |
1
⊢ (𝜑 → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) =
(Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛))))) |