Step | Hyp | Ref
| Expression |
1 | | voliunlem.3 |
. . . 4
⊢ (𝜑 → 𝐹:ℕ⟶dom vol) |
2 | | voliunlem.5 |
. . . 4
⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖)) |
3 | | voliunlem.6 |
. . . 4
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) |
4 | 1, 2, 3 | voliunlem2 23716 |
. . 3
⊢ (𝜑 → ∪ ran 𝐹 ∈ dom vol) |
5 | | mblvol 23695 |
. . 3
⊢ (∪ ran 𝐹 ∈ dom vol → (vol‘∪ ran 𝐹) = (vol*‘∪
ran 𝐹)) |
6 | 4, 5 | syl 17 |
. 2
⊢ (𝜑 → (vol‘∪ ran 𝐹) = (vol*‘∪
ran 𝐹)) |
7 | | eqid 2824 |
. . . . 5
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) |
8 | | eqid 2824 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛))) |
9 | 1 | ffvelrnda 6607 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ dom vol) |
10 | | mblss 23696 |
. . . . . 6
⊢ ((𝐹‘𝑛) ∈ dom vol → (𝐹‘𝑛) ⊆ ℝ) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ ℝ) |
12 | | mblvol 23695 |
. . . . . . 7
⊢ ((𝐹‘𝑛) ∈ dom vol → (vol‘(𝐹‘𝑛)) = (vol*‘(𝐹‘𝑛))) |
13 | 9, 12 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) = (vol*‘(𝐹‘𝑛))) |
14 | | voliunlem3.4 |
. . . . . . 7
⊢ (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ) |
15 | | 2fveq3 6437 |
. . . . . . . . 9
⊢ (𝑖 = 𝑛 → (vol‘(𝐹‘𝑖)) = (vol‘(𝐹‘𝑛))) |
16 | 15 | eleq1d 2890 |
. . . . . . . 8
⊢ (𝑖 = 𝑛 → ((vol‘(𝐹‘𝑖)) ∈ ℝ ↔ (vol‘(𝐹‘𝑛)) ∈ ℝ)) |
17 | 16 | rspccva 3524 |
. . . . . . 7
⊢
((∀𝑖 ∈
ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) ∈ ℝ) |
18 | 14, 17 | sylan 577 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) ∈ ℝ) |
19 | 13, 18 | eqeltrrd 2906 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘(𝐹‘𝑛)) ∈ ℝ) |
20 | 7, 8, 11, 19 | ovoliun 23670 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ (𝐹‘𝑛)) ≤ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛)))), ℝ*, <
)) |
21 | 1 | ffnd 6278 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn ℕ) |
22 | | fniunfv 6759 |
. . . . . 6
⊢ (𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹) |
24 | 23 | fveq2d 6436 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ (𝐹‘𝑛)) = (vol*‘∪
ran 𝐹)) |
25 | | voliunlem3.1 |
. . . . . . 7
⊢ 𝑆 = seq1( + , 𝐺) |
26 | | voliunlem3.2 |
. . . . . . . . 9
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛))) |
27 | 13 | mpteq2dva 4966 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛)))) |
28 | 26, 27 | syl5eq 2872 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛)))) |
29 | 28 | seqeq3d 13102 |
. . . . . . 7
⊢ (𝜑 → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛))))) |
30 | 25, 29 | syl5req 2873 |
. . . . . 6
⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) = 𝑆) |
31 | 30 | rneqd 5584 |
. . . . 5
⊢ (𝜑 → ran seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) = ran 𝑆) |
32 | 31 | supeq1d 8620 |
. . . 4
⊢ (𝜑 → sup(ran seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))), ℝ*, <
) = sup(ran 𝑆,
ℝ*, < )) |
33 | 20, 24, 32 | 3brtr3d 4903 |
. . 3
⊢ (𝜑 → (vol*‘∪ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, <
)) |
34 | 1 | frnd 6284 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝐹 ⊆ dom vol) |
35 | | mblss 23696 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ dom vol → 𝑥 ⊆
ℝ) |
36 | | reex 10342 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
37 | 36 | elpw2 5049 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝒫 ℝ ↔
𝑥 ⊆
ℝ) |
38 | 35, 37 | sylibr 226 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ dom vol → 𝑥 ∈ 𝒫
ℝ) |
39 | 38 | ssriv 3830 |
. . . . . . . . . . . 12
⊢ dom vol
⊆ 𝒫 ℝ |
40 | 34, 39 | syl6ss 3838 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐹 ⊆ 𝒫 ℝ) |
41 | | sspwuni 4831 |
. . . . . . . . . . 11
⊢ (ran
𝐹 ⊆ 𝒫 ℝ
↔ ∪ ran 𝐹 ⊆ ℝ) |
42 | 40, 41 | sylib 210 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ ran 𝐹 ⊆ ℝ) |
43 | | ovolcl 23643 |
. . . . . . . . . 10
⊢ (∪ ran 𝐹 ⊆ ℝ → (vol*‘∪ ran 𝐹) ∈
ℝ*) |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (vol*‘∪ ran 𝐹) ∈
ℝ*) |
45 | | ovolge0 23646 |
. . . . . . . . . 10
⊢ (∪ ran 𝐹 ⊆ ℝ → 0 ≤
(vol*‘∪ ran 𝐹)) |
46 | 42, 45 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (vol*‘∪ ran 𝐹)) |
47 | | mnflt0 12244 |
. . . . . . . . . 10
⊢ -∞
< 0 |
48 | | mnfxr 10413 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
49 | | 0xr 10402 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
50 | | xrltletr 12275 |
. . . . . . . . . . 11
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ (vol*‘∪ ran 𝐹) ∈ ℝ*) →
((-∞ < 0 ∧ 0 ≤ (vol*‘∪ ran
𝐹)) → -∞ <
(vol*‘∪ ran 𝐹))) |
51 | 48, 49, 50 | mp3an12 1581 |
. . . . . . . . . 10
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* →
((-∞ < 0 ∧ 0 ≤ (vol*‘∪ ran
𝐹)) → -∞ <
(vol*‘∪ ran 𝐹))) |
52 | 47, 51 | mpani 689 |
. . . . . . . . 9
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* → (0 ≤
(vol*‘∪ ran 𝐹) → -∞ < (vol*‘∪ ran 𝐹))) |
53 | 44, 46, 52 | sylc 65 |
. . . . . . . 8
⊢ (𝜑 → -∞ <
(vol*‘∪ ran 𝐹)) |
54 | | xrrebnd 12286 |
. . . . . . . . . 10
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* →
((vol*‘∪ ran 𝐹) ∈ ℝ ↔ (-∞ <
(vol*‘∪ ran 𝐹) ∧ (vol*‘∪ ran 𝐹) < +∞))) |
55 | 44, 54 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) ∈ ℝ ↔ (-∞ <
(vol*‘∪ ran 𝐹) ∧ (vol*‘∪ ran 𝐹) < +∞))) |
56 | 36 | elpw2 5049 |
. . . . . . . . . . . 12
⊢ (∪ ran 𝐹 ∈ 𝒫 ℝ ↔ ∪ ran 𝐹 ⊆ ℝ) |
57 | 42, 56 | sylibr 226 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ ran 𝐹 ∈ 𝒫 ℝ) |
58 | | simpl 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → 𝑥 = ∪ ran 𝐹) |
59 | 58 | sseq1d 3856 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (𝑥 ⊆ ℝ ↔ ∪ ran 𝐹 ⊆ ℝ)) |
60 | 58 | fveq2d 6436 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (vol*‘𝑥) = (vol*‘∪
ran 𝐹)) |
61 | 60 | eleq1d 2890 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘∪ ran 𝐹) ∈ ℝ)) |
62 | | simpll 785 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → 𝑥 = ∪ ran 𝐹) |
63 | 62 | ineq1d 4039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (𝑥 ∩ (𝐹‘𝑛)) = (∪ ran 𝐹 ∩ (𝐹‘𝑛))) |
64 | | fnfvelrn 6604 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐹 Fn ℕ ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ran 𝐹) |
65 | 21, 64 | sylan 577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ran 𝐹) |
66 | | elssuni 4688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐹‘𝑛) ∈ ran 𝐹 → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
68 | 67 | adantll 707 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
69 | | sseqin2 4043 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐹‘𝑛) ⊆ ∪ ran
𝐹 ↔ (∪ ran 𝐹 ∩ (𝐹‘𝑛)) = (𝐹‘𝑛)) |
70 | 68, 69 | sylib 210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (∪ ran 𝐹 ∩ (𝐹‘𝑛)) = (𝐹‘𝑛)) |
71 | 63, 70 | eqtrd 2860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (𝑥 ∩ (𝐹‘𝑛)) = (𝐹‘𝑛)) |
72 | 71 | fveq2d 6436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝑥 ∩ (𝐹‘𝑛))) = (vol*‘(𝐹‘𝑛))) |
73 | 13 | adantll 707 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) = (vol*‘(𝐹‘𝑛))) |
74 | 72, 73 | eqtr4d 2863 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝑥 ∩ (𝐹‘𝑛))) = (vol‘(𝐹‘𝑛))) |
75 | 74 | mpteq2dva 4966 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛)))) |
76 | 75 | adantrr 710 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛)))) |
77 | 76, 3, 26 | 3eqtr4g 2885 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → 𝐻 = 𝐺) |
78 | 77 | seqeq3d 13102 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → seq1( + , 𝐻) = seq1( + , 𝐺)) |
79 | 78, 25 | syl6eqr 2878 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → seq1( + , 𝐻) = 𝑆) |
80 | 79 | fveq1d 6434 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (seq1( + , 𝐻)‘𝑘) = (𝑆‘𝑘)) |
81 | | difeq1 3947 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = ∪
ran 𝐹 → (𝑥 ∖ ∪ ran 𝐹) = (∪ ran 𝐹 ∖ ∪ ran 𝐹)) |
82 | | difid 4177 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∪ ran 𝐹 ∖ ∪ ran
𝐹) =
∅ |
83 | 81, 82 | syl6eq 2876 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = ∪
ran 𝐹 → (𝑥 ∖ ∪ ran 𝐹) = ∅) |
84 | 83 | fveq2d 6436 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = ∪
ran 𝐹 →
(vol*‘(𝑥 ∖
∪ ran 𝐹)) = (vol*‘∅)) |
85 | | ovol0 23658 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(vol*‘∅) = 0 |
86 | 84, 85 | syl6eq 2876 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = ∪
ran 𝐹 →
(vol*‘(𝑥 ∖
∪ ran 𝐹)) = 0) |
87 | 86 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (vol*‘(𝑥 ∖ ∪ ran 𝐹)) = 0) |
88 | 80, 87 | oveq12d 6922 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) = ((𝑆‘𝑘) + 0)) |
89 | | nnuz 12004 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ℕ =
(ℤ≥‘1) |
90 | | 1zzd 11735 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 1 ∈
ℤ) |
91 | | 2fveq3 6437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑘 → (vol‘(𝐹‘𝑛)) = (vol‘(𝐹‘𝑘))) |
92 | | fvex 6445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(vol‘(𝐹‘𝑘)) ∈ V |
93 | 91, 26, 92 | fvmpt 6528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = (vol‘(𝐹‘𝑘))) |
94 | 93 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) = (vol‘(𝐹‘𝑘))) |
95 | | 2fveq3 6437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 = 𝑘 → (vol‘(𝐹‘𝑖)) = (vol‘(𝐹‘𝑘))) |
96 | 95 | eleq1d 2890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 = 𝑘 → ((vol‘(𝐹‘𝑖)) ∈ ℝ ↔ (vol‘(𝐹‘𝑘)) ∈ ℝ)) |
97 | 96 | rspccva 3524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((∀𝑖 ∈
ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ ∧ 𝑘 ∈ ℕ) → (vol‘(𝐹‘𝑘)) ∈ ℝ) |
98 | 14, 97 | sylan 577 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol‘(𝐹‘𝑘)) ∈ ℝ) |
99 | 94, 98 | eqeltrd 2905 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ) |
100 | 89, 90, 99 | serfre 13123 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ) |
101 | 25 | feq1i 6268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑆:ℕ⟶ℝ ↔
seq1( + , 𝐺):ℕ⟶ℝ) |
102 | 100, 101 | sylibr 226 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑆:ℕ⟶ℝ) |
103 | 102 | ffvelrnda 6607 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℝ) |
104 | 103 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (𝑆‘𝑘) ∈ ℝ) |
105 | 104 | recnd 10384 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (𝑆‘𝑘) ∈ ℂ) |
106 | 105 | addid1d 10554 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((𝑆‘𝑘) + 0) = (𝑆‘𝑘)) |
107 | 88, 106 | eqtrd 2860 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) = (𝑆‘𝑘)) |
108 | | fveq2 6432 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ∪
ran 𝐹 →
(vol*‘𝑥) =
(vol*‘∪ ran 𝐹)) |
109 | 108 | adantr 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (vol*‘𝑥) = (vol*‘∪ ran 𝐹)) |
110 | 107, 109 | breq12d 4885 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝑥) ↔ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
111 | 110 | expr 450 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (𝑘 ∈ ℕ → (((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝑥) ↔ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
112 | 111 | pm5.74d 265 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → ((𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝑥)) ↔ (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
113 | 61, 112 | imbi12d 336 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝑥))) ↔ ((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))))) |
114 | 59, 113 | imbi12d 336 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → ((𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( +
, 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥)))) ↔ (∪ ran
𝐹 ⊆ ℝ →
((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))))) |
115 | 114 | pm5.74da 840 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∪
ran 𝐹 → ((𝜑 → (𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( +
, 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥))))) ↔ (𝜑 → (∪ ran
𝐹 ⊆ ℝ →
((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))))))) |
116 | 1 | 3ad2ant1 1169 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → 𝐹:ℕ⟶dom
vol) |
117 | 2 | 3ad2ant1 1169 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
Disj 𝑖 ∈
ℕ (𝐹‘𝑖)) |
118 | | simp2 1173 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → 𝑥 ⊆
ℝ) |
119 | | simp3 1174 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘𝑥) ∈
ℝ) |
120 | 116, 117,
3, 118, 119 | voliunlem1 23715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((seq1(
+ , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥)) |
121 | 120 | 3exp1 1467 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( +
, 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥))))) |
122 | 115, 121 | vtoclg 3481 |
. . . . . . . . . . 11
⊢ (∪ ran 𝐹 ∈ 𝒫 ℝ → (𝜑 → (∪ ran 𝐹 ⊆ ℝ → ((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))))) |
123 | 57, 122 | mpcom 38 |
. . . . . . . . . 10
⊢ (𝜑 → (∪ ran 𝐹 ⊆ ℝ → ((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))))) |
124 | 42, 123 | mpd 15 |
. . . . . . . . 9
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
125 | 55, 124 | sylbird 252 |
. . . . . . . 8
⊢ (𝜑 → ((-∞ <
(vol*‘∪ ran 𝐹) ∧ (vol*‘∪ ran 𝐹) < +∞) → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
126 | 53, 125 | mpand 688 |
. . . . . . 7
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) < +∞ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
127 | | nltpnft 12282 |
. . . . . . . . 9
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* →
((vol*‘∪ ran 𝐹) = +∞ ↔ ¬ (vol*‘∪ ran 𝐹) < +∞)) |
128 | 44, 127 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) = +∞ ↔ ¬ (vol*‘∪ ran 𝐹) < +∞)) |
129 | | rexr 10401 |
. . . . . . . . . . 11
⊢ ((𝑆‘𝑘) ∈ ℝ → (𝑆‘𝑘) ∈
ℝ*) |
130 | | pnfge 12249 |
. . . . . . . . . . 11
⊢ ((𝑆‘𝑘) ∈ ℝ* → (𝑆‘𝑘) ≤ +∞) |
131 | 103, 129,
130 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ +∞) |
132 | 131 | ex 403 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ +∞)) |
133 | | breq2 4876 |
. . . . . . . . . 10
⊢
((vol*‘∪ ran 𝐹) = +∞ → ((𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹) ↔ (𝑆‘𝑘) ≤ +∞)) |
134 | 133 | imbi2d 332 |
. . . . . . . . 9
⊢
((vol*‘∪ ran 𝐹) = +∞ → ((𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)) ↔ (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ +∞))) |
135 | 132, 134 | syl5ibrcom 239 |
. . . . . . . 8
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) = +∞ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
136 | 128, 135 | sylbird 252 |
. . . . . . 7
⊢ (𝜑 → (¬ (vol*‘∪ ran 𝐹) < +∞ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
137 | 126, 136 | pm2.61d 172 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
138 | 137 | ralrimiv 3173 |
. . . . 5
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)) |
139 | 102 | ffnd 6278 |
. . . . . 6
⊢ (𝜑 → 𝑆 Fn ℕ) |
140 | | breq1 4875 |
. . . . . . 7
⊢ (𝑧 = (𝑆‘𝑘) → (𝑧 ≤ (vol*‘∪ ran 𝐹) ↔ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
141 | 140 | ralrn 6610 |
. . . . . 6
⊢ (𝑆 Fn ℕ →
(∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹) ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
142 | 139, 141 | syl 17 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹) ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
143 | 138, 142 | mpbird 249 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹)) |
144 | 102 | frnd 6284 |
. . . . . 6
⊢ (𝜑 → ran 𝑆 ⊆ ℝ) |
145 | | ressxr 10399 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
146 | 144, 145 | syl6ss 3838 |
. . . . 5
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
147 | | supxrleub 12443 |
. . . . 5
⊢ ((ran
𝑆 ⊆
ℝ* ∧ (vol*‘∪ ran 𝐹) ∈ ℝ*)
→ (sup(ran 𝑆,
ℝ*, < ) ≤ (vol*‘∪ ran
𝐹) ↔ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹))) |
148 | 146, 44, 147 | syl2anc 581 |
. . . 4
⊢ (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran 𝐹) ↔ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹))) |
149 | 143, 148 | mpbird 249 |
. . 3
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran 𝐹)) |
150 | | supxrcl 12432 |
. . . . 5
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
151 | 146, 150 | syl 17 |
. . . 4
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
152 | | xrletri3 12272 |
. . . 4
⊢
(((vol*‘∪ ran 𝐹) ∈ ℝ* ∧ sup(ran
𝑆, ℝ*,
< ) ∈ ℝ*) → ((vol*‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, < ) ↔
((vol*‘∪ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, < ) ∧ sup(ran
𝑆, ℝ*,
< ) ≤ (vol*‘∪ ran 𝐹)))) |
153 | 44, 151, 152 | syl2anc 581 |
. . 3
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, < ) ↔
((vol*‘∪ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, < ) ∧ sup(ran
𝑆, ℝ*,
< ) ≤ (vol*‘∪ ran 𝐹)))) |
154 | 33, 149, 153 | mpbir2and 706 |
. 2
⊢ (𝜑 → (vol*‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, <
)) |
155 | 6, 154 | eqtrd 2860 |
1
⊢ (𝜑 → (vol‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, <
)) |