Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itg2addnc Structured version   Unicode version

Theorem itg2addnc 30037
Description: Alternate proof of itg2add 22032 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 21981, 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 8813, and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017.) (Revised by Brendan Leahy, 13-Mar-2018.)
Hypotheses
Ref Expression
itg2addnc.f1  |-  ( ph  ->  F  e. MblFn )
itg2addnc.f2  |-  ( ph  ->  F : RR --> ( 0 [,) +oo ) )
itg2addnc.f3  |-  ( ph  ->  ( S.2 `  F
)  e.  RR )
itg2addnc.g2  |-  ( ph  ->  G : RR --> ( 0 [,) +oo ) )
itg2addnc.g3  |-  ( ph  ->  ( S.2 `  G
)  e.  RR )
Assertion
Ref Expression
itg2addnc  |-  ( ph  ->  ( S.2 `  ( F  oF  +  G
) )  =  ( ( S.2 `  F
)  +  ( S.2 `  G ) ) )

Proof of Theorem itg2addnc
Dummy variables  t 
s  u  x  y  z  f  g  h  a  b  c  d are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprr 756 . . . . . . 7  |-  ( ( f  e.  dom  S.1  /\  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  =  ( S.1 `  f ) )
2 itg1cl 21958 . . . . . . . 8  |-  ( f  e.  dom  S.1  ->  ( S.1 `  f )  e.  RR )
32adantr 465 . . . . . . 7  |-  ( ( f  e.  dom  S.1  /\  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  -> 
( S.1 `  f )  e.  RR )
41, 3eqeltrd 2529 . . . . . 6  |-  ( ( f  e.  dom  S.1  /\  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  e.  RR )
54rexlimiva 2929 . . . . 5  |-  ( E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) )  ->  x  e.  RR )
65abssi 3557 . . . 4  |-  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  C_  RR
76a1i 11 . . 3  |-  ( ph  ->  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  C_  RR )
8 i1f0 21960 . . . . . 6  |-  ( RR 
X.  { 0 } )  e.  dom  S.1
9 3nn 10695 . . . . . . . 8  |-  3  e.  NN
10 nnrp 11233 . . . . . . . 8  |-  ( 3  e.  NN  ->  3  e.  RR+ )
11 ne0i 3773 . . . . . . . 8  |-  ( 3  e.  RR+  ->  RR+  =/=  (/) )
129, 10, 11mp2b 10 . . . . . . 7  |-  RR+  =/=  (/)
13 itg2addnc.f2 . . . . . . . . . . . . 13  |-  ( ph  ->  F : RR --> ( 0 [,) +oo ) )
1413ffvelrnda 6012 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  RR )  ->  ( F `
 z )  e.  ( 0 [,) +oo ) )
15 elrege0 11631 . . . . . . . . . . . 12  |-  ( ( F `  z )  e.  ( 0 [,) +oo )  <->  ( ( F `
 z )  e.  RR  /\  0  <_ 
( F `  z
) ) )
1614, 15sylib 196 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  RR )  ->  ( ( F `  z )  e.  RR  /\  0  <_  ( F `  z
) ) )
1716simprd 463 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  RR )  ->  0  <_ 
( F `  z
) )
1817ralrimiva 2855 . . . . . . . . 9  |-  ( ph  ->  A. z  e.  RR  0  <_  ( F `  z ) )
19 reex 9581 . . . . . . . . . . 11  |-  RR  e.  _V
2019a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  e.  _V )
21 c0ex 9588 . . . . . . . . . . 11  |-  0  e.  _V
2221a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  RR )  ->  0  e. 
_V )
23 eqidd 2442 . . . . . . . . . 10  |-  ( ph  ->  ( z  e.  RR  |->  0 )  =  ( z  e.  RR  |->  0 ) )
2413feqmptd 5907 . . . . . . . . . 10  |-  ( ph  ->  F  =  ( z  e.  RR  |->  ( F `
 z ) ) )
2520, 22, 14, 23, 24ofrfval2 6538 . . . . . . . . 9  |-  ( ph  ->  ( ( z  e.  RR  |->  0 )  oR  <_  F  <->  A. z  e.  RR  0  <_  ( F `  z )
) )
2618, 25mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( z  e.  RR  |->  0 )  oR  <_  F )
2726ralrimivw 2856 . . . . . . 7  |-  ( ph  ->  A. c  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  F )
28 r19.2z 3900 . . . . . . 7  |-  ( (
RR+  =/=  (/)  /\  A. c  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  F
)  ->  E. c  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  F )
2912, 27, 28sylancr 663 . . . . . 6  |-  ( ph  ->  E. c  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  F )
30 fveq2 5852 . . . . . . . . . 10  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( S.1 `  f
)  =  ( S.1 `  ( RR  X.  {
0 } ) ) )
31 itg10 21961 . . . . . . . . . 10  |-  ( S.1 `  ( RR  X.  {
0 } ) )  =  0
3230, 31syl6req 2499 . . . . . . . . 9  |-  ( f  =  ( RR  X.  { 0 } )  ->  0  =  ( S.1 `  f ) )
3332biantrud 507 . . . . . . . 8  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  <->  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  0  =  ( S.1 `  f
) ) ) )
34 fveq1 5851 . . . . . . . . . . . . 13  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( f `  z )  =  ( ( RR  X.  {
0 } ) `  z ) )
3521fvconst2 6107 . . . . . . . . . . . . 13  |-  ( z  e.  RR  ->  (
( RR  X.  {
0 } ) `  z )  =  0 )
3634, 35sylan9eq 2502 . . . . . . . . . . . 12  |-  ( ( f  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  (
f `  z )  =  0 )
3736iftrued 3930 . . . . . . . . . . 11  |-  ( ( f  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) )  =  0 )
3837mpteq2dva 4519 . . . . . . . . . 10  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  =  ( z  e.  RR  |->  0 ) )
3938breq1d 4443 . . . . . . . . 9  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( ( z  e.  RR  |->  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  c ) ) )  oR  <_  F 
<->  ( z  e.  RR  |->  0 )  oR  <_  F ) )
4039rexbidv 2952 . . . . . . . 8  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  <->  E. c  e.  RR+  (
z  e.  RR  |->  0 )  oR  <_  F ) )
4133, 40bitr3d 255 . . . . . . 7  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  0  =  ( S.1 `  f
) )  <->  E. c  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  F )
)
4241rspcev 3194 . . . . . 6  |-  ( ( ( RR  X.  {
0 } )  e. 
dom  S.1  /\  E. c  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  F )  ->  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  0  =  ( S.1 `  f
) ) )
438, 29, 42sylancr 663 . . . . 5  |-  ( ph  ->  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  0  =  ( S.1 `  f
) ) )
44 eqeq1 2445 . . . . . . . 8  |-  ( x  =  0  ->  (
x  =  ( S.1 `  f )  <->  0  =  ( S.1 `  f ) ) )
4544anbi2d 703 . . . . . . 7  |-  ( x  =  0  ->  (
( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) )  <->  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  c ) ) )  oR  <_  F  /\  0  =  ( S.1 `  f ) ) ) )
4645rexbidv 2952 . . . . . 6  |-  ( x  =  0  ->  ( E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) )  <->  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  0  =  ( S.1 `  f ) ) ) )
4721, 46elab 3230 . . . . 5  |-  ( 0  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  <->  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  0  =  ( S.1 `  f ) ) )
4843, 47sylibr 212 . . . 4  |-  ( ph  ->  0  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } )
49 ne0i 3773 . . . 4  |-  ( 0  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  ->  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f ) ) }  =/=  (/) )
5048, 49syl 16 . . 3  |-  ( ph  ->  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  =/=  (/) )
51 icossicc 11615 . . . . . . 7  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
52 fss 5725 . . . . . . 7  |-  ( ( F : RR --> ( 0 [,) +oo )  /\  ( 0 [,) +oo )  C_  ( 0 [,] +oo ) )  ->  F : RR --> ( 0 [,] +oo ) )
5351, 52mpan2 671 . . . . . 6  |-  ( F : RR --> ( 0 [,) +oo )  ->  F : RR --> ( 0 [,] +oo ) )
54 eqid 2441 . . . . . . 7  |-  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  =  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }
5554itg2addnclem 30034 . . . . . 6  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( S.2 `  F )  =  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR* ,  <  ) )
5613, 53, 553syl 20 . . . . 5  |-  ( ph  ->  ( S.2 `  F
)  =  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  ) )
57 itg2addnc.f3 . . . . 5  |-  ( ph  ->  ( S.2 `  F
)  e.  RR )
5856, 57eqeltrrd 2530 . . . 4  |-  ( ph  ->  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  )  e.  RR )
59 ressxr 9635 . . . . . . 7  |-  RR  C_  RR*
606, 59sstri 3495 . . . . . 6  |-  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  C_  RR*
61 supxrub 11520 . . . . . 6  |-  ( ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  C_  RR* 
/\  b  e.  {
x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } )  ->  b  <_  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  ) )
6260, 61mpan 670 . . . . 5  |-  ( b  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  ->  b  <_  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  ) )
6362rgen 2801 . . . 4  |-  A. b  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } b  <_  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  )
64 breq2 4437 . . . . . 6  |-  ( a  =  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR* ,  <  )  ->  ( b  <_ 
a  <->  b  <_  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  ) ) )
6564ralbidv 2880 . . . . 5  |-  ( a  =  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR* ,  <  )  ->  ( A. b  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } b  <_  a  <->  A. b  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } b  <_  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  ) ) )
6665rspcev 3194 . . . 4  |-  ( ( sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  )  e.  RR  /\  A. b  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } b  <_  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  ) )  ->  E. a  e.  RR  A. b  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } b  <_  a )
6758, 63, 66sylancl 662 . . 3  |-  ( ph  ->  E. a  e.  RR  A. b  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } b  <_  a )
68 simprr 756 . . . . . . 7  |-  ( ( g  e.  dom  S.1  /\  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) )  ->  x  =  ( S.1 `  g ) )
69 itg1cl 21958 . . . . . . . 8  |-  ( g  e.  dom  S.1  ->  ( S.1 `  g )  e.  RR )
7069adantr 465 . . . . . . 7  |-  ( ( g  e.  dom  S.1  /\  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) )  -> 
( S.1 `  g )  e.  RR )
7168, 70eqeltrd 2529 . . . . . 6  |-  ( ( g  e.  dom  S.1  /\  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) )  ->  x  e.  RR )
7271rexlimiva 2929 . . . . 5  |-  ( E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) )  ->  x  e.  RR )
7372abssi 3557 . . . 4  |-  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }  C_  RR
7473a1i 11 . . 3  |-  ( ph  ->  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }  C_  RR )
75 itg2addnc.g2 . . . . . . . . . . . . 13  |-  ( ph  ->  G : RR --> ( 0 [,) +oo ) )
7675ffvelrnda 6012 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  RR )  ->  ( G `
 z )  e.  ( 0 [,) +oo ) )
77 elrege0 11631 . . . . . . . . . . . 12  |-  ( ( G `  z )  e.  ( 0 [,) +oo )  <->  ( ( G `
 z )  e.  RR  /\  0  <_ 
( G `  z
) ) )
7876, 77sylib 196 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  RR )  ->  ( ( G `  z )  e.  RR  /\  0  <_  ( G `  z
) ) )
7978simprd 463 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  RR )  ->  0  <_ 
( G `  z
) )
8079ralrimiva 2855 . . . . . . . . 9  |-  ( ph  ->  A. z  e.  RR  0  <_  ( G `  z ) )
8175feqmptd 5907 . . . . . . . . . 10  |-  ( ph  ->  G  =  ( z  e.  RR  |->  ( G `
 z ) ) )
8220, 22, 76, 23, 81ofrfval2 6538 . . . . . . . . 9  |-  ( ph  ->  ( ( z  e.  RR  |->  0 )  oR  <_  G  <->  A. z  e.  RR  0  <_  ( G `  z )
) )
8380, 82mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( z  e.  RR  |->  0 )  oR  <_  G )
8483ralrimivw 2856 . . . . . . 7  |-  ( ph  ->  A. d  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  G )
85 r19.2z 3900 . . . . . . 7  |-  ( (
RR+  =/=  (/)  /\  A. d  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  G
)  ->  E. d  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  G )
8612, 84, 85sylancr 663 . . . . . 6  |-  ( ph  ->  E. d  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  G )
87 fveq2 5852 . . . . . . . . . 10  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( S.1 `  g
)  =  ( S.1 `  ( RR  X.  {
0 } ) ) )
8887, 31syl6req 2499 . . . . . . . . 9  |-  ( g  =  ( RR  X.  { 0 } )  ->  0  =  ( S.1 `  g ) )
8988biantrud 507 . . . . . . . 8  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  oR  <_  G  <->  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  0  =  ( S.1 `  g
) ) ) )
90 fveq1 5851 . . . . . . . . . . . . 13  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( g `  z )  =  ( ( RR  X.  {
0 } ) `  z ) )
9190, 35sylan9eq 2502 . . . . . . . . . . . 12  |-  ( ( g  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  (
g `  z )  =  0 )
9291iftrued 3930 . . . . . . . . . . 11  |-  ( ( g  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  =  0 )
9392mpteq2dva 4519 . . . . . . . . . 10  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  =  ( z  e.  RR  |->  0 ) )
9493breq1d 4443 . . . . . . . . 9  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( ( z  e.  RR  |->  if ( ( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  d ) ) )  oR  <_  G 
<->  ( z  e.  RR  |->  0 )  oR  <_  G ) )
9594rexbidv 2952 . . . . . . . 8  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  oR  <_  G  <->  E. d  e.  RR+  (
z  e.  RR  |->  0 )  oR  <_  G ) )
9689, 95bitr3d 255 . . . . . . 7  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  0  =  ( S.1 `  g
) )  <->  E. d  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  G )
)
9796rspcev 3194 . . . . . 6  |-  ( ( ( RR  X.  {
0 } )  e. 
dom  S.1  /\  E. d  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  G )  ->  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  0  =  ( S.1 `  g
) ) )
988, 86, 97sylancr 663 . . . . 5  |-  ( ph  ->  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  0  =  ( S.1 `  g
) ) )
99 eqeq1 2445 . . . . . . . 8  |-  ( x  =  0  ->  (
x  =  ( S.1 `  g )  <->  0  =  ( S.1 `  g ) ) )
10099anbi2d 703 . . . . . . 7  |-  ( x  =  0  ->  (
( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) )  <->  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  d ) ) )  oR  <_  G  /\  0  =  ( S.1 `  g ) ) ) )
101100rexbidv 2952 . . . . . 6  |-  ( x  =  0  ->  ( E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) )  <->  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  oR  <_  G  /\  0  =  ( S.1 `  g ) ) ) )
10221, 101elab 3230 . . . . 5  |-  ( 0  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }  <->  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  oR  <_  G  /\  0  =  ( S.1 `  g ) ) )
10398, 102sylibr 212 . . . 4  |-  ( ph  ->  0  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } )
104 ne0i 3773 . . . 4  |-  ( 0  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }  ->  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g ) ) }  =/=  (/) )
105103, 104syl 16 . . 3  |-  ( ph  ->  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }  =/=  (/) )
106 fss 5725 . . . . . . 7  |-  ( ( G : RR --> ( 0 [,) +oo )  /\  ( 0 [,) +oo )  C_  ( 0 [,] +oo ) )  ->  G : RR --> ( 0 [,] +oo ) )
10751, 106mpan2 671 . . . . . 6  |-  ( G : RR --> ( 0 [,) +oo )  ->  G : RR --> ( 0 [,] +oo ) )
108 eqid 2441 . . . . . . 7  |-  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }  =  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }
109108itg2addnclem 30034 . . . . . 6  |-  ( G : RR --> ( 0 [,] +oo )  -> 
( S.2 `  G )  =  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g ) ) } ,  RR* ,  <  ) )
11075, 107, 1093syl 20 . . . . 5  |-  ( ph  ->  ( S.2 `  G
)  =  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  ) )
111 itg2addnc.g3 . . . . 5  |-  ( ph  ->  ( S.2 `  G
)  e.  RR )
112110, 111eqeltrrd 2530 . . . 4  |-  ( ph  ->  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  )  e.  RR )
11373, 59sstri 3495 . . . . . 6  |-  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }  C_  RR*
114 supxrub 11520 . . . . . 6  |-  ( ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }  C_  RR* 
/\  b  e.  {
x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g ) ) } )  ->  b  <_  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  ) )
115113, 114mpan 670 . . . . 5  |-  ( b  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }  ->  b  <_  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  ) )
116115rgen 2801 . . . 4  |-  A. b  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } b  <_  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  )
117 breq2 4437 . . . . . 6  |-  ( a  =  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g ) ) } ,  RR* ,  <  )  ->  ( b  <_ 
a  <->  b  <_  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  ) ) )
118117ralbidv 2880 . . . . 5  |-  ( a  =  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g ) ) } ,  RR* ,  <  )  ->  ( A. b  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } b  <_  a  <->  A. b  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } b  <_  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  ) ) )
119118rspcev 3194 . . . 4  |-  ( ( sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  )  e.  RR  /\  A. b  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } b  <_  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  ) )  ->  E. a  e.  RR  A. b  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } b  <_  a )
120112, 116, 119sylancl 662 . . 3  |-  ( ph  ->  E. a  e.  RR  A. b  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } b  <_  a )
121 eqid 2441 . . 3  |-  { s  |  E. t  e. 
{ x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } E. u  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } s  =  ( t  +  u ) }  =  { s  |  E. t  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } E. u  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } s  =  ( t  +  u ) }
1227, 50, 67, 74, 105, 120, 121supadd 30010 . 2  |-  ( ph  ->  ( sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR ,  <  )  +  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR ,  <  ) )  =  sup ( { s  |  E. t  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } E. u  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } s  =  ( t  +  u ) } ,  RR ,  <  ) )
123 supxrre 11523 . . . . 5  |-  ( ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  C_  RR  /\  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  =/=  (/) 
/\  E. a  e.  RR  A. b  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } b  <_  a )  ->  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  )  =  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR ,  <  ) )
1247, 50, 67, 123syl3anc 1227 . . . 4  |-  ( ph  ->  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  )  =  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR ,  <  ) )
12556, 124eqtrd 2482 . . 3  |-  ( ph  ->  ( S.2 `  F
)  =  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR ,  <  ) )
126 supxrre 11523 . . . . 5  |-  ( ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }  C_  RR  /\  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }  =/=  (/) 
/\  E. a  e.  RR  A. b  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } b  <_  a )  ->  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  )  =  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR ,  <  ) )
12774, 105, 120, 126syl3anc 1227 . . . 4  |-  ( ph  ->  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  )  =  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR ,  <  ) )
128110, 127eqtrd 2482 . . 3  |-  ( ph  ->  ( S.2 `  G
)  =  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR ,  <  ) )
129125, 128oveq12d 6295 . 2  |-  ( ph  ->  ( ( S.2 `  F
)  +  ( S.2 `  G ) )  =  ( sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR ,  <  )  +  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR ,  <  ) ) )
130 ge0addcl 11636 . . . . . . 7  |-  ( ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  +  y )  e.  ( 0 [,) +oo )
)
13151, 130sseldi 3484 . . . . . 6  |-  ( ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  +  y )  e.  ( 0 [,] +oo )
)
132131adantl 466 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo )
) )  ->  (
x  +  y )  e.  ( 0 [,] +oo ) )
133 inidm 3689 . . . . 5  |-  ( RR 
i^i  RR )  =  RR
134132, 13, 75, 20, 20, 133off 6535 . . . 4  |-  ( ph  ->  ( F  oF  +  G ) : RR --> ( 0 [,] +oo ) )
135 eqid 2441 . . . . 5  |-  { s  |  E. h  e. 
dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `
 z )  +  y ) ) )  oR  <_  ( F  oF  +  G
)  /\  s  =  ( S.1 `  h ) ) }  =  {
s  |  E. h  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `
 z )  +  y ) ) )  oR  <_  ( F  oF  +  G
)  /\  s  =  ( S.1 `  h ) ) }
136135itg2addnclem 30034 . . . 4  |-  ( ( F  oF  +  G ) : RR --> ( 0 [,] +oo )  ->  ( S.2 `  ( F  oF  +  G
) )  =  sup ( { s  |  E. h  e.  dom  S.1 ( E. y  e.  RR+  (
z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `  z
)  +  y ) ) )  oR  <_  ( F  oF  +  G )  /\  s  =  ( S.1 `  h ) ) } ,  RR* ,  <  ) )
137134, 136syl 16 . . 3  |-  ( ph  ->  ( S.2 `  ( F  oF  +  G
) )  =  sup ( { s  |  E. h  e.  dom  S.1 ( E. y  e.  RR+  (
z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `  z
)  +  y ) ) )  oR  <_  ( F  oF  +  G )  /\  s  =  ( S.1 `  h ) ) } ,  RR* ,  <  ) )
138 itg2addnc.f1 . . . . . . . 8  |-  ( ph  ->  F  e. MblFn )
139138, 13, 57, 75, 111itg2addnclem3 30036 . . . . . . 7  |-  ( ph  ->  ( E. h  e. 
dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `
 z )  +  y ) ) )  oR  <_  ( F  oF  +  G
)  /\  s  =  ( S.1 `  h ) )  ->  E. t E. u ( E. f  e.  dom  S.1 E. g  e. 
dom  S.1 ( ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  t  =  ( S.1 `  f
) )  /\  ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  u  =  ( S.1 `  g
) ) )  /\  s  =  ( t  +  u ) ) ) )
140 simpl 457 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  f  e.  dom  S.1 )
141 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  g  e.  dom  S.1 )
142140, 141i1fadd 21968 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( f  oF  +  g )  e.  dom  S.1 )
143142ad3antlr 730 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  t  =  ( S.1 `  f
) )  /\  ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  u  =  ( S.1 `  g
) ) ) )  /\  s  =  ( t  +  u ) )  ->  ( f  oF  +  g
)  e.  dom  S.1 )
144 reeanv 3009 . . . . . . . . . . . . . . . . 17  |-  ( E. c  e.  RR+  E. d  e.  RR+  ( ( z  e.  RR  |->  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  c ) ) )  oR  <_  F  /\  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  oR  <_  G
)  <->  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G ) )
145144biimpri 206 . . . . . . . . . . . . . . . 16  |-  ( ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  d ) ) )  oR  <_  G )  ->  E. c  e.  RR+  E. d  e.  RR+  ( ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G ) )
146145ad2ant2r 746 . . . . . . . . . . . . . . 15  |-  ( ( ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  t  =  ( S.1 `  f
) )  /\  ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  u  =  ( S.1 `  g
) ) )  ->  E. c  e.  RR+  E. d  e.  RR+  ( ( z  e.  RR  |->  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  c ) ) )  oR  <_  F  /\  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  oR  <_  G
) )
147 ifcl 3964 . . . . . . . . . . . . . . . . . . 19  |-  ( ( c  e.  RR+  /\  d  e.  RR+ )  ->  if ( c  <_  d ,  c ,  d )  e.  RR+ )
148147ad2antlr 726 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  ( ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G ) )  ->  if ( c  <_  d ,  c ,  d )  e.  RR+ )
149 breq1 4436 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0  =  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) )  -> 
( 0  <_  ( F `  z )  <->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) )  <_  ( F `  z ) ) )
150149anbi1d 704 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  =  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) )  -> 
( ( 0  <_ 
( F `  z
)  /\  if (
( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  d ) )  <_  ( G `  z ) )  <->  ( if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) )  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) ) ) )
151150imbi1d 317 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  =  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) )  -> 
( ( ( 0  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )  <->  ( ( if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) )  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) ) )
152 breq1 4436 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( f `  z
)  +  c )  =  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) )  -> 
( ( ( f `
 z )  +  c )  <_  ( F `  z )  <->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) )  <_  ( F `  z ) ) )
153152anbi1d 704 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( f `  z
)  +  c )  =  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) )  -> 
( ( ( ( f `  z )  +  c )  <_ 
( F `  z
)  /\  if (
( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  d ) )  <_  ( G `  z ) )  <->  ( if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) )  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) ) ) )
154153imbi1d 317 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( f `  z
)  +  c )  =  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) )  -> 
( ( ( ( ( f `  z
)  +  c )  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )  <->  ( ( if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) )  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) ) )
155 breq1 4436 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( 0  <_  ( G `  z )  <->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) ) )
156155anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( ( 0  <_ 
( F `  z
)  /\  0  <_  ( G `  z ) )  <->  ( 0  <_ 
( F `  z
)  /\  if (
( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  d ) )  <_  ( G `  z ) ) ) )
157156imbi1d 317 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( ( ( 0  <_  ( F `  z )  /\  0  <_  ( G `  z
) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )  <->  ( ( 0  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) ) )
158 breq1 4436 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( g `  z
)  +  d )  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( ( ( g `
 z )  +  d )  <_  ( G `  z )  <->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) ) )
159158anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( g `  z
)  +  d )  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( ( 0  <_ 
( F `  z
)  /\  ( (
g `  z )  +  d )  <_ 
( G `  z
) )  <->  ( 0  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) ) ) )
160159imbi1d 317 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( g `  z
)  +  d )  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( ( ( 0  <_  ( F `  z )  /\  (
( g `  z
)  +  d )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )  <->  ( ( 0  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) ) )
161 oveq12 6286 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( f `  z
)  =  0  /\  ( g `  z
)  =  0 )  ->  ( ( f `
 z )  +  ( g `  z
) )  =  ( 0  +  0 ) )
162 00id 9753 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0  +  0 )  =  0
163161, 162syl6eq 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f `  z
)  =  0  /\  ( g `  z
)  =  0 )  ->  ( ( f `
 z )  +  ( g `  z
) )  =  0 )
164163iftrued 3930 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( f `  z
)  =  0  /\  ( g `  z
)  =  0 )  ->  if ( ( ( f `  z
)  +  ( g `
 z ) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_ 
d ,  c ,  d ) ) )  =  0 )
165164adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( c  e.  RR+  /\  d  e.  RR+ )
)  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  /\  ( g `  z
)  =  0 )  ->  if ( ( ( f `  z
)  +  ( g `
 z ) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_ 
d ,  c ,  d ) ) )  =  0 )
166 simpll 753 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  ->  ph )
16715simplbi 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F `  z )  e.  ( 0 [,) +oo )  ->  ( F `
 z )  e.  RR )
16814, 167syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR )  ->  ( F `
 z )  e.  RR )
16977simplbi 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( G `  z )  e.  ( 0 [,) +oo )  ->  ( G `
 z )  e.  RR )
17076, 169syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR )  ->  ( G `
 z )  e.  RR )
171168, 170, 17, 79addge0d 10129 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  z  e.  RR )  ->  0  <_ 
( ( F `  z )  +  ( G `  z ) ) )
172166, 171sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  0  <_  ( ( F `  z )  +  ( G `  z ) ) )
173172ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( c  e.  RR+  /\  d  e.  RR+ )
)  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  /\  ( g `  z
)  =  0 )  ->  0  <_  (
( F `  z
)  +  ( G `
 z ) ) )
174165, 173eqbrtrd 4453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( c  e.  RR+  /\  d  e.  RR+ )
)  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  /\  ( g `  z
)  =  0 )  ->  if ( ( ( f `  z
)  +  ( g `
 z ) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_ 
d ,  c ,  d ) ) )  <_  ( ( F `
 z )  +  ( G `  z
) ) )
175174a1d 25 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( c  e.  RR+  /\  d  e.  RR+ )
)  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  /\  ( g `  z
)  =  0 )  ->  ( ( 0  <_  ( F `  z )  /\  0  <_  ( G `  z
) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) )
176172ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( c  e.  RR+  /\  d  e.  RR+ )
)  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  /\  ( ( g `  z )  +  d )  <_  ( G `  z ) )  -> 
0  <_  ( ( F `  z )  +  ( G `  z ) ) )
177 oveq1 6284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( f `  z )  =  0  ->  (
( f `  z
)  +  ( g `
 z ) )  =  ( 0  +  ( g `  z
) ) )
178 simplrr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  -> 
g  e.  dom  S.1 )
179 i1ff 21949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
180179ffvelrnda 6012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( g  e.  dom  S.1  /\  z  e.  RR )  ->  ( g `  z )  e.  RR )
181178, 180sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  ( g `  z
)  e.  RR )
182181recnd 9620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  ( g `  z
)  e.  CC )
183182addid2d 9779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  ( 0  +  ( g `  z ) )  =  ( g `
 z ) )
184177, 183sylan9eqr 2504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  /\  ( f `  z
)  =  0 )  ->  ( ( f `
 z )  +  ( g `  z
) )  =  ( g `  z ) )
185184oveq1d 6292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  /\  ( f `  z
)  =  0 )  ->  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_ 
d ,  c ,  d ) )  =  ( ( g `  z )  +  if ( c  <_  d ,  c ,  d ) ) )
186185adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( c  e.  RR+  /\  d  e.  RR+ )
)  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  /\  ( ( g `  z )  +  d )  <_  ( G `  z ) )  -> 
( ( ( f `
 z )  +  ( g `  z
) )  +  if ( c  <_  d ,  c ,  d ) )  =  ( ( g `  z
)  +  if ( c  <_  d , 
c ,  d ) ) )
187147rpred 11260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( c  e.  RR+  /\  d  e.  RR+ )  ->  if ( c  <_  d ,  c ,  d )  e.  RR )
188187ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  if ( c  <_ 
d ,  c ,  d )  e.  RR )
189181, 188readdcld 9621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  ( ( g `  z )  +  if ( c  <_  d ,  c ,  d ) )  e.  RR )
190189adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  /\  ( ( g `  z )  +  d )  <_  ( G `  z ) )  -> 
( ( g `  z )  +  if ( c  <_  d ,  c ,  d ) )  e.  RR )
191166, 170sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  ( G `  z
)  e.  RR )
192191adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  /\  ( ( g `  z )  +  d )  <_  ( G `  z ) )  -> 
( G `  z
)  e.  RR )
193166, 168sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  ( F `  z
)  e.  RR )
194193, 191readdcld 9621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  ( ( F `  z )  +  ( G `  z ) )  e.  RR )
195194adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  /\  ( ( g `  z )  +  d )  <_  ( G `  z ) )  -> 
( ( F `  z )  +  ( G `  z ) )  e.  RR )
196 simplrr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  d  e.  RR+ )
197196rpred 11260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  d  e.  RR )
198 rpre 11230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  e.  RR+  ->  c  e.  RR )
199 rpre 11230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( d  e.  RR+  ->  d  e.  RR )
200 min2 11394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( c  e.  RR  /\  d  e.  RR )  ->  if ( c  <_ 
d ,  c ,  d )  <_  d
)
201198, 199, 200syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  RR+  /\  d  e.  RR+ )  ->  if ( c  <_  d ,  c ,  d )  <_  d )
202201ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  if ( c  <_ 
d ,  c ,  d )  <_  d
)
203188, 197, 181, 202leadd2dd 10168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  ( ( g `  z )  +  if ( c  <_  d ,  c ,  d ) )  <_  (
( g `  z
)  +  d ) )
204181, 197readdcld 9621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  ( ( g `  z )  +  d )  e.  RR )
205 letr 9676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( g `  z )  +  if ( c  <_  d ,  c ,  d ) )  e.  RR  /\  ( ( g `  z )  +  d )  e.  RR  /\  ( G `  z )  e.  RR )  -> 
( ( ( ( g `  z )  +  if ( c  <_  d ,  c ,  d ) )  <_  ( ( g `
 z )  +  d )  /\  (
( g `  z
)  +  d )  <_  ( G `  z ) )  -> 
( ( g `  z )  +  if ( c  <_  d ,  c ,  d ) )  <_  ( G `  z )
) )
206189, 204, 191, 205syl3anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  ( ( ( ( g `  z )  +  if ( c  <_  d ,  c ,  d ) )  <_  ( ( g `
 z )  +  d )  /\  (
( g `  z
)  +  d )  <_  ( G `  z ) )  -> 
( ( g `  z )  +  if ( c  <_  d ,  c ,  d ) )  <_  ( G `  z )
) )
207203, 206mpand 675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  ( ( ( g `
 z )  +  d )  <_  ( G `  z )  ->  ( ( g `  z )  +  if ( c  <_  d ,  c ,  d ) )  <_  ( G `  z )
) )
208207imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  /\  ( ( g `  z )  +  d )  <_  ( G `  z ) )  -> 
( ( g `  z )  +  if ( c  <_  d ,  c ,  d ) )  <_  ( G `  z )
)
209170, 168addge02d 10142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  RR )  ->  ( 0  <_  ( F `  z )  <->  ( G `  z )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) )
21017, 209mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  RR )  ->  ( G `
 z )  <_ 
( ( F `  z )  +  ( G `  z ) ) )
211166, 210sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  ( G `  z
)  <_  ( ( F `  z )  +  ( G `  z ) ) )
212211adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  /\  ( ( g `  z )  +  d )  <_  ( G `  z ) )  -> 
( G `  z
)  <_  ( ( F `  z )  +  ( G `  z ) ) )
213190, 192, 195, 208, 212letrd 9737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  /\  ( ( g `  z )  +  d )  <_  ( G `  z ) )  -> 
( ( g `  z )  +  if ( c  <_  d ,  c ,  d ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )
214213adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( c  e.  RR+  /\  d  e.  RR+ )
)  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  /\  ( ( g `  z )  +  d )  <_  ( G `  z ) )  -> 
( ( g `  z )  +  if ( c  <_  d ,  c ,  d ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )
215186, 214eqbrtrd 4453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( c  e.  RR+  /\  d  e.  RR+ )
)  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  /\  ( ( g `  z )  +  d )  <_  ( G `  z ) )  -> 
( ( ( f `
 z )  +  ( g `  z
) )  +  if ( c  <_  d ,  c ,  d ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )
216 breq1 4436 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0  =  if ( ( ( f `  z
)  +  ( g `
 z ) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_ 
d ,  c ,  d ) ) )  ->  ( 0  <_ 
( ( F `  z )  +  ( G `  z ) )  <->  if ( ( ( f `  z )  +  ( g `  z ) )  =  0 ,  0 ,  ( ( ( f `
 z )  +  ( g `  z
) )  +  if ( c  <_  d ,  c ,  d ) ) )  <_ 
( ( F `  z )  +  ( G `  z ) ) ) )
217 breq1 4436 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) )  =  if ( ( ( f `  z )  +  ( g `  z ) )  =  0 ,  0 ,  ( ( ( f `  z
)  +  ( g `
 z ) )  +  if ( c  <_  d ,  c ,  d ) ) )  ->  ( (
( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) )  <_  ( ( F `  z )  +  ( G `  z ) )  <->  if (
( ( f `  z )  +  ( g `  z ) )  =  0 ,  0 ,  ( ( ( f `  z
)  +  ( g `
 z ) )  +  if ( c  <_  d ,  c ,  d ) ) )  <_  ( ( F `  z )  +  ( G `  z ) ) ) )
218216, 217ifboth 3958 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 0  <_  ( ( F `  z )  +  ( G `  z ) )  /\  ( ( ( f `
 z )  +  ( g `  z
) )  +  if ( c  <_  d ,  c ,  d ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )  ->  if (
( ( f `  z )  +  ( g `  z ) )  =  0 ,  0 ,  ( ( ( f `  z
)  +  ( g `
 z ) )  +  if ( c  <_  d ,  c ,  d ) ) )  <_  ( ( F `  z )  +  ( G `  z ) ) )
219176, 215, 218syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( c  e.  RR+  /\  d  e.  RR+ )
)  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  /\  ( ( g `  z )  +  d )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )
220219ex 434 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  /\  ( f `  z
)  =  0 )  ->  ( ( ( g `  z )  +  d )  <_ 
( G `  z
)  ->  if (
( ( f `  z )  +  ( g `  z ) )  =  0 ,  0 ,  ( ( ( f `  z
)  +  ( g `
 z ) )  +  if ( c  <_  d ,  c ,  d ) ) )  <_  ( ( F `  z )  +  ( G `  z ) ) ) )
221220adantld 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  /\  ( f `  z
)  =  0 )  ->  ( ( 0  <_  ( F `  z )  /\  (
( g `  z
)  +  d )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) )
222221adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( c  e.  RR+  /\  d  e.  RR+ )
)  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  /\  -.  ( g `  z
)  =  0 )  ->  ( ( 0  <_  ( F `  z )  /\  (
( g `  z
)  +  d )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) )
223157, 160, 175, 222ifbothda 3957 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  /\  ( f `  z
)  =  0 )  ->  ( ( 0  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) )
224155anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( ( ( ( f `  z )  +  c )  <_ 
( F `  z
)  /\  0  <_  ( G `  z ) )  <->  ( ( ( f `  z )  +  c )  <_ 
( F `  z
)  /\  if (
( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  d ) )  <_  ( G `  z ) ) ) )
225224imbi1d 317 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( ( ( ( ( f `  z
)  +  c )  <_  ( F `  z )  /\  0  <_  ( G `  z
) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )  <->  ( ( ( ( f `  z
)  +  c )  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) ) )
226158anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( g `  z
)  +  d )  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( ( ( ( f `  z )  +  c )  <_ 
( F `  z
)  /\  ( (
g `  z )  +  d )  <_ 
( G `  z
) )  <->  ( (
( f `  z
)  +  c )  <_  ( F `  z )  /\  if ( ( g `