Theorem itg2addnc 32060

Description: Alternate proof of itg2add 22796 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 22745, 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 8883, 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 774	. . . . . . 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 22722	. . . . . . . 8 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
3	2	adantr 472	. . . . . . 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 2549	. . . . . 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 2868	. . . . 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 3490	. . . 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 22724	. . . . . 6 |- ( RR X. { 0 } ) e. dom S.1
9		3nn 10791	. . . . . . . 8 |- 3 e. NN
10		nnrp 11334	. . . . . . . 8 |- ( 3 e. NN -> 3 e. RR+ )
11		ne0i 3728	. . . . . . . 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 6037	. . . . . . . . . . . 12 |- ( ( ph /\ z e. RR ) -> ( F ` z ) e. ( 0 [,) +oo ) )
15		elrege0 11764	. . . . . . . . . . . 12 |- ( ( F ` z ) e. ( 0 [,) +oo ) <-> ( ( F ` z ) e. RR /\ 0 <_ ( F ` z ) ) )
16	14, 15	sylib 201	. . . . . . . . . . 11 |- ( ( ph /\ z e. RR ) -> ( ( F ` z ) e. RR /\ 0 <_ ( F ` z ) ) )
17	16	simprd 470	. . . . . . . . . 10 |- ( ( ph /\ z e. RR ) -> 0 <_ ( F ` z ) )
18	17	ralrimiva 2809	. . . . . . . . 9 |- ( ph -> A. z e. RR 0 <_ ( F ` z ) )
19		reex 9648	. . . . . . . . . . 11 |- RR e. _V
20	19	a1i 11	. . . . . . . . . 10 |- ( ph -> RR e. _V )
21		c0ex 9655	. . . . . . . . . . 11 |- 0 e. _V
22	21	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ z e. RR ) -> 0 e. _V )
23		eqidd 2472	. . . . . . . . . 10 |- ( ph -> ( z e. RR |-> 0 ) = ( z e. RR |-> 0 ) )
24	13	feqmptd 5932	. . . . . . . . . 10 |- ( ph -> F = ( z e. RR |-> ( F ` z ) ) )
25	20, 22, 14, 23, 24	ofrfval2 6568	. . . . . . . . 9 |- ( ph -> ( ( z e. RR |-> 0 ) oR <_ F <-> A. z e. RR 0 <_ ( F ` z ) ) )
26	18, 25	mpbird 240	. . . . . . . 8 |- ( ph -> ( z e. RR |-> 0 ) oR <_ F )
27	26	ralrimivw 2810	. . . . . . 7 |- ( ph -> A. c e. RR+ ( z e. RR |-> 0 ) oR <_ F )
28		r19.2z 3849	. . . . . . 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 676	. . . . . 6 |- ( ph -> E. c e. RR+ ( z e. RR |-> 0 ) oR <_ F )
30		fveq2 5879	. . . . . . . . . 10 |- ( f = ( RR X. { 0 } ) -> ( S.1 ` f ) = ( S.1 ` ( RR X. { 0 } ) ) )
31		itg10 22725	. . . . . . . . . 10 |- ( S.1 ` ( RR X. { 0 } ) ) = 0
32	30, 31	syl6req 2522	. . . . . . . . 9 |- ( f = ( RR X. { 0 } ) -> 0 = ( S.1 ` f ) )
33	32	biantrud 515	. . . . . . . 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 5878	. . . . . . . . . . . . 13 |- ( f = ( RR X. { 0 } ) -> ( f ` z ) = ( ( RR X. { 0 } ) ` z ) )
35	21	fvconst2 6136	. . . . . . . . . . . . 13 |- ( z e. RR -> ( ( RR X. { 0 } ) ` z ) = 0 )
36	34, 35	sylan9eq 2525	. . . . . . . . . . . 12 |- ( ( f = ( RR X. { 0 } ) /\ z e. RR ) -> ( f ` z ) = 0 )
37	36	iftrued 3880	. . . . . . . . . . 11 |- ( ( f = ( RR X. { 0 } ) /\ z e. RR ) -> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) = 0 )
38	37	mpteq2dva 4482	. . . . . . . . . 10 |- ( f = ( RR X. { 0 } ) -> ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) = ( z e. RR |-> 0 ) )
39	38	breq1d 4405	. . . . . . . . 9 |- ( f = ( RR X. { 0 } ) -> ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F <-> ( z e. RR |-> 0 ) oR <_ F ) )
40	39	rexbidv 2892	. . . . . . . 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 ) )
41	33, 40	bitr3d 263	. . . . . . 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 ) )
42	41	rspcev 3136	. . . . . 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 ) ) )
43	8, 29, 42	sylancr 676	. . . . 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 ) ) )
44		eqeq1 2475	. . . . . . . 8 |- ( x = 0 -> ( x = ( S.1 ` f ) <-> 0 = ( S.1 ` f ) ) )
45	44	anbi2d 718	. . . . . . 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 ) ) ) )
46	45	rexbidv 2892	. . . . . 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 ) ) ) )
47	21, 46	elab 3173	. . . . 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 ) ) )
48	43, 47	sylibr 217	. . . 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 ) ) } )
49		ne0i 3728	. . . 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 ) ) } =/= (/) )
50	48, 49	syl 17	. . 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 ) ) } =/= (/) )
51		icossicc 11746	. . . . . . 7 |- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
52		fss 5749	. . . . . . 7 |- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : RR --> ( 0 [,] +oo ) )
53	51, 52	mpan2 685	. . . . . 6 |- ( F : RR --> ( 0 [,) +oo ) -> F : RR --> ( 0 [,] +oo ) )
54		eqid 2471	. . . . . . 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 ) ) }
55	54	itg2addnclem 32057	. . . . . 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* , < ) )
56	13, 53, 55	3syl 18	. . . . 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* , < ) )
57		itg2addnc.f3	. . . . 5 |- ( ph -> ( S.2 ` F ) e. RR )
58	56, 57	eqeltrrd 2550	. . . 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 )
59		ressxr 9702	. . . . . . 7 |- RR C_ RR*
60	6, 59	sstri 3427	. . . . . 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*
61		supxrub 11635	. . . . . 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* , < ) )
62	60, 61	mpan 684	. . . . 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* , < ) )
63	62	rgen 2766	. . . 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* , < )
64		breq2 4399	. . . . . 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* , < ) ) )
65	64	ralbidv 2829	. . . . 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* , < ) ) )
66	65	rspcev 3136	. . . 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 )
67	58, 63, 66	sylancl 675	. . 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 )
68		simprr 774	. . . . . . 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 ) )
69		itg1cl 22722	. . . . . . . 8 |- ( g e. dom S.1 -> ( S.1 ` g ) e. RR )
70	69	adantr 472	. . . . . . 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 )
71	68, 70	eqeltrd 2549	. . . . . 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 )
72	71	rexlimiva 2868	. . . . 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 )
73	72	abssi 3490	. . . 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
74	73	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 )
75		itg2addnc.g2	. . . . . . . . . . . . 13 |- ( ph -> G : RR --> ( 0 [,) +oo ) )
76	75	ffvelrnda 6037	. . . . . . . . . . . 12 |- ( ( ph /\ z e. RR ) -> ( G ` z ) e. ( 0 [,) +oo ) )
77		elrege0 11764	. . . . . . . . . . . 12 |- ( ( G ` z ) e. ( 0 [,) +oo ) <-> ( ( G ` z ) e. RR /\ 0 <_ ( G ` z ) ) )
78	76, 77	sylib 201	. . . . . . . . . . 11 |- ( ( ph /\ z e. RR ) -> ( ( G ` z ) e. RR /\ 0 <_ ( G ` z ) ) )
79	78	simprd 470	. . . . . . . . . 10 |- ( ( ph /\ z e. RR ) -> 0 <_ ( G ` z ) )
80	79	ralrimiva 2809	. . . . . . . . 9 |- ( ph -> A. z e. RR 0 <_ ( G ` z ) )
81	75	feqmptd 5932	. . . . . . . . . 10 |- ( ph -> G = ( z e. RR |-> ( G ` z ) ) )
82	20, 22, 76, 23, 81	ofrfval2 6568	. . . . . . . . 9 |- ( ph -> ( ( z e. RR |-> 0 ) oR <_ G <-> A. z e. RR 0 <_ ( G ` z ) ) )
83	80, 82	mpbird 240	. . . . . . . 8 |- ( ph -> ( z e. RR |-> 0 ) oR <_ G )
84	83	ralrimivw 2810	. . . . . . 7 |- ( ph -> A. d e. RR+ ( z e. RR |-> 0 ) oR <_ G )
85		r19.2z 3849	. . . . . . 7 |- ( ( RR+ =/= (/) /\ A. d e. RR+ ( z e. RR |-> 0 ) oR <_ G ) -> E. d e. RR+ ( z e. RR |-> 0 ) oR <_ G )
86	12, 84, 85	sylancr 676	. . . . . 6 |- ( ph -> E. d e. RR+ ( z e. RR |-> 0 ) oR <_ G )
87		fveq2 5879	. . . . . . . . . 10 |- ( g = ( RR X. { 0 } ) -> ( S.1 ` g ) = ( S.1 ` ( RR X. { 0 } ) ) )
88	87, 31	syl6req 2522	. . . . . . . . 9 |- ( g = ( RR X. { 0 } ) -> 0 = ( S.1 ` g ) )
89	88	biantrud 515	. . . . . . . 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 ) ) ) )
90		fveq1 5878	. . . . . . . . . . . . 13 |- ( g = ( RR X. { 0 } ) -> ( g ` z ) = ( ( RR X. { 0 } ) ` z ) )
91	90, 35	sylan9eq 2525	. . . . . . . . . . . 12 |- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> ( g ` z ) = 0 )
92	91	iftrued 3880	. . . . . . . . . . 11 |- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) = 0 )
93	92	mpteq2dva 4482	. . . . . . . . . 10 |- ( g = ( RR X. { 0 } ) -> ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) = ( z e. RR |-> 0 ) )
94	93	breq1d 4405	. . . . . . . . 9 |- ( g = ( RR X. { 0 } ) -> ( ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G <-> ( z e. RR |-> 0 ) oR <_ G ) )
95	94	rexbidv 2892	. . . . . . . 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 ) )
96	89, 95	bitr3d 263	. . . . . . 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 ) )
97	96	rspcev 3136	. . . . . 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 ) ) )
98	8, 86, 97	sylancr 676	. . . . 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 ) ) )
99		eqeq1 2475	. . . . . . . 8 |- ( x = 0 -> ( x = ( S.1 ` g ) <-> 0 = ( S.1 ` g ) ) )
100	99	anbi2d 718	. . . . . . 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 ) ) ) )
101	100	rexbidv 2892	. . . . . 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 ) ) ) )
102	21, 101	elab 3173	. . . . 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 ) ) )
103	98, 102	sylibr 217	. . . 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 ) ) } )
104		ne0i 3728	. . . 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 ) ) } =/= (/) )
105	103, 104	syl 17	. . 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 ) ) } =/= (/) )
106		fss 5749	. . . . . . 7 |- ( ( G : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> G : RR --> ( 0 [,] +oo ) )
107	51, 106	mpan2 685	. . . . . 6 |- ( G : RR --> ( 0 [,) +oo ) -> G : RR --> ( 0 [,] +oo ) )
108		eqid 2471	. . . . . . 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 ) ) }
109	108	itg2addnclem 32057	. . . . . 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* , < ) )
110	75, 107, 109	3syl 18	. . . . 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* , < ) )
111		itg2addnc.g3	. . . . 5 |- ( ph -> ( S.2 ` G ) e. RR )
112	110, 111	eqeltrrd 2550	. . . 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 )
113	73, 59	sstri 3427	. . . . . 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*
114		supxrub 11635	. . . . . 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* , < ) )
115	113, 114	mpan 684	. . . . 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* , < ) )
116	115	rgen 2766	. . . 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* , < )
117		breq2 4399	. . . . . 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* , < ) ) )
118	117	ralbidv 2829	. . . . 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* , < ) ) )
119	118	rspcev 3136	. . . 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 )
120	112, 116, 119	sylancl 675	. . 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 )
121		eqid 2471	. . 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 ) }
122	7, 50, 67, 74, 105, 120, 121	supadd 10597	. 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 , < ) )
123		supxrre 11638	. . . . 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 , < ) )
124	7, 50, 67, 123	syl3anc 1292	. . . 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 , < ) )
125	56, 124	eqtrd 2505	. . 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 , < ) )
126		supxrre 11638	. . . . 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 , < ) )
127	74, 105, 120, 126	syl3anc 1292	. . . 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 , < ) )
128	110, 127	eqtrd 2505	. . 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 , < ) )
129	125, 128	oveq12d 6326	. 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 , < ) ) )
130		ge0addcl 11770	. . . . . . 7 |- ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
131	51, 130	sseldi 3416	. . . . . 6 |- ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,] +oo ) )
132	131	adantl 473	. . . . 5 |- ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) e. ( 0 [,] +oo ) )
133		inidm 3632	. . . . 5 |- ( RR i^i RR ) = RR
134	132, 13, 75, 20, 20, 133	off 6565	. . . 4 |- ( ph -> ( F oF + G ) : RR --> ( 0 [,] +oo ) )
135		eqid 2471	. . . . 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 ) ) }
136	135	itg2addnclem 32057	. . . 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* , < ) )
137	134, 136	syl 17	. . 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* , < ) )
138		itg2addnc.f1	. . . . . . . 8 |- ( ph -> F e. MblFn )
139	138, 13, 57, 75, 111	itg2addnclem3 32059	. . . . . . 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 ) ) ) )
140		simpl 464	. . . . . . . . . . . . . 14 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> f e. dom S.1 )
141		simpr 468	. . . . . . . . . . . . . 14 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> g e. dom S.1 )
142	140, 141	i1fadd 22732	. . . . . . . . . . . . 13 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( f oF + g ) e. dom S.1 )
143	142	ad3antlr 745	. . . . . . . . . . . 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 )
144		reeanv 2944	. . . . . . . . . . . . . . . . 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 ) )
145	144	biimpri 211	. . . . . . . . . . . . . . . 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 ) )
146	145	ad2ant2r 761	. . . . . . . . . . . . . . 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 ) )
147		ifcl 3914	. . . . . . . . . . . . . . . . . . 19 |- ( ( c e. RR+ /\ d e. RR+ ) -> if ( c <_ d , c , d ) e. RR+ )
148	147	ad2antlr 741	. . . . . . . . . . . . . . . . . 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+ )
149		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 0 = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) -> ( 0 <_ ( F ` z ) <-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) ) )
150	149	anbi1d 719	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
151	150	imbi1d 324	. . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
152		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
153	152	anbi1d 719	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
154	153	imbi1d 324	. . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
155		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 0 = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( 0 <_ ( G ` z ) <-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) )
156	155	anbi2d 718	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
157	156	imbi1d 324	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
158		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
159	158	anbi2d 718	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
160	159	imbi1d 324	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
161		oveq12 6317	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f ` z ) = 0 /\ ( g ` z ) = 0 ) -> ( ( f ` z ) + ( g ` z ) ) = ( 0 + 0 ) )
162		00id 9826	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 0 + 0 ) = 0
163	161, 162	syl6eq 2521	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f ` z ) = 0 /\ ( g ` z ) = 0 ) -> ( ( f ` z ) + ( g ` z ) ) = 0 )
164	163	iftrued 3880	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( f ` z ) = 0 /\ ( g ` z ) = 0 ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) = 0 )
165	164	adantll 728	. . . . . . . . . . . . . . . . . . . . . . . . 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 )
166		simpll 768	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> ph )
167	15	simplbi 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( F ` z ) e. ( 0 [,) +oo ) -> ( F ` z ) e. RR )
168	14, 167	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ z e. RR ) -> ( F ` z ) e. RR )
169	77	simplbi 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( G ` z ) e. ( 0 [,) +oo ) -> ( G ` z ) e. RR )
170	76, 169	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ z e. RR ) -> ( G ` z ) e. RR )
171	168, 170, 17, 79	addge0d 10210	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ z e. RR ) -> 0 <_ ( ( F ` z ) + ( G ` z ) ) )
172	166, 171	sylan 479	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
173	172	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
174	165, 173	eqbrtrd 4416	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
175	174	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 ) ) ) )
176	172	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
177		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( f ` z ) = 0 -> ( ( f ` z ) + ( g ` z ) ) = ( 0 + ( g ` z ) ) )
178		simplrr 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> g e. dom S.1 )
179		i1ff 22713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( g e. dom S.1 -> g : RR --> RR )
180	179	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( g e. dom S.1 /\ z e. RR ) -> ( g ` z ) e. RR )
181	178, 180	sylan 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
182	181	recnd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
183	182	addid2d 9852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
184	177, 183	sylan9eqr 2527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
185	184	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
186	185	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
187	147	rpred 11364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( c e. RR+ /\ d e. RR+ ) -> if ( c <_ d , c , d ) e. RR )
188	187	ad2antlr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
189	181, 188	readdcld 9688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
190	189	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
191	166, 170	sylan 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
192	191	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
193	166, 168	sylan 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
194	193, 191	readdcld 9688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
195	194	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
196		simplrr 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> d e. RR+ )
197	196	rpred 11364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> d e. RR )
198		rpre 11331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( c e. RR+ -> c e. RR )
199		rpre 11331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( d e. RR+ -> d e. RR )
200		min2 11507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( c e. RR /\ d e. RR ) -> if ( c <_ d , c , d ) <_ d )
201	198, 199, 200	syl2an 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( c e. RR+ /\ d e. RR+ ) -> if ( c <_ d , c , d ) <_ d )
202	201	ad2antlr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
203	188, 197, 181, 202	leadd2dd 10249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
204	181, 197	readdcld 9688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
205		letr 9745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
206	189, 204, 191, 205	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
207	203, 206	mpand 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
208	207	imp 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
209	170, 168	addge02d 10223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ z e. RR ) -> ( 0 <_ ( F ` z ) <-> ( G ` z ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
210	17, 209	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ z e. RR ) -> ( G ` z ) <_ ( ( F ` z ) + ( G ` z ) ) )
211	166, 210	sylan 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
212	211	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
213	190, 192, 195, 208, 212	letrd 9809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
214	213	adantlr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
215	186, 214	eqbrtrd 4416	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
216		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
217		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
218	216, 217	ifboth 3908	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
219	176, 215, 218	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
220	219	ex 441	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
221	220	adantld 474	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
222	221	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
223	157, 160, 175, 222	ifbothda 3907	. . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
224	155	anbi2d 718	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
225	224	imbi1d 324	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( ( ( ( ( f ` z ) + c ) <_ ( 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 ) ) ) <-> ( ( ( ( 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 ) ) ) ) )
226	158	anbi2d 718	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( g ` z ) + d ) = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( ( ( ( f ` z ) + c ) <_ ( F ` z ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) <-> ( ( ( f ` z ) + c ) <_ ( F ` z ) /\ if ( (