Theorem itg2addnc

Description: Alternate proof of itg2add 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 , 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 , and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017) (Revised by Brendan Leahy, 13-Mar-2018)

	Ref	Expression
Hypotheses	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	itg2addnc	|- ( ph -> ( S.2 ` ( F oF + G ) ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )

Proof

Step	Hyp	Ref	Expression
1		itg2addnc.f1	|- ( ph -> F e. MblFn )
2		itg2addnc.f2	|- ( ph -> F : RR --> ( 0 [,) +oo ) )
3		itg2addnc.f3	|- ( ph -> ( S.2 ` F ) e. RR )
4		itg2addnc.g2	|- ( ph -> G : RR --> ( 0 [,) +oo ) )
5		itg2addnc.g3	|- ( ph -> ( S.2 ` G ) e. RR )
6		simprr	|- ( ( 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 ) )
7		itg1cl	|- ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
8	7	adantr	|- ( ( 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 )
9	6 8	eqeltrd	|- ( ( 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 )
10	9	rexlimiva	|- ( 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 )
11	10	abssi	|- { 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
12	11	a1i	|- ( 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 )
13		i1f0	|- ( RR X. { 0 } ) e. dom S.1
14		3nn	|- 3 e. NN
15		nnrp	|- ( 3 e. NN -> 3 e. RR+ )
16		ne0i	|- ( 3 e. RR+ -> RR+ =/= (/) )
17	14 15 16	mp2b	|- RR+ =/= (/)
18	2	ffvelrnda	|- ( ( ph /\ z e. RR ) -> ( F ` z ) e. ( 0 [,) +oo ) )
19		elrege0	|- ( ( F ` z ) e. ( 0 [,) +oo ) <-> ( ( F ` z ) e. RR /\ 0 <_ ( F ` z ) ) )
20	18 19	sylib	|- ( ( ph /\ z e. RR ) -> ( ( F ` z ) e. RR /\ 0 <_ ( F ` z ) ) )
21	20	simprd	|- ( ( ph /\ z e. RR ) -> 0 <_ ( F ` z ) )
22	21	ralrimiva	|- ( ph -> A. z e. RR 0 <_ ( F ` z ) )
23		reex	|- RR e. _V
24	23	a1i	|- ( ph -> RR e. _V )
25		c0ex	|- 0 e. _V
26	25	a1i	|- ( ( ph /\ z e. RR ) -> 0 e. _V )
27		eqidd	|- ( ph -> ( z e. RR |-> 0 ) = ( z e. RR |-> 0 ) )
28	2	feqmptd	|- ( ph -> F = ( z e. RR |-> ( F ` z ) ) )
29	24 26 18 27 28	ofrfval2	|- ( ph -> ( ( z e. RR |-> 0 ) oR <_ F <-> A. z e. RR 0 <_ ( F ` z ) ) )
30	22 29	mpbird	|- ( ph -> ( z e. RR |-> 0 ) oR <_ F )
31	30	ralrimivw	|- ( ph -> A. c e. RR+ ( z e. RR |-> 0 ) oR <_ F )
32		r19.2z	|- ( ( RR+ =/= (/) /\ A. c e. RR+ ( z e. RR |-> 0 ) oR <_ F ) -> E. c e. RR+ ( z e. RR |-> 0 ) oR <_ F )
33	17 31 32	sylancr	|- ( ph -> E. c e. RR+ ( z e. RR |-> 0 ) oR <_ F )
34		fveq2	|- ( f = ( RR X. { 0 } ) -> ( S.1 ` f ) = ( S.1 ` ( RR X. { 0 } ) ) )
35		itg10	|- ( S.1 ` ( RR X. { 0 } ) ) = 0
36	34 35	eqtr2di	|- ( f = ( RR X. { 0 } ) -> 0 = ( S.1 ` f ) )
37	36	biantrud	|- ( 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 ) ) ) )
38		fveq1	|- ( f = ( RR X. { 0 } ) -> ( f ` z ) = ( ( RR X. { 0 } ) ` z ) )
39	25	fvconst2	|- ( z e. RR -> ( ( RR X. { 0 } ) ` z ) = 0 )
40	38 39	sylan9eq	|- ( ( f = ( RR X. { 0 } ) /\ z e. RR ) -> ( f ` z ) = 0 )
41	40	iftrued	|- ( ( f = ( RR X. { 0 } ) /\ z e. RR ) -> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) = 0 )
42	41	mpteq2dva	|- ( f = ( RR X. { 0 } ) -> ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) = ( z e. RR |-> 0 ) )
43	42	breq1d	|- ( f = ( RR X. { 0 } ) -> ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F <-> ( z e. RR |-> 0 ) oR <_ F ) )
44	43	rexbidv	|- ( 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 ) )
45	37 44	bitr3d	|- ( 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 ) )
46	45	rspcev	|- ( ( ( 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 ) ) )
47	13 33 46	sylancr	|- ( 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 ) ) )
48		eqeq1	|- ( x = 0 -> ( x = ( S.1 ` f ) <-> 0 = ( S.1 ` f ) ) )
49	48	anbi2d	|- ( 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 ) ) ) )
50	49	rexbidv	|- ( 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 ) ) ) )
51	25 50	elab	|- ( 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 ) ) )
52	47 51	sylibr	|- ( 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 ) ) } )
53	52	ne0d	|- ( 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 ) ) } =/= (/) )
54		icossicc	|- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
55		fss	|- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : RR --> ( 0 [,] +oo ) )
56	54 55	mpan2	|- ( F : RR --> ( 0 [,) +oo ) -> F : RR --> ( 0 [,] +oo ) )
57		eqid	|- { 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 ) ) }
58	57	itg2addnclem	|- ( 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* , < ) )
59	2 56 58	3syl	|- ( 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* , < ) )
60	59 3	eqeltrrd	|- ( 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 )
61		ressxr	|- RR C_ RR*
62	11 61	sstri	|- { 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*
63		supxrub	|- ( ( { 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* , < ) )
64	62 63	mpan	|- ( 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* , < ) )
65	64	rgen	|- 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		brralrspcev	|- ( ( 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	60 65 66	sylancl	|- ( 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	|- ( ( 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	|- ( g e. dom S.1 -> ( S.1 ` g ) e. RR )
70	69	adantr	|- ( ( 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	|- ( ( 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	|- ( 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	|- { 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	|- ( 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	4	ffvelrnda	|- ( ( ph /\ z e. RR ) -> ( G ` z ) e. ( 0 [,) +oo ) )
76		elrege0	|- ( ( G ` z ) e. ( 0 [,) +oo ) <-> ( ( G ` z ) e. RR /\ 0 <_ ( G ` z ) ) )
77	75 76	sylib	|- ( ( ph /\ z e. RR ) -> ( ( G ` z ) e. RR /\ 0 <_ ( G ` z ) ) )
78	77	simprd	|- ( ( ph /\ z e. RR ) -> 0 <_ ( G ` z ) )
79	78	ralrimiva	|- ( ph -> A. z e. RR 0 <_ ( G ` z ) )
80	4	feqmptd	|- ( ph -> G = ( z e. RR |-> ( G ` z ) ) )
81	24 26 75 27 80	ofrfval2	|- ( ph -> ( ( z e. RR |-> 0 ) oR <_ G <-> A. z e. RR 0 <_ ( G ` z ) ) )
82	79 81	mpbird	|- ( ph -> ( z e. RR |-> 0 ) oR <_ G )
83	82	ralrimivw	|- ( ph -> A. d e. RR+ ( z e. RR |-> 0 ) oR <_ G )
84		r19.2z	|- ( ( RR+ =/= (/) /\ A. d e. RR+ ( z e. RR |-> 0 ) oR <_ G ) -> E. d e. RR+ ( z e. RR |-> 0 ) oR <_ G )
85	17 83 84	sylancr	|- ( ph -> E. d e. RR+ ( z e. RR |-> 0 ) oR <_ G )
86		fveq2	|- ( g = ( RR X. { 0 } ) -> ( S.1 ` g ) = ( S.1 ` ( RR X. { 0 } ) ) )
87	86 35	eqtr2di	|- ( g = ( RR X. { 0 } ) -> 0 = ( S.1 ` g ) )
88	87	biantrud	|- ( 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 ) ) ) )
89		fveq1	|- ( g = ( RR X. { 0 } ) -> ( g ` z ) = ( ( RR X. { 0 } ) ` z ) )
90	89 39	sylan9eq	|- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> ( g ` z ) = 0 )
91	90	iftrued	|- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) = 0 )
92	91	mpteq2dva	|- ( g = ( RR X. { 0 } ) -> ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) = ( z e. RR |-> 0 ) )
93	92	breq1d	|- ( g = ( RR X. { 0 } ) -> ( ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G <-> ( z e. RR |-> 0 ) oR <_ G ) )
94	93	rexbidv	|- ( 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 ) )
95	88 94	bitr3d	|- ( 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 ) )
96	95	rspcev	|- ( ( ( 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 ) ) )
97	13 85 96	sylancr	|- ( 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 ) ) )
98		eqeq1	|- ( x = 0 -> ( x = ( S.1 ` g ) <-> 0 = ( S.1 ` g ) ) )
99	98	anbi2d	|- ( 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 ) ) ) )
100	99	rexbidv	|- ( 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 ) ) ) )
101	25 100	elab	|- ( 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 ) ) )
102	97 101	sylibr	|- ( 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 ) ) } )
103	102	ne0d	|- ( 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 ) ) } =/= (/) )
104		fss	|- ( ( G : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> G : RR --> ( 0 [,] +oo ) )
105	54 104	mpan2	|- ( G : RR --> ( 0 [,) +oo ) -> G : RR --> ( 0 [,] +oo ) )
106		eqid	|- { 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 ) ) }
107	106	itg2addnclem	|- ( 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* , < ) )
108	4 105 107	3syl	|- ( 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* , < ) )
109	108 5	eqeltrrd	|- ( 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 )
110	73 61	sstri	|- { 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*
111		supxrub	|- ( ( { 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* , < ) )
112	110 111	mpan	|- ( 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* , < ) )
113	112	rgen	|- 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* , < )
114		brralrspcev	|- ( ( 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 )
115	109 113 114	sylancl	|- ( 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 )
116		eqid	|- { 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 ) }
117	12 53 67 74 103 115 116	supadd	|- ( 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 , < ) )
118		supxrre	|- ( ( { 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 , < ) )
119	12 53 67 118	syl3anc	|- ( 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 , < ) )
120	59 119	eqtrd	|- ( 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 , < ) )
121		supxrre	|- ( ( { 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 , < ) )
122	74 103 115 121	syl3anc	|- ( 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 , < ) )
123	108 122	eqtrd	|- ( 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 , < ) )
124	120 123	oveq12d	|- ( 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 , < ) ) )
125		ge0addcl	|- ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
126	54 125	sseldi	|- ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,] +oo ) )
127	126	adantl	|- ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) e. ( 0 [,] +oo ) )
128		inidm	|- ( RR i^i RR ) = RR
129	127 2 4 24 24 128	off	|- ( ph -> ( F oF + G ) : RR --> ( 0 [,] +oo ) )
130		eqid	|- { 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 ) ) }
131	130	itg2addnclem	|- ( ( 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* , < ) )
132	129 131	syl	|- ( 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* , < ) )
133	1 2 3 4 5	itg2addnclem3	|- ( 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 ) ) ) )
134		simpl	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> f e. dom S.1 )
135		simpr	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> g e. dom S.1 )
136	134 135	i1fadd	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( f oF + g ) e. dom S.1 )
137	136	ad3antlr	|- ( ( ( ( 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 )
138		reeanv	|- ( 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 ) )
139	138	biimpri	|- ( ( 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 ) )
140	139	ad2ant2r	|- ( ( ( 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 ) )
141		ifcl	|- ( ( c e. RR+ /\ d e. RR+ ) -> if ( c <_ d , c , d ) e. RR+ )
142	141	ad2antlr	|- ( ( ( ( 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+ )
143		breq1	|- ( 0 = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) -> ( 0 <_ ( F ` z ) <-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) ) )
144	143	anbi1d	|- ( 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 ) ) ) )
145	144	imbi1d	|- ( 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 ) ) ) ) )
146		breq1	|- ( ( ( 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 ) ) )
147	146	anbi1d	|- ( ( ( 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 ) ) ) )
148	147	imbi1d	|- ( ( ( 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 ) ) ) ) )
149		breq1	|- ( 0 = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( 0 <_ ( G ` z ) <-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) )
150	149	anbi2d	|- ( 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 ) ) ) )
151	150	imbi1d	|- ( 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 ) ) ) ) )
152		breq1	|- ( ( ( 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 ) ) )
153	152	anbi2d	|- ( ( ( 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 ) ) ) )
154	153	imbi1d	|- ( ( ( 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 ) ) ) ) )
155		oveq12	|- ( ( ( f ` z ) = 0 /\ ( g ` z ) = 0 ) -> ( ( f ` z ) + ( g ` z ) ) = ( 0 + 0 ) )
156		00id	|- ( 0 + 0 ) = 0
157	155 156	eqtrdi	|- ( ( ( f ` z ) = 0 /\ ( g ` z ) = 0 ) -> ( ( f ` z ) + ( g ` z ) ) = 0 )
158	157	iftrued	|- ( ( ( f ` z ) = 0 /\ ( g ` z ) = 0 ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) = 0 )
159	158	adantll	|- ( ( ( ( ( ( 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 )
160		simpll	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> ph )
161	19	simplbi	|- ( ( F ` z ) e. ( 0 [,) +oo ) -> ( F ` z ) e. RR )
162	18 161	syl	|- ( ( ph /\ z e. RR ) -> ( F ` z ) e. RR )
163	76	simplbi	|- ( ( G ` z ) e. ( 0 [,) +oo ) -> ( G ` z ) e. RR )
164	75 163	syl	|- ( ( ph /\ z e. RR ) -> ( G ` z ) e. RR )
165	162 164 21 78	addge0d	|- ( ( ph /\ z e. RR ) -> 0 <_ ( ( F ` z ) + ( G ` z ) ) )
166	160 165	sylan	|- ( ( ( ( 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 ) ) )
167	166	ad2antrr	|- ( ( ( ( ( ( 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 ) ) )
168	159 167	eqbrtrd	|- ( ( ( ( ( ( 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 ) ) )
169	168	a1d	|- ( ( ( ( ( ( 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 ) ) ) )
170	166	ad2antrr	|- ( ( ( ( ( ( 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 ) ) )
171		oveq1	|- ( ( f ` z ) = 0 -> ( ( f ` z ) + ( g ` z ) ) = ( 0 + ( g ` z ) ) )
172		simplrr	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> g e. dom S.1 )
173		i1ff	|- ( g e. dom S.1 -> g : RR --> RR )
174	173	ffvelrnda	|- ( ( g e. dom S.1 /\ z e. RR ) -> ( g ` z ) e. RR )
175	172 174	sylan	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( g ` z ) e. RR )
176	175	recnd	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( g ` z ) e. CC )
177	176	addid2d	|- ( ( ( ( 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 ) )
178	171 177	sylan9eqr	|- ( ( ( ( ( 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 ) )
179	178	oveq1d	|- ( ( ( ( ( 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 ) ) )
180	179	adantr	|- ( ( ( ( ( ( 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 ) ) )
181	141	rpred	|- ( ( c e. RR+ /\ d e. RR+ ) -> if ( c <_ d , c , d ) e. RR )
182	181	ad2antlr	|- ( ( ( ( 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 )
183	175 182	readdcld	|- ( ( ( ( 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 )
184	183	adantr	|- ( ( ( ( ( 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 )
185	160 164	sylan	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( G ` z ) e. RR )
186	185	adantr	|- ( ( ( ( ( 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 )
187	160 162	sylan	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( F ` z ) e. RR )
188	187 185	readdcld	|- ( ( ( ( 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 )
189	188	adantr	|- ( ( ( ( ( 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 )
190		simplrr	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> d e. RR+ )
191	190	rpred	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> d e. RR )
192		rpre	|- ( c e. RR+ -> c e. RR )
193		rpre	|- ( d e. RR+ -> d e. RR )
194		min2	|- ( ( c e. RR /\ d e. RR ) -> if ( c <_ d , c , d ) <_ d )
195	192 193 194	syl2an	|- ( ( c e. RR+ /\ d e. RR+ ) -> if ( c <_ d , c , d ) <_ d )
196	195	ad2antlr	|- ( ( ( ( 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 )
197	182 191 175 196	leadd2dd	|- ( ( ( ( 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 ) )
198	175 191	readdcld	|- ( ( ( ( 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 )
199		letr	|- ( ( ( ( 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 ) ) )
200	183 198 185 199	syl3anc	|- ( ( ( ( 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 ) ) )
201	197 200	mpand	|- ( ( ( ( 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 ) ) )
202	201	imp	|- ( ( ( ( ( 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 ) )
203	164 162	addge02d	|- ( ( ph /\ z e. RR ) -> ( 0 <_ ( F ` z ) <-> ( G ` z ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
204	21 203	mpbid	|- ( ( ph /\ z e. RR ) -> ( G ` z ) <_ ( ( F ` z ) + ( G ` z ) ) )
205	160 204	sylan	|- ( ( ( ( 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 ) ) )
206	205	adantr	|- ( ( ( ( ( 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 ) ) )
207	184 186 189 202 206	letrd	|- ( ( ( ( ( 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 ) ) )
208	207	adantlr	|- ( ( ( ( ( ( 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 ) ) )
209	180 208	eqbrtrd	|- ( ( ( ( ( ( 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 ) ) )
210		breq1	|- ( 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 ) ) ) )
211		breq1	|- ( ( ( ( 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 ) ) ) )
212	210 211	ifboth	|- ( ( 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 ) ) )
213	170 209 212	syl2anc	|- ( ( ( ( ( ( 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 ) ) )
214	213	ex	|- ( ( ( ( ( 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 ) ) ) )
215	214	adantld	|- ( ( ( ( ( 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 ) ) ) )
216	215	adantr	|- ( ( ( ( ( ( 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 ) ) ) )
217	151 154 169 216	ifbothda	|- ( ( ( ( ( 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 ) ) ) )
218	149	anbi2d	|- ( 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 ) ) ) )
219	218	imbi1d	|- ( 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 ) ) ) ) )
220	152	anbi2d	|- ( ( ( 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 ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) ) )
221	220	imbi1d	|- ( ( ( g ` z ) + d ) = if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) -> ( ( ( ( ( f ` z ) + c ) <_ ( 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 ) ) ) <-> ( ( ( ( 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 ) ) ) ) )
222	166	ad2antrr	|- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( g ` z ) = 0 ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> 0 <_ ( ( F ` z ) + ( G ` z ) ) )
223		oveq2	|- ( ( g ` z ) = 0 -> ( ( f ` z ) + ( g ` z ) ) = ( ( f ` z ) + 0 ) )
224		simplrl	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> f e. dom S.1 )
225		i1ff	|- ( f e. dom S.1 -> f : RR --> RR )
226	225	ffvelrnda	|- ( ( f e. dom S.1 /\ z e. RR ) -> ( f ` z ) e. RR )
227	224 226	sylan	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( f ` z ) e. RR )
228	227	recnd	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( f ` z ) e. CC )
229	228	addid1d	|- ( ( ( ( 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 ) )
230	223 229	sylan9eqr	|- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( g ` z ) = 0 ) -> ( ( f ` z ) + ( g ` z ) ) = ( f ` z ) )
231	230	oveq1d	|- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( g ` z ) = 0 ) -> ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) = ( ( f ` z ) + if ( c <_ d , c , d ) ) )
232	231	adantr	|- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( g ` z ) = 0 ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) = ( ( f ` z ) + if ( c <_ d , c , d ) ) )
233	227 182	readdcld	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( f ` z ) + if ( c <_ d , c , d ) ) e. RR )
234	233	adantr	|- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> ( ( f ` z ) + if ( c <_ d , c , d ) ) e. RR )
235	187	adantr	|- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> ( F ` z ) e. RR )
236	188	adantr	|- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> ( ( F ` z ) + ( G ` z ) ) e. RR )
237		simplrl	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> c e. RR+ )
238	237	rpred	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> c e. RR )
239		min1	|- ( ( c e. RR /\ d e. RR ) -> if ( c <_ d , c , d ) <_ c )
240	192 193 239	syl2an	|- ( ( c e. RR+ /\ d e. RR+ ) -> if ( c <_ d , c , d ) <_ c )
241	240	ad2antlr	|- ( ( ( ( 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 ) <_ c )
242	182 238 227 241	leadd2dd	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( f ` z ) + if ( c <_ d , c , d ) ) <_ ( ( f ` z ) + c ) )
243	227 238	readdcld	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( f ` z ) + c ) e. RR )
244		letr	|- ( ( ( ( f ` z ) + if ( c <_ d , c , d ) ) e. RR /\ ( ( f ` z ) + c ) e. RR /\ ( F ` z ) e. RR ) -> ( ( ( ( f ` z ) + if ( c <_ d , c , d ) ) <_ ( ( f ` z ) + c ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> ( ( f ` z ) + if ( c <_ d , c , d ) ) <_ ( F ` z ) ) )
245	233 243 187 244	syl3anc	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( ( ( f ` z ) + if ( c <_ d , c , d ) ) <_ ( ( f ` z ) + c ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> ( ( f ` z ) + if ( c <_ d , c , d ) ) <_ ( F ` z ) ) )
246	242 245	mpand	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( ( f ` z ) + c ) <_ ( F ` z ) -> ( ( f ` z ) + if ( c <_ d , c , d ) ) <_ ( F ` z ) ) )
247	246	imp	|- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> ( ( f ` z ) + if ( c <_ d , c , d ) ) <_ ( F ` z ) )
248	162 164	addge01d	|- ( ( ph /\ z e. RR ) -> ( 0 <_ ( G ` z ) <-> ( F ` z ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
249	78 248	mpbid	|- ( ( ph /\ z e. RR ) -> ( F ` z ) <_ ( ( F ` z ) + ( G ` z ) ) )
250	160 249	sylan	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( F ` z ) <_ ( ( F ` z ) + ( G ` z ) ) )
251	250	adantr	|- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> ( F ` z ) <_ ( ( F ` z ) + ( G ` z ) ) )
252	234 235 236 247 251	letrd	|- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> ( ( f ` z ) + if ( c <_ d , c , d ) ) <_ ( ( F ` z ) + ( G ` z ) ) )
253	252	adantlr	|- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( g ` z ) = 0 ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> ( ( f ` z ) + if ( c <_ d , c , d ) ) <_ ( ( F ` z ) + ( G ` z ) ) )
254	232 253	eqbrtrd	|- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( g ` z ) = 0 ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) <_ ( ( F ` z ) + ( G ` z ) ) )
255	222 254 212	syl2anc	|- ( ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( g ` z ) = 0 ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) )
256	255	ex	|- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( g ` z ) = 0 ) -> ( ( ( f ` z ) + c ) <_ ( F ` z ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
257	256	adantlr	|- ( ( ( ( ( ( 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 ) -> ( ( ( f ` z ) + c ) <_ ( F ` z ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
258	257	adantrd	|- ( ( ( ( ( ( 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 ) -> ( ( ( ( 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 ) ) ) )
259	166	adantr	|- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( ( f ` z ) + c ) <_ ( F ` z ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) ) -> 0 <_ ( ( F ` z ) + ( G ` z ) ) )
260	182	recnd	|- ( ( ( ( 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. CC )
261	228 176 260	addassd	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) = ( ( f ` z ) + ( ( g ` z ) + if ( c <_ d , c , d ) ) ) )
262	261	adantr	|- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( ( f ` z ) + c ) <_ ( F ` z ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) ) -> ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) = ( ( f ` z ) + ( ( g ` z ) + if ( c <_ d , c , d ) ) ) )
263	227 237	ltaddrpd	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( f ` z ) < ( ( f ` z ) + c ) )
264	227 243 263	ltled	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( f ` z ) <_ ( ( f ` z ) + c ) )
265		letr	|- ( ( ( f ` z ) e. RR /\ ( ( f ` z ) + c ) e. RR /\ ( F ` z ) e. RR ) -> ( ( ( f ` z ) <_ ( ( f ` z ) + c ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> ( f ` z ) <_ ( F ` z ) ) )
266	227 243 187 265	syl3anc	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( ( f ` z ) <_ ( ( f ` z ) + c ) /\ ( ( f ` z ) + c ) <_ ( F ` z ) ) -> ( f ` z ) <_ ( F ` z ) ) )
267	264 266	mpand	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( ( f ` z ) + c ) <_ ( F ` z ) -> ( f ` z ) <_ ( F ` z ) ) )
268		le2add	|- ( ( ( ( f ` z ) e. RR /\ ( ( g ` z ) + if ( c <_ d , c , d ) ) e. RR ) /\ ( ( F ` z ) e. RR /\ ( G ` z ) e. RR ) ) -> ( ( ( f ` z ) <_ ( F ` z ) /\ ( ( g ` z ) + if ( c <_ d , c , d ) ) <_ ( G ` z ) ) -> ( ( f ` z ) + ( ( g ` z ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
269	227 183 187 185 268	syl22anc	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( ( f ` z ) <_ ( F ` z ) /\ ( ( g ` z ) + if ( c <_ d , c , d ) ) <_ ( G ` z ) ) -> ( ( f ` z ) + ( ( g ` z ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
270	267 201 269	syl2and	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( ( ( f ` z ) + c ) <_ ( F ` z ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) -> ( ( f ` z ) + ( ( g ` z ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
271	270	imp	|- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( ( f ` z ) + c ) <_ ( F ` z ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) ) -> ( ( f ` z ) + ( ( g ` z ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) )
272	262 271	eqbrtrd	|- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( ( f ` z ) + c ) <_ ( F ` z ) /\ ( ( g ` z ) + d ) <_ ( G ` z ) ) ) -> ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) <_ ( ( F ` z ) + ( G ` z ) ) )
273	259 272 212	syl2anc	|- ( ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) /\ ( ( ( f ` z ) + c ) <_ ( 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 ) ) )
274	273	ex	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( ( ( f ` z ) + c ) <_ ( 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 ) ) ) )
275	274	ad2antrr	|- ( ( ( ( ( ( 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 ) -> ( ( ( ( f ` z ) + c ) <_ ( 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 ) ) ) )
276	219 221 258 275	ifbothda	|- ( ( ( ( ( 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 ) + 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 ) ) ) )
277	145 148 217 276	ifbothda	|- ( ( ( ( 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 ) ) <_ ( 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 ) ) ) )
278	277	ralimdva	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> ( A. z e. RR ( if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) -> A. z e. RR if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
279		ovex	|- ( ( f ` z ) + c ) e. _V
280	25 279	ifex	|- if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) e. _V
281	280	a1i	|- ( ( ph /\ z e. RR ) -> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) e. _V )
282		eqidd	|- ( ph -> ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) = ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) )
283	24 281 18 282 28	ofrfval2	|- ( ph -> ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F <-> A. z e. RR if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) ) )
284		ovex	|- ( ( g ` z ) + d ) e. _V
285	25 284	ifex	|- if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) e. _V
286	285	a1i	|- ( ( ph /\ z e. RR ) -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) e. _V )
287		eqidd	|- ( ph -> ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) = ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) )
288	24 286 75 287 80	ofrfval2	|- ( ph -> ( ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G <-> A. z e. RR if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) )
289	283 288	anbi12d	|- ( ph -> ( ( ( 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 ) <-> ( A. z e. RR if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) /\ A. z e. RR if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) ) )
290		r19.26	|- ( A. z e. RR ( if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) <-> ( A. z e. RR if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) /\ A. z e. RR if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) )
291	289 290	bitr4di	|- ( ph -> ( ( ( 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 ) <-> A. z e. RR ( if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) ) )
292	291	ad2antrr	|- ( ( ( 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 ) <-> A. z e. RR ( if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) <_ ( F ` z ) /\ if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) <_ ( G ` z ) ) ) )
293	23	a1i	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> RR e. _V )
294		ovex	|- ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) e. _V
295	25 294	ifex	|- if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) e. _V
296	295	a1i	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) e. _V )
297		ovexd	|- ( ( ( ( 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. _V )
298	225	ffnd	|- ( f e. dom S.1 -> f Fn RR )
299	298	adantr	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> f Fn RR )
300	299	ad2antlr	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> f Fn RR )
301	173	ffnd	|- ( g e. dom S.1 -> g Fn RR )
302	301	adantl	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> g Fn RR )
303	302	ad2antlr	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> g Fn RR )
304		eqidd	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( f ` z ) = ( f ` z ) )
305		eqidd	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( g ` z ) = ( g ` z ) )
306	300 303 293 293 128 304 305	ofval	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( f oF + g ) ` z ) = ( ( f ` z ) + ( g ` z ) ) )
307	306	eqeq1d	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( ( f oF + g ) ` z ) = 0 <-> ( ( f ` z ) + ( g ` z ) ) = 0 ) )
308	306	oveq1d	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> ( ( ( f oF + g ) ` z ) + if ( c <_ d , c , d ) ) = ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) )
309	307 308	ifbieq2d	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ z e. RR ) -> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + if ( c <_ d , c , d ) ) ) = if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) )
310	309	mpteq2dva	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + if ( c <_ d , c , d ) ) ) ) = ( z e. RR |-> if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) ) )
311	2	ffnd	|- ( ph -> F Fn RR )
312	4	ffnd	|- ( ph -> G Fn RR )
313		eqidd	|- ( ( ph /\ z e. RR ) -> ( F ` z ) = ( F ` z ) )
314		eqidd	|- ( ( ph /\ z e. RR ) -> ( G ` z ) = ( G ` z ) )
315	311 312 24 24 128 313 314	offval	|- ( ph -> ( F oF + G ) = ( z e. RR |-> ( ( F ` z ) + ( G ` z ) ) ) )
316	315	ad2antrr	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> ( F oF + G ) = ( z e. RR |-> ( ( F ` z ) + ( G ` z ) ) ) )
317	293 296 297 310 316	ofrfval2	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> ( ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + if ( c <_ d , c , d ) ) ) ) oR <_ ( F oF + G ) <-> A. z e. RR if ( ( ( f ` z ) + ( g ` z ) ) = 0 , 0 , ( ( ( f ` z ) + ( g ` z ) ) + if ( c <_ d , c , d ) ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
318	278 292 317	3imtr4d	|- ( ( ( 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 ) -> ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + if ( c <_ d , c , d ) ) ) ) oR <_ ( F oF + G ) ) )
319	318	imp	|- ( ( ( ( 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 ) ) -> ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + if ( c <_ d , c , d ) ) ) ) oR <_ ( F oF + G ) )
320		oveq2	|- ( y = if ( c <_ d , c , d ) -> ( ( ( f oF + g ) ` z ) + y ) = ( ( ( f oF + g ) ` z ) + if ( c <_ d , c , d ) ) )
321	320	ifeq2d	|- ( y = if ( c <_ d , c , d ) -> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) = if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + if ( c <_ d , c , d ) ) ) )
322	321	mpteq2dv	|- ( y = if ( c <_ d , c , d ) -> ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) ) = ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + if ( c <_ d , c , d ) ) ) ) )
323	322	breq1d	|- ( y = if ( c <_ d , c , d ) -> ( ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) ) oR <_ ( F oF + G ) <-> ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + if ( c <_ d , c , d ) ) ) ) oR <_ ( F oF + G ) ) )
324	323	rspcev	|- ( ( if ( c <_ d , c , d ) e. RR+ /\ ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + if ( c <_ d , c , d ) ) ) ) oR <_ ( F oF + G ) ) -> E. y e. RR+ ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) ) oR <_ ( F oF + G ) )
325	142 319 324	syl2anc	|- ( ( ( ( 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 ) ) -> E. y e. RR+ ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) ) oR <_ ( F oF + G ) )
326	325	ex	|- ( ( ( 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 ) -> E. y e. RR+ ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) ) oR <_ ( F oF + G ) ) )
327	326	rexlimdvva	|- ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( 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. y e. RR+ ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) ) oR <_ ( F oF + G ) ) )
328	140 327	syl5	|- ( ( 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 ) ) ) -> E. y e. RR+ ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) ) oR <_ ( F oF + G ) ) )
329	328	a1dd	|- ( ( 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 ) -> E. y e. RR+ ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) ) oR <_ ( F oF + G ) ) ) )
330	329	imp31	|- ( ( ( ( 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 ) ) -> E. y e. RR+ ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) ) oR <_ ( F oF + G ) )
331		oveq12	|- ( ( t = ( S.1 ` f ) /\ u = ( S.1 ` g ) ) -> ( t + u ) = ( ( S.1 ` f ) + ( S.1 ` g ) ) )
332	331	ad2ant2l	|- ( ( ( 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 ) ) ) -> ( t + u ) = ( ( S.1 ` f ) + ( S.1 ` g ) ) )
333	134 135	itg1add	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( S.1 ` ( f oF + g ) ) = ( ( S.1 ` f ) + ( S.1 ` g ) ) )
334	333	eqcomd	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( ( S.1 ` f ) + ( S.1 ` g ) ) = ( S.1 ` ( f oF + g ) ) )
335	334	adantl	|- ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( S.1 ` f ) + ( S.1 ` g ) ) = ( S.1 ` ( f oF + g ) ) )
336	332 335	sylan9eqr	|- ( ( ( 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 ) ) ) ) -> ( t + u ) = ( S.1 ` ( f oF + g ) ) )
337		eqtr	|- ( ( s = ( t + u ) /\ ( t + u ) = ( S.1 ` ( f oF + g ) ) ) -> s = ( S.1 ` ( f oF + g ) ) )
338	337	ancoms	|- ( ( ( t + u ) = ( S.1 ` ( f oF + g ) ) /\ s = ( t + u ) ) -> s = ( S.1 ` ( f oF + g ) ) )
339	336 338	sylan	|- ( ( ( ( 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 ) ) -> s = ( S.1 ` ( f oF + g ) ) )
340		fveq1	|- ( h = ( f oF + g ) -> ( h ` z ) = ( ( f oF + g ) ` z ) )
341	340	eqeq1d	|- ( h = ( f oF + g ) -> ( ( h ` z ) = 0 <-> ( ( f oF + g ) ` z ) = 0 ) )
342	340	oveq1d	|- ( h = ( f oF + g ) -> ( ( h ` z ) + y ) = ( ( ( f oF + g ) ` z ) + y ) )
343	341 342	ifbieq2d	|- ( h = ( f oF + g ) -> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) = if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) )
344	343	mpteq2dv	|- ( h = ( f oF + g ) -> ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) = ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) ) )
345	344	breq1d	|- ( h = ( f oF + g ) -> ( ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) <-> ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) ) oR <_ ( F oF + G ) ) )
346	345	rexbidv	|- ( h = ( f oF + g ) -> ( E. y e. RR+ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) <-> E. y e. RR+ ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) ) oR <_ ( F oF + G ) ) )
347		fveq2	|- ( h = ( f oF + g ) -> ( S.1 ` h ) = ( S.1 ` ( f oF + g ) ) )
348	347	eqeq2d	|- ( h = ( f oF + g ) -> ( s = ( S.1 ` h ) <-> s = ( S.1 ` ( f oF + g ) ) ) )
349	346 348	anbi12d	|- ( h = ( f oF + g ) -> ( ( E. y e. RR+ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) /\ s = ( S.1 ` h ) ) <-> ( E. y e. RR+ ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) ) oR <_ ( F oF + G ) /\ s = ( S.1 ` ( f oF + g ) ) ) ) )
350	349	rspcev	|- ( ( ( f oF + g ) e. dom S.1 /\ ( E. y e. RR+ ( z e. RR |-> if ( ( ( f oF + g ) ` z ) = 0 , 0 , ( ( ( f oF + g ) ` z ) + y ) ) ) oR <_ ( F oF + G ) /\ s = ( S.1 ` ( f oF + g ) ) ) ) -> 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 ) ) )
351	137 330 339 350	syl12anc	|- ( ( ( ( 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 ) ) -> 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 ) ) )
352	351	exp31	|- ( ( 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 ) -> 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 ) ) ) ) )
353	352	rexlimdvva	|- ( ph -> ( 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 ) -> 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 ) ) ) ) )
354	353	impd	|- ( ph -> ( ( 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 ) ) -> 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 ) ) ) )
355	354	exlimdvv	|- ( ph -> ( 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 ) ) -> 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 ) ) ) )
356	133 355	impbid	|- ( 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 ) ) ) )
357		eqeq1	|- ( x = t -> ( x = ( S.1 ` f ) <-> t = ( S.1 ` f ) ) )
358	357	anbi2d	|- ( x = t -> ( ( 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 /\ t = ( S.1 ` f ) ) ) )
359	358	rexbidv	|- ( x = t -> ( 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 /\ t = ( S.1 ` f ) ) ) )
360	359	rexab	|- ( 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 ) <-> E. t ( E. f 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. 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 ) ) )
361		eqeq1	|- ( x = u -> ( x = ( S.1 ` g ) <-> u = ( S.1 ` g ) ) )
362	361	anbi2d	|- ( x = u -> ( ( 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 /\ u = ( S.1 ` g ) ) ) )
363	362	rexbidv	|- ( x = u -> ( 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 /\ u = ( S.1 ` g ) ) ) )
364	363	rexab	|- ( 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 ) <-> E. u ( E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) /\ s = ( t + u ) ) )
365	364	anbi2i	|- ( ( E. f 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. 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 ) ) <-> ( E. f 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. u ( E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) /\ s = ( t + u ) ) ) )
366		19.42v	|- ( E. u ( E. f 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. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) /\ s = ( t + u ) ) ) <-> ( E. f 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. u ( E. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) /\ s = ( t + u ) ) ) )
367		reeanv	|- ( 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 ) ) ) <-> ( E. f 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. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) )
368	367	anbi1i	|- ( ( 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 ) ) <-> ( ( E. f 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. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) )
369		anass	|- ( ( ( E. f 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. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> ( E. f 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. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) /\ s = ( t + u ) ) ) )
370	368 369	bitr2i	|- ( ( E. f 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. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) /\ s = ( t + 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 ) ) )
371	370	exbii	|- ( E. u ( E. f 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. g e. dom S.1 ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) /\ s = ( t + u ) ) ) <-> 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 ) ) )
372	365 366 371	3bitr2i	|- ( ( E. f 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. 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 ) ) <-> 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 ) ) )
373	372	exbii	|- ( E. t ( E. f 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. 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 ) ) <-> 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 ) ) )
374	360 373	bitri	|- ( 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 ) <-> 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 ) ) )
375	356 374	bitr4di	|- ( 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. { 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 ) ) )
376	375	abbidv	|- ( ph -> { 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. 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 ) } )
377	376	supeq1d	|- ( ph -> 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* , < ) = 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* , < ) )
378		simpr	|- ( ( ( 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 ) ) } /\ 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 = ( t + u ) )
379	11	sseli	|- ( 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 ) ) } -> t e. RR )
380	379	ad2antrr	|- ( ( ( 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 ) ) } /\ 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 ) ) -> t e. RR )
381	73	sseli	|- ( 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 ) ) } -> u e. RR )
382	381	ad2antlr	|- ( ( ( 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 ) ) } /\ 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 ) ) -> u e. RR )
383	380 382	readdcld	|- ( ( ( 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 ) ) } /\ 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 ) ) -> ( t + u ) e. RR )
384	378 383	eqeltrd	|- ( ( ( 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 ) ) } /\ 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. RR )
385	384	ex	|- ( ( 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 ) ) } /\ 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. RR ) )
386	385	rexlimivv	|- ( 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. RR )
387	386	abssi	|- { 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 ) } C_ RR
388	387	a1i	|- ( ph -> { 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 ) } C_ RR )
389	156	eqcomi	|- 0 = ( 0 + 0 )
390		rspceov	|- ( ( 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 ) ) } /\ 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 ) ) } /\ 0 = ( 0 + 0 ) ) -> 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 ) ) } 0 = ( t + u ) )
391	389 390	mp3an3	|- ( ( 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 ) ) } /\ 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. 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 ) ) } 0 = ( t + u ) )
392	52 102 391	syl2anc	|- ( ph -> 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 ) ) } 0 = ( t + u ) )
393		eqeq1	|- ( s = 0 -> ( s = ( t + u ) <-> 0 = ( t + u ) ) )
394	393	2rexbidv	|- ( s = 0 -> ( 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 ) <-> 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 ) ) } 0 = ( t + u ) ) )
395	25 394	spcev	|- ( 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 ) ) } 0 = ( t + u ) -> E. 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 ) )
396	392 395	syl	|- ( ph -> E. 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 ) )
397		abn0	|- ( { 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 ) } =/= (/) <-> E. 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 ) )
398	396 397	sylibr	|- ( ph -> { 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 ) } =/= (/) )
399	60 109	readdcld	|- ( 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* , < ) ) e. RR )
400		simpr	|- ( ( ( ph /\ ( 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 ) ) } /\ 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 ) ) } ) ) /\ b = ( t + u ) ) -> b = ( t + u ) )
401	379	ad2antrl	|- ( ( ph /\ ( 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 ) ) } /\ 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 ) ) } ) ) -> t e. RR )
402	381	ad2antll	|- ( ( ph /\ ( 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 ) ) } /\ 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 ) ) } ) ) -> u e. RR )
403	60	adantr	|- ( ( ph /\ ( 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 ) ) } /\ 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 ) ) } ) ) -> 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 )
404	109	adantr	|- ( ( ph /\ ( 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 ) ) } /\ 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 ) ) } ) ) -> 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 )
405		supxrub	|- ( ( { 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* /\ 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 ) ) } ) -> t <_ 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* , < ) )
406	62 405	mpan	|- ( 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 ) ) } -> t <_ 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* , < ) )
407	406	ad2antrl	|- ( ( ph /\ ( 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 ) ) } /\ 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 ) ) } ) ) -> t <_ 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* , < ) )
408		supxrub	|- ( ( { 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* /\ 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 ) ) } ) -> u <_ 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* , < ) )
409	110 408	mpan	|- ( 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 ) ) } -> u <_ 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* , < ) )
410	409	ad2antll	|- ( ( ph /\ ( 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 ) ) } /\ 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 ) ) } ) ) -> u <_ 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* , < ) )
411	401 402 403 404 407 410	le2addd	|- ( ( ph /\ ( 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 ) ) } /\ 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 ) ) } ) ) -> ( t + u ) <_ ( 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* , < ) ) )
412	411	adantr	|- ( ( ( ph /\ ( 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 ) ) } /\ 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 ) ) } ) ) /\ b = ( t + u ) ) -> ( t + u ) <_ ( 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* , < ) ) )
413	400 412	eqbrtrd	|- ( ( ( ph /\ ( 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 ) ) } /\ 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 ) ) } ) ) /\ b = ( t + u ) ) -> 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* , < ) + 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* , < ) ) )
414	413	ex	|- ( ( ph /\ ( 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 ) ) } /\ 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 ) ) } ) ) -> ( b = ( t + u ) -> 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* , < ) + 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* , < ) ) ) )
415	414	rexlimdvva	|- ( ph -> ( 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 ) ) } b = ( t + u ) -> 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* , < ) + 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* , < ) ) ) )
416	415	alrimiv	|- ( ph -> A. b ( 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 ) ) } b = ( t + u ) -> 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* , < ) + 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* , < ) ) ) )
417		breq2	|- ( 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. 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. 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* , < ) ) ) )
418	417	ralbidv	|- ( 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. 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. { 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 ) } b <_ a <-> A. b e. { 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 ) } 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* , < ) + 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* , < ) ) ) )
419		eqeq1	|- ( s = b -> ( s = ( t + u ) <-> b = ( t + u ) ) )
420	419	2rexbidv	|- ( s = b -> ( 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 ) <-> 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 ) ) } b = ( t + u ) ) )
421	420	ralab	|- ( A. b e. { 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 ) } 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* , < ) + 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. 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 ) ) } b = ( t + u ) -> 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* , < ) + 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* , < ) ) ) )
422	418 421	bitrdi	|- ( 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. 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. { 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 ) } b <_ a <-> A. b ( 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 ) ) } b = ( t + u ) -> 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* , < ) + 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* , < ) ) ) ) )
423	422	rspcev	|- ( ( ( 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* , < ) ) e. RR /\ A. b ( 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 ) ) } b = ( t + u ) -> 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* , < ) + 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. { 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 ) } b <_ a )
424	399 416 423	syl2anc	|- ( ph -> E. a e. RR A. b e. { 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 ) } b <_ a )
425		supxrre	|- ( ( { 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 ) } C_ RR /\ { 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 ) } =/= (/) /\ E. a e. RR A. b e. { 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 ) } b <_ a ) -> 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* , < ) = 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 , < ) )
426	388 398 424 425	syl3anc	|- ( ph -> 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* , < ) = 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 , < ) )
427	132 377 426	3eqtrd	|- ( ph -> ( S.2 ` ( F oF + G ) ) = 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 , < ) )
428	117 124 427	3eqtr4rd	|- ( ph -> ( S.2 ` ( F oF + G ) ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )