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

Theorem itg2addnc 28290
Description: Alternate proof of itg2add 21079 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 21028, 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 8592, 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 749 . . . . . . 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 21005 . . . . . . . 8  |-  ( f  e.  dom  S.1  ->  ( S.1 `  f )  e.  RR )
32adantr 462 . . . . . . 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 2507 . . . . . 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 2826 . . . . 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 3415 . . . 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 21007 . . . . . 6  |-  ( RR 
X.  { 0 } )  e.  dom  S.1
9 3nn 10468 . . . . . . . 8  |-  3  e.  NN
10 nnrp 10988 . . . . . . . 8  |-  ( 3  e.  NN  ->  3  e.  RR+ )
11 ne0i 3631 . . . . . . . 8  |-  ( 3  e.  RR+  ->  RR+  =/=  (/) )
129, 10, 11mp2b 10 . . . . . . 7  |-  RR+  =/=  (/)
13 itg2addnc.f2 . . . . . . . . . . . . 13  |-  ( ph  ->  F : RR --> ( 0 [,) +oo ) )
1413ffvelrnda 5831 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  RR )  ->  ( F `
 z )  e.  ( 0 [,) +oo ) )
15 elrege0 11380 . . . . . . . . . . . 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 460 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  RR )  ->  0  <_ 
( F `  z
) )
1817ralrimiva 2789 . . . . . . . . 9  |-  ( ph  ->  A. z  e.  RR  0  <_  ( F `  z ) )
19 reex 9361 . . . . . . . . . . 11  |-  RR  e.  _V
2019a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  e.  _V )
21 c0ex 9368 . . . . . . . . . . 11  |-  0  e.  _V
2221a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  RR )  ->  0  e. 
_V )
23 eqidd 2434 . . . . . . . . . 10  |-  ( ph  ->  ( z  e.  RR  |->  0 )  =  ( z  e.  RR  |->  0 ) )
2413feqmptd 5732 . . . . . . . . . 10  |-  ( ph  ->  F  =  ( z  e.  RR  |->  ( F `
 z ) ) )
2520, 22, 14, 23, 24ofrfval2 6326 . . . . . . . . 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 2790 . . . . . . 7  |-  ( ph  ->  A. c  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  F )
28 r19.2z 3757 . . . . . . 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 656 . . . . . 6  |-  ( ph  ->  E. c  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  F )
30 fveq2 5679 . . . . . . . . . 10  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( S.1 `  f
)  =  ( S.1 `  ( RR  X.  {
0 } ) ) )
31 itg10 21008 . . . . . . . . . 10  |-  ( S.1 `  ( RR  X.  {
0 } ) )  =  0
3230, 31syl6req 2482 . . . . . . . . 9  |-  ( f  =  ( RR  X.  { 0 } )  ->  0  =  ( S.1 `  f ) )
3332biantrud 504 . . . . . . . 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 5678 . . . . . . . . . . . . 13  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( f `  z )  =  ( ( RR  X.  {
0 } ) `  z ) )
3521fvconst2 5920 . . . . . . . . . . . . 13  |-  ( z  e.  RR  ->  (
( RR  X.  {
0 } ) `  z )  =  0 )
3634, 35sylan9eq 2485 . . . . . . . . . . . 12  |-  ( ( f  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  (
f `  z )  =  0 )
37 iftrue 3785 . . . . . . . . . . . 12  |-  ( ( f `  z )  =  0  ->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) )  =  0 )
3836, 37syl 16 . . . . . . . . . . 11  |-  ( ( f  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) )  =  0 )
3938mpteq2dva 4366 . . . . . . . . . 10  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  =  ( z  e.  RR  |->  0 ) )
4039breq1d 4290 . . . . . . . . 9  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( ( z  e.  RR  |->  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  c ) ) )  oR  <_  F 
<->  ( z  e.  RR  |->  0 )  oR  <_  F ) )
4140rexbidv 2726 . . . . . . . 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 ) )
4233, 41bitr3d 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 )
)
4342rspcev 3062 . . . . . 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
) ) )
448, 29, 43sylancr 656 . . . . 5  |-  ( ph  ->  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  0  =  ( S.1 `  f
) ) )
45 eqeq1 2439 . . . . . . . 8  |-  ( x  =  0  ->  (
x  =  ( S.1 `  f )  <->  0  =  ( S.1 `  f ) ) )
4645anbi2d 696 . . . . . . 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 ) ) ) )
4746rexbidv 2726 . . . . . 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 ) ) ) )
4821, 47elab 3095 . . . . 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 ) ) )
4944, 48sylibr 212 . . . 4  |-  ( ph  ->  0  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } )
50 ne0i 3631 . . . 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 ) ) }  =/=  (/) )
5149, 50syl 16 . . 3  |-  ( ph  ->  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  =/=  (/) )
52 rexr 9417 . . . . . . . . . 10  |-  ( x  e.  RR  ->  x  e.  RR* )
5352anim1i 563 . . . . . . . . 9  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( x  e.  RR*  /\  0  <_  x )
)
54 elrege0 11380 . . . . . . . . 9  |-  ( x  e.  ( 0 [,) +oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
55 elxrge0 11381 . . . . . . . . 9  |-  ( x  e.  ( 0 [,] +oo )  <->  ( x  e. 
RR*  /\  0  <_  x ) )
5653, 54, 553imtr4i 266 . . . . . . . 8  |-  ( x  e.  ( 0 [,) +oo )  ->  x  e.  ( 0 [,] +oo ) )
5756ssriv 3348 . . . . . . 7  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
58 fss 5555 . . . . . . 7  |-  ( ( F : RR --> ( 0 [,) +oo )  /\  ( 0 [,) +oo )  C_  ( 0 [,] +oo ) )  ->  F : RR --> ( 0 [,] +oo ) )
5957, 58mpan2 664 . . . . . 6  |-  ( F : RR --> ( 0 [,) +oo )  ->  F : RR --> ( 0 [,] +oo ) )
60 eqid 2433 . . . . . . 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
) ) }
6160itg2addnclem 28287 . . . . . 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* ,  <  ) )
6213, 59, 613syl 20 . . . . 5  |-  ( ph  ->  ( S.2 `  F
)  =  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  ) )
63 itg2addnc.f3 . . . . 5  |-  ( ph  ->  ( S.2 `  F
)  e.  RR )
6462, 63eqeltrrd 2508 . . . 4  |-  ( ph  ->  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  )  e.  RR )
65 ressxr 9415 . . . . . . 7  |-  RR  C_  RR*
666, 65sstri 3353 . . . . . 6  |-  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  C_  RR*
67 supxrub 11275 . . . . . 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* ,  <  ) )
6866, 67mpan 663 . . . . 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* ,  <  ) )
6968rgen 2771 . . . 4  |-  A. b  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } b  <_  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  )
70 breq2 4284 . . . . . 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* ,  <  ) ) )
7170ralbidv 2725 . . . . 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* ,  <  ) ) )
7271rspcev 3062 . . . 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 )
7364, 69, 72sylancl 655 . . 3  |-  ( ph  ->  E. a  e.  RR  A. b  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } b  <_  a )
74 simprr 749 . . . . . . 7  |-  ( ( g  e.  dom  S.1  /\  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) )  ->  x  =  ( S.1 `  g ) )
75 itg1cl 21005 . . . . . . . 8  |-  ( g  e.  dom  S.1  ->  ( S.1 `  g )  e.  RR )
7675adantr 462 . . . . . . 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 )
7774, 76eqeltrd 2507 . . . . . 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 )
7877rexlimiva 2826 . . . . 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 )
7978abssi 3415 . . . 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
8079a1i 11 . . 3  |-  ( ph  ->  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }  C_  RR )
81 itg2addnc.g2 . . . . . . . . . . . . 13  |-  ( ph  ->  G : RR --> ( 0 [,) +oo ) )
8281ffvelrnda 5831 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  RR )  ->  ( G `
 z )  e.  ( 0 [,) +oo ) )
83 elrege0 11380 . . . . . . . . . . . 12  |-  ( ( G `  z )  e.  ( 0 [,) +oo )  <->  ( ( G `
 z )  e.  RR  /\  0  <_ 
( G `  z
) ) )
8482, 83sylib 196 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  RR )  ->  ( ( G `  z )  e.  RR  /\  0  <_  ( G `  z
) ) )
8584simprd 460 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  RR )  ->  0  <_ 
( G `  z
) )
8685ralrimiva 2789 . . . . . . . . 9  |-  ( ph  ->  A. z  e.  RR  0  <_  ( G `  z ) )
8781feqmptd 5732 . . . . . . . . . 10  |-  ( ph  ->  G  =  ( z  e.  RR  |->  ( G `
 z ) ) )
8820, 22, 82, 23, 87ofrfval2 6326 . . . . . . . . 9  |-  ( ph  ->  ( ( z  e.  RR  |->  0 )  oR  <_  G  <->  A. z  e.  RR  0  <_  ( G `  z )
) )
8986, 88mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( z  e.  RR  |->  0 )  oR  <_  G )
9089ralrimivw 2790 . . . . . . 7  |-  ( ph  ->  A. d  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  G )
91 r19.2z 3757 . . . . . . 7  |-  ( (
RR+  =/=  (/)  /\  A. d  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  G
)  ->  E. d  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  G )
9212, 90, 91sylancr 656 . . . . . 6  |-  ( ph  ->  E. d  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  G )
93 fveq2 5679 . . . . . . . . . 10  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( S.1 `  g
)  =  ( S.1 `  ( RR  X.  {
0 } ) ) )
9493, 31syl6req 2482 . . . . . . . . 9  |-  ( g  =  ( RR  X.  { 0 } )  ->  0  =  ( S.1 `  g ) )
9594biantrud 504 . . . . . . . 8  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  oR  <_  G  <->  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  0  =  ( S.1 `  g
) ) ) )
96 fveq1 5678 . . . . . . . . . . . . 13  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( g `  z )  =  ( ( RR  X.  {
0 } ) `  z ) )
9796, 35sylan9eq 2485 . . . . . . . . . . . 12  |-  ( ( g  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  (
g `  z )  =  0 )
98 iftrue 3785 . . . . . . . . . . . 12  |-  ( ( g `  z )  =  0  ->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  =  0 )
9997, 98syl 16 . . . . . . . . . . 11  |-  ( ( g  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  =  0 )
10099mpteq2dva 4366 . . . . . . . . . 10  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  =  ( z  e.  RR  |->  0 ) )
101100breq1d 4290 . . . . . . . . 9  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( ( z  e.  RR  |->  if ( ( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  d ) ) )  oR  <_  G 
<->  ( z  e.  RR  |->  0 )  oR  <_  G ) )
102101rexbidv 2726 . . . . . . . 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 ) )
10395, 102bitr3d 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 )
)
104103rspcev 3062 . . . . . 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
) ) )
1058, 92, 104sylancr 656 . . . . 5  |-  ( ph  ->  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  0  =  ( S.1 `  g
) ) )
106 eqeq1 2439 . . . . . . . 8  |-  ( x  =  0  ->  (
x  =  ( S.1 `  g )  <->  0  =  ( S.1 `  g ) ) )
107106anbi2d 696 . . . . . . 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 ) ) ) )
108107rexbidv 2726 . . . . . 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 ) ) ) )
10921, 108elab 3095 . . . . 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 ) ) )
110105, 109sylibr 212 . . . 4  |-  ( ph  ->  0  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } )
111 ne0i 3631 . . . 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 ) ) }  =/=  (/) )
112110, 111syl 16 . . 3  |-  ( ph  ->  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }  =/=  (/) )
113 fss 5555 . . . . . . 7  |-  ( ( G : RR --> ( 0 [,) +oo )  /\  ( 0 [,) +oo )  C_  ( 0 [,] +oo ) )  ->  G : RR --> ( 0 [,] +oo ) )
11457, 113mpan2 664 . . . . . 6  |-  ( G : RR --> ( 0 [,) +oo )  ->  G : RR --> ( 0 [,] +oo ) )
115 eqid 2433 . . . . . . 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
) ) }
116115itg2addnclem 28287 . . . . . 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* ,  <  ) )
11781, 114, 1163syl 20 . . . . 5  |-  ( ph  ->  ( S.2 `  G
)  =  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  ) )
118 itg2addnc.g3 . . . . 5  |-  ( ph  ->  ( S.2 `  G
)  e.  RR )
119117, 118eqeltrrd 2508 . . . 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 )
12079, 65sstri 3353 . . . . . 6  |-  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) }  C_  RR*
121 supxrub 11275 . . . . . 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* ,  <  ) )
122120, 121mpan 663 . . . . 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* ,  <  ) )
123122rgen 2771 . . . 4  |-  A. b  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } b  <_  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  )
124 breq2 4284 . . . . . 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* ,  <  ) ) )
125124ralbidv 2725 . . . . 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* ,  <  ) ) )
126125rspcev 3062 . . . 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 )
127119, 123, 126sylancl 655 . . 3  |-  ( ph  ->  E. a  e.  RR  A. b  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } b  <_  a )
128 eqid 2433 . . 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 ) }
1297, 51, 73, 80, 112, 127, 128supadd 28262 . 2  |-  ( ph  ->  ( sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR ,  <  )  +  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR ,  <  ) )  =  sup ( { s  |  E. t  e.  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } E. u  e.  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } s  =  ( t  +  u ) } ,  RR ,  <  ) )
130 supxrre 11278 . . . . 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 ,  <  ) )
1317, 51, 73, 130syl3anc 1211 . . . 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 ,  <  ) )
13262, 131eqtrd 2465 . . 3  |-  ( ph  ->  ( S.2 `  F
)  =  sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR ,  <  ) )
133 supxrre 11278 . . . . 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 ,  <  ) )
13480, 112, 127, 133syl3anc 1211 . . . 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 ,  <  ) )
135117, 134eqtrd 2465 . . 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 ,  <  ) )
136132, 135oveq12d 6098 . 2  |-  ( ph  ->  ( ( S.2 `  F
)  +  ( S.2 `  G ) )  =  ( sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR ,  <  )  +  sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR ,  <  ) ) )
137 ge0addcl 11384 . . . . . . 7  |-  ( ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  +  y )  e.  ( 0 [,) +oo )
)
13857, 137sseldi 3342 . . . . . 6  |-  ( ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  +  y )  e.  ( 0 [,] +oo )
)
139138adantl 463 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo )
) )  ->  (
x  +  y )  e.  ( 0 [,] +oo ) )
140 inidm 3547 . . . . 5  |-  ( RR 
i^i  RR )  =  RR
141139, 13, 81, 20, 20, 140off 6323 . . . 4  |-  ( ph  ->  ( F  oF  +  G ) : RR --> ( 0 [,] +oo ) )
142 eqid 2433 . . . . 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 ) ) }
143142itg2addnclem 28287 . . . 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* ,  <  ) )
144141, 143syl 16 . . 3  |-  ( ph  ->  ( S.2 `  ( F  oF  +  G
) )  =  sup ( { s  |  E. h  e.  dom  S.1 ( E. y  e.  RR+  (
z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `  z
)  +  y ) ) )  oR  <_  ( F  oF  +  G )  /\  s  =  ( S.1 `  h ) ) } ,  RR* ,  <  ) )
145 itg2addnc.f1 . . . . . . . 8  |-  ( ph  ->  F  e. MblFn )
146145, 13, 63, 81, 118itg2addnclem3 28289 . . . . . . 7  |-  ( ph  ->  ( E. h  e. 
dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `
 z )  +  y ) ) )  oR  <_  ( F  oF  +  G
)  /\  s  =  ( S.1 `  h ) )  ->  E. t E. u ( E. f  e.  dom  S.1 E. g  e. 
dom  S.1 ( ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  t  =  ( S.1 `  f
) )  /\  ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  u  =  ( S.1 `  g
) ) )  /\  s  =  ( t  +  u ) ) ) )
147 simpl 454 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  f  e.  dom  S.1 )
148 simpr 458 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  g  e.  dom  S.1 )
149147, 148i1fadd 21015 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( f  oF  +  g )  e.  dom  S.1 )
150149ad3antlr 723 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  t  =  ( S.1 `  f
) )  /\  ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  u  =  ( S.1 `  g
) ) ) )  /\  s  =  ( t  +  u ) )  ->  ( f  oF  +  g
)  e.  dom  S.1 )
151 reeanv 2878 . . . . . . . . . . . . . . . . 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 ) )
152151biimpri 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 ) )
153152ad2ant2r 739 . . . . . . . . . . . . . . 15  |-  ( ( ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  oR  <_  F  /\  t  =  ( S.1 `  f
) )  /\  ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G  /\  u  =  ( S.1 `  g
) ) )  ->  E. c  e.  RR+  E. d  e.  RR+  ( ( z  e.  RR  |->  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  c ) ) )  oR  <_  F  /\  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  oR  <_  G
) )
154 ifcl 3819 . . . . . . . . . . . . . . . . . . 19  |-  ( ( c  e.  RR+  /\  d  e.  RR+ )  ->  if ( c  <_  d ,  c ,  d )  e.  RR+ )
155154ad2antlr 719 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  ( ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  oR  <_  F  /\  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  oR  <_  G ) )  ->  if ( c  <_  d ,  c ,  d )  e.  RR+ )
156 breq1 4283 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0  =  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) )  -> 
( 0  <_  ( F `  z )  <->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) )  <_  ( F `  z ) ) )
157156anbi1d 697 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
158157imbi1d 317 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  =  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) )  -> 
( ( ( 0  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )  <->  ( ( if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) )  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) ) )
159 breq1 4283 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
160159anbi1d 697 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
161160imbi1d 317 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( f `  z
)  +  c )  =  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) )  -> 
( ( ( ( ( f `  z
)  +  c )  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )  <->  ( ( if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) )  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) ) )
162 breq1 4283 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( 0  <_  ( G `  z )  <->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) ) )
163162anbi2d 696 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
164163imbi1d 317 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( ( ( 0  <_  ( F `  z )  /\  0  <_  ( G `  z
) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )  <->  ( ( 0  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) ) )
165 breq1 4283 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
166165anbi2d 696 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
167166imbi1d 317 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( g `  z
)  +  d )  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( ( ( 0  <_  ( F `  z )  /\  (
( g `  z
)  +  d )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )  <->  ( ( 0  <_  ( F `  z )  /\  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) )  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) ) )
168 oveq12 6089 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( f `  z
)  =  0  /\  ( g `  z
)  =  0 )  ->  ( ( f `
 z )  +  ( g `  z
) )  =  ( 0  +  0 ) )
169 00id 9532 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0  +  0 )  =  0
170168, 169syl6eq 2481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f `  z
)  =  0  /\  ( g `  z
)  =  0 )  ->  ( ( f `
 z )  +  ( g `  z
) )  =  0 )
171 iftrue 3785 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f `  z
)  +  ( g `
 z ) )  =  0  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  =  0 )
172170, 171syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( f `  z
)  =  0  /\  ( g `  z
)  =  0 )  ->  if ( ( ( f `  z
)  +  ( g `
 z ) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_ 
d ,  c ,  d ) ) )  =  0 )
173172adantll 706 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( c  e.  RR+  /\  d  e.  RR+ )
)  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  /\  ( g `  z
)  =  0 )  ->  if ( ( ( f `  z
)  +  ( g `
 z ) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_ 
d ,  c ,  d ) ) )  =  0 )
174 simpll 746 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  ->  ph )
17515simplbi 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F `  z )  e.  ( 0 [,) +oo )  ->  ( F `
 z )  e.  RR )
17614, 175syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR )  ->  ( F `
 z )  e.  RR )
17783simplbi 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( G `  z )  e.  ( 0 [,) +oo )  ->  ( G `
 z )  e.  RR )
17882, 177syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR )  ->  ( G `
 z )  e.  RR )
179176, 178, 17, 85addge0d 9903 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  z  e.  RR )  ->  0  <_ 
( ( F `  z )  +  ( G `  z ) ) )
180174, 179sylan 468 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
181180ad2antrr 718 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
182173, 181eqbrtrd 4300 . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
183182a1d 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 ) ) ) )
184180ad2antrr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( c  e.  RR+  /\  d  e.  RR+ )
)  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  /\  ( ( g `  z )  +  d )  <_  ( G `  z ) )  -> 
0  <_  ( ( F `  z )  +  ( G `  z ) ) )
185 oveq1 6087 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( f `  z )  =  0  ->  (
( f `  z
)  +  ( g `
 z ) )  =  ( 0  +  ( g `  z
) ) )
186 simplrr 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  -> 
g  e.  dom  S.1 )
187 i1ff 20996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
188187ffvelrnda 5831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( g  e.  dom  S.1  /\  z  e.  RR )  ->  ( g `  z )  e.  RR )
189186, 188sylan 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
190189recnd 9400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
191190addid2d 9558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
192185, 191sylan9eqr 2487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
193192oveq1d 6095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
194193adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
195154rpred 11015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( c  e.  RR+  /\  d  e.  RR+ )  ->  if ( c  <_  d ,  c ,  d )  e.  RR )
196195ad2antlr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
197189, 196readdcld 9401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
198197adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
199174, 178sylan 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
200199adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
201174, 176sylan 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
202201, 199readdcld 9401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
203202adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  /\  ( ( g `  z )  +  d )  <_  ( G `  z ) )  -> 
( ( F `  z )  +  ( G `  z ) )  e.  RR )
204 simplrr 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  d  e.  RR+ )
205204rpred 11015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  d  e.  RR )
206 rpre 10985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  e.  RR+  ->  c  e.  RR )
207 rpre 10985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( d  e.  RR+  ->  d  e.  RR )
208 min2 11149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( c  e.  RR  /\  d  e.  RR )  ->  if ( c  <_ 
d ,  c ,  d )  <_  d
)
209206, 207, 208syl2an 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  RR+  /\  d  e.  RR+ )  ->  if ( c  <_  d ,  c ,  d )  <_  d )
210209ad2antlr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
211196, 205, 189, 210leadd2dd 9942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
212189, 205readdcld 9401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  ( ( g `  z )  +  d )  e.  RR )
213 letr 9456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
214197, 212, 199, 213syl3anc 1211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
215211, 214mpand 668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
216215imp 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 )
)
217178, 176addge02d 9916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  RR )  ->  ( 0  <_  ( F `  z )  <->  ( G `  z )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) )
21817, 217mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  RR )  ->  ( G `
 z )  <_ 
( ( F `  z )  +  ( G `  z ) ) )
219174, 218sylan 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
220219adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
221198, 200, 203, 216, 220letrd 9516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
222221adantlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
223194, 222eqbrtrd 4300 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( c  e.  RR+  /\  d  e.  RR+ )
)  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  /\  ( ( g `  z )  +  d )  <_  ( G `  z ) )  -> 
( ( ( f `
 z )  +  ( g `  z
) )  +  if ( c  <_  d ,  c ,  d ) )  <_  (
( F `  z
)  +  ( G `
 z ) ) )
224 breq1 4283 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0  =  if ( ( ( f `  z
)  +  ( g `
 z ) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_ 
d ,  c ,  d ) ) )  ->  ( 0  <_ 
( ( F `  z )  +  ( G `  z ) )  <->  if ( ( ( f `  z )  +  ( g `  z ) )  =  0 ,  0 ,  ( ( ( f `
 z )  +  ( g `  z
) )  +  if ( c  <_  d ,  c ,  d ) ) )  <_ 
( ( F `  z )  +  ( G `  z ) ) ) )
225 breq1 4283 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
226224, 225ifboth 3813 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
227184, 223, 226syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
228227ex 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 ) ) ) )
229228adantld 464 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
230229adantr 462 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
231164, 167, 183, 230ifbothda 3812 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
232162anbi2d 696 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
233232imbi1d 317 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( ( ( ( ( f `  z
)  +  c )  <_  ( F `  z )  /\  0  <_  ( G `  z
) )