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

Theorem itg2split 23807
Description: The 2 integral splits under an almost disjoint union. (The proof avoids the use of itg2add 23817 which requires CC.) (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
itg2split (𝜑 → (∫2𝐻) = ((∫2𝐹) + (∫2𝐺)))
Distinct variable groups:   𝜑,𝑥   𝑥,𝐴   𝑥,𝐵   𝑥,𝑈
Allowed substitution hints:   𝐶(𝑥)   𝐹(𝑥)   𝐺(𝑥)   𝐻(𝑥)

Proof of Theorem itg2split
Dummy variables 𝑓 𝑔 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itg2split.a . . 3 (𝜑𝐴 ∈ dom vol)
2 itg2split.b . . 3 (𝜑𝐵 ∈ dom vol)
3 itg2split.i . . 3 (𝜑 → (vol*‘(𝐴𝐵)) = 0)
4 itg2split.u . . 3 (𝜑𝑈 = (𝐴𝐵))
5 itg2split.c . . 3 ((𝜑𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
6 itg2split.f . . 3 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0))
7 itg2split.g . . 3 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0))
8 itg2split.h . . 3 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
9 itg2split.sf . . 3 (𝜑 → (∫2𝐹) ∈ ℝ)
10 itg2split.sg . . 3 (𝜑 → (∫2𝐺) ∈ ℝ)
111, 2, 3, 4, 5, 6, 7, 8, 9, 10itg2splitlem 23806 . 2 (𝜑 → (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)))
1210adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → (∫2𝐺) ∈ ℝ)
135adantlr 706 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
14 0e0iccpnf 12487 . . . . . . . . . . . 12 0 ∈ (0[,]+∞)
1514a1i 11 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝑈) → 0 ∈ (0[,]+∞))
1613, 15ifclda 4277 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
1716, 8fmptd 6574 . . . . . . . . 9 (𝜑𝐻:ℝ⟶(0[,]+∞))
189, 10readdcld 10323 . . . . . . . . 9 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ)
19 itg2lecl 23796 . . . . . . . . 9 ((𝐻:ℝ⟶(0[,]+∞) ∧ ((∫2𝐹) + (∫2𝐺)) ∈ ℝ ∧ (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺))) → (∫2𝐻) ∈ ℝ)
2017, 18, 11, 19syl3anc 1490 . . . . . . . 8 (𝜑 → (∫2𝐻) ∈ ℝ)
2120adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → (∫2𝐻) ∈ ℝ)
22 itg1cl 23743 . . . . . . . 8 (𝑓 ∈ dom ∫1 → (∫1𝑓) ∈ ℝ)
2322ad2antrl 719 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → (∫1𝑓) ∈ ℝ)
24 simprll 797 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑓 ∈ dom ∫1)
25 simprrl 799 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑔 ∈ dom ∫1)
2624, 25itg1add 23759 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (∫1‘(𝑓𝑓 + 𝑔)) = ((∫1𝑓) + (∫1𝑔)))
2717adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝐻:ℝ⟶(0[,]+∞))
2824, 25i1fadd 23753 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (𝑓𝑓 + 𝑔) ∈ dom ∫1)
29 inss1 3992 . . . . . . . . . . . . . . . 16 (𝐴𝐵) ⊆ 𝐴
30 mblss 23589 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
311, 30syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ⊆ ℝ)
3229, 31syl5ss 3772 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐵) ⊆ ℝ)
3332adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (𝐴𝐵) ⊆ ℝ)
343adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (vol*‘(𝐴𝐵)) = 0)
35 nfv 2009 . . . . . . . . . . . . . . . . . 18 𝑥𝜑
36 nfv 2009 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑓 ∈ dom ∫1
37 nfcv 2907 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑓
38 nfcv 2907 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑟
39 nfmpt1 4906 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0))
406, 39nfcxfr 2905 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐹
4137, 38, 40nfbr 4856 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑓𝑟𝐹
4236, 41nfan 1998 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑓 ∈ dom ∫1𝑓𝑟𝐹)
43 nfv 2009 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑔 ∈ dom ∫1
44 nfcv 2907 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑔
45 nfmpt1 4906 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0))
467, 45nfcxfr 2905 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐺
4744, 38, 46nfbr 4856 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑔𝑟𝐺
4843, 47nfan 1998 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑔 ∈ dom ∫1𝑔𝑟𝐺)
4942, 48nfan 1998 . . . . . . . . . . . . . . . . . 18 𝑥((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))
5035, 49nfan 1998 . . . . . . . . . . . . . . . . 17 𝑥(𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺)))
51 eldifi 3894 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → 𝑥 ∈ ℝ)
52 i1ff 23734 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
5324, 52syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑓:ℝ⟶ℝ)
5453ffnd 6224 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑓 Fn ℝ)
55 i1ff 23734 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
5625, 55syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑔:ℝ⟶ℝ)
5756ffnd 6224 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑔 Fn ℝ)
58 reex 10280 . . . . . . . . . . . . . . . . . . . . . 22 ℝ ∈ V
5958a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → ℝ ∈ V)
60 inidm 3982 . . . . . . . . . . . . . . . . . . . . 21 (ℝ ∩ ℝ) = ℝ
61 eqidd 2766 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) = (𝑓𝑥))
62 eqidd 2766 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) = (𝑔𝑥))
6354, 57, 59, 59, 60, 61, 62ofval 7104 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → ((𝑓𝑓 + 𝑔)‘𝑥) = ((𝑓𝑥) + (𝑔𝑥)))
6451, 63sylan2 586 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑓 + 𝑔)‘𝑥) = ((𝑓𝑥) + (𝑔𝑥)))
65 ffvelrn 6547 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ ℝ)
6653, 51, 65syl2an 589 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑥) ∈ ℝ)
67 ffvelrn 6547 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℝ)
6856, 51, 67syl2an 589 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑔𝑥) ∈ ℝ)
6966, 68readdcld 10323 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ)
7069rexrd 10343 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ*)
7170adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ*)
7266adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℝ)
7372rexrd 10343 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℝ*)
74 iccssxr 12458 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,]+∞) ⊆ ℝ*
75 ffvelrn 6547 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐻:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝐻𝑥) ∈ (0[,]+∞))
7627, 51, 75syl2an 589 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝐻𝑥) ∈ (0[,]+∞))
7774, 76sseldi 3759 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝐻𝑥) ∈ ℝ*)
7877adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝐻𝑥) ∈ ℝ*)
7968adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑔𝑥) ∈ ℝ)
80 0red 10297 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → 0 ∈ ℝ)
81 simprrr 800 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑔𝑟𝐺)
8258a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → ℝ ∈ V)
83 fvexd 6390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ∈ V)
84 ssun2 3939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝐵 ⊆ (𝐴𝐵)
8584, 4syl5sseqr 3814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑𝐵𝑈)
8685sselda 3761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑥𝐵) → 𝑥𝑈)
8786adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝑥𝑈)
8887, 13syldan 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝐶 ∈ (0[,]+∞))
8914a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐵) → 0 ∈ (0[,]+∞))
9088, 89ifclda 4277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐵, 𝐶, 0) ∈ (0[,]+∞))
9190adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥𝐵, 𝐶, 0) ∈ (0[,]+∞))
92 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑔 Fn ℝ) → 𝑔 Fn ℝ)
93 dffn5 6430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑔 Fn ℝ ↔ 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔𝑥)))
9492, 93sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔𝑥)))
957a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0)))
9682, 83, 91, 94, 95ofrfval2 7113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑔 Fn ℝ) → (𝑔𝑟𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0)))
9757, 96syldan 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (𝑔𝑟𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0)))
9881, 97mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
9998r19.21bi 3079 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
10051, 99sylan2 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
101100adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
102 eldifn 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → ¬ 𝑥 ∈ (𝐴𝐵))
103102adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ 𝑥 ∈ (𝐴𝐵))
104 elin 3958 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
105103, 104sylnib 319 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ (𝑥𝐴𝑥𝐵))
106 imnan 388 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ ¬ (𝑥𝐴𝑥𝐵))
107105, 106sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑥𝐴 → ¬ 𝑥𝐵))
108107imp 395 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ¬ 𝑥𝐵)
109108iffalsed 4254 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝐵, 𝐶, 0) = 0)
110101, 109breqtrd 4835 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑔𝑥) ≤ 0)
11179, 80, 72, 110leadd2dd 10896 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ ((𝑓𝑥) + 0))
11272recnd 10322 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℂ)
113112addid1d 10490 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + 0) = (𝑓𝑥))
114111, 113breqtrd 4835 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝑓𝑥))
115 simprlr 798 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑓𝑟𝐹)
11658a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → ℝ ∈ V)
117 fvexd 6390 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ V)
118 ssun1 3938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝐴 ⊆ (𝐴𝐵)
119118, 4syl5sseqr 3814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐴𝑈)
120119sselda 3761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑥𝐴) → 𝑥𝑈)
121120adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝑥𝑈)
122121, 13syldan 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝐶 ∈ (0[,]+∞))
12314a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐴) → 0 ∈ (0[,]+∞))
124122, 123ifclda 4277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐴, 𝐶, 0) ∈ (0[,]+∞))
125124adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥𝐴, 𝐶, 0) ∈ (0[,]+∞))
126 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑓 Fn ℝ) → 𝑓 Fn ℝ)
127 dffn5 6430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 Fn ℝ ↔ 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
128126, 127sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
1296a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0)))
130116, 117, 125, 128, 129ofrfval2 7113 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 Fn ℝ) → (𝑓𝑟𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0)))
13154, 130syldan 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (𝑓𝑟𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0)))
132115, 131mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
133132r19.21bi 3079 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
13451, 133sylan2 586 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
135134adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
136119ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → 𝐴𝑈)
137136sselda 3761 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → 𝑥𝑈)
138137iftrued 4251 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝑈, 𝐶, 0) = 𝐶)
139 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
14016adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
1418fvmpt2 6480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ ℝ ∧ if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞)) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
142139, 140, 141syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
14351, 142sylan2 586 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
144143adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
145 iftrue 4249 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 𝐶)
146145adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝐴, 𝐶, 0) = 𝐶)
147138, 144, 1463eqtr4d 2809 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝐴, 𝐶, 0))
148135, 147breqtrrd 4837 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ (𝐻𝑥))
14971, 73, 78, 114, 148xrletrd 12195 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝐻𝑥))
15070adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ*)
15168adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ∈ ℝ)
152151rexrd 10343 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ∈ ℝ*)
15377adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝐻𝑥) ∈ ℝ*)
15466adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑓𝑥) ∈ ℝ)
155 0red 10297 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → 0 ∈ ℝ)
156134adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
157 iffalse 4252 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 0)
158157adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → if(𝑥𝐴, 𝐶, 0) = 0)
159156, 158breqtrd 4835 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑓𝑥) ≤ 0)
160154, 155, 151, 159leadd1dd 10895 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (0 + (𝑔𝑥)))
161151recnd 10322 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ∈ ℂ)
162161addid2d 10491 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (0 + (𝑔𝑥)) = (𝑔𝑥))
163160, 162breqtrd 4835 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝑔𝑥))
164100adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
165143adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
1664ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → 𝑈 = (𝐴𝐵))
167166eleq2d 2830 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑥𝑈𝑥 ∈ (𝐴𝐵)))
168 biorf 960 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥𝐴 → (𝑥𝐵 ↔ (𝑥𝐴𝑥𝐵)))
169 elun 3915 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
170168, 169syl6rbbr 281 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥𝐴 → (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
171170adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
172167, 171bitrd 270 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑥𝑈𝑥𝐵))
173172ifbid 4265 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → if(𝑥𝑈, 𝐶, 0) = if(𝑥𝐵, 𝐶, 0))
174165, 173eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝐵, 𝐶, 0))
175164, 174breqtrrd 4837 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ≤ (𝐻𝑥))
176150, 152, 153, 163, 175xrletrd 12195 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝐻𝑥))
177149, 176pm2.61dan 847 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝐻𝑥))
17864, 177eqbrtrd 4831 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑓 + 𝑔)‘𝑥) ≤ (𝐻𝑥))
179178ex 401 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → ((𝑓𝑓 + 𝑔)‘𝑥) ≤ (𝐻𝑥)))
18050, 179ralrimi 3104 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → ∀𝑥 ∈ (ℝ ∖ (𝐴𝐵))((𝑓𝑓 + 𝑔)‘𝑥) ≤ (𝐻𝑥))
181 nfv 2009 . . . . . . . . . . . . . . . . 17 𝑦((𝑓𝑓 + 𝑔)‘𝑥) ≤ (𝐻𝑥)
182 nfcv 2907 . . . . . . . . . . . . . . . . . 18 𝑥((𝑓𝑓 + 𝑔)‘𝑦)
183 nfcv 2907 . . . . . . . . . . . . . . . . . 18 𝑥
184 nfmpt1 4906 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
1858, 184nfcxfr 2905 . . . . . . . . . . . . . . . . . . 19 𝑥𝐻
186 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑥𝑦
187185, 186nffv 6385 . . . . . . . . . . . . . . . . . 18 𝑥(𝐻𝑦)
188182, 183, 187nfbr 4856 . . . . . . . . . . . . . . . . 17 𝑥((𝑓𝑓 + 𝑔)‘𝑦) ≤ (𝐻𝑦)
189 fveq2 6375 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝑓𝑓 + 𝑔)‘𝑥) = ((𝑓𝑓 + 𝑔)‘𝑦))
190 fveq2 6375 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
191189, 190breq12d 4822 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (((𝑓𝑓 + 𝑔)‘𝑥) ≤ (𝐻𝑥) ↔ ((𝑓𝑓 + 𝑔)‘𝑦) ≤ (𝐻𝑦)))
192181, 188, 191cbvral 3315 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ (ℝ ∖ (𝐴𝐵))((𝑓𝑓 + 𝑔)‘𝑥) ≤ (𝐻𝑥) ↔ ∀𝑦 ∈ (ℝ ∖ (𝐴𝐵))((𝑓𝑓 + 𝑔)‘𝑦) ≤ (𝐻𝑦))
193180, 192sylib 209 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → ∀𝑦 ∈ (ℝ ∖ (𝐴𝐵))((𝑓𝑓 + 𝑔)‘𝑦) ≤ (𝐻𝑦))
194193r19.21bi 3079 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑓 + 𝑔)‘𝑦) ≤ (𝐻𝑦))
19527, 28, 33, 34, 194itg2uba 23801 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (∫1‘(𝑓𝑓 + 𝑔)) ≤ (∫2𝐻))
19626, 195eqbrtrrd 4833 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → ((∫1𝑓) + (∫1𝑔)) ≤ (∫2𝐻))
19723adantrr 708 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (∫1𝑓) ∈ ℝ)
198 itg1cl 23743 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → (∫1𝑔) ∈ ℝ)
19925, 198syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (∫1𝑔) ∈ ℝ)
20020adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (∫2𝐻) ∈ ℝ)
201197, 199, 200leaddsub2d 10883 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (((∫1𝑓) + (∫1𝑔)) ≤ (∫2𝐻) ↔ (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓))))
202196, 201mpbid 223 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))
203202anassrs 459 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺)) → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))
204203expr 448 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) ∧ 𝑔 ∈ dom ∫1) → (𝑔𝑟𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓))))
205204ralrimiva 3113 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → ∀𝑔 ∈ dom ∫1(𝑔𝑟𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓))))
20690, 7fmptd 6574 . . . . . . . . . 10 (𝜑𝐺:ℝ⟶(0[,]+∞))
207206adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → 𝐺:ℝ⟶(0[,]+∞))
20821, 23resubcld 10712 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → ((∫2𝐻) − (∫1𝑓)) ∈ ℝ)
209208rexrd 10343 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → ((∫2𝐻) − (∫1𝑓)) ∈ ℝ*)
210 itg2leub 23792 . . . . . . . . 9 ((𝐺:ℝ⟶(0[,]+∞) ∧ ((∫2𝐻) − (∫1𝑓)) ∈ ℝ*) → ((∫2𝐺) ≤ ((∫2𝐻) − (∫1𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔𝑟𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))))
211207, 209, 210syl2anc 579 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → ((∫2𝐺) ≤ ((∫2𝐻) − (∫1𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔𝑟𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))))
212205, 211mpbird 248 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → (∫2𝐺) ≤ ((∫2𝐻) − (∫1𝑓)))
21312, 21, 23, 212lesubd 10885 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺)))
214213expr 448 . . . . 5 ((𝜑𝑓 ∈ dom ∫1) → (𝑓𝑟𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺))))
215214ralrimiva 3113 . . . 4 (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺))))
216124, 6fmptd 6574 . . . . 5 (𝜑𝐹:ℝ⟶(0[,]+∞))
21720, 10resubcld 10712 . . . . . 6 (𝜑 → ((∫2𝐻) − (∫2𝐺)) ∈ ℝ)
218217rexrd 10343 . . . . 5 (𝜑 → ((∫2𝐻) − (∫2𝐺)) ∈ ℝ*)
219 itg2leub 23792 . . . . 5 ((𝐹:ℝ⟶(0[,]+∞) ∧ ((∫2𝐻) − (∫2𝐺)) ∈ ℝ*) → ((∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺)))))
220216, 218, 219syl2anc 579 . . . 4 (𝜑 → ((∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺)))))
221215, 220mpbird 248 . . 3 (𝜑 → (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺)))
222 leaddsub 10758 . . . 4 (((∫2𝐹) ∈ ℝ ∧ (∫2𝐺) ∈ ℝ ∧ (∫2𝐻) ∈ ℝ) → (((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻) ↔ (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺))))
2239, 10, 20, 222syl3anc 1490 . . 3 (𝜑 → (((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻) ↔ (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺))))
224221, 223mpbird 248 . 2 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻))
225 itg2cl 23790 . . . 4 (𝐻:ℝ⟶(0[,]+∞) → (∫2𝐻) ∈ ℝ*)
22617, 225syl 17 . . 3 (𝜑 → (∫2𝐻) ∈ ℝ*)
22718rexrd 10343 . . 3 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ*)
228 xrletri3 12187 . . 3 (((∫2𝐻) ∈ ℝ* ∧ ((∫2𝐹) + (∫2𝐺)) ∈ ℝ*) → ((∫2𝐻) = ((∫2𝐹) + (∫2𝐺)) ↔ ((∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)) ∧ ((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻))))
229226, 227, 228syl2anc 579 . 2 (𝜑 → ((∫2𝐻) = ((∫2𝐹) + (∫2𝐺)) ↔ ((∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)) ∧ ((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻))))
23011, 224, 229mpbir2and 704 1 (𝜑 → (∫2𝐻) = ((∫2𝐹) + (∫2𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873   = wceq 1652  wcel 2155  wral 3055  Vcvv 3350  cdif 3729  cun 3730  cin 3731  wss 3732  ifcif 4243   class class class wbr 4809  cmpt 4888  dom cdm 5277   Fn wfn 6063  wf 6064  cfv 6068  (class class class)co 6842  𝑓 cof 7093  𝑟 cofr 7094  cr 10188  0cc0 10189   + caddc 10192  +∞cpnf 10325  *cxr 10327  cle 10329  cmin 10520  [,]cicc 12380  vol*covol 23520  volcvol 23521  1citg1 23673  2citg2 23674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-disj 4778  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-ofr 7096  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ioo 12381  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-clim 14506  df-sum 14704  df-rest 16351  df-topgen 16372  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-top 20978  df-topon 20995  df-bases 21030  df-cmp 21470  df-ovol 23522  df-vol 23523  df-mbf 23677  df-itg1 23678  df-itg2 23679
This theorem is referenced by:  itg2cnlem2  23820  itgsplit  23893  iblsplit  40751
  Copyright terms: Public domain W3C validator