Theorem itg2addnc 26158

Description: Alternate proof of itg2add 19604 using the "buffer zone" definition from the first lemma, in which every simple function in the set is divided into to by dividing its buffer by a third and finding the largest allowable function locked to a grid laid out in increments of the new, smaller buffer up to the original simple function. The measurability of this function follows from that of the augend, and subtracting it from the original simple function yields another simple function by i1fsub 19553, which is allowable by the fact that the grid must have a mark between one third and two thirds the original buffer. This has two advantages over the current approach: first, eliminating ax-cc 8271, and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017.) (Revised by Brendan Leahy, 13-Mar-2018.)

Hypotheses

Ref	Expression
itg2addnc.f1	|- ( ph -> F e. MblFn )
itg2addnc.f2	|- ( ph -> F : RR --> ( 0 [,) +oo ) )
itg2addnc.f3	|- ( ph -> ( S.2 ` F ) e. RR )
itg2addnc.g2	|- ( ph -> G : RR --> ( 0 [,) +oo ) )
itg2addnc.g3	|- ( ph -> ( S.2 ` G ) e. RR )

Assertion

Ref	Expression
itg2addnc	|- ( ph -> ( S.2 ` ( F o F + G ) ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )

Proof of Theorem itg2addnc

Dummy variables t s u x y z f g h a b c d are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprr 734	. . . . . . 7 |- ( ( f e. dom S.1 /\ ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) ) -> x = ( S.1 ` f ) )
2		itg1cl 19530	. . . . . . . 8 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
3	2	adantr 452	. . . . . . 7 |- ( ( f e. dom S.1 /\ ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR )
4	1, 3	eqeltrd 2478	. . . . . 6 |- ( ( f e. dom S.1 /\ ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) ) -> x e. RR )
5	4	rexlimiva 2785	. . . . 5 |- ( E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) -> x e. RR )
6	5	abssi 3378	. . . 4 |- { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } C_ RR
7	6	a1i 11	. . 3 |- ( ph -> { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } C_ RR )
8		i1f0 19532	. . . . . 6 |- ( RR X. { 0 } ) e. dom S.1
9		3nn 10090	. . . . . . . 8 |- 3 e. NN
10		nnrp 10577	. . . . . . . 8 |- ( 3 e. NN -> 3 e. RR+ )
11		ne0i 3594	. . . . . . . 8 |- ( 3 e. RR+ -> RR+ =/= (/) )
12	9, 10, 11	mp2b 10	. . . . . . 7 |- RR+ =/= (/)
13		itg2addnc.f2	. . . . . . . . . . . . 13 |- ( ph -> F : RR --> ( 0 [,) +oo ) )
14	13	ffvelrnda 5829	. . . . . . . . . . . 12 |- ( ( ph /\ z e. RR ) -> ( F ` z ) e. ( 0 [,) +oo ) )
15		elrege0 10963	. . . . . . . . . . . 12 |- ( ( F ` z ) e. ( 0 [,) +oo ) <-> ( ( F ` z ) e. RR /\ 0 <_ ( F ` z ) ) )
16	14, 15	sylib 189	. . . . . . . . . . 11 |- ( ( ph /\ z e. RR ) -> ( ( F ` z ) e. RR /\ 0 <_ ( F ` z ) ) )
17	16	simprd 450	. . . . . . . . . 10 |- ( ( ph /\ z e. RR ) -> 0 <_ ( F ` z ) )
18	17	ralrimiva 2749	. . . . . . . . 9 |- ( ph -> A. z e. RR 0 <_ ( F ` z ) )
19		reex 9037	. . . . . . . . . . 11 |- RR e. _V
20	19	a1i 11	. . . . . . . . . 10 |- ( ph -> RR e. _V )
21		c0ex 9041	. . . . . . . . . . 11 |- 0 e. _V
22	21	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ z e. RR ) -> 0 e. _V )
23		eqidd 2405	. . . . . . . . . 10 |- ( ph -> ( z e. RR |-> 0 ) = ( z e. RR |-> 0 ) )
24	13	feqmptd 5738	. . . . . . . . . 10 |- ( ph -> F = ( z e. RR |-> ( F ` z ) ) )
25	20, 22, 14, 23, 24	ofrfval2 6282	. . . . . . . . 9 |- ( ph -> ( ( z e. RR |-> 0 ) o R <_ F <-> A. z e. RR 0 <_ ( F ` z ) ) )
26	18, 25	mpbird 224	. . . . . . . 8 |- ( ph -> ( z e. RR |-> 0 ) o R <_ F )
27	26	ralrimivw 2750	. . . . . . 7 |- ( ph -> A. c e. RR+ ( z e. RR |-> 0 ) o R <_ F )
28		r19.2z 3677	. . . . . . 7 |- ( ( RR+ =/= (/) /\ A. c e. RR+ ( z e. RR |-> 0 ) o R <_ F ) -> E. c e. RR+ ( z e. RR |-> 0 ) o R <_ F )
29	12, 27, 28	sylancr 645	. . . . . 6 |- ( ph -> E. c e. RR+ ( z e. RR |-> 0 ) o R <_ F )
30		fveq2 5687	. . . . . . . . . 10 |- ( f = ( RR X. { 0 } ) -> ( S.1 ` f ) = ( S.1 ` ( RR X. { 0 } ) ) )
31		itg10 19533	. . . . . . . . . 10 |- ( S.1 ` ( RR X. { 0 } ) ) = 0
32	30, 31	syl6req 2453	. . . . . . . . 9 |- ( f = ( RR X. { 0 } ) -> 0 = ( S.1 ` f ) )
33	32	biantrud 494	. . . . . . . 8 |- ( f = ( RR X. { 0 } ) -> ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F <-> ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ 0 = ( S.1 ` f ) ) ) )
34		fveq1 5686	. . . . . . . . . . . . 13 |- ( f = ( RR X. { 0 } ) -> ( f ` z ) = ( ( RR X. { 0 } ) ` z ) )
35	21	fvconst2 5906	. . . . . . . . . . . . 13 |- ( z e. RR -> ( ( RR X. { 0 } ) ` z ) = 0 )
36	34, 35	sylan9eq 2456	. . . . . . . . . . . 12 |- ( ( f = ( RR X. { 0 } ) /\ z e. RR ) -> ( f ` z ) = 0 )
37		iftrue 3705	. . . . . . . . . . . 12 |- ( ( f ` z ) = 0 -> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) = 0 )
38	36, 37	syl 16	. . . . . . . . . . 11 |- ( ( f = ( RR X. { 0 } ) /\ z e. RR ) -> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) = 0 )
39	38	mpteq2dva 4255	. . . . . . . . . 10 |- ( f = ( RR X. { 0 } ) -> ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) = ( z e. RR |-> 0 ) )
40	39	breq1d 4182	. . . . . . . . 9 |- ( f = ( RR X. { 0 } ) -> ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F <-> ( z e. RR |-> 0 ) o R <_ F ) )
41	40	rexbidv 2687	. . . . . . . 8 |- ( f = ( RR X. { 0 } ) -> ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F <-> E. c e. RR+ ( z e. RR |-> 0 ) o R <_ F ) )
42	33, 41	bitr3d 247	. . . . . . 7 |- ( f = ( RR X. { 0 } ) -> ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ 0 = ( S.1 ` f ) ) <-> E. c e. RR+ ( z e. RR |-> 0 ) o R <_ F ) )
43	42	rspcev 3012	. . . . . 6 |- ( ( ( RR X. { 0 } ) e. dom S.1 /\ E. c e. RR+ ( z e. RR |-> 0 ) o R <_ F ) -> E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ 0 = ( S.1 ` f ) ) )
44	8, 29, 43	sylancr 645	. . . . 5 |- ( ph -> E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ 0 = ( S.1 ` f ) ) )
45		eqeq1 2410	. . . . . . . 8 |- ( x = 0 -> ( x = ( S.1 ` f ) <-> 0 = ( S.1 ` f ) ) )
46	45	anbi2d 685	. . . . . . 7 |- ( x = 0 -> ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) <-> ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ 0 = ( S.1 ` f ) ) ) )
47	46	rexbidv 2687	. . . . . 6 |- ( x = 0 -> ( E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) <-> E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ 0 = ( S.1 ` f ) ) ) )
48	21, 47	elab 3042	. . . . 5 |- ( 0 e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } <-> E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ 0 = ( S.1 ` f ) ) )
49	44, 48	sylibr 204	. . . 4 |- ( ph -> 0 e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } )
50		ne0i 3594	. . . 4 |- ( 0 e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } -> { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } =/= (/) )
51	49, 50	syl 16	. . 3 |- ( ph -> { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } =/= (/) )
52		icossicc 24082	. . . . . . 7 |- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
53		fss 5558	. . . . . . 7 |- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : RR --> ( 0 [,] +oo ) )
54	52, 53	mpan2 653	. . . . . 6 |- ( F : RR --> ( 0 [,) +oo ) -> F : RR --> ( 0 [,] +oo ) )
55		eqid 2404	. . . . . . 7 |- { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } = { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) }
56	55	itg2addnclem 26155	. . . . . 6 |- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) = sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) )
57	13, 54, 56	3syl 19	. . . . 5 |- ( ph -> ( S.2 ` F ) = sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) )
58		itg2addnc.f3	. . . . 5 |- ( ph -> ( S.2 ` F ) e. RR )
59	57, 58	eqeltrrd 2479	. . . 4 |- ( ph -> sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) e. RR )
60		ressxr 9085	. . . . . . 7 |- RR C_ RR*
61	6, 60	sstri 3317	. . . . . 6 |- { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } C_ RR*
62		supxrub 10859	. . . . . 6 |- ( ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } C_ RR* /\ b e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } ) -> b <_ sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) )
63	61, 62	mpan 652	. . . . 5 |- ( b e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } -> b <_ sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) )
64	63	rgen 2731	. . . 4 |- A. b e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } b <_ sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < )
65		breq2 4176	. . . . . 6 |- ( a = sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) -> ( b <_ a <-> b <_ sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) ) )
66	65	ralbidv 2686	. . . . 5 |- ( a = sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) -> ( A. b e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } b <_ a <-> A. b e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } b <_ sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) ) )
67	66	rspcev 3012	. . . 4 |- ( ( sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) e. RR /\ A. b e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } b <_ sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) ) -> E. a e. RR A. b e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } b <_ a )
68	59, 64, 67	sylancl 644	. . 3 |- ( ph -> E. a e. RR A. b e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } b <_ a )
69		simprr 734	. . . . . . 7 |- ( ( g e. dom S.1 /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) ) -> x = ( S.1 ` g ) )
70		itg1cl 19530	. . . . . . . 8 |- ( g e. dom S.1 -> ( S.1 ` g ) e. RR )
71	70	adantr 452	. . . . . . 7 |- ( ( g e. dom S.1 /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) ) -> ( S.1 ` g ) e. RR )
72	69, 71	eqeltrd 2478	. . . . . 6 |- ( ( g e. dom S.1 /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) ) -> x e. RR )
73	72	rexlimiva 2785	. . . . 5 |- ( E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) -> x e. RR )
74	73	abssi 3378	. . . 4 |- { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } C_ RR
75	74	a1i 11	. . 3 |- ( ph -> { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } C_ RR )
76		itg2addnc.g2	. . . . . . . . . . . . 13 |- ( ph -> G : RR --> ( 0 [,) +oo ) )
77	76	ffvelrnda 5829	. . . . . . . . . . . 12 |- ( ( ph /\ z e. RR ) -> ( G ` z ) e. ( 0 [,) +oo ) )
78		elrege0 10963	. . . . . . . . . . . 12 |- ( ( G ` z ) e. ( 0 [,) +oo ) <-> ( ( G ` z ) e. RR /\ 0 <_ ( G ` z ) ) )
79	77, 78	sylib 189	. . . . . . . . . . 11 |- ( ( ph /\ z e. RR ) -> ( ( G ` z ) e. RR /\ 0 <_ ( G ` z ) ) )
80	79	simprd 450	. . . . . . . . . 10 |- ( ( ph /\ z e. RR ) -> 0 <_ ( G ` z ) )
81	80	ralrimiva 2749	. . . . . . . . 9 |- ( ph -> A. z e. RR 0 <_ ( G ` z ) )
82	76	feqmptd 5738	. . . . . . . . . 10 |- ( ph -> G = ( z e. RR |-> ( G ` z ) ) )
83	20, 22, 77, 23, 82	ofrfval2 6282	. . . . . . . . 9 |- ( ph -> ( ( z e. RR |-> 0 ) o R <_ G <-> A. z e. RR 0 <_ ( G ` z ) ) )
84	81, 83	mpbird 224	. . . . . . . 8 |- ( ph -> ( z e. RR |-> 0 ) o R <_ G )
85	84	ralrimivw 2750	. . . . . . 7 |- ( ph -> A. d e. RR+ ( z e. RR |-> 0 ) o R <_ G )
86		r19.2z 3677	. . . . . . 7 |- ( ( RR+ =/= (/) /\ A. d e. RR+ ( z e. RR |-> 0 ) o R <_ G ) -> E. d e. RR+ ( z e. RR |-> 0 ) o R <_ G )
87	12, 85, 86	sylancr 645	. . . . . 6 |- ( ph -> E. d e. RR+ ( z e. RR |-> 0 ) o R <_ G )
88		fveq2 5687	. . . . . . . . . 10 |- ( g = ( RR X. { 0 } ) -> ( S.1 ` g ) = ( S.1 ` ( RR X. { 0 } ) ) )
89	88, 31	syl6req 2453	. . . . . . . . 9 |- ( g = ( RR X. { 0 } ) -> 0 = ( S.1 ` g ) )
90	89	biantrud 494	. . . . . . . 8 |- ( g = ( RR X. { 0 } ) -> ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G <-> ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ 0 = ( S.1 ` g ) ) ) )
91		fveq1 5686	. . . . . . . . . . . . 13 |- ( g = ( RR X. { 0 } ) -> ( g ` z ) = ( ( RR X. { 0 } ) ` z ) )
92	91, 35	sylan9eq 2456	. . . . . . . . . . . 12 |- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> ( g ` z ) = 0 )
93		iftrue 3705	. . . . . . . . . . . 12 |- ( ( g ` z ) = 0 -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) = 0 )
94	92, 93	syl 16	. . . . . . . . . . 11 |- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) = 0 )
95	94	mpteq2dva 4255	. . . . . . . . . 10 |- ( g = ( RR X. { 0 } ) -> ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) = ( z e. RR |-> 0 ) )
96	95	breq1d 4182	. . . . . . . . 9 |- ( g = ( RR X. { 0 } ) -> ( ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G <-> ( z e. RR |-> 0 ) o R <_ G ) )
97	96	rexbidv 2687	. . . . . . . 8 |- ( g = ( RR X. { 0 } ) -> ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G <-> E. d e. RR+ ( z e. RR |-> 0 ) o R <_ G ) )
98	90, 97	bitr3d 247	. . . . . . 7 |- ( g = ( RR X. { 0 } ) -> ( ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ 0 = ( S.1 ` g ) ) <-> E. d e. RR+ ( z e. RR |-> 0 ) o R <_ G ) )
99	98	rspcev 3012	. . . . . 6 |- ( ( ( RR X. { 0 } ) e. dom S.1 /\ E. d e. RR+ ( z e. RR |-> 0 ) o R <_ G ) -> E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ 0 = ( S.1 ` g ) ) )
100	8, 87, 99	sylancr 645	. . . . 5 |- ( ph -> E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ 0 = ( S.1 ` g ) ) )
101		eqeq1 2410	. . . . . . . 8 |- ( x = 0 -> ( x = ( S.1 ` g ) <-> 0 = ( S.1 ` g ) ) )
102	101	anbi2d 685	. . . . . . 7 |- ( x = 0 -> ( ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) <-> ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ 0 = ( S.1 ` g ) ) ) )
103	102	rexbidv 2687	. . . . . 6 |- ( x = 0 -> ( E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) <-> E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ 0 = ( S.1 ` g ) ) ) )
104	21, 103	elab 3042	. . . . 5 |- ( 0 e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } <-> E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ 0 = ( S.1 ` g ) ) )
105	100, 104	sylibr 204	. . . 4 |- ( ph -> 0 e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } )
106		ne0i 3594	. . . 4 |- ( 0 e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } -> { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } =/= (/) )
107	105, 106	syl 16	. . 3 |- ( ph -> { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } =/= (/) )
108		fss 5558	. . . . . . 7 |- ( ( G : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> G : RR --> ( 0 [,] +oo ) )
109	52, 108	mpan2 653	. . . . . 6 |- ( G : RR --> ( 0 [,) +oo ) -> G : RR --> ( 0 [,] +oo ) )
110		eqid 2404	. . . . . . 7 |- { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } = { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) }
111	110	itg2addnclem 26155	. . . . . 6 |- ( G : RR --> ( 0 [,] +oo ) -> ( S.2 ` G ) = sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) )
112	76, 109, 111	3syl 19	. . . . 5 |- ( ph -> ( S.2 ` G ) = sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) )
113		itg2addnc.g3	. . . . 5 |- ( ph -> ( S.2 ` G ) e. RR )
114	112, 113	eqeltrrd 2479	. . . 4 |- ( ph -> sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) e. RR )
115	74, 60	sstri 3317	. . . . . 6 |- { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } C_ RR*
116		supxrub 10859	. . . . . 6 |- ( ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } C_ RR* /\ b e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } ) -> b <_ sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) )
117	115, 116	mpan 652	. . . . 5 |- ( b e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } -> b <_ sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) )
118	117	rgen 2731	. . . 4 |- A. b e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } b <_ sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR* , < )
119		breq2 4176	. . . . . 6 |- ( a = sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) -> ( b <_ a <-> b <_ sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) ) )
120	119	ralbidv 2686	. . . . 5 |- ( a = sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) -> ( A. b e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } b <_ a <-> A. b e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } b <_ sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) ) )
121	120	rspcev 3012	. . . 4 |- ( ( sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) e. RR /\ A. b e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } b <_ sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) ) -> E. a e. RR A. b e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } b <_ a )
122	114, 118, 121	sylancl 644	. . 3 |- ( ph -> E. a e. RR A. b e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } b <_ a )
123		eqid 2404	. . 3 |- { s | E. t e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } E. u e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } s = ( t + u ) } = { s | E. t e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } E. u e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } s = ( t + u ) }
124	7, 51, 68, 75, 107, 122, 123	supadd 26138	. 2 |- ( ph -> ( sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR , < ) + sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR , < ) ) = sup ( { s | E. t e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } E. u e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } s = ( t + u ) } , RR , < ) )
125		supxrre 10862	. . . . 5 |- ( ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } C_ RR /\ { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } =/= (/) /\ E. a e. RR A. b e. { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } b <_ a ) -> sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) = sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR , < ) )
126	7, 51, 68, 125	syl3anc 1184	. . . 4 |- ( ph -> sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) = sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR , < ) )
127	57, 126	eqtrd 2436	. . 3 |- ( ph -> ( S.2 ` F ) = sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR , < ) )
128		supxrre 10862	. . . . 5 |- ( ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } C_ RR /\ { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } =/= (/) /\ E. a e. RR A. b e. { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } b <_ a ) -> sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) = sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR , < ) )
129	75, 107, 122, 128	syl3anc 1184	. . . 4 |- ( ph -> sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) = sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR , < ) )
130	112, 129	eqtrd 2436	. . 3 |- ( ph -> ( S.2 ` G ) = sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR , < ) )
131	127, 130	oveq12d 6058	. 2 |- ( ph -> ( ( S.2 ` F ) + ( S.2 ` G ) ) = ( sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) } , RR , < ) + sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ x = ( S.1 ` g ) ) } , RR , < ) ) )
132		rexr 9086	. . . . . . . . . 10 |- ( x e. RR -> x e. RR* )
133	132	anim1i 552	. . . . . . . . 9 |- ( ( x e. RR /\ 0 <_ x ) -> ( x e. RR* /\ 0 <_ x ) )
134		elrege0 10963	. . . . . . . . 9 |- ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x ) )
135		elxrge0 10964	. . . . . . . . 9 |- ( x e. ( 0 [,] +oo ) <-> ( x e. RR* /\ 0 <_ x ) )
136	133, 134, 135	3imtr4i 258	. . . . . . . 8 |- ( x e. ( 0 [,) +oo ) -> x e. ( 0 [,] +oo ) )
137	136	ssriv 3312	. . . . . . 7 |- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
138		ge0addcl 10965	. . . . . . 7 |- ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
139	137, 138	sseldi 3306	. . . . . 6 |- ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,] +oo ) )
140	139	adantl 453	. . . . 5 |- ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) e. ( 0 [,] +oo ) )
141		inidm 3510	. . . . 5 |- ( RR i^i RR ) = RR
142	140, 13, 76, 20, 20, 141	off 6279	. . . 4 |- ( ph -> ( F o F + G ) : RR --> ( 0 [,] +oo ) )
143		eqid 2404	. . . . 5 |- { s | E. h e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) o R <_ ( F o F + G ) /\ s = ( S.1 ` h ) ) } = { s | E. h e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) o R <_ ( F o F + G ) /\ s = ( S.1 ` h ) ) }
144	143	itg2addnclem 26155	. . . 4 |- ( ( F o F + G ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( F o F + G ) ) = sup ( { s | E. h e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) o R <_ ( F o F + G ) /\ s = ( S.1 ` h ) ) } , RR* , < ) )
145	142, 144	syl 16	. . 3 |- ( ph -> ( S.2 ` ( F o F + G ) ) = sup ( { s | E. h e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) o R <_ ( F o F + G ) /\ s = ( S.1 ` h ) ) } , RR* , < ) )
146		itg2addnc.f1	. . . . . . . 8 |- ( ph -> F e. MblFn )
147	146, 13, 58, 76, 113	itg2addnclem3 26157	. . . . . . 7 |- ( ph -> ( E. h e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) o R <_ ( F o F + G ) /\ s = ( S.1 ` h ) ) -> E. t E. u ( E. f e. dom S.1 E. g e. dom S.1 ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) ) )
148		simpl 444	. . . . . . . . . . . . . 14 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> f e. dom S.1 )
149		simpr 448	. . . . . . . . . . . . . 14 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> g e. dom S.1 )
150	148, 149	i1fadd 19540	. . . . . . . . . . . . 13 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( f o F + g ) e. dom S.1 )
151	150	ad3antlr 712	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ u = ( S.1 ` g ) ) ) ) /\ s = ( t + u ) ) -> ( f o F + g ) e. dom S.1 )
152		reeanv 2835	. . . . . . . . . . . . . . . . 17 |- ( E. c e. RR+ E. d e. RR+ ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G ) <-> ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G ) )
153	152	biimpri 198	. . . . . . . . . . . . . . . 16 |- ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G ) -> E. c e. RR+ E. d e. RR+ ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G ) )
154	153	ad2ant2r 728	. . . . . . . . . . . . . . 15 |- ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G /\ u = ( S.1 ` g ) ) ) -> E. c e. RR+ E. d e. RR+ ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G ) )
155		ifcl 3735	. . . . . . . . . . . . . . . . . . 19 |- ( ( c e. RR+ /\ d e. RR+ ) -> if ( c <_ d , c , d ) e. RR+ )
156	155	ad2antlr 708	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) o R <_ F /\ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) o R <_ G ) ) -> if ( c <_ d , c , d ) e. RR+ )
157		breq1 4175	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 0 = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) -> ( 0 <_ ( F ` z ) <-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) ) )
158	157	anbi1d 686	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) -> ( ( 0 <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) <-> ( if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) ) )
159	158	imbi1d 309	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 0 = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) -> ( ( ( 0 <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) <-> ( ( if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) ) )
160		breq1 4175	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( f ` z ) + c ) = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) -> ( ( ( f ` z ) + c ) <_ ( F ` z ) <-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) ) )
161	160	anbi1d 686	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( f ` z ) + c ) = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) -> ( ( ( ( f ` z ) + c ) <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) <-> ( if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) ) )
162	161	imbi1d 309	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( f ` z ) + c ) = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) -> ( ( ( ( ( f ` z ) + c ) <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) <-> ( ( if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) ) )
163		breq1 4175	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 0 = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( 0 <_ ( G ` z ) <-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) )
164	163	anbi2d 685	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 0 = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( ( 0 <_ ( F ` z ) /\ 0 <_ ( G ` z ) ) <-> ( 0 <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) ) )
165	164	imbi1d 309	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( ( ( 0 <_ ( F ` z ) /\ 0 <_ ( G ` z ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) <-> ( ( 0 <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) ) )
166		breq1 4175	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( g ` z ) + d ) = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( ( ( g ` z ) + d ) <_ ( G ` z ) <-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) )
167	166	anbi2d 685	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( g ` z ) + d ) = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( ( 0 <_ ( F ` z ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) <-> ( 0 <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) ) )
168	167	imbi1d 309	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( g ` z ) + d ) = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( ( ( 0 <_ ( F ` z ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) <-> ( ( 0 <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) ) )
169		oveq12 6049	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f ` z ) = 0 /\ ( g ` z ) = 0 ) -> ( ( f ` z ) + ( g ` z ) ) = ( 0 + 0 ) )
170		00id 9197	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 0 + 0 ) = 0
171	169, 170	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f ` z ) = 0 /\ ( g ` z ) = 0 ) -> ( ( f ` z ) + ( g ` z ) ) = 0 )
172		iftrue 3705	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f ` z ) + ( g ` z ) ) = 0 -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) = 0 )
173	171, 172	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( f ` z ) = 0 /\ ( g ` z ) = 0 ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) = 0 )
174	173	adantll 695	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) /\ ( g ` z ) = 0 ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) = 0 )
175		simpll 731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> ph )
176	15	simplbi 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( F ` z ) e. ( 0 [,) +oo ) -> ( F ` z ) e. RR )
177	14, 176	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ z e. RR ) -> ( F ` z ) e. RR )
178	78	simplbi 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( G ` z ) e. ( 0 [,) +oo ) -> ( G ` z ) e. RR )
179	77, 178	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ z e. RR ) -> ( G ` z ) e. RR )
180	177, 179, 17, 80	addge0d 9558	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ z e. RR ) -> 0 <_ ( ( F ` z ) + ( G ` z ) ) )
181	175, 180	sylan 458	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> 0 <_ ( ( F ` z ) + ( G ` z ) ) )
182	181	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) /\ ( g ` z ) = 0 ) -> 0 <_ ( ( F ` z ) + ( G ` z ) ) )
183	174, 182	eqbrtrd 4192	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) /\ ( g ` z ) = 0 ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) )
184	183	a1d 23	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) /\ ( g ` z ) = 0 ) -> ( ( 0 <_ ( F ` z ) /\ 0 <_ ( G ` z ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
185	181	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> 0 <_ ( ( F ` z ) + ( G ` z ) ) )
186		oveq1 6047	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( f ` z ) = 0 -> ( ( f ` z ) + ( g ` z ) ) = ( 0 + ( g ` z ) ) )
187		simplrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> g e. dom S.1 )
188		i1ff 19521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( g e. dom S.1 -> g : RR --> RR )
189	188	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( g e. dom S.1 /\ z e. RR ) -> ( g ` z ) e. RR )
190	187, 189	sylan 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( g ` z ) e. RR )
191	190	recnd 9070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( g ` z ) e. CC )
192	191	addid2d 9223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( 0 + ( g ` z ) ) = ( g ` z ) )
193	186, 192	sylan9eqr 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) -> ( ( f ` z ) + ( g ` z ) ) = ( g ` z ) )
194	193	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) -> ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) = ( ( g ` z ) + if ( c <_ d , c , d ) ) )
195	194	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) = ( ( g ` z ) + if ( c <_ d , c , d ) ) )
196	155	rpred 10604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( c e. RR+ /\ d e. RR+ ) -> if ( c <_ d , c , d ) e. RR )
197	196	ad2antlr 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> if ( c <_ d , c , d ) e. RR )
198	190, 197	readdcld 9071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( g ` z ) + if ( c <_ d , c , d ) ) e. RR )
199	198	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> ( ( g ` z ) + if ( c <_ d , c , d ) ) e. RR )
200	175, 179	sylan 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( G ` z ) e. RR )
201	200	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> ( G ` z ) e. RR )
202	175, 177	sylan 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( F ` z ) e. RR )
203	202, 200	readdcld 9071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( F ` z ) + ( G ` z ) ) e. RR )
204	203	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> ( ( F ` z ) + ( G ` z ) ) e. RR )
205		simplrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> d e. RR+ )
206	205	rpred 10604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> d e. RR )
207		rpre 10574	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( c e. RR+ -> c e. RR )
208		rpre 10574	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( d e. RR+ -> d e. RR )
209		min2 10733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( c e. RR /\ d e. RR ) -> if ( c <_ d , c , d ) <_ d )
210	207, 208, 209	syl2an 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( c e. RR+ /\ d e. RR+ ) -> if ( c <_ d , c , d ) <_ d )
211	210	ad2antlr 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> if ( c <_ d , c , d ) <_ d )
212	197, 206, 190, 211	leadd2dd 9597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( g ` z ) + if ( c <_ d , c , d ) ) <_ ( ( g ` z ) + d ) )
213	190, 206	readdcld 9071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( g ` z ) + d ) e. RR )
214		letr 9123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( g ` z ) + if ( c <_ d , c , d ) ) e. RR /\ ( ( g ` z ) + d ) e. RR /\ ( G ` z ) e. RR ) -> ( ( ( ( g ` z ) + if ( c <_ d , c , d ) ) <_ ( ( g ` z ) + d ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> ( ( g ` z ) + if ( c <_ d , c , d ) ) <_ ( G ` z ) ) )
215	198, 213, 200, 214	syl3anc 1184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( ( ( g ` z ) + if ( c <_ d , c , d ) ) <_ ( ( g ` z ) + d ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> ( ( g ` z ) + if ( c <_ d , c , d ) ) <_ ( G ` z ) ) )
216	212, 215	mpand 657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( ( g ` z ) + d ) <_ ( G ` z ) -> ( ( g ` z ) + if ( c <_ d , c , d ) ) <_ ( G ` z ) ) )
217	216	imp 419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> ( ( g ` z ) + if ( c <_ d , c , d ) ) <_ ( G ` z ) )
218	179, 177	addge02d 9571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ z e. RR ) -> ( 0 <_ ( F ` z ) <-> ( G ` z ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
219	17, 218	mpbid 202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ z e. RR ) -> ( G ` z ) <_ ( ( F ` z ) + ( G ` z ) ) )
220	175, 219	sylan 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( G ` z ) <_ ( ( F ` z ) + ( G ` z ) ) )
221	220	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> ( G ` z ) <_ ( ( F ` z ) + ( G ` z ) ) )
222	199, 201, 204, 217, 221	letrd 9183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> ( ( g ` z ) + if ( c <_ d , c , d ) ) <_ ( ( F ` z ) + ( G ` z ) ) )
223	222	adantlr 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> ( ( g ` z ) + if ( c <_ d , c , d ) ) <_ ( ( F ` z ) + ( G ` z ) ) )
224	195, 223	eqbrtrd 4192	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) <_ ( ( F ` z ) + ( G ` z ) ) )
225		breq1 4175	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 0 = if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) -> ( 0 <_ ( ( F ` z ) + ( G ` z ) ) <-> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
226		breq1 4175	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) = if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) -> ( ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) <_ ( ( F ` z ) + ( G ` z ) ) <-> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
227	225, 226	ifboth 3730	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( 0 <_ ( ( F ` z ) + ( G ` z ) ) /\ ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) )
228	185, 224, 227	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) )
229	228	ex 424	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) -> ( ( ( g ` z ) + d ) <_ ( G ` z ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
230	229	adantld 454	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) -> ( ( 0 <_ ( F ` z ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
231	230	adantr 452	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) /\ -. ( g ` z ) = 0 ) -> ( ( 0 <_ ( F ` z ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
232	165, 168, 184, 231	ifbothda 3729	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( f ` z ) = 0 ) -> ( ( 0 <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
233	163	anbi2d 685	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 0 = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( ( ( ( f ` z ) + c ) <_ ( F ` z ) /\ 0 <_ ( G ` z ) ) <-> ( ( ( f ` z ) + c ) <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) ) )
234	233	imbi1d 309	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( ( ( ( ( f ` z