Theorem itg2addnc 29633

Description: Alternate proof of itg2add 21894 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 21843, 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 8804, 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 oF + 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 756	. . . . . . 7 |- ( ( f e. dom S.1 /\ ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) ) -> x = ( S.1 ` f ) )
2		itg1cl 21820	. . . . . . . 8 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
3	2	adantr 465	. . . . . . 7 |- ( ( f e. dom S.1 /\ ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR )
4	1, 3	eqeltrd 2548	. . . . . 6 |- ( ( f e. dom S.1 /\ ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) ) -> x e. RR )
5	4	rexlimiva 2944	. . . . 5 |- ( E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) -> x e. RR )
6	5	abssi 3568	. . . 4 |- { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR )
8		i1f0 21822	. . . . . 6 |- ( RR X. { 0 } ) e. dom S.1
9		3nn 10683	. . . . . . . 8 |- 3 e. NN
10		nnrp 11218	. . . . . . . 8 |- ( 3 e. NN -> 3 e. RR+ )
11		ne0i 3784	. . . . . . . 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 6012	. . . . . . . . . . . 12 |- ( ( ph /\ z e. RR ) -> ( F ` z ) e. ( 0 [,) +oo ) )
15		elrege0 11616	. . . . . . . . . . . 12 |- ( ( F ` z ) e. ( 0 [,) +oo ) <-> ( ( F ` z ) e. RR /\ 0 <_ ( F ` z ) ) )
16	14, 15	sylib 196	. . . . . . . . . . 11 |- ( ( ph /\ z e. RR ) -> ( ( F ` z ) e. RR /\ 0 <_ ( F ` z ) ) )
17	16	simprd 463	. . . . . . . . . 10 |- ( ( ph /\ z e. RR ) -> 0 <_ ( F ` z ) )
18	17	ralrimiva 2871	. . . . . . . . 9 |- ( ph -> A. z e. RR 0 <_ ( F ` z ) )
19		reex 9572	. . . . . . . . . . 11 |- RR e. _V
20	19	a1i 11	. . . . . . . . . 10 |- ( ph -> RR e. _V )
21		c0ex 9579	. . . . . . . . . . 11 |- 0 e. _V
22	21	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ z e. RR ) -> 0 e. _V )
23		eqidd 2461	. . . . . . . . . 10 |- ( ph -> ( z e. RR |-> 0 ) = ( z e. RR |-> 0 ) )
24	13	feqmptd 5911	. . . . . . . . . 10 |- ( ph -> F = ( z e. RR |-> ( F ` z ) ) )
25	20, 22, 14, 23, 24	ofrfval2 6532	. . . . . . . . 9 |- ( ph -> ( ( z e. RR |-> 0 ) oR <_ F <-> A. z e. RR 0 <_ ( F ` z ) ) )
26	18, 25	mpbird 232	. . . . . . . 8 |- ( ph -> ( z e. RR |-> 0 ) oR <_ F )
27	26	ralrimivw 2872	. . . . . . 7 |- ( ph -> A. c e. RR+ ( z e. RR |-> 0 ) oR <_ F )
28		r19.2z 3910	. . . . . . 7 |- ( ( RR+ =/= (/) /\ A. c e. RR+ ( z e. RR |-> 0 ) oR <_ F ) -> E. c e. RR+ ( z e. RR |-> 0 ) oR <_ F )
29	12, 27, 28	sylancr 663	. . . . . 6 |- ( ph -> E. c e. RR+ ( z e. RR |-> 0 ) oR <_ F )
30		fveq2 5857	. . . . . . . . . 10 |- ( f = ( RR X. { 0 } ) -> ( S.1 ` f ) = ( S.1 ` ( RR X. { 0 } ) ) )
31		itg10 21823	. . . . . . . . . 10 |- ( S.1 ` ( RR X. { 0 } ) ) = 0
32	30, 31	syl6req 2518	. . . . . . . . 9 |- ( f = ( RR X. { 0 } ) -> 0 = ( S.1 ` f ) )
33	32	biantrud 507	. . . . . . . 8 |- ( f = ( RR X. { 0 } ) -> ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F <-> ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ 0 = ( S.1 ` f ) ) ) )
34		fveq1 5856	. . . . . . . . . . . . 13 |- ( f = ( RR X. { 0 } ) -> ( f ` z ) = ( ( RR X. { 0 } ) ` z ) )
35	21	fvconst2 6107	. . . . . . . . . . . . 13 |- ( z e. RR -> ( ( RR X. { 0 } ) ` z ) = 0 )
36	34, 35	sylan9eq 2521	. . . . . . . . . . . 12 |- ( ( f = ( RR X. { 0 } ) /\ z e. RR ) -> ( f ` z ) = 0 )
37		iftrue 3938	. . . . . . . . . . . 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 4526	. . . . . . . . . 10 |- ( f = ( RR X. { 0 } ) -> ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) = ( z e. RR |-> 0 ) )
40	39	breq1d 4450	. . . . . . . . 9 |- ( f = ( RR X. { 0 } ) -> ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F <-> ( z e. RR |-> 0 ) oR <_ F ) )
41	40	rexbidv 2966	. . . . . . . 8 |- ( f = ( RR X. { 0 } ) -> ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F <-> E. c e. RR+ ( z e. RR |-> 0 ) oR <_ F ) )
42	33, 41	bitr3d 255	. . . . . . 7 |- ( f = ( RR X. { 0 } ) -> ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ 0 = ( S.1 ` f ) ) <-> E. c e. RR+ ( z e. RR |-> 0 ) oR <_ F ) )
43	42	rspcev 3207	. . . . . 6 |- ( ( ( RR X. { 0 } ) e. dom S.1 /\ E. c e. RR+ ( z e. RR |-> 0 ) oR <_ F ) -> E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ 0 = ( S.1 ` f ) ) )
44	8, 29, 43	sylancr 663	. . . . 5 |- ( ph -> E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ 0 = ( S.1 ` f ) ) )
45		eqeq1 2464	. . . . . . . 8 |- ( x = 0 -> ( x = ( S.1 ` f ) <-> 0 = ( S.1 ` f ) ) )
46	45	anbi2d 703	. . . . . . 7 |- ( x = 0 -> ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) <-> ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ 0 = ( S.1 ` f ) ) ) )
47	46	rexbidv 2966	. . . . . 6 |- ( x = 0 -> ( E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ 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 ) ) ) oR <_ F /\ 0 = ( S.1 ` f ) ) ) )
48	21, 47	elab 3243	. . . . 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 ) ) ) oR <_ 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 ) ) ) oR <_ F /\ 0 = ( S.1 ` f ) ) )
49	44, 48	sylibr 212	. . . 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } )
50		ne0i 3784	. . . 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } =/= (/) )
52		rexr 9628	. . . . . . . . . 10 |- ( x e. RR -> x e. RR* )
53	52	anim1i 568	. . . . . . . . 9 |- ( ( x e. RR /\ 0 <_ x ) -> ( x e. RR* /\ 0 <_ x ) )
54		elrege0 11616	. . . . . . . . 9 |- ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x ) )
55		elxrge0 11618	. . . . . . . . 9 |- ( x e. ( 0 [,] +oo ) <-> ( x e. RR* /\ 0 <_ x ) )
56	53, 54, 55	3imtr4i 266	. . . . . . . 8 |- ( x e. ( 0 [,) +oo ) -> x e. ( 0 [,] +oo ) )
57	56	ssriv 3501	. . . . . . 7 |- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
58		fss 5730	. . . . . . 7 |- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : RR --> ( 0 [,] +oo ) )
59	57, 58	mpan2 671	. . . . . 6 |- ( F : RR --> ( 0 [,) +oo ) -> F : RR --> ( 0 [,] +oo ) )
60		eqid 2460	. . . . . . 7 |- { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) }
61	60	itg2addnclem 29630	. . . . . 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) )
62	13, 59, 61	3syl 20	. . . . 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) )
63		itg2addnc.f3	. . . . 5 |- ( ph -> ( S.2 ` F ) e. RR )
64	62, 63	eqeltrrd 2549	. . . 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) e. RR )
65		ressxr 9626	. . . . . . 7 |- RR C_ RR*
66	6, 65	sstri 3506	. . . . . 6 |- { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR*
67		supxrub 11505	. . . . . 6 |- ( ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) )
68	66, 67	mpan 670	. . . . 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 ) ) ) oR <_ 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) )
69	68	rgen 2817	. . . 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 ) ) ) oR <_ 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < )
70		breq2 4444	. . . . . 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 ) ) ) oR <_ 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) ) )
71	70	ralbidv 2896	. . . . 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) ) )
72	71	rspcev 3207	. . . 4 |- ( ( sup ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } b <_ a )
73	64, 69, 72	sylancl 662	. . 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } b <_ a )
74		simprr 756	. . . . . . 7 |- ( ( g e. dom S.1 /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) ) -> x = ( S.1 ` g ) )
75		itg1cl 21820	. . . . . . . 8 |- ( g e. dom S.1 -> ( S.1 ` g ) e. RR )
76	75	adantr 465	. . . . . . 7 |- ( ( g e. dom S.1 /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) ) -> ( S.1 ` g ) e. RR )
77	74, 76	eqeltrd 2548	. . . . . 6 |- ( ( g e. dom S.1 /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) ) -> x e. RR )
78	77	rexlimiva 2944	. . . . 5 |- ( E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) -> x e. RR )
79	78	abssi 3568	. . . 4 |- { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } C_ RR
80	79	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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } C_ RR )
81		itg2addnc.g2	. . . . . . . . . . . . 13 |- ( ph -> G : RR --> ( 0 [,) +oo ) )
82	81	ffvelrnda 6012	. . . . . . . . . . . 12 |- ( ( ph /\ z e. RR ) -> ( G ` z ) e. ( 0 [,) +oo ) )
83		elrege0 11616	. . . . . . . . . . . 12 |- ( ( G ` z ) e. ( 0 [,) +oo ) <-> ( ( G ` z ) e. RR /\ 0 <_ ( G ` z ) ) )
84	82, 83	sylib 196	. . . . . . . . . . 11 |- ( ( ph /\ z e. RR ) -> ( ( G ` z ) e. RR /\ 0 <_ ( G ` z ) ) )
85	84	simprd 463	. . . . . . . . . 10 |- ( ( ph /\ z e. RR ) -> 0 <_ ( G ` z ) )
86	85	ralrimiva 2871	. . . . . . . . 9 |- ( ph -> A. z e. RR 0 <_ ( G ` z ) )
87	81	feqmptd 5911	. . . . . . . . . 10 |- ( ph -> G = ( z e. RR |-> ( G ` z ) ) )
88	20, 22, 82, 23, 87	ofrfval2 6532	. . . . . . . . 9 |- ( ph -> ( ( z e. RR |-> 0 ) oR <_ G <-> A. z e. RR 0 <_ ( G ` z ) ) )
89	86, 88	mpbird 232	. . . . . . . 8 |- ( ph -> ( z e. RR |-> 0 ) oR <_ G )
90	89	ralrimivw 2872	. . . . . . 7 |- ( ph -> A. d e. RR+ ( z e. RR |-> 0 ) oR <_ G )
91		r19.2z 3910	. . . . . . 7 |- ( ( RR+ =/= (/) /\ A. d e. RR+ ( z e. RR |-> 0 ) oR <_ G ) -> E. d e. RR+ ( z e. RR |-> 0 ) oR <_ G )
92	12, 90, 91	sylancr 663	. . . . . 6 |- ( ph -> E. d e. RR+ ( z e. RR |-> 0 ) oR <_ G )
93		fveq2 5857	. . . . . . . . . 10 |- ( g = ( RR X. { 0 } ) -> ( S.1 ` g ) = ( S.1 ` ( RR X. { 0 } ) ) )
94	93, 31	syl6req 2518	. . . . . . . . 9 |- ( g = ( RR X. { 0 } ) -> 0 = ( S.1 ` g ) )
95	94	biantrud 507	. . . . . . . 8 |- ( g = ( RR X. { 0 } ) -> ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G <-> ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ 0 = ( S.1 ` g ) ) ) )
96		fveq1 5856	. . . . . . . . . . . . 13 |- ( g = ( RR X. { 0 } ) -> ( g ` z ) = ( ( RR X. { 0 } ) ` z ) )
97	96, 35	sylan9eq 2521	. . . . . . . . . . . 12 |- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> ( g ` z ) = 0 )
98		iftrue 3938	. . . . . . . . . . . 12 |- ( ( g ` z ) = 0 -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) = 0 )
99	97, 98	syl 16	. . . . . . . . . . 11 |- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) = 0 )
100	99	mpteq2dva 4526	. . . . . . . . . 10 |- ( g = ( RR X. { 0 } ) -> ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) = ( z e. RR |-> 0 ) )
101	100	breq1d 4450	. . . . . . . . 9 |- ( g = ( RR X. { 0 } ) -> ( ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G <-> ( z e. RR |-> 0 ) oR <_ G ) )
102	101	rexbidv 2966	. . . . . . . 8 |- ( g = ( RR X. { 0 } ) -> ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G <-> E. d e. RR+ ( z e. RR |-> 0 ) oR <_ G ) )
103	95, 102	bitr3d 255	. . . . . . 7 |- ( g = ( RR X. { 0 } ) -> ( ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ 0 = ( S.1 ` g ) ) <-> E. d e. RR+ ( z e. RR |-> 0 ) oR <_ G ) )
104	103	rspcev 3207	. . . . . 6 |- ( ( ( RR X. { 0 } ) e. dom S.1 /\ E. d e. RR+ ( z e. RR |-> 0 ) oR <_ G ) -> E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ 0 = ( S.1 ` g ) ) )
105	8, 92, 104	sylancr 663	. . . . 5 |- ( ph -> E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ 0 = ( S.1 ` g ) ) )
106		eqeq1 2464	. . . . . . . 8 |- ( x = 0 -> ( x = ( S.1 ` g ) <-> 0 = ( S.1 ` g ) ) )
107	106	anbi2d 703	. . . . . . 7 |- ( x = 0 -> ( ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) <-> ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ 0 = ( S.1 ` g ) ) ) )
108	107	rexbidv 2966	. . . . . 6 |- ( x = 0 -> ( E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ 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 ) ) ) oR <_ G /\ 0 = ( S.1 ` g ) ) ) )
109	21, 108	elab 3243	. . . . 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 ) ) ) oR <_ 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 ) ) ) oR <_ G /\ 0 = ( S.1 ` g ) ) )
110	105, 109	sylibr 212	. . . 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } )
111		ne0i 3784	. . . 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 ) ) ) oR <_ 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } =/= (/) )
112	110, 111	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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } =/= (/) )
113		fss 5730	. . . . . . 7 |- ( ( G : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> G : RR --> ( 0 [,] +oo ) )
114	57, 113	mpan2 671	. . . . . 6 |- ( G : RR --> ( 0 [,) +oo ) -> G : RR --> ( 0 [,] +oo ) )
115		eqid 2460	. . . . . . 7 |- { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) }
116	115	itg2addnclem 29630	. . . . . 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) )
117	81, 114, 116	3syl 20	. . . . 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) )
118		itg2addnc.g3	. . . . 5 |- ( ph -> ( S.2 ` G ) e. RR )
119	117, 118	eqeltrrd 2549	. . . 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) e. RR )
120	79, 65	sstri 3506	. . . . . 6 |- { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } C_ RR*
121		supxrub 11505	. . . . . 6 |- ( ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) )
122	120, 121	mpan 670	. . . . 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 ) ) ) oR <_ 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) )
123	122	rgen 2817	. . . 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 ) ) ) oR <_ 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } , RR* , < )
124		breq2 4444	. . . . . 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 ) ) ) oR <_ 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) ) )
125	124	ralbidv 2896	. . . . 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } , RR* , < ) ) )
126	125	rspcev 3207	. . . 4 |- ( ( sup ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } b <_ a )
127	119, 123, 126	sylancl 662	. . 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } b <_ a )
128		eqid 2460	. . 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } s = ( t + u ) }
129	7, 51, 73, 80, 112, 127, 128	supadd 29605	. 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } s = ( t + u ) } , RR , < ) )
130		supxrre 11508	. . . . 5 |- ( ( { x | E. f e. dom S.1 ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } , RR , < ) )
131	7, 51, 73, 130	syl3anc 1223	. . . 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 ) ) ) oR <_ 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } , RR , < ) )
132	62, 131	eqtrd 2501	. . 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) } , RR , < ) )
133		supxrre 11508	. . . . 5 |- ( ( { x | E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } , RR , < ) )
134	80, 112, 127, 133	syl3anc 1223	. . . 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 ) ) ) oR <_ 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } , RR , < ) )
135	117, 134	eqtrd 2501	. . 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } , RR , < ) )
136	132, 135	oveq12d 6293	. 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 ) ) ) oR <_ 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 ) ) ) oR <_ G /\ x = ( S.1 ` g ) ) } , RR , < ) ) )
137		ge0addcl 11621	. . . . . . 7 |- ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
138	57, 137	sseldi 3495	. . . . . 6 |- ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,] +oo ) )
139	138	adantl 466	. . . . 5 |- ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) e. ( 0 [,] +oo ) )
140		inidm 3700	. . . . 5 |- ( RR i^i RR ) = RR
141	139, 13, 81, 20, 20, 140	off 6529	. . . 4 |- ( ph -> ( F oF + G ) : RR --> ( 0 [,] +oo ) )
142		eqid 2460	. . . . 5 |- { s | E. h e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + 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 ) ) ) oR <_ ( F oF + G ) /\ s = ( S.1 ` h ) ) }
143	142	itg2addnclem 29630	. . . 4 |- ( ( F oF + G ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( F oF + G ) ) = sup ( { s | E. h e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) /\ s = ( S.1 ` h ) ) } , RR* , < ) )
144	141, 143	syl 16	. . 3 |- ( ph -> ( S.2 ` ( F oF + G ) ) = sup ( { s | E. h e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) /\ s = ( S.1 ` h ) ) } , RR* , < ) )
145		itg2addnc.f1	. . . . . . . 8 |- ( ph -> F e. MblFn )
146	145, 13, 63, 81, 118	itg2addnclem3 29632	. . . . . . 7 |- ( ph -> ( E. h e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + 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 ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) ) )
147		simpl 457	. . . . . . . . . . . . . 14 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> f e. dom S.1 )
148		simpr 461	. . . . . . . . . . . . . 14 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> g e. dom S.1 )
149	147, 148	i1fadd 21830	. . . . . . . . . . . . 13 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( f oF + g ) e. dom S.1 )
150	149	ad3antlr 730	. . . . . . . . . . . 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 ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) ) /\ s = ( t + u ) ) -> ( f oF + g ) e. dom S.1 )
151		reeanv 3022	. . . . . . . . . . . . . . . . 17 |- ( E. c e. RR+ E. d e. RR+ ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G ) <-> ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G ) )
152	151	biimpri 206	. . . . . . . . . . . . . . . 16 |- ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G ) -> E. c e. RR+ E. d e. RR+ ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G ) )
153	152	ad2ant2r 746	. . . . . . . . . . . . . . 15 |- ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) -> E. c e. RR+ E. d e. RR+ ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G ) )
154		ifcl 3974	. . . . . . . . . . . . . . . . . . 19 |- ( ( c e. RR+ /\ d e. RR+ ) -> if ( c <_ d , c , d ) e. RR+ )
155	154	ad2antlr 726	. . . . . . . . . . . . . . . . . 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 ) ) ) oR <_ F /\ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G ) ) -> if ( c <_ d , c , d ) e. RR+ )
156		breq1 4443	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 0 = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) -> ( 0 <_ ( F ` z ) <-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) ) )
157	156	anbi1d 704	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
158	157	imbi1d 317	. . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
159		breq1 4443	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
160	159	anbi1d 704	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
161	160	imbi1d 317	. . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
162		breq1 4443	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 0 = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( 0 <_ ( G ` z ) <-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) )
163	162	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
164	163	imbi1d 317	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
165		breq1 4443	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
166	165	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
167	166	imbi1d 317	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
168		oveq12 6284	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f ` z ) = 0 /\ ( g ` z ) = 0 ) -> ( ( f ` z ) + ( g ` z ) ) = ( 0 + 0 ) )
169		00id 9743	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 0 + 0 ) = 0
170	168, 169	syl6eq 2517	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f ` z ) = 0 /\ ( g ` z ) = 0 ) -> ( ( f ` z ) + ( g ` z ) ) = 0 )
171		iftrue 3938	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f ` z ) + ( g ` z ) ) = 0 -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) = 0 )
172	170, 171	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 )
173	172	adantll 713	. . . . . . . . . . . . . . . . . . . . . . . . 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 )
174		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> ph )
175	15	simplbi 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( F ` z ) e. ( 0 [,) +oo ) -> ( F ` z ) e. RR )
176	14, 175	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ z e. RR ) -> ( F ` z ) e. RR )
177	83	simplbi 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( G ` z ) e. ( 0 [,) +oo ) -> ( G ` z ) e. RR )
178	82, 177	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ z e. RR ) -> ( G ` z ) e. RR )
179	176, 178, 17, 85	addge0d 10117	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ z e. RR ) -> 0 <_ ( ( F ` z ) + ( G ` z ) ) )
180	174, 179	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
181	180	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
182	173, 181	eqbrtrd 4460	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
183	182	a1d 25	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
184	180	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
185		oveq1 6282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( f ` z ) = 0 -> ( ( f ` z ) + ( g ` z ) ) = ( 0 + ( g ` z ) ) )
186		simplrr 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> g e. dom S.1 )
187		i1ff 21811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( g e. dom S.1 -> g : RR --> RR )
188	187	ffvelrnda 6012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( g e. dom S.1 /\ z e. RR ) -> ( g ` z ) e. RR )
189	186, 188	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
190	189	recnd 9611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
191	190	addid2d 9769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
192	185, 191	sylan9eqr 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
193	192	oveq1d 6290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
194	193	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
195	154	rpred 11245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( c e. RR+ /\ d e. RR+ ) -> if ( c <_ d , c , d ) e. RR )
196	195	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
197	189, 196	readdcld 9612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
198	197	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
199	174, 178	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
200	199	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
201	174, 176	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
202	201, 199	readdcld 9612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
203	202	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
204		simplrr 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> d e. RR+ )
205	204	rpred 11245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> d e. RR )
206		rpre 11215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( c e. RR+ -> c e. RR )
207		rpre 11215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( d e. RR+ -> d e. RR )
208		min2 11379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( c e. RR /\ d e. RR ) -> if ( c <_ d , c , d ) <_ d )
209	206, 207, 208	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( c e. RR+ /\ d e. RR+ ) -> if ( c <_ d , c , d ) <_ d )
210	209	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
211	196, 205, 189, 210	leadd2dd 10156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
212	189, 205	readdcld 9612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
213		letr 9667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
214	197, 212, 199, 213	syl3anc 1223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
215	211, 214	mpand 675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
216	215	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
217	178, 176	addge02d 10130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ z e. RR ) -> ( 0 <_ ( F ` z ) <-> ( G ` z ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
218	17, 217	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ z e. RR ) -> ( G ` z ) <_ ( ( F ` z ) + ( G ` z ) ) )
219	174, 218	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
220	219	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
221	198, 200, 203, 216, 220	letrd 9727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
222	221	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
223	194, 222	eqbrtrd 4460	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
224		breq1 4443	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
225		breq1 4443	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
226	224, 225	ifboth 3968	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
227	184, 223, 226	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
228	227	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
229	228	adantld 467	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
230	229	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
231	164, 167, 183, 230	ifbothda 3967	. . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
232	162	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
233	232	imbi1d 317	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( ( ( ( ( f ` z ) + c ) <_ ( F ` z ) /\ 0 <_ ( G ` z ) )