Step | Hyp | Ref
| Expression |
1 | | ovolun.a |
. . . . 5
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈
ℝ)) |
2 | 1 | simpld 474 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
3 | | ovolun.b |
. . . . 5
⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈
ℝ)) |
4 | 3 | simpld 474 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
5 | 2, 4 | unssd 3751 |
. . 3
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ ℝ) |
6 | | ovolun.g1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
7 | | reex 9906 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
8 | 7, 7 | xpex 6860 |
. . . . . . . . . . . . . 14
⊢ (ℝ
× ℝ) ∈ V |
9 | 8 | inex2 4728 |
. . . . . . . . . . . . 13
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V |
10 | | nnex 10903 |
. . . . . . . . . . . . 13
⊢ ℕ
∈ V |
11 | 9, 10 | elmap 7772 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
12 | 6, 11 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
13 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
14 | 13 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
15 | | nneo 11337 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) ∈ ℕ ↔
¬ ((𝑛 + 1) / 2) ∈
ℕ)) |
16 | 15 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈
ℕ)) |
17 | 16 | con2bid 343 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑛 + 1) / 2) ∈ ℕ ↔ ¬ (𝑛 / 2) ∈
ℕ)) |
18 | 17 | biimpar 501 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) →
((𝑛 + 1) / 2) ∈
ℕ) |
19 | | ovolun.f1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
20 | 9, 10 | elmap 7772 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
21 | 19, 20 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
22 | 21 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
23 | 22 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ
× ℝ))) |
24 | 18, 23 | syldan 486 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) →
(𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩
(ℝ × ℝ))) |
25 | 14, 24 | ifclda 4070 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ
× ℝ))) |
26 | | ovolun.h |
. . . . . . . 8
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2)))) |
27 | 25, 26 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
28 | | eqid 2610 |
. . . . . . . 8
⊢ ((abs
∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻) |
29 | | ovolun.u |
. . . . . . . 8
⊢ 𝑈 = seq1( + , ((abs ∘
− ) ∘ 𝐻)) |
30 | 28, 29 | ovolsf 23048 |
. . . . . . 7
⊢ (𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞)) |
31 | 27, 30 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑈:ℕ⟶(0[,)+∞)) |
32 | | rge0ssre 12151 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℝ |
33 | | fss 5969 |
. . . . . 6
⊢ ((𝑈:ℕ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ) |
34 | 31, 32, 33 | sylancl 693 |
. . . . 5
⊢ (𝜑 → 𝑈:ℕ⟶ℝ) |
35 | | frn 5966 |
. . . . 5
⊢ (𝑈:ℕ⟶ℝ →
ran 𝑈 ⊆
ℝ) |
36 | 34, 35 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝑈 ⊆ ℝ) |
37 | | 1nn 10908 |
. . . . . . 7
⊢ 1 ∈
ℕ |
38 | | 1z 11284 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
39 | | seqfn 12675 |
. . . . . . . . . 10
⊢ (1 ∈
ℤ → seq1( + , ((abs ∘ − ) ∘ 𝐻)) Fn
(ℤ≥‘1)) |
40 | 38, 39 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐻)) Fn
(ℤ≥‘1)) |
41 | 29 | fneq1i 5899 |
. . . . . . . . . 10
⊢ (𝑈 Fn ℕ ↔ seq1( + ,
((abs ∘ − ) ∘ 𝐻)) Fn ℕ) |
42 | | nnuz 11599 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
43 | 42 | fneq2i 5900 |
. . . . . . . . . 10
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝐻)) Fn ℕ ↔ seq1( + , ((abs ∘
− ) ∘ 𝐻)) Fn
(ℤ≥‘1)) |
44 | 41, 43 | bitri 263 |
. . . . . . . . 9
⊢ (𝑈 Fn ℕ ↔ seq1( + ,
((abs ∘ − ) ∘ 𝐻)) Fn
(ℤ≥‘1)) |
45 | 40, 44 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 Fn ℕ) |
46 | | fndm 5904 |
. . . . . . . 8
⊢ (𝑈 Fn ℕ → dom 𝑈 = ℕ) |
47 | 45, 46 | syl 17 |
. . . . . . 7
⊢ (𝜑 → dom 𝑈 = ℕ) |
48 | 37, 47 | syl5eleqr 2695 |
. . . . . 6
⊢ (𝜑 → 1 ∈ dom 𝑈) |
49 | | ne0i 3880 |
. . . . . 6
⊢ (1 ∈
dom 𝑈 → dom 𝑈 ≠ ∅) |
50 | 48, 49 | syl 17 |
. . . . 5
⊢ (𝜑 → dom 𝑈 ≠ ∅) |
51 | | dm0rn0 5263 |
. . . . . 6
⊢ (dom
𝑈 = ∅ ↔ ran
𝑈 =
∅) |
52 | 51 | necon3bii 2834 |
. . . . 5
⊢ (dom
𝑈 ≠ ∅ ↔ ran
𝑈 ≠
∅) |
53 | 50, 52 | sylib 207 |
. . . 4
⊢ (𝜑 → ran 𝑈 ≠ ∅) |
54 | 1 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → (vol*‘𝐴) ∈
ℝ) |
55 | 3 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → (vol*‘𝐵) ∈
ℝ) |
56 | 54, 55 | readdcld 9948 |
. . . . . . 7
⊢ (𝜑 → ((vol*‘𝐴) + (vol*‘𝐵)) ∈
ℝ) |
57 | | ovolun.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
58 | 57 | rpred 11748 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℝ) |
59 | 56, 58 | readdcld 9948 |
. . . . . 6
⊢ (𝜑 → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ) |
60 | | ovolun.s |
. . . . . . . . 9
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
61 | | ovolun.t |
. . . . . . . . 9
⊢ 𝑇 = seq1( + , ((abs ∘
− ) ∘ 𝐺)) |
62 | | ovolun.f2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ∪ ran
((,) ∘ 𝐹)) |
63 | | ovolun.f3 |
. . . . . . . . 9
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 / 2))) |
64 | | ovolun.g2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ⊆ ∪ ran
((,) ∘ 𝐺)) |
65 | | ovolun.g3 |
. . . . . . . . 9
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤
((vol*‘𝐵) + (𝐶 / 2))) |
66 | 1, 3, 57, 60, 61, 29, 19, 62, 63, 6, 64, 65, 26 | ovolunlem1a 23071 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) |
67 | 66 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) |
68 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑧 = (𝑈‘𝑘) → (𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ↔ (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))) |
69 | 68 | ralrn 6270 |
. . . . . . . 8
⊢ (𝑈 Fn ℕ →
(∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ↔ ∀𝑘 ∈ ℕ (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))) |
70 | 45, 69 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ↔ ∀𝑘 ∈ ℕ (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))) |
71 | 67, 70 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) |
72 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑘 = (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) → (𝑧 ≤ 𝑘 ↔ 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))) |
73 | 72 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑘 = (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑘 ↔ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))) |
74 | 73 | rspcev 3282 |
. . . . . 6
⊢
(((((vol*‘𝐴) +
(vol*‘𝐵)) + 𝐶) ∈ ℝ ∧
∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) → ∃𝑘 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑘) |
75 | 59, 71, 74 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑘) |
76 | | ressxr 9962 |
. . . . . . 7
⊢ ℝ
⊆ ℝ* |
77 | 36, 76 | syl6ss 3580 |
. . . . . 6
⊢ (𝜑 → ran 𝑈 ⊆
ℝ*) |
78 | | supxrbnd2 12024 |
. . . . . 6
⊢ (ran
𝑈 ⊆
ℝ* → (∃𝑘 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑘 ↔ sup(ran 𝑈, ℝ*, < ) <
+∞)) |
79 | 77, 78 | syl 17 |
. . . . 5
⊢ (𝜑 → (∃𝑘 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑘 ↔ sup(ran 𝑈, ℝ*, < ) <
+∞)) |
80 | 75, 79 | mpbid 221 |
. . . 4
⊢ (𝜑 → sup(ran 𝑈, ℝ*, < ) <
+∞) |
81 | | supxrbnd 12030 |
. . . 4
⊢ ((ran
𝑈 ⊆ ℝ ∧ ran
𝑈 ≠ ∅ ∧
sup(ran 𝑈,
ℝ*, < ) < +∞) → sup(ran 𝑈, ℝ*, < ) ∈
ℝ) |
82 | 36, 53, 80, 81 | syl3anc 1318 |
. . 3
⊢ (𝜑 → sup(ran 𝑈, ℝ*, < ) ∈
ℝ) |
83 | | nncn 10905 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
84 | 83 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ) |
85 | 84 | 2timesd 11152 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2 · 𝑚) = (𝑚 + 𝑚)) |
86 | 85 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((2 · 𝑚) − 1) = ((𝑚 + 𝑚) − 1)) |
87 | | 1cnd 9935 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 1 ∈
ℂ) |
88 | 84, 84, 87 | addsubassd 10291 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 + 𝑚) − 1) = (𝑚 + (𝑚 − 1))) |
89 | 86, 88 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((2 · 𝑚) − 1) = (𝑚 + (𝑚 − 1))) |
90 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ) |
91 | | nnm1nn0 11211 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → (𝑚 − 1) ∈
ℕ0) |
92 | 91 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 − 1) ∈
ℕ0) |
93 | | nnnn0addcl 11200 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 − 1) ∈
ℕ0) → (𝑚 + (𝑚 − 1)) ∈ ℕ) |
94 | 90, 92, 93 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 + (𝑚 − 1)) ∈ ℕ) |
95 | 89, 94 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((2 · 𝑚) − 1) ∈
ℕ) |
96 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = ((2 · 𝑚) − 1) → (𝑛 / 2) = (((2 · 𝑚) − 1) /
2)) |
97 | 96 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = ((2 · 𝑚) − 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2
· 𝑚) − 1) / 2)
∈ ℕ)) |
98 | 96 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = ((2 · 𝑚) − 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑚) − 1) / 2))) |
99 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = ((2 · 𝑚) − 1) → (𝑛 + 1) = (((2 · 𝑚) − 1) +
1)) |
100 | 99 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = ((2 · 𝑚) − 1) → ((𝑛 + 1) / 2) = ((((2 ·
𝑚) − 1) + 1) /
2)) |
101 | 100 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = ((2 · 𝑚) − 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑚) − 1) + 1) / 2))) |
102 | 97, 98, 101 | ifbieq12d 4063 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = ((2 · 𝑚) − 1) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if((((2 · 𝑚) − 1) / 2) ∈
ℕ, (𝐺‘(((2
· 𝑚) − 1) /
2)), (𝐹‘((((2
· 𝑚) − 1) + 1)
/ 2)))) |
103 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐺‘(((2 · 𝑚) − 1) / 2)) ∈
V |
104 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘((((2 · 𝑚) − 1) + 1) / 2)) ∈
V |
105 | 103, 104 | ifex 4106 |
. . . . . . . . . . . . . 14
⊢ if((((2
· 𝑚) − 1) / 2)
∈ ℕ, (𝐺‘(((2 · 𝑚) − 1) / 2)), (𝐹‘((((2 · 𝑚) − 1) + 1) / 2))) ∈
V |
106 | 102, 26, 105 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ (((2
· 𝑚) − 1)
∈ ℕ → (𝐻‘((2 · 𝑚) − 1)) = if((((2 · 𝑚) − 1) / 2) ∈
ℕ, (𝐺‘(((2
· 𝑚) − 1) /
2)), (𝐹‘((((2
· 𝑚) − 1) + 1)
/ 2)))) |
107 | 95, 106 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘((2 · 𝑚) − 1)) = if((((2 · 𝑚) − 1) / 2) ∈
ℕ, (𝐺‘(((2
· 𝑚) − 1) /
2)), (𝐹‘((((2
· 𝑚) − 1) + 1)
/ 2)))) |
108 | | 2nn 11062 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℕ |
109 | | nnmulcl 10920 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ ℕ ∧ 𝑚
∈ ℕ) → (2 · 𝑚) ∈ ℕ) |
110 | 108, 90, 109 | sylancr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2 · 𝑚) ∈
ℕ) |
111 | 110 | nncnd 10913 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2 · 𝑚) ∈
ℂ) |
112 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
113 | | npcan 10169 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· 𝑚) ∈ ℂ
∧ 1 ∈ ℂ) → (((2 · 𝑚) − 1) + 1) = (2 · 𝑚)) |
114 | 111, 112,
113 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((2 · 𝑚) − 1) + 1) = (2 ·
𝑚)) |
115 | 114 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((((2 · 𝑚) − 1) + 1) / 2) = ((2
· 𝑚) /
2)) |
116 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℂ |
117 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 |
118 | | divcan3 10590 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → ((2 · 𝑚) / 2) = 𝑚) |
119 | 116, 117,
118 | mp3an23 1408 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℂ → ((2
· 𝑚) / 2) = 𝑚) |
120 | 84, 119 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((2 · 𝑚) / 2) = 𝑚) |
121 | 115, 120 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((((2 · 𝑚) − 1) + 1) / 2) = 𝑚) |
122 | 121, 90 | eqeltrd 2688 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((((2 · 𝑚) − 1) + 1) / 2) ∈
ℕ) |
123 | | nneo 11337 |
. . . . . . . . . . . . . . . 16
⊢ (((2
· 𝑚) − 1)
∈ ℕ → ((((2 · 𝑚) − 1) / 2) ∈ ℕ ↔ ¬
((((2 · 𝑚) −
1) + 1) / 2) ∈ ℕ)) |
124 | 95, 123 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((((2 · 𝑚) − 1) / 2) ∈ ℕ
↔ ¬ ((((2 · 𝑚) − 1) + 1) / 2) ∈
ℕ)) |
125 | 124 | con2bid 343 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((((2 · 𝑚) − 1) + 1) / 2) ∈
ℕ ↔ ¬ (((2 · 𝑚) − 1) / 2) ∈
ℕ)) |
126 | 122, 125 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ¬ (((2 ·
𝑚) − 1) / 2) ∈
ℕ) |
127 | 126 | iffalsed 4047 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → if((((2 ·
𝑚) − 1) / 2) ∈
ℕ, (𝐺‘(((2
· 𝑚) − 1) /
2)), (𝐹‘((((2
· 𝑚) − 1) + 1)
/ 2))) = (𝐹‘((((2
· 𝑚) − 1) + 1)
/ 2))) |
128 | 121 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐹‘((((2 · 𝑚) − 1) + 1) / 2)) = (𝐹‘𝑚)) |
129 | 107, 127,
128 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘((2 · 𝑚) − 1)) = (𝐹‘𝑚)) |
130 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ((2 · 𝑚) − 1) → (𝐻‘𝑘) = (𝐻‘((2 · 𝑚) − 1))) |
131 | 130 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑘 = ((2 · 𝑚) − 1) → ((𝐻‘𝑘) = (𝐹‘𝑚) ↔ (𝐻‘((2 · 𝑚) − 1)) = (𝐹‘𝑚))) |
132 | 131 | rspcev 3282 |
. . . . . . . . . . 11
⊢ ((((2
· 𝑚) − 1)
∈ ℕ ∧ (𝐻‘((2 · 𝑚) − 1)) = (𝐹‘𝑚)) → ∃𝑘 ∈ ℕ (𝐻‘𝑘) = (𝐹‘𝑚)) |
133 | 95, 129, 132 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∃𝑘 ∈ ℕ (𝐻‘𝑘) = (𝐹‘𝑚)) |
134 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ ((𝐻‘𝑘) = (𝐹‘𝑚) → (1st ‘(𝐻‘𝑘)) = (1st ‘(𝐹‘𝑚))) |
135 | 134 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝐻‘𝑘) = (𝐹‘𝑚) → ((1st ‘(𝐻‘𝑘)) < 𝑧 ↔ (1st ‘(𝐹‘𝑚)) < 𝑧)) |
136 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ ((𝐻‘𝑘) = (𝐹‘𝑚) → (2nd ‘(𝐻‘𝑘)) = (2nd ‘(𝐹‘𝑚))) |
137 | 136 | breq2d 4595 |
. . . . . . . . . . . . 13
⊢ ((𝐻‘𝑘) = (𝐹‘𝑚) → (𝑧 < (2nd ‘(𝐻‘𝑘)) ↔ 𝑧 < (2nd ‘(𝐹‘𝑚)))) |
138 | 135, 137 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ ((𝐻‘𝑘) = (𝐹‘𝑚) → (((1st ‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))) ↔ ((1st ‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))))) |
139 | 138 | biimprcd 239 |
. . . . . . . . . . 11
⊢
(((1st ‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))) → ((𝐻‘𝑘) = (𝐹‘𝑚) → ((1st ‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
140 | 139 | reximdv 2999 |
. . . . . . . . . 10
⊢
(((1st ‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))) → (∃𝑘 ∈ ℕ (𝐻‘𝑘) = (𝐹‘𝑚) → ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
141 | 133, 140 | syl5com 31 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((1st
‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))) → ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
142 | 141 | rexlimdva 3013 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑚 ∈ ℕ ((1st
‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))) → ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
143 | 142 | ralimdv 2946 |
. . . . . . 7
⊢ (𝜑 → (∀𝑧 ∈ 𝐴 ∃𝑚 ∈ ℕ ((1st
‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))) → ∀𝑧 ∈ 𝐴 ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
144 | | ovolfioo 23043 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑧 ∈ 𝐴 ∃𝑚 ∈ ℕ ((1st
‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))))) |
145 | 2, 21, 144 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑧 ∈ 𝐴 ∃𝑚 ∈ ℕ ((1st
‘(𝐹‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑚))))) |
146 | | ovolfioo 23043 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐻) ↔
∀𝑧 ∈ 𝐴 ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
147 | 2, 27, 146 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐻) ↔
∀𝑧 ∈ 𝐴 ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
148 | 143, 145,
147 | 3imtr4d 282 |
. . . . . 6
⊢ (𝜑 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) →
𝐴 ⊆ ∪ ran ((,) ∘ 𝐻))) |
149 | 62, 148 | mpd 15 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ∪ ran
((,) ∘ 𝐻)) |
150 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (2 · 𝑚) → (𝑛 / 2) = ((2 · 𝑚) / 2)) |
151 | 150 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (2 · 𝑚) → ((𝑛 / 2) ∈ ℕ ↔ ((2 ·
𝑚) / 2) ∈
ℕ)) |
152 | 150 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (2 · 𝑚) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · 𝑚) / 2))) |
153 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (2 · 𝑚) → (𝑛 + 1) = ((2 · 𝑚) + 1)) |
154 | 153 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (2 · 𝑚) → ((𝑛 + 1) / 2) = (((2 · 𝑚) + 1) / 2)) |
155 | 154 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (2 · 𝑚) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · 𝑚) + 1) / 2))) |
156 | 151, 152,
155 | ifbieq12d 4063 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (2 · 𝑚) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if(((2 · 𝑚) / 2) ∈ ℕ, (𝐺‘((2 · 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2)))) |
157 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐺‘((2 · 𝑚) / 2)) ∈
V |
158 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘(((2 · 𝑚) + 1) / 2)) ∈
V |
159 | 157, 158 | ifex 4106 |
. . . . . . . . . . . . . 14
⊢ if(((2
· 𝑚) / 2) ∈
ℕ, (𝐺‘((2
· 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2))) ∈
V |
160 | 156, 26, 159 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑚) ∈ ℕ
→ (𝐻‘(2 ·
𝑚)) = if(((2 · 𝑚) / 2) ∈ ℕ, (𝐺‘((2 · 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2)))) |
161 | 110, 160 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘(2 · 𝑚)) = if(((2 · 𝑚) / 2) ∈ ℕ, (𝐺‘((2 · 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2)))) |
162 | 120, 90 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((2 · 𝑚) / 2) ∈
ℕ) |
163 | 162 | iftrued 4044 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → if(((2 · 𝑚) / 2) ∈ ℕ, (𝐺‘((2 · 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2))) = (𝐺‘((2 · 𝑚) / 2))) |
164 | 120 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘((2 · 𝑚) / 2)) = (𝐺‘𝑚)) |
165 | 161, 163,
164 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘(2 · 𝑚)) = (𝐺‘𝑚)) |
166 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (2 · 𝑚) → (𝐻‘𝑘) = (𝐻‘(2 · 𝑚))) |
167 | 166 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑘 = (2 · 𝑚) → ((𝐻‘𝑘) = (𝐺‘𝑚) ↔ (𝐻‘(2 · 𝑚)) = (𝐺‘𝑚))) |
168 | 167 | rspcev 3282 |
. . . . . . . . . . 11
⊢ (((2
· 𝑚) ∈ ℕ
∧ (𝐻‘(2 ·
𝑚)) = (𝐺‘𝑚)) → ∃𝑘 ∈ ℕ (𝐻‘𝑘) = (𝐺‘𝑚)) |
169 | 110, 165,
168 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∃𝑘 ∈ ℕ (𝐻‘𝑘) = (𝐺‘𝑚)) |
170 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ ((𝐻‘𝑘) = (𝐺‘𝑚) → (1st ‘(𝐻‘𝑘)) = (1st ‘(𝐺‘𝑚))) |
171 | 170 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝐻‘𝑘) = (𝐺‘𝑚) → ((1st ‘(𝐻‘𝑘)) < 𝑧 ↔ (1st ‘(𝐺‘𝑚)) < 𝑧)) |
172 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ ((𝐻‘𝑘) = (𝐺‘𝑚) → (2nd ‘(𝐻‘𝑘)) = (2nd ‘(𝐺‘𝑚))) |
173 | 172 | breq2d 4595 |
. . . . . . . . . . . . 13
⊢ ((𝐻‘𝑘) = (𝐺‘𝑚) → (𝑧 < (2nd ‘(𝐻‘𝑘)) ↔ 𝑧 < (2nd ‘(𝐺‘𝑚)))) |
174 | 171, 173 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ ((𝐻‘𝑘) = (𝐺‘𝑚) → (((1st ‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))) ↔ ((1st ‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))))) |
175 | 174 | biimprcd 239 |
. . . . . . . . . . 11
⊢
(((1st ‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))) → ((𝐻‘𝑘) = (𝐺‘𝑚) → ((1st ‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
176 | 175 | reximdv 2999 |
. . . . . . . . . 10
⊢
(((1st ‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))) → (∃𝑘 ∈ ℕ (𝐻‘𝑘) = (𝐺‘𝑚) → ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
177 | 169, 176 | syl5com 31 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((1st
‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))) → ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
178 | 177 | rexlimdva 3013 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑚 ∈ ℕ ((1st
‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))) → ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
179 | 178 | ralimdv 2946 |
. . . . . . 7
⊢ (𝜑 → (∀𝑧 ∈ 𝐵 ∃𝑚 ∈ ℕ ((1st
‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))) → ∀𝑧 ∈ 𝐵 ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
180 | | ovolfioo 23043 |
. . . . . . . 8
⊢ ((𝐵 ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑧 ∈ 𝐵 ∃𝑚 ∈ ℕ ((1st
‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))))) |
181 | 4, 12, 180 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑧 ∈ 𝐵 ∃𝑚 ∈ ℕ ((1st
‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))))) |
182 | | ovolfioo 23043 |
. . . . . . . 8
⊢ ((𝐵 ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐻) ↔
∀𝑧 ∈ 𝐵 ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
183 | 4, 27, 182 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐻) ↔
∀𝑧 ∈ 𝐵 ∃𝑘 ∈ ℕ ((1st
‘(𝐻‘𝑘)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑘))))) |
184 | 179, 181,
183 | 3imtr4d 282 |
. . . . . 6
⊢ (𝜑 → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) →
𝐵 ⊆ ∪ ran ((,) ∘ 𝐻))) |
185 | 64, 184 | mpd 15 |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ ∪ ran
((,) ∘ 𝐻)) |
186 | 149, 185 | unssd 3751 |
. . . 4
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ ∪ ran
((,) ∘ 𝐻)) |
187 | 29 | ovollb 23054 |
. . . 4
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (𝐴 ∪ 𝐵) ⊆ ∪ ran
((,) ∘ 𝐻)) →
(vol*‘(𝐴 ∪ 𝐵)) ≤ sup(ran 𝑈, ℝ*, <
)) |
188 | 27, 186, 187 | syl2anc 691 |
. . 3
⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ sup(ran 𝑈, ℝ*, <
)) |
189 | | ovollecl 23058 |
. . 3
⊢ (((𝐴 ∪ 𝐵) ⊆ ℝ ∧ sup(ran 𝑈, ℝ*, < )
∈ ℝ ∧ (vol*‘(𝐴 ∪ 𝐵)) ≤ sup(ran 𝑈, ℝ*, < )) →
(vol*‘(𝐴 ∪ 𝐵)) ∈
ℝ) |
190 | 5, 82, 188, 189 | syl3anc 1318 |
. 2
⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ∈ ℝ) |
191 | 59 | rexrd 9968 |
. . . 4
⊢ (𝜑 → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈
ℝ*) |
192 | | supxrleub 12028 |
. . . 4
⊢ ((ran
𝑈 ⊆
ℝ* ∧ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ*) →
(sup(ran 𝑈,
ℝ*, < ) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ↔ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))) |
193 | 77, 191, 192 | syl2anc 691 |
. . 3
⊢ (𝜑 → (sup(ran 𝑈, ℝ*, < ) ≤
(((vol*‘𝐴) +
(vol*‘𝐵)) + 𝐶) ↔ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))) |
194 | 71, 193 | mpbird 246 |
. 2
⊢ (𝜑 → sup(ran 𝑈, ℝ*, < ) ≤
(((vol*‘𝐴) +
(vol*‘𝐵)) + 𝐶)) |
195 | 190, 82, 59, 188, 194 | letrd 10073 |
1
⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) |