Step | Hyp | Ref
| Expression |
1 | | inss1 4028 |
. . . . 5
⊢ (𝐸 ∩ 𝐴) ⊆ 𝐸 |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ 𝐸) |
3 | | uniioombl.s |
. . . . 5
⊢ (𝜑 → 𝐸 ⊆ ∪ ran
((,) ∘ 𝐺)) |
4 | | uniioombl.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
5 | 4 | uniiccdif 23686 |
. . . . . . 7
⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
([,] ∘ 𝐺) ∧
(vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran
((,) ∘ 𝐺))) =
0)) |
6 | 5 | simpld 489 |
. . . . . 6
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
([,] ∘ 𝐺)) |
7 | | ovolficcss 23577 |
. . . . . . 7
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐺) ⊆
ℝ) |
8 | 4, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ) |
9 | 6, 8 | sstrd 3808 |
. . . . 5
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ) |
10 | 3, 9 | sstrd 3808 |
. . . 4
⊢ (𝜑 → 𝐸 ⊆ ℝ) |
11 | | uniioombl.e |
. . . 4
⊢ (𝜑 → (vol*‘𝐸) ∈
ℝ) |
12 | | ovolsscl 23594 |
. . . 4
⊢ (((𝐸 ∩ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∩ 𝐴)) ∈
ℝ) |
13 | 2, 10, 11, 12 | syl3anc 1491 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ∈ ℝ) |
14 | | difssd 3936 |
. . . 4
⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ 𝐸) |
15 | | ovolsscl 23594 |
. . . 4
⊢ (((𝐸 ∖ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∖
𝐴)) ∈
ℝ) |
16 | 14, 10, 11, 15 | syl3anc 1491 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ∈ ℝ) |
17 | | inss1 4028 |
. . . . . 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 23692 |
. . . . . . 7
⊢ (𝜑 → (𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ∧ (vol*‘𝐾) ∈ ℝ)) |
30 | 29 | simpld 489 |
. . . . . 6
⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
31 | | inss2 4029 |
. . . . . . . . . . . . 13
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
32 | | elfznn 12624 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ) |
33 | | ffvelrn 6583 |
. . . . . . . . . . . . . 14
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
34 | 4, 32, 33 | syl2an 590 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
35 | 31, 34 | sseldi 3796 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ ×
ℝ)) |
36 | | 1st2nd2 7440 |
. . . . . . . . . . . 12
⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) →
(𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
38 | 37 | fveq2d 6415 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉)) |
39 | | df-ov 6881 |
. . . . . . . . . 10
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉) |
40 | 38, 39 | syl6eqr 2851 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗)))) |
41 | | ioossre 12484 |
. . . . . . . . 9
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) ⊆ ℝ |
42 | 40, 41 | syl6eqss 3851 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
43 | 42 | ralrimiva 3147 |
. . . . . . 7
⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
44 | | iunss 4751 |
. . . . . . 7
⊢ (∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ ↔ ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
45 | 43, 44 | sylibr 226 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
46 | 30, 45 | eqsstrd 3835 |
. . . . 5
⊢ (𝜑 → 𝐾 ⊆ ℝ) |
47 | 29 | simprd 490 |
. . . . 5
⊢ (𝜑 → (vol*‘𝐾) ∈
ℝ) |
48 | | ovolsscl 23594 |
. . . . 5
⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∩ 𝐴)) ∈
ℝ) |
49 | 18, 46, 47, 48 | syl3anc 1491 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ) |
50 | 23 | rpred 12117 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℝ) |
51 | 49, 50 | readdcld 10358 |
. . 3
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) ∈ ℝ) |
52 | | difssd 3936 |
. . . . 5
⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ 𝐾) |
53 | | ovolsscl 23594 |
. . . . 5
⊢ (((𝐾 ∖ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∖
𝐴)) ∈
ℝ) |
54 | 52, 46, 47, 53 | syl3anc 1491 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ) |
55 | 54, 50 | readdcld 10358 |
. . 3
⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶) ∈ ℝ) |
56 | | ssun2 3975 |
. . . . . . 7
⊢ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
57 | | ioof 12521 |
. . . . . . . . . . . . . . 15
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
58 | | rexpssxrxp 10373 |
. . . . . . . . . . . . . . . . 17
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
59 | 31, 58 | sstri 3807 |
. . . . . . . . . . . . . . . 16
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
60 | | fss 6269 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
61 | 4, 59, 60 | sylancl 581 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
62 | | fco 6273 |
. . . . . . . . . . . . . . 15
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐺:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
63 | 57, 61, 62 | sylancr 582 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
64 | 63 | ffnd 6257 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ) |
65 | | fnima 6221 |
. . . . . . . . . . . . 13
⊢ (((,)
∘ 𝐺) Fn ℕ
→ (((,) ∘ 𝐺)
“ ℕ) = ran ((,) ∘ 𝐺)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = ran ((,)
∘ 𝐺)) |
67 | | nnuz 11967 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
68 | 26 | peano2nnd 11331 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 + 1) ∈ ℕ) |
69 | 68, 67 | syl6eleq 2888 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘1)) |
70 | | uzsplit 12666 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 + 1) ∈
(ℤ≥‘1) → (ℤ≥‘1) =
((1...((𝑀 + 1) − 1))
∪ (ℤ≥‘(𝑀 + 1)))) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(ℤ≥‘1) = ((1...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1)))) |
72 | 67, 71 | syl5eq 2845 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℕ = ((1...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1)))) |
73 | 26 | nncnd 11330 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ ℂ) |
74 | | ax-1cn 10282 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
75 | | pncan 10578 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 1) = 𝑀) |
76 | 73, 74, 75 | sylancl 581 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀) |
77 | 76 | oveq2d 6894 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...((𝑀 + 1) − 1)) = (1...𝑀)) |
78 | 77 | uneq1d 3964 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((1...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1))) = ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))) |
79 | 72, 78 | eqtrd 2833 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℕ = ((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
80 | 79 | imaeq2d 5683 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = (((,)
∘ 𝐺) “
((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1))))) |
81 | 66, 80 | eqtr3d 2835 |
. . . . . . . . . . 11
⊢ (𝜑 → ran ((,) ∘ 𝐺) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1))))) |
82 | | imaundi 5762 |
. . . . . . . . . . 11
⊢ (((,)
∘ 𝐺) “
((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
83 | 81, 82 | syl6eq 2849 |
. . . . . . . . . 10
⊢ (𝜑 → ran ((,) ∘ 𝐺) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
84 | 83 | unieqd 4638 |
. . . . . . . . 9
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪ ((((,)
∘ 𝐺) “
(1...𝑀)) ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
85 | | uniun 4649 |
. . . . . . . . 9
⊢ ∪ ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) = (∪
(((,) ∘ 𝐺) “
(1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
86 | 84, 85 | syl6eq 2849 |
. . . . . . . 8
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (∪ (((,)
∘ 𝐺) “
(1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
87 | 28 | uneq1i 3961 |
. . . . . . . 8
⊢ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) = (∪
(((,) ∘ 𝐺) “
(1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
88 | 86, 87 | syl6eqr 2851 |
. . . . . . 7
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
89 | 56, 88 | syl5sseqr 3850 |
. . . . . 6
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ 𝐺)) |
90 | 19, 20, 21, 22, 11, 23, 4, 3, 24, 25 | uniioombllem1 23689 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
91 | | ssid 3819 |
. . . . . . . 8
⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
((,) ∘ 𝐺) |
92 | 24 | ovollb 23587 |
. . . . . . . 8
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ∪ ran ((,) ∘
𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, <
)) |
93 | 4, 91, 92 | sylancl 581 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, <
)) |
94 | | ovollecl 23591 |
. . . . . . 7
⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ*, < )
∈ ℝ ∧ (vol*‘∪ ran ((,) ∘
𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
→ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈
ℝ) |
95 | 9, 90, 93, 94 | syl3anc 1491 |
. . . . . 6
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) |
96 | | ovolsscl 23594 |
. . . . . 6
⊢ ((∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ 𝐺) ∧
∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ) |
97 | 89, 9, 95, 96 | syl3anc 1491 |
. . . . 5
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ) |
98 | 49, 97 | readdcld 10358 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
99 | | unss1 3980 |
. . . . . . . 8
⊢ ((𝐾 ∩ 𝐴) ⊆ 𝐾 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
100 | 17, 99 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
101 | 100, 88 | syl5sseqr 3850 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺)) |
102 | | ovolsscl 23594 |
. . . . . 6
⊢ ((((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran
((,) ∘ 𝐺) ⊆
ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) →
(vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
103 | 101, 9, 95, 102 | syl3anc 1491 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
104 | 3, 88 | sseqtrd 3837 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
105 | 104 | ssrind 4035 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∩ 𝐴)) |
106 | | indir 4076 |
. . . . . . . 8
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∩ 𝐴) = ((𝐾 ∩ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴)) |
107 | | inss1 4028 |
. . . . . . . . 9
⊢ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) |
108 | | unss2 3982 |
. . . . . . . . 9
⊢ ((∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) → ((𝐾 ∩ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
109 | 107, 108 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐾 ∩ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
110 | 106, 109 | eqsstri 3831 |
. . . . . . 7
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
111 | 105, 110 | syl6ss 3810 |
. . . . . 6
⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
112 | 101, 9 | sstrd 3808 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) |
113 | | ovolss 23593 |
. . . . . 6
⊢ (((𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∧ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) →
(vol*‘(𝐸 ∩ 𝐴)) ≤ (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
114 | 111, 112,
113 | syl2anc 580 |
. . . . 5
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ≤ (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
115 | 18, 46 | sstrd 3808 |
. . . . . 6
⊢ (𝜑 → (𝐾 ∩ 𝐴) ⊆ ℝ) |
116 | 89, 9 | sstrd 3808 |
. . . . . 6
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ℝ) |
117 | | ovolun 23607 |
. . . . . 6
⊢ ((((𝐾 ∩ 𝐴) ⊆ ℝ ∧ (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ℝ ∧
(vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ)) →
(vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
118 | 115, 49, 116, 97, 117 | syl22anc 868 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
119 | 13, 103, 98, 114, 118 | letrd 10484 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
120 | | rge0ssre 12531 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℝ |
121 | | eqid 2799 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) |
122 | 121, 24 | ovolsf 23580 |
. . . . . . . . . 10
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞)) |
123 | 4, 122 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞)) |
124 | 123, 26 | ffvelrnd 6586 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘𝑀) ∈ (0[,)+∞)) |
125 | 120, 124 | sseldi 3796 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘𝑀) ∈ ℝ) |
126 | 90, 125 | resubcld 10750 |
. . . . . 6
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ∈ ℝ) |
127 | 97 | rexrd 10378 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈
ℝ*) |
128 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℕ) |
129 | | nnaddcl 11336 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ) |
130 | 128, 26, 129 | syl2anr 591 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ) |
131 | 4 | ffvelrnda 6585 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 + 𝑀) ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
132 | 130, 131 | syldan 586 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
133 | 132 | fmpttd 6611 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
134 | | eqid 2799 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((abs ∘ − ) ∘
(𝑧 ∈ ℕ ↦
(𝐺‘(𝑧 + 𝑀)))) |
135 | | eqid 2799 |
. . . . . . . . . . . 12
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) = seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀))))) |
136 | 134, 135 | ovolsf 23580 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞)) |
137 | 133, 136 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞)) |
138 | 137 | frnd 6263 |
. . . . . . . . 9
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆
(0[,)+∞)) |
139 | | icossxr 12507 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ* |
140 | 138, 139 | syl6ss 3810 |
. . . . . . . 8
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆
ℝ*) |
141 | | supxrcl 12394 |
. . . . . . . 8
⊢ (ran
seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ* →
sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ∈
ℝ*) |
142 | 140, 141 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ∈
ℝ*) |
143 | 126 | rexrd 10378 |
. . . . . . 7
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ∈
ℝ*) |
144 | | 1zzd 11698 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 1 ∈
ℤ) |
145 | 26 | nnzd 11771 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℤ) |
146 | 145 | adantr 473 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℤ) |
147 | | addcom 10512 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑀 + 1) =
(1 + 𝑀)) |
148 | 73, 74, 147 | sylancl 581 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑀 + 1) = (1 + 𝑀)) |
149 | 148 | fveq2d 6415 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) = (ℤ≥‘(1 +
𝑀))) |
150 | 149 | eleq2d 2864 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑥 ∈ (ℤ≥‘(𝑀 + 1)) ↔ 𝑥 ∈ (ℤ≥‘(1 +
𝑀)))) |
151 | 150 | biimpa 469 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
(ℤ≥‘(1 + 𝑀))) |
152 | | eluzsub 11960 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℤ ∧ 𝑀
∈ ℤ ∧ 𝑥
∈ (ℤ≥‘(1 + 𝑀))) → (𝑥 − 𝑀) ∈
(ℤ≥‘1)) |
153 | 144, 146,
151, 152 | syl3anc 1491 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈
(ℤ≥‘1)) |
154 | 153, 67 | syl6eleqr 2889 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈ ℕ) |
155 | | eluzelz 11940 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑥 ∈ ℤ) |
156 | 155 | adantl 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
ℤ) |
157 | 156 | zcnd 11773 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
ℂ) |
158 | 73 | adantr 473 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℂ) |
159 | 157, 158 | npcand 10688 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑥 − 𝑀) + 𝑀) = 𝑥) |
160 | 159 | eqcomd 2805 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 = ((𝑥 − 𝑀) + 𝑀)) |
161 | | oveq1 6885 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑥 − 𝑀) → (𝑧 + 𝑀) = ((𝑥 − 𝑀) + 𝑀)) |
162 | 161 | rspceeqv 3515 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 − 𝑀) ∈ ℕ ∧ 𝑥 = ((𝑥 − 𝑀) + 𝑀)) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)) |
163 | 154, 160,
162 | syl2anc 580 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)) |
164 | | vex 3388 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
165 | | eqid 2799 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) |
166 | 165 | elrnmpt 5576 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))) |
167 | 164, 166 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)) |
168 | 163, 167 | sylibr 226 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
169 | 168 | ex 402 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))) |
170 | 169 | ssrdv 3804 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
171 | | imass2 5718 |
. . . . . . . . . . . . 13
⊢
((ℤ≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) → (𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))) |
172 | 170, 171 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))) |
173 | | rnco2 5861 |
. . . . . . . . . . . . 13
⊢ ran
(𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
174 | | eqidd 2800 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
175 | 4 | feqmptd 6474 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 = (𝑤 ∈ ℕ ↦ (𝐺‘𝑤))) |
176 | | fveq2 6411 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝑧 + 𝑀) → (𝐺‘𝑤) = (𝐺‘(𝑧 + 𝑀))) |
177 | 130, 174,
175, 176 | fmptco 6623 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
178 | 177 | rneqd 5556 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
179 | 173, 178 | syl5eqr 2847 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
180 | 172, 179 | sseqtrd 3837 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
181 | | imass2 5718 |
. . . . . . . . . . 11
⊢ ((𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) → ((,) “ (𝐺 “
(ℤ≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
182 | 180, 181 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((,) “ (𝐺 “
(ℤ≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
183 | | imaco 5859 |
. . . . . . . . . 10
⊢ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) = ((,) “ (𝐺 “
(ℤ≥‘(𝑀 + 1)))) |
184 | | rnco2 5861 |
. . . . . . . . . 10
⊢ ran ((,)
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))) = ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
185 | 182, 183,
184 | 3sstr4g 3842 |
. . . . . . . . 9
⊢ (𝜑 → (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
186 | 185 | unissd 4654 |
. . . . . . . 8
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
187 | 135 | ovollb 23587 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ∧ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, <
)) |
188 | 133, 186,
187 | syl2anc 580 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, <
)) |
189 | 123 | frnd 6263 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞)) |
190 | 189, 139 | syl6ss 3810 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝑇 ⊆
ℝ*) |
191 | 190 | adantr 473 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran 𝑇 ⊆
ℝ*) |
192 | 24 | fveq1i 6412 |
. . . . . . . . . . . . . 14
⊢ (𝑇‘(𝑀 + 𝑛)) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘(𝑀 + 𝑛)) |
193 | 26 | nnred 11329 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℝ) |
194 | 193 | ltp1d 11246 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
195 | | fzdisj 12622 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅) |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅) |
197 | 196 | adantr 473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅) |
198 | | nnnn0 11588 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
199 | | nn0addge1 11628 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℝ ∧ 𝑛 ∈ ℕ0)
→ 𝑀 ≤ (𝑀 + 𝑛)) |
200 | 193, 198,
199 | syl2an 590 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ≤ (𝑀 + 𝑛)) |
201 | 26 | adantr 473 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℕ) |
202 | 201, 67 | syl6eleq 2888 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈
(ℤ≥‘1)) |
203 | | nnaddcl 11336 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ) |
204 | 26, 203 | sylan 576 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ) |
205 | 204 | nnzd 11771 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℤ) |
206 | | elfz5 12588 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈
(ℤ≥‘1) ∧ (𝑀 + 𝑛) ∈ ℤ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛))) |
207 | 202, 205,
206 | syl2anc 580 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛))) |
208 | 200, 207 | mpbird 249 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ (1...(𝑀 + 𝑛))) |
209 | | fzsplit 12621 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ (1...(𝑀 + 𝑛)) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛)))) |
210 | 208, 209 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛)))) |
211 | | fzfid 13027 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) ∈ Fin) |
212 | 4 | adantr 473 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
213 | | elfznn 12624 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (1...(𝑀 + 𝑛)) → 𝑗 ∈ ℕ) |
214 | | ovolfcl 23574 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st
‘(𝐺‘𝑗)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1st
‘(𝐺‘𝑗)) ≤ (2nd
‘(𝐺‘𝑗)))) |
215 | 212, 213,
214 | syl2an 590 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
216 | 215 | simp2d 1174 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
217 | 215 | simp1d 1173 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
218 | 216, 217 | resubcld 10750 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
219 | 218 | recnd 10357 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ) |
220 | 197, 210,
211, 219 | fsumsplit 14812 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))))) |
221 | 121 | ovolfsval 23578 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
222 | 212, 213,
221 | syl2an 590 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (((abs ∘ − ) ∘
𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
223 | 204, 67 | syl6eleq 2888 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈
(ℤ≥‘1)) |
224 | 222, 223,
219 | fsumser 14802 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘(𝑀 + 𝑛))) |
225 | 4 | ad2antrr 718 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
226 | 32 | adantl 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ) |
227 | 225, 226,
221 | syl2anc 580 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → (((abs ∘ − ) ∘
𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
228 | 4, 32, 214 | syl2an 590 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
229 | 228 | simp2d 1174 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
230 | 228 | simp1d 1173 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
231 | 229, 230 | resubcld 10750 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
232 | 231 | adantlr 707 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
233 | 232 | recnd 10357 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ) |
234 | 227, 202,
233 | fsumser 14802 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑀)) |
235 | 24 | fveq1i 6412 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇‘𝑀) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑀) |
236 | 234, 235 | syl6eqr 2851 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (𝑇‘𝑀)) |
237 | 201 | nnzd 11771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℤ) |
238 | 237 | peano2zd 11775 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℤ) |
239 | 4 | ad2antrr 718 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
240 | 201 | peano2nnd 11331 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℕ) |
241 | | elfzuz 12592 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛)) → 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) |
242 | | eluznn 12003 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑗 ∈ ℕ) |
243 | 240, 241,
242 | syl2an 590 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝑗 ∈ ℕ) |
244 | 239, 243,
214 | syl2anc 580 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
245 | 244 | simp2d 1174 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
246 | 244 | simp1d 1173 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
247 | 245, 246 | resubcld 10750 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
248 | 247 | recnd 10357 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ) |
249 | | 2fveq3 6416 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑘 + 𝑀) → (2nd ‘(𝐺‘𝑗)) = (2nd ‘(𝐺‘(𝑘 + 𝑀)))) |
250 | | 2fveq3 6416 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑘 + 𝑀) → (1st ‘(𝐺‘𝑗)) = (1st ‘(𝐺‘(𝑘 + 𝑀)))) |
251 | 249, 250 | oveq12d 6896 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑘 + 𝑀) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
252 | 237, 238,
205, 248, 251 | fsumshftm 14851 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
253 | 201 | nncnd 11330 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℂ) |
254 | | pncan2 10579 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 𝑀) =
1) |
255 | 253, 74, 254 | sylancl 581 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 1) − 𝑀) = 1) |
256 | | nncn 11321 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
257 | 256 | adantl 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
258 | 253, 257 | pncan2d 10686 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 𝑛) − 𝑀) = 𝑛) |
259 | 255, 258 | oveq12d 6896 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀)) = (1...𝑛)) |
260 | 259 | sumeq1d 14772 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) = Σ𝑘 ∈ (1...𝑛)((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
261 | 133 | adantr 473 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
262 | | elfznn 12624 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
263 | 134 | ovolfsval 23578 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ∧ 𝑘
∈ ℕ) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)))) |
264 | 261, 262,
263 | syl2an 590 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘
(𝑧 ∈ ℕ ↦
(𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)))) |
265 | 262 | adantl 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
266 | | fvoveq1 6901 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 𝑘 → (𝐺‘(𝑧 + 𝑀)) = (𝐺‘(𝑘 + 𝑀))) |
267 | | eqid 2799 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) |
268 | | fvex 6424 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺‘(𝑘 + 𝑀)) ∈ V |
269 | 266, 267,
268 | fvmpt 6507 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℕ → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀))) |
270 | 265, 269 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀))) |
271 | 270 | fveq2d 6415 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (2nd ‘(𝐺‘(𝑘 + 𝑀)))) |
272 | 270 | fveq2d 6415 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (1st ‘(𝐺‘(𝑘 + 𝑀)))) |
273 | 271, 272 | oveq12d 6896 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
274 | 264, 273 | eqtrd 2833 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘
(𝑧 ∈ ℕ ↦
(𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
275 | | simpr 478 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
276 | 275, 67 | syl6eleq 2888 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
277 | 4 | ad2antrr 718 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
278 | | nnaddcl 11336 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 + 𝑀) ∈ ℕ) |
279 | 262, 201,
278 | syl2anr 591 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 𝑀) ∈ ℕ) |
280 | | ovolfcl 23574 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (𝑘 + 𝑀) ∈ ℕ) → ((1st
‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2nd
‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1st
‘(𝐺‘(𝑘 + 𝑀))) ≤ (2nd ‘(𝐺‘(𝑘 + 𝑀))))) |
281 | 277, 279,
280 | syl2anc 580 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((1st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2nd
‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1st
‘(𝐺‘(𝑘 + 𝑀))) ≤ (2nd ‘(𝐺‘(𝑘 + 𝑀))))) |
282 | 281 | simp2d 1174 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ) |
283 | 281 | simp1d 1173 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ) |
284 | 282, 283 | resubcld 10750 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℝ) |
285 | 284 | recnd 10357 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℂ) |
286 | 274, 276,
285 | fsumser 14802 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) = (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) |
287 | 252, 260,
286 | 3eqtrd 2837 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) |
288 | 236, 287 | oveq12d 6896 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))) |
289 | 220, 224,
288 | 3eqtr3d 2841 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))) |
290 | 192, 289 | syl5eq 2845 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))) |
291 | 123 | ffnd 6257 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇 Fn ℕ) |
292 | 291 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑇 Fn ℕ) |
293 | | fnfvelrn 6582 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 Fn ℕ ∧ (𝑀 + 𝑛) ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇) |
294 | 292, 204,
293 | syl2anc 580 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇) |
295 | 290, 294 | eqeltrrd 2879 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇) |
296 | | supxrub 12403 |
. . . . . . . . . . . 12
⊢ ((ran
𝑇 ⊆
ℝ* ∧ ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, <
)) |
297 | 191, 295,
296 | syl2anc 580 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, <
)) |
298 | 125 | adantr 473 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑀) ∈ ℝ) |
299 | 137 | ffvelrnda 6585 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ (0[,)+∞)) |
300 | 120, 299 | sseldi 3796 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ ℝ) |
301 | 90 | adantr 473 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑇, ℝ*, < )
∈ ℝ) |
302 | 298, 300,
301 | leaddsub2d 10921 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, < ) ↔ (seq1(
+ , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
303 | 297, 302 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
304 | 303 | ralrimiva 3147 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
305 | 137 | ffnd 6257 |
. . . . . . . . . 10
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ) |
306 | | breq1 4846 |
. . . . . . . . . . 11
⊢ (𝑥 = (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) → (𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
307 | 306 | ralrn 6588 |
. . . . . . . . . 10
⊢ (seq1( +
, ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ → (∀𝑥 ∈ ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
308 | 305, 307 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑥 ∈ ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
309 | 304, 308 | mpbird 249 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ran seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
310 | | supxrleub 12405 |
. . . . . . . . 9
⊢ ((ran
seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ* ∧
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀)) ∈ ℝ*) →
(sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
311 | 140, 143,
310 | syl2anc 580 |
. . . . . . . 8
⊢ (𝜑 → (sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
312 | 309, 311 | mpbird 249 |
. . . . . . 7
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀))) |
313 | 127, 142,
143, 188, 312 | xrletrd 12242 |
. . . . . 6
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
314 | 125, 90, 50 | absdifltd 14513 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶 ↔ ((sup(ran 𝑇, ℝ*, < )
− 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ*, < ) + 𝐶)))) |
315 | 27, 314 | mpbid 224 |
. . . . . . . 8
⊢ (𝜑 → ((sup(ran 𝑇, ℝ*, < )
− 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ*, < ) + 𝐶))) |
316 | 315 | simpld 489 |
. . . . . . 7
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − 𝐶) < (𝑇‘𝑀)) |
317 | 90, 50, 125, 316 | ltsub23d 10924 |
. . . . . 6
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) < 𝐶) |
318 | 97, 126, 50, 313, 317 | lelttrd 10485 |
. . . . 5
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) < 𝐶) |
319 | 97, 50, 49, 318 | ltadd2dd 10486 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶)) |
320 | 13, 98, 51, 119, 319 | lelttrd 10485 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) < ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶)) |
321 | 54, 97 | readdcld 10358 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
322 | | difss 3935 |
. . . . . . . 8
⊢ (𝐾 ∖ 𝐴) ⊆ 𝐾 |
323 | | unss1 3980 |
. . . . . . . 8
⊢ ((𝐾 ∖ 𝐴) ⊆ 𝐾 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
324 | 322, 323 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
325 | 324, 88 | syl5sseqr 3850 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺)) |
326 | | ovolsscl 23594 |
. . . . . 6
⊢ ((((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran
((,) ∘ 𝐺) ⊆
ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) →
(vol*‘((𝐾 ∖
𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
327 | 325, 9, 95, 326 | syl3anc 1491 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
328 | 104 | ssdifd 3944 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∖ 𝐴)) |
329 | | difundir 4081 |
. . . . . . . 8
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∖ 𝐴) = ((𝐾 ∖ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴)) |
330 | | difss 3935 |
. . . . . . . . 9
⊢ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) |
331 | | unss2 3982 |
. . . . . . . . 9
⊢ ((∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) → ((𝐾 ∖ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
332 | 330, 331 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐾 ∖ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
333 | 329, 332 | eqsstri 3831 |
. . . . . . 7
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
334 | 328, 333 | syl6ss 3810 |
. . . . . 6
⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
335 | 325, 9 | sstrd 3808 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) |
336 | | ovolss 23593 |
. . . . . 6
⊢ (((𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∧ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) →
(vol*‘(𝐸 ∖
𝐴)) ≤
(vol*‘((𝐾 ∖
𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
337 | 334, 335,
336 | syl2anc 580 |
. . . . 5
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ≤ (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
338 | 52, 46 | sstrd 3808 |
. . . . . 6
⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ ℝ) |
339 | | ovolun 23607 |
. . . . . 6
⊢ ((((𝐾 ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ℝ ∧
(vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ)) →
(vol*‘((𝐾 ∖
𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
340 | 338, 54, 116, 97, 339 | syl22anc 868 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
341 | 16, 327, 321, 337, 340 | letrd 10484 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
342 | 97, 50, 54, 318 | ltadd2dd 10486 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶)) |
343 | 16, 321, 55, 341, 342 | lelttrd 10485 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) < ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶)) |
344 | 13, 16, 51, 55, 320, 343 | lt2addd 10942 |
. 2
⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) < (((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶))) |
345 | 49 | recnd 10357 |
. . 3
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℂ) |
346 | 50 | recnd 10357 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℂ) |
347 | 54 | recnd 10357 |
. . 3
⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℂ) |
348 | 345, 346,
347, 346 | add4d 10554 |
. 2
⊢ (𝜑 → (((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶)) = (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶))) |
349 | 344, 348 | breqtrd 4869 |
1
⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) < (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶))) |