Step | Hyp | Ref
| Expression |
1 | | inss1 3833 |
. . . . 5
⊢ (𝐸 ∩ 𝐴) ⊆ 𝐸 |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ 𝐸) |
3 | | uniioombl.s |
. . . . 5
⊢ (𝜑 → 𝐸 ⊆ ∪ ran
((,) ∘ 𝐺)) |
4 | | uniioombl.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
5 | 4 | uniiccdif 23346 |
. . . . . . 7
⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
([,] ∘ 𝐺) ∧
(vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran
((,) ∘ 𝐺))) =
0)) |
6 | 5 | simpld 475 |
. . . . . 6
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
([,] ∘ 𝐺)) |
7 | | ovolficcss 23238 |
. . . . . . 7
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐺) ⊆
ℝ) |
8 | 4, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ) |
9 | 6, 8 | sstrd 3613 |
. . . . 5
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ) |
10 | 3, 9 | sstrd 3613 |
. . . 4
⊢ (𝜑 → 𝐸 ⊆ ℝ) |
11 | | uniioombl.e |
. . . 4
⊢ (𝜑 → (vol*‘𝐸) ∈
ℝ) |
12 | | ovolsscl 23254 |
. . . 4
⊢ (((𝐸 ∩ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∩ 𝐴)) ∈
ℝ) |
13 | 2, 10, 11, 12 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ∈ ℝ) |
14 | | difssd 3738 |
. . . 4
⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ 𝐸) |
15 | | ovolsscl 23254 |
. . . 4
⊢ (((𝐸 ∖ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∖
𝐴)) ∈
ℝ) |
16 | 14, 10, 11, 15 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ∈ ℝ) |
17 | | inss1 3833 |
. . . . . 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 23352 |
. . . . . . 7
⊢ (𝜑 → (𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ∧ (vol*‘𝐾) ∈ ℝ)) |
30 | 29 | simpld 475 |
. . . . . 6
⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
31 | | inss2 3834 |
. . . . . . . . . . . . 13
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
32 | | elfznn 12370 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ) |
33 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
34 | 4, 32, 33 | syl2an 494 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
35 | 31, 34 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ ×
ℝ)) |
36 | | 1st2nd2 7205 |
. . . . . . . . . . . 12
⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) →
(𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
38 | 37 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉)) |
39 | | df-ov 6653 |
. . . . . . . . . 10
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉) |
40 | 38, 39 | syl6eqr 2674 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗)))) |
41 | | ioossre 12235 |
. . . . . . . . 9
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) ⊆ ℝ |
42 | 40, 41 | syl6eqss 3655 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
43 | 42 | ralrimiva 2966 |
. . . . . . 7
⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
44 | | iunss 4561 |
. . . . . . 7
⊢ (∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ ↔ ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
45 | 43, 44 | sylibr 224 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
46 | 30, 45 | eqsstrd 3639 |
. . . . 5
⊢ (𝜑 → 𝐾 ⊆ ℝ) |
47 | 29 | simprd 479 |
. . . . 5
⊢ (𝜑 → (vol*‘𝐾) ∈
ℝ) |
48 | | ovolsscl 23254 |
. . . . 5
⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∩ 𝐴)) ∈
ℝ) |
49 | 18, 46, 47, 48 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ) |
50 | 23 | rpred 11872 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℝ) |
51 | 49, 50 | readdcld 10069 |
. . 3
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) ∈ ℝ) |
52 | | difssd 3738 |
. . . . 5
⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ 𝐾) |
53 | | ovolsscl 23254 |
. . . . 5
⊢ (((𝐾 ∖ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∖
𝐴)) ∈
ℝ) |
54 | 52, 46, 47, 53 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ) |
55 | 54, 50 | readdcld 10069 |
. . 3
⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶) ∈ ℝ) |
56 | | ssun2 3777 |
. . . . . . 7
⊢ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
57 | | ioof 12271 |
. . . . . . . . . . . . . . 15
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
58 | | rexpssxrxp 10084 |
. . . . . . . . . . . . . . . . 17
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
59 | 31, 58 | sstri 3612 |
. . . . . . . . . . . . . . . 16
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
60 | | fss 6056 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
61 | 4, 59, 60 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
62 | | fco 6058 |
. . . . . . . . . . . . . . 15
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐺:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
63 | 57, 61, 62 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
64 | | ffn 6045 |
. . . . . . . . . . . . . 14
⊢ (((,)
∘ 𝐺):ℕ⟶𝒫 ℝ →
((,) ∘ 𝐺) Fn
ℕ) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ) |
66 | | fnima 6010 |
. . . . . . . . . . . . 13
⊢ (((,)
∘ 𝐺) Fn ℕ
→ (((,) ∘ 𝐺)
“ ℕ) = ran ((,) ∘ 𝐺)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = ran ((,)
∘ 𝐺)) |
68 | | nnuz 11723 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
69 | 26 | peano2nnd 11037 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 + 1) ∈ ℕ) |
70 | 69, 68 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘1)) |
71 | | uzsplit 12412 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 + 1) ∈
(ℤ≥‘1) → (ℤ≥‘1) =
((1...((𝑀 + 1) − 1))
∪ (ℤ≥‘(𝑀 + 1)))) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(ℤ≥‘1) = ((1...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1)))) |
73 | 68, 72 | syl5eq 2668 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℕ = ((1...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1)))) |
74 | 26 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ ℂ) |
75 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
76 | | pncan 10287 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 1) = 𝑀) |
77 | 74, 75, 76 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀) |
78 | 77 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...((𝑀 + 1) − 1)) = (1...𝑀)) |
79 | 78 | uneq1d 3766 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((1...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1))) = ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))) |
80 | 73, 79 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℕ = ((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
81 | 80 | imaeq2d 5466 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = (((,)
∘ 𝐺) “
((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1))))) |
82 | 67, 81 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ (𝜑 → ran ((,) ∘ 𝐺) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1))))) |
83 | | imaundi 5545 |
. . . . . . . . . . 11
⊢ (((,)
∘ 𝐺) “
((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
84 | 82, 83 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝜑 → ran ((,) ∘ 𝐺) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
85 | 84 | unieqd 4446 |
. . . . . . . . 9
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪ ((((,)
∘ 𝐺) “
(1...𝑀)) ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
86 | | uniun 4456 |
. . . . . . . . 9
⊢ ∪ ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) = (∪
(((,) ∘ 𝐺) “
(1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
87 | 85, 86 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (∪ (((,)
∘ 𝐺) “
(1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
88 | 28 | uneq1i 3763 |
. . . . . . . 8
⊢ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) = (∪
(((,) ∘ 𝐺) “
(1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
89 | 87, 88 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
90 | 56, 89 | syl5sseqr 3654 |
. . . . . 6
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ 𝐺)) |
91 | 19, 20, 21, 22, 11, 23, 4, 3, 24, 25 | uniioombllem1 23349 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
92 | | ssid 3624 |
. . . . . . . 8
⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
((,) ∘ 𝐺) |
93 | 24 | ovollb 23247 |
. . . . . . . 8
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ∪ ran ((,) ∘
𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, <
)) |
94 | 4, 92, 93 | sylancl 694 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, <
)) |
95 | | ovollecl 23251 |
. . . . . . 7
⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ*, < )
∈ ℝ ∧ (vol*‘∪ ran ((,) ∘
𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
→ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈
ℝ) |
96 | 9, 91, 94, 95 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) |
97 | | ovolsscl 23254 |
. . . . . 6
⊢ ((∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ 𝐺) ∧
∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ) |
98 | 90, 9, 96, 97 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ) |
99 | 49, 98 | readdcld 10069 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
100 | | unss1 3782 |
. . . . . . . 8
⊢ ((𝐾 ∩ 𝐴) ⊆ 𝐾 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
101 | 17, 100 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
102 | 101, 89 | syl5sseqr 3654 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺)) |
103 | | ovolsscl 23254 |
. . . . . 6
⊢ ((((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran
((,) ∘ 𝐺) ⊆
ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) →
(vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
104 | 102, 9, 96, 103 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
105 | 3, 89 | sseqtrd 3641 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
106 | | ssrin 3838 |
. . . . . . . 8
⊢ (𝐸 ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∩ 𝐴)) |
107 | 105, 106 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∩ 𝐴)) |
108 | | indir 3875 |
. . . . . . . 8
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∩ 𝐴) = ((𝐾 ∩ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴)) |
109 | | inss1 3833 |
. . . . . . . . 9
⊢ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) |
110 | | unss2 3784 |
. . . . . . . . 9
⊢ ((∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) → ((𝐾 ∩ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
111 | 109, 110 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐾 ∩ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
112 | 108, 111 | eqsstri 3635 |
. . . . . . 7
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
113 | 107, 112 | syl6ss 3615 |
. . . . . 6
⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
114 | 102, 9 | sstrd 3613 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) |
115 | | ovolss 23253 |
. . . . . 6
⊢ (((𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∧ ((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) →
(vol*‘(𝐸 ∩ 𝐴)) ≤ (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
116 | 113, 114,
115 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ≤ (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
117 | 18, 46 | sstrd 3613 |
. . . . . 6
⊢ (𝜑 → (𝐾 ∩ 𝐴) ⊆ ℝ) |
118 | 90, 9 | sstrd 3613 |
. . . . . 6
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ℝ) |
119 | | ovolun 23267 |
. . . . . 6
⊢ ((((𝐾 ∩ 𝐴) ⊆ ℝ ∧ (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ℝ ∧
(vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ)) →
(vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
120 | 117, 49, 118, 98, 119 | syl22anc 1327 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
121 | 13, 104, 99, 116, 120 | letrd 10194 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
122 | | rge0ssre 12280 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℝ |
123 | | eqid 2622 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) |
124 | 123, 24 | ovolsf 23241 |
. . . . . . . . . 10
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞)) |
125 | 4, 124 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞)) |
126 | 125, 26 | ffvelrnd 6360 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘𝑀) ∈ (0[,)+∞)) |
127 | 122, 126 | sseldi 3601 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘𝑀) ∈ ℝ) |
128 | 91, 127 | resubcld 10458 |
. . . . . 6
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ∈ ℝ) |
129 | 98 | rexrd 10089 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈
ℝ*) |
130 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℕ) |
131 | | nnaddcl 11042 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ) |
132 | 130, 26, 131 | syl2anr 495 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ) |
133 | 4 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 + 𝑀) ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
134 | 132, 133 | syldan 487 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
135 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) |
136 | 134, 135 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
137 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((abs ∘ − ) ∘
(𝑧 ∈ ℕ ↦
(𝐺‘(𝑧 + 𝑀)))) |
138 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) = seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀))))) |
139 | 137, 138 | ovolsf 23241 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞)) |
140 | 136, 139 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞)) |
141 | | frn 6053 |
. . . . . . . . . 10
⊢ (seq1( +
, ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞) →
ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆
(0[,)+∞)) |
142 | 140, 141 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆
(0[,)+∞)) |
143 | | icossxr 12258 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ* |
144 | 142, 143 | syl6ss 3615 |
. . . . . . . 8
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆
ℝ*) |
145 | | supxrcl 12145 |
. . . . . . . 8
⊢ (ran
seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ* →
sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ∈
ℝ*) |
146 | 144, 145 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ∈
ℝ*) |
147 | 128 | rexrd 10089 |
. . . . . . 7
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ∈
ℝ*) |
148 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 1 ∈
ℤ) |
149 | 26 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℤ) |
150 | 149 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℤ) |
151 | | addcom 10222 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑀 + 1) =
(1 + 𝑀)) |
152 | 74, 75, 151 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑀 + 1) = (1 + 𝑀)) |
153 | 152 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) = (ℤ≥‘(1 +
𝑀))) |
154 | 153 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑥 ∈ (ℤ≥‘(𝑀 + 1)) ↔ 𝑥 ∈ (ℤ≥‘(1 +
𝑀)))) |
155 | 154 | biimpa 501 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
(ℤ≥‘(1 + 𝑀))) |
156 | | eluzsub 11717 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℤ ∧ 𝑀
∈ ℤ ∧ 𝑥
∈ (ℤ≥‘(1 + 𝑀))) → (𝑥 − 𝑀) ∈
(ℤ≥‘1)) |
157 | 148, 150,
155, 156 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈
(ℤ≥‘1)) |
158 | 157, 68 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈ ℕ) |
159 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑥 ∈ ℤ) |
160 | 159 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
ℤ) |
161 | 160 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
ℂ) |
162 | 74 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℂ) |
163 | 161, 162 | npcand 10396 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑥 − 𝑀) + 𝑀) = 𝑥) |
164 | 163 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 = ((𝑥 − 𝑀) + 𝑀)) |
165 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝑥 − 𝑀) → (𝑧 + 𝑀) = ((𝑥 − 𝑀) + 𝑀)) |
166 | 165 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑥 − 𝑀) → (𝑥 = (𝑧 + 𝑀) ↔ 𝑥 = ((𝑥 − 𝑀) + 𝑀))) |
167 | 166 | rspcev 3309 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 − 𝑀) ∈ ℕ ∧ 𝑥 = ((𝑥 − 𝑀) + 𝑀)) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)) |
168 | 158, 164,
167 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)) |
169 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
170 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) |
171 | 170 | elrnmpt 5372 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))) |
172 | 169, 171 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)) |
173 | 168, 172 | sylibr 224 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
174 | 173 | ex 450 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))) |
175 | 174 | ssrdv 3609 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
176 | | imass2 5501 |
. . . . . . . . . . . . 13
⊢
((ℤ≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) → (𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))) |
177 | 175, 176 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))) |
178 | | rnco2 5642 |
. . . . . . . . . . . . 13
⊢ ran
(𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
179 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) |
180 | 4 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 = (𝑤 ∈ ℕ ↦ (𝐺‘𝑤))) |
181 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝑧 + 𝑀) → (𝐺‘𝑤) = (𝐺‘(𝑧 + 𝑀))) |
182 | 132, 179,
180, 181 | fmptco 6396 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
183 | 182 | rneqd 5353 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
184 | 178, 183 | syl5eqr 2670 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
185 | 177, 184 | sseqtrd 3641 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
186 | | imass2 5501 |
. . . . . . . . . . 11
⊢ ((𝐺 “
(ℤ≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) → ((,) “ (𝐺 “
(ℤ≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
187 | 185, 186 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((,) “ (𝐺 “
(ℤ≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
188 | | imaco 5640 |
. . . . . . . . . 10
⊢ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) = ((,) “ (𝐺 “
(ℤ≥‘(𝑀 + 1)))) |
189 | | rnco2 5642 |
. . . . . . . . . 10
⊢ ran ((,)
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))) = ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) |
190 | 187, 188,
189 | 3sstr4g 3646 |
. . . . . . . . 9
⊢ (𝜑 → (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
191 | 190 | unissd 4462 |
. . . . . . . 8
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) |
192 | 138 | ovollb 23247 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ∧ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ∪
ran ((,) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, <
)) |
193 | 136, 191,
192 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, <
)) |
194 | | frn 6053 |
. . . . . . . . . . . . . . 15
⊢ (𝑇:ℕ⟶(0[,)+∞)
→ ran 𝑇 ⊆
(0[,)+∞)) |
195 | 125, 194 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞)) |
196 | 195, 143 | syl6ss 3615 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝑇 ⊆
ℝ*) |
197 | 196 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran 𝑇 ⊆
ℝ*) |
198 | 24 | fveq1i 6192 |
. . . . . . . . . . . . . 14
⊢ (𝑇‘(𝑀 + 𝑛)) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘(𝑀 + 𝑛)) |
199 | 26 | nnred 11035 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℝ) |
200 | 199 | ltp1d 10954 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
201 | | fzdisj 12368 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅) |
202 | 200, 201 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅) |
203 | 202 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅) |
204 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
205 | | nn0addge1 11339 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℝ ∧ 𝑛 ∈ ℕ0)
→ 𝑀 ≤ (𝑀 + 𝑛)) |
206 | 199, 204,
205 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ≤ (𝑀 + 𝑛)) |
207 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℕ) |
208 | 207, 68 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈
(ℤ≥‘1)) |
209 | | nnaddcl 11042 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ) |
210 | 26, 209 | sylan 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ) |
211 | 210 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℤ) |
212 | | elfz5 12334 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈
(ℤ≥‘1) ∧ (𝑀 + 𝑛) ∈ ℤ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛))) |
213 | 208, 211,
212 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛))) |
214 | 206, 213 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ (1...(𝑀 + 𝑛))) |
215 | | fzsplit 12367 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ (1...(𝑀 + 𝑛)) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛)))) |
216 | 214, 215 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛)))) |
217 | | fzfid 12772 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) ∈ Fin) |
218 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
219 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (1...(𝑀 + 𝑛)) → 𝑗 ∈ ℕ) |
220 | | ovolfcl 23235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st
‘(𝐺‘𝑗)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1st
‘(𝐺‘𝑗)) ≤ (2nd
‘(𝐺‘𝑗)))) |
221 | 218, 219,
220 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
222 | 221 | simp2d 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
223 | 221 | simp1d 1073 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
224 | 222, 223 | resubcld 10458 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
225 | 224 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ) |
226 | 203, 216,
217, 225 | fsumsplit 14471 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))))) |
227 | 123 | ovolfsval 23239 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
228 | 218, 219,
227 | syl2an 494 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (((abs ∘ − ) ∘
𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
229 | 210, 68 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈
(ℤ≥‘1)) |
230 | 228, 229,
225 | fsumser 14461 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘(𝑀 + 𝑛))) |
231 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
232 | 32 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ) |
233 | 231, 232,
227 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → (((abs ∘ − ) ∘
𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
234 | 4, 32, 220 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
235 | 234 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
236 | 234 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
237 | 235, 236 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
238 | 237 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
239 | 238 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ) |
240 | 233, 208,
239 | fsumser 14461 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑀)) |
241 | 24 | fveq1i 6192 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇‘𝑀) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑀) |
242 | 240, 241 | syl6eqr 2674 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (𝑇‘𝑀)) |
243 | 207 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℤ) |
244 | 243 | peano2zd 11485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℤ) |
245 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
246 | 207 | peano2nnd 11037 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℕ) |
247 | | elfzuz 12338 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛)) → 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) |
248 | | eluznn 11758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑗 ∈ ℕ) |
249 | 246, 247,
248 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝑗 ∈ ℕ) |
250 | 245, 249,
220 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
251 | 250 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
252 | 250 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
253 | 251, 252 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
254 | 253 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ) |
255 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = (𝑘 + 𝑀) → (𝐺‘𝑗) = (𝐺‘(𝑘 + 𝑀))) |
256 | 255 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑘 + 𝑀) → (2nd ‘(𝐺‘𝑗)) = (2nd ‘(𝐺‘(𝑘 + 𝑀)))) |
257 | 255 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑘 + 𝑀) → (1st ‘(𝐺‘𝑗)) = (1st ‘(𝐺‘(𝑘 + 𝑀)))) |
258 | 256, 257 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑘 + 𝑀) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
259 | 243, 244,
211, 254, 258 | fsumshftm 14513 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
260 | 207 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℂ) |
261 | | pncan2 10288 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 𝑀) =
1) |
262 | 260, 75, 261 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 1) − 𝑀) = 1) |
263 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
264 | 263 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
265 | 260, 264 | pncan2d 10394 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 𝑛) − 𝑀) = 𝑛) |
266 | 262, 265 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀)) = (1...𝑛)) |
267 | 266 | sumeq1d 14431 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) = Σ𝑘 ∈ (1...𝑛)((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
268 | 136 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
269 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
270 | 137 | ovolfsval 23239 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ∧ 𝑘
∈ ℕ) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)))) |
271 | 268, 269,
270 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘
(𝑧 ∈ ℕ ↦
(𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)))) |
272 | 269 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
273 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑘 → (𝑧 + 𝑀) = (𝑘 + 𝑀)) |
274 | 273 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 𝑘 → (𝐺‘(𝑧 + 𝑀)) = (𝐺‘(𝑘 + 𝑀))) |
275 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺‘(𝑘 + 𝑀)) ∈ V |
276 | 274, 135,
275 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℕ → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀))) |
277 | 272, 276 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀))) |
278 | 277 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (2nd ‘(𝐺‘(𝑘 + 𝑀)))) |
279 | 277 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (1st ‘(𝐺‘(𝑘 + 𝑀)))) |
280 | 278, 279 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
281 | 271, 280 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘
(𝑧 ∈ ℕ ↦
(𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀))))) |
282 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
283 | 282, 68 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
284 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
285 | | nnaddcl 11042 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 + 𝑀) ∈ ℕ) |
286 | 269, 207,
285 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 𝑀) ∈ ℕ) |
287 | | ovolfcl 23235 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (𝑘 + 𝑀) ∈ ℕ) → ((1st
‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2nd
‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1st
‘(𝐺‘(𝑘 + 𝑀))) ≤ (2nd ‘(𝐺‘(𝑘 + 𝑀))))) |
288 | 284, 286,
287 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((1st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2nd
‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1st
‘(𝐺‘(𝑘 + 𝑀))) ≤ (2nd ‘(𝐺‘(𝑘 + 𝑀))))) |
289 | 288 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ) |
290 | 288 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ) |
291 | 289, 290 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℝ) |
292 | 291 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℂ) |
293 | 281, 283,
292 | fsumser 14461 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) = (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) |
294 | 259, 267,
293 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) |
295 | 242, 294 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))) |
296 | 226, 230,
295 | 3eqtr3d 2664 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))) |
297 | 198, 296 | syl5eq 2668 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))) |
298 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇:ℕ⟶(0[,)+∞)
→ 𝑇 Fn
ℕ) |
299 | 125, 298 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇 Fn ℕ) |
300 | 299 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑇 Fn ℕ) |
301 | | fnfvelrn 6356 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 Fn ℕ ∧ (𝑀 + 𝑛) ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇) |
302 | 300, 210,
301 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇) |
303 | 297, 302 | eqeltrrd 2702 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇) |
304 | | supxrub 12154 |
. . . . . . . . . . . 12
⊢ ((ran
𝑇 ⊆
ℝ* ∧ ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, <
)) |
305 | 197, 303,
304 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, <
)) |
306 | 127 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑀) ∈ ℝ) |
307 | 140 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ (0[,)+∞)) |
308 | 122, 307 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ ℝ) |
309 | 91 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑇, ℝ*, < )
∈ ℝ) |
310 | 306, 308,
309 | leaddsub2d 10629 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑇‘𝑀) + (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, < ) ↔ (seq1(
+ , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
311 | 305, 310 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
312 | 311 | ralrimiva 2966 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
313 | | ffn 6045 |
. . . . . . . . . . 11
⊢ (seq1( +
, ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞) →
seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ) |
314 | 140, 313 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ) |
315 | | breq1 4656 |
. . . . . . . . . . 11
⊢ (𝑥 = (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) → (𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ (seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
316 | 315 | ralrn 6362 |
. . . . . . . . . 10
⊢ (seq1( +
, ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ → (∀𝑥 ∈ ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
317 | 314, 316 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑥 ∈ ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝑧 ∈
ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
318 | 312, 317 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ran seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
319 | | supxrleub 12156 |
. . . . . . . . 9
⊢ ((ran
seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ* ∧
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀)) ∈ ℝ*) →
(sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
320 | 144, 147,
319 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − )
∘ (𝑧 ∈ ℕ
↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))) |
321 | 318, 320 | mpbird 247 |
. . . . . . 7
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤
(sup(ran 𝑇,
ℝ*, < ) − (𝑇‘𝑀))) |
322 | 129, 146,
147, 193, 321 | xrletrd 11993 |
. . . . . 6
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))) |
323 | 127, 91, 50 | absdifltd 14172 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶 ↔ ((sup(ran 𝑇, ℝ*, < )
− 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ*, < ) + 𝐶)))) |
324 | 27, 323 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → ((sup(ran 𝑇, ℝ*, < )
− 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ*, < ) + 𝐶))) |
325 | 324 | simpld 475 |
. . . . . . 7
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − 𝐶) < (𝑇‘𝑀)) |
326 | 91, 50, 127, 325 | ltsub23d 10632 |
. . . . . 6
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) < 𝐶) |
327 | 98, 128, 50, 322, 326 | lelttrd 10195 |
. . . . 5
⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) < 𝐶) |
328 | 98, 50, 49, 327 | ltadd2dd 10196 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶)) |
329 | 13, 99, 51, 121, 328 | lelttrd 10195 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) < ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶)) |
330 | 54, 98 | readdcld 10069 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
331 | | difss 3737 |
. . . . . . . 8
⊢ (𝐾 ∖ 𝐴) ⊆ 𝐾 |
332 | | unss1 3782 |
. . . . . . . 8
⊢ ((𝐾 ∖ 𝐴) ⊆ 𝐾 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
333 | 331, 332 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
334 | 333, 89 | syl5sseqr 3654 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺)) |
335 | | ovolsscl 23254 |
. . . . . 6
⊢ ((((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran
((,) ∘ 𝐺) ⊆
ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) →
(vol*‘((𝐾 ∖
𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
336 | 334, 9, 96, 335 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ∈ ℝ) |
337 | 105 | ssdifd 3746 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∖ 𝐴)) |
338 | | difundir 3880 |
. . . . . . . 8
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∖ 𝐴) = ((𝐾 ∖ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴)) |
339 | | difss 3737 |
. . . . . . . . 9
⊢ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) |
340 | | unss2 3784 |
. . . . . . . . 9
⊢ ((∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) → ((𝐾 ∖ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
341 | 339, 340 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐾 ∖ 𝐴) ∪ (∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
342 | 338, 341 | eqsstri 3635 |
. . . . . . 7
⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) |
343 | 337, 342 | syl6ss 3615 |
. . . . . 6
⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) |
344 | 334, 9 | sstrd 3613 |
. . . . . 6
⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) |
345 | | ovolss 23253 |
. . . . . 6
⊢ (((𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∧ ((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) →
(vol*‘(𝐸 ∖
𝐴)) ≤
(vol*‘((𝐾 ∖
𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
346 | 343, 344,
345 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ≤ (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
347 | 52, 46 | sstrd 3613 |
. . . . . 6
⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ ℝ) |
348 | | ovolun 23267 |
. . . . . 6
⊢ ((((𝐾 ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))) ⊆ ℝ ∧
(vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))) ∈ ℝ)) →
(vol*‘((𝐾 ∖
𝐴) ∪ ∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
349 | 347, 54, 118, 98, 348 | syl22anc 1327 |
. . . . 5
⊢ (𝜑 → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,)
∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
350 | 16, 336, 330, 346, 349 | letrd 10194 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1)))))) |
351 | 98, 50, 54, 327 | ltadd2dd 10196 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “
(ℤ≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶)) |
352 | 16, 330, 55, 350, 351 | lelttrd 10195 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) < ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶)) |
353 | 13, 16, 51, 55, 329, 352 | lt2addd 10650 |
. 2
⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) < (((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶))) |
354 | 49 | recnd 10068 |
. . 3
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℂ) |
355 | 50 | recnd 10068 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℂ) |
356 | 54 | recnd 10068 |
. . 3
⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℂ) |
357 | 354, 355,
356, 355 | add4d 10264 |
. 2
⊢ (𝜑 → (((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶)) = (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶))) |
358 | 353, 357 | breqtrd 4679 |
1
⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) < (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶))) |