Theorem ibladdnclem 31991

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

Hypotheses

Ref	Expression
ibladdnclem.1	|- ( ( ph /\ x e. A ) -> B e. RR )
ibladdnclem.2	|- ( ( ph /\ x e. A ) -> C e. RR )
ibladdnclem.3	|- ( ( ph /\ x e. A ) -> D = ( B + C ) )
ibladdnclem.4	|- ( ph -> ( x e. A |-> B ) e. MblFn )
ibladdnclem.6	|- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR )
ibladdnclem.7	|- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) e. RR )

Assertion

Ref	Expression
ibladdnclem	|- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) e. RR )

Distinct variable groups:   x, A   ph, x

Allowed substitution hints:   B( x)   C( x)   D( x)

Proof of Theorem ibladdnclem

Step	Hyp	Ref	Expression
1		ifan 3926	. . . 4 |- if ( ( x e. A /\ 0 <_ D ) , D , 0 ) = if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 )
2		ibladdnclem.3	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> D = ( B + C ) )
3		ibladdnclem.1	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> B e. RR )
4		ibladdnclem.2	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> C e. RR )
5	3, 4	readdcld 9667	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( B + C ) e. RR )
6	2, 5	eqeltrd 2528	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> D e. RR )
7		0re 9640	. . . . . . . . 9 |- 0 e. RR
8		ifcl 3922	. . . . . . . . 9 |- ( ( D e. RR /\ 0 e. RR ) -> if ( 0 <_ D , D , 0 ) e. RR )
9	6, 7, 8	sylancl 667	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> if ( 0 <_ D , D , 0 ) e. RR )
10	9	rexrd 9687	. . . . . . 7 |- ( ( ph /\ x e. A ) -> if ( 0 <_ D , D , 0 ) e. RR* )
11		max1 11477	. . . . . . . 8 |- ( ( 0 e. RR /\ D e. RR ) -> 0 <_ if ( 0 <_ D , D , 0 ) )
12	7, 6, 11	sylancr 668	. . . . . . 7 |- ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ D , D , 0 ) )
13		elxrge0 11738	. . . . . . 7 |- ( if ( 0 <_ D , D , 0 ) e. ( 0 [,] +oo ) <-> ( if ( 0 <_ D , D , 0 ) e. RR* /\ 0 <_ if ( 0 <_ D , D , 0 ) ) )
14	10, 12, 13	sylanbrc 669	. . . . . 6 |- ( ( ph /\ x e. A ) -> if ( 0 <_ D , D , 0 ) e. ( 0 [,] +oo ) )
15		0e0iccpnf 11740	. . . . . . 7 |- 0 e. ( 0 [,] +oo )
16	15	a1i 11	. . . . . 6 |- ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,] +oo ) )
17	14, 16	ifclda 3912	. . . . 5 |- ( ph -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) e. ( 0 [,] +oo ) )
18	17	adantr 467	. . . 4 |- ( ( ph /\ x e. RR ) -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) e. ( 0 [,] +oo ) )
19	1, 18	syl5eqel 2532	. . 3 |- ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) e. ( 0 [,] +oo ) )
20		eqid 2450	. . 3 |- ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) )
21	19, 20	fmptd 6044	. 2 |- ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) : RR --> ( 0 [,] +oo ) )
22		reex 9627	. . . . . . . 8 |- RR e. _V
23	22	a1i 11	. . . . . . 7 |- ( ph -> RR e. _V )
24		ifan 3926	. . . . . . . . 9 |- if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 )
25		ifcl 3922	. . . . . . . . . . 11 |- ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
26	3, 7, 25	sylancl 667	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
27	7	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ -. x e. A ) -> 0 e. RR )
28	26, 27	ifclda 3912	. . . . . . . . 9 |- ( ph -> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) e. RR )
29	24, 28	syl5eqel 2532	. . . . . . . 8 |- ( ph -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. RR )
30	29	adantr 467	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. RR )
31		ifan 3926	. . . . . . . . 9 |- if ( ( x e. A /\ 0 <_ C ) , C , 0 ) = if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 )
32		ifcl 3922	. . . . . . . . . . 11 |- ( ( C e. RR /\ 0 e. RR ) -> if ( 0 <_ C , C , 0 ) e. RR )
33	4, 7, 32	sylancl 667	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. RR )
34	33, 27	ifclda 3912	. . . . . . . . 9 |- ( ph -> if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 ) e. RR )
35	31, 34	syl5eqel 2532	. . . . . . . 8 |- ( ph -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) e. RR )
36	35	adantr 467	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) e. RR )
37		eqidd 2451	. . . . . . 7 |- ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) )
38		eqidd 2451	. . . . . . 7 |- ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) )
39	23, 30, 36, 37, 38	offval2 6545	. . . . . 6 |- ( ph -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) = ( x e. RR |-> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) )
40		iftrue 3886	. . . . . . . . 9 |- ( x e. A -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
41		ibar 507	. . . . . . . . . . 11 |- ( x e. A -> ( 0 <_ B <-> ( x e. A /\ 0 <_ B ) ) )
42	41	ifbid 3902	. . . . . . . . . 10 |- ( x e. A -> if ( 0 <_ B , B , 0 ) = if ( ( x e. A /\ 0 <_ B ) , B , 0 ) )
43		ibar 507	. . . . . . . . . . 11 |- ( x e. A -> ( 0 <_ C <-> ( x e. A /\ 0 <_ C ) ) )
44	43	ifbid 3902	. . . . . . . . . 10 |- ( x e. A -> if ( 0 <_ C , C , 0 ) = if ( ( x e. A /\ 0 <_ C ) , C , 0 ) )
45	42, 44	oveq12d 6306	. . . . . . . . 9 |- ( x e. A -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) )
46	40, 45	eqtr2d 2485	. . . . . . . 8 |- ( x e. A -> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
47		00id 9805	. . . . . . . . 9 |- ( 0 + 0 ) = 0
48		simpl 459	. . . . . . . . . . . 12 |- ( ( x e. A /\ 0 <_ B ) -> x e. A )
49	48	con3i 141	. . . . . . . . . . 11 |- ( -. x e. A -> -. ( x e. A /\ 0 <_ B ) )
50	49	iffalsed 3891	. . . . . . . . . 10 |- ( -. x e. A -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = 0 )
51		simpl 459	. . . . . . . . . . . 12 |- ( ( x e. A /\ 0 <_ C ) -> x e. A )
52	51	con3i 141	. . . . . . . . . . 11 |- ( -. x e. A -> -. ( x e. A /\ 0 <_ C ) )
53	52	iffalsed 3891	. . . . . . . . . 10 |- ( -. x e. A -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) = 0 )
54	50, 53	oveq12d 6306	. . . . . . . . 9 |- ( -. x e. A -> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = ( 0 + 0 ) )
55		iffalse 3889	. . . . . . . . 9 |- ( -. x e. A -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) = 0 )
56	47, 54, 55	3eqtr4a 2510	. . . . . . . 8 |- ( -. x e. A -> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
57	46, 56	pm2.61i 168	. . . . . . 7 |- ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 )
58	57	mpteq2i 4485	. . . . . 6 |- ( x e. RR |-> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) = ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
59	39, 58	syl6eq 2500	. . . . 5 |- ( ph -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) = ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
60	59	fveq2d 5867	. . . 4 |- ( ph -> ( S.2 ` ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) ) = ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) )
61		ibladdnclem.4	. . . . . . . 8 |- ( ph -> ( x e. A |-> B ) e. MblFn )
62	61, 3	mbfdm2 22587	. . . . . . 7 |- ( ph -> A e. dom vol )
63		mblss 22478	. . . . . . 7 |- ( A e. dom vol -> A C_ RR )
64	62, 63	syl 17	. . . . . 6 |- ( ph -> A C_ RR )
65		rembl 22487	. . . . . . 7 |- RR e. dom vol
66	65	a1i 11	. . . . . 6 |- ( ph -> RR e. dom vol )
67	29	adantr 467	. . . . . 6 |- ( ( ph /\ x e. A ) -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. RR )
68		eldifn 3555	. . . . . . . . 9 |- ( x e. ( RR \ A ) -> -. x e. A )
69	68	adantl 468	. . . . . . . 8 |- ( ( ph /\ x e. ( RR \ A ) ) -> -. x e. A )
70	69	intnanrd 927	. . . . . . 7 |- ( ( ph /\ x e. ( RR \ A ) ) -> -. ( x e. A /\ 0 <_ B ) )
71	70	iffalsed 3891	. . . . . 6 |- ( ( ph /\ x e. ( RR \ A ) ) -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = 0 )
72	42	mpteq2ia 4484	. . . . . . 7 |- ( x e. A |-> if ( 0 <_ B , B , 0 ) ) = ( x e. A |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) )
73	3, 61	mbfpos 22600	. . . . . . 7 |- ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
74	72, 73	syl5eqelr 2533	. . . . . 6 |- ( ph -> ( x e. A |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) e. MblFn )
75	64, 66, 67, 71, 74	mbfss 22595	. . . . 5 |- ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) e. MblFn )
76		max1 11477	. . . . . . . . . . 11 |- ( ( 0 e. RR /\ B e. RR ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
77	7, 3, 76	sylancr 668	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
78		elrege0 11735	. . . . . . . . . 10 |- ( if ( 0 <_ B , B , 0 ) e. ( 0 [,) +oo ) <-> ( if ( 0 <_ B , B , 0 ) e. RR /\ 0 <_ if ( 0 <_ B , B , 0 ) ) )
79	26, 77, 78	sylanbrc 669	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. ( 0 [,) +oo ) )
80		0e0icopnf 11739	. . . . . . . . . 10 |- 0 e. ( 0 [,) +oo )
81	80	a1i 11	. . . . . . . . 9 |- ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,) +oo ) )
82	79, 81	ifclda 3912	. . . . . . . 8 |- ( ph -> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) e. ( 0 [,) +oo ) )
83	24, 82	syl5eqel 2532	. . . . . . 7 |- ( ph -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. ( 0 [,) +oo ) )
84	83	adantr 467	. . . . . 6 |- ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. ( 0 [,) +oo ) )
85		eqid 2450	. . . . . 6 |- ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) )
86	84, 85	fmptd 6044	. . . . 5 |- ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) : RR --> ( 0 [,) +oo ) )
87		ibladdnclem.6	. . . . 5 |- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR )
88		max1 11477	. . . . . . . . . . 11 |- ( ( 0 e. RR /\ C e. RR ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
89	7, 4, 88	sylancr 668	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
90		elrege0 11735	. . . . . . . . . 10 |- ( if ( 0 <_ C , C , 0 ) e. ( 0 [,) +oo ) <-> ( if ( 0 <_ C , C , 0 ) e. RR /\ 0 <_ if ( 0 <_ C , C , 0 ) ) )
91	33, 89, 90	sylanbrc 669	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. ( 0 [,) +oo ) )
92	91, 81	ifclda 3912	. . . . . . . 8 |- ( ph -> if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 ) e. ( 0 [,) +oo ) )
93	31, 92	syl5eqel 2532	. . . . . . 7 |- ( ph -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) e. ( 0 [,) +oo ) )
94	93	adantr 467	. . . . . 6 |- ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) e. ( 0 [,) +oo ) )
95		eqid 2450	. . . . . 6 |- ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) )
96	94, 95	fmptd 6044	. . . . 5 |- ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) : RR --> ( 0 [,) +oo ) )
97		ibladdnclem.7	. . . . 5 |- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) e. RR )
98	75, 86, 87, 96, 97	itg2addnc 31989	. . . 4 |- ( ph -> ( S.2 ` ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) ) = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) ) )
99	60, 98	eqtr3d 2486	. . 3 |- ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) ) )
100	87, 97	readdcld 9667	. . 3 |- ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) ) e. RR )
101	99, 100	eqeltrd 2528	. 2 |- ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) e. RR )
102	26, 33	readdcld 9667	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR )
103	102	rexrd 9687	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR* )
104	26, 33, 77, 89	addge0d 10186	. . . . . . 7 |- ( ( ph /\ x e. A ) -> 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
105		elxrge0 11738	. . . . . . 7 |- ( ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. ( 0 [,] +oo ) <-> ( ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR* /\ 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
106	103, 104, 105	sylanbrc 669	. . . . . 6 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. ( 0 [,] +oo ) )
107	106, 16	ifclda 3912	. . . . 5 |- ( ph -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) e. ( 0 [,] +oo ) )
108	107	adantr 467	. . . 4 |- ( ( ph /\ x e. RR ) -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) e. ( 0 [,] +oo ) )
109		eqid 2450	. . . 4 |- ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) = ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
110	108, 109	fmptd 6044	. . 3 |- ( ph -> ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
111		max2 11479	. . . . . . . . . . . . 13 |- ( ( 0 e. RR /\ B e. RR ) -> B <_ if ( 0 <_ B , B , 0 ) )
112	7, 3, 111	sylancr 668	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> B <_ if ( 0 <_ B , B , 0 ) )
113		max2 11479	. . . . . . . . . . . . 13 |- ( ( 0 e. RR /\ C e. RR ) -> C <_ if ( 0 <_ C , C , 0 ) )
114	7, 4, 113	sylancr 668	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> C <_ if ( 0 <_ C , C , 0 ) )
115	3, 4, 26, 33, 112, 114	le2addd 10229	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( B + C ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
116	2, 115	eqbrtrd 4422	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> D <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
117		breq1 4404	. . . . . . . . . . 11 |- ( D = if ( 0 <_ D , D , 0 ) -> ( D <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) <-> if ( 0 <_ D , D , 0 ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
118		breq1 4404	. . . . . . . . . . 11 |- ( 0 = if ( 0 <_ D , D , 0 ) -> ( 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) <-> if ( 0 <_ D , D , 0 ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
119	117, 118	ifboth 3916	. . . . . . . . . 10 |- ( ( D <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) /\ 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) -> if ( 0 <_ D , D , 0 ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
120	116, 104, 119	syl2anc 666	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> if ( 0 <_ D , D , 0 ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
121		iftrue 3886	. . . . . . . . . 10 |- ( x e. A -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) = if ( 0 <_ D , D , 0 ) )
122	121	adantl 468	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) = if ( 0 <_ D , D , 0 ) )
123	40	adantl 468	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
124	120, 122, 123	3brtr4d 4432	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
125	124	ex 436	. . . . . . 7 |- ( ph -> ( x e. A -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
126		0le0 10696	. . . . . . . . 9 |- 0 <_ 0
127	126	a1i 11	. . . . . . . 8 |- ( -. x e. A -> 0 <_ 0 )
128		iffalse 3889	. . . . . . . 8 |- ( -. x e. A -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) = 0 )
129	127, 128, 55	3brtr4d 4432	. . . . . . 7 |- ( -. x e. A -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
130	125, 129	pm2.61d1 163	. . . . . 6 |- ( ph -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
131	1, 130	syl5eqbr 4435	. . . . 5 |- ( ph -> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
132	131	ralrimivw 2802	. . . 4 |- ( ph -> A. x e. RR if ( ( x e. A /\ 0 <_ D ) , D , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
133		eqidd 2451	. . . . 5 |- ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) )
134		eqidd 2451	. . . . 5 |- ( ph -> ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) = ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
135	23, 19, 108, 133, 134	ofrfval2 6546	. . . 4 |- ( ph -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) <-> A. x e. RR if ( ( x e. A /\ 0 <_ D ) , D , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
136	132, 135	mpbird 236	. . 3 |- ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
137		itg2le 22690	. . 3 |- ( ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) )
138	21, 110, 136, 137	syl3anc 1267	. 2 |- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) )
139		itg2lecl 22689	. 2 |- ( ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) e. RR )
140	21, 101, 138, 139	syl3anc 1267	1 |- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) e. RR )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 371   = wceq 1443   e. wcel 1886   A.wral 2736   _Vcvv 3044   \ cdif 3400   C_ wss 3403   ifcif 3880   class class class wbr 4401   |-> cmpt 4460   dom cdm 4833   -->wf 5577   ` cfv 5581  (class class class)co 6288   oFcof 6526   oRcofr 6527   RRcr 9535   0cc0 9536   + caddc 9539   +oocpnf 9669   RR*cxr 9671   <_ cle 9673   [,)cico 11634   [,]cicc 11635   volcvol 22408  MblFncmbf 22565   S.2citg2 22567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-inf2 8143  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613  ax-pre-sup 9614  ax-addf 9615

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-fal 1449  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-disj 4373  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-se 4793  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-isom 5590  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-of 6528  df-ofr 6529  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-2o 7180  df-oadd 7183  df-er 7360  df-map 7471  df-pm 7472  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570  df-fi 7922  df-sup 7953  df-inf 7954  df-oi 8022  df-card 8370  df-cda 8595  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-2 10665  df-3 10666  df-n0 10867  df-z 10935  df-uz 11157  df-q 11262  df-rp 11300  df-xneg 11406  df-xadd 11407  df-xmul 11408  df-ioo 11636  df-ico 11638  df-icc 11639  df-fz 11782  df-fzo 11913  df-fl 12025  df-seq 12211  df-exp 12270  df-hash 12513  df-cj 13155  df-re 13156  df-im 13157  df-sqrt 13291  df-abs 13292  df-clim 13545  df-sum 13746  df-rest 15314  df-topgen 15335  df-psmet 18955  df-xmet 18956  df-met 18957  df-bl 18958  df-mopn 18959  df-top 19914  df-bases 19915  df-topon 19916  df-cmp 20395  df-ovol 22409  df-vol 22411  df-mbf 22570  df-itg1 22571  df-itg2 22572

This theorem is referenced by:  ibladdnc  31992