| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpll 766 | . . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → 𝐴 ∈
dom vol) | 
| 2 |  | simpr 484 | . . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → (vol‘𝐴) ∈ ℝ) | 
| 3 |  | rpre 13044 | . . . . . 6
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ∈
ℝ) | 
| 4 | 3 | ad2antlr 727 | . . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → 𝐵 ∈
ℝ) | 
| 5 |  | rpge0 13049 | . . . . . 6
⊢ (𝐵 ∈ ℝ+
→ 0 ≤ 𝐵) | 
| 6 | 5 | ad2antlr 727 | . . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → 0 ≤ 𝐵) | 
| 7 |  | elrege0 13495 | . . . . 5
⊢ (𝐵 ∈ (0[,)+∞) ↔
(𝐵 ∈ ℝ ∧ 0
≤ 𝐵)) | 
| 8 | 4, 6, 7 | sylanbrc 583 | . . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → 𝐵 ∈
(0[,)+∞)) | 
| 9 |  | itg2const 25776 | . . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) = (𝐵 · (vol‘𝐴))) | 
| 10 | 1, 2, 8, 9 | syl3anc 1372 | . . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) = (𝐵 · (vol‘𝐴))) | 
| 11 | 4, 2 | remulcld 11292 | . . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → (𝐵 ·
(vol‘𝐴)) ∈
ℝ) | 
| 12 | 10, 11 | eqeltrd 2840 | . 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (vol‘𝐴) ∈
ℝ) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) | 
| 13 |  | mblvol 25566 | . . . 4
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) =
(vol*‘𝐴)) | 
| 14 | 13 | ad2antrr 726 | . . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(vol‘𝐴) =
(vol*‘𝐴)) | 
| 15 |  | mblss 25567 | . . . . . 6
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) | 
| 16 | 15 | ad3antrrr 730 | . . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(vol*‘𝐴) ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) → 𝐴 ⊆ ℝ) | 
| 17 |  | peano2re 11435 | . . . . . . . 8
⊢
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ∈ ℝ) | 
| 18 | 17 | adantl 481 | . . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ∈ ℝ) | 
| 19 |  | simplr 768 | . . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → 𝐵 ∈
ℝ+) | 
| 20 | 18, 19 | rerpdivcld 13109 | . . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ) | 
| 21 | 20 | adantr 480 | . . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(vol*‘𝐴) ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) → (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ) | 
| 22 |  | simpr 484 | . . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(vol*‘𝐴) ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) → (vol*‘𝐴) ≤ (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) | 
| 23 |  | ovollecl 25519 | . . . . 5
⊢ ((𝐴 ⊆ ℝ ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ ∧ (vol*‘𝐴) ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) → (vol*‘𝐴) ∈ ℝ) | 
| 24 | 16, 21, 22, 23 | syl3anc 1372 | . . . 4
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(vol*‘𝐴) ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) → (vol*‘𝐴) ∈ ℝ) | 
| 25 |  | simplll 774 | . . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → 𝐴 ∈ dom vol) | 
| 26 | 20 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ) | 
| 27 | 26 | rexrd 11312 | . . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈
ℝ*) | 
| 28 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0))) ∈ ℝ) | 
| 29 | 3 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑥 ∈ ℝ)
→ 𝐵 ∈
ℝ) | 
| 30 | 29 | rexrd 11312 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑥 ∈ ℝ)
→ 𝐵 ∈
ℝ*) | 
| 31 | 5 | ad2antlr 727 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑥 ∈ ℝ)
→ 0 ≤ 𝐵) | 
| 32 |  | elxrge0 13498 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ∈ (0[,]+∞) ↔
(𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵)) | 
| 33 | 30, 31, 32 | sylanbrc 583 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑥 ∈ ℝ)
→ 𝐵 ∈
(0[,]+∞)) | 
| 34 |  | 0e0iccpnf 13500 | . . . . . . . . . . . . . . . . 17
⊢ 0 ∈
(0[,]+∞) | 
| 35 |  | ifcl 4570 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ (0[,]+∞) ∧ 0
∈ (0[,]+∞)) → if(𝑥 ∈ 𝐴, 𝐵, 0) ∈ (0[,]+∞)) | 
| 36 | 33, 34, 35 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑥 ∈ ℝ)
→ if(𝑥 ∈ 𝐴, 𝐵, 0) ∈ (0[,]+∞)) | 
| 37 | 36 | fmpttd 7134 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐴, 𝐵,
0)):ℝ⟶(0[,]+∞)) | 
| 38 | 37 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵,
0)):ℝ⟶(0[,]+∞)) | 
| 39 |  | itg2ge0 25771 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)):ℝ⟶(0[,]+∞) → 0
≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)))) | 
| 40 | 38, 39 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → 0 ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0)))) | 
| 41 | 28, 40 | ge0p1rpd 13108 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ∈
ℝ+) | 
| 42 | 41, 19 | rpdivcld 13095 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈
ℝ+) | 
| 43 | 42 | rpge0d 13082 | . . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → 0 ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) | 
| 44 | 43 | adantr 480 | . . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → 0 ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) | 
| 45 | 14 | breq2d 5154 | . . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
((((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol‘𝐴) ↔ (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴))) | 
| 46 | 45 | biimpar 477 | . . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol‘𝐴)) | 
| 47 |  | 0xr 11309 | . . . . . . . . . 10
⊢ 0 ∈
ℝ* | 
| 48 |  | iccssxr 13471 | . . . . . . . . . . . 12
⊢
(0[,]+∞) ⊆ ℝ* | 
| 49 |  | volf 25565 | . . . . . . . . . . . . 13
⊢ vol:dom
vol⟶(0[,]+∞) | 
| 50 | 49 | ffvelcdmi 7102 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
(0[,]+∞)) | 
| 51 | 48, 50 | sselid 3980 | . . . . . . . . . . 11
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
ℝ*) | 
| 52 | 25, 51 | syl 17 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → (vol‘𝐴) ∈
ℝ*) | 
| 53 |  | elicc1 13432 | . . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ (vol‘𝐴) ∈ ℝ*) →
((((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ (0[,](vol‘𝐴)) ↔ ((((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ* ∧ 0 ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∧ (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol‘𝐴)))) | 
| 54 | 47, 52, 53 | sylancr 587 | . . . . . . . . 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‘𝐴)))) | 
| 55 | 27, 44, 46, 54 | mpbir3and 1342 | . . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ (0[,](vol‘𝐴))) | 
| 56 |  | volivth 25643 | . . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ (0[,](vol‘𝐴))) → ∃𝑧 ∈ dom vol(𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵))) | 
| 57 | 25, 55, 56 | syl2anc 584 | . . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → ∃𝑧 ∈ dom vol(𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵))) | 
| 58 | 57 | ex 412 | . . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
((((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴) → ∃𝑧 ∈ dom vol(𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) | 
| 59 |  | simprl 770 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → 𝑧 ∈ dom vol) | 
| 60 |  | simprrr 781 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) | 
| 61 | 20 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) →
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ) | 
| 62 | 60, 61 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (vol‘𝑧) ∈ ℝ) | 
| 63 | 3 | ad2antlr 727 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → 𝐵 ∈
ℝ) | 
| 64 | 63 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → 𝐵 ∈ ℝ) | 
| 65 | 19 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → 𝐵 ∈
ℝ+) | 
| 66 | 65 | rpge0d 13082 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → 0 ≤ 𝐵) | 
| 67 | 64, 66, 7 | sylanbrc 583 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → 𝐵 ∈ (0[,)+∞)) | 
| 68 |  | itg2const 25776 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ dom vol ∧
(vol‘𝑧) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0))) = (𝐵 · (vol‘𝑧))) | 
| 69 | 59, 62, 67, 68 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0))) = (𝐵 · (vol‘𝑧))) | 
| 70 | 60 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (𝐵 · (vol‘𝑧)) = (𝐵 · (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵))) | 
| 71 | 18 | recnd 11290 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ∈ ℂ) | 
| 72 | 63 | recnd 11290 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → 𝐵 ∈
ℂ) | 
| 73 |  | rpne0 13052 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ≠
0) | 
| 74 | 73 | ad2antlr 727 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → 𝐵 ≠ 0) | 
| 75 | 71, 72, 74 | divcan2d 12046 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → (𝐵 ·
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1)) | 
| 76 | 75 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (𝐵 · (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1)) | 
| 77 | 69, 70, 76 | 3eqtrd 2780 | . . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0))) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1)) | 
| 78 | 3 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ 𝐵 ∈
ℝ) | 
| 79 | 78 | rexrd 11312 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ 𝐵 ∈
ℝ*) | 
| 80 | 5 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ 0 ≤ 𝐵) | 
| 81 | 79, 80, 32 | sylanbrc 583 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ 𝐵 ∈
(0[,]+∞)) | 
| 82 |  | ifcl 4570 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ (0[,]+∞) ∧ 0
∈ (0[,]+∞)) → if(𝑥 ∈ 𝑧, 𝐵, 0) ∈ (0[,]+∞)) | 
| 83 | 81, 34, 82 | sylancl 586 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ if(𝑥 ∈ 𝑧, 𝐵, 0) ∈ (0[,]+∞)) | 
| 84 | 83 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑥 ∈ ℝ)
→ if(𝑥 ∈ 𝑧, 𝐵, 0) ∈ (0[,]+∞)) | 
| 85 | 84 | fmpttd 7134 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝑧, 𝐵,
0)):ℝ⟶(0[,]+∞)) | 
| 86 | 85 | ad2antrr 726 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵,
0)):ℝ⟶(0[,]+∞)) | 
| 87 | 38 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵,
0)):ℝ⟶(0[,]+∞)) | 
| 88 |  | simpl 482 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → (𝐴 ∈ dom vol ∧ 𝐵 ∈
ℝ+)) | 
| 89 |  | simprl 770 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵))) → 𝑧 ⊆ 𝐴) | 
| 90 | 78 | ad3antrrr 730 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑧) → 𝐵 ∈ ℝ) | 
| 91 | 90 | leidd 11830 | . . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑧) → 𝐵 ≤ 𝐵) | 
| 92 |  | iftrue 4530 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑧 → if(𝑥 ∈ 𝑧, 𝐵, 0) = 𝐵) | 
| 93 | 92 | adantl 481 | . . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑧) → if(𝑥 ∈ 𝑧, 𝐵, 0) = 𝐵) | 
| 94 |  | simplr 768 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) → 𝑧 ⊆ 𝐴) | 
| 95 | 94 | sselda 3982 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝐴) | 
| 96 | 95 | iftrued 4532 | . . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑧) → if(𝑥 ∈ 𝐴, 𝐵, 0) = 𝐵) | 
| 97 | 91, 93, 96 | 3brtr4d 5174 | . . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑧) → if(𝑥 ∈ 𝑧, 𝐵, 0) ≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) | 
| 98 |  | iffalse 4533 | . . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 ∈ 𝑧 → if(𝑥 ∈ 𝑧, 𝐵, 0) = 0) | 
| 99 | 98 | adantl 481 | . . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝑧) → if(𝑥 ∈ 𝑧, 𝐵, 0) = 0) | 
| 100 |  | 0le0 12368 | . . . . . . . . . . . . . . . . 17
⊢ 0 ≤
0 | 
| 101 |  | breq2 5146 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐵 = if(𝑥 ∈ 𝐴, 𝐵, 0) → (0 ≤ 𝐵 ↔ 0 ≤ if(𝑥 ∈ 𝐴, 𝐵, 0))) | 
| 102 |  | breq2 5146 | . . . . . . . . . . . . . . . . . 18
⊢ (0 =
if(𝑥 ∈ 𝐴, 𝐵, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑥 ∈ 𝐴, 𝐵, 0))) | 
| 103 | 101, 102 | ifboth 4564 | . . . . . . . . . . . . . . . . 17
⊢ ((0 ≤
𝐵 ∧ 0 ≤ 0) → 0
≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) | 
| 104 | 80, 100, 103 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ 0 ≤ if(𝑥 ∈
𝐴, 𝐵, 0)) | 
| 105 | 104 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝑧) → 0 ≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) | 
| 106 | 99, 105 | eqbrtrd 5164 | . . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
ℝ+) ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝑧) → if(𝑥 ∈ 𝑧, 𝐵, 0) ≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) | 
| 107 | 97, 106 | pm2.61dan 812 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑧, 𝐵, 0) ≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) | 
| 108 | 107 | ralrimiva 3145 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑧 ⊆ 𝐴) → ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝑧, 𝐵, 0) ≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) | 
| 109 |  | reex 11247 | . . . . . . . . . . . . . . 15
⊢ ℝ
∈ V | 
| 110 | 109 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ ℝ ∈ V) | 
| 111 |  | eqidd 2737 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝑧, 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0))) | 
| 112 |  | eqidd 2737 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) | 
| 113 | 110, 84, 36, 111, 112 | ofrfval2 7719 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ ((𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝑧, 𝐵, 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝑧, 𝐵, 0) ≤ if(𝑥 ∈ 𝐴, 𝐵, 0))) | 
| 114 | 113 | biimpar 477 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ ∀𝑥 ∈
ℝ if(𝑥 ∈ 𝑧, 𝐵, 0) ≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) | 
| 115 | 108, 114 | syldan 591 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ 𝑧 ⊆ 𝐴) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) | 
| 116 | 88, 89, 115 | syl2an 596 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) | 
| 117 |  | itg2le 25775 | . . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0)):ℝ⟶(0[,]+∞) ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, 𝐵, 0)):ℝ⟶(0[,]+∞) ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝑧, 𝐵, 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝑧, 𝐵, 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)))) | 
| 118 | 86, 87, 116, 117 | syl3anc 1372 | . . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑧, 𝐵, 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)))) | 
| 119 | 77, 118 | eqbrtrrd 5166 | . . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0)))) | 
| 120 |  | ltp1 12108 | . . . . . . . . . 10
⊢
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0))) < ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1)) | 
| 121 | 120 | ad2antlr 727 | . . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) < ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1)) | 
| 122 |  | simplr 768 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) | 
| 123 | 17 | ad2antlr 727 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ∈ ℝ) | 
| 124 | 122, 123 | ltnled 11409 | . . . . . . . . 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))))) | 
| 125 | 121, 124 | mpbid 232 | . . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → ¬
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0)))) | 
| 126 | 119, 125 | pm2.21dd 195 | . . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧ (𝑧 ∈ dom vol ∧ (𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)))) → (vol*‘𝐴) ∈ ℝ) | 
| 127 | 126 | rexlimdvaa 3155 | . . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) → (∃𝑧 ∈ dom vol(𝑧 ⊆ 𝐴 ∧ (vol‘𝑧) = (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵)) → (vol*‘𝐴) ∈ ℝ)) | 
| 128 | 58, 127 | syld 47 | . . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
((((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴) → (vol*‘𝐴) ∈ ℝ)) | 
| 129 | 128 | imp 406 | . . . 4
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) ∧
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴)) → (vol*‘𝐴) ∈ ℝ) | 
| 130 | 51 | ad2antrr 726 | . . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(vol‘𝐴) ∈
ℝ*) | 
| 131 | 14, 130 | eqeltrrd 2841 | . . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(vol*‘𝐴) ∈
ℝ*) | 
| 132 | 20 | rexrd 11312 | . . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈
ℝ*) | 
| 133 |  | xrletri 13196 | . . . . 5
⊢
(((vol*‘𝐴)
∈ ℝ* ∧ (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∈ ℝ*) →
((vol*‘𝐴) ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∨ (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴))) | 
| 134 | 131, 132,
133 | syl2anc 584 | . . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
((vol*‘𝐴) ≤
(((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ∨ (((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + 1) / 𝐵) ≤ (vol*‘𝐴))) | 
| 135 | 24, 129, 134 | mpjaodan 960 | . . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(vol*‘𝐴) ∈
ℝ) | 
| 136 | 14, 135 | eqeltrd 2840 | . 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ) →
(vol‘𝐴) ∈
ℝ) | 
| 137 | 12, 136 | impbida 800 | 1
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+)
→ ((vol‘𝐴)
∈ ℝ ↔ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ)) |