ibladdnclem

Description: Lemma for ibladdnc ; cf ibladdlem , whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc . (Contributed by Brendan Leahy, 31-Oct-2017)

	Ref	Expression
Hypotheses	ibladdnclem.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	ibladdnclem.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
	ibladdnclem.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 = ( 𝐵 + 𝐶 ) )
	ibladdnclem.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
	ibladdnclem.6	⊢ ( 𝜑 → ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) ∈ ℝ )
	ibladdnclem.7	⊢ ( 𝜑 → ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ∈ ℝ )
Assertion	ibladdnclem	⊢ ( 𝜑 → ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		ibladdnclem.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
2		ibladdnclem.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
3		ibladdnclem.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 = ( 𝐵 + 𝐶 ) )
4		ibladdnclem.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
5		ibladdnclem.6	⊢ ( 𝜑 → ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) ∈ ℝ )
6		ibladdnclem.7	⊢ ( 𝜑 → ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ∈ ℝ )
7		ifan	⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 )
8	1 2	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
9	3 8	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ ℝ )
10		0re	⊢ 0 ∈ ℝ
11		ifcl	⊢ ( ( 𝐷 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ∈ ℝ )
12	9 10 11	sylancl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ∈ ℝ )
13	12	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ∈ ℝ^* )
14		max1	⊢ ( ( 0 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐷 , 𝐷 , 0 ) )
15	10 9 14	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ 𝐷 , 𝐷 , 0 ) )
16		elxrge0	⊢ ( if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ∈ ( 0 [,] +∞ ) ↔ ( if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ∈ ℝ^* ∧ 0 ≤ if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ) )
17	13 15 16	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ∈ ( 0 [,] +∞ ) )
18		0e0iccpnf	⊢ 0 ∈ ( 0 [,] +∞ )
19	18	a1i	⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,] +∞ ) )
20	17 19	ifclda	⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) ∈ ( 0 [,] +∞ ) )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) ∈ ( 0 [,] +∞ ) )
22	7 21	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ∈ ( 0 [,] +∞ ) )
23	22	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
24		reex	⊢ ℝ ∈ V
25	24	a1i	⊢ ( 𝜑 → ℝ ∈ V )
26		ifan	⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐵 , 𝐵 , 0 ) , 0 )
27		ifcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
28	1 10 27	sylancl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
29	10	a1i	⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ℝ )
30	28 29	ifclda	⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐵 , 𝐵 , 0 ) , 0 ) ∈ ℝ )
31	26 30	eqeltrid	⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ∈ ℝ )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ∈ ℝ )
33		ifan	⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐶 , 𝐶 , 0 ) , 0 )
34		ifcl	⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
35	2 10 34	sylancl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
36	35 29	ifclda	⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐶 , 𝐶 , 0 ) , 0 ) ∈ ℝ )
37	33 36	eqeltrid	⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ∈ ℝ )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ∈ ℝ )
39		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) )
40		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) )
41	25 32 38 39 40	offval2	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∘_f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) )
42		iftrue	⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
43		ibar	⊢ ( 𝑥 ∈ 𝐴 → ( 0 ≤ 𝐵 ↔ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) ) )
44	43	ifbid	⊢ ( 𝑥 ∈ 𝐴 → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) )
45		ibar	⊢ ( 𝑥 ∈ 𝐴 → ( 0 ≤ 𝐶 ↔ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) ) )
46	45	ifbid	⊢ ( 𝑥 ∈ 𝐴 → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) )
47	44 46	oveq12d	⊢ ( 𝑥 ∈ 𝐴 → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) )
48	42 47	eqtr2d	⊢ ( 𝑥 ∈ 𝐴 → ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
49		00id	⊢ ( 0 + 0 ) = 0
50		simpl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) → 𝑥 ∈ 𝐴 )
51	50	con3i	⊢ ( ¬ 𝑥 ∈ 𝐴 → ¬ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) )
52	51	iffalsed	⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) = 0 )
53		simpl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) → 𝑥 ∈ 𝐴 )
54	53	con3i	⊢ ( ¬ 𝑥 ∈ 𝐴 → ¬ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) )
55	54	iffalsed	⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) = 0 )
56	52 55	oveq12d	⊢ ( ¬ 𝑥 ∈ 𝐴 → ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) = ( 0 + 0 ) )
57		iffalse	⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) = 0 )
58	49 56 57	3eqtr4a	⊢ ( ¬ 𝑥 ∈ 𝐴 → ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
59	48 58	pm2.61i	⊢ ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 )
60	59	mpteq2i	⊢ ( 𝑥 ∈ ℝ ↦ ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
61	41 60	eqtrdi	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∘_f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) )
62	61	fveq2d	⊢ ( 𝜑 → ( ∫₂ ‘ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∘_f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ) = ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) )
63	4 1	mbfdm2	⊢ ( 𝜑 → 𝐴 ∈ dom vol )
64		mblss	⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
65	63 64	syl	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
66		rembl	⊢ ℝ ∈ dom vol
67	66	a1i	⊢ ( 𝜑 → ℝ ∈ dom vol )
68	31	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ∈ ℝ )
69		eldifn	⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 )
70	69	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ¬ 𝑥 ∈ 𝐴 )
71	70	intnanrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ¬ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) )
72	71	iffalsed	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) = 0 )
73	44	mpteq2ia	⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) )
74	1 4	mbfpos	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn )
75	73 74	eqeltrrid	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∈ MblFn )
76	65 67 68 72 75	mbfss	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∈ MblFn )
77		max1	⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
78	10 1 77	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
79		elrege0	⊢ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) ↔ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) )
80	28 78 79	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
81		0e0icopnf	⊢ 0 ∈ ( 0 [,) +∞ )
82	81	a1i	⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,) +∞ ) )
83	80 82	ifclda	⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐵 , 𝐵 , 0 ) , 0 ) ∈ ( 0 [,) +∞ ) )
84	26 83	eqeltrid	⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
85	84	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
86	85	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
87		max1	⊢ ( ( 0 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
88	10 2 87	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
89		elrege0	⊢ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ( 0 [,) +∞ ) ↔ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
90	35 88 89	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ( 0 [,) +∞ ) )
91	90 82	ifclda	⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐶 , 𝐶 , 0 ) , 0 ) ∈ ( 0 [,) +∞ ) )
92	33 91	eqeltrid	⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ∈ ( 0 [,) +∞ ) )
93	92	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ∈ ( 0 [,) +∞ ) )
94	93	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
95	76 86 5 94 6	itg2addnc	⊢ ( 𝜑 → ( ∫₂ ‘ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∘_f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ) = ( ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) + ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ) )
96	62 95	eqtr3d	⊢ ( 𝜑 → ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) = ( ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) + ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ) )
97	5 6	readdcld	⊢ ( 𝜑 → ( ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) + ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ) ∈ ℝ )
98	96 97	eqeltrd	⊢ ( 𝜑 → ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) ∈ ℝ )
99	28 35	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ℝ )
100	99	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ℝ^* )
101	28 35 78 88	addge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
102		elxrge0	⊢ ( ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ℝ^* ∧ 0 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
103	100 101 102	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ( 0 [,] +∞ ) )
104	103 19	ifclda	⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
105	104	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
106	105	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
107		max2	⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
108	10 1 107	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
109		max2	⊢ ( ( 0 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
110	10 2 109	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
111	1 2 28 35 108 110	le2addd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
112	3 111	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
113		breq1	⊢ ( 𝐷 = if ( 0 ≤ 𝐷 , 𝐷 , 0 ) → ( 𝐷 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ↔ if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
114		breq1	⊢ ( 0 = if ( 0 ≤ 𝐷 , 𝐷 , 0 ) → ( 0 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ↔ if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
115	113 114	ifboth	⊢ ( ( 𝐷 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∧ 0 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) → if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
116	112 101 115	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
117		iftrue	⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) = if ( 0 ≤ 𝐷 , 𝐷 , 0 ) )
118	117	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) = if ( 0 ≤ 𝐷 , 𝐷 , 0 ) )
119	42	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
120	116 118 119	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
121	120	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) )
122		0le0	⊢ 0 ≤ 0
123	122	a1i	⊢ ( ¬ 𝑥 ∈ 𝐴 → 0 ≤ 0 )
124		iffalse	⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) = 0 )
125	123 124 57	3brtr4d	⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
126	121 125	pm2.61d1	⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
127	7 126	eqbrtrid	⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
128	127	ralrimivw	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
129		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) )
130		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) )
131	25 22 105 129 130	ofrfval2	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ∘_r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) )
132	128 131	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ∘_r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) )
133		itg2le	⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ∘_r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) → ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ) ≤ ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) )
134	23 106 132 133	syl3anc	⊢ ( 𝜑 → ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ) ≤ ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) )
135		itg2lecl	⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ) ≤ ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) ) → ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ) ∈ ℝ )
136	23 98 134 135	syl3anc	⊢ ( 𝜑 → ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ) ∈ ℝ )

Metamath Proof Explorer

Theorem ibladdnclem

Proof