Step | Hyp | Ref
| Expression |
1 | | voliunlem1.7 |
. . . . 5
⊢ (𝜑 → 𝐸 ⊆ ℝ) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐸 ⊆ ℝ) |
3 | | voliunlem1.8 |
. . . . 5
⊢ (𝜑 → (vol*‘𝐸) ∈
ℝ) |
4 | 3 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐸) ∈
ℝ) |
5 | | difss 3699 |
. . . . 5
⊢ (𝐸 ∖ ∪ ran 𝐹) ⊆ 𝐸 |
6 | | ovolsscl 23061 |
. . . . 5
⊢ (((𝐸 ∖ ∪ ran 𝐹) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∖
∪ ran 𝐹)) ∈ ℝ) |
7 | 5, 6 | mp3an1 1403 |
. . . 4
⊢ ((𝐸 ⊆ ℝ ∧
(vol*‘𝐸) ∈
ℝ) → (vol*‘(𝐸 ∖ ∪ ran
𝐹)) ∈
ℝ) |
8 | 2, 4, 7 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘(𝐸 ∖ ∪ ran 𝐹)) ∈ ℝ) |
9 | | difss 3699 |
. . . . 5
⊢ (𝐸 ∖ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) ⊆ 𝐸 |
10 | | ovolsscl 23061 |
. . . . 5
⊢ (((𝐸 ∖ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∖
∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) ∈ ℝ) |
11 | 9, 10 | mp3an1 1403 |
. . . 4
⊢ ((𝐸 ⊆ ℝ ∧
(vol*‘𝐸) ∈
ℝ) → (vol*‘(𝐸 ∖ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) ∈ ℝ) |
12 | 2, 4, 11 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘(𝐸 ∖ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) ∈ ℝ) |
13 | | inss1 3795 |
. . . . 5
⊢ (𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) ⊆ 𝐸 |
14 | | ovolsscl 23061 |
. . . . 5
⊢ (((𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∩
∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) ∈ ℝ) |
15 | 13, 14 | mp3an1 1403 |
. . . 4
⊢ ((𝐸 ⊆ ℝ ∧
(vol*‘𝐸) ∈
ℝ) → (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) ∈ ℝ) |
16 | 2, 4, 15 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) ∈ ℝ) |
17 | | elfznn 12241 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ) |
18 | | voliunlem.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:ℕ⟶dom vol) |
19 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝐹:ℕ⟶dom vol →
𝐹 Fn
ℕ) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 Fn ℕ) |
21 | | fnfvelrn 6264 |
. . . . . . . . . . 11
⊢ ((𝐹 Fn ℕ ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ran 𝐹) |
22 | 20, 21 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ran 𝐹) |
23 | | elssuni 4403 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑛) ∈ ran 𝐹 → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
25 | 17, 24 | sylan2 490 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑘)) → (𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
26 | 25 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
27 | 26 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
28 | | iunss 4497 |
. . . . . 6
⊢ (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ⊆ ∪ ran
𝐹 ↔ ∀𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
29 | 27, 28 | sylibr 223 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ⊆ ∪ ran
𝐹) |
30 | 29 | sscond 3709 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐸 ∖ ∪ ran
𝐹) ⊆ (𝐸 ∖ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) |
31 | 9, 2 | syl5ss 3579 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐸 ∖ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) ⊆ ℝ) |
32 | | ovolss 23060 |
. . . 4
⊢ (((𝐸 ∖ ∪ ran 𝐹) ⊆ (𝐸 ∖ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) ∧ (𝐸 ∖ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) ⊆ ℝ) → (vol*‘(𝐸 ∖ ∪ ran 𝐹)) ≤ (vol*‘(𝐸 ∖ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛)))) |
33 | 30, 31, 32 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘(𝐸 ∖ ∪ ran 𝐹)) ≤ (vol*‘(𝐸 ∖ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛)))) |
34 | 8, 12, 16, 33 | leadd2dd 10521 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) + (vol*‘(𝐸 ∖ ∪ ran
𝐹))) ≤
((vol*‘(𝐸 ∩
∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) + (vol*‘(𝐸 ∖ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))))) |
35 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑧 = 1 → (1...𝑧) = (1...1)) |
36 | 35 | iuneq1d 4481 |
. . . . . . . . . 10
⊢ (𝑧 = 1 → ∪ 𝑛 ∈ (1...𝑧)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛)) |
37 | 36 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑧 = 1 → (∪ 𝑛 ∈ (1...𝑧)(𝐹‘𝑛) ∈ dom vol ↔ ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) ∈ dom vol)) |
38 | 36 | ineq2d 3776 |
. . . . . . . . . . 11
⊢ (𝑧 = 1 → (𝐸 ∩ ∪
𝑛 ∈ (1...𝑧)(𝐹‘𝑛)) = (𝐸 ∩ ∪
𝑛 ∈ (1...1)(𝐹‘𝑛))) |
39 | 38 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑧 = 1 → (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑧)(𝐹‘𝑛))) = (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...1)(𝐹‘𝑛)))) |
40 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑧 = 1 → (seq1( + , 𝐻)‘𝑧) = (seq1( + , 𝐻)‘1)) |
41 | 39, 40 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑧 = 1 → ((vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑧)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑧) ↔ (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...1)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘1))) |
42 | 37, 41 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑧 = 1 → ((∪ 𝑛 ∈ (1...𝑧)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑧)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑧)) ↔ (∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘1)))) |
43 | 42 | imbi2d 329 |
. . . . . . 7
⊢ (𝑧 = 1 → ((𝜑 → (∪
𝑛 ∈ (1...𝑧)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑧)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑧))) ↔ (𝜑 → (∪
𝑛 ∈ (1...1)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘1))))) |
44 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑘 → (1...𝑧) = (1...𝑘)) |
45 | 44 | iuneq1d 4481 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑘 → ∪
𝑛 ∈ (1...𝑧)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) |
46 | 45 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑧 = 𝑘 → (∪
𝑛 ∈ (1...𝑧)(𝐹‘𝑛) ∈ dom vol ↔ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∈ dom vol)) |
47 | 45 | ineq2d 3776 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑘 → (𝐸 ∩ ∪
𝑛 ∈ (1...𝑧)(𝐹‘𝑛)) = (𝐸 ∩ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) |
48 | 47 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑘 → (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑧)(𝐹‘𝑛))) = (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛)))) |
49 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑘 → (seq1( + , 𝐻)‘𝑧) = (seq1( + , 𝐻)‘𝑘)) |
50 | 48, 49 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑧 = 𝑘 → ((vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑧)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑧) ↔ (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑘))) |
51 | 46, 50 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑧 = 𝑘 → ((∪
𝑛 ∈ (1...𝑧)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑧)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑧)) ↔ (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑘)))) |
52 | 51 | imbi2d 329 |
. . . . . . 7
⊢ (𝑧 = 𝑘 → ((𝜑 → (∪
𝑛 ∈ (1...𝑧)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑧)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑧))) ↔ (𝜑 → (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑘))))) |
53 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑘 + 1) → (1...𝑧) = (1...(𝑘 + 1))) |
54 | 53 | iuneq1d 4481 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑘 + 1) → ∪ 𝑛 ∈ (1...𝑧)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) |
55 | 54 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑧 = (𝑘 + 1) → (∪ 𝑛 ∈ (1...𝑧)(𝐹‘𝑛) ∈ dom vol ↔ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ∈ dom vol)) |
56 | 54 | ineq2d 3776 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑘 + 1) → (𝐸 ∩ ∪
𝑛 ∈ (1...𝑧)(𝐹‘𝑛)) = (𝐸 ∩ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) |
57 | 56 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑘 + 1) → (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑧)(𝐹‘𝑛))) = (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)))) |
58 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑘 + 1) → (seq1( + , 𝐻)‘𝑧) = (seq1( + , 𝐻)‘(𝑘 + 1))) |
59 | 57, 58 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑧 = (𝑘 + 1) → ((vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑧)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑧) ↔ (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1)))) |
60 | 55, 59 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑧 = (𝑘 + 1) → ((∪ 𝑛 ∈ (1...𝑧)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑧)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑧)) ↔ (∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1))))) |
61 | 60 | imbi2d 329 |
. . . . . . 7
⊢ (𝑧 = (𝑘 + 1) → ((𝜑 → (∪
𝑛 ∈ (1...𝑧)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑧)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑧))) ↔ (𝜑 → (∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1)))))) |
62 | | 1z 11284 |
. . . . . . . . . . 11
⊢ 1 ∈
ℤ |
63 | | fzsn 12254 |
. . . . . . . . . . 11
⊢ (1 ∈
ℤ → (1...1) = {1}) |
64 | | iuneq1 4470 |
. . . . . . . . . . 11
⊢ ((1...1)
= {1} → ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = ∪ 𝑛 ∈ {1} (𝐹‘𝑛)) |
65 | 62, 63, 64 | mp2b 10 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = ∪ 𝑛 ∈ {1} (𝐹‘𝑛) |
66 | | 1ex 9914 |
. . . . . . . . . . 11
⊢ 1 ∈
V |
67 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑛 = 1 → (𝐹‘𝑛) = (𝐹‘1)) |
68 | 66, 67 | iunxsn 4539 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ {1} (𝐹‘𝑛) = (𝐹‘1) |
69 | 65, 68 | eqtri 2632 |
. . . . . . . . 9
⊢ ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = (𝐹‘1) |
70 | | 1nn 10908 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
71 | | ffvelrn 6265 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶dom vol ∧ 1
∈ ℕ) → (𝐹‘1) ∈ dom vol) |
72 | 18, 70, 71 | sylancl 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘1) ∈ dom vol) |
73 | 69, 72 | syl5eqel 2692 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) ∈ dom vol) |
74 | 67 | ineq2d 3776 |
. . . . . . . . . . . 12
⊢ (𝑛 = 1 → (𝐸 ∩ (𝐹‘𝑛)) = (𝐸 ∩ (𝐹‘1))) |
75 | 74 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑛 = 1 → (vol*‘(𝐸 ∩ (𝐹‘𝑛))) = (vol*‘(𝐸 ∩ (𝐹‘1)))) |
76 | | voliunlem1.6 |
. . . . . . . . . . 11
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐸 ∩ (𝐹‘𝑛)))) |
77 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(vol*‘(𝐸 ∩
(𝐹‘1))) ∈
V |
78 | 75, 76, 77 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (1 ∈
ℕ → (𝐻‘1)
= (vol*‘(𝐸 ∩
(𝐹‘1)))) |
79 | 70, 78 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝐻‘1) = (vol*‘(𝐸 ∩ (𝐹‘1))) |
80 | | seq1 12676 |
. . . . . . . . . 10
⊢ (1 ∈
ℤ → (seq1( + , 𝐻)‘1) = (𝐻‘1)) |
81 | 62, 80 | ax-mp 5 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐻)‘1) = (𝐻‘1) |
82 | 69 | ineq2i 3773 |
. . . . . . . . . 10
⊢ (𝐸 ∩ ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛)) = (𝐸 ∩ (𝐹‘1)) |
83 | 82 | fveq2i 6106 |
. . . . . . . . 9
⊢
(vol*‘(𝐸 ∩
∪ 𝑛 ∈ (1...1)(𝐹‘𝑛))) = (vol*‘(𝐸 ∩ (𝐹‘1))) |
84 | 79, 81, 83 | 3eqtr4ri 2643 |
. . . . . . . 8
⊢
(vol*‘(𝐸 ∩
∪ 𝑛 ∈ (1...1)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘1) |
85 | 73, 84 | jctir 559 |
. . . . . . 7
⊢ (𝜑 → (∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘1))) |
86 | | peano2nn 10909 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
87 | | ffvelrn 6265 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶dom vol ∧
(𝑘 + 1) ∈ ℕ)
→ (𝐹‘(𝑘 + 1)) ∈ dom
vol) |
88 | 18, 86, 87 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ dom vol) |
89 | | unmbl 23112 |
. . . . . . . . . . . . 13
⊢
((∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∈ dom vol ∧ (𝐹‘(𝑘 + 1)) ∈ dom vol) → (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) ∈ dom vol) |
90 | 89 | ex 449 |
. . . . . . . . . . . 12
⊢ (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∈ dom vol → ((𝐹‘(𝑘 + 1)) ∈ dom vol → (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) ∈ dom vol)) |
91 | 88, 90 | syl5com 31 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∈ dom vol → (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) ∈ dom vol)) |
92 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
93 | | nnuz 11599 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
94 | 92, 93 | syl6eleq 2698 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) |
95 | | fzsuc 12258 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(ℤ≥‘1) → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)})) |
96 | | iuneq1 4470 |
. . . . . . . . . . . . . 14
⊢
((1...(𝑘 + 1)) =
((1...𝑘) ∪ {(𝑘 + 1)}) → ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = ∪ 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹‘𝑛)) |
97 | 94, 95, 96 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = ∪ 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹‘𝑛)) |
98 | | iunxun 4541 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ ∪
𝑛 ∈ {(𝑘 + 1)} (𝐹‘𝑛)) |
99 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 + 1) ∈ V |
100 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑘 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑘 + 1))) |
101 | 99, 100 | iunxsn 4539 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑛 ∈ {(𝑘 + 1)} (𝐹‘𝑛) = (𝐹‘(𝑘 + 1)) |
102 | 101 | uneq2i 3726 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ ∪
𝑛 ∈ {(𝑘 + 1)} (𝐹‘𝑛)) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) |
103 | 98, 102 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) |
104 | 97, 103 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1)))) |
105 | 104 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ∈ dom vol ↔ (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) ∈ dom vol)) |
106 | 91, 105 | sylibrd 248 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∈ dom vol → ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ∈ dom vol)) |
107 | | oveq1 6556 |
. . . . . . . . . . 11
⊢
((vol*‘(𝐸
∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑘) → ((vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))) = ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))) |
108 | | inss1 3795 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ⊆ 𝐸 |
109 | 108, 2 | syl5ss 3579 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐸 ∩ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ⊆ ℝ) |
110 | | ovolsscl 23061 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∩
∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) ∈ ℝ) |
111 | 108, 110 | mp3an1 1403 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸 ⊆ ℝ ∧
(vol*‘𝐸) ∈
ℝ) → (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) ∈ ℝ) |
112 | 2, 4, 111 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) ∈ ℝ) |
113 | | mblsplit 23107 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘(𝑘 + 1)) ∈ dom vol ∧ (𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ⊆ ℝ ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) ∈ ℝ) → (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) = ((vol*‘((𝐸 ∩ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘((𝐸 ∩ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ∖ (𝐹‘(𝑘 + 1)))))) |
114 | 88, 109, 112, 113 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) = ((vol*‘((𝐸 ∩ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘((𝐸 ∩ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ∖ (𝐹‘(𝑘 + 1)))))) |
115 | | in32 3787 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ∩ (𝐹‘(𝑘 + 1))) = ((𝐸 ∩ (𝐹‘(𝑘 + 1))) ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) |
116 | | inss2 3796 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ (𝐹‘(𝑘 + 1)) |
117 | 86 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ) |
118 | 117, 93 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈
(ℤ≥‘1)) |
119 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 + 1) ∈
(ℤ≥‘1) → (𝑘 + 1) ∈ (1...(𝑘 + 1))) |
120 | 100 | ssiun2s 4500 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 + 1) ∈ (1...(𝑘 + 1)) → (𝐹‘(𝑘 + 1)) ⊆ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) |
121 | 118, 119,
120 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ⊆ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) |
122 | 116, 121 | syl5ss 3579 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) |
123 | | df-ss 3554 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ↔ ((𝐸 ∩ (𝐹‘(𝑘 + 1))) ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) = (𝐸 ∩ (𝐹‘(𝑘 + 1)))) |
124 | 122, 123 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐸 ∩ (𝐹‘(𝑘 + 1))) ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) = (𝐸 ∩ (𝐹‘(𝑘 + 1)))) |
125 | 115, 124 | syl5eq 2656 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐸 ∩ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ∩ (𝐹‘(𝑘 + 1))) = (𝐸 ∩ (𝐹‘(𝑘 + 1)))) |
126 | 125 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘((𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ∩ (𝐹‘(𝑘 + 1)))) = (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))) |
127 | | indif2 3829 |
. . . . . . . . . . . . . . . 16
⊢ (𝐸 ∩ (∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ∖ (𝐹‘(𝑘 + 1)))) = ((𝐸 ∩ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ∖ (𝐹‘(𝑘 + 1))) |
128 | | uncom 3719 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) = ((𝐹‘(𝑘 + 1)) ∪ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) |
129 | 104, 128 | syl6req 2661 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘(𝑘 + 1)) ∪ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) = ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) |
130 | | voliunlem.5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖)) |
131 | 130 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → Disj 𝑖 ∈ ℕ (𝐹‘𝑖)) |
132 | 117 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝑘 + 1) ∈ ℕ) |
133 | 17 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ) |
134 | 133 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℝ) |
135 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ (1...𝑘) → 𝑛 ≤ 𝑘) |
136 | 135 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ≤ 𝑘) |
137 | 92 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑘 ∈ ℕ) |
138 | | nnleltp1 11309 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑛 ≤ 𝑘 ↔ 𝑛 < (𝑘 + 1))) |
139 | 133, 137,
138 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝑛 ≤ 𝑘 ↔ 𝑛 < (𝑘 + 1))) |
140 | 136, 139 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 < (𝑘 + 1)) |
141 | 134, 140 | gtned 10051 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝑘 + 1) ≠ 𝑛) |
142 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = (𝑘 + 1) → (𝐹‘𝑖) = (𝐹‘(𝑘 + 1))) |
143 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = 𝑛 → (𝐹‘𝑖) = (𝐹‘𝑛)) |
144 | 142, 143 | disji2 4569 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((Disj 𝑖
∈ ℕ (𝐹‘𝑖) ∧ ((𝑘 + 1) ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑘 + 1) ≠ 𝑛) → ((𝐹‘(𝑘 + 1)) ∩ (𝐹‘𝑛)) = ∅) |
145 | 131, 132,
133, 141, 144 | syl121anc 1323 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((𝐹‘(𝑘 + 1)) ∩ (𝐹‘𝑛)) = ∅) |
146 | 145 | iuneq2dv 4478 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∪ 𝑛 ∈ (1...𝑘)((𝐹‘(𝑘 + 1)) ∩ (𝐹‘𝑛)) = ∪
𝑛 ∈ (1...𝑘)∅) |
147 | | iunin2 4520 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∪ 𝑛 ∈ (1...𝑘)((𝐹‘(𝑘 + 1)) ∩ (𝐹‘𝑛)) = ((𝐹‘(𝑘 + 1)) ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) |
148 | | iun0 4512 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∪ 𝑛 ∈ (1...𝑘)∅ = ∅ |
149 | 146, 147,
148 | 3eqtr3g 2667 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘(𝑘 + 1)) ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) = ∅) |
150 | | uneqdifeq 4009 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹‘(𝑘 + 1)) ⊆ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ∧ ((𝐹‘(𝑘 + 1)) ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) = ∅) → (((𝐹‘(𝑘 + 1)) ∪ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) = ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ↔ (∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ∖ (𝐹‘(𝑘 + 1))) = ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) |
151 | 121, 149,
150 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐹‘(𝑘 + 1)) ∪ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) = ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ↔ (∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ∖ (𝐹‘(𝑘 + 1))) = ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) |
152 | 129, 151 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ∖ (𝐹‘(𝑘 + 1))) = ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) |
153 | 152 | ineq2d 3776 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐸 ∩ (∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ∖ (𝐹‘(𝑘 + 1)))) = (𝐸 ∩ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) |
154 | 127, 153 | syl5eqr 2658 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐸 ∩ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ∖ (𝐹‘(𝑘 + 1))) = (𝐸 ∩ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) |
155 | 154 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘((𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ∖ (𝐹‘(𝑘 + 1)))) = (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛)))) |
156 | 126, 155 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘((𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘((𝐸 ∩ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) ∖ (𝐹‘(𝑘 + 1))))) = ((vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))))) |
157 | | inss1 3795 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ 𝐸 |
158 | | ovolsscl 23061 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) ∈ ℝ) |
159 | 157, 158 | mp3an1 1403 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸 ⊆ ℝ ∧
(vol*‘𝐸) ∈
ℝ) → (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) ∈ ℝ) |
160 | 2, 4, 159 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) ∈ ℝ) |
161 | 160 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) ∈ ℂ) |
162 | 16 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) ∈ ℂ) |
163 | 161, 162 | addcomd 10117 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛)))) = ((vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))) |
164 | 114, 156,
163 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) = ((vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))) |
165 | | seqp1 12678 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(ℤ≥‘1) → (seq1( + , 𝐻)‘(𝑘 + 1)) = ((seq1( + , 𝐻)‘𝑘) + (𝐻‘(𝑘 + 1)))) |
166 | 94, 165 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘(𝑘 + 1)) = ((seq1( + , 𝐻)‘𝑘) + (𝐻‘(𝑘 + 1)))) |
167 | 100 | ineq2d 3776 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑘 + 1) → (𝐸 ∩ (𝐹‘𝑛)) = (𝐸 ∩ (𝐹‘(𝑘 + 1)))) |
168 | 167 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑘 + 1) → (vol*‘(𝐸 ∩ (𝐹‘𝑛))) = (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))) |
169 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢
(vol*‘(𝐸 ∩
(𝐹‘(𝑘 + 1)))) ∈
V |
170 | 168, 76, 169 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 + 1) ∈ ℕ →
(𝐻‘(𝑘 + 1)) = (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))) |
171 | 117, 170 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(𝑘 + 1)) = (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))) |
172 | 171 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (𝐻‘(𝑘 + 1))) = ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))) |
173 | 166, 172 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘(𝑘 + 1)) = ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))) |
174 | 164, 173 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1)) ↔ ((vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))) = ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))))) |
175 | 107, 174 | syl5ibr 235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑘) → (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1)))) |
176 | 106, 175 | anim12d 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑘)) → (∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1))))) |
177 | 176 | expcom 450 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝜑 → ((∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑘)) → (∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1)))))) |
178 | 177 | a2d 29 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝜑 → (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑘))) → (𝜑 → (∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1)))))) |
179 | 43, 52, 61, 52, 85, 178 | nnind 10915 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (𝜑 → (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑘)))) |
180 | 179 | impcom 445 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∈ dom vol ∧ (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑘))) |
181 | 180 | simprd 478 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) = (seq1( + , 𝐻)‘𝑘)) |
182 | 181 | eqcomd 2616 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘𝑘) = (vol*‘(𝐸 ∩ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛)))) |
183 | 182 | oveq1d 6564 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∖ ∪ ran
𝐹))) = ((vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) + (vol*‘(𝐸 ∖ ∪ ran
𝐹)))) |
184 | 180 | simpld 474 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∈ dom vol) |
185 | | mblsplit 23107 |
. . 3
⊢
((∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∈ dom vol ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘𝐸) =
((vol*‘(𝐸 ∩
∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) + (vol*‘(𝐸 ∖ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))))) |
186 | 184, 2, 4, 185 | syl3anc 1318 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐸) = ((vol*‘(𝐸 ∩ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛))) + (vol*‘(𝐸 ∖ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛))))) |
187 | 34, 183, 186 | 3brtr4d 4615 |
1
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∖ ∪ ran
𝐹))) ≤ (vol*‘𝐸)) |