| 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 25586 |
. . 3
⊢ (𝜑 → ∪ ran 𝐹 ∈ dom vol) |
| 5 | | mblvol 25565 |
. . 3
⊢ (∪ ran 𝐹 ∈ dom vol → (vol‘∪ ran 𝐹) = (vol*‘∪
ran 𝐹)) |
| 6 | 4, 5 | syl 17 |
. 2
⊢ (𝜑 → (vol‘∪ ran 𝐹) = (vol*‘∪
ran 𝐹)) |
| 7 | 1 | frnd 6744 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 ⊆ dom vol) |
| 8 | | mblss 25566 |
. . . . . . . 8
⊢ (𝑥 ∈ dom vol → 𝑥 ⊆
ℝ) |
| 9 | | reex 11246 |
. . . . . . . . 9
⊢ ℝ
∈ V |
| 10 | 9 | elpw2 5334 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 ℝ ↔
𝑥 ⊆
ℝ) |
| 11 | 8, 10 | sylibr 234 |
. . . . . . 7
⊢ (𝑥 ∈ dom vol → 𝑥 ∈ 𝒫
ℝ) |
| 12 | 11 | ssriv 3987 |
. . . . . 6
⊢ dom vol
⊆ 𝒫 ℝ |
| 13 | 7, 12 | sstrdi 3996 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ⊆ 𝒫 ℝ) |
| 14 | | sspwuni 5100 |
. . . . 5
⊢ (ran
𝐹 ⊆ 𝒫 ℝ
↔ ∪ ran 𝐹 ⊆ ℝ) |
| 15 | 13, 14 | sylib 218 |
. . . 4
⊢ (𝜑 → ∪ ran 𝐹 ⊆ ℝ) |
| 16 | | ovolcl 25513 |
. . . 4
⊢ (∪ ran 𝐹 ⊆ ℝ → (vol*‘∪ ran 𝐹) ∈
ℝ*) |
| 17 | 15, 16 | syl 17 |
. . 3
⊢ (𝜑 → (vol*‘∪ ran 𝐹) ∈
ℝ*) |
| 18 | | nnuz 12921 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
| 19 | | 1zzd 12648 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℤ) |
| 20 | | 2fveq3 6911 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (vol‘(𝐹‘𝑛)) = (vol‘(𝐹‘𝑘))) |
| 21 | | voliunlem3.2 |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛))) |
| 22 | | fvex 6919 |
. . . . . . . . . . 11
⊢
(vol‘(𝐹‘𝑘)) ∈ V |
| 23 | 20, 21, 22 | fvmpt 7016 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = (vol‘(𝐹‘𝑘))) |
| 24 | 23 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) = (vol‘(𝐹‘𝑘))) |
| 25 | | voliunlem3.4 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ) |
| 26 | | 2fveq3 6911 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (vol‘(𝐹‘𝑖)) = (vol‘(𝐹‘𝑘))) |
| 27 | 26 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → ((vol‘(𝐹‘𝑖)) ∈ ℝ ↔ (vol‘(𝐹‘𝑘)) ∈ ℝ)) |
| 28 | 27 | rspccva 3621 |
. . . . . . . . . 10
⊢
((∀𝑖 ∈
ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ ∧ 𝑘 ∈ ℕ) → (vol‘(𝐹‘𝑘)) ∈ ℝ) |
| 29 | 25, 28 | sylan 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol‘(𝐹‘𝑘)) ∈ ℝ) |
| 30 | 24, 29 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ) |
| 31 | 18, 19, 30 | serfre 14072 |
. . . . . . 7
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ) |
| 32 | | voliunlem3.1 |
. . . . . . . 8
⊢ 𝑆 = seq1( + , 𝐺) |
| 33 | 32 | feq1i 6727 |
. . . . . . 7
⊢ (𝑆:ℕ⟶ℝ ↔
seq1( + , 𝐺):ℕ⟶ℝ) |
| 34 | 31, 33 | sylibr 234 |
. . . . . 6
⊢ (𝜑 → 𝑆:ℕ⟶ℝ) |
| 35 | 34 | frnd 6744 |
. . . . 5
⊢ (𝜑 → ran 𝑆 ⊆ ℝ) |
| 36 | | ressxr 11305 |
. . . . 5
⊢ ℝ
⊆ ℝ* |
| 37 | 35, 36 | sstrdi 3996 |
. . . 4
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
| 38 | | supxrcl 13357 |
. . . 4
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
| 39 | 37, 38 | syl 17 |
. . 3
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
| 40 | | eqid 2737 |
. . . . 5
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) |
| 41 | | eqid 2737 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛))) |
| 42 | 1 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ dom vol) |
| 43 | | mblss 25566 |
. . . . . 6
⊢ ((𝐹‘𝑛) ∈ dom vol → (𝐹‘𝑛) ⊆ ℝ) |
| 44 | 42, 43 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ ℝ) |
| 45 | | mblvol 25565 |
. . . . . . 7
⊢ ((𝐹‘𝑛) ∈ dom vol → (vol‘(𝐹‘𝑛)) = (vol*‘(𝐹‘𝑛))) |
| 46 | 42, 45 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) = (vol*‘(𝐹‘𝑛))) |
| 47 | | 2fveq3 6911 |
. . . . . . . . 9
⊢ (𝑖 = 𝑛 → (vol‘(𝐹‘𝑖)) = (vol‘(𝐹‘𝑛))) |
| 48 | 47 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑖 = 𝑛 → ((vol‘(𝐹‘𝑖)) ∈ ℝ ↔ (vol‘(𝐹‘𝑛)) ∈ ℝ)) |
| 49 | 48 | rspccva 3621 |
. . . . . . 7
⊢
((∀𝑖 ∈
ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) ∈ ℝ) |
| 50 | 25, 49 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) ∈ ℝ) |
| 51 | 46, 50 | eqeltrrd 2842 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘(𝐹‘𝑛)) ∈ ℝ) |
| 52 | 40, 41, 44, 51 | ovoliun 25540 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ (𝐹‘𝑛)) ≤ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛)))), ℝ*, <
)) |
| 53 | 1 | ffnd 6737 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn ℕ) |
| 54 | | fniunfv 7267 |
. . . . . 6
⊢ (𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹) |
| 55 | 53, 54 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹) |
| 56 | 55 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ (𝐹‘𝑛)) = (vol*‘∪
ran 𝐹)) |
| 57 | 46 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛)))) |
| 58 | 21, 57 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛)))) |
| 59 | 58 | seqeq3d 14050 |
. . . . . . 7
⊢ (𝜑 → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛))))) |
| 60 | 32, 59 | eqtr2id 2790 |
. . . . . 6
⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) = 𝑆) |
| 61 | 60 | rneqd 5949 |
. . . . 5
⊢ (𝜑 → ran seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) = ran 𝑆) |
| 62 | 61 | supeq1d 9486 |
. . . 4
⊢ (𝜑 → sup(ran seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))), ℝ*, <
) = sup(ran 𝑆,
ℝ*, < )) |
| 63 | 52, 56, 62 | 3brtr3d 5174 |
. . 3
⊢ (𝜑 → (vol*‘∪ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, <
)) |
| 64 | | ovolge0 25516 |
. . . . . . . . . 10
⊢ (∪ ran 𝐹 ⊆ ℝ → 0 ≤
(vol*‘∪ ran 𝐹)) |
| 65 | 15, 64 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (vol*‘∪ ran 𝐹)) |
| 66 | | mnflt0 13167 |
. . . . . . . . . 10
⊢ -∞
< 0 |
| 67 | | mnfxr 11318 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
| 68 | | 0xr 11308 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
| 69 | | xrltletr 13199 |
. . . . . . . . . . 11
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ (vol*‘∪ ran 𝐹) ∈ ℝ*) →
((-∞ < 0 ∧ 0 ≤ (vol*‘∪ ran
𝐹)) → -∞ <
(vol*‘∪ ran 𝐹))) |
| 70 | 67, 68, 69 | mp3an12 1453 |
. . . . . . . . . 10
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* →
((-∞ < 0 ∧ 0 ≤ (vol*‘∪ ran
𝐹)) → -∞ <
(vol*‘∪ ran 𝐹))) |
| 71 | 66, 70 | mpani 696 |
. . . . . . . . 9
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* → (0 ≤
(vol*‘∪ ran 𝐹) → -∞ < (vol*‘∪ ran 𝐹))) |
| 72 | 17, 65, 71 | sylc 65 |
. . . . . . . 8
⊢ (𝜑 → -∞ <
(vol*‘∪ ran 𝐹)) |
| 73 | | xrrebnd 13210 |
. . . . . . . . . 10
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* →
((vol*‘∪ ran 𝐹) ∈ ℝ ↔ (-∞ <
(vol*‘∪ ran 𝐹) ∧ (vol*‘∪ ran 𝐹) < +∞))) |
| 74 | 17, 73 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) ∈ ℝ ↔ (-∞ <
(vol*‘∪ ran 𝐹) ∧ (vol*‘∪ ran 𝐹) < +∞))) |
| 75 | 9 | elpw2 5334 |
. . . . . . . . . . . 12
⊢ (∪ ran 𝐹 ∈ 𝒫 ℝ ↔ ∪ ran 𝐹 ⊆ ℝ) |
| 76 | 15, 75 | sylibr 234 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ ran 𝐹 ∈ 𝒫 ℝ) |
| 77 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → 𝑥 = ∪ ran 𝐹) |
| 78 | 77 | sseq1d 4015 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (𝑥 ⊆ ℝ ↔ ∪ ran 𝐹 ⊆ ℝ)) |
| 79 | 77 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (vol*‘𝑥) = (vol*‘∪
ran 𝐹)) |
| 80 | 79 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘∪ ran 𝐹) ∈ ℝ)) |
| 81 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → 𝑥 = ∪ ran 𝐹) |
| 82 | 81 | ineq1d 4219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (𝑥 ∩ (𝐹‘𝑛)) = (∪ ran 𝐹 ∩ (𝐹‘𝑛))) |
| 83 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐹 Fn ℕ ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ran 𝐹) |
| 84 | 53, 83 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ran 𝐹) |
| 85 | | elssuni 4937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐹‘𝑛) ∈ ran 𝐹 → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
| 86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
| 87 | 86 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
| 88 | | sseqin2 4223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐹‘𝑛) ⊆ ∪ ran
𝐹 ↔ (∪ ran 𝐹 ∩ (𝐹‘𝑛)) = (𝐹‘𝑛)) |
| 89 | 87, 88 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (∪ ran 𝐹 ∩ (𝐹‘𝑛)) = (𝐹‘𝑛)) |
| 90 | 82, 89 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (𝑥 ∩ (𝐹‘𝑛)) = (𝐹‘𝑛)) |
| 91 | 90 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝑥 ∩ (𝐹‘𝑛))) = (vol*‘(𝐹‘𝑛))) |
| 92 | 46 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) = (vol*‘(𝐹‘𝑛))) |
| 93 | 91, 92 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝑥 ∩ (𝐹‘𝑛))) = (vol‘(𝐹‘𝑛))) |
| 94 | 93 | mpteq2dva 5242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛)))) |
| 95 | 94 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛)))) |
| 96 | 95, 3, 21 | 3eqtr4g 2802 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → 𝐻 = 𝐺) |
| 97 | 96 | seqeq3d 14050 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → seq1( + , 𝐻) = seq1( + , 𝐺)) |
| 98 | 97, 32 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → seq1( + , 𝐻) = 𝑆) |
| 99 | 98 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (seq1( + , 𝐻)‘𝑘) = (𝑆‘𝑘)) |
| 100 | | difeq1 4119 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = ∪
ran 𝐹 → (𝑥 ∖ ∪ ran 𝐹) = (∪ ran 𝐹 ∖ ∪ ran 𝐹)) |
| 101 | | difid 4376 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∪ ran 𝐹 ∖ ∪ ran
𝐹) =
∅ |
| 102 | 100, 101 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = ∪
ran 𝐹 → (𝑥 ∖ ∪ ran 𝐹) = ∅) |
| 103 | 102 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = ∪
ran 𝐹 →
(vol*‘(𝑥 ∖
∪ ran 𝐹)) = (vol*‘∅)) |
| 104 | | ovol0 25528 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(vol*‘∅) = 0 |
| 105 | 103, 104 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = ∪
ran 𝐹 →
(vol*‘(𝑥 ∖
∪ ran 𝐹)) = 0) |
| 106 | 105 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (vol*‘(𝑥 ∖ ∪ ran 𝐹)) = 0) |
| 107 | 99, 106 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) = ((𝑆‘𝑘) + 0)) |
| 108 | 34 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℝ) |
| 109 | 108 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (𝑆‘𝑘) ∈ ℝ) |
| 110 | 109 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (𝑆‘𝑘) ∈ ℂ) |
| 111 | 110 | addridd 11461 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((𝑆‘𝑘) + 0) = (𝑆‘𝑘)) |
| 112 | 107, 111 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) = (𝑆‘𝑘)) |
| 113 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ∪
ran 𝐹 →
(vol*‘𝑥) =
(vol*‘∪ ran 𝐹)) |
| 114 | 113 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (vol*‘𝑥) = (vol*‘∪ ran 𝐹)) |
| 115 | 112, 114 | breq12d 5156 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝑥) ↔ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
| 116 | 115 | expr 456 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (𝑘 ∈ ℕ → (((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝑥) ↔ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
| 117 | 116 | pm5.74d 273 |
. . . . . . . . . . . . . . 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 804 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∪
ran 𝐹 → ((𝜑 → (𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( +
, 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥))))) ↔ (𝜑 → (∪ ran
𝐹 ⊆ ℝ →
((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))))))) |
| 121 | 1 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → 𝐹:ℕ⟶dom
vol) |
| 122 | 2 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
Disj 𝑖 ∈
ℕ (𝐹‘𝑖)) |
| 123 | | simp2 1138 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → 𝑥 ⊆
ℝ) |
| 124 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘𝑥) ∈
ℝ) |
| 125 | 121, 122,
3, 123, 124 | voliunlem1 25585 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((seq1(
+ , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥)) |
| 126 | 125 | 3exp1 1353 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( +
, 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥))))) |
| 127 | 120, 126 | vtoclg 3554 |
. . . . . . . . . . 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 260 |
. . . . . . . 8
⊢ (𝜑 → ((-∞ <
(vol*‘∪ ran 𝐹) ∧ (vol*‘∪ ran 𝐹) < +∞) → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
| 131 | 72, 130 | mpand 695 |
. . . . . . 7
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) < +∞ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
| 132 | | nltpnft 13206 |
. . . . . . . . 9
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* →
((vol*‘∪ ran 𝐹) = +∞ ↔ ¬ (vol*‘∪ ran 𝐹) < +∞)) |
| 133 | 17, 132 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) = +∞ ↔ ¬ (vol*‘∪ ran 𝐹) < +∞)) |
| 134 | | rexr 11307 |
. . . . . . . . . . 11
⊢ ((𝑆‘𝑘) ∈ ℝ → (𝑆‘𝑘) ∈
ℝ*) |
| 135 | | pnfge 13172 |
. . . . . . . . . . 11
⊢ ((𝑆‘𝑘) ∈ ℝ* → (𝑆‘𝑘) ≤ +∞) |
| 136 | 108, 134,
135 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ +∞) |
| 137 | 136 | ex 412 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ +∞)) |
| 138 | | breq2 5147 |
. . . . . . . . . 10
⊢
((vol*‘∪ ran 𝐹) = +∞ → ((𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹) ↔ (𝑆‘𝑘) ≤ +∞)) |
| 139 | 138 | imbi2d 340 |
. . . . . . . . 9
⊢
((vol*‘∪ ran 𝐹) = +∞ → ((𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)) ↔ (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ +∞))) |
| 140 | 137, 139 | syl5ibrcom 247 |
. . . . . . . 8
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) = +∞ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
| 141 | 133, 140 | sylbird 260 |
. . . . . . 7
⊢ (𝜑 → (¬ (vol*‘∪ ran 𝐹) < +∞ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
| 142 | 131, 141 | pm2.61d 179 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
| 143 | 142 | ralrimiv 3145 |
. . . . 5
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)) |
| 144 | 34 | ffnd 6737 |
. . . . . 6
⊢ (𝜑 → 𝑆 Fn ℕ) |
| 145 | | breq1 5146 |
. . . . . . 7
⊢ (𝑧 = (𝑆‘𝑘) → (𝑧 ≤ (vol*‘∪ ran 𝐹) ↔ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
| 146 | 145 | ralrn 7108 |
. . . . . 6
⊢ (𝑆 Fn ℕ →
(∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹) ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
| 147 | 144, 146 | syl 17 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹) ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
| 148 | 143, 147 | mpbird 257 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹)) |
| 149 | | supxrleub 13368 |
. . . . 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 257 |
. . 3
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran 𝐹)) |
| 152 | 17, 39, 63, 151 | xrletrid 13197 |
. 2
⊢ (𝜑 → (vol*‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, <
)) |
| 153 | 6, 152 | eqtrd 2777 |
1
⊢ (𝜑 → (vol‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, <
)) |