| Step | Hyp | Ref
| Expression |
| 1 | | simpll 767 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐴 ∈ dom vol) |
| 2 | | mnfxr 11318 |
. . . . . 6
⊢ -∞
∈ ℝ* |
| 3 | 2 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → -∞ ∈
ℝ*) |
| 4 | | iccssxr 13470 |
. . . . . . 7
⊢
(0[,](vol‘𝐴))
⊆ ℝ* |
| 5 | | simpr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 𝐵 ∈ (0[,](vol‘𝐴))) |
| 6 | 4, 5 | sselid 3981 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 𝐵 ∈
ℝ*) |
| 7 | 6 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐵 ∈
ℝ*) |
| 8 | | iccssxr 13470 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
| 9 | | volf 25564 |
. . . . . . . . 9
⊢ vol:dom
vol⟶(0[,]+∞) |
| 10 | 9 | ffvelcdmi 7103 |
. . . . . . . 8
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
(0[,]+∞)) |
| 11 | 8, 10 | sselid 3981 |
. . . . . . 7
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
ℝ*) |
| 12 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (vol‘𝐴) ∈
ℝ*) |
| 13 | 12 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → (vol‘𝐴) ∈
ℝ*) |
| 14 | | 0xr 11308 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
| 15 | | elicc1 13431 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ (vol‘𝐴) ∈ ℝ*) → (𝐵 ∈ (0[,](vol‘𝐴)) ↔ (𝐵 ∈ ℝ* ∧ 0 ≤
𝐵 ∧ 𝐵 ≤ (vol‘𝐴)))) |
| 16 | 14, 12, 15 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 ∈ (0[,](vol‘𝐴)) ↔ (𝐵 ∈ ℝ* ∧ 0 ≤
𝐵 ∧ 𝐵 ≤ (vol‘𝐴)))) |
| 17 | 5, 16 | mpbid 232 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 ∈ ℝ* ∧ 0 ≤
𝐵 ∧ 𝐵 ≤ (vol‘𝐴))) |
| 18 | 17 | simp2d 1144 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 0 ≤ 𝐵) |
| 19 | 18 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 0 ≤ 𝐵) |
| 20 | | mnflt0 13167 |
. . . . . . . 8
⊢ -∞
< 0 |
| 21 | | xrltletr 13199 |
. . . . . . . 8
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((-∞ < 0 ∧ 0 ≤ 𝐵) → -∞ < 𝐵)) |
| 22 | 20, 21 | mpani 696 |
. . . . . . 7
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (0 ≤ 𝐵 → -∞ < 𝐵)) |
| 23 | 2, 14, 22 | mp3an12 1453 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
→ (0 ≤ 𝐵 →
-∞ < 𝐵)) |
| 24 | 7, 19, 23 | sylc 65 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → -∞ < 𝐵) |
| 25 | | simpr 484 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐵 < (vol‘𝐴)) |
| 26 | | xrre2 13212 |
. . . . 5
⊢
(((-∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧
(vol‘𝐴) ∈
ℝ*) ∧ (-∞ < 𝐵 ∧ 𝐵 < (vol‘𝐴))) → 𝐵 ∈ ℝ) |
| 27 | 3, 7, 13, 24, 25, 26 | syl32anc 1380 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐵 ∈ ℝ) |
| 28 | | volsup2 25640 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
| 29 | 1, 27, 25, 28 | syl3anc 1373 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
| 30 | | nnre 12273 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
| 31 | 30 | ad2antrl 728 |
. . . . . 6
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝑛 ∈ ℝ) |
| 32 | 31 | renegcld 11690 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → -𝑛 ∈ ℝ) |
| 33 | 27 | adantr 480 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 ∈ ℝ) |
| 34 | | 0red 11264 |
. . . . . 6
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 0 ∈
ℝ) |
| 35 | | nngt0 12297 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 0 <
𝑛) |
| 36 | 35 | ad2antrl 728 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 0 < 𝑛) |
| 37 | 31 | lt0neg2d 11833 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (0 < 𝑛 ↔ -𝑛 < 0)) |
| 38 | 36, 37 | mpbid 232 |
. . . . . 6
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → -𝑛 < 0) |
| 39 | 32, 34, 31, 38, 36 | lttrd 11422 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → -𝑛 < 𝑛) |
| 40 | | iccssre 13469 |
. . . . . 6
⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ⊆ ℝ) |
| 41 | 32, 31, 40 | syl2anc 584 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (-𝑛[,]𝑛) ⊆ ℝ) |
| 42 | | ax-resscn 11212 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
| 43 | | ssid 4006 |
. . . . . . 7
⊢ ℂ
⊆ ℂ |
| 44 | | cncfss 24925 |
. . . . . . 7
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ)) |
| 45 | 42, 43, 44 | mp2an 692 |
. . . . . 6
⊢
(ℝ–cn→ℝ)
⊆ (ℝ–cn→ℂ) |
| 46 | 1 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐴 ∈ dom vol) |
| 47 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ ↦
(vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) = (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) |
| 48 | 47 | volcn 25641 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ -𝑛 ∈ ℝ) → (𝑦 ∈ ℝ ↦
(vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ)) |
| 49 | 46, 32, 48 | syl2anc 584 |
. . . . . 6
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ)) |
| 50 | 45, 49 | sselid 3981 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) ∈ (ℝ–cn→ℂ)) |
| 51 | 41 | sselda 3983 |
. . . . . 6
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑢 ∈ (-𝑛[,]𝑛)) → 𝑢 ∈ ℝ) |
| 52 | | cncff 24919 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ↦
(vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))):ℝ⟶ℝ) |
| 53 | 49, 52 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))):ℝ⟶ℝ) |
| 54 | 53 | ffvelcdmda 7104 |
. . . . . 6
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑢 ∈ ℝ) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑢) ∈ ℝ) |
| 55 | 51, 54 | syldan 591 |
. . . . 5
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑢 ∈ (-𝑛[,]𝑛)) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑢) ∈ ℝ) |
| 56 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑦 = -𝑛 → (-𝑛[,]𝑦) = (-𝑛[,]-𝑛)) |
| 57 | 56 | ineq2d 4220 |
. . . . . . . . . . 11
⊢ (𝑦 = -𝑛 → (𝐴 ∩ (-𝑛[,]𝑦)) = (𝐴 ∩ (-𝑛[,]-𝑛))) |
| 58 | 57 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑦 = -𝑛 → (vol‘(𝐴 ∩ (-𝑛[,]𝑦))) = (vol‘(𝐴 ∩ (-𝑛[,]-𝑛)))) |
| 59 | | fvex 6919 |
. . . . . . . . . 10
⊢
(vol‘(𝐴 ∩
(-𝑛[,]-𝑛))) ∈ V |
| 60 | 58, 47, 59 | fvmpt 7016 |
. . . . . . . . 9
⊢ (-𝑛 ∈ ℝ → ((𝑦 ∈ ℝ ↦
(vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) = (vol‘(𝐴 ∩ (-𝑛[,]-𝑛)))) |
| 61 | 32, 60 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) = (vol‘(𝐴 ∩ (-𝑛[,]-𝑛)))) |
| 62 | | inss2 4238 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ (-𝑛[,]-𝑛) |
| 63 | 32 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → -𝑛 ∈ ℝ*) |
| 64 | | iccid 13432 |
. . . . . . . . . . . . 13
⊢ (-𝑛 ∈ ℝ*
→ (-𝑛[,]-𝑛) = {-𝑛}) |
| 65 | 63, 64 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (-𝑛[,]-𝑛) = {-𝑛}) |
| 66 | 62, 65 | sseqtrid 4026 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ {-𝑛}) |
| 67 | 32 | snssd 4809 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → {-𝑛} ⊆ ℝ) |
| 68 | 66, 67 | sstrd 3994 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ ℝ) |
| 69 | | ovolsn 25530 |
. . . . . . . . . . . 12
⊢ (-𝑛 ∈ ℝ →
(vol*‘{-𝑛}) =
0) |
| 70 | 32, 69 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (vol*‘{-𝑛}) = 0) |
| 71 | | ovolssnul 25522 |
. . . . . . . . . . 11
⊢ (((𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ {-𝑛} ∧ {-𝑛} ⊆ ℝ ∧ (vol*‘{-𝑛}) = 0) →
(vol*‘(𝐴 ∩
(-𝑛[,]-𝑛))) = 0) |
| 72 | 66, 67, 70, 71 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (vol*‘(𝐴 ∩ (-𝑛[,]-𝑛))) = 0) |
| 73 | | nulmbl 25570 |
. . . . . . . . . 10
⊢ (((𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ ℝ ∧ (vol*‘(𝐴 ∩ (-𝑛[,]-𝑛))) = 0) → (𝐴 ∩ (-𝑛[,]-𝑛)) ∈ dom vol) |
| 74 | 68, 72, 73 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝐴 ∩ (-𝑛[,]-𝑛)) ∈ dom vol) |
| 75 | | mblvol 25565 |
. . . . . . . . 9
⊢ ((𝐴 ∩ (-𝑛[,]-𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]-𝑛))) = (vol*‘(𝐴 ∩ (-𝑛[,]-𝑛)))) |
| 76 | 74, 75 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (vol‘(𝐴 ∩ (-𝑛[,]-𝑛))) = (vol*‘(𝐴 ∩ (-𝑛[,]-𝑛)))) |
| 77 | 61, 76, 72 | 3eqtrd 2781 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) = 0) |
| 78 | 19 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 0 ≤ 𝐵) |
| 79 | 77, 78 | eqbrtrd 5165 |
. . . . . 6
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) ≤ 𝐵) |
| 80 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 ∈
ℝ*) |
| 81 | | iccmbl 25601 |
. . . . . . . . . . 11
⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ∈ dom vol) |
| 82 | 32, 31, 81 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (-𝑛[,]𝑛) ∈ dom vol) |
| 83 | | inmbl 25577 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧ (-𝑛[,]𝑛) ∈ dom vol) → (𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol) |
| 84 | 46, 82, 83 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol) |
| 85 | 9 | ffvelcdmi 7103 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈ (0[,]+∞)) |
| 86 | 8, 85 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈
ℝ*) |
| 87 | 84, 86 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈
ℝ*) |
| 88 | | simprr 773 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
| 89 | 80, 87, 88 | xrltled 13192 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 ≤ (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
| 90 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑛 → (-𝑛[,]𝑦) = (-𝑛[,]𝑛)) |
| 91 | 90 | ineq2d 4220 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑛 → (𝐴 ∩ (-𝑛[,]𝑦)) = (𝐴 ∩ (-𝑛[,]𝑛))) |
| 92 | 91 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑦 = 𝑛 → (vol‘(𝐴 ∩ (-𝑛[,]𝑦))) = (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
| 93 | | fvex 6919 |
. . . . . . . . 9
⊢
(vol‘(𝐴 ∩
(-𝑛[,]𝑛))) ∈ V |
| 94 | 92, 47, 93 | fvmpt 7016 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ → ((𝑦 ∈ ℝ ↦
(vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑛) = (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
| 95 | 31, 94 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑛) = (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
| 96 | 89, 95 | breqtrrd 5171 |
. . . . . 6
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 ≤ ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑛)) |
| 97 | 79, 96 | jca 511 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) ≤ 𝐵 ∧ 𝐵 ≤ ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑛))) |
| 98 | 32, 31, 33, 39, 41, 50, 55, 97 | ivthle 25491 |
. . . 4
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ∃𝑧 ∈ (-𝑛[,]𝑛)((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = 𝐵) |
| 99 | 41 | sselda 3983 |
. . . . . . . 8
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → 𝑧 ∈ ℝ) |
| 100 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (-𝑛[,]𝑦) = (-𝑛[,]𝑧)) |
| 101 | 100 | ineq2d 4220 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (𝐴 ∩ (-𝑛[,]𝑦)) = (𝐴 ∩ (-𝑛[,]𝑧))) |
| 102 | 101 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (vol‘(𝐴 ∩ (-𝑛[,]𝑦))) = (vol‘(𝐴 ∩ (-𝑛[,]𝑧)))) |
| 103 | | fvex 6919 |
. . . . . . . . 9
⊢
(vol‘(𝐴 ∩
(-𝑛[,]𝑧))) ∈ V |
| 104 | 102, 47, 103 | fvmpt 7016 |
. . . . . . . 8
⊢ (𝑧 ∈ ℝ → ((𝑦 ∈ ℝ ↦
(vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = (vol‘(𝐴 ∩ (-𝑛[,]𝑧)))) |
| 105 | 99, 104 | syl 17 |
. . . . . . 7
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = (vol‘(𝐴 ∩ (-𝑛[,]𝑧)))) |
| 106 | 105 | eqeq1d 2739 |
. . . . . 6
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → (((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = 𝐵 ↔ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) |
| 107 | 46 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → 𝐴 ∈ dom vol) |
| 108 | 32 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → -𝑛 ∈ ℝ) |
| 109 | 99 | adantrr 717 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → 𝑧 ∈ ℝ) |
| 110 | | iccmbl 25601 |
. . . . . . . . . 10
⊢ ((-𝑛 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-𝑛[,]𝑧) ∈ dom vol) |
| 111 | 108, 109,
110 | syl2anc 584 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → (-𝑛[,]𝑧) ∈ dom vol) |
| 112 | | inmbl 25577 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧ (-𝑛[,]𝑧) ∈ dom vol) → (𝐴 ∩ (-𝑛[,]𝑧)) ∈ dom vol) |
| 113 | 107, 111,
112 | syl2anc 584 |
. . . . . . . 8
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → (𝐴 ∩ (-𝑛[,]𝑧)) ∈ dom vol) |
| 114 | | inss1 4237 |
. . . . . . . . 9
⊢ (𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴 |
| 115 | 114 | a1i 11 |
. . . . . . . 8
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → (𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴) |
| 116 | | simprr 773 |
. . . . . . . 8
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵) |
| 117 | | sseq1 4009 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐴 ∩ (-𝑛[,]𝑧)) → (𝑥 ⊆ 𝐴 ↔ (𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴)) |
| 118 | | fveqeq2 6915 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐴 ∩ (-𝑛[,]𝑧)) → ((vol‘𝑥) = 𝐵 ↔ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) |
| 119 | 117, 118 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴 ∩ (-𝑛[,]𝑧)) → ((𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵) ↔ ((𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴 ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵))) |
| 120 | 119 | rspcev 3622 |
. . . . . . . 8
⊢ (((𝐴 ∩ (-𝑛[,]𝑧)) ∈ dom vol ∧ ((𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴 ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)) |
| 121 | 113, 115,
116, 120 | syl12anc 837 |
. . . . . . 7
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)) |
| 122 | 121 | expr 456 |
. . . . . 6
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → ((vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵 → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))) |
| 123 | 106, 122 | sylbid 240 |
. . . . 5
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → (((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = 𝐵 → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))) |
| 124 | 123 | rexlimdva 3155 |
. . . 4
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (∃𝑧 ∈ (-𝑛[,]𝑛)((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = 𝐵 → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))) |
| 125 | 98, 124 | mpd 15 |
. . 3
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)) |
| 126 | 29, 125 | rexlimddv 3161 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)) |
| 127 | | simpll 767 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐴 ∈ dom vol) |
| 128 | | ssid 4006 |
. . . 4
⊢ 𝐴 ⊆ 𝐴 |
| 129 | 128 | a1i 11 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐴 ⊆ 𝐴) |
| 130 | | simpr 484 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐵 = (vol‘𝐴)) |
| 131 | 130 | eqcomd 2743 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → (vol‘𝐴) = 𝐵) |
| 132 | | sseq1 4009 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
| 133 | | fveqeq2 6915 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((vol‘𝑥) = 𝐵 ↔ (vol‘𝐴) = 𝐵)) |
| 134 | 132, 133 | anbi12d 632 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵) ↔ (𝐴 ⊆ 𝐴 ∧ (vol‘𝐴) = 𝐵))) |
| 135 | 134 | rspcev 3622 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧ (𝐴 ⊆ 𝐴 ∧ (vol‘𝐴) = 𝐵)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)) |
| 136 | 127, 129,
131, 135 | syl12anc 837 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)) |
| 137 | 17 | simp3d 1145 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 𝐵 ≤ (vol‘𝐴)) |
| 138 | | xrleloe 13186 |
. . . 4
⊢ ((𝐵 ∈ ℝ*
∧ (vol‘𝐴) ∈
ℝ*) → (𝐵 ≤ (vol‘𝐴) ↔ (𝐵 < (vol‘𝐴) ∨ 𝐵 = (vol‘𝐴)))) |
| 139 | 6, 12, 138 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 ≤ (vol‘𝐴) ↔ (𝐵 < (vol‘𝐴) ∨ 𝐵 = (vol‘𝐴)))) |
| 140 | 137, 139 | mpbid 232 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 < (vol‘𝐴) ∨ 𝐵 = (vol‘𝐴))) |
| 141 | 126, 136,
140 | mpjaodan 961 |
1
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)) |