| Step | Hyp | Ref
| Expression |
| 1 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → 𝑓 ∈ dom
∫1) |
| 2 | | itg1cl 25720 |
. . . . . 6
⊢ (𝑓 ∈ dom ∫1
→ (∫1‘𝑓) ∈ ℝ) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
(∫1‘𝑓)
∈ ℝ) |
| 4 | | itg2split.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ dom vol) |
| 5 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → 𝐴 ∈ dom vol) |
| 6 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) |
| 7 | 6 | i1fres 25740 |
. . . . . . . 8
⊢ ((𝑓 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∈ dom
∫1) |
| 8 | 1, 5, 7 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∈ dom
∫1) |
| 9 | | itg1cl 25720 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∈ dom ∫1 →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (𝑓‘𝑥), 0))) ∈ ℝ) |
| 10 | 8, 9 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (𝑓‘𝑥), 0))) ∈ ℝ) |
| 11 | | itg2split.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ dom vol) |
| 12 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → 𝐵 ∈ dom vol) |
| 13 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) |
| 14 | 13 | i1fres 25740 |
. . . . . . . 8
⊢ ((𝑓 ∈ dom ∫1
∧ 𝐵 ∈ dom vol)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∈ dom
∫1) |
| 15 | 1, 12, 14 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∈ dom
∫1) |
| 16 | | itg1cl 25720 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∈ dom ∫1 →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, (𝑓‘𝑥), 0))) ∈ ℝ) |
| 17 | 15, 16 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, (𝑓‘𝑥), 0))) ∈ ℝ) |
| 18 | 10, 17 | readdcld 11290 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))) ∈ ℝ) |
| 19 | | itg2split.sf |
. . . . . . 7
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ) |
| 20 | | itg2split.sg |
. . . . . . 7
⊢ (𝜑 →
(∫2‘𝐺)
∈ ℝ) |
| 21 | 19, 20 | readdcld 11290 |
. . . . . 6
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ∈
ℝ) |
| 22 | 21 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
((∫2‘𝐹) + (∫2‘𝐺)) ∈
ℝ) |
| 23 | | inss1 4237 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
| 24 | | mblss 25566 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
| 25 | 4, 24 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
| 26 | 23, 25 | sstrid 3995 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ ℝ) |
| 27 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → (𝐴 ∩ 𝐵) ⊆ ℝ) |
| 28 | | itg2split.i |
. . . . . . . 8
⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0) |
| 29 | 28 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → (vol*‘(𝐴 ∩ 𝐵)) = 0) |
| 30 | | reex 11246 |
. . . . . . . . . . 11
⊢ ℝ
∈ V |
| 31 | 30 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ∈
V) |
| 32 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝑓‘𝑥) ∈ V |
| 33 | | c0ex 11255 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
| 34 | 32, 33 | ifex 4576 |
. . . . . . . . . . 11
⊢ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ∈ V |
| 35 | 34 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ∈ V) |
| 36 | 32, 33 | ifex 4576 |
. . . . . . . . . . 11
⊢ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ∈ V |
| 37 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ∈ V) |
| 38 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0))) |
| 39 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))) |
| 40 | 31, 35, 37, 38, 39 | offval2 7717 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))) |
| 41 | 40 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))) |
| 42 | 8, 15 | i1fadd 25730 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))) ∈ dom
∫1) |
| 43 | 41, 42 | eqeltrrd 2842 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))) ∈ dom
∫1) |
| 44 | | i1ff 25711 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ dom ∫1
→ 𝑓:ℝ⟶ℝ) |
| 45 | 1, 44 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → 𝑓:ℝ⟶ℝ) |
| 46 | | eldifi 4131 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → 𝑦 ∈ ℝ) |
| 47 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℝ⟶ℝ ∧
𝑦 ∈ ℝ) →
(𝑓‘𝑦) ∈ ℝ) |
| 48 | 45, 46, 47 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑦) ∈ ℝ) |
| 49 | 48 | leidd 11829 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑦) ≤ (𝑓‘𝑦)) |
| 50 | 49 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → (𝑓‘𝑦) ≤ (𝑓‘𝑦)) |
| 51 | | iftrue 4531 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐴 → if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) = (𝑓‘𝑦)) |
| 52 | 51 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) = (𝑓‘𝑦)) |
| 53 | | eldifn 4132 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → ¬ 𝑦 ∈ (𝐴 ∩ 𝐵)) |
| 54 | 53 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ¬ 𝑦 ∈ (𝐴 ∩ 𝐵)) |
| 55 | | elin 3967 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 56 | 54, 55 | sylnib 328 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ¬ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 57 | | imnan 399 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝐴 → ¬ 𝑦 ∈ 𝐵) ↔ ¬ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 58 | 56, 57 | sylibr 234 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑦 ∈ 𝐴 → ¬ 𝑦 ∈ 𝐵)) |
| 59 | 58 | imp 406 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → ¬ 𝑦 ∈ 𝐵) |
| 60 | | iffalse 4534 |
. . . . . . . . . . . . 13
⊢ (¬
𝑦 ∈ 𝐵 → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) = 0) |
| 61 | 59, 60 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) = 0) |
| 62 | 52, 61 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) = ((𝑓‘𝑦) + 0)) |
| 63 | 48 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑦) ∈ ℂ) |
| 64 | 63 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → (𝑓‘𝑦) ∈ ℂ) |
| 65 | 64 | addridd 11461 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → ((𝑓‘𝑦) + 0) = (𝑓‘𝑦)) |
| 66 | 62, 65 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) = (𝑓‘𝑦)) |
| 67 | 50, 66 | breqtrrd 5171 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑦 ∈ 𝐴) → (𝑓‘𝑦) ≤ (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0))) |
| 68 | 49 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑓 ∘r
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑓‘𝑦) ≤ (𝑓‘𝑦)) |
| 69 | | iftrue 4531 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐵 → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) = (𝑓‘𝑦)) |
| 70 | 69 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑓 ∘r
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) = (𝑓‘𝑦)) |
| 71 | 68, 70 | breqtrrd 5171 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑓 ∘r
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑓‘𝑦) ≤ if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) |
| 72 | | itg2split.u |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) |
| 73 | 72 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → 𝑈 = (𝐴 ∪ 𝐵)) |
| 74 | 73 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑦 ∈ 𝑈 ↔ 𝑦 ∈ (𝐴 ∪ 𝐵))) |
| 75 | | elun 4153 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (𝐴 ∪ 𝐵) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)) |
| 76 | 74, 75 | bitrdi 287 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑦 ∈ 𝑈 ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))) |
| 77 | 76 | notbid 318 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (¬ 𝑦 ∈ 𝑈 ↔ ¬ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))) |
| 78 | | ioran 986 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵) ↔ (¬ 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)) |
| 79 | 77, 78 | bitrdi 287 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (¬ 𝑦 ∈ 𝑈 ↔ (¬ 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))) |
| 80 | 79 | biimpar 477 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ (¬ 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)) → ¬ 𝑦 ∈ 𝑈) |
| 81 | | simprr 773 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → 𝑓 ∘r ≤ 𝐻) |
| 82 | 45 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → 𝑓 Fn ℝ) |
| 83 | | itg2split.c |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞)) |
| 84 | 83 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞)) |
| 85 | | 0e0iccpnf 13499 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
(0[,]+∞) |
| 86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝑈) → 0 ∈
(0[,]+∞)) |
| 87 | 84, 86 | ifclda 4561 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞)) |
| 88 | | itg2split.h |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
| 89 | 87, 88 | fmptd 7134 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐻:ℝ⟶(0[,]+∞)) |
| 90 | 89 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐻 Fn ℝ) |
| 91 | 90 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → 𝐻 Fn ℝ) |
| 92 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → ℝ ∈
V) |
| 93 | | inidm 4227 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℝ
∩ ℝ) = ℝ |
| 94 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ ℝ) → (𝑓‘𝑦) = (𝑓‘𝑦)) |
| 95 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ ℝ) → (𝐻‘𝑦) = (𝐻‘𝑦)) |
| 96 | 82, 91, 92, 92, 93, 94, 95 | ofrfval 7707 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → (𝑓 ∘r ≤ 𝐻 ↔ ∀𝑦 ∈ ℝ (𝑓‘𝑦) ≤ (𝐻‘𝑦))) |
| 97 | 81, 96 | mpbid 232 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → ∀𝑦 ∈ ℝ (𝑓‘𝑦) ≤ (𝐻‘𝑦)) |
| 98 | 97 | r19.21bi 3251 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ ℝ) → (𝑓‘𝑦) ≤ (𝐻‘𝑦)) |
| 99 | 46, 98 | sylan2 593 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑦) ≤ (𝐻‘𝑦)) |
| 100 | 99 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝑈) → (𝑓‘𝑦) ≤ (𝐻‘𝑦)) |
| 101 | 46 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → 𝑦 ∈ ℝ) |
| 102 | | eldif 3961 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (ℝ ∖ 𝑈) ↔ (𝑦 ∈ ℝ ∧ ¬ 𝑦 ∈ 𝑈)) |
| 103 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥𝑦 |
| 104 | | nfmpt1 5250 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
| 105 | 88, 104 | nfcxfr 2903 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥𝐻 |
| 106 | 105, 103 | nffv 6916 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝐻‘𝑦) |
| 107 | 106 | nfeq1 2921 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥(𝐻‘𝑦) = 0 |
| 108 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝐻‘𝑥) = 0 ↔ (𝐻‘𝑦) = 0)) |
| 109 | | eldif 3961 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (ℝ ∖ 𝑈) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝑈)) |
| 110 | 88 | fvmpt2i 7026 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ → (𝐻‘𝑥) = ( I ‘if(𝑥 ∈ 𝑈, 𝐶, 0))) |
| 111 | | iffalse 4534 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑥 ∈ 𝑈 → if(𝑥 ∈ 𝑈, 𝐶, 0) = 0) |
| 112 | 111 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑥 ∈ 𝑈 → ( I ‘if(𝑥 ∈ 𝑈, 𝐶, 0)) = ( I ‘0)) |
| 113 | | 0cn 11253 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℂ |
| 114 | | fvi 6985 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ∈
ℂ → ( I ‘0) = 0) |
| 115 | 113, 114 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( I
‘0) = 0 |
| 116 | 112, 115 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑥 ∈ 𝑈 → ( I ‘if(𝑥 ∈ 𝑈, 𝐶, 0)) = 0) |
| 117 | 110, 116 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ ¬
𝑥 ∈ 𝑈) → (𝐻‘𝑥) = 0) |
| 118 | 109, 117 | sylbi 217 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (ℝ ∖ 𝑈) → (𝐻‘𝑥) = 0) |
| 119 | 103, 107,
108, 118 | vtoclgaf 3576 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (ℝ ∖ 𝑈) → (𝐻‘𝑦) = 0) |
| 120 | 102, 119 | sylbir 235 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ ∧ ¬
𝑦 ∈ 𝑈) → (𝐻‘𝑦) = 0) |
| 121 | 101, 120 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝑈) → (𝐻‘𝑦) = 0) |
| 122 | 100, 121 | breqtrd 5169 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝑈) → (𝑓‘𝑦) ≤ 0) |
| 123 | 80, 122 | syldan 591 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ (¬ 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)) → (𝑓‘𝑦) ≤ 0) |
| 124 | 123 | anassrs 467 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑓 ∘r
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ∈ 𝐵) → (𝑓‘𝑦) ≤ 0) |
| 125 | 60 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑓 ∘r
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ∈ 𝐵) → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) = 0) |
| 126 | 124, 125 | breqtrrd 5171 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑓 ∘r
≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ∈ 𝐵) → (𝑓‘𝑦) ≤ if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) |
| 127 | 71, 126 | pm2.61dan 813 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) → (𝑓‘𝑦) ≤ if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) |
| 128 | | iffalse 4534 |
. . . . . . . . . . . . 13
⊢ (¬
𝑦 ∈ 𝐴 → if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) = 0) |
| 129 | 128 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) → if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) = 0) |
| 130 | 129 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) → (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) = (0 + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0))) |
| 131 | | 0re 11263 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
| 132 | | ifcl 4571 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) ∈ ℝ) |
| 133 | 48, 131, 132 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) ∈ ℝ) |
| 134 | 133 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) ∈ ℂ) |
| 135 | 134 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) → if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0) ∈ ℂ) |
| 136 | 135 | addlidd 11462 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) → (0 + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) = if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) |
| 137 | 130, 136 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) → (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) = if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) |
| 138 | 127, 137 | breqtrrd 5171 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑦 ∈ 𝐴) → (𝑓‘𝑦) ≤ (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0))) |
| 139 | 67, 138 | pm2.61dan 813 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑦) ≤ (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0))) |
| 140 | | eleq1w 2824 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
| 141 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑓‘𝑥) = (𝑓‘𝑦)) |
| 142 | 140, 141 | ifbieq1d 4550 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) = if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0)) |
| 143 | | eleq1w 2824 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
| 144 | 143, 141 | ifbieq1d 4550 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) = if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) |
| 145 | 142, 144 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) = (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0))) |
| 146 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ ↦
(if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))) |
| 147 | | ovex 7464 |
. . . . . . . . . 10
⊢ (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0)) ∈ V |
| 148 | 145, 146,
147 | fvmpt 7016 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → ((𝑥 ∈ ℝ ↦
(if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))‘𝑦) = (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0))) |
| 149 | 101, 148 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))‘𝑦) = (if(𝑦 ∈ 𝐴, (𝑓‘𝑦), 0) + if(𝑦 ∈ 𝐵, (𝑓‘𝑦), 0))) |
| 150 | 139, 149 | breqtrrd 5171 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑦) ≤ ((𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))‘𝑦)) |
| 151 | 1, 27, 29, 43, 150 | itg1lea 25747 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
(∫1‘𝑓)
≤ (∫1‘(𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))))) |
| 152 | 41 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
(∫1‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))) = (∫1‘(𝑥 ∈ ℝ ↦
(if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))))) |
| 153 | 8, 15 | itg1add 25736 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
(∫1‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))) = ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))))) |
| 154 | 152, 153 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
(∫1‘(𝑥
∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) + if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))) = ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))))) |
| 155 | 151, 154 | breqtrd 5169 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
(∫1‘𝑓)
≤ ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0))))) |
| 156 | 19 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
(∫2‘𝐹)
∈ ℝ) |
| 157 | 20 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
(∫2‘𝐺)
∈ ℝ) |
| 158 | | ssun1 4178 |
. . . . . . . . . . . . . 14
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
| 159 | 158, 72 | sseqtrrid 4027 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆ 𝑈) |
| 160 | 159 | sselda 3983 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) |
| 161 | 160 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) |
| 162 | 161, 84 | syldan 591 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) |
| 163 | 85 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) |
| 164 | 162, 163 | ifclda 4561 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,]+∞)) |
| 165 | | itg2split.f |
. . . . . . . . 9
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
| 166 | 164, 165 | fmptd 7134 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) |
| 167 | 166 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → 𝐹:ℝ⟶(0[,]+∞)) |
| 168 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝜑 |
| 169 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑓 ∈ dom
∫1 |
| 170 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑓 |
| 171 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥
∘r ≤ |
| 172 | 170, 171,
105 | nfbr 5190 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑓 ∘r ≤ 𝐻 |
| 173 | 169, 172 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑓 ∈ dom ∫1
∧ 𝑓 ∘r
≤ 𝐻) |
| 174 | 168, 173 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) |
| 175 | 5, 24 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → 𝐴 ⊆ ℝ) |
| 176 | 175 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
| 177 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ℝ
∈ V) |
| 178 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) ∈ V) |
| 179 | 87 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞)) |
| 180 | 44 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝑓:ℝ⟶ℝ) |
| 181 | 180 | feqmptd 6977 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓‘𝑥))) |
| 182 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0))) |
| 183 | 177, 178,
179, 181, 182 | ofrfval2 7718 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑓 ∘r ≤ 𝐻 ↔ ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝑈, 𝐶, 0))) |
| 184 | 183 | biimpd 229 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑓 ∘r ≤ 𝐻 → ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝑈, 𝐶, 0))) |
| 185 | 184 | impr 454 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
| 186 | 185 | r19.21bi 3251 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
| 187 | 176, 186 | syldan 591 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
| 188 | 160 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) |
| 189 | 188 | iftrued 4533 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑈, 𝐶, 0) = 𝐶) |
| 190 | 187, 189 | breqtrd 5169 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ 𝐶) |
| 191 | | iftrue 4531 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) = (𝑓‘𝑥)) |
| 192 | 191 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) = (𝑓‘𝑥)) |
| 193 | | iftrue 4531 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶) |
| 194 | 193 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶) |
| 195 | 190, 192,
194 | 3brtr4d 5175 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
| 196 | | 0le0 12367 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
0 |
| 197 | 196 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 𝐴 → 0 ≤ 0) |
| 198 | | iffalse 4534 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) = 0) |
| 199 | | iffalse 4534 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 0) |
| 200 | 197, 198,
199 | 3brtr4d 5175 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
| 201 | 200 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
| 202 | 195, 201 | pm2.61dan 813 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
| 203 | 202 | a1d 25 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → (𝑥 ∈ ℝ → if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
| 204 | 174, 203 | ralrimi 3257 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
| 205 | 165 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
| 206 | 31, 35, 164, 38, 205 | ofrfval2 7718 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
| 207 | 206 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
| 208 | 204, 207 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘r ≤ 𝐹) |
| 209 | | itg2ub 25768 |
. . . . . . 7
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∈ dom ∫1 ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0)) ∘r ≤ 𝐹) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (𝑓‘𝑥), 0))) ≤ (∫2‘𝐹)) |
| 210 | 167, 8, 208, 209 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (𝑓‘𝑥), 0))) ≤ (∫2‘𝐹)) |
| 211 | | ssun2 4179 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
| 212 | 211, 72 | sseqtrrid 4027 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ⊆ 𝑈) |
| 213 | 212 | sselda 3983 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈) |
| 214 | 213 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈) |
| 215 | 214, 84 | syldan 591 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
| 216 | 85 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐵) → 0 ∈
(0[,]+∞)) |
| 217 | 215, 216 | ifclda 4561 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐵, 𝐶, 0) ∈ (0[,]+∞)) |
| 218 | | itg2split.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
| 219 | 217, 218 | fmptd 7134 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞)) |
| 220 | 219 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → 𝐺:ℝ⟶(0[,]+∞)) |
| 221 | | mblss 25566 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ dom vol → 𝐵 ⊆
ℝ) |
| 222 | 12, 221 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → 𝐵 ⊆ ℝ) |
| 223 | 222 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ℝ) |
| 224 | 223, 186 | syldan 591 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
| 225 | 213 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈) |
| 226 | 225 | iftrued 4533 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝑈, 𝐶, 0) = 𝐶) |
| 227 | 224, 226 | breqtrd 5169 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → (𝑓‘𝑥) ≤ 𝐶) |
| 228 | | iftrue 4531 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐵 → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) = (𝑓‘𝑥)) |
| 229 | 228 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) = (𝑓‘𝑥)) |
| 230 | | iftrue 4531 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐵 → if(𝑥 ∈ 𝐵, 𝐶, 0) = 𝐶) |
| 231 | 230 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐵, 𝐶, 0) = 𝐶) |
| 232 | 227, 229,
231 | 3brtr4d 5175 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
| 233 | 196 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 𝐵 → 0 ≤ 0) |
| 234 | | iffalse 4534 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 𝐵 → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) = 0) |
| 235 | | iffalse 4534 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 𝐵 → if(𝑥 ∈ 𝐵, 𝐶, 0) = 0) |
| 236 | 233, 234,
235 | 3brtr4d 5175 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 ∈ 𝐵 → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
| 237 | 236 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) ∧ ¬ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
| 238 | 232, 237 | pm2.61dan 813 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
| 239 | 238 | a1d 25 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → (𝑥 ∈ ℝ → if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))) |
| 240 | 174, 239 | ralrimi 3257 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
| 241 | 218 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0))) |
| 242 | 31, 37, 217, 39, 241 | ofrfval2 7718 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∘r ≤ 𝐺 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))) |
| 243 | 242 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∘r ≤ 𝐺 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))) |
| 244 | 240, 243 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∘r ≤ 𝐺) |
| 245 | | itg2ub 25768 |
. . . . . . 7
⊢ ((𝐺:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∈ dom ∫1 ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)) ∘r ≤ 𝐺) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, (𝑓‘𝑥), 0))) ≤ (∫2‘𝐺)) |
| 246 | 220, 15, 244, 245 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, (𝑓‘𝑥), 0))) ≤ (∫2‘𝐺)) |
| 247 | 10, 17, 156, 157, 210, 246 | le2addd 11882 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝑓‘𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, (𝑓‘𝑥), 0)))) ≤ ((∫2‘𝐹) +
(∫2‘𝐺))) |
| 248 | 3, 18, 22, 155, 247 | letrd 11418 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐻)) →
(∫1‘𝑓)
≤ ((∫2‘𝐹) + (∫2‘𝐺))) |
| 249 | 248 | expr 456 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑓 ∘r ≤ 𝐻 →
(∫1‘𝑓)
≤ ((∫2‘𝐹) + (∫2‘𝐺)))) |
| 250 | 249 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐻 →
(∫1‘𝑓)
≤ ((∫2‘𝐹) + (∫2‘𝐺)))) |
| 251 | 21 | rexrd 11311 |
. . 3
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ∈
ℝ*) |
| 252 | | itg2leub 25769 |
. . 3
⊢ ((𝐻:ℝ⟶(0[,]+∞)
∧ ((∫2‘𝐹) + (∫2‘𝐺)) ∈ ℝ*)
→ ((∫2‘𝐻) ≤ ((∫2‘𝐹) +
(∫2‘𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐻 →
(∫1‘𝑓)
≤ ((∫2‘𝐹) + (∫2‘𝐺))))) |
| 253 | 89, 251, 252 | syl2anc 584 |
. 2
⊢ (𝜑 →
((∫2‘𝐻) ≤ ((∫2‘𝐹) +
(∫2‘𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐻 →
(∫1‘𝑓)
≤ ((∫2‘𝐹) + (∫2‘𝐺))))) |
| 254 | 250, 253 | mpbird 257 |
1
⊢ (𝜑 →
(∫2‘𝐻)
≤ ((∫2‘𝐹) + (∫2‘𝐺))) |