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 24915 |
. . 3
⊢ (𝜑 → ∪ ran 𝐹 ∈ dom vol) |
5 | | mblvol 24894 |
. . 3
⊢ (∪ ran 𝐹 ∈ dom vol → (vol‘∪ ran 𝐹) = (vol*‘∪
ran 𝐹)) |
6 | 4, 5 | syl 17 |
. 2
⊢ (𝜑 → (vol‘∪ ran 𝐹) = (vol*‘∪
ran 𝐹)) |
7 | 1 | frnd 6676 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 ⊆ dom vol) |
8 | | mblss 24895 |
. . . . . . . 8
⊢ (𝑥 ∈ dom vol → 𝑥 ⊆
ℝ) |
9 | | reex 11142 |
. . . . . . . . 9
⊢ ℝ
∈ V |
10 | 9 | elpw2 5302 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 ℝ ↔
𝑥 ⊆
ℝ) |
11 | 8, 10 | sylibr 233 |
. . . . . . 7
⊢ (𝑥 ∈ dom vol → 𝑥 ∈ 𝒫
ℝ) |
12 | 11 | ssriv 3948 |
. . . . . 6
⊢ dom vol
⊆ 𝒫 ℝ |
13 | 7, 12 | sstrdi 3956 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ⊆ 𝒫 ℝ) |
14 | | sspwuni 5060 |
. . . . 5
⊢ (ran
𝐹 ⊆ 𝒫 ℝ
↔ ∪ ran 𝐹 ⊆ ℝ) |
15 | 13, 14 | sylib 217 |
. . . 4
⊢ (𝜑 → ∪ ran 𝐹 ⊆ ℝ) |
16 | | ovolcl 24842 |
. . . 4
⊢ (∪ ran 𝐹 ⊆ ℝ → (vol*‘∪ ran 𝐹) ∈
ℝ*) |
17 | 15, 16 | syl 17 |
. . 3
⊢ (𝜑 → (vol*‘∪ ran 𝐹) ∈
ℝ*) |
18 | | nnuz 12806 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
19 | | 1zzd 12534 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℤ) |
20 | | 2fveq3 6847 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (vol‘(𝐹‘𝑛)) = (vol‘(𝐹‘𝑘))) |
21 | | voliunlem3.2 |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛))) |
22 | | fvex 6855 |
. . . . . . . . . . 11
⊢
(vol‘(𝐹‘𝑘)) ∈ V |
23 | 20, 21, 22 | fvmpt 6948 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = (vol‘(𝐹‘𝑘))) |
24 | 23 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) = (vol‘(𝐹‘𝑘))) |
25 | | voliunlem3.4 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ) |
26 | | 2fveq3 6847 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (vol‘(𝐹‘𝑖)) = (vol‘(𝐹‘𝑘))) |
27 | 26 | eleq1d 2822 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → ((vol‘(𝐹‘𝑖)) ∈ ℝ ↔ (vol‘(𝐹‘𝑘)) ∈ ℝ)) |
28 | 27 | rspccva 3580 |
. . . . . . . . . 10
⊢
((∀𝑖 ∈
ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ ∧ 𝑘 ∈ ℕ) → (vol‘(𝐹‘𝑘)) ∈ ℝ) |
29 | 25, 28 | sylan 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol‘(𝐹‘𝑘)) ∈ ℝ) |
30 | 24, 29 | eqeltrd 2838 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ) |
31 | 18, 19, 30 | serfre 13937 |
. . . . . . 7
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ) |
32 | | voliunlem3.1 |
. . . . . . . 8
⊢ 𝑆 = seq1( + , 𝐺) |
33 | 32 | feq1i 6659 |
. . . . . . 7
⊢ (𝑆:ℕ⟶ℝ ↔
seq1( + , 𝐺):ℕ⟶ℝ) |
34 | 31, 33 | sylibr 233 |
. . . . . 6
⊢ (𝜑 → 𝑆:ℕ⟶ℝ) |
35 | 34 | frnd 6676 |
. . . . 5
⊢ (𝜑 → ran 𝑆 ⊆ ℝ) |
36 | | ressxr 11199 |
. . . . 5
⊢ ℝ
⊆ ℝ* |
37 | 35, 36 | sstrdi 3956 |
. . . 4
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
38 | | supxrcl 13234 |
. . . 4
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
39 | 37, 38 | syl 17 |
. . 3
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
40 | | eqid 2736 |
. . . . 5
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) |
41 | | eqid 2736 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛))) |
42 | 1 | ffvelcdmda 7035 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ dom vol) |
43 | | mblss 24895 |
. . . . . 6
⊢ ((𝐹‘𝑛) ∈ dom vol → (𝐹‘𝑛) ⊆ ℝ) |
44 | 42, 43 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ ℝ) |
45 | | mblvol 24894 |
. . . . . . 7
⊢ ((𝐹‘𝑛) ∈ dom vol → (vol‘(𝐹‘𝑛)) = (vol*‘(𝐹‘𝑛))) |
46 | 42, 45 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) = (vol*‘(𝐹‘𝑛))) |
47 | | 2fveq3 6847 |
. . . . . . . . 9
⊢ (𝑖 = 𝑛 → (vol‘(𝐹‘𝑖)) = (vol‘(𝐹‘𝑛))) |
48 | 47 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑖 = 𝑛 → ((vol‘(𝐹‘𝑖)) ∈ ℝ ↔ (vol‘(𝐹‘𝑛)) ∈ ℝ)) |
49 | 48 | rspccva 3580 |
. . . . . . 7
⊢
((∀𝑖 ∈
ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) ∈ ℝ) |
50 | 25, 49 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) ∈ ℝ) |
51 | 46, 50 | eqeltrrd 2839 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘(𝐹‘𝑛)) ∈ ℝ) |
52 | 40, 41, 44, 51 | ovoliun 24869 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ (𝐹‘𝑛)) ≤ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛)))), ℝ*, <
)) |
53 | 1 | ffnd 6669 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn ℕ) |
54 | | fniunfv 7194 |
. . . . . 6
⊢ (𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹) |
55 | 53, 54 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹) |
56 | 55 | fveq2d 6846 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ (𝐹‘𝑛)) = (vol*‘∪
ran 𝐹)) |
57 | 46 | mpteq2dva 5205 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛)))) |
58 | 21, 57 | eqtrid 2788 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛)))) |
59 | 58 | seqeq3d 13914 |
. . . . . . 7
⊢ (𝜑 → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛))))) |
60 | 32, 59 | eqtr2id 2789 |
. . . . . 6
⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) = 𝑆) |
61 | 60 | rneqd 5893 |
. . . . 5
⊢ (𝜑 → ran seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) = ran 𝑆) |
62 | 61 | supeq1d 9382 |
. . . 4
⊢ (𝜑 → sup(ran seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))), ℝ*, <
) = sup(ran 𝑆,
ℝ*, < )) |
63 | 52, 56, 62 | 3brtr3d 5136 |
. . 3
⊢ (𝜑 → (vol*‘∪ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, <
)) |
64 | | ovolge0 24845 |
. . . . . . . . . 10
⊢ (∪ ran 𝐹 ⊆ ℝ → 0 ≤
(vol*‘∪ ran 𝐹)) |
65 | 15, 64 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (vol*‘∪ ran 𝐹)) |
66 | | mnflt0 13046 |
. . . . . . . . . 10
⊢ -∞
< 0 |
67 | | mnfxr 11212 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
68 | | 0xr 11202 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
69 | | xrltletr 13076 |
. . . . . . . . . . 11
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ (vol*‘∪ ran 𝐹) ∈ ℝ*) →
((-∞ < 0 ∧ 0 ≤ (vol*‘∪ ran
𝐹)) → -∞ <
(vol*‘∪ ran 𝐹))) |
70 | 67, 68, 69 | mp3an12 1451 |
. . . . . . . . . 10
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* →
((-∞ < 0 ∧ 0 ≤ (vol*‘∪ ran
𝐹)) → -∞ <
(vol*‘∪ ran 𝐹))) |
71 | 66, 70 | mpani 694 |
. . . . . . . . 9
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* → (0 ≤
(vol*‘∪ ran 𝐹) → -∞ < (vol*‘∪ ran 𝐹))) |
72 | 17, 65, 71 | sylc 65 |
. . . . . . . 8
⊢ (𝜑 → -∞ <
(vol*‘∪ ran 𝐹)) |
73 | | xrrebnd 13087 |
. . . . . . . . . 10
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* →
((vol*‘∪ ran 𝐹) ∈ ℝ ↔ (-∞ <
(vol*‘∪ ran 𝐹) ∧ (vol*‘∪ ran 𝐹) < +∞))) |
74 | 17, 73 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) ∈ ℝ ↔ (-∞ <
(vol*‘∪ ran 𝐹) ∧ (vol*‘∪ ran 𝐹) < +∞))) |
75 | 9 | elpw2 5302 |
. . . . . . . . . . . 12
⊢ (∪ ran 𝐹 ∈ 𝒫 ℝ ↔ ∪ ran 𝐹 ⊆ ℝ) |
76 | 15, 75 | sylibr 233 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ ran 𝐹 ∈ 𝒫 ℝ) |
77 | | simpl 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → 𝑥 = ∪ ran 𝐹) |
78 | 77 | sseq1d 3975 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (𝑥 ⊆ ℝ ↔ ∪ ran 𝐹 ⊆ ℝ)) |
79 | 77 | fveq2d 6846 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (vol*‘𝑥) = (vol*‘∪
ran 𝐹)) |
80 | 79 | eleq1d 2822 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘∪ ran 𝐹) ∈ ℝ)) |
81 | | simpll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → 𝑥 = ∪ ran 𝐹) |
82 | 81 | ineq1d 4171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (𝑥 ∩ (𝐹‘𝑛)) = (∪ ran 𝐹 ∩ (𝐹‘𝑛))) |
83 | | fnfvelrn 7031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐹 Fn ℕ ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ran 𝐹) |
84 | 53, 83 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ran 𝐹) |
85 | | elssuni 4898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐹‘𝑛) ∈ ran 𝐹 → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
87 | 86 | adantll 712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
88 | | sseqin2 4175 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐹‘𝑛) ⊆ ∪ ran
𝐹 ↔ (∪ ran 𝐹 ∩ (𝐹‘𝑛)) = (𝐹‘𝑛)) |
89 | 87, 88 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (∪ ran 𝐹 ∩ (𝐹‘𝑛)) = (𝐹‘𝑛)) |
90 | 82, 89 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (𝑥 ∩ (𝐹‘𝑛)) = (𝐹‘𝑛)) |
91 | 90 | fveq2d 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝑥 ∩ (𝐹‘𝑛))) = (vol*‘(𝐹‘𝑛))) |
92 | 46 | adantll 712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) = (vol*‘(𝐹‘𝑛))) |
93 | 91, 92 | eqtr4d 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝑥 ∩ (𝐹‘𝑛))) = (vol‘(𝐹‘𝑛))) |
94 | 93 | mpteq2dva 5205 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛)))) |
95 | 94 | adantrr 715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛)))) |
96 | 95, 3, 21 | 3eqtr4g 2801 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → 𝐻 = 𝐺) |
97 | 96 | seqeq3d 13914 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → seq1( + , 𝐻) = seq1( + , 𝐺)) |
98 | 97, 32 | eqtr4di 2794 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → seq1( + , 𝐻) = 𝑆) |
99 | 98 | fveq1d 6844 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (seq1( + , 𝐻)‘𝑘) = (𝑆‘𝑘)) |
100 | | difeq1 4075 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = ∪
ran 𝐹 → (𝑥 ∖ ∪ ran 𝐹) = (∪ ran 𝐹 ∖ ∪ ran 𝐹)) |
101 | | difid 4330 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∪ ran 𝐹 ∖ ∪ ran
𝐹) =
∅ |
102 | 100, 101 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = ∪
ran 𝐹 → (𝑥 ∖ ∪ ran 𝐹) = ∅) |
103 | 102 | fveq2d 6846 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = ∪
ran 𝐹 →
(vol*‘(𝑥 ∖
∪ ran 𝐹)) = (vol*‘∅)) |
104 | | ovol0 24857 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(vol*‘∅) = 0 |
105 | 103, 104 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = ∪
ran 𝐹 →
(vol*‘(𝑥 ∖
∪ ran 𝐹)) = 0) |
106 | 105 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (vol*‘(𝑥 ∖ ∪ ran 𝐹)) = 0) |
107 | 99, 106 | oveq12d 7375 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) = ((𝑆‘𝑘) + 0)) |
108 | 34 | ffvelcdmda 7035 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℝ) |
109 | 108 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (𝑆‘𝑘) ∈ ℝ) |
110 | 109 | recnd 11183 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (𝑆‘𝑘) ∈ ℂ) |
111 | 110 | addid1d 11355 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((𝑆‘𝑘) + 0) = (𝑆‘𝑘)) |
112 | 107, 111 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) = (𝑆‘𝑘)) |
113 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ∪
ran 𝐹 →
(vol*‘𝑥) =
(vol*‘∪ ran 𝐹)) |
114 | 113 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (vol*‘𝑥) = (vol*‘∪ ran 𝐹)) |
115 | 112, 114 | breq12d 5118 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝑥) ↔ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
116 | 115 | expr 457 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (𝑘 ∈ ℕ → (((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝑥) ↔ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
117 | 116 | pm5.74d 272 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → ((𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝑥)) ↔ (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
118 | 80, 117 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝑥))) ↔ ((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))))) |
119 | 78, 118 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → ((𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( +
, 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥)))) ↔ (∪ ran
𝐹 ⊆ ℝ →
((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))))) |
120 | 119 | pm5.74da 802 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∪
ran 𝐹 → ((𝜑 → (𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( +
, 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥))))) ↔ (𝜑 → (∪ ran
𝐹 ⊆ ℝ →
((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))))))) |
121 | 1 | 3ad2ant1 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → 𝐹:ℕ⟶dom
vol) |
122 | 2 | 3ad2ant1 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
Disj 𝑖 ∈
ℕ (𝐹‘𝑖)) |
123 | | simp2 1137 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → 𝑥 ⊆
ℝ) |
124 | | simp3 1138 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘𝑥) ∈
ℝ) |
125 | 121, 122,
3, 123, 124 | voliunlem1 24914 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((seq1(
+ , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥)) |
126 | 125 | 3exp1 1352 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( +
, 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥))))) |
127 | 120, 126 | vtoclg 3525 |
. . . . . . . . . . 11
⊢ (∪ ran 𝐹 ∈ 𝒫 ℝ → (𝜑 → (∪ ran 𝐹 ⊆ ℝ → ((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))))) |
128 | 76, 127 | mpcom 38 |
. . . . . . . . . 10
⊢ (𝜑 → (∪ ran 𝐹 ⊆ ℝ → ((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))))) |
129 | 15, 128 | mpd 15 |
. . . . . . . . 9
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
130 | 74, 129 | sylbird 259 |
. . . . . . . 8
⊢ (𝜑 → ((-∞ <
(vol*‘∪ ran 𝐹) ∧ (vol*‘∪ ran 𝐹) < +∞) → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
131 | 72, 130 | mpand 693 |
. . . . . . 7
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) < +∞ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
132 | | nltpnft 13083 |
. . . . . . . . 9
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* →
((vol*‘∪ ran 𝐹) = +∞ ↔ ¬ (vol*‘∪ ran 𝐹) < +∞)) |
133 | 17, 132 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) = +∞ ↔ ¬ (vol*‘∪ ran 𝐹) < +∞)) |
134 | | rexr 11201 |
. . . . . . . . . . 11
⊢ ((𝑆‘𝑘) ∈ ℝ → (𝑆‘𝑘) ∈
ℝ*) |
135 | | pnfge 13051 |
. . . . . . . . . . 11
⊢ ((𝑆‘𝑘) ∈ ℝ* → (𝑆‘𝑘) ≤ +∞) |
136 | 108, 134,
135 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ +∞) |
137 | 136 | ex 413 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ +∞)) |
138 | | breq2 5109 |
. . . . . . . . . 10
⊢
((vol*‘∪ ran 𝐹) = +∞ → ((𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹) ↔ (𝑆‘𝑘) ≤ +∞)) |
139 | 138 | imbi2d 340 |
. . . . . . . . 9
⊢
((vol*‘∪ ran 𝐹) = +∞ → ((𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)) ↔ (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ +∞))) |
140 | 137, 139 | syl5ibrcom 246 |
. . . . . . . 8
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) = +∞ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
141 | 133, 140 | sylbird 259 |
. . . . . . 7
⊢ (𝜑 → (¬ (vol*‘∪ ran 𝐹) < +∞ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
142 | 131, 141 | pm2.61d 179 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
143 | 142 | ralrimiv 3142 |
. . . . 5
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)) |
144 | 34 | ffnd 6669 |
. . . . . 6
⊢ (𝜑 → 𝑆 Fn ℕ) |
145 | | breq1 5108 |
. . . . . . 7
⊢ (𝑧 = (𝑆‘𝑘) → (𝑧 ≤ (vol*‘∪ ran 𝐹) ↔ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
146 | 145 | ralrn 7038 |
. . . . . 6
⊢ (𝑆 Fn ℕ →
(∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹) ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
147 | 144, 146 | syl 17 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹) ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
148 | 143, 147 | mpbird 256 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹)) |
149 | | supxrleub 13245 |
. . . . 5
⊢ ((ran
𝑆 ⊆
ℝ* ∧ (vol*‘∪ ran 𝐹) ∈ ℝ*)
→ (sup(ran 𝑆,
ℝ*, < ) ≤ (vol*‘∪ ran
𝐹) ↔ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹))) |
150 | 37, 17, 149 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran 𝐹) ↔ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹))) |
151 | 148, 150 | mpbird 256 |
. . 3
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran 𝐹)) |
152 | 17, 39, 63, 151 | xrletrid 13074 |
. 2
⊢ (𝜑 → (vol*‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, <
)) |
153 | 6, 152 | eqtrd 2776 |
1
⊢ (𝜑 → (vol‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, <
)) |