MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg2splitlem Structured version   Visualization version   GIF version

Theorem itg2splitlem 23560
Description: Lemma for itg2split 23561. (Contributed by Mario Carneiro, 11-Aug-2014.)
Hypotheses
Ref Expression
itg2split.a (𝜑𝐴 ∈ dom vol)
itg2split.b (𝜑𝐵 ∈ dom vol)
itg2split.i (𝜑 → (vol*‘(𝐴𝐵)) = 0)
itg2split.u (𝜑𝑈 = (𝐴𝐵))
itg2split.c ((𝜑𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
itg2split.f 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0))
itg2split.g 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0))
itg2split.h 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
itg2split.sf (𝜑 → (∫2𝐹) ∈ ℝ)
itg2split.sg (𝜑 → (∫2𝐺) ∈ ℝ)
Assertion
Ref Expression
itg2splitlem (𝜑 → (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)))
Distinct variable groups:   𝜑,𝑥   𝑥,𝐴   𝑥,𝐵   𝑥,𝑈
Allowed substitution hints:   𝐶(𝑥)   𝐹(𝑥)   𝐺(𝑥)   𝐻(𝑥)

Proof of Theorem itg2splitlem
Dummy variables 𝑓 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprl 809 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝑓 ∈ dom ∫1)
2 itg1cl 23497 . . . . . 6 (𝑓 ∈ dom ∫1 → (∫1𝑓) ∈ ℝ)
31, 2syl 17 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1𝑓) ∈ ℝ)
4 itg2split.a . . . . . . . . 9 (𝜑𝐴 ∈ dom vol)
54adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐴 ∈ dom vol)
6 eqid 2651 . . . . . . . . 9 (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))
76i1fres 23517 . . . . . . . 8 ((𝑓 ∈ dom ∫1𝐴 ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∈ dom ∫1)
81, 5, 7syl2anc 694 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∈ dom ∫1)
9 itg1cl 23497 . . . . . . 7 ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) ∈ ℝ)
108, 9syl 17 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) ∈ ℝ)
11 itg2split.b . . . . . . . . 9 (𝜑𝐵 ∈ dom vol)
1211adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐵 ∈ dom vol)
13 eqid 2651 . . . . . . . . 9 (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))
1413i1fres 23517 . . . . . . . 8 ((𝑓 ∈ dom ∫1𝐵 ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∈ dom ∫1)
151, 12, 14syl2anc 694 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∈ dom ∫1)
16 itg1cl 23497 . . . . . . 7 ((𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ∈ ℝ)
1715, 16syl 17 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ∈ ℝ)
1810, 17readdcld 10107 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))) ∈ ℝ)
19 itg2split.sf . . . . . . 7 (𝜑 → (∫2𝐹) ∈ ℝ)
20 itg2split.sg . . . . . . 7 (𝜑 → (∫2𝐺) ∈ ℝ)
2119, 20readdcld 10107 . . . . . 6 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ)
2221adantr 480 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ)
23 inss1 3866 . . . . . . . . 9 (𝐴𝐵) ⊆ 𝐴
24 mblss 23345 . . . . . . . . . 10 (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
254, 24syl 17 . . . . . . . . 9 (𝜑𝐴 ⊆ ℝ)
2623, 25syl5ss 3647 . . . . . . . 8 (𝜑 → (𝐴𝐵) ⊆ ℝ)
2726adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝐴𝐵) ⊆ ℝ)
28 itg2split.i . . . . . . . 8 (𝜑 → (vol*‘(𝐴𝐵)) = 0)
2928adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (vol*‘(𝐴𝐵)) = 0)
30 reex 10065 . . . . . . . . . . 11 ℝ ∈ V
3130a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ∈ V)
32 fvex 6239 . . . . . . . . . . . 12 (𝑓𝑥) ∈ V
33 c0ex 10072 . . . . . . . . . . . 12 0 ∈ V
3432, 33ifex 4189 . . . . . . . . . . 11 if(𝑥𝐴, (𝑓𝑥), 0) ∈ V
3534a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐴, (𝑓𝑥), 0) ∈ V)
3632, 33ifex 4189 . . . . . . . . . . 11 if(𝑥𝐵, (𝑓𝑥), 0) ∈ V
3736a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐵, (𝑓𝑥), 0) ∈ V)
38 eqidd 2652 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)))
39 eqidd 2652 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))
4031, 35, 37, 38, 39offval2 6956 . . . . . . . . 9 (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0))))
4140adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0))))
428, 15i1fadd 23507 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ∈ dom ∫1)
4341, 42eqeltrrd 2731 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0))) ∈ dom ∫1)
44 i1ff 23488 . . . . . . . . . . . . . 14 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
451, 44syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝑓:ℝ⟶ℝ)
46 eldifi 3765 . . . . . . . . . . . . 13 (𝑦 ∈ (ℝ ∖ (𝐴𝐵)) → 𝑦 ∈ ℝ)
47 ffvelrn 6397 . . . . . . . . . . . . 13 ((𝑓:ℝ⟶ℝ ∧ 𝑦 ∈ ℝ) → (𝑓𝑦) ∈ ℝ)
4845, 46, 47syl2an 493 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ∈ ℝ)
4948leidd 10632 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ≤ (𝑓𝑦))
5049adantr 480 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (𝑓𝑦) ≤ (𝑓𝑦))
51 iftrue 4125 . . . . . . . . . . . . 13 (𝑦𝐴 → if(𝑦𝐴, (𝑓𝑦), 0) = (𝑓𝑦))
5251adantl 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → if(𝑦𝐴, (𝑓𝑦), 0) = (𝑓𝑦))
53 eldifn 3766 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (ℝ ∖ (𝐴𝐵)) → ¬ 𝑦 ∈ (𝐴𝐵))
5453adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ 𝑦 ∈ (𝐴𝐵))
55 elin 3829 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴𝑦𝐵))
5654, 55sylnib 317 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ (𝑦𝐴𝑦𝐵))
57 imnan 437 . . . . . . . . . . . . . . 15 ((𝑦𝐴 → ¬ 𝑦𝐵) ↔ ¬ (𝑦𝐴𝑦𝐵))
5856, 57sylibr 224 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑦𝐴 → ¬ 𝑦𝐵))
5958imp 444 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → ¬ 𝑦𝐵)
60 iffalse 4128 . . . . . . . . . . . . 13 𝑦𝐵 → if(𝑦𝐵, (𝑓𝑦), 0) = 0)
6159, 60syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → if(𝑦𝐵, (𝑓𝑦), 0) = 0)
6252, 61oveq12d 6708 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) = ((𝑓𝑦) + 0))
6348recnd 10106 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ∈ ℂ)
6463adantr 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (𝑓𝑦) ∈ ℂ)
6564addid1d 10274 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → ((𝑓𝑦) + 0) = (𝑓𝑦))
6662, 65eqtrd 2685 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) = (𝑓𝑦))
6750, 66breqtrrd 4713 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (𝑓𝑦) ≤ (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
6849ad2antrr 762 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ 𝑦𝐵) → (𝑓𝑦) ≤ (𝑓𝑦))
69 iftrue 4125 . . . . . . . . . . . . 13 (𝑦𝐵 → if(𝑦𝐵, (𝑓𝑦), 0) = (𝑓𝑦))
7069adantl 481 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ 𝑦𝐵) → if(𝑦𝐵, (𝑓𝑦), 0) = (𝑓𝑦))
7168, 70breqtrrd 4713 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ 𝑦𝐵) → (𝑓𝑦) ≤ if(𝑦𝐵, (𝑓𝑦), 0))
72 itg2split.u . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑈 = (𝐴𝐵))
7372ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → 𝑈 = (𝐴𝐵))
7473eleq2d 2716 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑦𝑈𝑦 ∈ (𝐴𝐵)))
75 elun 3786 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴𝑦𝐵))
7674, 75syl6bb 276 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑦𝑈 ↔ (𝑦𝐴𝑦𝐵)))
7776notbid 307 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (¬ 𝑦𝑈 ↔ ¬ (𝑦𝐴𝑦𝐵)))
78 ioran 510 . . . . . . . . . . . . . . . 16 (¬ (𝑦𝐴𝑦𝐵) ↔ (¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵))
7977, 78syl6bb 276 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (¬ 𝑦𝑈 ↔ (¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵)))
8079biimpar 501 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ (¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵)) → ¬ 𝑦𝑈)
81 simprr 811 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝑓𝑟𝐻)
82 ffn 6083 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:ℝ⟶ℝ → 𝑓 Fn ℝ)
8345, 82syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝑓 Fn ℝ)
84 itg2split.c . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
8584adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
86 0e0iccpnf 12321 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ (0[,]+∞)
8786a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝑈) → 0 ∈ (0[,]+∞))
8885, 87ifclda 4153 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
89 itg2split.h . . . . . . . . . . . . . . . . . . . . . . 23 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
9088, 89fmptd 6425 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐻:ℝ⟶(0[,]+∞))
91 ffn 6083 . . . . . . . . . . . . . . . . . . . . . 22 (𝐻:ℝ⟶(0[,]+∞) → 𝐻 Fn ℝ)
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐻 Fn ℝ)
9392adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐻 Fn ℝ)
9430a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ℝ ∈ V)
95 inidm 3855 . . . . . . . . . . . . . . . . . . . 20 (ℝ ∩ ℝ) = ℝ
96 eqidd 2652 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ ℝ) → (𝑓𝑦) = (𝑓𝑦))
97 eqidd 2652 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ ℝ) → (𝐻𝑦) = (𝐻𝑦))
9883, 93, 94, 94, 95, 96, 97ofrfval 6947 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑓𝑟𝐻 ↔ ∀𝑦 ∈ ℝ (𝑓𝑦) ≤ (𝐻𝑦)))
9981, 98mpbid 222 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ∀𝑦 ∈ ℝ (𝑓𝑦) ≤ (𝐻𝑦))
10099r19.21bi 2961 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ ℝ) → (𝑓𝑦) ≤ (𝐻𝑦))
10146, 100sylan2 490 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ≤ (𝐻𝑦))
102101adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝑈) → (𝑓𝑦) ≤ (𝐻𝑦))
10346adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → 𝑦 ∈ ℝ)
104 eldif 3617 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (ℝ ∖ 𝑈) ↔ (𝑦 ∈ ℝ ∧ ¬ 𝑦𝑈))
105 nfcv 2793 . . . . . . . . . . . . . . . . . 18 𝑥𝑦
106 nfmpt1 4780 . . . . . . . . . . . . . . . . . . . . 21 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
10789, 106nfcxfr 2791 . . . . . . . . . . . . . . . . . . . 20 𝑥𝐻
108107, 105nffv 6236 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐻𝑦)
109108nfeq1 2807 . . . . . . . . . . . . . . . . . 18 𝑥(𝐻𝑦) = 0
110 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
111110eqeq1d 2653 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝐻𝑥) = 0 ↔ (𝐻𝑦) = 0))
112 eldif 3617 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (ℝ ∖ 𝑈) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥𝑈))
11389fvmpt2i 6329 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → (𝐻𝑥) = ( I ‘if(𝑥𝑈, 𝐶, 0)))
114 iffalse 4128 . . . . . . . . . . . . . . . . . . . . . 22 𝑥𝑈 → if(𝑥𝑈, 𝐶, 0) = 0)
115114fveq2d 6233 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑈 → ( I ‘if(𝑥𝑈, 𝐶, 0)) = ( I ‘0))
116 0cn 10070 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℂ
117 fvi 6294 . . . . . . . . . . . . . . . . . . . . . 22 (0 ∈ ℂ → ( I ‘0) = 0)
118116, 117ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ( I ‘0) = 0
119115, 118syl6eq 2701 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑈 → ( I ‘if(𝑥𝑈, 𝐶, 0)) = 0)
120113, 119sylan9eq 2705 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℝ ∧ ¬ 𝑥𝑈) → (𝐻𝑥) = 0)
121112, 120sylbi 207 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (ℝ ∖ 𝑈) → (𝐻𝑥) = 0)
122105, 109, 111, 121vtoclgaf 3302 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (ℝ ∖ 𝑈) → (𝐻𝑦) = 0)
123104, 122sylbir 225 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ ∧ ¬ 𝑦𝑈) → (𝐻𝑦) = 0)
124103, 123sylan 487 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝑈) → (𝐻𝑦) = 0)
125102, 124breqtrd 4711 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝑈) → (𝑓𝑦) ≤ 0)
12680, 125syldan 486 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ (¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵)) → (𝑓𝑦) ≤ 0)
127126anassrs 681 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ ¬ 𝑦𝐵) → (𝑓𝑦) ≤ 0)
12860adantl 481 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ ¬ 𝑦𝐵) → if(𝑦𝐵, (𝑓𝑦), 0) = 0)
129127, 128breqtrrd 4713 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ ¬ 𝑦𝐵) → (𝑓𝑦) ≤ if(𝑦𝐵, (𝑓𝑦), 0))
13071, 129pm2.61dan 849 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (𝑓𝑦) ≤ if(𝑦𝐵, (𝑓𝑦), 0))
131 iffalse 4128 . . . . . . . . . . . . 13 𝑦𝐴 → if(𝑦𝐴, (𝑓𝑦), 0) = 0)
132131adantl 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → if(𝑦𝐴, (𝑓𝑦), 0) = 0)
133132oveq1d 6705 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) = (0 + if(𝑦𝐵, (𝑓𝑦), 0)))
134 0re 10078 . . . . . . . . . . . . . . 15 0 ∈ ℝ
135 ifcl 4163 . . . . . . . . . . . . . . 15 (((𝑓𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑦𝐵, (𝑓𝑦), 0) ∈ ℝ)
13648, 134, 135sylancl 695 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → if(𝑦𝐵, (𝑓𝑦), 0) ∈ ℝ)
137136recnd 10106 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → if(𝑦𝐵, (𝑓𝑦), 0) ∈ ℂ)
138137adantr 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → if(𝑦𝐵, (𝑓𝑦), 0) ∈ ℂ)
139138addid2d 10275 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (0 + if(𝑦𝐵, (𝑓𝑦), 0)) = if(𝑦𝐵, (𝑓𝑦), 0))
140133, 139eqtrd 2685 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) = if(𝑦𝐵, (𝑓𝑦), 0))
141130, 140breqtrrd 4713 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (𝑓𝑦) ≤ (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
14267, 141pm2.61dan 849 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ≤ (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
143 eleq1 2718 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
144 fveq2 6229 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑓𝑥) = (𝑓𝑦))
145143, 144ifbieq1d 4142 . . . . . . . . . . 11 (𝑥 = 𝑦 → if(𝑥𝐴, (𝑓𝑥), 0) = if(𝑦𝐴, (𝑓𝑦), 0))
146 eleq1 2718 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
147146, 144ifbieq1d 4142 . . . . . . . . . . 11 (𝑥 = 𝑦 → if(𝑥𝐵, (𝑓𝑥), 0) = if(𝑦𝐵, (𝑓𝑦), 0))
148145, 147oveq12d 6708 . . . . . . . . . 10 (𝑥 = 𝑦 → (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)) = (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
149 eqid 2651 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))
150 ovex 6718 . . . . . . . . . 10 (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) ∈ V
151148, 149, 150fvmpt 6321 . . . . . . . . 9 (𝑦 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))‘𝑦) = (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
152103, 151syl 17 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))‘𝑦) = (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
153142, 152breqtrrd 4713 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ≤ ((𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))‘𝑦))
1541, 27, 29, 43, 153itg1lea 23524 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1𝑓) ≤ (∫1‘(𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))))
15541fveq2d 6233 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))) = (∫1‘(𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))))
1568, 15itg1add 23513 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))) = ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))))
157155, 156eqtr3d 2687 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))) = ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))))
158154, 157breqtrd 4711 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1𝑓) ≤ ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))))
15919adantr 480 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫2𝐹) ∈ ℝ)
16020adantr 480 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫2𝐺) ∈ ℝ)
161 ssun1 3809 . . . . . . . . . . . . . 14 𝐴 ⊆ (𝐴𝐵)
162161, 72syl5sseqr 3687 . . . . . . . . . . . . 13 (𝜑𝐴𝑈)
163162sselda 3636 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝑥𝑈)
164163adantlr 751 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝑥𝑈)
165164, 85syldan 486 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝐶 ∈ (0[,]+∞))
16686a1i 11 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐴) → 0 ∈ (0[,]+∞))
167165, 166ifclda 4153 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐴, 𝐶, 0) ∈ (0[,]+∞))
168 itg2split.f . . . . . . . . 9 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0))
169167, 168fmptd 6425 . . . . . . . 8 (𝜑𝐹:ℝ⟶(0[,]+∞))
170169adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐹:ℝ⟶(0[,]+∞))
171 nfv 1883 . . . . . . . . . 10 𝑥𝜑
172 nfv 1883 . . . . . . . . . . 11 𝑥 𝑓 ∈ dom ∫1
173 nfcv 2793 . . . . . . . . . . . 12 𝑥𝑓
174 nfcv 2793 . . . . . . . . . . . 12 𝑥𝑟
175173, 174, 107nfbr 4732 . . . . . . . . . . 11 𝑥 𝑓𝑟𝐻
176172, 175nfan 1868 . . . . . . . . . 10 𝑥(𝑓 ∈ dom ∫1𝑓𝑟𝐻)
177171, 176nfan 1868 . . . . . . . . 9 𝑥(𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻))
1785, 24syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐴 ⊆ ℝ)
179178sselda 3636 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → 𝑥 ∈ ℝ)
18030a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓 ∈ dom ∫1) → ℝ ∈ V)
18132a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ V)
18288adantlr 751 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
18344adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓 ∈ dom ∫1) → 𝑓:ℝ⟶ℝ)
184183feqmptd 6288 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓 ∈ dom ∫1) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
18589a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓 ∈ dom ∫1) → 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0)))
186180, 181, 182, 184, 185ofrfval2 6957 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓 ∈ dom ∫1) → (𝑓𝑟𝐻 ↔ ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0)))
187186biimpd 219 . . . . . . . . . . . . . . . 16 ((𝜑𝑓 ∈ dom ∫1) → (𝑓𝑟𝐻 → ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0)))
188187impr 648 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0))
189188r19.21bi 2961 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0))
190179, 189syldan 486 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0))
191163adantlr 751 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → 𝑥𝑈)
192191iftrued 4127 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → if(𝑥𝑈, 𝐶, 0) = 𝐶)
193190, 192breqtrd 4711 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ 𝐶)
194 iftrue 4125 . . . . . . . . . . . . 13 (𝑥𝐴 → if(𝑥𝐴, (𝑓𝑥), 0) = (𝑓𝑥))
195194adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → if(𝑥𝐴, (𝑓𝑥), 0) = (𝑓𝑥))
196 iftrue 4125 . . . . . . . . . . . . 13 (𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 𝐶)
197196adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → if(𝑥𝐴, 𝐶, 0) = 𝐶)
198193, 195, 1973brtr4d 4717 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
199 0le0 11148 . . . . . . . . . . . . . 14 0 ≤ 0
200199a1i 11 . . . . . . . . . . . . 13 𝑥𝐴 → 0 ≤ 0)
201 iffalse 4128 . . . . . . . . . . . . 13 𝑥𝐴 → if(𝑥𝐴, (𝑓𝑥), 0) = 0)
202 iffalse 4128 . . . . . . . . . . . . 13 𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 0)
203200, 201, 2023brtr4d 4717 . . . . . . . . . . . 12 𝑥𝐴 → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
204203adantl 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ ¬ 𝑥𝐴) → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
205198, 204pm2.61dan 849 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
206205a1d 25 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0)))
207177, 206ralrimi 2986 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ∀𝑥 ∈ ℝ if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
208168a1i 11 . . . . . . . . . 10 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0)))
20931, 35, 167, 38, 208ofrfval2 6957 . . . . . . . . 9 (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0)))
210209adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0)))
211207, 210mpbird 247 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑟𝐹)
212 itg2ub 23545 . . . . . . 7 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑟𝐹) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) ≤ (∫2𝐹))
213170, 8, 211, 212syl3anc 1366 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) ≤ (∫2𝐹))
214 ssun2 3810 . . . . . . . . . . . . . 14 𝐵 ⊆ (𝐴𝐵)
215214, 72syl5sseqr 3687 . . . . . . . . . . . . 13 (𝜑𝐵𝑈)
216215sselda 3636 . . . . . . . . . . . 12 ((𝜑𝑥𝐵) → 𝑥𝑈)
217216adantlr 751 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝑥𝑈)
218217, 85syldan 486 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝐶 ∈ (0[,]+∞))
21986a1i 11 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐵) → 0 ∈ (0[,]+∞))
220218, 219ifclda 4153 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐵, 𝐶, 0) ∈ (0[,]+∞))
221 itg2split.g . . . . . . . . 9 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0))
222220, 221fmptd 6425 . . . . . . . 8 (𝜑𝐺:ℝ⟶(0[,]+∞))
223222adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐺:ℝ⟶(0[,]+∞))
224 mblss 23345 . . . . . . . . . . . . . . . 16 (𝐵 ∈ dom vol → 𝐵 ⊆ ℝ)
22512, 224syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐵 ⊆ ℝ)
226225sselda 3636 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → 𝑥 ∈ ℝ)
227226, 189syldan 486 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0))
228216adantlr 751 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → 𝑥𝑈)
229228iftrued 4127 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → if(𝑥𝑈, 𝐶, 0) = 𝐶)
230227, 229breqtrd 4711 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → (𝑓𝑥) ≤ 𝐶)
231 iftrue 4125 . . . . . . . . . . . . 13 (𝑥𝐵 → if(𝑥𝐵, (𝑓𝑥), 0) = (𝑓𝑥))
232231adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → if(𝑥𝐵, (𝑓𝑥), 0) = (𝑓𝑥))
233 iftrue 4125 . . . . . . . . . . . . 13 (𝑥𝐵 → if(𝑥𝐵, 𝐶, 0) = 𝐶)
234233adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → if(𝑥𝐵, 𝐶, 0) = 𝐶)
235230, 232, 2343brtr4d 4717 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
236199a1i 11 . . . . . . . . . . . . 13 𝑥𝐵 → 0 ≤ 0)
237 iffalse 4128 . . . . . . . . . . . . 13 𝑥𝐵 → if(𝑥𝐵, (𝑓𝑥), 0) = 0)
238 iffalse 4128 . . . . . . . . . . . . 13 𝑥𝐵 → if(𝑥𝐵, 𝐶, 0) = 0)
239236, 237, 2383brtr4d 4717 . . . . . . . . . . . 12 𝑥𝐵 → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
240239adantl 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ ¬ 𝑥𝐵) → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
241235, 240pm2.61dan 849 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
242241a1d 25 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0)))
243177, 242ralrimi 2986 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ∀𝑥 ∈ ℝ if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
244221a1i 11 . . . . . . . . . 10 (𝜑𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0)))
24531, 37, 220, 39, 244ofrfval2 6957 . . . . . . . . 9 (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∘𝑟𝐺 ↔ ∀𝑥 ∈ ℝ if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0)))
246245adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∘𝑟𝐺 ↔ ∀𝑥 ∈ ℝ if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0)))
247243, 246mpbird 247 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∘𝑟𝐺)
248 itg2ub 23545 . . . . . . 7 ((𝐺:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∘𝑟𝐺) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ≤ (∫2𝐺))
249223, 15, 247, 248syl3anc 1366 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ≤ (∫2𝐺))
25010, 17, 159, 160, 213, 249le2addd 10684 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))) ≤ ((∫2𝐹) + (∫2𝐺)))
2513, 18, 22, 158, 250letrd 10232 . . . 4 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺)))
252251expr 642 . . 3 ((𝜑𝑓 ∈ dom ∫1) → (𝑓𝑟𝐻 → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺))))
253252ralrimiva 2995 . 2 (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐻 → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺))))
25421rexrd 10127 . . 3 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ*)
255 itg2leub 23546 . . 3 ((𝐻:ℝ⟶(0[,]+∞) ∧ ((∫2𝐹) + (∫2𝐺)) ∈ ℝ*) → ((∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐻 → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺)))))
25690, 254, 255syl2anc 694 . 2 (𝜑 → ((∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐻 → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺)))))
257253, 256mpbird 247 1 (𝜑 → (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030  wral 2941  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  ifcif 4119   class class class wbr 4685  cmpt 4762   I cid 5052  dom cdm 5143   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  𝑓 cof 6937  𝑟 cofr 6938  cc 9972  cr 9973  0cc0 9974   + caddc 9977  +∞cpnf 10109  *cxr 10111  cle 10113  [,]cicc 12216  vol*covol 23277  volcvol 23278  1citg1 23429  2citg2 23430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-ofr 6940  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-rest 16130  df-topgen 16151  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-top 20747  df-topon 20764  df-bases 20798  df-cmp 21238  df-ovol 23279  df-vol 23280  df-mbf 23433  df-itg1 23434  df-itg2 23435
This theorem is referenced by:  itg2split  23561
  Copyright terms: Public domain W3C validator