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

Theorem itg2split 24033
Description: The 2 integral splits under an almost disjoint union. (The proof avoids the use of itg2add 24043 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.c . . . . . 6 ((𝜑𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
21adantlr 711 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
3 0e0iccpnf 12697 . . . . . 6 0 ∈ (0[,]+∞)
43a1i 11 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝑈) → 0 ∈ (0[,]+∞))
52, 4ifclda 4415 . . . 4 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
6 itg2split.h . . . 4 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
75, 6fmptd 6741 . . 3 (𝜑𝐻:ℝ⟶(0[,]+∞))
8 itg2cl 24016 . . 3 (𝐻:ℝ⟶(0[,]+∞) → (∫2𝐻) ∈ ℝ*)
97, 8syl 17 . 2 (𝜑 → (∫2𝐻) ∈ ℝ*)
10 itg2split.sf . . . 4 (𝜑 → (∫2𝐹) ∈ ℝ)
11 itg2split.sg . . . 4 (𝜑 → (∫2𝐺) ∈ ℝ)
1210, 11readdcld 10516 . . 3 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ)
1312rexrd 10537 . 2 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ*)
14 itg2split.a . . 3 (𝜑𝐴 ∈ dom vol)
15 itg2split.b . . 3 (𝜑𝐵 ∈ dom vol)
16 itg2split.i . . 3 (𝜑 → (vol*‘(𝐴𝐵)) = 0)
17 itg2split.u . . 3 (𝜑𝑈 = (𝐴𝐵))
18 itg2split.f . . 3 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0))
19 itg2split.g . . 3 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0))
2014, 15, 16, 17, 1, 18, 19, 6, 10, 11itg2splitlem 24032 . 2 (𝜑 → (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)))
2111adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → (∫2𝐺) ∈ ℝ)
22 itg2lecl 24022 . . . . . . . . 9 ((𝐻:ℝ⟶(0[,]+∞) ∧ ((∫2𝐹) + (∫2𝐺)) ∈ ℝ ∧ (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺))) → (∫2𝐻) ∈ ℝ)
237, 12, 20, 22syl3anc 1364 . . . . . . . 8 (𝜑 → (∫2𝐻) ∈ ℝ)
2423adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → (∫2𝐻) ∈ ℝ)
25 itg1cl 23969 . . . . . . . 8 (𝑓 ∈ dom ∫1 → (∫1𝑓) ∈ ℝ)
2625ad2antrl 724 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → (∫1𝑓) ∈ ℝ)
27 simprll 775 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑓 ∈ dom ∫1)
28 simprrl 777 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑔 ∈ dom ∫1)
2927, 28itg1add 23985 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (∫1‘(𝑓𝑓 + 𝑔)) = ((∫1𝑓) + (∫1𝑔)))
307adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝐻:ℝ⟶(0[,]+∞))
3127, 28i1fadd 23979 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (𝑓𝑓 + 𝑔) ∈ dom ∫1)
32 inss1 4125 . . . . . . . . . . . . . . . 16 (𝐴𝐵) ⊆ 𝐴
33 mblss 23815 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
3414, 33syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ⊆ ℝ)
3532, 34syl5ss 3900 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐵) ⊆ ℝ)
3635adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (𝐴𝐵) ⊆ ℝ)
3716adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (vol*‘(𝐴𝐵)) = 0)
38 nfv 1892 . . . . . . . . . . . . . . . . . 18 𝑥𝜑
39 nfv 1892 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑓 ∈ dom ∫1
40 nfcv 2949 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑓
41 nfcv 2949 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑟
42 nfmpt1 5058 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0))
4318, 42nfcxfr 2947 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐹
4440, 41, 43nfbr 5009 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑓𝑟𝐹
4539, 44nfan 1881 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑓 ∈ dom ∫1𝑓𝑟𝐹)
46 nfv 1892 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑔 ∈ dom ∫1
47 nfcv 2949 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑔
48 nfmpt1 5058 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0))
4919, 48nfcxfr 2947 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐺
5047, 41, 49nfbr 5009 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑔𝑟𝐺
5146, 50nfan 1881 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑔 ∈ dom ∫1𝑔𝑟𝐺)
5245, 51nfan 1881 . . . . . . . . . . . . . . . . . 18 𝑥((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))
5338, 52nfan 1881 . . . . . . . . . . . . . . . . 17 𝑥(𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺)))
54 eldifi 4024 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → 𝑥 ∈ ℝ)
55 i1ff 23960 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
5627, 55syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑓:ℝ⟶ℝ)
5756ffnd 6383 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑓 Fn ℝ)
58 i1ff 23960 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
5928, 58syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑔:ℝ⟶ℝ)
6059ffnd 6383 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑔 Fn ℝ)
61 reex 10474 . . . . . . . . . . . . . . . . . . . . . 22 ℝ ∈ V
6261a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → ℝ ∈ V)
63 inidm 4115 . . . . . . . . . . . . . . . . . . . . 21 (ℝ ∩ ℝ) = ℝ
64 eqidd 2796 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) = (𝑓𝑥))
65 eqidd 2796 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) = (𝑔𝑥))
6657, 60, 62, 62, 63, 64, 65ofval 7276 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → ((𝑓𝑓 + 𝑔)‘𝑥) = ((𝑓𝑥) + (𝑔𝑥)))
6754, 66sylan2 592 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑓 + 𝑔)‘𝑥) = ((𝑓𝑥) + (𝑔𝑥)))
68 ffvelrn 6714 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ ℝ)
6956, 54, 68syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑥) ∈ ℝ)
70 ffvelrn 6714 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℝ)
7159, 54, 70syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑔𝑥) ∈ ℝ)
7269, 71readdcld 10516 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ)
7372rexrd 10537 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ*)
7473adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ*)
7569adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℝ)
7675rexrd 10537 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℝ*)
77 iccssxr 12669 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,]+∞) ⊆ ℝ*
78 ffvelrn 6714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐻:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝐻𝑥) ∈ (0[,]+∞))
7930, 54, 78syl2an 595 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝐻𝑥) ∈ (0[,]+∞))
8077, 79sseldi 3887 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝐻𝑥) ∈ ℝ*)
8180adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝐻𝑥) ∈ ℝ*)
8271adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑔𝑥) ∈ ℝ)
83 0red 10490 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → 0 ∈ ℝ)
84 simprrr 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑔𝑟𝐺)
8561a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → ℝ ∈ V)
86 fvexd 6553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ∈ V)
87 ssun2 4070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝐵 ⊆ (𝐴𝐵)
8887, 17sseqtrrid 3941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑𝐵𝑈)
8988sselda 3889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑥𝐵) → 𝑥𝑈)
9089adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝑥𝑈)
9190, 2syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝐶 ∈ (0[,]+∞))
923a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐵) → 0 ∈ (0[,]+∞))
9391, 92ifclda 4415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐵, 𝐶, 0) ∈ (0[,]+∞))
9493adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥𝐵, 𝐶, 0) ∈ (0[,]+∞))
95 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑔 Fn ℝ) → 𝑔 Fn ℝ)
96 dffn5 6592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑔 Fn ℝ ↔ 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔𝑥)))
9795, 96sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔𝑥)))
9819a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0)))
9985, 86, 94, 97, 98ofrfval2 7285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑔 Fn ℝ) → (𝑔𝑟𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0)))
10060, 99syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (𝑔𝑟𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0)))
10184, 100mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
102101r19.21bi 3175 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
10354, 102sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
104103adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
105 eldifn 4025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → ¬ 𝑥 ∈ (𝐴𝐵))
106105adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ 𝑥 ∈ (𝐴𝐵))
107 elin 4090 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
108106, 107sylnib 329 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ (𝑥𝐴𝑥𝐵))
109 imnan 400 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ ¬ (𝑥𝐴𝑥𝐵))
110108, 109sylibr 235 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑥𝐴 → ¬ 𝑥𝐵))
111110imp 407 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ¬ 𝑥𝐵)
112111iffalsed 4392 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝐵, 𝐶, 0) = 0)
113104, 112breqtrd 4988 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑔𝑥) ≤ 0)
11482, 83, 75, 113leadd2dd 11103 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ ((𝑓𝑥) + 0))
11575recnd 10515 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℂ)
116115addid1d 10687 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + 0) = (𝑓𝑥))
117114, 116breqtrd 4988 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝑓𝑥))
118 simprlr 776 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → 𝑓𝑟𝐹)
11961a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → ℝ ∈ V)
120 fvexd 6553 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ V)
121 ssun1 4069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝐴 ⊆ (𝐴𝐵)
122121, 17sseqtrrid 3941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐴𝑈)
123122sselda 3889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑥𝐴) → 𝑥𝑈)
124123adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝑥𝑈)
125124, 2syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝐶 ∈ (0[,]+∞))
1263a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐴) → 0 ∈ (0[,]+∞))
127125, 126ifclda 4415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐴, 𝐶, 0) ∈ (0[,]+∞))
128127adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥𝐴, 𝐶, 0) ∈ (0[,]+∞))
129 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑓 Fn ℝ) → 𝑓 Fn ℝ)
130 dffn5 6592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 Fn ℝ ↔ 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
131129, 130sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
13218a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0)))
133119, 120, 128, 131, 132ofrfval2 7285 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 Fn ℝ) → (𝑓𝑟𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0)))
13457, 133syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (𝑓𝑟𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0)))
135118, 134mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
136135r19.21bi 3175 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
13754, 136sylan2 592 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
138137adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
139122ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → 𝐴𝑈)
140139sselda 3889 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → 𝑥𝑈)
141140iftrued 4389 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝑈, 𝐶, 0) = 𝐶)
142 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
1435adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
1446fvmpt2 6645 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ ℝ ∧ if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞)) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
145142, 143, 144syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ ℝ) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
14654, 145sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
147146adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
148 iftrue 4387 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 𝐶)
149148adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝐴, 𝐶, 0) = 𝐶)
150141, 147, 1493eqtr4d 2841 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝐴, 𝐶, 0))
151138, 150breqtrrd 4990 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ (𝐻𝑥))
15274, 76, 81, 117, 151xrletrd 12405 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝐻𝑥))
15373adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ*)
15471adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ∈ ℝ)
155154rexrd 10537 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ∈ ℝ*)
15680adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝐻𝑥) ∈ ℝ*)
15769adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑓𝑥) ∈ ℝ)
158 0red 10490 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → 0 ∈ ℝ)
159137adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
160 iffalse 4390 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 0)
161160adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → if(𝑥𝐴, 𝐶, 0) = 0)
162159, 161breqtrd 4988 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑓𝑥) ≤ 0)
163157, 158, 154, 162leadd1dd 11102 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (0 + (𝑔𝑥)))
164154recnd 10515 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ∈ ℂ)
165164addid2d 10688 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (0 + (𝑔𝑥)) = (𝑔𝑥))
166163, 165breqtrd 4988 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝑔𝑥))
167103adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
168146adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
16917ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → 𝑈 = (𝐴𝐵))
170169eleq2d 2868 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑥𝑈𝑥 ∈ (𝐴𝐵)))
171 biorf 931 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥𝐴 → (𝑥𝐵 ↔ (𝑥𝐴𝑥𝐵)))
172 elun 4046 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
173171, 172syl6rbbr 291 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥𝐴 → (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
174173adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
175170, 174bitrd 280 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑥𝑈𝑥𝐵))
176175ifbid 4403 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → if(𝑥𝑈, 𝐶, 0) = if(𝑥𝐵, 𝐶, 0))
177168, 176eqtrd 2831 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝐵, 𝐶, 0))
178167, 177breqtrrd 4990 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ≤ (𝐻𝑥))
179153, 155, 156, 166, 178xrletrd 12405 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝐻𝑥))
180152, 179pm2.61dan 809 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝐻𝑥))
18167, 180eqbrtrd 4984 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑓 + 𝑔)‘𝑥) ≤ (𝐻𝑥))
182181ex 413 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → ((𝑓𝑓 + 𝑔)‘𝑥) ≤ (𝐻𝑥)))
18353, 182ralrimi 3183 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → ∀𝑥 ∈ (ℝ ∖ (𝐴𝐵))((𝑓𝑓 + 𝑔)‘𝑥) ≤ (𝐻𝑥))
184 nfv 1892 . . . . . . . . . . . . . . . . 17 𝑦((𝑓𝑓 + 𝑔)‘𝑥) ≤ (𝐻𝑥)
185 nfcv 2949 . . . . . . . . . . . . . . . . . 18 𝑥((𝑓𝑓 + 𝑔)‘𝑦)
186 nfcv 2949 . . . . . . . . . . . . . . . . . 18 𝑥
187 nfmpt1 5058 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
1886, 187nfcxfr 2947 . . . . . . . . . . . . . . . . . . 19 𝑥𝐻
189 nfcv 2949 . . . . . . . . . . . . . . . . . . 19 𝑥𝑦
190188, 189nffv 6548 . . . . . . . . . . . . . . . . . 18 𝑥(𝐻𝑦)
191185, 186, 190nfbr 5009 . . . . . . . . . . . . . . . . 17 𝑥((𝑓𝑓 + 𝑔)‘𝑦) ≤ (𝐻𝑦)
192 fveq2 6538 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝑓𝑓 + 𝑔)‘𝑥) = ((𝑓𝑓 + 𝑔)‘𝑦))
193 fveq2 6538 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
194192, 193breq12d 4975 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (((𝑓𝑓 + 𝑔)‘𝑥) ≤ (𝐻𝑥) ↔ ((𝑓𝑓 + 𝑔)‘𝑦) ≤ (𝐻𝑦)))
195184, 191, 194cbvral 3399 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ (ℝ ∖ (𝐴𝐵))((𝑓𝑓 + 𝑔)‘𝑥) ≤ (𝐻𝑥) ↔ ∀𝑦 ∈ (ℝ ∖ (𝐴𝐵))((𝑓𝑓 + 𝑔)‘𝑦) ≤ (𝐻𝑦))
196183, 195sylib 219 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → ∀𝑦 ∈ (ℝ ∖ (𝐴𝐵))((𝑓𝑓 + 𝑔)‘𝑦) ≤ (𝐻𝑦))
197196r19.21bi 3175 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑓 + 𝑔)‘𝑦) ≤ (𝐻𝑦))
19830, 31, 36, 37, 197itg2uba 24027 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (∫1‘(𝑓𝑓 + 𝑔)) ≤ (∫2𝐻))
19929, 198eqbrtrrd 4986 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → ((∫1𝑓) + (∫1𝑔)) ≤ (∫2𝐻))
20026adantrr 713 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (∫1𝑓) ∈ ℝ)
201 itg1cl 23969 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → (∫1𝑔) ∈ ℝ)
20228, 201syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (∫1𝑔) ∈ ℝ)
20323adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (∫2𝐻) ∈ ℝ)
204200, 202, 203leaddsub2d 11090 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (((∫1𝑓) + (∫1𝑔)) ≤ (∫2𝐻) ↔ (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓))))
205199, 204mpbid 233 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓𝑟𝐹) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺))) → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))
206205anassrs 468 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) ∧ (𝑔 ∈ dom ∫1𝑔𝑟𝐺)) → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))
207206expr 457 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) ∧ 𝑔 ∈ dom ∫1) → (𝑔𝑟𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓))))
208207ralrimiva 3149 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → ∀𝑔 ∈ dom ∫1(𝑔𝑟𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓))))
20993, 19fmptd 6741 . . . . . . . . . 10 (𝜑𝐺:ℝ⟶(0[,]+∞))
210209adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → 𝐺:ℝ⟶(0[,]+∞))
21124, 26resubcld 10916 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → ((∫2𝐻) − (∫1𝑓)) ∈ ℝ)
212211rexrd 10537 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → ((∫2𝐻) − (∫1𝑓)) ∈ ℝ*)
213 itg2leub 24018 . . . . . . . . 9 ((𝐺:ℝ⟶(0[,]+∞) ∧ ((∫2𝐻) − (∫1𝑓)) ∈ ℝ*) → ((∫2𝐺) ≤ ((∫2𝐻) − (∫1𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔𝑟𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))))
214210, 212, 213syl2anc 584 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → ((∫2𝐺) ≤ ((∫2𝐻) − (∫1𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔𝑟𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))))
215208, 214mpbird 258 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → (∫2𝐺) ≤ ((∫2𝐻) − (∫1𝑓)))
21621, 24, 26, 215lesubd 11092 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐹)) → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺)))
217216expr 457 . . . . 5 ((𝜑𝑓 ∈ dom ∫1) → (𝑓𝑟𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺))))
218217ralrimiva 3149 . . . 4 (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺))))
219127, 18fmptd 6741 . . . . 5 (𝜑𝐹:ℝ⟶(0[,]+∞))
22023, 11resubcld 10916 . . . . . 6 (𝜑 → ((∫2𝐻) − (∫2𝐺)) ∈ ℝ)
221220rexrd 10537 . . . . 5 (𝜑 → ((∫2𝐻) − (∫2𝐺)) ∈ ℝ*)
222 itg2leub 24018 . . . . 5 ((𝐹:ℝ⟶(0[,]+∞) ∧ ((∫2𝐻) − (∫2𝐺)) ∈ ℝ*) → ((∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺)))))
223219, 221, 222syl2anc 584 . . . 4 (𝜑 → ((∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺)))))
224218, 223mpbird 258 . . 3 (𝜑 → (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺)))
225 leaddsub 10964 . . . 4 (((∫2𝐹) ∈ ℝ ∧ (∫2𝐺) ∈ ℝ ∧ (∫2𝐻) ∈ ℝ) → (((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻) ↔ (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺))))
22610, 11, 23, 225syl3anc 1364 . . 3 (𝜑 → (((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻) ↔ (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺))))
227224, 226mpbird 258 . 2 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻))
2289, 13, 20, 227xrletrid 12398 1 (𝜑 → (∫2𝐻) = ((∫2𝐹) + (∫2𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 842   = wceq 1522  wcel 2081  wral 3105  Vcvv 3437  cdif 3856  cun 3857  cin 3858  wss 3859  ifcif 4381   class class class wbr 4962  cmpt 5041  dom cdm 5443   Fn wfn 6220  wf 6221  cfv 6225  (class class class)co 7016  𝑓 cof 7265  𝑟 cofr 7266  cr 10382  0cc0 10383   + caddc 10386  +∞cpnf 10518  *cxr 10520  cle 10522  cmin 10717  [,]cicc 12591  vol*covol 23746  volcvol 23747  1citg1 23899  2citg2 23900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-inf2 8950  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460  ax-pre-sup 10461  ax-addf 10462
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-disj 4931  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-se 5403  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-isom 6234  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-of 7267  df-ofr 7268  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-2o 7954  df-oadd 7957  df-er 8139  df-map 8258  df-pm 8259  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-fi 8721  df-sup 8752  df-inf 8753  df-oi 8820  df-dju 9176  df-card 9214  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-div 11146  df-nn 11487  df-2 11548  df-3 11549  df-n0 11746  df-z 11830  df-uz 12094  df-q 12198  df-rp 12240  df-xneg 12357  df-xadd 12358  df-xmul 12359  df-ioo 12592  df-ico 12594  df-icc 12595  df-fz 12743  df-fzo 12884  df-fl 13012  df-seq 13220  df-exp 13280  df-hash 13541  df-cj 14292  df-re 14293  df-im 14294  df-sqrt 14428  df-abs 14429  df-clim 14679  df-sum 14877  df-rest 16525  df-topgen 16546  df-psmet 20219  df-xmet 20220  df-met 20221  df-bl 20222  df-mopn 20223  df-top 21186  df-topon 21203  df-bases 21238  df-cmp 21679  df-ovol 23748  df-vol 23749  df-mbf 23903  df-itg1 23904  df-itg2 23905
This theorem is referenced by:  itg2cnlem2  24046  itgsplit  24119  iblsplit  41812
  Copyright terms: Public domain W3C validator