Step | Hyp | Ref
| Expression |
1 | | inss1 3981 |
. . . . 5
⊢ (𝐸 ∩ 𝐴) ⊆ 𝐸 |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ 𝐸) |
3 | | uniioombl.s |
. . . . 5
⊢ (𝜑 → 𝐸 ⊆ ∪ ran
((,) ∘ 𝐺)) |
4 | | uniioombl.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
5 | 4 | uniiccdif 23565 |
. . . . . . 7
⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
([,] ∘ 𝐺) ∧
(vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran
((,) ∘ 𝐺))) =
0)) |
6 | 5 | simpld 482 |
. . . . . 6
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
([,] ∘ 𝐺)) |
7 | | ovolficcss 23456 |
. . . . . . 7
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐺) ⊆
ℝ) |
8 | 4, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ) |
9 | 6, 8 | sstrd 3762 |
. . . . 5
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ) |
10 | 3, 9 | sstrd 3762 |
. . . 4
⊢ (𝜑 → 𝐸 ⊆ ℝ) |
11 | | uniioombl.e |
. . . 4
⊢ (𝜑 → (vol*‘𝐸) ∈
ℝ) |
12 | | ovolsscl 23473 |
. . . 4
⊢ (((𝐸 ∩ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∩ 𝐴)) ∈
ℝ) |
13 | 2, 10, 11, 12 | syl3anc 1476 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ∈ ℝ) |
14 | | difssd 3889 |
. . . 4
⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ 𝐸) |
15 | | ovolsscl 23473 |
. . . 4
⊢ (((𝐸 ∖ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∖
𝐴)) ∈
ℝ) |
16 | 14, 10, 11, 15 | syl3anc 1476 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ∈ ℝ) |
17 | | inss1 3981 |
. . . . . 6
⊢ (𝐾 ∩ 𝐴) ⊆ 𝐾 |
18 | 17 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐾 ∩ 𝐴) ⊆ 𝐾) |
19 | | uniioombl.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
20 | | uniioombl.2 |
. . . . . . . 8
⊢ (𝜑 → Disj 𝑥 ∈ ℕ
((,)‘(𝐹‘𝑥))) |
21 | | uniioombl.3 |
. . . . . . . 8
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
22 | | uniioombl.a |
. . . . . . . 8
⊢ 𝐴 = ∪
ran ((,) ∘ 𝐹) |
23 | | uniioombl.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
24 | | uniioombl.t |
. . . . . . . 8
⊢ 𝑇 = seq1( + , ((abs ∘
− ) ∘ 𝐺)) |
25 | | uniioombl.v |
. . . . . . . 8
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤
((vol*‘𝐸) + 𝐶)) |
26 | | uniioombl.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
27 | | uniioombl.m2 |
. . . . . . . 8
⊢ (𝜑 → (abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) |
28 | | uniioombl.k |
. . . . . . . 8
⊢ 𝐾 = ∪
(((,) ∘ 𝐺) “
(1...𝑀)) |
29 | 19, 20, 21, 22, 11, 23, 4, 3, 24, 25, 26, 27, 28 | uniioombllem3a 23571 |
. . . . . . 7
⊢ (𝜑 → (𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ∧ (vol*‘𝐾) ∈ ℝ)) |
30 | 29 | simpld 482 |
. . . . . 6
⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
31 | | inss2 3982 |
. . . . . . . . . . . . 13
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
32 | | elfznn 12576 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ) |
33 | | ffvelrn 6502 |
. . . . . . . . . . . . . 14
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
34 | 4, 32, 33 | syl2an 583 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
35 | 31, 34 | sseldi 3750 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ ×
ℝ)) |
36 | | 1st2nd2 7357 |
. . . . . . . . . . . 12
⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) →
(𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
38 | 37 | fveq2d 6337 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉)) |
39 | | df-ov 6798 |
. . . . . . . . . 10
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉) |
40 | 38, 39 | syl6eqr 2823 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗)))) |
41 | | ioossre 12439 |
. . . . . . . . 9
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) ⊆ ℝ |
42 | 40, 41 | syl6eqss 3804 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
43 | 42 | ralrimiva 3115 |
. . . . . . 7
⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
44 | | iunss 4696 |
. . . . . . 7
⊢ (∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ ↔ ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
45 | 43, 44 | sylibr 224 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
46 | 30, 45 | eqsstrd 3788 |
. . . . 5
⊢ (𝜑 → 𝐾 ⊆ ℝ) |
47 | 29 | simprd 483 |
. . . . 5
⊢ (𝜑 → (vol*‘𝐾) ∈
ℝ) |
48 | | ovolsscl 23473 |
. . . . 5
⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∩ 𝐴)) ∈
ℝ) |
49 | 18, 46, 47, 48 | syl3anc 1476 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ) |
50 | 23 | rpred 12074 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℝ) |
51 | 49, 50 | readdcld 10274 |
. . 3
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) ∈ ℝ) |
52 | | difssd 3889 |
. . . . 5
⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ 𝐾) |
53 | | ovolsscl 23473 |
. . . . 5
⊢ (((𝐾 ∖ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∖
𝐴)) ∈
ℝ) |
54 | 52, 46, 47, 53 | syl3anc 1476 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ) |
55 | 54, 50 | readdcld 10274 |
. . 3
⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶) ∈ ℝ) |
56 | | ssun2 3928 |
. . . . . . 7
⊢ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
57 | | ioof 12476 |
. . . . . . . . . . . . . . 15
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
58 | | rexpssxrxp 10289 |
. . . . . . . . . . . . . . . . 17
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
59 | 31, 58 | sstri 3761 |
. . . . . . . . . . . . . . . 16
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
60 | | fss 6197 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
61 | 4, 59, 60 | sylancl 574 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
62 | | fco 6199 |
. . . . . . . . . . . . . . 15
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐺:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
63 | 57, 61, 62 | sylancr 575 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
64 | 63 | ffnd 6185 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ) |
65 | | fnima 6149 |
. . . . . . . . . . . . 13
⊢ (((,)
∘ 𝐺) Fn ℕ
→ (((,) ∘ 𝐺)
“ ℕ) = ran ((,) ∘ 𝐺)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = ran ((,)
∘ 𝐺)) |
67 | | nnuz 11929 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
68 | 26 | peano2nnd 11242 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 + 1) ∈ ℕ) |
69 | 68, 67 | syl6eleq 2860 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘1)) |
70 | | uzsplit 12618 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 + 1) ∈
(ℤ≥‘1) → (ℤ≥‘1) =
((1...((𝑀 + 1) − 1))
∪ (ℤ≥‘(𝑀 + 1)))) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(ℤ≥‘1) = ((1...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1)))) |
72 | 67, 71 | syl5eq 2817 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℕ = ((1...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1)))) |
73 | 26 | nncnd 11241 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ ℂ) |
74 | | ax-1cn 10199 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
75 | | pncan 10492 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 1) = 𝑀) |
76 | 73, 74, 75 | sylancl 574 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀) |
77 | 76 | oveq2d 6811 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...((𝑀 + 1) − 1)) = (1...𝑀)) |
78 | 77 | uneq1d 3917 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((1...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1))) = ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))) |
79 | 72, 78 | eqtrd 2805 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℕ = ((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
80 | 79 | imaeq2d 5606 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = (((,)
∘ 𝐺) “
((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1))))) |
81 | 66, 80 | eqtr3d 2807 |
. . . . . . . . . . 11
⊢ (𝜑 → ran ((,) ∘ 𝐺) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1))))) |
82 | | imaundi 5685 |
. . . . . . . . . . 11
⊢ (((,)
∘ 𝐺) “
((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
83 | 81, 82 | syl6eq 2821 |
. . . . . . . . . 10
⊢ (𝜑 → ran ((,) ∘ 𝐺) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
84 | 83 | unieqd 4585 |
. . . . . . . . 9
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪ ((((,)
∘ 𝐺) “
(1...𝑀)) ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
85 | | uniun 4594 |
. . . . . . . . 9
⊢ ∪ ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) = (∪
(((,) ∘ 𝐺) “
(1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
86 | 84, 85 | syl6eq 2821 |
. . . . . . . 8
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (∪ (((,)
∘ 𝐺) “
(1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
87 | 28 | uneq1i 3914 |
. . . . . . . 8
⊢ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) = (∪
(((,) ∘ 𝐺) “
(1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
88 | 86, 87 | syl6eqr 2823 |
. . . . . . 7
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
89 | 56, 88 | syl5sseqr 3803 |
. . . . . 6
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ 𝐺)) |
90 | 19, 20, 21, 22, 11, 23, 4, 3, 24, 25 | uniioombllem1 23568 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
91 | | ssid 3773 |
. . . . . . . 8
⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
((,) ∘ 𝐺) |
92 | 24 | ovollb 23466 |
. . . . . . . 8
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ∪ ran ((,) ∘
𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, <
)) |
93 | 4, 91, 92 | sylancl 574 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, <
)) |
94 | | ovollecl 23470 |
. . . . . . 7
⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ*, < )
∈ ℝ ∧ (vol*‘∪ ran ((,) ∘
𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
→ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈
ℝ) |
95 | 9, 90, 93, 94 | syl3anc 1476 |
. . . . . 6
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) |
96 | | ovolsscl 23473 |
. . . . . 6
⊢ ((∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ 𝐺) ∧
∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ) |
97 | 89, 9, 95, 96 | syl3anc 1476 |
. . . . 5
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ) |
98 | 49, 97 | readdcld 10274 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
99 | | unss1 3933 |
. . . . . . . 8
⊢ ((𝐾 ∩ 𝐴) ⊆ 𝐾 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
100 | 17, 99 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
101 | 100, 88 | syl5sseqr 3803 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺)) |
102 | | ovolsscl 23473 |
. . . . . 6
⊢ ((((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran
((,) ∘ 𝐺) ⊆
ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) →
(vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
103 | 101, 9, 95, 102 | syl3anc 1476 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
104 | 3, 88 | sseqtrd 3790 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
105 | 104 | ssrind 3988 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∩ 𝐴)) |
106 | | indir 4024 |
. . . . . . . 8
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∩ 𝐴) = ((𝐾 ∩ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴)) |
107 | | inss1 3981 |
. . . . . . . . 9
⊢ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) |
108 | | unss2 3935 |
. . . . . . . . 9
⊢ ((∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) → ((𝐾 ∩ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
109 | 107, 108 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐾 ∩ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
110 | 106, 109 | eqsstri 3784 |
. . . . . . 7
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
111 | 105, 110 | syl6ss 3764 |
. . . . . 6
⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
112 | 101, 9 | sstrd 3762 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) |
113 | | ovolss 23472 |
. . . . . 6
⊢ (((𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∧ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) →
(vol*‘(𝐸 ∩ 𝐴)) ≤ (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
114 | 111, 112,
113 | syl2anc 573 |
. . . . 5
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ≤ (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
115 | 18, 46 | sstrd 3762 |
. . . . . 6
⊢ (𝜑 → (𝐾 ∩ 𝐴) ⊆ ℝ) |
116 | 89, 9 | sstrd 3762 |
. . . . . 6
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ℝ) |
117 | | ovolun 23486 |
. . . . . 6
⊢ ((((𝐾 ∩ 𝐴) ⊆ ℝ ∧ (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ℝ ∧
(vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ)) →
(vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
118 | 115, 49, 116, 97, 117 | syl22anc 1477 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
119 | 13, 103, 98, 114, 118 | letrd 10399 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
120 | | rge0ssre 12486 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℝ |
121 | | eqid 2771 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) |
122 | 121, 24 | ovolsf 23459 |
. . . . . . . . . 10
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞)) |
123 | 4, 122 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞)) |
124 | 123, 26 | ffvelrnd 6505 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘𝑀) ∈ (0[,)+∞)) |
125 | 120, 124 | sseldi 3750 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘𝑀) ∈ ℝ) |
126 | 90, 125 | resubcld 10663 |
. . . . . 6
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ∈ ℝ) |
127 | 97 | rexrd 10294 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈
ℝ*) |
128 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℕ) |
129 | | nnaddcl 11247 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ) |
130 | 128, 26, 129 | syl2anr 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ) |
131 | 4 | ffvelrnda 6504 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 + 𝑀) ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
132 | 130, 131 | syldan 579 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
133 | | eqid 2771 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) |
134 | 132, 133 | fmptd 6529 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
135 | | eqid 2771 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((abs ∘ − ) ∘
(𝑧 ∈ ℕ ↦
(𝐺‘(𝑧 + 𝑀)))) |
136 | | eqid 2771 |
. . . . . . . . . . . 12
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) = seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀))))) |
137 | 135, 136 | ovolsf 23459 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞)) |
138 | 134, 137 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞)) |
139 | 138 | frnd 6191 |
. . . . . . . . 9
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆
(0[,)+∞)) |
140 | | icossxr 12462 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ* |
141 | 139, 140 | syl6ss 3764 |
. . . . . . . 8
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆
ℝ*) |
142 | | supxrcl 12349 |
. . . . . . . 8
⊢ (ran
seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ* →
sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ∈
ℝ*) |
143 | 141, 142 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ∈
ℝ*) |
144 | 126 | rexrd 10294 |
. . . . . . 7
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ∈
ℝ*) |
145 | | 1zzd 11614 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 1 ∈
ℤ) |
146 | 26 | nnzd 11687 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℤ) |
147 | 146 | adantr 466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℤ) |
148 | | addcom 10427 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑀 + 1) =
(1 + 𝑀)) |
149 | 73, 74, 148 | sylancl 574 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑀 + 1) = (1 + 𝑀)) |
150 | 149 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) = (ℤ≥‘(1 +
𝑀))) |
151 | 150 | eleq2d 2836 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑥 ∈ (ℤ≥‘(𝑀 + 1)) ↔ 𝑥 ∈ (ℤ≥‘(1 +
𝑀)))) |
152 | 151 | biimpa 462 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
(ℤ≥‘(1 + 𝑀))) |
153 | | eluzsub 11922 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℤ ∧ 𝑀
∈ ℤ ∧ 𝑥
∈ (ℤ≥‘(1 + 𝑀))) → (𝑥 − 𝑀) ∈
(ℤ≥‘1)) |
154 | 145, 147,
152, 153 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈
(ℤ≥‘1)) |
155 | 154, 67 | syl6eleqr 2861 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈ ℕ) |
156 | | eluzelz 11902 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑥 ∈ ℤ) |
157 | 156 | adantl 467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
ℤ) |
158 | 157 | zcnd 11689 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
ℂ) |
159 | 73 | adantr 466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℂ) |
160 | 158, 159 | npcand 10601 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑥 − 𝑀) + 𝑀) = 𝑥) |
161 | 160 | eqcomd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 = ((𝑥 − 𝑀) + 𝑀)) |
162 | | oveq1 6802 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝑥 − 𝑀) → (𝑧 + 𝑀) = ((𝑥 − 𝑀) + 𝑀)) |
163 | 162 | eqeq2d 2781 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑥 − 𝑀) → (𝑥 = (𝑧 + 𝑀) ↔ 𝑥 = ((𝑥 − 𝑀) + 𝑀))) |
164 | 163 | rspcev 3460 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 − 𝑀) ∈ ℕ ∧ 𝑥 = ((𝑥 − 𝑀) + 𝑀)) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)) |
165 | 155, 161,
164 | syl2anc 573 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)) |
166 | | vex 3354 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
167 | | eqid 2771 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) |
168 | 167 | elrnmpt 5509 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))) |
169 | 166, 168 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)) |
170 | 165, 169 | sylibr 224 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
171 | 170 | ex 397 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))) |
172 | 171 | ssrdv 3758 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
173 | | imass2 5641 |
. . . . . . . . . . . . 13
⊢
((ℤ≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) → (𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))) |
174 | 172, 173 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))) |
175 | | rnco2 5785 |
. . . . . . . . . . . . 13
⊢ ran
(𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
176 | | eqidd 2772 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
177 | 4 | feqmptd 6393 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 = (𝑤 ∈ ℕ ↦ (𝐺‘𝑤))) |
178 | | fveq2 6333 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝑧 + 𝑀) → (𝐺‘𝑤) = (𝐺‘(𝑧 + 𝑀))) |
179 | 130, 176,
177, 178 | fmptco 6541 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
180 | 179 | rneqd 5490 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
181 | 175, 180 | syl5eqr 2819 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
182 | 174, 181 | sseqtrd 3790 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
183 | | imass2 5641 |
. . . . . . . . . . 11
⊢ ((𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) → ((,) “ (𝐺 “
(ℤ≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
184 | 182, 183 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((,) “ (𝐺 “
(ℤ≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
185 | | imaco 5783 |
. . . . . . . . . 10
⊢ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) = ((,) “ (𝐺 “
(ℤ≥‘(𝑀 + 1)))) |
186 | | rnco2 5785 |
. . . . . . . . . 10
⊢ ran ((,)
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))) = ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
187 | 184, 185,
186 | 3sstr4g 3795 |
. . . . . . . . 9
⊢ (𝜑 → (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
188 | 187 | unissd 4599 |
. . . . . . . 8
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
189 | 136 | ovollb 23466 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ∧ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, <
)) |
190 | 134, 188,
189 | syl2anc 573 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, <
)) |
191 | 123 | frnd 6191 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞)) |
192 | 191, 140 | syl6ss 3764 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝑇 ⊆
ℝ*) |
193 | 192 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran 𝑇 ⊆
ℝ*) |
194 | 24 | fveq1i 6334 |
. . . . . . . . . . . . . 14
⊢ (𝑇‘(𝑀 + 𝑛)) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘(𝑀 + 𝑛)) |
195 | 26 | nnred 11240 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℝ) |
196 | 195 | ltp1d 11159 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
197 | | fzdisj 12574 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅) |
198 | 196, 197 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅) |
199 | 198 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅) |
200 | | nnnn0 11505 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
201 | | nn0addge1 11545 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℝ ∧ 𝑛 ∈ ℕ0)
→ 𝑀 ≤ (𝑀 + 𝑛)) |
202 | 195, 200,
201 | syl2an 583 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ≤ (𝑀 + 𝑛)) |
203 | 26 | adantr 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℕ) |
204 | 203, 67 | syl6eleq 2860 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈
(ℤ≥‘1)) |
205 | | nnaddcl 11247 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ) |
206 | 26, 205 | sylan 569 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ) |
207 | 206 | nnzd 11687 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℤ) |
208 | | elfz5 12540 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈
(ℤ≥‘1) ∧ (𝑀 + 𝑛) ∈ ℤ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛))) |
209 | 204, 207,
208 | syl2anc 573 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛))) |
210 | 202, 209 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ (1...(𝑀 + 𝑛))) |
211 | | fzsplit 12573 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ (1...(𝑀 + 𝑛)) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛)))) |
212 | 210, 211 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛)))) |
213 | | fzfid 12979 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) ∈ Fin) |
214 | 4 | adantr 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
215 | | elfznn 12576 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (1...(𝑀 + 𝑛)) → 𝑗 ∈ ℕ) |
216 | | ovolfcl 23453 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st
‘(𝐺‘𝑗)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1st
‘(𝐺‘𝑗)) ≤ (2nd
‘(𝐺‘𝑗)))) |
217 | 214, 215,
216 | syl2an 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
218 | 217 | simp2d 1137 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
219 | 217 | simp1d 1136 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
220 | 218, 219 | resubcld 10663 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
221 | 220 | recnd 10273 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ) |
222 | 199, 212,
213, 221 | fsumsplit 14678 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))))) |
223 | 121 | ovolfsval 23457 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
224 | 214, 215,
223 | syl2an 583 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (((abs ∘ − ) ∘
𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
225 | 206, 67 | syl6eleq 2860 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈
(ℤ≥‘1)) |
226 | 224, 225,
221 | fsumser 14668 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘(𝑀 + 𝑛))) |
227 | 4 | ad2antrr 705 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
228 | 32 | adantl 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ) |
229 | 227, 228,
223 | syl2anc 573 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → (((abs ∘ − ) ∘
𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
230 | 4, 32, 216 | syl2an 583 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
231 | 230 | simp2d 1137 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
232 | 230 | simp1d 1136 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
233 | 231, 232 | resubcld 10663 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
234 | 233 | adantlr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
235 | 234 | recnd 10273 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ) |
236 | 229, 204,
235 | fsumser 14668 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑀)) |
237 | 24 | fveq1i 6334 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇‘𝑀) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑀) |
238 | 236, 237 | syl6eqr 2823 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (𝑇‘𝑀)) |
239 | 203 | nnzd 11687 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℤ) |
240 | 239 | peano2zd 11691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℤ) |
241 | 4 | ad2antrr 705 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
242 | 203 | peano2nnd 11242 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℕ) |
243 | | elfzuz 12544 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛)) → 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) |
244 | | eluznn 11965 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑗 ∈ ℕ) |
245 | 242, 243,
244 | syl2an 583 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝑗 ∈ ℕ) |
246 | 241, 245,
216 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
247 | 246 | simp2d 1137 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
248 | 246 | simp1d 1136 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
249 | 247, 248 | resubcld 10663 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
250 | 249 | recnd 10273 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ) |
251 | | fveq2 6333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = (𝑘 + 𝑀) → (𝐺‘𝑗) = (𝐺‘(𝑘 + 𝑀))) |
252 | 251 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑘 + 𝑀) → (2nd ‘(𝐺‘𝑗)) = (2nd ‘(𝐺‘(𝑘 + 𝑀)))) |
253 | 251 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑘 + 𝑀) → (1st ‘(𝐺‘𝑗)) = (1st ‘(𝐺‘(𝑘 + 𝑀)))) |
254 | 252, 253 | oveq12d 6813 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑘 + 𝑀) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
255 | 239, 240,
207, 250, 254 | fsumshftm 14719 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
256 | 203 | nncnd 11241 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℂ) |
257 | | pncan2 10493 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 𝑀) =
1) |
258 | 256, 74, 257 | sylancl 574 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 1) − 𝑀) = 1) |
259 | | nncn 11233 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
260 | 259 | adantl 467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
261 | 256, 260 | pncan2d 10599 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 𝑛) − 𝑀) = 𝑛) |
262 | 258, 261 | oveq12d 6813 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀)) = (1...𝑛)) |
263 | 262 | sumeq1d 14638 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) = Σ𝑘 ∈ (1...𝑛)((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
264 | 134 | adantr 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
265 | | elfznn 12576 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
266 | 135 | ovolfsval 23457 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ∧ 𝑘
∈ ℕ) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)))) |
267 | 264, 265,
266 | syl2an 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘
(𝑧 ∈ ℕ ↦
(𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)))) |
268 | 265 | adantl 467 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
269 | | fvoveq1 6818 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 𝑘 → (𝐺‘(𝑧 + 𝑀)) = (𝐺‘(𝑘 + 𝑀))) |
270 | | fvex 6344 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺‘(𝑘 + 𝑀)) ∈ V |
271 | 269, 133,
270 | fvmpt 6426 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℕ → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀))) |
272 | 268, 271 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀))) |
273 | 272 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (2nd ‘(𝐺‘(𝑘 + 𝑀)))) |
274 | 272 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (1st ‘(𝐺‘(𝑘 + 𝑀)))) |
275 | 273, 274 | oveq12d 6813 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
276 | 267, 275 | eqtrd 2805 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘
(𝑧 ∈ ℕ ↦
(𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
277 | | simpr 471 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
278 | 277, 67 | syl6eleq 2860 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
279 | 4 | ad2antrr 705 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
280 | | nnaddcl 11247 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 + 𝑀) ∈ ℕ) |
281 | 265, 203,
280 | syl2anr 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 𝑀) ∈ ℕ) |
282 | | ovolfcl 23453 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (𝑘 + 𝑀) ∈ ℕ) → ((1st
‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2nd
‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1st
‘(𝐺‘(𝑘 + 𝑀))) ≤ (2nd ‘(𝐺‘(𝑘 + 𝑀))))) |
283 | 279, 281,
282 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((1st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2nd
‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1st
‘(𝐺‘(𝑘 + 𝑀))) ≤ (2nd ‘(𝐺‘(𝑘 + 𝑀))))) |
284 | 283 | simp2d 1137 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ) |
285 | 283 | simp1d 1136 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ) |
286 | 284, 285 | resubcld 10663 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℝ) |
287 | 286 | recnd 10273 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℂ) |
288 | 276, 278,
287 | fsumser 14668 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) = (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) |
289 | 255, 263,
288 | 3eqtrd 2809 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) |
290 | 238, 289 | oveq12d 6813 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))) |
291 | 222, 226,
290 | 3eqtr3d 2813 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))) |
292 | 194, 291 | syl5eq 2817 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))) |
293 | 123 | ffnd 6185 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇 Fn ℕ) |
294 | 293 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑇 Fn ℕ) |
295 | | fnfvelrn 6501 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 Fn ℕ ∧ (𝑀 + 𝑛) ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇) |
296 | 294, 206,
295 | syl2anc 573 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇) |
297 | 292, 296 | eqeltrrd 2851 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇) |
298 | | supxrub 12358 |
. . . . . . . . . . . 12
⊢ ((ran
𝑇 ⊆
ℝ* ∧ ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, <
)) |
299 | 193, 297,
298 | syl2anc 573 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, <
)) |
300 | 125 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑀) ∈ ℝ) |
301 | 138 | ffvelrnda 6504 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ (0[,)+∞)) |
302 | 120, 301 | sseldi 3750 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ ℝ) |
303 | 90 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑇, ℝ*, < )
∈ ℝ) |
304 | 300, 302,
303 | leaddsub2d 10834 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, < ) ↔ (seq1(
+ , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
305 | 299, 304 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
306 | 305 | ralrimiva 3115 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
307 | 138 | ffnd 6185 |
. . . . . . . . . 10
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ) |
308 | | breq1 4790 |
. . . . . . . . . . 11
⊢ (𝑥 = (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) → (𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
309 | 308 | ralrn 6507 |
. . . . . . . . . 10
⊢ (seq1( +
, ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ → (∀𝑥 ∈ ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
310 | 307, 309 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑥 ∈ ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
311 | 306, 310 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ran seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
312 | | supxrleub 12360 |
. . . . . . . . 9
⊢ ((ran
seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ* ∧
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀)) ∈ ℝ*) →
(sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
313 | 141, 144,
312 | syl2anc 573 |
. . . . . . . 8
⊢ (𝜑 → (sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
314 | 311, 313 | mpbird 247 |
. . . . . . 7
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀))) |
315 | 127, 143,
144, 190, 314 | xrletrd 12197 |
. . . . . 6
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
316 | 125, 90, 50 | absdifltd 14379 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶 ↔ ((sup(ran 𝑇, ℝ*, < )
− 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ*, < ) + 𝐶)))) |
317 | 27, 316 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → ((sup(ran 𝑇, ℝ*, < )
− 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ*, < ) + 𝐶))) |
318 | 317 | simpld 482 |
. . . . . . 7
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − 𝐶) < (𝑇‘𝑀)) |
319 | 90, 50, 125, 318 | ltsub23d 10837 |
. . . . . 6
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) < 𝐶) |
320 | 97, 126, 50, 315, 319 | lelttrd 10400 |
. . . . 5
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) < 𝐶) |
321 | 97, 50, 49, 320 | ltadd2dd 10401 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶)) |
322 | 13, 98, 51, 119, 321 | lelttrd 10400 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) < ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶)) |
323 | 54, 97 | readdcld 10274 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
324 | | difss 3888 |
. . . . . . . 8
⊢ (𝐾 ∖ 𝐴) ⊆ 𝐾 |
325 | | unss1 3933 |
. . . . . . . 8
⊢ ((𝐾 ∖ 𝐴) ⊆ 𝐾 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
326 | 324, 325 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
327 | 326, 88 | syl5sseqr 3803 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺)) |
328 | | ovolsscl 23473 |
. . . . . 6
⊢ ((((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran
((,) ∘ 𝐺) ⊆
ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) →
(vol*‘((𝐾 ∖
𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
329 | 327, 9, 95, 328 | syl3anc 1476 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
330 | 104 | ssdifd 3897 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∖ 𝐴)) |
331 | | difundir 4029 |
. . . . . . . 8
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∖ 𝐴) = ((𝐾 ∖ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴)) |
332 | | difss 3888 |
. . . . . . . . 9
⊢ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) |
333 | | unss2 3935 |
. . . . . . . . 9
⊢ ((∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) → ((𝐾 ∖ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
334 | 332, 333 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐾 ∖ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
335 | 331, 334 | eqsstri 3784 |
. . . . . . 7
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
336 | 330, 335 | syl6ss 3764 |
. . . . . 6
⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
337 | 327, 9 | sstrd 3762 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) |
338 | | ovolss 23472 |
. . . . . 6
⊢ (((𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∧ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) →
(vol*‘(𝐸 ∖
𝐴)) ≤
(vol*‘((𝐾 ∖
𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
339 | 336, 337,
338 | syl2anc 573 |
. . . . 5
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ≤ (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
340 | 52, 46 | sstrd 3762 |
. . . . . 6
⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ ℝ) |
341 | | ovolun 23486 |
. . . . . 6
⊢ ((((𝐾 ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ℝ ∧
(vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ)) →
(vol*‘((𝐾 ∖
𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
342 | 340, 54, 116, 97, 341 | syl22anc 1477 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
343 | 16, 329, 323, 339, 342 | letrd 10399 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
344 | 97, 50, 54, 320 | ltadd2dd 10401 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶)) |
345 | 16, 323, 55, 343, 344 | lelttrd 10400 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) < ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶)) |
346 | 13, 16, 51, 55, 322, 345 | lt2addd 10855 |
. 2
⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) < (((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶))) |
347 | 49 | recnd 10273 |
. . 3
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℂ) |
348 | 50 | recnd 10273 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℂ) |
349 | 54 | recnd 10273 |
. . 3
⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℂ) |
350 | 347, 348,
349, 348 | add4d 10469 |
. 2
⊢ (𝜑 → (((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶)) = (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶))) |
351 | 346, 350 | breqtrd 4813 |
1
⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) < (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶))) |