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

Theorem itg2split 25804
Description: The 2 integral splits under an almost disjoint union. The proof avoids the use of itg2add 25814, which requires countable choice. (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 714 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
3 0e0iccpnf 13519 . . . . . 6 0 ∈ (0[,]+∞)
43a1i 11 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝑈) → 0 ∈ (0[,]+∞))
52, 4ifclda 4583 . . . 4 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
6 itg2split.h . . . 4 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
75, 6fmptd 7148 . . 3 (𝜑𝐻:ℝ⟶(0[,]+∞))
8 itg2cl 25787 . . 3 (𝐻:ℝ⟶(0[,]+∞) → (∫2𝐻) ∈ ℝ*)
97, 8syl 17 . 2 (𝜑 → (∫2𝐻) ∈ ℝ*)
10 itg2split.sf . . . 4 (𝜑 → (∫2𝐹) ∈ ℝ)
11 itg2split.sg . . . 4 (𝜑 → (∫2𝐺) ∈ ℝ)
1210, 11readdcld 11319 . . 3 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ)
1312rexrd 11340 . 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 25803 . 2 (𝜑 → (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)))
2111adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫2𝐺) ∈ ℝ)
22 itg2lecl 25793 . . . . . . . . 9 ((𝐻:ℝ⟶(0[,]+∞) ∧ ((∫2𝐹) + (∫2𝐺)) ∈ ℝ ∧ (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺))) → (∫2𝐻) ∈ ℝ)
237, 12, 20, 22syl3anc 1371 . . . . . . . 8 (𝜑 → (∫2𝐻) ∈ ℝ)
2423adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫2𝐻) ∈ ℝ)
25 itg1cl 25739 . . . . . . . 8 (𝑓 ∈ dom ∫1 → (∫1𝑓) ∈ ℝ)
2625ad2antrl 727 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫1𝑓) ∈ ℝ)
27 simprll 778 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑓 ∈ dom ∫1)
28 simprrl 780 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑔 ∈ dom ∫1)
2927, 28itg1add 25756 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫1‘(𝑓f + 𝑔)) = ((∫1𝑓) + (∫1𝑔)))
307adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝐻:ℝ⟶(0[,]+∞))
3127, 28i1fadd 25749 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝑓f + 𝑔) ∈ dom ∫1)
32 inss1 4258 . . . . . . . . . . . . . . . 16 (𝐴𝐵) ⊆ 𝐴
33 mblss 25585 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
3414, 33syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ⊆ ℝ)
3532, 34sstrid 4020 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐵) ⊆ ℝ)
3635adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝐴𝐵) ⊆ ℝ)
3716adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (vol*‘(𝐴𝐵)) = 0)
38 nfv 1913 . . . . . . . . . . . . . . . . . 18 𝑥𝜑
39 nfv 1913 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑓 ∈ dom ∫1
40 nfcv 2908 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑓
41 nfcv 2908 . . . . . . . . . . . . . . . . . . . . 21 𝑥r
42 nfmpt1 5274 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0))
4318, 42nfcxfr 2906 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐹
4440, 41, 43nfbr 5213 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑓r𝐹
4539, 44nfan 1898 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑓 ∈ dom ∫1𝑓r𝐹)
46 nfv 1913 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑔 ∈ dom ∫1
47 nfcv 2908 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑔
48 nfmpt1 5274 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0))
4919, 48nfcxfr 2906 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐺
5047, 41, 49nfbr 5213 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑔r𝐺
5146, 50nfan 1898 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑔 ∈ dom ∫1𝑔r𝐺)
5245, 51nfan 1898 . . . . . . . . . . . . . . . . . 18 𝑥((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))
5338, 52nfan 1898 . . . . . . . . . . . . . . . . 17 𝑥(𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺)))
54 eldifi 4154 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → 𝑥 ∈ ℝ)
55 i1ff 25730 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
5627, 55syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑓:ℝ⟶ℝ)
5756ffnd 6748 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑓 Fn ℝ)
58 i1ff 25730 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
5928, 58syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑔:ℝ⟶ℝ)
6059ffnd 6748 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑔 Fn ℝ)
61 reex 11275 . . . . . . . . . . . . . . . . . . . . . 22 ℝ ∈ V
6261a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ℝ ∈ V)
63 inidm 4248 . . . . . . . . . . . . . . . . . . . . 21 (ℝ ∩ ℝ) = ℝ
64 eqidd 2741 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) = (𝑓𝑥))
65 eqidd 2741 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) = (𝑔𝑥))
6657, 60, 62, 62, 63, 64, 65ofval 7725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → ((𝑓f + 𝑔)‘𝑥) = ((𝑓𝑥) + (𝑔𝑥)))
6754, 66sylan2 592 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓f + 𝑔)‘𝑥) = ((𝑓𝑥) + (𝑔𝑥)))
68 ffvelcdm 7115 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ ℝ)
6956, 54, 68syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑥) ∈ ℝ)
70 ffvelcdm 7115 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℝ)
7159, 54, 70syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑔𝑥) ∈ ℝ)
7269, 71readdcld 11319 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ)
7372rexrd 11340 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ*)
7473adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ*)
7569adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℝ)
7675rexrd 11340 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℝ*)
77 iccssxr 13490 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,]+∞) ⊆ ℝ*
78 ffvelcdm 7115 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐻:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝐻𝑥) ∈ (0[,]+∞))
7930, 54, 78syl2an 595 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝐻𝑥) ∈ (0[,]+∞))
8077, 79sselid 4006 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝐻𝑥) ∈ ℝ*)
8180adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝐻𝑥) ∈ ℝ*)
8271adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑔𝑥) ∈ ℝ)
83 0red 11293 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → 0 ∈ ℝ)
84 simprrr 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑔r𝐺)
8561a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → ℝ ∈ V)
86 fvexd 6935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ∈ V)
87 ssun2 4202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝐵 ⊆ (𝐴𝐵)
8887, 17sseqtrrid 4062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑𝐵𝑈)
8988sselda 4008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑥𝐵) → 𝑥𝑈)
9089adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝑥𝑈)
9190, 2syldan 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝐶 ∈ (0[,]+∞))
923a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐵) → 0 ∈ (0[,]+∞))
9391, 92ifclda 4583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐵, 𝐶, 0) ∈ (0[,]+∞))
9493adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥𝐵, 𝐶, 0) ∈ (0[,]+∞))
95 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑔 Fn ℝ) → 𝑔 Fn ℝ)
96 dffn5 6980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑔 Fn ℝ ↔ 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔𝑥)))
9795, 96sylib 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔𝑥)))
9819a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0)))
9985, 86, 94, 97, 98ofrfval2 7735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑔 Fn ℝ) → (𝑔r𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0)))
10060, 99syldan 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝑔r𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0)))
10184, 100mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
102101r19.21bi 3257 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
10354, 102sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
104103adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
105 eldifn 4155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → ¬ 𝑥 ∈ (𝐴𝐵))
106105adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ 𝑥 ∈ (𝐴𝐵))
107 elin 3992 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
108106, 107sylnib 328 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ (𝑥𝐴𝑥𝐵))
109 imnan 399 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ ¬ (𝑥𝐴𝑥𝐵))
110108, 109sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑥𝐴 → ¬ 𝑥𝐵))
111110imp 406 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ¬ 𝑥𝐵)
112111iffalsed 4559 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝐵, 𝐶, 0) = 0)
113104, 112breqtrd 5192 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑔𝑥) ≤ 0)
11482, 83, 75, 113leadd2dd 11905 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ ((𝑓𝑥) + 0))
11575recnd 11318 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℂ)
116115addridd 11490 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + 0) = (𝑓𝑥))
117114, 116breqtrd 5192 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝑓𝑥))
118 simprlr 779 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑓r𝐹)
11961a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → ℝ ∈ V)
120 fvexd 6935 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ V)
121 ssun1 4201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝐴 ⊆ (𝐴𝐵)
122121, 17sseqtrrid 4062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐴𝑈)
123122sselda 4008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑥𝐴) → 𝑥𝑈)
124123adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝑥𝑈)
125124, 2syldan 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝐶 ∈ (0[,]+∞))
1263a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐴) → 0 ∈ (0[,]+∞))
127125, 126ifclda 4583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐴, 𝐶, 0) ∈ (0[,]+∞))
128127adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥𝐴, 𝐶, 0) ∈ (0[,]+∞))
129 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑓 Fn ℝ) → 𝑓 Fn ℝ)
130 dffn5 6980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 Fn ℝ ↔ 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
131129, 130sylib 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
13218a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0)))
133119, 120, 128, 131, 132ofrfval2 7735 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 Fn ℝ) → (𝑓r𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0)))
13457, 133syldan 590 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝑓r𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0)))
135118, 134mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
136135r19.21bi 3257 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
13754, 136sylan2 592 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
138137adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
139122ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → 𝐴𝑈)
140139sselda 4008 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → 𝑥𝑈)
141140iftrued 4556 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝑈, 𝐶, 0) = 𝐶)
142 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
1435adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
1446fvmpt2 7040 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ ℝ ∧ if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞)) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
145142, 143, 144syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
14654, 145sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
147146adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
148 iftrue 4554 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 𝐶)
149148adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝐴, 𝐶, 0) = 𝐶)
150141, 147, 1493eqtr4d 2790 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝐴, 𝐶, 0))
151138, 150breqtrrd 5194 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ (𝐻𝑥))
15274, 76, 81, 117, 151xrletrd 13224 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝐻𝑥))
15373adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ*)
15471adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ∈ ℝ)
155154rexrd 11340 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ∈ ℝ*)
15680adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝐻𝑥) ∈ ℝ*)
15769adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑓𝑥) ∈ ℝ)
158 0red 11293 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → 0 ∈ ℝ)
159137adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
160 iffalse 4557 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 0)
161160adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → if(𝑥𝐴, 𝐶, 0) = 0)
162159, 161breqtrd 5192 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑓𝑥) ≤ 0)
163157, 158, 154, 162leadd1dd 11904 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (0 + (𝑔𝑥)))
164154recnd 11318 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ∈ ℂ)
165164addlidd 11491 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (0 + (𝑔𝑥)) = (𝑔𝑥))
166163, 165breqtrd 5192 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝑔𝑥))
167103adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
168146adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
16917ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → 𝑈 = (𝐴𝐵))
170169eleq2d 2830 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑥𝑈𝑥 ∈ (𝐴𝐵)))
171 elun 4176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
172 biorf 935 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥𝐴 → (𝑥𝐵 ↔ (𝑥𝐴𝑥𝐵)))
173171, 172bitr4id 290 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥𝐴 → (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
174173adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
175170, 174bitrd 279 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑥𝑈𝑥𝐵))
176175ifbid 4571 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → if(𝑥𝑈, 𝐶, 0) = if(𝑥𝐵, 𝐶, 0))
177168, 176eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝐵, 𝐶, 0))
178167, 177breqtrrd 5194 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ≤ (𝐻𝑥))
179153, 155, 156, 166, 178xrletrd 13224 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝐻𝑥))
180152, 179pm2.61dan 812 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝐻𝑥))
18167, 180eqbrtrd 5188 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥))
182181ex 412 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → ((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥)))
18353, 182ralrimi 3263 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ∀𝑥 ∈ (ℝ ∖ (𝐴𝐵))((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥))
184 nfv 1913 . . . . . . . . . . . . . . . . 17 𝑦((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥)
185 nfcv 2908 . . . . . . . . . . . . . . . . . 18 𝑥((𝑓f + 𝑔)‘𝑦)
186 nfcv 2908 . . . . . . . . . . . . . . . . . 18 𝑥
187 nfmpt1 5274 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
1886, 187nfcxfr 2906 . . . . . . . . . . . . . . . . . . 19 𝑥𝐻
189 nfcv 2908 . . . . . . . . . . . . . . . . . . 19 𝑥𝑦
190188, 189nffv 6930 . . . . . . . . . . . . . . . . . 18 𝑥(𝐻𝑦)
191185, 186, 190nfbr 5213 . . . . . . . . . . . . . . . . 17 𝑥((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦)
192 fveq2 6920 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝑓f + 𝑔)‘𝑥) = ((𝑓f + 𝑔)‘𝑦))
193 fveq2 6920 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
194192, 193breq12d 5179 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥) ↔ ((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦)))
195184, 191, 194cbvralw 3312 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ (ℝ ∖ (𝐴𝐵))((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥) ↔ ∀𝑦 ∈ (ℝ ∖ (𝐴𝐵))((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦))
196183, 195sylib 218 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ∀𝑦 ∈ (ℝ ∖ (𝐴𝐵))((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦))
197196r19.21bi 3257 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦))
19830, 31, 36, 37, 197itg2uba 25798 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫1‘(𝑓f + 𝑔)) ≤ (∫2𝐻))
19929, 198eqbrtrrd 5190 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ((∫1𝑓) + (∫1𝑔)) ≤ (∫2𝐻))
20026adantrr 716 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫1𝑓) ∈ ℝ)
201 itg1cl 25739 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → (∫1𝑔) ∈ ℝ)
20228, 201syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫1𝑔) ∈ ℝ)
20323adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫2𝐻) ∈ ℝ)
204200, 202, 203leaddsub2d 11892 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (((∫1𝑓) + (∫1𝑔)) ≤ (∫2𝐻) ↔ (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓))))
205199, 204mpbid 232 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))
206205anassrs 467 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺)) → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))
207206expr 456 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) ∧ 𝑔 ∈ dom ∫1) → (𝑔r𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓))))
208207ralrimiva 3152 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → ∀𝑔 ∈ dom ∫1(𝑔r𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓))))
20993, 19fmptd 7148 . . . . . . . . . 10 (𝜑𝐺:ℝ⟶(0[,]+∞))
210209adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → 𝐺:ℝ⟶(0[,]+∞))
21124, 26resubcld 11718 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → ((∫2𝐻) − (∫1𝑓)) ∈ ℝ)
212211rexrd 11340 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → ((∫2𝐻) − (∫1𝑓)) ∈ ℝ*)
213 itg2leub 25789 . . . . . . . . 9 ((𝐺:ℝ⟶(0[,]+∞) ∧ ((∫2𝐻) − (∫1𝑓)) ∈ ℝ*) → ((∫2𝐺) ≤ ((∫2𝐻) − (∫1𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔r𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))))
214210, 212, 213syl2anc 583 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → ((∫2𝐺) ≤ ((∫2𝐻) − (∫1𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔r𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))))
215208, 214mpbird 257 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫2𝐺) ≤ ((∫2𝐻) − (∫1𝑓)))
21621, 24, 26, 215lesubd 11894 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺)))
217216expr 456 . . . . 5 ((𝜑𝑓 ∈ dom ∫1) → (𝑓r𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺))))
218217ralrimiva 3152 . . . 4 (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓r𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺))))
219127, 18fmptd 7148 . . . . 5 (𝜑𝐹:ℝ⟶(0[,]+∞))
22023, 11resubcld 11718 . . . . . 6 (𝜑 → ((∫2𝐻) − (∫2𝐺)) ∈ ℝ)
221220rexrd 11340 . . . . 5 (𝜑 → ((∫2𝐻) − (∫2𝐺)) ∈ ℝ*)
222 itg2leub 25789 . . . . 5 ((𝐹:ℝ⟶(0[,]+∞) ∧ ((∫2𝐻) − (∫2𝐺)) ∈ ℝ*) → ((∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓r𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺)))))
223219, 221, 222syl2anc 583 . . . 4 (𝜑 → ((∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓r𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺)))))
224218, 223mpbird 257 . . 3 (𝜑 → (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺)))
225 leaddsub 11766 . . . 4 (((∫2𝐹) ∈ ℝ ∧ (∫2𝐺) ∈ ℝ ∧ (∫2𝐻) ∈ ℝ) → (((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻) ↔ (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺))))
22610, 11, 23, 225syl3anc 1371 . . 3 (𝜑 → (((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻) ↔ (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺))))
227224, 226mpbird 257 . 2 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻))
2289, 13, 20, 227xrletrid 13217 1 (𝜑 → (∫2𝐻) = ((∫2𝐹) + (∫2𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 846   = wceq 1537  wcel 2108  wral 3067  Vcvv 3488  cdif 3973  cun 3974  cin 3975  wss 3976  ifcif 4548   class class class wbr 5166  cmpt 5249  dom cdm 5700   Fn wfn 6568  wf 6569  cfv 6573  (class class class)co 7448  f cof 7712  r cofr 7713  cr 11183  0cc0 11184   + caddc 11187  +∞cpnf 11321  *cxr 11323  cle 11325  cmin 11520  [,]cicc 13410  vol*covol 25516  volcvol 25517  1citg1 25669  2citg2 25670
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262  ax-addf 11263
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-disj 5134  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-ofr 7715  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-er 8763  df-map 8886  df-pm 8887  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fi 9480  df-sup 9511  df-inf 9512  df-oi 9579  df-dju 9970  df-card 10008  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-n0 12554  df-z 12640  df-uz 12904  df-q 13014  df-rp 13058  df-xneg 13175  df-xadd 13176  df-xmul 13177  df-ioo 13411  df-ico 13413  df-icc 13414  df-fz 13568  df-fzo 13712  df-fl 13843  df-seq 14053  df-exp 14113  df-hash 14380  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-clim 15534  df-sum 15735  df-rest 17482  df-topgen 17503  df-psmet 21379  df-xmet 21380  df-met 21381  df-bl 21382  df-mopn 21383  df-top 22921  df-topon 22938  df-bases 22974  df-cmp 23416  df-ovol 25518  df-vol 25519  df-mbf 25673  df-itg1 25674  df-itg2 25675
This theorem is referenced by:  itg2cnlem2  25817  itgsplit  25891  iblsplit  45887
  Copyright terms: Public domain W3C validator