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 23126 |
. . 3
⊢ (𝜑 → ∪ ran 𝐹 ∈ dom vol) |
5 | | mblvol 23105 |
. . 3
⊢ (∪ ran 𝐹 ∈ dom vol → (vol‘∪ ran 𝐹) = (vol*‘∪
ran 𝐹)) |
6 | 4, 5 | syl 17 |
. 2
⊢ (𝜑 → (vol‘∪ ran 𝐹) = (vol*‘∪
ran 𝐹)) |
7 | | eqid 2610 |
. . . . 5
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) |
8 | | eqid 2610 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛))) |
9 | 1 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ dom vol) |
10 | | mblss 23106 |
. . . . . 6
⊢ ((𝐹‘𝑛) ∈ dom vol → (𝐹‘𝑛) ⊆ ℝ) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ ℝ) |
12 | | mblvol 23105 |
. . . . . . 7
⊢ ((𝐹‘𝑛) ∈ dom vol → (vol‘(𝐹‘𝑛)) = (vol*‘(𝐹‘𝑛))) |
13 | 9, 12 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) = (vol*‘(𝐹‘𝑛))) |
14 | | voliunlem3.4 |
. . . . . . 7
⊢ (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ) |
15 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑛 → (𝐹‘𝑖) = (𝐹‘𝑛)) |
16 | 15 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑖 = 𝑛 → (vol‘(𝐹‘𝑖)) = (vol‘(𝐹‘𝑛))) |
17 | 16 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑖 = 𝑛 → ((vol‘(𝐹‘𝑖)) ∈ ℝ ↔ (vol‘(𝐹‘𝑛)) ∈ ℝ)) |
18 | 17 | rspccva 3281 |
. . . . . . 7
⊢
((∀𝑖 ∈
ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) ∈ ℝ) |
19 | 14, 18 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) ∈ ℝ) |
20 | 13, 19 | eqeltrrd 2689 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘(𝐹‘𝑛)) ∈ ℝ) |
21 | 7, 8, 11, 20 | ovoliun 23080 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ (𝐹‘𝑛)) ≤ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛)))), ℝ*, <
)) |
22 | | ffn 5958 |
. . . . . . 7
⊢ (𝐹:ℕ⟶dom vol →
𝐹 Fn
ℕ) |
23 | 1, 22 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn ℕ) |
24 | | fniunfv 6409 |
. . . . . 6
⊢ (𝐹 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹) |
25 | 23, 24 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ ran 𝐹) |
26 | 25 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ (𝐹‘𝑛)) = (vol*‘∪
ran 𝐹)) |
27 | | voliunlem3.1 |
. . . . . . 7
⊢ 𝑆 = seq1( + , 𝐺) |
28 | | voliunlem3.2 |
. . . . . . . . 9
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛))) |
29 | 13 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛)))) |
30 | 28, 29 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹‘𝑛)))) |
31 | 30 | seqeq3d 12671 |
. . . . . . 7
⊢ (𝜑 → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛))))) |
32 | 27, 31 | syl5req 2657 |
. . . . . 6
⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) = 𝑆) |
33 | 32 | rneqd 5274 |
. . . . 5
⊢ (𝜑 → ran seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))) = ran 𝑆) |
34 | 33 | supeq1d 8235 |
. . . 4
⊢ (𝜑 → sup(ran seq1( + , (𝑛 ∈ ℕ ↦
(vol*‘(𝐹‘𝑛)))), ℝ*, <
) = sup(ran 𝑆,
ℝ*, < )) |
35 | 21, 26, 34 | 3brtr3d 4614 |
. . 3
⊢ (𝜑 → (vol*‘∪ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, <
)) |
36 | | frn 5966 |
. . . . . . . . . . . . 13
⊢ (𝐹:ℕ⟶dom vol →
ran 𝐹 ⊆ dom
vol) |
37 | 1, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝐹 ⊆ dom vol) |
38 | | mblss 23106 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ dom vol → 𝑥 ⊆
ℝ) |
39 | | reex 9906 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
40 | 39 | elpw2 4755 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝒫 ℝ ↔
𝑥 ⊆
ℝ) |
41 | 38, 40 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ dom vol → 𝑥 ∈ 𝒫
ℝ) |
42 | 41 | ssriv 3572 |
. . . . . . . . . . . 12
⊢ dom vol
⊆ 𝒫 ℝ |
43 | 37, 42 | syl6ss 3580 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐹 ⊆ 𝒫 ℝ) |
44 | | sspwuni 4547 |
. . . . . . . . . . 11
⊢ (ran
𝐹 ⊆ 𝒫 ℝ
↔ ∪ ran 𝐹 ⊆ ℝ) |
45 | 43, 44 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ ran 𝐹 ⊆ ℝ) |
46 | | ovolcl 23053 |
. . . . . . . . . 10
⊢ (∪ ran 𝐹 ⊆ ℝ → (vol*‘∪ ran 𝐹) ∈
ℝ*) |
47 | 45, 46 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (vol*‘∪ ran 𝐹) ∈
ℝ*) |
48 | | ovolge0 23056 |
. . . . . . . . . 10
⊢ (∪ ran 𝐹 ⊆ ℝ → 0 ≤
(vol*‘∪ ran 𝐹)) |
49 | 45, 48 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (vol*‘∪ ran 𝐹)) |
50 | | mnflt0 11835 |
. . . . . . . . . 10
⊢ -∞
< 0 |
51 | | mnfxr 9975 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
52 | | 0xr 9965 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
53 | | xrltletr 11864 |
. . . . . . . . . . 11
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ (vol*‘∪ ran 𝐹) ∈ ℝ*) →
((-∞ < 0 ∧ 0 ≤ (vol*‘∪ ran
𝐹)) → -∞ <
(vol*‘∪ ran 𝐹))) |
54 | 51, 52, 53 | mp3an12 1406 |
. . . . . . . . . 10
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* →
((-∞ < 0 ∧ 0 ≤ (vol*‘∪ ran
𝐹)) → -∞ <
(vol*‘∪ ran 𝐹))) |
55 | 50, 54 | mpani 708 |
. . . . . . . . 9
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* → (0 ≤
(vol*‘∪ ran 𝐹) → -∞ < (vol*‘∪ ran 𝐹))) |
56 | 47, 49, 55 | sylc 63 |
. . . . . . . 8
⊢ (𝜑 → -∞ <
(vol*‘∪ ran 𝐹)) |
57 | | xrrebnd 11873 |
. . . . . . . . . 10
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* →
((vol*‘∪ ran 𝐹) ∈ ℝ ↔ (-∞ <
(vol*‘∪ ran 𝐹) ∧ (vol*‘∪ ran 𝐹) < +∞))) |
58 | 47, 57 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) ∈ ℝ ↔ (-∞ <
(vol*‘∪ ran 𝐹) ∧ (vol*‘∪ ran 𝐹) < +∞))) |
59 | 39 | elpw2 4755 |
. . . . . . . . . . . 12
⊢ (∪ ran 𝐹 ∈ 𝒫 ℝ ↔ ∪ ran 𝐹 ⊆ ℝ) |
60 | 45, 59 | sylibr 223 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ ran 𝐹 ∈ 𝒫 ℝ) |
61 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → 𝑥 = ∪ ran 𝐹) |
62 | 61 | sseq1d 3595 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (𝑥 ⊆ ℝ ↔ ∪ ran 𝐹 ⊆ ℝ)) |
63 | 61 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (vol*‘𝑥) = (vol*‘∪
ran 𝐹)) |
64 | 63 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘∪ ran 𝐹) ∈ ℝ)) |
65 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → 𝑥 = ∪ ran 𝐹) |
66 | 65 | ineq1d 3775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (𝑥 ∩ (𝐹‘𝑛)) = (∪ ran 𝐹 ∩ (𝐹‘𝑛))) |
67 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐹 Fn ℕ ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ran 𝐹) |
68 | 23, 67 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ran 𝐹) |
69 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐹‘𝑛) ∈ ran 𝐹 → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
71 | 70 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
72 | | sseqin2 3779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐹‘𝑛) ⊆ ∪ ran
𝐹 ↔ (∪ ran 𝐹 ∩ (𝐹‘𝑛)) = (𝐹‘𝑛)) |
73 | 71, 72 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (∪ ran 𝐹 ∩ (𝐹‘𝑛)) = (𝐹‘𝑛)) |
74 | 66, 73 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (𝑥 ∩ (𝐹‘𝑛)) = (𝐹‘𝑛)) |
75 | 74 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝑥 ∩ (𝐹‘𝑛))) = (vol*‘(𝐹‘𝑛))) |
76 | 13 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹‘𝑛)) = (vol*‘(𝐹‘𝑛))) |
77 | 75, 76 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 = ∪
ran 𝐹 ∧ 𝜑) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝑥 ∩ (𝐹‘𝑛))) = (vol‘(𝐹‘𝑛))) |
78 | 77 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛)))) |
79 | 78 | adantrr 749 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛)))) |
80 | 79, 3, 28 | 3eqtr4g 2669 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → 𝐻 = 𝐺) |
81 | 80 | seqeq3d 12671 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → seq1( + , 𝐻) = seq1( + , 𝐺)) |
82 | 81, 27 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → seq1( + , 𝐻) = 𝑆) |
83 | 82 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (seq1( + , 𝐻)‘𝑘) = (𝑆‘𝑘)) |
84 | | difeq1 3683 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = ∪
ran 𝐹 → (𝑥 ∖ ∪ ran 𝐹) = (∪ ran 𝐹 ∖ ∪ ran 𝐹)) |
85 | | difid 3902 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∪ ran 𝐹 ∖ ∪ ran
𝐹) =
∅ |
86 | 84, 85 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = ∪
ran 𝐹 → (𝑥 ∖ ∪ ran 𝐹) = ∅) |
87 | 86 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = ∪
ran 𝐹 →
(vol*‘(𝑥 ∖
∪ ran 𝐹)) = (vol*‘∅)) |
88 | | ovol0 23068 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(vol*‘∅) = 0 |
89 | 87, 88 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = ∪
ran 𝐹 →
(vol*‘(𝑥 ∖
∪ ran 𝐹)) = 0) |
90 | 89 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (vol*‘(𝑥 ∖ ∪ ran 𝐹)) = 0) |
91 | 83, 90 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) = ((𝑆‘𝑘) + 0)) |
92 | | nnuz 11599 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ℕ =
(ℤ≥‘1) |
93 | | 1zzd 11285 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 1 ∈
ℤ) |
94 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
95 | 94 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑘 → (vol‘(𝐹‘𝑛)) = (vol‘(𝐹‘𝑘))) |
96 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(vol‘(𝐹‘𝑘)) ∈ V |
97 | 95, 28, 96 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = (vol‘(𝐹‘𝑘))) |
98 | 97 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) = (vol‘(𝐹‘𝑘))) |
99 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 = 𝑘 → (𝐹‘𝑖) = (𝐹‘𝑘)) |
100 | 99 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 = 𝑘 → (vol‘(𝐹‘𝑖)) = (vol‘(𝐹‘𝑘))) |
101 | 100 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 = 𝑘 → ((vol‘(𝐹‘𝑖)) ∈ ℝ ↔ (vol‘(𝐹‘𝑘)) ∈ ℝ)) |
102 | 101 | rspccva 3281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((∀𝑖 ∈
ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ ∧ 𝑘 ∈ ℕ) → (vol‘(𝐹‘𝑘)) ∈ ℝ) |
103 | 14, 102 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol‘(𝐹‘𝑘)) ∈ ℝ) |
104 | 98, 103 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ) |
105 | 92, 93, 104 | serfre 12692 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ) |
106 | 27 | feq1i 5949 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑆:ℕ⟶ℝ ↔
seq1( + , 𝐺):ℕ⟶ℝ) |
107 | 105, 106 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑆:ℕ⟶ℝ) |
108 | 107 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℝ) |
109 | 108 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (𝑆‘𝑘) ∈ ℝ) |
110 | 109 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (𝑆‘𝑘) ∈ ℂ) |
111 | 110 | addid1d 10115 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((𝑆‘𝑘) + 0) = (𝑆‘𝑘)) |
112 | 91, 111 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) = (𝑆‘𝑘)) |
113 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ∪
ran 𝐹 →
(vol*‘𝑥) =
(vol*‘∪ ran 𝐹)) |
114 | 113 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (vol*‘𝑥) = (vol*‘∪ ran 𝐹)) |
115 | 112, 114 | breq12d 4596 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = ∪
ran 𝐹 ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → (((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝑥) ↔ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
116 | 115 | expr 641 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (𝑘 ∈ ℕ → (((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝑥) ↔ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
117 | 116 | pm5.74d 261 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → ((𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝑥)) ↔ (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
118 | 64, 117 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → (((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝑥))) ↔ ((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))))) |
119 | 62, 118 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = ∪
ran 𝐹 ∧ 𝜑) → ((𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( +
, 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥)))) ↔ (∪ ran
𝐹 ⊆ ℝ →
((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))))) |
120 | 119 | pm5.74da 719 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∪
ran 𝐹 → ((𝜑 → (𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( +
, 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥))))) ↔ (𝜑 → (∪ ran
𝐹 ⊆ ℝ →
((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))))))) |
121 | 1 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → 𝐹:ℕ⟶dom
vol) |
122 | 2 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
Disj 𝑖 ∈
ℕ (𝐹‘𝑖)) |
123 | | simp2 1055 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → 𝑥 ⊆
ℝ) |
124 | | simp3 1056 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘𝑥) ∈
ℝ) |
125 | 121, 122,
3, 123, 124 | voliunlem1 23125 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((seq1(
+ , 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥)) |
126 | 125 | 3exp1 1275 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( +
, 𝐻)‘𝑘) + (vol*‘(𝑥 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝑥))))) |
127 | 120, 126 | vtoclg 3239 |
. . . . . . . . . . 11
⊢ (∪ ran 𝐹 ∈ 𝒫 ℝ → (𝜑 → (∪ ran 𝐹 ⊆ ℝ → ((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))))) |
128 | 60, 127 | mpcom 37 |
. . . . . . . . . 10
⊢ (𝜑 → (∪ ran 𝐹 ⊆ ℝ → ((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))))) |
129 | 45, 128 | mpd 15 |
. . . . . . . . 9
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
130 | 58, 129 | sylbird 249 |
. . . . . . . 8
⊢ (𝜑 → ((-∞ <
(vol*‘∪ ran 𝐹) ∧ (vol*‘∪ ran 𝐹) < +∞) → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
131 | 56, 130 | mpand 707 |
. . . . . . 7
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) < +∞ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
132 | | nltpnft 11871 |
. . . . . . . . 9
⊢
((vol*‘∪ ran 𝐹) ∈ ℝ* →
((vol*‘∪ ran 𝐹) = +∞ ↔ ¬ (vol*‘∪ ran 𝐹) < +∞)) |
133 | 47, 132 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) = +∞ ↔ ¬ (vol*‘∪ ran 𝐹) < +∞)) |
134 | | rexr 9964 |
. . . . . . . . . . 11
⊢ ((𝑆‘𝑘) ∈ ℝ → (𝑆‘𝑘) ∈
ℝ*) |
135 | | pnfge 11840 |
. . . . . . . . . . 11
⊢ ((𝑆‘𝑘) ∈ ℝ* → (𝑆‘𝑘) ≤ +∞) |
136 | 108, 134,
135 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ +∞) |
137 | 136 | ex 449 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ +∞)) |
138 | | breq2 4587 |
. . . . . . . . . 10
⊢
((vol*‘∪ ran 𝐹) = +∞ → ((𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹) ↔ (𝑆‘𝑘) ≤ +∞)) |
139 | 138 | imbi2d 329 |
. . . . . . . . 9
⊢
((vol*‘∪ ran 𝐹) = +∞ → ((𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)) ↔ (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ +∞))) |
140 | 137, 139 | syl5ibrcom 236 |
. . . . . . . 8
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) = +∞ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
141 | 133, 140 | sylbird 249 |
. . . . . . 7
⊢ (𝜑 → (¬ (vol*‘∪ ran 𝐹) < +∞ → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)))) |
142 | 131, 141 | pm2.61d 169 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ → (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
143 | 142 | ralrimiv 2948 |
. . . . 5
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹)) |
144 | | ffn 5958 |
. . . . . . 7
⊢ (𝑆:ℕ⟶ℝ →
𝑆 Fn
ℕ) |
145 | 107, 144 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑆 Fn ℕ) |
146 | | breq1 4586 |
. . . . . . 7
⊢ (𝑧 = (𝑆‘𝑘) → (𝑧 ≤ (vol*‘∪ ran 𝐹) ↔ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
147 | 146 | ralrn 6270 |
. . . . . 6
⊢ (𝑆 Fn ℕ →
(∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹) ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
148 | 145, 147 | syl 17 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹) ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ (vol*‘∪ ran 𝐹))) |
149 | 143, 148 | mpbird 246 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹)) |
150 | | frn 5966 |
. . . . . . 7
⊢ (𝑆:ℕ⟶ℝ →
ran 𝑆 ⊆
ℝ) |
151 | 107, 150 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝑆 ⊆ ℝ) |
152 | | ressxr 9962 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
153 | 151, 152 | syl6ss 3580 |
. . . . 5
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
154 | | supxrleub 12028 |
. . . . 5
⊢ ((ran
𝑆 ⊆
ℝ* ∧ (vol*‘∪ ran 𝐹) ∈ ℝ*)
→ (sup(ran 𝑆,
ℝ*, < ) ≤ (vol*‘∪ ran
𝐹) ↔ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹))) |
155 | 153, 47, 154 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran 𝐹) ↔ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘∪ ran 𝐹))) |
156 | 149, 155 | mpbird 246 |
. . 3
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran 𝐹)) |
157 | | supxrcl 12017 |
. . . . 5
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
158 | 153, 157 | syl 17 |
. . . 4
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
159 | | xrletri3 11861 |
. . . 4
⊢
(((vol*‘∪ ran 𝐹) ∈ ℝ* ∧ sup(ran
𝑆, ℝ*,
< ) ∈ ℝ*) → ((vol*‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, < ) ↔
((vol*‘∪ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, < ) ∧ sup(ran
𝑆, ℝ*,
< ) ≤ (vol*‘∪ ran 𝐹)))) |
160 | 47, 158, 159 | syl2anc 691 |
. . 3
⊢ (𝜑 → ((vol*‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, < ) ↔
((vol*‘∪ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, < ) ∧ sup(ran
𝑆, ℝ*,
< ) ≤ (vol*‘∪ ran 𝐹)))) |
161 | 35, 156, 160 | mpbir2and 959 |
. 2
⊢ (𝜑 → (vol*‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, <
)) |
162 | 6, 161 | eqtrd 2644 |
1
⊢ (𝜑 → (vol‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, <
)) |