Step | Hyp | Ref
| Expression |
1 | | inss1 4119 |
. . . . 5
⊢ (𝐸 ∩ 𝐴) ⊆ 𝐸 |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ 𝐸) |
3 | | uniioombl.s |
. . . . 5
⊢ (𝜑 → 𝐸 ⊆ ∪ ran
((,) ∘ 𝐺)) |
4 | | uniioombl.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
5 | 4 | uniiccdif 24330 |
. . . . . . 7
⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
([,] ∘ 𝐺) ∧
(vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran
((,) ∘ 𝐺))) =
0)) |
6 | 5 | simpld 498 |
. . . . . 6
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
([,] ∘ 𝐺)) |
7 | | ovolficcss 24221 |
. . . . . . 7
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐺) ⊆
ℝ) |
8 | 4, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ) |
9 | 6, 8 | sstrd 3887 |
. . . . 5
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ) |
10 | 3, 9 | sstrd 3887 |
. . . 4
⊢ (𝜑 → 𝐸 ⊆ ℝ) |
11 | | uniioombl.e |
. . . 4
⊢ (𝜑 → (vol*‘𝐸) ∈
ℝ) |
12 | | ovolsscl 24238 |
. . . 4
⊢ (((𝐸 ∩ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∩ 𝐴)) ∈
ℝ) |
13 | 2, 10, 11, 12 | syl3anc 1372 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ∈ ℝ) |
14 | | difssd 4023 |
. . . 4
⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ 𝐸) |
15 | | ovolsscl 24238 |
. . . 4
⊢ (((𝐸 ∖ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∖
𝐴)) ∈
ℝ) |
16 | 14, 10, 11, 15 | syl3anc 1372 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ∈ ℝ) |
17 | | inss1 4119 |
. . . . . 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 24336 |
. . . . . . 7
⊢ (𝜑 → (𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ∧ (vol*‘𝐾) ∈ ℝ)) |
30 | 29 | simpld 498 |
. . . . . 6
⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
31 | | inss2 4120 |
. . . . . . . . . . . . 13
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
32 | | elfznn 13027 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ) |
33 | | ffvelrn 6859 |
. . . . . . . . . . . . . 14
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
34 | 4, 32, 33 | syl2an 599 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
35 | 31, 34 | sseldi 3875 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ ×
ℝ)) |
36 | | 1st2nd2 7753 |
. . . . . . . . . . . 12
⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) →
(𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
38 | 37 | fveq2d 6678 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉)) |
39 | | df-ov 7173 |
. . . . . . . . . 10
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉) |
40 | 38, 39 | eqtr4di 2791 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗)))) |
41 | | ioossre 12882 |
. . . . . . . . 9
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) ⊆ ℝ |
42 | 40, 41 | eqsstrdi 3931 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
43 | 42 | ralrimiva 3096 |
. . . . . . 7
⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
44 | | iunss 4931 |
. . . . . . 7
⊢ (∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ ↔ ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
45 | 43, 44 | sylibr 237 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
46 | 30, 45 | eqsstrd 3915 |
. . . . 5
⊢ (𝜑 → 𝐾 ⊆ ℝ) |
47 | 29 | simprd 499 |
. . . . 5
⊢ (𝜑 → (vol*‘𝐾) ∈
ℝ) |
48 | | ovolsscl 24238 |
. . . . 5
⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∩ 𝐴)) ∈
ℝ) |
49 | 18, 46, 47, 48 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ) |
50 | 23 | rpred 12514 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℝ) |
51 | 49, 50 | readdcld 10748 |
. . 3
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) ∈ ℝ) |
52 | | difssd 4023 |
. . . . 5
⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ 𝐾) |
53 | | ovolsscl 24238 |
. . . . 5
⊢ (((𝐾 ∖ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∖
𝐴)) ∈
ℝ) |
54 | 52, 46, 47, 53 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ) |
55 | 54, 50 | readdcld 10748 |
. . 3
⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶) ∈ ℝ) |
56 | | ssun2 4063 |
. . . . . . 7
⊢ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
57 | | ioof 12921 |
. . . . . . . . . . . . . . 15
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
58 | | rexpssxrxp 10764 |
. . . . . . . . . . . . . . . . 17
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
59 | 31, 58 | sstri 3886 |
. . . . . . . . . . . . . . . 16
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
60 | | fss 6521 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
61 | 4, 59, 60 | sylancl 589 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
62 | | fco 6528 |
. . . . . . . . . . . . . . 15
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐺:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
63 | 57, 61, 62 | sylancr 590 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
64 | 63 | ffnd 6505 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ) |
65 | | fnima 6467 |
. . . . . . . . . . . . 13
⊢ (((,)
∘ 𝐺) Fn ℕ
→ (((,) ∘ 𝐺)
“ ℕ) = ran ((,) ∘ 𝐺)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = ran ((,)
∘ 𝐺)) |
67 | | nnuz 12363 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
68 | 26 | peano2nnd 11733 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 + 1) ∈ ℕ) |
69 | 68, 67 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘1)) |
70 | | uzsplit 13070 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 + 1) ∈
(ℤ≥‘1) → (ℤ≥‘1) =
((1...((𝑀 + 1) − 1))
∪ (ℤ≥‘(𝑀 + 1)))) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(ℤ≥‘1) = ((1...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1)))) |
72 | 67, 71 | syl5eq 2785 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℕ = ((1...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1)))) |
73 | 26 | nncnd 11732 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ ℂ) |
74 | | ax-1cn 10673 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
75 | | pncan 10970 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 1) = 𝑀) |
76 | 73, 74, 75 | sylancl 589 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀) |
77 | 76 | oveq2d 7186 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...((𝑀 + 1) − 1)) = (1...𝑀)) |
78 | 77 | uneq1d 4052 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((1...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1))) = ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))) |
79 | 72, 78 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℕ = ((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
80 | 79 | imaeq2d 5903 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = (((,)
∘ 𝐺) “
((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1))))) |
81 | 66, 80 | eqtr3d 2775 |
. . . . . . . . . . 11
⊢ (𝜑 → ran ((,) ∘ 𝐺) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1))))) |
82 | | imaundi 5982 |
. . . . . . . . . . 11
⊢ (((,)
∘ 𝐺) “
((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
83 | 81, 82 | eqtrdi 2789 |
. . . . . . . . . 10
⊢ (𝜑 → ran ((,) ∘ 𝐺) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
84 | 83 | unieqd 4810 |
. . . . . . . . 9
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪ ((((,)
∘ 𝐺) “
(1...𝑀)) ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
85 | | uniun 4821 |
. . . . . . . . 9
⊢ ∪ ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) = (∪
(((,) ∘ 𝐺) “
(1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
86 | 84, 85 | eqtrdi 2789 |
. . . . . . . 8
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (∪ (((,)
∘ 𝐺) “
(1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
87 | 28 | uneq1i 4049 |
. . . . . . . 8
⊢ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) = (∪
(((,) ∘ 𝐺) “
(1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
88 | 86, 87 | eqtr4di 2791 |
. . . . . . 7
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
89 | 56, 88 | sseqtrrid 3930 |
. . . . . 6
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ 𝐺)) |
90 | 19, 20, 21, 22, 11, 23, 4, 3, 24, 25 | uniioombllem1 24333 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
91 | | ssid 3899 |
. . . . . . . 8
⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
((,) ∘ 𝐺) |
92 | 24 | ovollb 24231 |
. . . . . . . 8
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ∪ ran ((,) ∘
𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, <
)) |
93 | 4, 91, 92 | sylancl 589 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, <
)) |
94 | | ovollecl 24235 |
. . . . . . 7
⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ*, < )
∈ ℝ ∧ (vol*‘∪ ran ((,) ∘
𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
→ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈
ℝ) |
95 | 9, 90, 93, 94 | syl3anc 1372 |
. . . . . 6
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) |
96 | | ovolsscl 24238 |
. . . . . 6
⊢ ((∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ 𝐺) ∧
∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ) |
97 | 89, 9, 95, 96 | syl3anc 1372 |
. . . . 5
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ) |
98 | 49, 97 | readdcld 10748 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
99 | | unss1 4069 |
. . . . . . . 8
⊢ ((𝐾 ∩ 𝐴) ⊆ 𝐾 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
100 | 17, 99 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
101 | 100, 88 | sseqtrrid 3930 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺)) |
102 | | ovolsscl 24238 |
. . . . . 6
⊢ ((((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran
((,) ∘ 𝐺) ⊆
ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) →
(vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
103 | 101, 9, 95, 102 | syl3anc 1372 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
104 | 3, 88 | sseqtrd 3917 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
105 | 104 | ssrind 4126 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∩ 𝐴)) |
106 | | indir 4166 |
. . . . . . . 8
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∩ 𝐴) = ((𝐾 ∩ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴)) |
107 | | inss1 4119 |
. . . . . . . . 9
⊢ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) |
108 | | unss2 4071 |
. . . . . . . . 9
⊢ ((∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) → ((𝐾 ∩ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
109 | 107, 108 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐾 ∩ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
110 | 106, 109 | eqsstri 3911 |
. . . . . . 7
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
111 | 105, 110 | sstrdi 3889 |
. . . . . 6
⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
112 | 101, 9 | sstrd 3887 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) |
113 | | ovolss 24237 |
. . . . . 6
⊢ (((𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∧ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) →
(vol*‘(𝐸 ∩ 𝐴)) ≤ (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
114 | 111, 112,
113 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ≤ (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
115 | 18, 46 | sstrd 3887 |
. . . . . 6
⊢ (𝜑 → (𝐾 ∩ 𝐴) ⊆ ℝ) |
116 | 89, 9 | sstrd 3887 |
. . . . . 6
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ℝ) |
117 | | ovolun 24251 |
. . . . . 6
⊢ ((((𝐾 ∩ 𝐴) ⊆ ℝ ∧ (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ℝ ∧
(vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ)) →
(vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
118 | 115, 49, 116, 97, 117 | syl22anc 838 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
119 | 13, 103, 98, 114, 118 | letrd 10875 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
120 | | rge0ssre 12930 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℝ |
121 | | eqid 2738 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) |
122 | 121, 24 | ovolsf 24224 |
. . . . . . . . . 10
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞)) |
123 | 4, 122 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞)) |
124 | 123, 26 | ffvelrnd 6862 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘𝑀) ∈ (0[,)+∞)) |
125 | 120, 124 | sseldi 3875 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘𝑀) ∈ ℝ) |
126 | 90, 125 | resubcld 11146 |
. . . . . 6
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ∈ ℝ) |
127 | 97 | rexrd 10769 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈
ℝ*) |
128 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℕ) |
129 | | nnaddcl 11739 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ) |
130 | 128, 26, 129 | syl2anr 600 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ) |
131 | 4 | ffvelrnda 6861 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 + 𝑀) ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
132 | 130, 131 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
133 | 132 | fmpttd 6889 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
134 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((abs ∘ − ) ∘
(𝑧 ∈ ℕ ↦
(𝐺‘(𝑧 + 𝑀)))) |
135 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) = seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀))))) |
136 | 134, 135 | ovolsf 24224 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞)) |
137 | 133, 136 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞)) |
138 | 137 | frnd 6512 |
. . . . . . . . 9
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆
(0[,)+∞)) |
139 | | icossxr 12906 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ* |
140 | 138, 139 | sstrdi 3889 |
. . . . . . . 8
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆
ℝ*) |
141 | | supxrcl 12791 |
. . . . . . . 8
⊢ (ran
seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ* →
sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ∈
ℝ*) |
142 | 140, 141 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ∈
ℝ*) |
143 | 126 | rexrd 10769 |
. . . . . . 7
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ∈
ℝ*) |
144 | | 1zzd 12094 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 1 ∈
ℤ) |
145 | 26 | nnzd 12167 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℤ) |
146 | 145 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℤ) |
147 | | addcom 10904 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑀 + 1) =
(1 + 𝑀)) |
148 | 73, 74, 147 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑀 + 1) = (1 + 𝑀)) |
149 | 148 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) = (ℤ≥‘(1 +
𝑀))) |
150 | 149 | eleq2d 2818 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑥 ∈ (ℤ≥‘(𝑀 + 1)) ↔ 𝑥 ∈ (ℤ≥‘(1 +
𝑀)))) |
151 | 150 | biimpa 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
(ℤ≥‘(1 + 𝑀))) |
152 | | eluzsub 12356 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℤ ∧ 𝑀
∈ ℤ ∧ 𝑥
∈ (ℤ≥‘(1 + 𝑀))) → (𝑥 − 𝑀) ∈
(ℤ≥‘1)) |
153 | 144, 146,
151, 152 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈
(ℤ≥‘1)) |
154 | 153, 67 | eleqtrrdi 2844 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈ ℕ) |
155 | | eluzelz 12334 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑥 ∈ ℤ) |
156 | 155 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
ℤ) |
157 | 156 | zcnd 12169 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
ℂ) |
158 | 73 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℂ) |
159 | 157, 158 | npcand 11079 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑥 − 𝑀) + 𝑀) = 𝑥) |
160 | 159 | eqcomd 2744 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 = ((𝑥 − 𝑀) + 𝑀)) |
161 | | oveq1 7177 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑥 − 𝑀) → (𝑧 + 𝑀) = ((𝑥 − 𝑀) + 𝑀)) |
162 | 161 | rspceeqv 3541 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 − 𝑀) ∈ ℕ ∧ 𝑥 = ((𝑥 − 𝑀) + 𝑀)) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)) |
163 | 154, 160,
162 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)) |
164 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) |
165 | 164 | elrnmpt 5799 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))) |
166 | 165 | elv 3404 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)) |
167 | 163, 166 | sylibr 237 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
168 | 167 | ex 416 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))) |
169 | 168 | ssrdv 3883 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
170 | | imass2 5939 |
. . . . . . . . . . . . 13
⊢
((ℤ≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) → (𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))) |
171 | 169, 170 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))) |
172 | | rnco2 6086 |
. . . . . . . . . . . . 13
⊢ ran
(𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
173 | 4, 130 | cofmpt 6904 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
174 | 173 | rneqd 5781 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
175 | 172, 174 | eqtr3id 2787 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
176 | 171, 175 | sseqtrd 3917 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
177 | | imass2 5939 |
. . . . . . . . . . 11
⊢ ((𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) → ((,) “ (𝐺 “
(ℤ≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
178 | 176, 177 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((,) “ (𝐺 “
(ℤ≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
179 | | imaco 6084 |
. . . . . . . . . 10
⊢ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) = ((,) “ (𝐺 “
(ℤ≥‘(𝑀 + 1)))) |
180 | | rnco2 6086 |
. . . . . . . . . 10
⊢ ran ((,)
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))) = ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
181 | 178, 179,
180 | 3sstr4g 3922 |
. . . . . . . . 9
⊢ (𝜑 → (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
182 | 181 | unissd 4806 |
. . . . . . . 8
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
183 | 135 | ovollb 24231 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ∧ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, <
)) |
184 | 133, 182,
183 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, <
)) |
185 | 123 | frnd 6512 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞)) |
186 | 185, 139 | sstrdi 3889 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝑇 ⊆
ℝ*) |
187 | 24 | fveq1i 6675 |
. . . . . . . . . . . . . 14
⊢ (𝑇‘(𝑀 + 𝑛)) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘(𝑀 + 𝑛)) |
188 | 26 | nnred 11731 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℝ) |
189 | 188 | ltp1d 11648 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
190 | | fzdisj 13025 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅) |
191 | 189, 190 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅) |
192 | 191 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅) |
193 | | nnnn0 11983 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
194 | | nn0addge1 12022 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℝ ∧ 𝑛 ∈ ℕ0)
→ 𝑀 ≤ (𝑀 + 𝑛)) |
195 | 188, 193,
194 | syl2an 599 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ≤ (𝑀 + 𝑛)) |
196 | 26 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℕ) |
197 | 196, 67 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈
(ℤ≥‘1)) |
198 | | nnaddcl 11739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ) |
199 | 26, 198 | sylan 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ) |
200 | 199 | nnzd 12167 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℤ) |
201 | | elfz5 12990 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈
(ℤ≥‘1) ∧ (𝑀 + 𝑛) ∈ ℤ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛))) |
202 | 197, 200,
201 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛))) |
203 | 195, 202 | mpbird 260 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ (1...(𝑀 + 𝑛))) |
204 | | fzsplit 13024 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ (1...(𝑀 + 𝑛)) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛)))) |
205 | 203, 204 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛)))) |
206 | | fzfid 13432 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) ∈ Fin) |
207 | 4 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
208 | | elfznn 13027 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (1...(𝑀 + 𝑛)) → 𝑗 ∈ ℕ) |
209 | | ovolfcl 24218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st
‘(𝐺‘𝑗)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1st
‘(𝐺‘𝑗)) ≤ (2nd
‘(𝐺‘𝑗)))) |
210 | 207, 208,
209 | syl2an 599 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
211 | 210 | simp2d 1144 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
212 | 210 | simp1d 1143 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
213 | 211, 212 | resubcld 11146 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
214 | 213 | recnd 10747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ) |
215 | 192, 205,
206, 214 | fsumsplit 15190 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))))) |
216 | 121 | ovolfsval 24222 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
217 | 207, 208,
216 | syl2an 599 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (((abs ∘ − ) ∘
𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
218 | 199, 67 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈
(ℤ≥‘1)) |
219 | 217, 218,
214 | fsumser 15180 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘(𝑀 + 𝑛))) |
220 | 4 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
221 | 32 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ) |
222 | 220, 221,
216 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → (((abs ∘ − ) ∘
𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
223 | 4, 32, 209 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
224 | 223 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
225 | 223 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
226 | 224, 225 | resubcld 11146 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
227 | 226 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
228 | 227 | recnd 10747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ) |
229 | 222, 197,
228 | fsumser 15180 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑀)) |
230 | 24 | fveq1i 6675 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇‘𝑀) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑀) |
231 | 229, 230 | eqtr4di 2791 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (𝑇‘𝑀)) |
232 | 196 | nnzd 12167 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℤ) |
233 | 232 | peano2zd 12171 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℤ) |
234 | 4 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
235 | 196 | peano2nnd 11733 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℕ) |
236 | | elfzuz 12994 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛)) → 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) |
237 | | eluznn 12400 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑗 ∈ ℕ) |
238 | 235, 236,
237 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝑗 ∈ ℕ) |
239 | 234, 238,
209 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
240 | 239 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
241 | 239 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
242 | 240, 241 | resubcld 11146 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
243 | 242 | recnd 10747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ) |
244 | | 2fveq3 6679 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑘 + 𝑀) → (2nd ‘(𝐺‘𝑗)) = (2nd ‘(𝐺‘(𝑘 + 𝑀)))) |
245 | | 2fveq3 6679 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑘 + 𝑀) → (1st ‘(𝐺‘𝑗)) = (1st ‘(𝐺‘(𝑘 + 𝑀)))) |
246 | 244, 245 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑘 + 𝑀) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
247 | 232, 233,
200, 243, 246 | fsumshftm 15229 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
248 | 196 | nncnd 11732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℂ) |
249 | | pncan2 10971 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 𝑀) =
1) |
250 | 248, 74, 249 | sylancl 589 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 1) − 𝑀) = 1) |
251 | | nncn 11724 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
252 | 251 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
253 | 248, 252 | pncan2d 11077 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 𝑛) − 𝑀) = 𝑛) |
254 | 250, 253 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀)) = (1...𝑛)) |
255 | 254 | sumeq1d 15151 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) = Σ𝑘 ∈ (1...𝑛)((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
256 | 133 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
257 | | elfznn 13027 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
258 | 134 | ovolfsval 24222 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ∧ 𝑘
∈ ℕ) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)))) |
259 | 256, 257,
258 | syl2an 599 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘
(𝑧 ∈ ℕ ↦
(𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)))) |
260 | 257 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
261 | | fvoveq1 7193 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 𝑘 → (𝐺‘(𝑧 + 𝑀)) = (𝐺‘(𝑘 + 𝑀))) |
262 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) |
263 | | fvex 6687 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺‘(𝑘 + 𝑀)) ∈ V |
264 | 261, 262,
263 | fvmpt 6775 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℕ → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀))) |
265 | 260, 264 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀))) |
266 | 265 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (2nd ‘(𝐺‘(𝑘 + 𝑀)))) |
267 | 265 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (1st ‘(𝐺‘(𝑘 + 𝑀)))) |
268 | 266, 267 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
269 | 259, 268 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘
(𝑧 ∈ ℕ ↦
(𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
270 | | simpr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
271 | 270, 67 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
272 | 4 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
273 | | nnaddcl 11739 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 + 𝑀) ∈ ℕ) |
274 | 257, 196,
273 | syl2anr 600 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 𝑀) ∈ ℕ) |
275 | | ovolfcl 24218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (𝑘 + 𝑀) ∈ ℕ) → ((1st
‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2nd
‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1st
‘(𝐺‘(𝑘 + 𝑀))) ≤ (2nd ‘(𝐺‘(𝑘 + 𝑀))))) |
276 | 272, 274,
275 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((1st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2nd
‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1st
‘(𝐺‘(𝑘 + 𝑀))) ≤ (2nd ‘(𝐺‘(𝑘 + 𝑀))))) |
277 | 276 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ) |
278 | 276 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ) |
279 | 277, 278 | resubcld 11146 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℝ) |
280 | 279 | recnd 10747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℂ) |
281 | 269, 271,
280 | fsumser 15180 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) = (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) |
282 | 247, 255,
281 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) |
283 | 231, 282 | oveq12d 7188 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))) |
284 | 215, 219,
283 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))) |
285 | 187, 284 | syl5eq 2785 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))) |
286 | 123 | ffnd 6505 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 Fn ℕ) |
287 | | fnfvelrn 6858 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 Fn ℕ ∧ (𝑀 + 𝑛) ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇) |
288 | 286, 199,
287 | syl2an2r 685 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇) |
289 | 285, 288 | eqeltrrd 2834 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇) |
290 | | supxrub 12800 |
. . . . . . . . . . . 12
⊢ ((ran
𝑇 ⊆
ℝ* ∧ ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, <
)) |
291 | 186, 289,
290 | syl2an2r 685 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, <
)) |
292 | 125 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑀) ∈ ℝ) |
293 | 137 | ffvelrnda 6861 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ (0[,)+∞)) |
294 | 120, 293 | sseldi 3875 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ ℝ) |
295 | 90 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑇, ℝ*, < )
∈ ℝ) |
296 | 292, 294,
295 | leaddsub2d 11320 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, < ) ↔ (seq1(
+ , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
297 | 291, 296 | mpbid 235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
298 | 297 | ralrimiva 3096 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
299 | 137 | ffnd 6505 |
. . . . . . . . . 10
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ) |
300 | | breq1 5033 |
. . . . . . . . . . 11
⊢ (𝑥 = (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) → (𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
301 | 300 | ralrn 6864 |
. . . . . . . . . 10
⊢ (seq1( +
, ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ → (∀𝑥 ∈ ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
302 | 299, 301 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑥 ∈ ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
303 | 298, 302 | mpbird 260 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ran seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
304 | | supxrleub 12802 |
. . . . . . . . 9
⊢ ((ran
seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ* ∧
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀)) ∈ ℝ*) →
(sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
305 | 140, 143,
304 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
306 | 303, 305 | mpbird 260 |
. . . . . . 7
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀))) |
307 | 127, 142,
143, 184, 306 | xrletrd 12638 |
. . . . . 6
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
308 | 125, 90, 50 | absdifltd 14883 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶 ↔ ((sup(ran 𝑇, ℝ*, < )
− 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ*, < ) + 𝐶)))) |
309 | 27, 308 | mpbid 235 |
. . . . . . . 8
⊢ (𝜑 → ((sup(ran 𝑇, ℝ*, < )
− 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ*, < ) + 𝐶))) |
310 | 309 | simpld 498 |
. . . . . . 7
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − 𝐶) < (𝑇‘𝑀)) |
311 | 90, 50, 125, 310 | ltsub23d 11323 |
. . . . . 6
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) < 𝐶) |
312 | 97, 126, 50, 307, 311 | lelttrd 10876 |
. . . . 5
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) < 𝐶) |
313 | 97, 50, 49, 312 | ltadd2dd 10877 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶)) |
314 | 13, 98, 51, 119, 313 | lelttrd 10876 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) < ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶)) |
315 | 54, 97 | readdcld 10748 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
316 | | difss 4022 |
. . . . . . . 8
⊢ (𝐾 ∖ 𝐴) ⊆ 𝐾 |
317 | | unss1 4069 |
. . . . . . . 8
⊢ ((𝐾 ∖ 𝐴) ⊆ 𝐾 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
318 | 316, 317 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
319 | 318, 88 | sseqtrrid 3930 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺)) |
320 | | ovolsscl 24238 |
. . . . . 6
⊢ ((((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran
((,) ∘ 𝐺) ⊆
ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) →
(vol*‘((𝐾 ∖
𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
321 | 319, 9, 95, 320 | syl3anc 1372 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
322 | 104 | ssdifd 4031 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∖ 𝐴)) |
323 | | difundir 4171 |
. . . . . . . 8
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∖ 𝐴) = ((𝐾 ∖ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴)) |
324 | | difss 4022 |
. . . . . . . . 9
⊢ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) |
325 | | unss2 4071 |
. . . . . . . . 9
⊢ ((∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) → ((𝐾 ∖ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
326 | 324, 325 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐾 ∖ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
327 | 323, 326 | eqsstri 3911 |
. . . . . . 7
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
328 | 322, 327 | sstrdi 3889 |
. . . . . 6
⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
329 | 319, 9 | sstrd 3887 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) |
330 | | ovolss 24237 |
. . . . . 6
⊢ (((𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∧ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) →
(vol*‘(𝐸 ∖
𝐴)) ≤
(vol*‘((𝐾 ∖
𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
331 | 328, 329,
330 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ≤ (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
332 | 52, 46 | sstrd 3887 |
. . . . . 6
⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ ℝ) |
333 | | ovolun 24251 |
. . . . . 6
⊢ ((((𝐾 ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ℝ ∧
(vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ)) →
(vol*‘((𝐾 ∖
𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
334 | 332, 54, 116, 97, 333 | syl22anc 838 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
335 | 16, 321, 315, 331, 334 | letrd 10875 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
336 | 97, 50, 54, 312 | ltadd2dd 10877 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶)) |
337 | 16, 315, 55, 335, 336 | lelttrd 10876 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) < ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶)) |
338 | 13, 16, 51, 55, 314, 337 | lt2addd 11341 |
. 2
⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) < (((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶))) |
339 | 49 | recnd 10747 |
. . 3
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℂ) |
340 | 50 | recnd 10747 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℂ) |
341 | 54 | recnd 10747 |
. . 3
⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℂ) |
342 | 339, 340,
341, 340 | add4d 10946 |
. 2
⊢ (𝜑 → (((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶)) = (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶))) |
343 | 338, 342 | breqtrd 5056 |
1
⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) < (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶))) |