Step | Hyp | Ref
| Expression |
1 | | simpll 790 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → 𝐴 ∈
dom vol) |
2 | | simpr 477 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → (vol‘𝐴) ∈ ℝ) |
3 | | rpre 11839 |
. . . . . 6
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ∈
ℝ) |
4 | 3 | ad2antlr 763 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → 𝐵 ∈
ℝ) |
5 | | rpge0 11845 |
. . . . . 6
⊢ (𝐵 ∈ ℝ+
→ 0 ≤ 𝐵) |
6 | 5 | ad2antlr 763 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → 0 ≤ 𝐵) |
7 | | elrege0 12278 |
. . . . 5
⊢ (𝐵 ∈ (0[,)+∞) ↔
(𝐵 ∈ ℝ ∧ 0
≤ 𝐵)) |
8 | 4, 6, 7 | sylanbrc 698 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → 𝐵 ∈
(0[,)+∞)) |
9 | | itg2const 23507 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) = (𝐵 · (vol‘𝐴))) |
10 | 1, 2, 8, 9 | syl3anc 1326 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) = (𝐵 · (vol‘𝐴))) |
11 | 4, 2 | remulcld 10070 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → (𝐵 ·
(vol‘𝐴)) ∈
ℝ) |
12 | 10, 11 | eqeltrd 2701 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) |
13 | | mblvol 23298 |
. . . 4
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) =
(vol*‘𝐴)) |
14 | 13 | ad2antrr 762 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(vol‘𝐴) =
(vol*‘𝐴)) |
15 | | mblss 23299 |
. . . . . 6
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
16 | 15 | ad3antrrr 766 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(vol*‘𝐴) ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) → 𝐴 ⊆ ℝ) |
17 | | peano2re 10209 |
. . . . . . . 8
⊢
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ∈ ℝ) |
18 | 17 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ∈ ℝ) |
19 | | simplr 792 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → 𝐵 ∈
ℝ+) |
20 | 18, 19 | rerpdivcld 11903 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ) |
21 | 20 | adantr 481 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(vol*‘𝐴) ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) → (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ) |
22 | | simpr 477 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(vol*‘𝐴) ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) → (vol*‘𝐴) ≤ (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) |
23 | | ovollecl 23251 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ ∧ (vol*‘𝐴) ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) → (vol*‘𝐴) ∈ ℝ) |
24 | 16, 21, 22, 23 | syl3anc 1326 |
. . . 4
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(vol*‘𝐴) ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) → (vol*‘𝐴) ∈ ℝ) |
25 | | simplll 798 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → 𝐴 ∈ dom vol) |
26 | 20 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ) |
27 | 26 | rexrd 10089 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈
ℝ*) |
28 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0))) ∈ ℝ) |
29 | 3 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑥 ∈ ℝ)
→ 𝐵 ∈
ℝ) |
30 | 29 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑥 ∈ ℝ)
→ 𝐵 ∈
ℝ*) |
31 | 5 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑥 ∈ ℝ)
→ 0 ≤ 𝐵) |
32 | | elxrge0 12281 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ∈ (0[,]+∞) ↔
(𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵)) |
33 | 30, 31, 32 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑥 ∈ ℝ)
→ 𝐵 ∈
(0[,]+∞)) |
34 | | 0e0iccpnf 12283 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
(0[,]+∞) |
35 | | ifcl 4130 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ (0[,]+∞) ∧ 0
∈ (0[,]+∞)) → if(𝑥 ∈ 𝐴, 𝐵, 0) ∈ (0[,]+∞)) |
36 | 33, 34, 35 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑥 ∈ ℝ)
→ if(𝑥 ∈ 𝐴, 𝐵, 0) ∈ (0[,]+∞)) |
37 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) |
38 | 36, 37 | fmptd 6385 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐴, 𝐵,
0)):ℝ⟶(0[,]+∞)) |
39 | 38 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵,
0)):ℝ⟶(0[,]+∞)) |
40 | | itg2ge0 23502 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)):ℝ⟶(0[,]+∞) → 0
≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)))) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → 0 ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0)))) |
42 | 28, 41 | ge0p1rpd 11902 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ∈
ℝ+) |
43 | 42, 19 | rpdivcld 11889 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈
ℝ+) |
44 | 43 | rpge0d 11876 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → 0 ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) |
45 | 44 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → 0 ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) |
46 | 14 | breq2d 4665 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
((((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol‘𝐴) ↔ (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴))) |
47 | 46 | biimpar 502 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol‘𝐴)) |
48 | | 0xr 10086 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
49 | | iccssxr 12256 |
. . . . . . . . . . . 12
⊢
(0[,]+∞) ⊆ ℝ* |
50 | | volf 23297 |
. . . . . . . . . . . . 13
⊢ vol:dom
vol⟶(0[,]+∞) |
51 | 50 | ffvelrni 6358 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
(0[,]+∞)) |
52 | 49, 51 | sseldi 3601 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
ℝ*) |
53 | 25, 52 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → (vol‘𝐴) ∈
ℝ*) |
54 | | elicc1 12219 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ (vol‘𝐴) ∈ ℝ*) →
((((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ (0[,](vol‘𝐴)) ↔ ((((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ* ∧ 0 ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∧ (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol‘𝐴)))) |
55 | 48, 53, 54 | sylancr 695 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → ((((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ (0[,](vol‘𝐴)) ↔ ((((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ* ∧ 0 ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∧ (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol‘𝐴)))) |
56 | 27, 45, 47, 55 | mpbir3and 1245 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ (0[,](vol‘𝐴))) |
57 | | volivth 23375 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ (0[,](vol‘𝐴))) → ∃𝑧 ∈ dom vol(𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵))) |
58 | 25, 56, 57 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → ∃𝑧 ∈ dom vol(𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵))) |
59 | 58 | ex 450 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
((((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴) → ∃𝑧 ∈ dom vol(𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) |
60 | | simprl 794 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → 𝑧 ∈ dom vol) |
61 | | simprrr 805 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) |
62 | 20 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) →
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ) |
63 | 61, 62 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (vol‘𝑧) ∈ ℝ) |
64 | 3 | ad2antlr 763 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → 𝐵 ∈
ℝ) |
65 | 64 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → 𝐵 ∈ ℝ) |
66 | 19 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → 𝐵 ∈
ℝ+) |
67 | 66 | rpge0d 11876 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → 0 ≤ 𝐵) |
68 | 65, 67, 7 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → 𝐵 ∈ (0[,)+∞)) |
69 | | itg2const 23507 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ dom vol ∧
(vol‘𝑧) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0))) = (𝐵 · (vol‘𝑧))) |
70 | 60, 63, 68, 69 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0))) = (𝐵 · (vol‘𝑧))) |
71 | 61 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (𝐵 · (vol‘𝑧)) = (𝐵 · (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵))) |
72 | 18 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ∈ ℂ) |
73 | 64 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → 𝐵 ∈
ℂ) |
74 | | rpne0 11848 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ≠
0) |
75 | 74 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → 𝐵 ≠ 0) |
76 | 72, 73, 75 | divcan2d 10803 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → (𝐵 ·
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1)) |
77 | 76 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (𝐵 · (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1)) |
78 | 70, 71, 77 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0))) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1)) |
79 | 3 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ 𝐵 ∈
ℝ) |
80 | 79 | rexrd 10089 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ 𝐵 ∈
ℝ*) |
81 | 5 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ 0 ≤ 𝐵) |
82 | 80, 81, 32 | sylanbrc 698 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ 𝐵 ∈
(0[,]+∞)) |
83 | | ifcl 4130 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ (0[,]+∞) ∧ 0
∈ (0[,]+∞)) → if(𝑥 ∈ 𝑧, 𝐵, 0) ∈ (0[,]+∞)) |
84 | 82, 34, 83 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ if(𝑥 ∈ 𝑧, 𝐵, 0) ∈ (0[,]+∞)) |
85 | 84 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑥 ∈ ℝ)
→ if(𝑥 ∈ 𝑧, 𝐵, 0) ∈ (0[,]+∞)) |
86 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0)) |
87 | 85, 86 | fmptd 6385 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝑧, 𝐵,
0)):ℝ⟶(0[,]+∞)) |
88 | 87 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵,
0)):ℝ⟶(0[,]+∞)) |
89 | 39 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵,
0)):ℝ⟶(0[,]+∞)) |
90 | | simpl 473 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → (𝐴 ∈ dom vol ∧ 𝐵 ∈
ℝ+)) |
91 | | simprl 794 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵))) → 𝑧 ⊆ 𝐴) |
92 | 79 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑧) → 𝐵 ∈ ℝ) |
93 | 92 | leidd 10594 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑧) → 𝐵 ≤ 𝐵) |
94 | | iftrue 4092 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑧 → if(𝑥 ∈ 𝑧, 𝐵, 0) = 𝐵) |
95 | 94 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑧) → if(𝑥 ∈ 𝑧, 𝐵, 0) = 𝐵) |
96 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) → 𝑧 ⊆ 𝐴) |
97 | 96 | sselda 3603 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝐴) |
98 | 97 | iftrued 4094 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑧) → if(𝑥 ∈ 𝐴, 𝐵, 0) = 𝐵) |
99 | 93, 95, 98 | 3brtr4d 4685 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑧) → if(𝑥 ∈ 𝑧, 𝐵, 0) ≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) |
100 | | iffalse 4095 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 ∈ 𝑧 → if(𝑥 ∈ 𝑧, 𝐵, 0) = 0) |
101 | 100 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝑧) → if(𝑥 ∈ 𝑧, 𝐵, 0) = 0) |
102 | | 0le0 11110 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ≤
0 |
103 | | breq2 4657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 = if(𝑥 ∈ 𝐴, 𝐵, 0) → (0 ≤ 𝐵 ↔ 0 ≤ if(𝑥 ∈ 𝐴, 𝐵, 0))) |
104 | | breq2 4657 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 =
if(𝑥 ∈ 𝐴, 𝐵, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑥 ∈ 𝐴, 𝐵, 0))) |
105 | 103, 104 | ifboth 4124 |
. . . . . . . . . . . . . . . . 17
⊢ ((0 ≤
𝐵 ∧ 0 ≤ 0) → 0
≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) |
106 | 81, 102, 105 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ 0 ≤ if(𝑥 ∈
𝐴, 𝐵, 0)) |
107 | 106 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝑧) → 0 ≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) |
108 | 101, 107 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝑧) → if(𝑥 ∈ 𝑧, 𝐵, 0) ≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) |
109 | 99, 108 | pm2.61dan 832 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑧, 𝐵, 0) ≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) |
110 | 109 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑧 ⊆ 𝐴) → ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝑧, 𝐵, 0) ≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) |
111 | | reex 10027 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
112 | 111 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ ℝ ∈ V) |
113 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝑧, 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0))) |
114 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) |
115 | 112, 85, 36, 113, 114 | ofrfval2 6915 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ ((𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝑧, 𝐵, 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, 𝐵, 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝑧, 𝐵, 0) ≤ if(𝑥 ∈ 𝐴, 𝐵, 0))) |
116 | 115 | biimpar 502 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ ∀𝑥 ∈
ℝ if(𝑥 ∈ 𝑧, 𝐵, 0) ≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, 𝐵, 0))) |
117 | 110, 116 | syldan 487 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑧 ⊆ 𝐴) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, 𝐵, 0))) |
118 | 90, 91, 117 | syl2an 494 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, 𝐵, 0))) |
119 | | itg2le 23506 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0)):ℝ⟶(0[,]+∞) ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, 𝐵, 0)):ℝ⟶(0[,]+∞) ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝑧, 𝐵, 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, 𝐵, 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝑧, 𝐵, 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)))) |
120 | 88, 89, 118, 119 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)))) |
121 | 78, 120 | eqbrtrrd 4677 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0)))) |
122 | | ltp1 10861 |
. . . . . . . . . 10
⊢
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0))) < ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1)) |
123 | 122 | ad2antlr 763 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) < ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1)) |
124 | | simplr 792 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) |
125 | 17 | ad2antlr 763 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ∈ ℝ) |
126 | 124, 125 | ltnled 10184 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) < ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ↔ ¬
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0))))) |
127 | 123, 126 | mpbid 222 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → ¬
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0)))) |
128 | 121, 127 | pm2.21dd 186 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (vol*‘𝐴) ∈ ℝ) |
129 | 128 | rexlimdvaa 3032 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → (∃𝑧 ∈ dom vol(𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) → (vol*‘𝐴) ∈ ℝ)) |
130 | 59, 129 | syld 47 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
((((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴) → (vol*‘𝐴) ∈ ℝ)) |
131 | 130 | imp 445 |
. . . 4
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → (vol*‘𝐴) ∈ ℝ) |
132 | 52 | ad2antrr 762 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(vol‘𝐴) ∈
ℝ*) |
133 | 14, 132 | eqeltrrd 2702 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(vol*‘𝐴) ∈
ℝ*) |
134 | 20 | rexrd 10089 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈
ℝ*) |
135 | | xrletri 11984 |
. . . . 5
⊢
(((vol*‘𝐴)
∈ ℝ* ∧ (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ*) →
((vol*‘𝐴) ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∨ (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴))) |
136 | 133, 134,
135 | syl2anc 693 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
((vol*‘𝐴) ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∨ (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴))) |
137 | 24, 131, 136 | mpjaodan 827 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(vol*‘𝐴) ∈
ℝ) |
138 | 14, 137 | eqeltrd 2701 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(vol‘𝐴) ∈
ℝ) |
139 | 12, 138 | impbida 877 |
1
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ ((vol‘𝐴)
∈ ℝ ↔ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ)) |