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

Theorem itg2split 25196
Description: The 2 integral splits under an almost disjoint union. The proof avoids the use of itg2add 25206, 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 713 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
3 0e0iccpnf 13418 . . . . . 6 0 ∈ (0[,]+∞)
43a1i 11 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝑈) → 0 ∈ (0[,]+∞))
52, 4ifclda 4557 . . . 4 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
6 itg2split.h . . . 4 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
75, 6fmptd 7098 . . 3 (𝜑𝐻:ℝ⟶(0[,]+∞))
8 itg2cl 25179 . . 3 (𝐻:ℝ⟶(0[,]+∞) → (∫2𝐻) ∈ ℝ*)
97, 8syl 17 . 2 (𝜑 → (∫2𝐻) ∈ ℝ*)
10 itg2split.sf . . . 4 (𝜑 → (∫2𝐹) ∈ ℝ)
11 itg2split.sg . . . 4 (𝜑 → (∫2𝐺) ∈ ℝ)
1210, 11readdcld 11225 . . 3 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ)
1312rexrd 11246 . 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 25195 . 2 (𝜑 → (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)))
2111adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫2𝐺) ∈ ℝ)
22 itg2lecl 25185 . . . . . . . . 9 ((𝐻:ℝ⟶(0[,]+∞) ∧ ((∫2𝐹) + (∫2𝐺)) ∈ ℝ ∧ (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺))) → (∫2𝐻) ∈ ℝ)
237, 12, 20, 22syl3anc 1371 . . . . . . . 8 (𝜑 → (∫2𝐻) ∈ ℝ)
2423adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫2𝐻) ∈ ℝ)
25 itg1cl 25131 . . . . . . . 8 (𝑓 ∈ dom ∫1 → (∫1𝑓) ∈ ℝ)
2625ad2antrl 726 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫1𝑓) ∈ ℝ)
27 simprll 777 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑓 ∈ dom ∫1)
28 simprrl 779 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑔 ∈ dom ∫1)
2927, 28itg1add 25148 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫1‘(𝑓f + 𝑔)) = ((∫1𝑓) + (∫1𝑔)))
307adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝐻:ℝ⟶(0[,]+∞))
3127, 28i1fadd 25141 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝑓f + 𝑔) ∈ dom ∫1)
32 inss1 4224 . . . . . . . . . . . . . . . 16 (𝐴𝐵) ⊆ 𝐴
33 mblss 24977 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
3414, 33syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ⊆ ℝ)
3532, 34sstrid 3989 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐵) ⊆ ℝ)
3635adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝐴𝐵) ⊆ ℝ)
3716adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (vol*‘(𝐴𝐵)) = 0)
38 nfv 1917 . . . . . . . . . . . . . . . . . 18 𝑥𝜑
39 nfv 1917 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑓 ∈ dom ∫1
40 nfcv 2902 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑓
41 nfcv 2902 . . . . . . . . . . . . . . . . . . . . 21 𝑥r
42 nfmpt1 5249 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0))
4318, 42nfcxfr 2900 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐹
4440, 41, 43nfbr 5188 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑓r𝐹
4539, 44nfan 1902 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑓 ∈ dom ∫1𝑓r𝐹)
46 nfv 1917 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑔 ∈ dom ∫1
47 nfcv 2902 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑔
48 nfmpt1 5249 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0))
4919, 48nfcxfr 2900 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐺
5047, 41, 49nfbr 5188 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑔r𝐺
5146, 50nfan 1902 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑔 ∈ dom ∫1𝑔r𝐺)
5245, 51nfan 1902 . . . . . . . . . . . . . . . . . 18 𝑥((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))
5338, 52nfan 1902 . . . . . . . . . . . . . . . . 17 𝑥(𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺)))
54 eldifi 4122 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → 𝑥 ∈ ℝ)
55 i1ff 25122 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
5627, 55syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑓:ℝ⟶ℝ)
5756ffnd 6705 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑓 Fn ℝ)
58 i1ff 25122 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
5928, 58syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑔:ℝ⟶ℝ)
6059ffnd 6705 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑔 Fn ℝ)
61 reex 11183 . . . . . . . . . . . . . . . . . . . . . 22 ℝ ∈ V
6261a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ℝ ∈ V)
63 inidm 4214 . . . . . . . . . . . . . . . . . . . . 21 (ℝ ∩ ℝ) = ℝ
64 eqidd 2732 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) = (𝑓𝑥))
65 eqidd 2732 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) = (𝑔𝑥))
6657, 60, 62, 62, 63, 64, 65ofval 7664 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → ((𝑓f + 𝑔)‘𝑥) = ((𝑓𝑥) + (𝑔𝑥)))
6754, 66sylan2 593 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓f + 𝑔)‘𝑥) = ((𝑓𝑥) + (𝑔𝑥)))
68 ffvelcdm 7068 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ ℝ)
6956, 54, 68syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑥) ∈ ℝ)
70 ffvelcdm 7068 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℝ)
7159, 54, 70syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑔𝑥) ∈ ℝ)
7269, 71readdcld 11225 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ)
7372rexrd 11246 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ*)
7473adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ*)
7569adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℝ)
7675rexrd 11246 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℝ*)
77 iccssxr 13389 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,]+∞) ⊆ ℝ*
78 ffvelcdm 7068 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐻:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝐻𝑥) ∈ (0[,]+∞))
7930, 54, 78syl2an 596 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝐻𝑥) ∈ (0[,]+∞))
8077, 79sselid 3976 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝐻𝑥) ∈ ℝ*)
8180adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝐻𝑥) ∈ ℝ*)
8271adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑔𝑥) ∈ ℝ)
83 0red 11199 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → 0 ∈ ℝ)
84 simprrr 780 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑔r𝐺)
8561a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → ℝ ∈ V)
86 fvexd 6893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ∈ V)
87 ssun2 4169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝐵 ⊆ (𝐴𝐵)
8887, 17sseqtrrid 4031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑𝐵𝑈)
8988sselda 3978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑥𝐵) → 𝑥𝑈)
9089adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝑥𝑈)
9190, 2syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝐶 ∈ (0[,]+∞))
923a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐵) → 0 ∈ (0[,]+∞))
9391, 92ifclda 4557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐵, 𝐶, 0) ∈ (0[,]+∞))
9493adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥𝐵, 𝐶, 0) ∈ (0[,]+∞))
95 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑔 Fn ℝ) → 𝑔 Fn ℝ)
96 dffn5 6937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑔 Fn ℝ ↔ 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔𝑥)))
9795, 96sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔𝑥)))
9819a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0)))
9985, 86, 94, 97, 98ofrfval2 7674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑔 Fn ℝ) → (𝑔r𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0)))
10060, 99syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝑔r𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0)))
10184, 100mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
102101r19.21bi 3247 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
10354, 102sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
104103adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
105 eldifn 4123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → ¬ 𝑥 ∈ (𝐴𝐵))
106105adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ 𝑥 ∈ (𝐴𝐵))
107 elin 3960 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
108106, 107sylnib 327 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ (𝑥𝐴𝑥𝐵))
109 imnan 400 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ ¬ (𝑥𝐴𝑥𝐵))
110108, 109sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑥𝐴 → ¬ 𝑥𝐵))
111110imp 407 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ¬ 𝑥𝐵)
112111iffalsed 4533 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝐵, 𝐶, 0) = 0)
113104, 112breqtrd 5167 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑔𝑥) ≤ 0)
11482, 83, 75, 113leadd2dd 11811 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ ((𝑓𝑥) + 0))
11575recnd 11224 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℂ)
116115addridd 11396 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + 0) = (𝑓𝑥))
117114, 116breqtrd 5167 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝑓𝑥))
118 simprlr 778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑓r𝐹)
11961a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → ℝ ∈ V)
120 fvexd 6893 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ V)
121 ssun1 4168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝐴 ⊆ (𝐴𝐵)
122121, 17sseqtrrid 4031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐴𝑈)
123122sselda 3978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑥𝐴) → 𝑥𝑈)
124123adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝑥𝑈)
125124, 2syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝐶 ∈ (0[,]+∞))
1263a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐴) → 0 ∈ (0[,]+∞))
127125, 126ifclda 4557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐴, 𝐶, 0) ∈ (0[,]+∞))
128127adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥𝐴, 𝐶, 0) ∈ (0[,]+∞))
129 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑓 Fn ℝ) → 𝑓 Fn ℝ)
130 dffn5 6937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 Fn ℝ ↔ 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
131129, 130sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
13218a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0)))
133119, 120, 128, 131, 132ofrfval2 7674 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 Fn ℝ) → (𝑓r𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0)))
13457, 133syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝑓r𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0)))
135118, 134mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
136135r19.21bi 3247 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
13754, 136sylan2 593 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
138137adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
139122ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → 𝐴𝑈)
140139sselda 3978 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → 𝑥𝑈)
141140iftrued 4530 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝑈, 𝐶, 0) = 𝐶)
142 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
1435adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
1446fvmpt2 6995 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ ℝ ∧ if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞)) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
145142, 143, 144syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
14654, 145sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
147146adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
148 iftrue 4528 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 𝐶)
149148adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝐴, 𝐶, 0) = 𝐶)
150141, 147, 1493eqtr4d 2781 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝐴, 𝐶, 0))
151138, 150breqtrrd 5169 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ (𝐻𝑥))
15274, 76, 81, 117, 151xrletrd 13123 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝐻𝑥))
15373adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ*)
15471adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ∈ ℝ)
155154rexrd 11246 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ∈ ℝ*)
15680adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝐻𝑥) ∈ ℝ*)
15769adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑓𝑥) ∈ ℝ)
158 0red 11199 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → 0 ∈ ℝ)
159137adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
160 iffalse 4531 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 0)
161160adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → if(𝑥𝐴, 𝐶, 0) = 0)
162159, 161breqtrd 5167 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑓𝑥) ≤ 0)
163157, 158, 154, 162leadd1dd 11810 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (0 + (𝑔𝑥)))
164154recnd 11224 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ∈ ℂ)
165164addlidd 11397 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (0 + (𝑔𝑥)) = (𝑔𝑥))
166163, 165breqtrd 5167 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝑔𝑥))
167103adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
168146adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
16917ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → 𝑈 = (𝐴𝐵))
170169eleq2d 2818 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑥𝑈𝑥 ∈ (𝐴𝐵)))
171 elun 4144 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
172 biorf 935 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥𝐴 → (𝑥𝐵 ↔ (𝑥𝐴𝑥𝐵)))
173171, 172bitr4id 289 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥𝐴 → (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
174173adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
175170, 174bitrd 278 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑥𝑈𝑥𝐵))
176175ifbid 4545 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → if(𝑥𝑈, 𝐶, 0) = if(𝑥𝐵, 𝐶, 0))
177168, 176eqtrd 2771 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝐵, 𝐶, 0))
178167, 177breqtrrd 5169 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ≤ (𝐻𝑥))
179153, 155, 156, 166, 178xrletrd 13123 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝐻𝑥))
180152, 179pm2.61dan 811 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝐻𝑥))
18167, 180eqbrtrd 5163 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥))
182181ex 413 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → ((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥)))
18353, 182ralrimi 3253 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ∀𝑥 ∈ (ℝ ∖ (𝐴𝐵))((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥))
184 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑦((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥)
185 nfcv 2902 . . . . . . . . . . . . . . . . . 18 𝑥((𝑓f + 𝑔)‘𝑦)
186 nfcv 2902 . . . . . . . . . . . . . . . . . 18 𝑥
187 nfmpt1 5249 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
1886, 187nfcxfr 2900 . . . . . . . . . . . . . . . . . . 19 𝑥𝐻
189 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑥𝑦
190188, 189nffv 6888 . . . . . . . . . . . . . . . . . 18 𝑥(𝐻𝑦)
191185, 186, 190nfbr 5188 . . . . . . . . . . . . . . . . 17 𝑥((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦)
192 fveq2 6878 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝑓f + 𝑔)‘𝑥) = ((𝑓f + 𝑔)‘𝑦))
193 fveq2 6878 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
194192, 193breq12d 5154 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥) ↔ ((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦)))
195184, 191, 194cbvralw 3302 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ (ℝ ∖ (𝐴𝐵))((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥) ↔ ∀𝑦 ∈ (ℝ ∖ (𝐴𝐵))((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦))
196183, 195sylib 217 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ∀𝑦 ∈ (ℝ ∖ (𝐴𝐵))((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦))
197196r19.21bi 3247 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦))
19830, 31, 36, 37, 197itg2uba 25190 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫1‘(𝑓f + 𝑔)) ≤ (∫2𝐻))
19929, 198eqbrtrrd 5165 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ((∫1𝑓) + (∫1𝑔)) ≤ (∫2𝐻))
20026adantrr 715 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫1𝑓) ∈ ℝ)
201 itg1cl 25131 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → (∫1𝑔) ∈ ℝ)
20228, 201syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫1𝑔) ∈ ℝ)
20323adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫2𝐻) ∈ ℝ)
204200, 202, 203leaddsub2d 11798 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (((∫1𝑓) + (∫1𝑔)) ≤ (∫2𝐻) ↔ (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓))))
205199, 204mpbid 231 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))
206205anassrs 468 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺)) → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))
207206expr 457 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) ∧ 𝑔 ∈ dom ∫1) → (𝑔r𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓))))
208207ralrimiva 3145 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → ∀𝑔 ∈ dom ∫1(𝑔r𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓))))
20993, 19fmptd 7098 . . . . . . . . . 10 (𝜑𝐺:ℝ⟶(0[,]+∞))
210209adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → 𝐺:ℝ⟶(0[,]+∞))
21124, 26resubcld 11624 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → ((∫2𝐻) − (∫1𝑓)) ∈ ℝ)
212211rexrd 11246 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → ((∫2𝐻) − (∫1𝑓)) ∈ ℝ*)
213 itg2leub 25181 . . . . . . . . 9 ((𝐺:ℝ⟶(0[,]+∞) ∧ ((∫2𝐻) − (∫1𝑓)) ∈ ℝ*) → ((∫2𝐺) ≤ ((∫2𝐻) − (∫1𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔r𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))))
214210, 212, 213syl2anc 584 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → ((∫2𝐺) ≤ ((∫2𝐻) − (∫1𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔r𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓)))))
215208, 214mpbird 256 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫2𝐺) ≤ ((∫2𝐻) − (∫1𝑓)))
21621, 24, 26, 215lesubd 11800 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺)))
217216expr 457 . . . . 5 ((𝜑𝑓 ∈ dom ∫1) → (𝑓r𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺))))
218217ralrimiva 3145 . . . 4 (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓r𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺))))
219127, 18fmptd 7098 . . . . 5 (𝜑𝐹:ℝ⟶(0[,]+∞))
22023, 11resubcld 11624 . . . . . 6 (𝜑 → ((∫2𝐻) − (∫2𝐺)) ∈ ℝ)
221220rexrd 11246 . . . . 5 (𝜑 → ((∫2𝐻) − (∫2𝐺)) ∈ ℝ*)
222 itg2leub 25181 . . . . 5 ((𝐹:ℝ⟶(0[,]+∞) ∧ ((∫2𝐻) − (∫2𝐺)) ∈ ℝ*) → ((∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓r𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺)))))
223219, 221, 222syl2anc 584 . . . 4 (𝜑 → ((∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓r𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺)))))
224218, 223mpbird 256 . . 3 (𝜑 → (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺)))
225 leaddsub 11672 . . . 4 (((∫2𝐹) ∈ ℝ ∧ (∫2𝐺) ∈ ℝ ∧ (∫2𝐻) ∈ ℝ) → (((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻) ↔ (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺))))
22610, 11, 23, 225syl3anc 1371 . . 3 (𝜑 → (((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻) ↔ (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺))))
227224, 226mpbird 256 . 2 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻))
2289, 13, 20, 227xrletrid 13116 1 (𝜑 → (∫2𝐻) = ((∫2𝐹) + (∫2𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wcel 2106  wral 3060  Vcvv 3473  cdif 3941  cun 3942  cin 3943  wss 3944  ifcif 4522   class class class wbr 5141  cmpt 5224  dom cdm 5669   Fn wfn 6527  wf 6528  cfv 6532  (class class class)co 7393  f cof 7651  r cofr 7652  cr 11091  0cc0 11092   + caddc 11095  +∞cpnf 11227  *cxr 11229  cle 11231  cmin 11426  [,]cicc 13309  vol*covol 24908  volcvol 24909  1citg1 25061  2citg2 25062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-inf2 9618  ax-cnex 11148  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169  ax-pre-sup 11170  ax-addf 11171
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-int 4944  df-iun 4992  df-disj 5107  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-isom 6541  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-of 7653  df-ofr 7654  df-om 7839  df-1st 7957  df-2nd 7958  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-1o 8448  df-2o 8449  df-er 8686  df-map 8805  df-pm 8806  df-en 8923  df-dom 8924  df-sdom 8925  df-fin 8926  df-fi 9388  df-sup 9419  df-inf 9420  df-oi 9487  df-dju 9878  df-card 9916  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-div 11854  df-nn 12195  df-2 12257  df-3 12258  df-n0 12455  df-z 12541  df-uz 12805  df-q 12915  df-rp 12957  df-xneg 13074  df-xadd 13075  df-xmul 13076  df-ioo 13310  df-ico 13312  df-icc 13313  df-fz 13467  df-fzo 13610  df-fl 13739  df-seq 13949  df-exp 14010  df-hash 14273  df-cj 15028  df-re 15029  df-im 15030  df-sqrt 15164  df-abs 15165  df-clim 15414  df-sum 15615  df-rest 17350  df-topgen 17371  df-psmet 20870  df-xmet 20871  df-met 20872  df-bl 20873  df-mopn 20874  df-top 22325  df-topon 22342  df-bases 22378  df-cmp 22820  df-ovol 24910  df-vol 24911  df-mbf 25065  df-itg1 25066  df-itg2 25067
This theorem is referenced by:  itg2cnlem2  25209  itgsplit  25282  iblsplit  44455
  Copyright terms: Public domain W3C validator