Step | Hyp | Ref
| Expression |
1 | | hspmbllem3.a |
. . . 4
⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ) |
2 | | hspmbllem3.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
3 | | inss1 3833 |
. . . . . 6
⊢ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ 𝐴 |
4 | | hspmbllem3.s |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚
𝑋)) |
5 | 3, 4 | syl5ss 3614 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ (ℝ
↑𝑚 𝑋)) |
6 | 2, 5 | ovncl 40781 |
. . . 4
⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∈ (0[,]+∞)) |
7 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ 𝐴) |
8 | 2, 7, 4 | ovnssle 40775 |
. . . 4
⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ≤ ((voln*‘𝑋)‘𝐴)) |
9 | 1, 6, 8 | ge0lere 39759 |
. . 3
⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ) |
10 | 4 | ssdifssd 3748 |
. . . . 5
⊢ (𝜑 → (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) ⊆ (ℝ
↑𝑚 𝑋)) |
11 | 2, 10 | ovncl 40781 |
. . . 4
⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∈ (0[,]+∞)) |
12 | | difssd 3738 |
. . . . 5
⊢ (𝜑 → (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) ⊆ 𝐴) |
13 | 2, 12, 4 | ovnssle 40775 |
. . . 4
⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ≤ ((voln*‘𝑋)‘𝐴)) |
14 | 1, 11, 13 | ge0lere 39759 |
. . 3
⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ) |
15 | | rexadd 12063 |
. . 3
⊢
((((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ ∧ ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ) →
(((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) +𝑒
((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) = (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))))) |
16 | 9, 14, 15 | syl2anc 693 |
. 2
⊢ (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) +𝑒
((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) = (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))))) |
17 | 2 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ Fin) |
18 | | hspmbllem3.i |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ 𝑋) |
19 | | ne0i 3921 |
. . . . . . . 8
⊢ (𝐾 ∈ 𝑋 → 𝑋 ≠ ∅) |
20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ≠ ∅) |
21 | 20 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑋 ≠ ∅) |
22 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝐴 ⊆ (ℝ
↑𝑚 𝑋)) |
23 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
ℝ+) |
24 | | hspmbllem3.c |
. . . . . 6
⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
25 | | hspmbllem3.l |
. . . . . 6
⊢ 𝐿 = (ℎ ∈ ((ℝ × ℝ)
↑𝑚 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘))) |
26 | | hspmbllem3.d |
. . . . . 6
⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)})) |
27 | 17, 21, 22, 23, 24, 25, 26 | ovncvrrp 40778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑖 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) |
28 | | hspmbllem3.h |
. . . . . . . 8
⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))) |
29 | 17 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → 𝑋 ∈ Fin) |
30 | 18 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → 𝐾 ∈ 𝑋) |
31 | | hspmbllem3.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ ℝ) |
32 | 31 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → 𝑌 ∈ ℝ) |
33 | 23 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → 𝑒 ∈ ℝ+) |
34 | 22 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → 𝐴 ⊆ (ℝ ↑𝑚
𝑋)) |
35 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = ℎ → (𝑖‘𝑗) = (ℎ‘𝑗)) |
36 | 35 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = ℎ → (𝐿‘(𝑖‘𝑗)) = (𝐿‘(ℎ‘𝑗))) |
37 | 36 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = ℎ → (𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘(ℎ‘𝑗)))) |
38 | 37 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = ℎ →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(ℎ‘𝑗))))) |
39 | 38 | breq1d 4663 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = ℎ →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(ℎ‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟))) |
40 | 39 | cbvrabv 3199 |
. . . . . . . . . . . . . 14
⊢ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)} = {ℎ ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(ℎ‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)} |
41 | 40 | mpteq2i 4741 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ+
↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)}) = (𝑟 ∈ ℝ+ ↦ {ℎ ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(ℎ‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)}) |
42 | 41 | mpteq2i 4741 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)})) = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑟 ∈ ℝ+ ↦ {ℎ ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(ℎ‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)})) |
43 | 26, 42 | eqtri 2644 |
. . . . . . . . . . 11
⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑟 ∈ ℝ+ ↦ {ℎ ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(ℎ‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)})) |
44 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) |
45 | | hspmbllem3.10 |
. . . . . . . . . . 11
⊢ 𝐵 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑘)))) |
46 | | hspmbllem3.11 |
. . . . . . . . . . 11
⊢ 𝑇 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑘)))) |
47 | 29, 34, 33, 24, 25, 43, 44, 45, 46 | ovncvr2 40825 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → (((𝐵:ℕ⟶(ℝ
↑𝑚 𝑋) ∧ 𝑇:ℕ⟶(ℝ
↑𝑚 𝑋)) ∧ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐵‘𝑗)‘𝑘)[,)((𝑇‘𝑗)‘𝑘))) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐵‘𝑗)‘𝑘)[,)((𝑇‘𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒))) |
48 | 47 | simplld 791 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → (𝐵:ℕ⟶(ℝ
↑𝑚 𝑋) ∧ 𝑇:ℕ⟶(ℝ
↑𝑚 𝑋))) |
49 | 48 | simpld 475 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → 𝐵:ℕ⟶(ℝ
↑𝑚 𝑋)) |
50 | 48 | simprd 479 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → 𝑇:ℕ⟶(ℝ
↑𝑚 𝑋)) |
51 | 47 | simplrd 793 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐵‘𝑗)‘𝑘)[,)((𝑇‘𝑗)‘𝑘))) |
52 | 47 | simprd 479 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐵‘𝑗)‘𝑘)[,)((𝑇‘𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)) |
53 | 1 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
((voln*‘𝑋)‘𝐴) ∈ ℝ) |
54 | 23 | rpred 11872 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
ℝ) |
55 | 53, 54 | rexaddd 12065 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(((voln*‘𝑋)‘𝐴) +𝑒 𝑒) = (((voln*‘𝑋)‘𝐴) + 𝑒)) |
56 | 55 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → (((voln*‘𝑋)‘𝐴) +𝑒 𝑒) = (((voln*‘𝑋)‘𝐴) + 𝑒)) |
57 | 52, 56 | breqtrd 4679 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐵‘𝑗)‘𝑘)[,)((𝑇‘𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝑒)) |
58 | 1 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → ((voln*‘𝑋)‘𝐴) ∈ ℝ) |
59 | 9 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ) |
60 | 14 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ) |
61 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ
↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
62 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ
↑𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) |
63 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ
↑𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ))))) |
64 | 28, 29, 30, 32, 33, 49, 50, 51, 57, 58, 59, 60, 61, 62, 63 | hspmbllem2 40841 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑖 ∈ ((𝐷‘𝐴)‘𝑒)) → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝑒)) |
65 | 64 | ex 450 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (𝑖 ∈ ((𝐷‘𝐴)‘𝑒) → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝑒))) |
66 | 65 | exlimdv 1861 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(∃𝑖 𝑖 ∈ ((𝐷‘𝐴)‘𝑒) → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝑒))) |
67 | 27, 66 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝑒)) |
68 | 67 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑒 ∈ ℝ+
(((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝑒)) |
69 | 9, 14 | readdcld 10069 |
. . . 4
⊢ (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ∈ ℝ) |
70 | | alrple 12037 |
. . . 4
⊢
(((((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ∈ ℝ ∧
((voln*‘𝑋)‘𝐴) ∈ ℝ) →
((((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((voln*‘𝑋)‘𝐴) ↔ ∀𝑒 ∈ ℝ+
(((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝑒))) |
71 | 69, 1, 70 | syl2anc 693 |
. . 3
⊢ (𝜑 → ((((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((voln*‘𝑋)‘𝐴) ↔ ∀𝑒 ∈ ℝ+
(((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝑒))) |
72 | 68, 71 | mpbird 247 |
. 2
⊢ (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((voln*‘𝑋)‘𝐴)) |
73 | 16, 72 | eqbrtrd 4675 |
1
⊢ (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) +𝑒
((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((voln*‘𝑋)‘𝐴)) |