Step | Hyp | Ref
| Expression |
1 | | ovolun.a |
. . . . 5
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈
ℝ)) |
2 | 1 | simpld 495 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
3 | | ovolun.b |
. . . . 5
⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈
ℝ)) |
4 | 3 | simpld 495 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
5 | 2, 4 | unssd 4085 |
. . 3
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ ℝ) |
6 | | ovolun.g1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
7 | | elovolmlem 23758 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
8 | 6, 7 | sylib 219 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
9 | 8 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
10 | 9 | ffvelrnda 6719 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
11 | | nneo 11916 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) ∈ ℕ ↔
¬ ((𝑛 + 1) / 2) ∈
ℕ)) |
12 | 11 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈
ℕ)) |
13 | 12 | con2bid 356 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑛 + 1) / 2) ∈ ℕ ↔ ¬ (𝑛 / 2) ∈
ℕ)) |
14 | 13 | biimpar 478 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) →
((𝑛 + 1) / 2) ∈
ℕ) |
15 | | ovolun.f1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
16 | | elovolmlem 23758 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
17 | 15, 16 | sylib 219 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
18 | 17 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
19 | 18 | ffvelrnda 6719 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ
× ℝ))) |
20 | 14, 19 | syldan 591 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) →
(𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩
(ℝ × ℝ))) |
21 | 10, 20 | ifclda 4417 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ
× ℝ))) |
22 | | ovolun.h |
. . . . . . . 8
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2)))) |
23 | 21, 22 | fmptd 6744 |
. . . . . . 7
⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
24 | | eqid 2794 |
. . . . . . . 8
⊢ ((abs
∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻) |
25 | | ovolun.u |
. . . . . . . 8
⊢ 𝑈 = seq1( + , ((abs ∘
− ) ∘ 𝐻)) |
26 | 24, 25 | ovolsf 23756 |
. . . . . . 7
⊢ (𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞)) |
27 | 23, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑈:ℕ⟶(0[,)+∞)) |
28 | | rge0ssre 12694 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℝ |
29 | | fss 6398 |
. . . . . 6
⊢ ((𝑈:ℕ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ) |
30 | 27, 28, 29 | sylancl 586 |
. . . . 5
⊢ (𝜑 → 𝑈:ℕ⟶ℝ) |
31 | 30 | frnd 6392 |
. . . 4
⊢ (𝜑 → ran 𝑈 ⊆ ℝ) |
32 | | 1nn 11499 |
. . . . . . 7
⊢ 1 ∈
ℕ |
33 | | 1z 11862 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
34 | | seqfn 13231 |
. . . . . . . . . 10
⊢ (1 ∈
ℤ → seq1( + , ((abs ∘ − ) ∘ 𝐻)) Fn
(ℤ≥‘1)) |
35 | 33, 34 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐻)) Fn
(ℤ≥‘1)) |
36 | 25 | fneq1i 6323 |
. . . . . . . . . 10
⊢ (𝑈 Fn ℕ ↔ seq1( + ,
((abs ∘ − ) ∘ 𝐻)) Fn ℕ) |
37 | | nnuz 12130 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
38 | 37 | fneq2i 6324 |
. . . . . . . . . 10
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝐻)) Fn ℕ ↔ seq1( + , ((abs ∘
− ) ∘ 𝐻)) Fn
(ℤ≥‘1)) |
39 | 36, 38 | bitri 276 |
. . . . . . . . 9
⊢ (𝑈 Fn ℕ ↔ seq1( + ,
((abs ∘ − ) ∘ 𝐻)) Fn
(ℤ≥‘1)) |
40 | 35, 39 | sylibr 235 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 Fn ℕ) |
41 | | fndm 6328 |
. . . . . . . 8
⊢ (𝑈 Fn ℕ → dom 𝑈 = ℕ) |
42 | 40, 41 | syl 17 |
. . . . . . 7
⊢ (𝜑 → dom 𝑈 = ℕ) |
43 | 32, 42 | syl5eleqr 2889 |
. . . . . 6
⊢ (𝜑 → 1 ∈ dom 𝑈) |
44 | 43 | ne0d 4223 |
. . . . 5
⊢ (𝜑 → dom 𝑈 ≠ ∅) |
45 | | dm0rn0 5682 |
. . . . . 6
⊢ (dom
𝑈 = ∅ ↔ ran
𝑈 =
∅) |
46 | 45 | necon3bii 3035 |
. . . . 5
⊢ (dom
𝑈 ≠ ∅ ↔ ran
𝑈 ≠
∅) |
47 | 44, 46 | sylib 219 |
. . . 4
⊢ (𝜑 → ran 𝑈 ≠ ∅) |
48 | 1 | simprd 496 |
. . . . . . . 8
⊢ (𝜑 → (vol*‘𝐴) ∈
ℝ) |
49 | 3 | simprd 496 |
. . . . . . . 8
⊢ (𝜑 → (vol*‘𝐵) ∈
ℝ) |
50 | 48, 49 | readdcld 10519 |
. . . . . . 7
⊢ (𝜑 → ((vol*‘𝐴) + (vol*‘𝐵)) ∈
ℝ) |
51 | | ovolun.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
52 | 51 | rpred 12281 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℝ) |
53 | 50, 52 | readdcld 10519 |
. . . . . 6
⊢ (𝜑 → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ) |
54 | | ovolun.s |
. . . . . . . . 9
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
55 | | ovolun.t |
. . . . . . . . 9
⊢ 𝑇 = seq1( + , ((abs ∘
− ) ∘ 𝐺)) |
56 | | ovolun.f2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ∪ ran
((,) ∘ 𝐹)) |
57 | | ovolun.f3 |
. . . . . . . . 9
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 / 2))) |
58 | | ovolun.g2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ⊆ ∪ ran
((,) ∘ 𝐺)) |
59 | | ovolun.g3 |
. . . . . . . . 9
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤
((vol*‘𝐵) + (𝐶 / 2))) |
60 | 1, 3, 51, 54, 55, 25, 15, 56, 57, 6, 58, 59, 22 | ovolunlem1a 23780 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) |
61 | 60 | ralrimiva 3148 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) |
62 | | breq1 4967 |
. . . . . . . . 9
⊢ (𝑧 = (𝑈‘𝑘) → (𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ↔ (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))) |
63 | 62 | ralrn 6722 |
. . . . . . . 8
⊢ (𝑈 Fn ℕ →
(∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ↔ ∀𝑘 ∈ ℕ (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))) |
64 | 40, 63 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ↔ ∀𝑘 ∈ ℕ (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))) |
65 | 61, 64 | mpbird 258 |
. . . . . 6
⊢ (𝜑 → ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) |
66 | | brralrspcev 5024 |
. . . . . 6
⊢
(((((vol*‘𝐴) +
(vol*‘𝐵)) + 𝐶) ∈ ℝ ∧
∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) → ∃𝑘 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑘) |
67 | 53, 65, 66 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑘) |
68 | | ressxr 10534 |
. . . . . . 7
⊢ ℝ
⊆ ℝ* |
69 | 31, 68 | syl6ss 3903 |
. . . . . 6
⊢ (𝜑 → ran 𝑈 ⊆
ℝ*) |
70 | | supxrbnd2 12565 |
. . . . . 6
⊢ (ran
𝑈 ⊆
ℝ* → (∃𝑘 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑘 ↔ sup(ran 𝑈, ℝ*, < ) <
+∞)) |
71 | 69, 70 | syl 17 |
. . . . 5
⊢ (𝜑 → (∃𝑘 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑘 ↔ sup(ran 𝑈, ℝ*, < ) <
+∞)) |
72 | 67, 71 | mpbid 233 |
. . . 4
⊢ (𝜑 → sup(ran 𝑈, ℝ*, < ) <
+∞) |
73 | | supxrbnd 12571 |
. . . 4
⊢ ((ran
𝑈 ⊆ ℝ ∧ ran
𝑈 ≠ ∅ ∧
sup(ran 𝑈,
ℝ*, < ) < +∞) → sup(ran 𝑈, ℝ*, < ) ∈
ℝ) |
74 | 31, 47, 72, 73 | syl3anc 1364 |
. . 3
⊢ (𝜑 → sup(ran 𝑈, ℝ*, < ) ∈
ℝ) |
75 | | nncn 11496 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
76 | 75 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ) |
77 | | 1cnd 10485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 1 ∈
ℂ) |
78 | 76 | 2timesd 11730 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2 · 𝑚) = (𝑚 + 𝑚)) |
79 | 78 | oveq1d 7034 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((2 · 𝑚) − 1) = ((𝑚 + 𝑚) − 1)) |
80 | 76, 76, 77, 79 | assraddsubd 10904 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((2 · 𝑚) − 1) = (𝑚 + (𝑚 − 1))) |
81 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ) |
82 | | nnm1nn0 11788 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ → (𝑚 − 1) ∈
ℕ0) |
83 | | nnnn0addcl 11777 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 − 1) ∈
ℕ0) → (𝑚 + (𝑚 − 1)) ∈ ℕ) |
84 | 81, 82, 83 | syl2anc2 585 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 + (𝑚 − 1)) ∈ ℕ) |
85 | 80, 84 | eqeltrd 2882 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((2 · 𝑚) − 1) ∈
ℕ) |
86 | | oveq1 7026 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = ((2 · 𝑚) − 1) → (𝑛 / 2) = (((2 · 𝑚) − 1) /
2)) |
87 | 86 | eleq1d 2866 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = ((2 · 𝑚) − 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2
· 𝑚) − 1) / 2)
∈ ℕ)) |
88 | 86 | fveq2d 6545 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = ((2 · 𝑚) − 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑚) − 1) / 2))) |
89 | | oveq1 7026 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = ((2 · 𝑚) − 1) → (𝑛 + 1) = (((2 · 𝑚) − 1) +
1)) |
90 | 89 | fvoveq1d 7041 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = ((2 · 𝑚) − 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑚) − 1) + 1) / 2))) |
91 | 87, 88, 90 | ifbieq12d 4410 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = ((2 · 𝑚) − 1) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if((((2 · 𝑚) − 1) / 2) ∈
ℕ, (𝐺‘(((2
· 𝑚) − 1) /
2)), (𝐹‘((((2
· 𝑚) − 1) + 1)
/ 2)))) |
92 | | fvex 6554 |
. . . . . . . . . . . . . . 15
⊢ (𝐺‘(((2 · 𝑚) − 1) / 2)) ∈
V |
93 | | fvex 6554 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘((((2 · 𝑚) − 1) + 1) / 2)) ∈
V |
94 | 92, 93 | ifex 4431 |
. . . . . . . . . . . . . 14
⊢ if((((2
· 𝑚) − 1) / 2)
∈ ℕ, (𝐺‘(((2 · 𝑚) − 1) / 2)), (𝐹‘((((2 · 𝑚) − 1) + 1) / 2))) ∈
V |
95 | 91, 22, 94 | fvmpt 6638 |
. . . . . . . . . . . . 13
⊢ (((2
· 𝑚) − 1)
∈ ℕ → (𝐻‘((2 · 𝑚) − 1)) = if((((2 · 𝑚) − 1) / 2) ∈
ℕ, (𝐺‘(((2
· 𝑚) − 1) /
2)), (𝐹‘((((2
· 𝑚) − 1) + 1)
/ 2)))) |
96 | 85, 95 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘((2 · 𝑚) − 1)) = if((((2 · 𝑚) − 1) / 2) ∈
ℕ, (𝐺‘(((2
· 𝑚) − 1) /
2)), (𝐹‘((((2
· 𝑚) − 1) + 1)
/ 2)))) |
97 | | 2nn 11560 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℕ |
98 | | nnmulcl 11511 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ ℕ ∧ 𝑚
∈ ℕ) → (2 · 𝑚) ∈ ℕ) |
99 | 97, 81, 98 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2 · 𝑚) ∈
ℕ) |
100 | 99 | nncnd 11504 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2 · 𝑚) ∈
ℂ) |
101 | | ax-1cn 10444 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
102 | | npcan 10745 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· 𝑚) ∈ ℂ
∧ 1 ∈ ℂ) → (((2 · 𝑚) − 1) + 1) = (2 · 𝑚)) |
103 | 100, 101,
102 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((2 · 𝑚) − 1) + 1) = (2 ·
𝑚)) |
104 | 103 | oveq1d 7034 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((((2 · 𝑚) − 1) + 1) / 2) = ((2
· 𝑚) /
2)) |
105 | | 2cn 11562 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℂ |
106 | | 2ne0 11591 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 |
107 | | divcan3 11174 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → ((2 · 𝑚) / 2) = 𝑚) |
108 | 105, 106,
107 | mp3an23 1445 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℂ → ((2
· 𝑚) / 2) = 𝑚) |
109 | 76, 108 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((2 · 𝑚) / 2) = 𝑚) |
110 | 104, 109 | eqtrd 2830 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((((2 · 𝑚) − 1) + 1) / 2) = 𝑚) |
111 | 110, 81 | eqeltrd 2882 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((((2 · 𝑚) − 1) + 1) / 2) ∈
ℕ) |
112 | | nneo 11916 |
. . . . . . . . . . . . . . . 16
⊢ (((2
· 𝑚) − 1)
∈ ℕ → ((((2 · 𝑚) − 1) / 2) ∈ ℕ ↔ ¬
((((2 · 𝑚) −
1) + 1) / 2) ∈ ℕ)) |
113 | 85, 112 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((((2 · 𝑚) − 1) / 2) ∈ ℕ
↔ ¬ ((((2 · 𝑚) − 1) + 1) / 2) ∈
ℕ)) |
114 | 113 | con2bid 356 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((((2 · 𝑚) − 1) + 1) / 2) ∈
ℕ ↔ ¬ (((2 · 𝑚) − 1) / 2) ∈
ℕ)) |
115 | 111, 114 | mpbid 233 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ¬ (((2 ·
𝑚) − 1) / 2) ∈
ℕ) |
116 | 115 | iffalsed 4394 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → if((((2 ·
𝑚) − 1) / 2) ∈
ℕ, (𝐺‘(((2
· 𝑚) − 1) /
2)), (𝐹‘((((2
· 𝑚) − 1) + 1)
/ 2))) = (𝐹‘((((2
· 𝑚) − 1) + 1)
/ 2))) |
117 | 110 | fveq2d 6545 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐹‘((((2 · 𝑚) − 1) + 1) / 2)) = (𝐹‘𝑚)) |
118 | 96, 116, 117 | 3eqtrd 2834 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘((2 · 𝑚) − 1)) = (𝐹‘𝑚)) |
119 | | fveqeq2 6550 |
. . . . . . . . . . . 12
⊢ (𝑘 = ((2 · 𝑚) − 1) → ((𝐻‘𝑘) = (𝐹‘𝑚) ↔ (𝐻‘((2 · 𝑚) − 1)) = (𝐹‘𝑚))) |
120 | 119 | rspcev 3557 |
. . . . . . . . . . 11
⊢ ((((2
· 𝑚) − 1)
∈ ℕ ∧ (𝐻‘((2 · 𝑚) − 1)) = (𝐹‘𝑚)) → ∃𝑘 ∈ ℕ (𝐻‘𝑘) = (𝐹‘𝑚)) |
121 | 85, 118, 120 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∃𝑘 ∈ ℕ (𝐻‘𝑘) = (𝐹‘𝑚)) |
122 | | fveq2 6541 |
. . . . . . . . . . . . . 14
⊢ ((𝐻‘𝑘) = (𝐹‘𝑚) → (1st ‘(𝐻‘𝑘)) = (1st ‘(𝐹‘𝑚))) |
123 | 122 | breq1d 4974 |
. . . . . . . . . . . . 13
⊢ ((𝐻‘𝑘) = (𝐹‘𝑚) → ((1st ‘(𝐻‘𝑘)) < 𝑧 ↔ (1st ‘(𝐹‘𝑚)) < 𝑧)) |
124 | | fveq2 6541 |
. . . . . . . . . . . . . 14
⊢ ((𝐻‘𝑘) = (𝐹‘𝑚) → (2nd ‘(𝐻‘𝑘)) = (2nd ‘(𝐹‘𝑚))) |
125 | 124 | breq2d 4976 |
. . . . . . . . . . . . 13
⊢ ((𝐻‘𝑘) = (𝐹‘𝑚) → (𝑧 < (2nd ‘(𝐻‘𝑘)) ↔ 𝑧 < (2nd ‘(𝐹‘𝑚)))) |
126 | 123, 125 | anbi12d 630 |
. . . . . . . . . . . 12
⊢ ((𝐻‘𝑘) = (𝐹‘𝑚) → (((1st ‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))) ↔ ((1st ‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))))) |
127 | 126 | biimprcd 251 |
. . . . . . . . . . 11
⊢
(((1st ‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))) → ((𝐻‘𝑘) = (𝐹‘𝑚) → ((1st ‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
128 | 127 | reximdv 3235 |
. . . . . . . . . 10
⊢
(((1st ‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))) → (∃𝑘 ∈ ℕ (𝐻‘𝑘) = (𝐹‘𝑚) → ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
129 | 121, 128 | syl5com 31 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((1st
‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))) → ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
130 | 129 | rexlimdva 3246 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑚 ∈ ℕ ((1st
‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))) → ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
131 | 130 | ralimdv 3144 |
. . . . . . 7
⊢ (𝜑 → (∀𝑧 ∈ 𝐴 ∃𝑚 ∈ ℕ ((1st
‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))) → ∀𝑧 ∈ 𝐴 ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
132 | | ovolfioo 23751 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑧 ∈ 𝐴 ∃𝑚 ∈ ℕ ((1st
‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))))) |
133 | 2, 17, 132 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑧 ∈ 𝐴 ∃𝑚 ∈ ℕ ((1st
‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))))) |
134 | | ovolfioo 23751 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐻) ↔
∀𝑧 ∈ 𝐴 ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
135 | 2, 23, 134 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐻) ↔
∀𝑧 ∈ 𝐴 ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
136 | 131, 133,
135 | 3imtr4d 295 |
. . . . . 6
⊢ (𝜑 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) →
𝐴 ⊆ ∪ ran ((,) ∘ 𝐻))) |
137 | 56, 136 | mpd 15 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ∪ ran
((,) ∘ 𝐻)) |
138 | | oveq1 7026 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (2 · 𝑚) → (𝑛 / 2) = ((2 · 𝑚) / 2)) |
139 | 138 | eleq1d 2866 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (2 · 𝑚) → ((𝑛 / 2) ∈ ℕ ↔ ((2 ·
𝑚) / 2) ∈
ℕ)) |
140 | 138 | fveq2d 6545 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (2 · 𝑚) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · 𝑚) / 2))) |
141 | | oveq1 7026 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (2 · 𝑚) → (𝑛 + 1) = ((2 · 𝑚) + 1)) |
142 | 141 | fvoveq1d 7041 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (2 · 𝑚) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · 𝑚) + 1) / 2))) |
143 | 139, 140,
142 | ifbieq12d 4410 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (2 · 𝑚) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if(((2 · 𝑚) / 2) ∈ ℕ, (𝐺‘((2 · 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2)))) |
144 | | fvex 6554 |
. . . . . . . . . . . . . . 15
⊢ (𝐺‘((2 · 𝑚) / 2)) ∈
V |
145 | | fvex 6554 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘(((2 · 𝑚) + 1) / 2)) ∈
V |
146 | 144, 145 | ifex 4431 |
. . . . . . . . . . . . . 14
⊢ if(((2
· 𝑚) / 2) ∈
ℕ, (𝐺‘((2
· 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2))) ∈
V |
147 | 143, 22, 146 | fvmpt 6638 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑚) ∈ ℕ
→ (𝐻‘(2 ·
𝑚)) = if(((2 · 𝑚) / 2) ∈ ℕ, (𝐺‘((2 · 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2)))) |
148 | 99, 147 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘(2 · 𝑚)) = if(((2 · 𝑚) / 2) ∈ ℕ, (𝐺‘((2 · 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2)))) |
149 | 109, 81 | eqeltrd 2882 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((2 · 𝑚) / 2) ∈
ℕ) |
150 | 149 | iftrued 4391 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → if(((2 · 𝑚) / 2) ∈ ℕ, (𝐺‘((2 · 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2))) = (𝐺‘((2 · 𝑚) / 2))) |
151 | 109 | fveq2d 6545 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘((2 · 𝑚) / 2)) = (𝐺‘𝑚)) |
152 | 148, 150,
151 | 3eqtrd 2834 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘(2 · 𝑚)) = (𝐺‘𝑚)) |
153 | | fveqeq2 6550 |
. . . . . . . . . . . 12
⊢ (𝑘 = (2 · 𝑚) → ((𝐻‘𝑘) = (𝐺‘𝑚) ↔ (𝐻‘(2 · 𝑚)) = (𝐺‘𝑚))) |
154 | 153 | rspcev 3557 |
. . . . . . . . . . 11
⊢ (((2
· 𝑚) ∈ ℕ
∧ (𝐻‘(2 ·
𝑚)) = (𝐺‘𝑚)) → ∃𝑘 ∈ ℕ (𝐻‘𝑘) = (𝐺‘𝑚)) |
155 | 99, 152, 154 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∃𝑘 ∈ ℕ (𝐻‘𝑘) = (𝐺‘𝑚)) |
156 | | fveq2 6541 |
. . . . . . . . . . . . . 14
⊢ ((𝐻‘𝑘) = (𝐺‘𝑚) → (1st ‘(𝐻‘𝑘)) = (1st ‘(𝐺‘𝑚))) |
157 | 156 | breq1d 4974 |
. . . . . . . . . . . . 13
⊢ ((𝐻‘𝑘) = (𝐺‘𝑚) → ((1st ‘(𝐻‘𝑘)) < 𝑧 ↔ (1st ‘(𝐺‘𝑚)) < 𝑧)) |
158 | | fveq2 6541 |
. . . . . . . . . . . . . 14
⊢ ((𝐻‘𝑘) = (𝐺‘𝑚) → (2nd ‘(𝐻‘𝑘)) = (2nd ‘(𝐺‘𝑚))) |
159 | 158 | breq2d 4976 |
. . . . . . . . . . . . 13
⊢ ((𝐻‘𝑘) = (𝐺‘𝑚) → (𝑧 < (2nd ‘(𝐻‘𝑘)) ↔ 𝑧 < (2nd ‘(𝐺‘𝑚)))) |
160 | 157, 159 | anbi12d 630 |
. . . . . . . . . . . 12
⊢ ((𝐻‘𝑘) = (𝐺‘𝑚) → (((1st ‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))) ↔ ((1st ‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))))) |
161 | 160 | biimprcd 251 |
. . . . . . . . . . 11
⊢
(((1st ‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))) → ((𝐻‘𝑘) = (𝐺‘𝑚) → ((1st ‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
162 | 161 | reximdv 3235 |
. . . . . . . . . 10
⊢
(((1st ‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))) → (∃𝑘 ∈ ℕ (𝐻‘𝑘) = (𝐺‘𝑚) → ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
163 | 155, 162 | syl5com 31 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((1st
‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))) → ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
164 | 163 | rexlimdva 3246 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑚 ∈ ℕ ((1st
‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))) → ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
165 | 164 | ralimdv 3144 |
. . . . . . 7
⊢ (𝜑 → (∀𝑧 ∈ 𝐵 ∃𝑚 ∈ ℕ ((1st
‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))) → ∀𝑧 ∈ 𝐵 ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
166 | | ovolfioo 23751 |
. . . . . . . 8
⊢ ((𝐵 ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑧 ∈ 𝐵 ∃𝑚 ∈ ℕ ((1st
‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))))) |
167 | 4, 8, 166 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑧 ∈ 𝐵 ∃𝑚 ∈ ℕ ((1st
‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))))) |
168 | | ovolfioo 23751 |
. . . . . . . 8
⊢ ((𝐵 ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐻) ↔
∀𝑧 ∈ 𝐵 ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
169 | 4, 23, 168 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐻) ↔
∀𝑧 ∈ 𝐵 ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
170 | 165, 167,
169 | 3imtr4d 295 |
. . . . . 6
⊢ (𝜑 → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) →
𝐵 ⊆ ∪ ran ((,) ∘ 𝐻))) |
171 | 58, 170 | mpd 15 |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ ∪ ran
((,) ∘ 𝐻)) |
172 | 137, 171 | unssd 4085 |
. . . 4
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ ∪ ran
((,) ∘ 𝐻)) |
173 | 25 | ovollb 23763 |
. . . 4
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (𝐴 ∪ 𝐵) ⊆ ∪ ran
((,) ∘ 𝐻)) →
(vol*‘(𝐴 ∪ 𝐵)) ≤ sup(ran 𝑈, ℝ*, <
)) |
174 | 23, 172, 173 | syl2anc 584 |
. . 3
⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ sup(ran 𝑈, ℝ*, <
)) |
175 | | ovollecl 23767 |
. . 3
⊢ (((𝐴 ∪ 𝐵) ⊆ ℝ ∧ sup(ran 𝑈, ℝ*, < )
∈ ℝ ∧ (vol*‘(𝐴 ∪ 𝐵)) ≤ sup(ran 𝑈, ℝ*, < )) →
(vol*‘(𝐴 ∪ 𝐵)) ∈
ℝ) |
176 | 5, 74, 174, 175 | syl3anc 1364 |
. 2
⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ∈ ℝ) |
177 | 53 | rexrd 10540 |
. . . 4
⊢ (𝜑 → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈
ℝ*) |
178 | | supxrleub 12569 |
. . . 4
⊢ ((ran
𝑈 ⊆
ℝ* ∧ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ*) →
(sup(ran 𝑈,
ℝ*, < ) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ↔ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))) |
179 | 69, 177, 178 | syl2anc 584 |
. . 3
⊢ (𝜑 → (sup(ran 𝑈, ℝ*, < ) ≤
(((vol*‘𝐴) +
(vol*‘𝐵)) + 𝐶) ↔ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))) |
180 | 65, 179 | mpbird 258 |
. 2
⊢ (𝜑 → sup(ran 𝑈, ℝ*, < ) ≤
(((vol*‘𝐴) +
(vol*‘𝐵)) + 𝐶)) |
181 | 176, 74, 53, 174, 180 | letrd 10646 |
1
⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) |