Theorem itg2split 23322

Description: The ∫₂ integral splits under an almost disjoint union. (The proof avoids the use of itg2add 23332 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.

Step	Hyp	Ref	Expression
1		itg2split.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ dom vol)
2		itg2split.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ dom vol)
3		itg2split.i	. . 3 ⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0)
4		itg2split.u	. . 3 ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))
5		itg2split.c	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞))
6		itg2split.f	. . 3 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))
7		itg2split.g	. . 3 ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0))
8		itg2split.h	. . 3 ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0))
9		itg2split.sf	. . 3 ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)
10		itg2split.sg	. . 3 ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ)
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	itg2splitlem 23321	. 2 ⊢ (𝜑 → (∫2‘𝐻) ≤ ((∫2‘𝐹) + (∫2‘𝐺)))
12	10	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹)) → (∫2‘𝐺) ∈ ℝ)
13	5	adantlr 747	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞))
14		0e0iccpnf 12154	. . . . . . . . . . . 12 ⊢ 0 ∈ (0[,]+∞)
15	14	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝑈) → 0 ∈ (0[,]+∞))
16	13, 15	ifclda 4070	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞))
17	16, 8	fmptd 6292	. . . . . . . . 9 ⊢ (𝜑 → 𝐻:ℝ⟶(0[,]+∞))
18	9, 10	readdcld 9948	. . . . . . . . 9 ⊢ (𝜑 → ((∫2‘𝐹) + (∫2‘𝐺)) ∈ ℝ)
19		itg2lecl 23311	. . . . . . . . 9 ⊢ ((𝐻:ℝ⟶(0[,]+∞) ∧ ((∫2‘𝐹) + (∫2‘𝐺)) ∈ ℝ ∧ (∫2‘𝐻) ≤ ((∫2‘𝐹) + (∫2‘𝐺))) → (∫2‘𝐻) ∈ ℝ)
20	17, 18, 11, 19	syl3anc 1318	. . . . . . . 8 ⊢ (𝜑 → (∫2‘𝐻) ∈ ℝ)
21	20	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹)) → (∫2‘𝐻) ∈ ℝ)
22		itg1cl 23258	. . . . . . . 8 ⊢ (𝑓 ∈ dom ∫1 → (∫1‘𝑓) ∈ ℝ)
23	22	ad2antrl 760	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹)) → (∫1‘𝑓) ∈ ℝ)
24		simprll 798	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → 𝑓 ∈ dom ∫1)
25		simprrl 800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → 𝑔 ∈ dom ∫1)
26	24, 25	itg1add 23274	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → (∫1‘(𝑓 ∘𝑓 + 𝑔)) = ((∫1‘𝑓) + (∫1‘𝑔)))
27	17	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → 𝐻:ℝ⟶(0[,]+∞))
28	24, 25	i1fadd 23268	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → (𝑓 ∘𝑓 + 𝑔) ∈ dom ∫1)
29		inss1 3795	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
30		mblss 23106	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
31	1, 30	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
32	29, 31	syl5ss 3579	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ ℝ)
33	32	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → (𝐴 ∩ 𝐵) ⊆ ℝ)
34	3	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → (vol*‘(𝐴 ∩ 𝐵)) = 0)
35		nfv 1830	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥𝜑
36		nfv 1830	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥 𝑓 ∈ dom ∫1
37		nfcv 2751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝑓
38		nfcv 2751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥 ∘𝑟 ≤
39		nfmpt1 4675	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))
40	6, 39	nfcxfr 2749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝐹
41	37, 38, 40	nfbr 4629	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥 𝑓 ∘𝑟 ≤ 𝐹
42	36, 41	nfan 1816	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹)
43		nfv 1830	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥 𝑔 ∈ dom ∫1
44		nfcv 2751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝑔
45		nfmpt1 4675	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0))
46	7, 45	nfcxfr 2749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝐺
47	44, 38, 46	nfbr 4629	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥 𝑔 ∘𝑟 ≤ 𝐺
48	43, 47	nfan 1816	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺)
49	42, 48	nfan 1816	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))
50	35, 49	nfan 1816	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺)))
51		eldifi 3694	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → 𝑥 ∈ ℝ)
52		i1ff 23249	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ dom ∫1 → 𝑓:ℝ⟶ℝ)
53	24, 52	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → 𝑓:ℝ⟶ℝ)
54		ffn 5958	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:ℝ⟶ℝ → 𝑓 Fn ℝ)
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → 𝑓 Fn ℝ)
56		i1ff 23249	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
57	25, 56	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → 𝑔:ℝ⟶ℝ)
58		ffn 5958	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔:ℝ⟶ℝ → 𝑔 Fn ℝ)
59	57, 58	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → 𝑔 Fn ℝ)
60		reex 9906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℝ ∈ V
61	60	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → ℝ ∈ V)
62		inidm 3784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℝ ∩ ℝ) = ℝ
63		eqidd 2611	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) = (𝑓‘𝑥))
64		eqidd 2611	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) = (𝑔‘𝑥))
65	55, 59, 61, 61, 62, 63, 64	ofval 6804	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) = ((𝑓‘𝑥) + (𝑔‘𝑥)))
66	51, 65	sylan2 490	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) = ((𝑓‘𝑥) + (𝑔‘𝑥)))
67		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) ∈ ℝ)
68	53, 51, 67	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑥) ∈ ℝ)
69		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ∈ ℝ)
70	57, 51, 69	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑔‘𝑥) ∈ ℝ)
71	68, 70	readdcld 9948	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈ ℝ)
72	71	rexrd 9968	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈ ℝ*)
73	72	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈ ℝ*)
74	68	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℝ)
75	74	rexrd 9968	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℝ*)
76		iccssxr 12127	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0[,]+∞) ⊆ ℝ*
77		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐻:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ (0[,]+∞))
78	27, 51, 77	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝐻‘𝑥) ∈ (0[,]+∞))
79	76, 78	sseldi 3566	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝐻‘𝑥) ∈ ℝ*)
80	79	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈ ℝ*)
81	70	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℝ)
82		0red 9920	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℝ)
83		simprrr 801	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → 𝑔 ∘𝑟 ≤ 𝐺)
84	60	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → ℝ ∈ V)
85		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑔‘𝑥) ∈ V
86	85	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ∈ V)
87		ssun2 3739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵)
88	87, 4	syl5sseqr 3617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → 𝐵 ⊆ 𝑈)
89	88	sselda 3568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈)
90	89	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈)
91	90, 13	syldan 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
92	14	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐵) → 0 ∈ (0[,]+∞))
93	91, 92	ifclda 4070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐵, 𝐶, 0) ∈ (0[,]+∞))
94	93	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐵, 𝐶, 0) ∈ (0[,]+∞))
95		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → 𝑔 Fn ℝ)
96		dffn5 6151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑔 Fn ℝ ↔ 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔‘𝑥)))
97	95, 96	sylib 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔‘𝑥)))
98	7	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0)))
99	84, 86, 94, 97, 98	ofrfval2 6813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → (𝑔 ∘𝑟 ≤ 𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)))
100	59, 99	syldan 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → (𝑔 ∘𝑟 ≤ 𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)))
101	83, 100	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → ∀𝑥 ∈ ℝ (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))
102	101	r19.21bi 2916	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))
103	51, 102	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))
104	103	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))
105		eldifn 3695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → ¬ 𝑥 ∈ (𝐴 ∩ 𝐵))
106	105	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ¬ 𝑥 ∈ (𝐴 ∩ 𝐵))
107		elin 3758	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
108	106, 107	sylnib 317	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
109		imnan 437	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
110	108, 109	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
111	110	imp 444	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ 𝐵)
112	111	iffalsed 4047	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐵, 𝐶, 0) = 0)
113	104, 112	breqtrd 4609	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ 0)
114	81, 82, 74, 113	leadd2dd 10521	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ ((𝑓‘𝑥) + 0))
115	74	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℂ)
116	115	addid1d 10115	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + 0) = (𝑓‘𝑥))
117	114, 116	breqtrd 4609	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝑓‘𝑥))
118		simprlr 799	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → 𝑓 ∘𝑟 ≤ 𝐹)
119	60	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → ℝ ∈ V)
120		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓‘𝑥) ∈ V
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) ∈ V)
122		ssun1 3738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
123	122, 4	syl5sseqr 3617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
124	123	sselda 3568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈)
125	124	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈)
126	125, 13	syldan 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))
127	14	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ (0[,]+∞))
128	126, 127	ifclda 4070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,]+∞))
129	128	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,]+∞))
130		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → 𝑓 Fn ℝ)
131		dffn5 6151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 Fn ℝ ↔ 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓‘𝑥)))
132	130, 131	sylib 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓‘𝑥)))
133	6	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)))
134	119, 121, 129, 132, 133	ofrfval2 6813	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → (𝑓 ∘𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)))
135	55, 134	syldan 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → (𝑓 ∘𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)))
136	118, 135	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))
137	136	r19.21bi 2916	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))
138	51, 137	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))
139	138	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))
140	123	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → 𝐴 ⊆ 𝑈)
141	140	sselda 3568	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈)
142	141	iftrued 4044	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑈, 𝐶, 0) = 𝐶)
143		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
144	16	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞))
145	8	fvmpt2 6200	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞)) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0))
146	143, 144, 145	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0))
147	51, 146	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0))
148	147	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0))
149		iftrue 4042	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶)
150	149	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶)
151	142, 148, 150	3eqtr4d 2654	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝐴, 𝐶, 0))
152	139, 151	breqtrrd 4611	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ (𝐻‘𝑥))
153	73, 75, 80, 117, 152	xrletrd 11869	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝐻‘𝑥))
154	72	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈ ℝ*)
155	70	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℝ)
156	155	rexrd 9968	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℝ*)
157	79	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈ ℝ*)
158	68	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℝ)
159		0red 9920	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ ℝ)
160	138	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))
161		iffalse 4045	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 0)
162	161	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 𝐶, 0) = 0)
163	160, 162	breqtrd 4609	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ 0)
164	158, 159, 155, 163	leadd1dd 10520	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (0 + (𝑔‘𝑥)))
165	155	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℂ)
166	165	addid2d 10116	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (0 + (𝑔‘𝑥)) = (𝑔‘𝑥))
167	164, 166	breqtrd 4609	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝑔‘𝑥))
168	103	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))
169	147	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0))
170	4	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → 𝑈 = (𝐴 ∪ 𝐵))
171	170	eleq2d 2673	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ (𝐴 ∪ 𝐵)))
172		biorf 419	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
173		elun 3715	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
174	172, 173	syl6rbbr 278	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
175	174	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
176	171, 175	bitrd 267	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ 𝐵))
177	176	ifbid 4058	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑈, 𝐶, 0) = if(𝑥 ∈ 𝐵, 𝐶, 0))
178	169, 177	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝐵, 𝐶, 0))
179	168, 178	breqtrrd 4611	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ (𝐻‘𝑥))
180	154, 156, 157, 167, 179	xrletrd 11869	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝐻‘𝑥))
181	153, 180	pm2.61dan 828	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝐻‘𝑥))
182	66, 181	eqbrtrd 4605	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥))
183	182	ex 449	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → (𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥)))
184	50, 183	ralrimi 2940	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → ∀𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥))
185		nfv 1830	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥)
186		nfcv 2751	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝑓 ∘𝑓 + 𝑔)‘𝑦)
187		nfcv 2751	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥 ≤
188		nfmpt1 4675	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0))
189	8, 188	nfcxfr 2749	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝐻
190		nfcv 2751	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝑦
191	189, 190	nffv 6110	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝐻‘𝑦)
192	186, 187, 191	nfbr 4629	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥((𝑓 ∘𝑓 + 𝑔)‘𝑦) ≤ (𝐻‘𝑦)
193		fveq2 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) = ((𝑓 ∘𝑓 + 𝑔)‘𝑦))
194		fveq2 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦))
195	193, 194	breq12d 4596	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥) ↔ ((𝑓 ∘𝑓 + 𝑔)‘𝑦) ≤ (𝐻‘𝑦)))
196	185, 192, 195	cbvral 3143	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥) ↔ ∀𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))((𝑓 ∘𝑓 + 𝑔)‘𝑦) ≤ (𝐻‘𝑦))
197	184, 196	sylib 207	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → ∀𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))((𝑓 ∘𝑓 + 𝑔)‘𝑦) ≤ (𝐻‘𝑦))
198	197	r19.21bi 2916	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓 ∘𝑓 + 𝑔)‘𝑦) ≤ (𝐻‘𝑦))
199	27, 28, 33, 34, 198	itg2uba 23316	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → (∫1‘(𝑓 ∘𝑓 + 𝑔)) ≤ (∫2‘𝐻))
200	26, 199	eqbrtrrd 4607	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → ((∫1‘𝑓) + (∫1‘𝑔)) ≤ (∫2‘𝐻))
201	23	adantrr 749	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → (∫1‘𝑓) ∈ ℝ)
202		itg1cl 23258	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ dom ∫1 → (∫1‘𝑔) ∈ ℝ)
203	25, 202	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → (∫1‘𝑔) ∈ ℝ)
204	20	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → (∫2‘𝐻) ∈ ℝ)
205	201, 203, 204	leaddsub2d 10508	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → (((∫1‘𝑓) + (∫1‘𝑔)) ≤ (∫2‘𝐻) ↔ (∫1‘𝑔) ≤ ((∫2‘𝐻) − (∫1‘𝑓))))
206	200, 205	mpbid 221	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺))) → (∫1‘𝑔) ≤ ((∫2‘𝐻) − (∫1‘𝑓)))
207	206	anassrs 678	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹)) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟 ≤ 𝐺)) → (∫1‘𝑔) ≤ ((∫2‘𝐻) − (∫1‘𝑓)))
208	207	expr 641	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹)) ∧ 𝑔 ∈ dom ∫1) → (𝑔 ∘𝑟 ≤ 𝐺 → (∫1‘𝑔) ≤ ((∫2‘𝐻) − (∫1‘𝑓))))
209	208	ralrimiva 2949	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹)) → ∀𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝐺 → (∫1‘𝑔) ≤ ((∫2‘𝐻) − (∫1‘𝑓))))
210	93, 7	fmptd 6292	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞))
211	210	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹)) → 𝐺:ℝ⟶(0[,]+∞))
212	21, 23	resubcld 10337	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹)) → ((∫2‘𝐻) − (∫1‘𝑓)) ∈ ℝ)
213	212	rexrd 9968	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹)) → ((∫2‘𝐻) − (∫1‘𝑓)) ∈ ℝ*)
214		itg2leub 23307	. . . . . . . . 9 ⊢ ((𝐺:ℝ⟶(0[,]+∞) ∧ ((∫2‘𝐻) − (∫1‘𝑓)) ∈ ℝ*) → ((∫2‘𝐺) ≤ ((∫2‘𝐻) − (∫1‘𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝐺 → (∫1‘𝑔) ≤ ((∫2‘𝐻) − (∫1‘𝑓)))))
215	211, 213, 214	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹)) → ((∫2‘𝐺) ≤ ((∫2‘𝐻) − (∫1‘𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝐺 → (∫1‘𝑔) ≤ ((∫2‘𝐻) − (∫1‘𝑓)))))
216	209, 215	mpbird 246	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹)) → (∫2‘𝐺) ≤ ((∫2‘𝐻) − (∫1‘𝑓)))
217	12, 21, 23, 216	lesubd 10510	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟 ≤ 𝐹)) → (∫1‘𝑓) ≤ ((∫2‘𝐻) − (∫2‘𝐺)))
218	217	expr 641	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑓 ∘𝑟 ≤ 𝐹 → (∫1‘𝑓) ≤ ((∫2‘𝐻) − (∫2‘𝐺))))
219	218	ralrimiva 2949	. . . 4 ⊢ (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟 ≤ 𝐹 → (∫1‘𝑓) ≤ ((∫2‘𝐻) − (∫2‘𝐺))))
220	128, 6	fmptd 6292	. . . . 5 ⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞))
221	20, 10	resubcld 10337	. . . . . 6 ⊢ (𝜑 → ((∫2‘𝐻) − (∫2‘𝐺)) ∈ ℝ)
222	221	rexrd 9968	. . . . 5 ⊢ (𝜑 → ((∫2‘𝐻) − (∫2‘𝐺)) ∈ ℝ*)
223		itg2leub 23307	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ ((∫2‘𝐻) − (∫2‘𝐺)) ∈ ℝ*) → ((∫2‘𝐹) ≤ ((∫2‘𝐻) − (∫2‘𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟 ≤ 𝐹 → (∫1‘𝑓) ≤ ((∫2‘𝐻) − (∫2‘𝐺)))))
224	220, 222, 223	syl2anc 691	. . . 4 ⊢ (𝜑 → ((∫2‘𝐹) ≤ ((∫2‘𝐻) − (∫2‘𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟 ≤ 𝐹 → (∫1‘𝑓) ≤ ((∫2‘𝐻) − (∫2‘𝐺)))))
225	219, 224	mpbird 246	. . 3 ⊢ (𝜑 → (∫2‘𝐹) ≤ ((∫2‘𝐻) − (∫2‘𝐺)))
226		leaddsub 10383	. . . 4 ⊢ (((∫2‘𝐹) ∈ ℝ ∧ (∫2‘𝐺) ∈ ℝ ∧ (∫2‘𝐻) ∈ ℝ) → (((∫2‘𝐹) + (∫2‘𝐺)) ≤ (∫2‘𝐻) ↔ (∫2‘𝐹) ≤ ((∫2‘𝐻) − (∫2‘𝐺))))
227	9, 10, 20, 226	syl3anc 1318	. . 3 ⊢ (𝜑 → (((∫2‘𝐹) + (∫2‘𝐺)) ≤ (∫2‘𝐻) ↔ (∫2‘𝐹) ≤ ((∫2‘𝐻) − (∫2‘𝐺))))
228	225, 227	mpbird 246	. 2 ⊢ (𝜑 → ((∫2‘𝐹) + (∫2‘𝐺)) ≤ (∫2‘𝐻))
229		itg2cl 23305	. . . 4 ⊢ (𝐻:ℝ⟶(0[,]+∞) → (∫2‘𝐻) ∈ ℝ*)
230	17, 229	syl 17	. . 3 ⊢ (𝜑 → (∫2‘𝐻) ∈ ℝ*)
231	18	rexrd 9968	. . 3 ⊢ (𝜑 → ((∫2‘𝐹) + (∫2‘𝐺)) ∈ ℝ*)
232		xrletri3 11861	. . 3 ⊢ (((∫2‘𝐻) ∈ ℝ* ∧ ((∫2‘𝐹) + (∫2‘𝐺)) ∈ ℝ*) → ((∫2‘𝐻) = ((∫2‘𝐹) + (∫2‘𝐺)) ↔ ((∫2‘𝐻) ≤ ((∫2‘𝐹) + (∫2‘𝐺)) ∧ ((∫2‘𝐹) + (∫2‘𝐺)) ≤ (∫2‘𝐻))))
233	230, 231, 232	syl2anc 691	. 2 ⊢ (𝜑 → ((∫2‘𝐻) = ((∫2‘𝐹) + (∫2‘𝐺)) ↔ ((∫2‘𝐻) ≤ ((∫2‘𝐹) + (∫2‘𝐺)) ∧ ((∫2‘𝐹) + (∫2‘𝐺)) ≤ (∫2‘𝐻))))
234	11, 228, 233	mpbir2and 959	1 ⊢ (𝜑 → (∫2‘𝐻) = ((∫2‘𝐹) + (∫2‘𝐺)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ∘_𝑓 cof 6793   ∘_𝑟 cofr 6794  ℝcr 9814  0cc0 9815   + caddc 9818  +∞cpnf 9950  ℝ^*cxr 9952   ≤ cle 9954   − cmin 10145  [,]cicc 12049  vol*covol 23038  volcvol 23039  ∫₁citg1 23190  ∫₂citg2 23191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-ofr 6796  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-rest 15906  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-cmp 21000  df-ovol 23040  df-vol 23041  df-mbf 23194  df-itg1 23195  df-itg2 23196

This theorem is referenced by:  itg2cnlem2  23335  itgsplit  23408  iblsplit  38858