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

Theorem itg2split 25799
Description: The 2 integral splits under an almost disjoint union. The proof avoids the use of itg2add 25809, 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 715 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
3 0e0iccpnf 13496 . . . . . 6 0 ∈ (0[,]+∞)
43a1i 11 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝑈) → 0 ∈ (0[,]+∞))
52, 4ifclda 4566 . . . 4 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
6 itg2split.h . . . 4 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
75, 6fmptd 7134 . . 3 (𝜑𝐻:ℝ⟶(0[,]+∞))
8 itg2cl 25782 . . 3 (𝐻:ℝ⟶(0[,]+∞) → (∫2𝐻) ∈ ℝ*)
97, 8syl 17 . 2 (𝜑 → (∫2𝐻) ∈ ℝ*)
10 itg2split.sf . . . 4 (𝜑 → (∫2𝐹) ∈ ℝ)
11 itg2split.sg . . . 4 (𝜑 → (∫2𝐺) ∈ ℝ)
1210, 11readdcld 11288 . . 3 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ)
1312rexrd 11309 . 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 25798 . 2 (𝜑 → (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)))
2111adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫2𝐺) ∈ ℝ)
22 itg2lecl 25788 . . . . . . . . 9 ((𝐻:ℝ⟶(0[,]+∞) ∧ ((∫2𝐹) + (∫2𝐺)) ∈ ℝ ∧ (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺))) → (∫2𝐻) ∈ ℝ)
237, 12, 20, 22syl3anc 1370 . . . . . . . 8 (𝜑 → (∫2𝐻) ∈ ℝ)
2423adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫2𝐻) ∈ ℝ)
25 itg1cl 25734 . . . . . . . 8 (𝑓 ∈ dom ∫1 → (∫1𝑓) ∈ ℝ)
2625ad2antrl 728 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫1𝑓) ∈ ℝ)
27 simprll 779 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑓 ∈ dom ∫1)
28 simprrl 781 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑔 ∈ dom ∫1)
2927, 28itg1add 25751 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫1‘(𝑓f + 𝑔)) = ((∫1𝑓) + (∫1𝑔)))
307adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝐻:ℝ⟶(0[,]+∞))
3127, 28i1fadd 25744 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝑓f + 𝑔) ∈ dom ∫1)
32 inss1 4245 . . . . . . . . . . . . . . . 16 (𝐴𝐵) ⊆ 𝐴
33 mblss 25580 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
3414, 33syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ⊆ ℝ)
3532, 34sstrid 4007 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐵) ⊆ ℝ)
3635adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝐴𝐵) ⊆ ℝ)
3716adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (vol*‘(𝐴𝐵)) = 0)
38 nfv 1912 . . . . . . . . . . . . . . . . . 18 𝑥𝜑
39 nfv 1912 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑓 ∈ dom ∫1
40 nfcv 2903 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑓
41 nfcv 2903 . . . . . . . . . . . . . . . . . . . . 21 𝑥r
42 nfmpt1 5256 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0))
4318, 42nfcxfr 2901 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐹
4440, 41, 43nfbr 5195 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑓r𝐹
4539, 44nfan 1897 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑓 ∈ dom ∫1𝑓r𝐹)
46 nfv 1912 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑔 ∈ dom ∫1
47 nfcv 2903 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑔
48 nfmpt1 5256 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0))
4919, 48nfcxfr 2901 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐺
5047, 41, 49nfbr 5195 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑔r𝐺
5146, 50nfan 1897 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑔 ∈ dom ∫1𝑔r𝐺)
5245, 51nfan 1897 . . . . . . . . . . . . . . . . . 18 𝑥((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))
5338, 52nfan 1897 . . . . . . . . . . . . . . . . 17 𝑥(𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺)))
54 eldifi 4141 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → 𝑥 ∈ ℝ)
55 i1ff 25725 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
5627, 55syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑓:ℝ⟶ℝ)
5756ffnd 6738 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑓 Fn ℝ)
58 i1ff 25725 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
5928, 58syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑔:ℝ⟶ℝ)
6059ffnd 6738 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑔 Fn ℝ)
61 reex 11244 . . . . . . . . . . . . . . . . . . . . . 22 ℝ ∈ V
6261a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ℝ ∈ V)
63 inidm 4235 . . . . . . . . . . . . . . . . . . . . 21 (ℝ ∩ ℝ) = ℝ
64 eqidd 2736 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) = (𝑓𝑥))
65 eqidd 2736 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) = (𝑔𝑥))
6657, 60, 62, 62, 63, 64, 65ofval 7708 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → ((𝑓f + 𝑔)‘𝑥) = ((𝑓𝑥) + (𝑔𝑥)))
6754, 66sylan2 593 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓f + 𝑔)‘𝑥) = ((𝑓𝑥) + (𝑔𝑥)))
68 ffvelcdm 7101 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ ℝ)
6956, 54, 68syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑥) ∈ ℝ)
70 ffvelcdm 7101 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℝ)
7159, 54, 70syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑔𝑥) ∈ ℝ)
7269, 71readdcld 11288 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑥) + (𝑔𝑥)) ∈ ℝ)
7372rexrd 11309 . . . . . . . . . . . . . . . . . . . . . 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 11309 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℝ*)
77 iccssxr 13467 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,]+∞) ⊆ ℝ*
78 ffvelcdm 7101 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐻:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝐻𝑥) ∈ (0[,]+∞))
7930, 54, 78syl2an 596 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝐻𝑥) ∈ (0[,]+∞))
8077, 79sselid 3993 . . . . . . . . . . . . . . . . . . . . . 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 11262 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → 0 ∈ ℝ)
84 simprrr 782 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑔r𝐺)
8561a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → ℝ ∈ V)
86 fvexd 6922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ∈ V)
87 ssun2 4189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝐵 ⊆ (𝐴𝐵)
8887, 17sseqtrrid 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑𝐵𝑈)
8988sselda 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑥𝐵) → 𝑥𝑈)
9089adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝑥𝑈)
9190, 2syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝐶 ∈ (0[,]+∞))
923a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐵) → 0 ∈ (0[,]+∞))
9391, 92ifclda 4566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐵, 𝐶, 0) ∈ (0[,]+∞))
9493adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥𝐵, 𝐶, 0) ∈ (0[,]+∞))
95 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑔 Fn ℝ) → 𝑔 Fn ℝ)
96 dffn5 6967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑔 Fn ℝ ↔ 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔𝑥)))
9795, 96sylib 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔𝑥)))
9819a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 Fn ℝ) → 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0)))
9985, 86, 94, 97, 98ofrfval2 7718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑔 Fn ℝ) → (𝑔r𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0)))
10060, 99syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝑔r𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0)))
10184, 100mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ∀𝑥 ∈ ℝ (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
102101r19.21bi 3249 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
10354, 102sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
104103adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑔𝑥) ≤ if(𝑥𝐵, 𝐶, 0))
105 eldifn 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → ¬ 𝑥 ∈ (𝐴𝐵))
106105adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ 𝑥 ∈ (𝐴𝐵))
107 elin 3979 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4542 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝐵, 𝐶, 0) = 0)
113104, 112breqtrd 5174 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑔𝑥) ≤ 0)
11482, 83, 75, 113leadd2dd 11876 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ ((𝑓𝑥) + 0))
11575recnd 11287 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℂ)
116115addridd 11459 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + 0) = (𝑓𝑥))
117114, 116breqtrd 5174 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝑓𝑥))
118 simprlr 780 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → 𝑓r𝐹)
11961a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → ℝ ∈ V)
120 fvexd 6922 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ V)
121 ssun1 4188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝐴 ⊆ (𝐴𝐵)
122121, 17sseqtrrid 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐴𝑈)
123122sselda 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑥𝐴) → 𝑥𝑈)
124123adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝑥𝑈)
125124, 2syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝐶 ∈ (0[,]+∞))
1263a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐴) → 0 ∈ (0[,]+∞))
127125, 126ifclda 4566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐴, 𝐶, 0) ∈ (0[,]+∞))
128127adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥𝐴, 𝐶, 0) ∈ (0[,]+∞))
129 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑓 Fn ℝ) → 𝑓 Fn ℝ)
130 dffn5 6967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 Fn ℝ ↔ 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
131129, 130sylib 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
13218a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑓 Fn ℝ) → 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0)))
133119, 120, 128, 131, 132ofrfval2 7718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 Fn ℝ) → (𝑓r𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0)))
13457, 133syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝑓r𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0)))
135118, 134mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
136135r19.21bi 3249 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
13754, 136sylan2 593 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
138137adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
139122ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → 𝐴𝑈)
140139sselda 3995 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → 𝑥𝑈)
141140iftrued 4539 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝑈, 𝐶, 0) = 𝐶)
142 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
1435adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
1446fvmpt2 7027 . . . . . . . . . . . . . . . . . . . . . . . . . 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 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝑈, 𝐶, 0))
148 iftrue 4537 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 𝐶)
149148adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → if(𝑥𝐴, 𝐶, 0) = 𝐶)
150141, 147, 1493eqtr4d 2785 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝐴, 𝐶, 0))
151138, 150breqtrrd 5176 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ (𝐻𝑥))
15274, 76, 81, 117, 151xrletrd 13201 . . . . . . . . . . . . . . . . . . . 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 11309 . . . . . . . . . . . . . . . . . . . . 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 11262 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → 0 ∈ ℝ)
159137adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑓𝑥) ≤ if(𝑥𝐴, 𝐶, 0))
160 iffalse 4540 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 0)
161160adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → if(𝑥𝐴, 𝐶, 0) = 0)
162159, 161breqtrd 5174 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑓𝑥) ≤ 0)
163157, 158, 154, 162leadd1dd 11875 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (0 + (𝑔𝑥)))
164154recnd 11287 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ∈ ℂ)
165164addlidd 11460 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (0 + (𝑔𝑥)) = (𝑔𝑥))
166163, 165breqtrd 5174 . . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → 𝑈 = (𝐴𝐵))
170169eleq2d 2825 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑥𝑈𝑥 ∈ (𝐴𝐵)))
171 elun 4163 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
172 biorf 936 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4554 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → if(𝑥𝑈, 𝐶, 0) = if(𝑥𝐵, 𝐶, 0))
177168, 176eqtrd 2775 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝐻𝑥) = if(𝑥𝐵, 𝐶, 0))
178167, 177breqtrrd 5176 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → (𝑔𝑥) ≤ (𝐻𝑥))
179153, 155, 156, 166, 178xrletrd 13201 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑥𝐴) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝐻𝑥))
180152, 179pm2.61dan 813 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓𝑥) + (𝑔𝑥)) ≤ (𝐻𝑥))
18167, 180eqbrtrd 5170 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥))
182181ex 412 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (𝑥 ∈ (ℝ ∖ (𝐴𝐵)) → ((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥)))
18353, 182ralrimi 3255 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ∀𝑥 ∈ (ℝ ∖ (𝐴𝐵))((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥))
184 nfv 1912 . . . . . . . . . . . . . . . . 17 𝑦((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥)
185 nfcv 2903 . . . . . . . . . . . . . . . . . 18 𝑥((𝑓f + 𝑔)‘𝑦)
186 nfcv 2903 . . . . . . . . . . . . . . . . . 18 𝑥
187 nfmpt1 5256 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
1886, 187nfcxfr 2901 . . . . . . . . . . . . . . . . . . 19 𝑥𝐻
189 nfcv 2903 . . . . . . . . . . . . . . . . . . 19 𝑥𝑦
190188, 189nffv 6917 . . . . . . . . . . . . . . . . . 18 𝑥(𝐻𝑦)
191185, 186, 190nfbr 5195 . . . . . . . . . . . . . . . . 17 𝑥((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦)
192 fveq2 6907 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝑓f + 𝑔)‘𝑥) = ((𝑓f + 𝑔)‘𝑦))
193 fveq2 6907 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
194192, 193breq12d 5161 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥) ↔ ((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦)))
195184, 191, 194cbvralw 3304 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ (ℝ ∖ (𝐴𝐵))((𝑓f + 𝑔)‘𝑥) ≤ (𝐻𝑥) ↔ ∀𝑦 ∈ (ℝ ∖ (𝐴𝐵))((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦))
196183, 195sylib 218 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ∀𝑦 ∈ (ℝ ∖ (𝐴𝐵))((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦))
197196r19.21bi 3249 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑓f + 𝑔)‘𝑦) ≤ (𝐻𝑦))
19830, 31, 36, 37, 197itg2uba 25793 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫1‘(𝑓f + 𝑔)) ≤ (∫2𝐻))
19929, 198eqbrtrrd 5172 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → ((∫1𝑓) + (∫1𝑔)) ≤ (∫2𝐻))
20026adantrr 717 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑓r𝐹) ∧ (𝑔 ∈ dom ∫1𝑔r𝐺))) → (∫1𝑓) ∈ ℝ)
201 itg1cl 25734 . . . . . . . . . . . . . 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 11863 . . . . . . . . . . . 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 3144 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → ∀𝑔 ∈ dom ∫1(𝑔r𝐺 → (∫1𝑔) ≤ ((∫2𝐻) − (∫1𝑓))))
20993, 19fmptd 7134 . . . . . . . . . 10 (𝜑𝐺:ℝ⟶(0[,]+∞))
210209adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → 𝐺:ℝ⟶(0[,]+∞))
21124, 26resubcld 11689 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → ((∫2𝐻) − (∫1𝑓)) ∈ ℝ)
212211rexrd 11309 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → ((∫2𝐻) − (∫1𝑓)) ∈ ℝ*)
213 itg2leub 25784 . . . . . . . . 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 257 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫2𝐺) ≤ ((∫2𝐻) − (∫1𝑓)))
21621, 24, 26, 215lesubd 11865 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓r𝐹)) → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺)))
217216expr 456 . . . . 5 ((𝜑𝑓 ∈ dom ∫1) → (𝑓r𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺))))
218217ralrimiva 3144 . . . 4 (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓r𝐹 → (∫1𝑓) ≤ ((∫2𝐻) − (∫2𝐺))))
219127, 18fmptd 7134 . . . . 5 (𝜑𝐹:ℝ⟶(0[,]+∞))
22023, 11resubcld 11689 . . . . . 6 (𝜑 → ((∫2𝐻) − (∫2𝐺)) ∈ ℝ)
221220rexrd 11309 . . . . 5 (𝜑 → ((∫2𝐻) − (∫2𝐺)) ∈ ℝ*)
222 itg2leub 25784 . . . . 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 257 . . 3 (𝜑 → (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺)))
225 leaddsub 11737 . . . 4 (((∫2𝐹) ∈ ℝ ∧ (∫2𝐺) ∈ ℝ ∧ (∫2𝐻) ∈ ℝ) → (((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻) ↔ (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺))))
22610, 11, 23, 225syl3anc 1370 . . 3 (𝜑 → (((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻) ↔ (∫2𝐹) ≤ ((∫2𝐻) − (∫2𝐺))))
227224, 226mpbird 257 . 2 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ≤ (∫2𝐻))
2289, 13, 20, 227xrletrid 13194 1 (𝜑 → (∫2𝐻) = ((∫2𝐹) + (∫2𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847   = wceq 1537  wcel 2106  wral 3059  Vcvv 3478  cdif 3960  cun 3961  cin 3962  wss 3963  ifcif 4531   class class class wbr 5148  cmpt 5231  dom cdm 5689   Fn wfn 6558  wf 6559  cfv 6563  (class class class)co 7431  f cof 7695  r cofr 7696  cr 11152  0cc0 11153   + caddc 11156  +∞cpnf 11290  *cxr 11292  cle 11294  cmin 11490  [,]cicc 13387  vol*covol 25511  volcvol 25512  1citg1 25664  2citg2 25665
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231  ax-addf 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-disj 5116  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-ofr 7698  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-er 8744  df-map 8867  df-pm 8868  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fi 9449  df-sup 9480  df-inf 9481  df-oi 9548  df-dju 9939  df-card 9977  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-z 12612  df-uz 12877  df-q 12989  df-rp 13033  df-xneg 13152  df-xadd 13153  df-xmul 13154  df-ioo 13388  df-ico 13390  df-icc 13391  df-fz 13545  df-fzo 13692  df-fl 13829  df-seq 14040  df-exp 14100  df-hash 14367  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-clim 15521  df-sum 15720  df-rest 17469  df-topgen 17490  df-psmet 21374  df-xmet 21375  df-met 21376  df-bl 21377  df-mopn 21378  df-top 22916  df-topon 22933  df-bases 22969  df-cmp 23411  df-ovol 25513  df-vol 25514  df-mbf 25668  df-itg1 25669  df-itg2 25670
This theorem is referenced by:  itg2cnlem2  25812  itgsplit  25886  iblsplit  45922
  Copyright terms: Public domain W3C validator