Step | Hyp | Ref
| Expression |
1 | | itg2uba.2 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ dom
∫1) |
2 | | itg1cl 24849 |
. . . 4
⊢ (𝐺 ∈ dom ∫1
→ (∫1‘𝐺) ∈ ℝ) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 →
(∫1‘𝐺)
∈ ℝ) |
4 | 3 | rexrd 11025 |
. 2
⊢ (𝜑 →
(∫1‘𝐺)
∈ ℝ*) |
5 | | itg2uba.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
6 | | itg2uba.4 |
. . . . . . 7
⊢ (𝜑 → (vol*‘𝐴) = 0) |
7 | | nulmbl 24699 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) = 0) →
𝐴 ∈ dom
vol) |
8 | 5, 6, 7 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ dom vol) |
9 | | cmmbl 24698 |
. . . . . 6
⊢ (𝐴 ∈ dom vol → (ℝ
∖ 𝐴) ∈ dom
vol) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ (𝜑 → (ℝ ∖ 𝐴) ∈ dom
vol) |
11 | | ifnot 4511 |
. . . . . . . 8
⊢ if(¬
𝑥 ∈ 𝐴, (𝐺‘𝑥), 0) = if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)) |
12 | | eldif 3897 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ℝ ∖ 𝐴) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝐴)) |
13 | 12 | baibr 537 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → (¬
𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (ℝ ∖ 𝐴))) |
14 | 13 | ifbid 4482 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ → if(¬
𝑥 ∈ 𝐴, (𝐺‘𝑥), 0) = if(𝑥 ∈ (ℝ ∖ 𝐴), (𝐺‘𝑥), 0)) |
15 | 11, 14 | eqtr3id 2792 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)) = if(𝑥 ∈ (ℝ ∖ 𝐴), (𝐺‘𝑥), 0)) |
16 | 15 | mpteq2ia 5177 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ 𝐴), (𝐺‘𝑥), 0)) |
17 | 16 | i1fres 24870 |
. . . . 5
⊢ ((𝐺 ∈ dom ∫1
∧ (ℝ ∖ 𝐴)
∈ dom vol) → (𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 0, (𝐺‘𝑥))) ∈ dom
∫1) |
18 | 1, 10, 17 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥))) ∈ dom
∫1) |
19 | | itg1cl 24849 |
. . . 4
⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥))) ∈ dom ∫1 →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 0, (𝐺‘𝑥)))) ∈ ℝ) |
20 | 18, 19 | syl 17 |
. . 3
⊢ (𝜑 →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 0, (𝐺‘𝑥)))) ∈ ℝ) |
21 | 20 | rexrd 11025 |
. 2
⊢ (𝜑 →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 0, (𝐺‘𝑥)))) ∈
ℝ*) |
22 | | itg2uba.1 |
. . 3
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) |
23 | | itg2cl 24897 |
. . 3
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ (∫2‘𝐹) ∈
ℝ*) |
24 | 22, 23 | syl 17 |
. 2
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ*) |
25 | | i1ff 24840 |
. . . . . . 7
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
26 | 1, 25 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) |
27 | | eldifi 4061 |
. . . . . 6
⊢ (𝑦 ∈ (ℝ ∖ 𝐴) → 𝑦 ∈ ℝ) |
28 | | ffvelrn 6959 |
. . . . . 6
⊢ ((𝐺:ℝ⟶ℝ ∧
𝑦 ∈ ℝ) →
(𝐺‘𝑦) ∈ ℝ) |
29 | 26, 27, 28 | syl2an 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ℝ ∖ 𝐴)) → (𝐺‘𝑦) ∈ ℝ) |
30 | 29 | leidd 11541 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ℝ ∖ 𝐴)) → (𝐺‘𝑦) ≤ (𝐺‘𝑦)) |
31 | | eldif 3897 |
. . . . . 6
⊢ (𝑦 ∈ (ℝ ∖ 𝐴) ↔ (𝑦 ∈ ℝ ∧ ¬ 𝑦 ∈ 𝐴)) |
32 | | eleq1w 2821 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
33 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐺‘𝑥) = (𝐺‘𝑦)) |
34 | 32, 33 | ifbieq2d 4485 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)) = if(𝑦 ∈ 𝐴, 0, (𝐺‘𝑦))) |
35 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥))) |
36 | | c0ex 10969 |
. . . . . . . . 9
⊢ 0 ∈
V |
37 | | fvex 6787 |
. . . . . . . . 9
⊢ (𝐺‘𝑦) ∈ V |
38 | 36, 37 | ifex 4509 |
. . . . . . . 8
⊢ if(𝑦 ∈ 𝐴, 0, (𝐺‘𝑦)) ∈ V |
39 | 34, 35, 38 | fvmpt 6875 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)))‘𝑦) = if(𝑦 ∈ 𝐴, 0, (𝐺‘𝑦))) |
40 | | iffalse 4468 |
. . . . . . 7
⊢ (¬
𝑦 ∈ 𝐴 → if(𝑦 ∈ 𝐴, 0, (𝐺‘𝑦)) = (𝐺‘𝑦)) |
41 | 39, 40 | sylan9eq 2798 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ ∧ ¬
𝑦 ∈ 𝐴) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)))‘𝑦) = (𝐺‘𝑦)) |
42 | 31, 41 | sylbi 216 |
. . . . 5
⊢ (𝑦 ∈ (ℝ ∖ 𝐴) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)))‘𝑦) = (𝐺‘𝑦)) |
43 | 42 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ℝ ∖ 𝐴)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)))‘𝑦) = (𝐺‘𝑦)) |
44 | 30, 43 | breqtrrd 5102 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ℝ ∖ 𝐴)) → (𝐺‘𝑦) ≤ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)))‘𝑦)) |
45 | 1, 5, 6, 18, 44 | itg1lea 24877 |
. 2
⊢ (𝜑 →
(∫1‘𝐺)
≤ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥))))) |
46 | | iftrue 4465 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)) = 0) |
47 | 46 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)) = 0) |
48 | 22 | ffvelrnda 6961 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,]+∞)) |
49 | | elxrge0 13189 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ (0[,]+∞) ↔ ((𝐹‘𝑥) ∈ ℝ* ∧ 0 ≤
(𝐹‘𝑥))) |
50 | 48, 49 | sylib 217 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ* ∧ 0 ≤
(𝐹‘𝑥))) |
51 | 50 | simprd 496 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥)) |
52 | 51 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 0 ≤ (𝐹‘𝑥)) |
53 | 47, 52 | eqbrtrd 5096 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)) ≤ (𝐹‘𝑥)) |
54 | | iffalse 4468 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)) = (𝐺‘𝑥)) |
55 | 54 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)) = (𝐺‘𝑥)) |
56 | | itg2uba.5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐺‘𝑥) ≤ (𝐹‘𝑥)) |
57 | 12, 56 | sylan2br 595 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝐴)) → (𝐺‘𝑥) ≤ (𝐹‘𝑥)) |
58 | 57 | anassrs 468 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≤ (𝐹‘𝑥)) |
59 | 55, 58 | eqbrtrd 5096 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)) ≤ (𝐹‘𝑥)) |
60 | 53, 59 | pm2.61dan 810 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)) ≤ (𝐹‘𝑥)) |
61 | 60 | ralrimiva 3103 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)) ≤ (𝐹‘𝑥)) |
62 | | reex 10962 |
. . . . . 6
⊢ ℝ
∈ V |
63 | 62 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈
V) |
64 | | fvex 6787 |
. . . . . . 7
⊢ (𝐺‘𝑥) ∈ V |
65 | 36, 64 | ifex 4509 |
. . . . . 6
⊢ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)) ∈ V |
66 | 65 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)) ∈ V) |
67 | | fvexd 6789 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ V) |
68 | | eqidd 2739 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)))) |
69 | 22 | feqmptd 6837 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
70 | 63, 66, 67, 68, 69 | ofrfval2 7554 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥))) ∘r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥)) ≤ (𝐹‘𝑥))) |
71 | 61, 70 | mpbird 256 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥))) ∘r ≤ 𝐹) |
72 | | itg2ub 24898 |
. . 3
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥))) ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 0, (𝐺‘𝑥))) ∘r ≤ 𝐹) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 0, (𝐺‘𝑥)))) ≤ (∫2‘𝐹)) |
73 | 22, 18, 71, 72 | syl3anc 1370 |
. 2
⊢ (𝜑 →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 0, (𝐺‘𝑥)))) ≤ (∫2‘𝐹)) |
74 | 4, 21, 24, 45, 73 | xrletrd 12896 |
1
⊢ (𝜑 →
(∫1‘𝐺)
≤ (∫2‘𝐹)) |