Step | Hyp | Ref
| Expression |
1 | | simprl 794 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → 𝑓 ∈ dom
∫1) |
2 | | itg1cl 23452 |
. . . . . 6
⊢ (𝑓 ∈ dom ∫1
→ (∫1‘𝑓) ∈ ℝ) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
(∫1‘𝑓)
∈ ℝ) |
4 | | itg2split.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ dom vol) |
5 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → 𝐴 ∈ dom
vol) |
6 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) |
7 | 6 | i1fres 23472 |
. . . . . . . 8
⊢ ((𝑓 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∈ dom
∫1) |
8 | 1, 5, 7 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∈ dom
∫1) |
9 | | itg1cl 23452 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∈ dom ∫1 →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (𝑓‘𝑥), 0))) ∈ ℝ) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (𝑓‘𝑥), 0))) ∈ ℝ) |
11 | | itg2split.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ dom vol) |
12 | 11 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → 𝐵 ∈ dom
vol) |
13 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) |
14 | 13 | i1fres 23472 |
. . . . . . . 8
⊢ ((𝑓 ∈ dom ∫1
∧ 𝐵 ∈ dom vol)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∈ dom
∫1) |
15 | 1, 12, 14 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∈ dom
∫1) |
16 | | itg1cl 23452 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∈ dom ∫1 →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, (𝑓‘𝑥), 0))) ∈ ℝ) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, (𝑓‘𝑥), 0))) ∈ ℝ) |
18 | 10, 17 | readdcld 10069 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))) ∈ ℝ) |
19 | | itg2split.sf |
. . . . . . 7
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ) |
20 | | itg2split.sg |
. . . . . . 7
⊢ (𝜑 →
(∫2‘𝐺)
∈ ℝ) |
21 | 19, 20 | readdcld 10069 |
. . . . . 6
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ∈
ℝ) |
22 | 21 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
((∫2‘𝐹) + (∫2‘𝐺)) ∈
ℝ) |
23 | | inss1 3833 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
24 | | mblss 23299 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
25 | 4, 24 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
26 | 23, 25 | syl5ss 3614 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ ℝ) |
27 | 26 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → (𝐴 ∩ 𝐵) ⊆ ℝ) |
28 | | itg2split.i |
. . . . . . . 8
⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0) |
29 | 28 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
(vol*‘(𝐴 ∩ 𝐵)) = 0) |
30 | | reex 10027 |
. . . . . . . . . . 11
⊢ ℝ
∈ V |
31 | 30 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ∈
V) |
32 | | fvex 6201 |
. . . . . . . . . . . 12
⊢ (𝑓‘𝑥) ∈ V |
33 | | c0ex 10034 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
34 | 32, 33 | ifex 4156 |
. . . . . . . . . . 11
⊢ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ∈ V |
35 | 34 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ∈ V) |
36 | 32, 33 | ifex 4156 |
. . . . . . . . . . 11
⊢ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ∈ V |
37 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ∈ V) |
38 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0))) |
39 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))) |
40 | 31, 35, 37, 38, 39 | offval2 6914 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))) |
41 | 40 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))) |
42 | 8, 15 | i1fadd 23462 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))) ∈ dom
∫1) |
43 | 41, 42 | eqeltrrd 2702 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → (𝑥 ∈ ℝ ↦
(if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))) ∈ dom
∫1) |
44 | | i1ff 23443 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ dom ∫1
→ 𝑓:ℝ⟶ℝ) |
45 | 1, 44 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → 𝑓:ℝ⟶ℝ) |
46 | | eldifi 3732 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → 𝑦 ∈ ℝ) |
47 | | ffvelrn 6357 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℝ⟶ℝ ∧
𝑦 ∈ ℝ) →
(𝑓‘𝑦) ∈ ℝ) |
48 | 45, 46, 47 | syl2an 494 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑦) ∈ ℝ) |
49 | 48 | leidd 10594 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑦) ≤ (𝑓‘𝑦)) |
50 | 49 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → (𝑓‘𝑦) ≤ (𝑓‘𝑦)) |
51 | | iftrue 4092 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐴 → if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) = (𝑓‘𝑦)) |
52 | 51 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) = (𝑓‘𝑦)) |
53 | | eldifn 3733 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → ¬ 𝑦 ∈ (𝐴 ∩ 𝐵)) |
54 | 53 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ¬ 𝑦 ∈ (𝐴 ∩ 𝐵)) |
55 | | elin 3796 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
56 | 54, 55 | sylnib 318 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ¬ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
57 | | imnan 438 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝐴 → ¬ 𝑦 ∈ 𝐵) ↔ ¬ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
58 | 56, 57 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑦 ∈ 𝐴 → ¬ 𝑦 ∈ 𝐵)) |
59 | 58 | imp 445 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → ¬ 𝑦 ∈ 𝐵) |
60 | | iffalse 4095 |
. . . . . . . . . . . . 13
⊢ (¬
𝑦 ∈ 𝐵 → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) = 0) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) = 0) |
62 | 52, 61 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) = ((𝑓‘𝑦) + 0)) |
63 | 48 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑦) ∈ ℂ) |
64 | 63 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → (𝑓‘𝑦) ∈ ℂ) |
65 | 64 | addid1d 10236 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → ((𝑓‘𝑦) + 0) = (𝑓‘𝑦)) |
66 | 62, 65 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) = (𝑓‘𝑦)) |
67 | 50, 66 | breqtrrd 4681 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → (𝑓‘𝑦) ≤ (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0))) |
68 | 49 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑓
∘𝑟 ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑓‘𝑦) ≤ (𝑓‘𝑦)) |
69 | | iftrue 4092 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐵 → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) = (𝑓‘𝑦)) |
70 | 69 | adantl 482 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑓
∘𝑟 ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) = (𝑓‘𝑦)) |
71 | 68, 70 | breqtrrd 4681 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑓
∘𝑟 ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑓‘𝑦) ≤ if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) |
72 | | itg2split.u |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) |
73 | 72 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → 𝑈 = (𝐴 ∪ 𝐵)) |
74 | 73 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑦 ∈ 𝑈 ↔ 𝑦 ∈ (𝐴 ∪ 𝐵))) |
75 | | elun 3753 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (𝐴 ∪ 𝐵) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)) |
76 | 74, 75 | syl6bb 276 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑦 ∈ 𝑈 ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))) |
77 | 76 | notbid 308 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (¬ 𝑦 ∈ 𝑈 ↔ ¬ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))) |
78 | | ioran 511 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵) ↔ (¬ 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)) |
79 | 77, 78 | syl6bb 276 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (¬ 𝑦 ∈ 𝑈 ↔ (¬ 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))) |
80 | 79 | biimpar 502 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ (¬ 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)) → ¬ 𝑦 ∈ 𝑈) |
81 | | simprr 796 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → 𝑓 ∘𝑟
≤ 𝐻) |
82 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:ℝ⟶ℝ →
𝑓 Fn
ℝ) |
83 | 45, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → 𝑓 Fn ℝ) |
84 | | itg2split.c |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞)) |
85 | 84 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞)) |
86 | | 0e0iccpnf 12283 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
(0[,]+∞) |
87 | 86 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝑈) → 0 ∈
(0[,]+∞)) |
88 | 85, 87 | ifclda 4120 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞)) |
89 | | itg2split.h |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
90 | 88, 89 | fmptd 6385 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐻:ℝ⟶(0[,]+∞)) |
91 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐻:ℝ⟶(0[,]+∞)
→ 𝐻 Fn
ℝ) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐻 Fn ℝ) |
93 | 92 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → 𝐻 Fn ℝ) |
94 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → ℝ
∈ V) |
95 | | inidm 3822 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℝ
∩ ℝ) = ℝ |
96 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ ℝ) → (𝑓‘𝑦) = (𝑓‘𝑦)) |
97 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ ℝ) → (𝐻‘𝑦) = (𝐻‘𝑦)) |
98 | 83, 93, 94, 94, 95, 96, 97 | ofrfval 6905 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → (𝑓 ∘𝑟
≤ 𝐻 ↔ ∀𝑦 ∈ ℝ (𝑓‘𝑦) ≤ (𝐻‘𝑦))) |
99 | 81, 98 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
∀𝑦 ∈ ℝ
(𝑓‘𝑦) ≤ (𝐻‘𝑦)) |
100 | 99 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ ℝ) → (𝑓‘𝑦) ≤ (𝐻‘𝑦)) |
101 | 46, 100 | sylan2 491 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑦) ≤ (𝐻‘𝑦)) |
102 | 101 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝑈) → (𝑓‘𝑦) ≤ (𝐻‘𝑦)) |
103 | 46 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → 𝑦 ∈ ℝ) |
104 | | eldif 3584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (ℝ ∖ 𝑈) ↔ (𝑦 ∈ ℝ ∧ ¬ 𝑦 ∈ 𝑈)) |
105 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥𝑦 |
106 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
107 | 89, 106 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥𝐻 |
108 | 107, 105 | nffv 6198 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝐻‘𝑦) |
109 | 108 | nfeq1 2778 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥(𝐻‘𝑦) = 0 |
110 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦)) |
111 | 110 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝐻‘𝑥) = 0 ↔ (𝐻‘𝑦) = 0)) |
112 | | eldif 3584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (ℝ ∖ 𝑈) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝑈)) |
113 | 89 | fvmpt2i 6290 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ → (𝐻‘𝑥) = ( I ‘if(𝑥 ∈ 𝑈, 𝐶, 0))) |
114 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑥 ∈ 𝑈 → if(𝑥 ∈ 𝑈, 𝐶, 0) = 0) |
115 | 114 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑥 ∈ 𝑈 → ( I ‘if(𝑥 ∈ 𝑈, 𝐶, 0)) = ( I ‘0)) |
116 | | 0cn 10032 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℂ |
117 | | fvi 6255 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ∈
ℂ → ( I ‘0) = 0) |
118 | 116, 117 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( I
‘0) = 0 |
119 | 115, 118 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑥 ∈ 𝑈 → ( I ‘if(𝑥 ∈ 𝑈, 𝐶, 0)) = 0) |
120 | 113, 119 | sylan9eq 2676 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ ¬
𝑥 ∈ 𝑈) → (𝐻‘𝑥) = 0) |
121 | 112, 120 | sylbi 207 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (ℝ ∖ 𝑈) → (𝐻‘𝑥) = 0) |
122 | 105, 109,
111, 121 | vtoclgaf 3271 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (ℝ ∖ 𝑈) → (𝐻‘𝑦) = 0) |
123 | 104, 122 | sylbir 225 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ ∧ ¬
𝑦 ∈ 𝑈) → (𝐻‘𝑦) = 0) |
124 | 103, 123 | sylan 488 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝑈) → (𝐻‘𝑦) = 0) |
125 | 102, 124 | breqtrd 4679 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝑈) → (𝑓‘𝑦) ≤ 0) |
126 | 80, 125 | syldan 487 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ (¬ 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)) → (𝑓‘𝑦) ≤ 0) |
127 | 126 | anassrs 680 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑓
∘𝑟 ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ∈ 𝐵) → (𝑓‘𝑦) ≤ 0) |
128 | 60 | adantl 482 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑓
∘𝑟 ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ∈ 𝐵) → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) = 0) |
129 | 127, 128 | breqtrrd 4681 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑓
∘𝑟 ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ∈ 𝐵) → (𝑓‘𝑦) ≤ if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) |
130 | 71, 129 | pm2.61dan 832 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) → (𝑓‘𝑦) ≤ if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) |
131 | | iffalse 4095 |
. . . . . . . . . . . . 13
⊢ (¬
𝑦 ∈ 𝐴 → if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) = 0) |
132 | 131 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) → if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) = 0) |
133 | 132 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) → (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) = (0 + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0))) |
134 | | 0re 10040 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
135 | | ifcl 4130 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) ∈ ℝ) |
136 | 48, 134, 135 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) ∈ ℝ) |
137 | 136 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) ∈ ℂ) |
138 | 137 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) ∈ ℂ) |
139 | 138 | addid2d 10237 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) → (0 + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) = if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) |
140 | 133, 139 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) → (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) = if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) |
141 | 130, 140 | breqtrrd 4681 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) → (𝑓‘𝑦) ≤ (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0))) |
142 | 67, 141 | pm2.61dan 832 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑦) ≤ (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0))) |
143 | | eleq1 2689 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
144 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑓‘𝑥) = (𝑓‘𝑦)) |
145 | 143, 144 | ifbieq1d 4109 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) = if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0)) |
146 | | eleq1 2689 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
147 | 146, 144 | ifbieq1d 4109 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) = if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) |
148 | 145, 147 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) = (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0))) |
149 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ ↦
(if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))) |
150 | | ovex 6678 |
. . . . . . . . . 10
⊢ (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) ∈ V |
151 | 148, 149,
150 | fvmpt 6282 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → ((𝑥 ∈ ℝ ↦
(if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))‘𝑦) = (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0))) |
152 | 103, 151 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))‘𝑦) = (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0))) |
153 | 142, 152 | breqtrrd 4681 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑦) ≤ ((𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))‘𝑦)) |
154 | 1, 27, 29, 43, 153 | itg1lea 23479 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
(∫1‘𝑓)
≤ (∫1‘(𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))))) |
155 | 41 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
(∫1‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))) = (∫1‘(𝑥 ∈ ℝ ↦
(if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))))) |
156 | 8, 15 | itg1add 23468 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
(∫1‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))) = ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))))) |
157 | 155, 156 | eqtr3d 2658 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
(∫1‘(𝑥
∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))) = ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))))) |
158 | 154, 157 | breqtrd 4679 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
(∫1‘𝑓)
≤ ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))))) |
159 | 19 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
(∫2‘𝐹)
∈ ℝ) |
160 | 20 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
(∫2‘𝐺)
∈ ℝ) |
161 | | ssun1 3776 |
. . . . . . . . . . . . . 14
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
162 | 161, 72 | syl5sseqr 3654 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆ 𝑈) |
163 | 162 | sselda 3603 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) |
164 | 163 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) |
165 | 164, 85 | syldan 487 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) |
166 | 86 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) |
167 | 165, 166 | ifclda 4120 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,]+∞)) |
168 | | itg2split.f |
. . . . . . . . 9
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
169 | 167, 168 | fmptd 6385 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) |
170 | 169 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → 𝐹:ℝ⟶(0[,]+∞)) |
171 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝜑 |
172 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑓 ∈ dom
∫1 |
173 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑓 |
174 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥
∘𝑟 ≤ |
175 | 173, 174,
107 | nfbr 4699 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑓 ∘𝑟
≤ 𝐻 |
176 | 172, 175 | nfan 1828 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑓 ∈ dom ∫1
∧ 𝑓
∘𝑟 ≤ 𝐻) |
177 | 171, 176 | nfan 1828 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) |
178 | 5, 24 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → 𝐴 ⊆
ℝ) |
179 | 178 | sselda 3603 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
180 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ℝ
∈ V) |
181 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) ∈ V) |
182 | 88 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞)) |
183 | 44 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝑓:ℝ⟶ℝ) |
184 | 183 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓‘𝑥))) |
185 | 89 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0))) |
186 | 180, 181,
182, 184, 185 | ofrfval2 6915 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑓 ∘𝑟
≤ 𝐻 ↔ ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝑈, 𝐶, 0))) |
187 | 186 | biimpd 219 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑓 ∘𝑟
≤ 𝐻 → ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝑈, 𝐶, 0))) |
188 | 187 | impr 649 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
∀𝑥 ∈ ℝ
(𝑓‘𝑥) ≤ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
189 | 188 | r19.21bi 2932 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
190 | 179, 189 | syldan 487 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
191 | 163 | adantlr 751 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) |
192 | 191 | iftrued 4094 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑈, 𝐶, 0) = 𝐶) |
193 | 190, 192 | breqtrd 4679 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ 𝐶) |
194 | | iftrue 4092 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) = (𝑓‘𝑥)) |
195 | 194 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) = (𝑓‘𝑥)) |
196 | | iftrue 4092 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶) |
197 | 196 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶) |
198 | 193, 195,
197 | 3brtr4d 4685 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
199 | | 0le0 11110 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
0 |
200 | 199 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 𝐴 → 0 ≤ 0) |
201 | | iffalse 4095 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) = 0) |
202 | | iffalse 4095 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 0) |
203 | 200, 201,
202 | 3brtr4d 4685 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
204 | 203 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
205 | 198, 204 | pm2.61dan 832 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
206 | 205 | a1d 25 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → (𝑥 ∈ ℝ → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
207 | 177, 206 | ralrimi 2957 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
∀𝑥 ∈ ℝ
if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
208 | 168 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
209 | 31, 35, 167, 38, 208 | ofrfval2 6915 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
210 | 209 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
211 | 207, 210 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘𝑟 ≤ 𝐹) |
212 | | itg2ub 23500 |
. . . . . . 7
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∈ dom ∫1 ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘𝑟 ≤ 𝐹) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (𝑓‘𝑥), 0))) ≤ (∫2‘𝐹)) |
213 | 170, 8, 211, 212 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (𝑓‘𝑥), 0))) ≤ (∫2‘𝐹)) |
214 | | ssun2 3777 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
215 | 214, 72 | syl5sseqr 3654 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ⊆ 𝑈) |
216 | 215 | sselda 3603 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈) |
217 | 216 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈) |
218 | 217, 85 | syldan 487 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
219 | 86 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐵) → 0 ∈
(0[,]+∞)) |
220 | 218, 219 | ifclda 4120 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐵, 𝐶, 0) ∈ (0[,]+∞)) |
221 | | itg2split.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
222 | 220, 221 | fmptd 6385 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞)) |
223 | 222 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → 𝐺:ℝ⟶(0[,]+∞)) |
224 | | mblss 23299 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ dom vol → 𝐵 ⊆
ℝ) |
225 | 12, 224 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → 𝐵 ⊆
ℝ) |
226 | 225 | sselda 3603 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ℝ) |
227 | 226, 189 | syldan 487 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
228 | 216 | adantlr 751 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈) |
229 | 228 | iftrued 4094 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝑈, 𝐶, 0) = 𝐶) |
230 | 227, 229 | breqtrd 4679 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → (𝑓‘𝑥) ≤ 𝐶) |
231 | | iftrue 4092 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐵 → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) = (𝑓‘𝑥)) |
232 | 231 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) = (𝑓‘𝑥)) |
233 | | iftrue 4092 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐵 → if(𝑥 ∈ 𝐵, 𝐶, 0) = 𝐶) |
234 | 233 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐵, 𝐶, 0) = 𝐶) |
235 | 230, 232,
234 | 3brtr4d 4685 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
236 | 199 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 𝐵 → 0 ≤ 0) |
237 | | iffalse 4095 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 𝐵 → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) = 0) |
238 | | iffalse 4095 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 𝐵 → if(𝑥 ∈ 𝐵, 𝐶, 0) = 0) |
239 | 236, 237,
238 | 3brtr4d 4685 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 ∈ 𝐵 → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
240 | 239 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) ∧ ¬ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
241 | 235, 240 | pm2.61dan 832 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
242 | 241 | a1d 25 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → (𝑥 ∈ ℝ → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))) |
243 | 177, 242 | ralrimi 2957 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
∀𝑥 ∈ ℝ
if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
244 | 221 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0))) |
245 | 31, 37, 220, 39, 244 | ofrfval2 6915 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∘𝑟 ≤ 𝐺 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))) |
246 | 245 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∘𝑟 ≤ 𝐺 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))) |
247 | 243, 246 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∘𝑟 ≤ 𝐺) |
248 | | itg2ub 23500 |
. . . . . . 7
⊢ ((𝐺:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∈ dom ∫1 ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∘𝑟 ≤ 𝐺) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, (𝑓‘𝑥), 0))) ≤ (∫2‘𝐺)) |
249 | 223, 15, 247, 248 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, (𝑓‘𝑥), 0))) ≤ (∫2‘𝐺)) |
250 | 10, 17, 159, 160, 213, 249 | le2addd 10646 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))) ≤ ((∫2‘𝐹) +
(∫2‘𝐺))) |
251 | 3, 18, 22, 158, 250 | letrd 10194 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐻)) →
(∫1‘𝑓)
≤ ((∫2‘𝐹) + (∫2‘𝐺))) |
252 | 251 | expr 643 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑓 ∘𝑟
≤ 𝐻 →
(∫1‘𝑓)
≤ ((∫2‘𝐹) + (∫2‘𝐺)))) |
253 | 252 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐻 →
(∫1‘𝑓)
≤ ((∫2‘𝐹) + (∫2‘𝐺)))) |
254 | 21 | rexrd 10089 |
. . 3
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ∈
ℝ*) |
255 | | itg2leub 23501 |
. . 3
⊢ ((𝐻:ℝ⟶(0[,]+∞)
∧ ((∫2‘𝐹) + (∫2‘𝐺)) ∈ ℝ*)
→ ((∫2‘𝐻) ≤ ((∫2‘𝐹) +
(∫2‘𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐻 →
(∫1‘𝑓)
≤ ((∫2‘𝐹) + (∫2‘𝐺))))) |
256 | 90, 254, 255 | syl2anc 693 |
. 2
⊢ (𝜑 →
((∫2‘𝐻) ≤ ((∫2‘𝐹) +
(∫2‘𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐻 →
(∫1‘𝑓)
≤ ((∫2‘𝐹) + (∫2‘𝐺))))) |
257 | 253, 256 | mpbird 247 |
1
⊢ (𝜑 →
(∫2‘𝐻)
≤ ((∫2‘𝐹) + (∫2‘𝐺))) |