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

Theorem itg2addnc 26222
Description: Alternate proof of itg2add 19641 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 19590, 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 8305, 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  o F  +  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 734 . . . . . . 7  |-  ( ( f  e.  dom  S.1  /\  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  =  ( S.1 `  f ) )
2 itg1cl 19567 . . . . . . . 8  |-  ( f  e.  dom  S.1  ->  ( S.1 `  f )  e.  RR )
32adantr 452 . . . . . . 7  |-  ( ( f  e.  dom  S.1  /\  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) )  -> 
( S.1 `  f )  e.  RR )
41, 3eqeltrd 2509 . . . . . 6  |-  ( ( f  e.  dom  S.1  /\  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  e.  RR )
54rexlimiva 2817 . . . . 5  |-  ( E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) )  ->  x  e.  RR )
65abssi 3410 . . . 4  |-  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) }  C_  RR )
8 i1f0 19569 . . . . . 6  |-  ( RR 
X.  { 0 } )  e.  dom  S.1
9 3nn 10124 . . . . . . . 8  |-  3  e.  NN
10 nnrp 10611 . . . . . . . 8  |-  ( 3  e.  NN  ->  3  e.  RR+ )
11 ne0i 3626 . . . . . . . 8  |-  ( 3  e.  RR+  ->  RR+  =/=  (/) )
129, 10, 11mp2b 10 . . . . . . 7  |-  RR+  =/=  (/)
13 itg2addnc.f2 . . . . . . . . . . . . 13  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
1413ffvelrnda 5862 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  RR )  ->  ( F `
 z )  e.  ( 0 [,)  +oo ) )
15 elrege0 10997 . . . . . . . . . . . 12  |-  ( ( F `  z )  e.  ( 0 [,) 
+oo )  <->  ( ( F `  z )  e.  RR  /\  0  <_ 
( F `  z
) ) )
1614, 15sylib 189 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  RR )  ->  ( ( F `  z )  e.  RR  /\  0  <_  ( F `  z
) ) )
1716simprd 450 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  RR )  ->  0  <_ 
( F `  z
) )
1817ralrimiva 2781 . . . . . . . . 9  |-  ( ph  ->  A. z  e.  RR  0  <_  ( F `  z ) )
19 reex 9071 . . . . . . . . . . 11  |-  RR  e.  _V
2019a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  e.  _V )
21 c0ex 9075 . . . . . . . . . . 11  |-  0  e.  _V
2221a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  RR )  ->  0  e. 
_V )
23 eqidd 2436 . . . . . . . . . 10  |-  ( ph  ->  ( z  e.  RR  |->  0 )  =  ( z  e.  RR  |->  0 ) )
2413feqmptd 5771 . . . . . . . . . 10  |-  ( ph  ->  F  =  ( z  e.  RR  |->  ( F `
 z ) ) )
2520, 22, 14, 23, 24ofrfval2 6315 . . . . . . . . 9  |-  ( ph  ->  ( ( z  e.  RR  |->  0 )  o R  <_  F  <->  A. z  e.  RR  0  <_  ( F `  z )
) )
2618, 25mpbird 224 . . . . . . . 8  |-  ( ph  ->  ( z  e.  RR  |->  0 )  o R  <_  F )
2726ralrimivw 2782 . . . . . . 7  |-  ( ph  ->  A. c  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  F )
28 r19.2z 3709 . . . . . . 7  |-  ( (
RR+  =/=  (/)  /\  A. c  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  F
)  ->  E. c  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  F )
2912, 27, 28sylancr 645 . . . . . 6  |-  ( ph  ->  E. c  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  F )
30 fveq2 5720 . . . . . . . . . 10  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( S.1 `  f
)  =  ( S.1 `  ( RR  X.  {
0 } ) ) )
31 itg10 19570 . . . . . . . . . 10  |-  ( S.1 `  ( RR  X.  {
0 } ) )  =  0
3230, 31syl6req 2484 . . . . . . . . 9  |-  ( f  =  ( RR  X.  { 0 } )  ->  0  =  ( S.1 `  f ) )
3332biantrud 494 . . . . . . . 8  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  o R  <_  F  <->  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  F  /\  0  =  ( S.1 `  f
) ) ) )
34 fveq1 5719 . . . . . . . . . . . . 13  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( f `  z )  =  ( ( RR  X.  {
0 } ) `  z ) )
3521fvconst2 5939 . . . . . . . . . . . . 13  |-  ( z  e.  RR  ->  (
( RR  X.  {
0 } ) `  z )  =  0 )
3634, 35sylan9eq 2487 . . . . . . . . . . . 12  |-  ( ( f  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  (
f `  z )  =  0 )
37 iftrue 3737 . . . . . . . . . . . 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 4287 . . . . . . . . . 10  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  =  ( z  e.  RR  |->  0 ) )
4039breq1d 4214 . . . . . . . . 9  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( ( z  e.  RR  |->  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  c ) ) )  o R  <_  F 
<->  ( z  e.  RR  |->  0 )  o R  <_  F ) )
4140rexbidv 2718 . . . . . . . 8  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  o R  <_  F  <->  E. c  e.  RR+  (
z  e.  RR  |->  0 )  o R  <_  F ) )
4233, 41bitr3d 247 . . . . . . 7  |-  ( f  =  ( RR  X.  { 0 } )  ->  ( ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  F  /\  0  =  ( S.1 `  f
) )  <->  E. c  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  F )
)
4342rspcev 3044 . . . . . 6  |-  ( ( ( RR  X.  {
0 } )  e. 
dom  S.1  /\  E. c  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  F )  ->  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  F  /\  0  =  ( S.1 `  f
) ) )
448, 29, 43sylancr 645 . . . . 5  |-  ( ph  ->  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  F  /\  0  =  ( S.1 `  f
) ) )
45 eqeq1 2441 . . . . . . . 8  |-  ( x  =  0  ->  (
x  =  ( S.1 `  f )  <->  0  =  ( S.1 `  f ) ) )
4645anbi2d 685 . . . . . . 7  |-  ( x  =  0  ->  (
( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) )  <->  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  c ) ) )  o R  <_  F  /\  0  =  ( S.1 `  f ) ) ) )
4746rexbidv 2718 . . . . . 6  |-  ( x  =  0  ->  ( E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  0  =  ( S.1 `  f ) ) ) )
4821, 47elab 3074 . . . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  0  =  ( S.1 `  f ) ) )
4944, 48sylibr 204 . . . 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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } )
50 ne0i 3626 . . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) }  =/=  (/) )
52 icossicc 24119 . . . . . . 7  |-  ( 0 [,)  +oo )  C_  (
0 [,]  +oo )
53 fss 5591 . . . . . . 7  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  ( 0 [,]  +oo ) )  ->  F : RR --> ( 0 [,] 
+oo ) )
5452, 53mpan2 653 . . . . . 6  |-  ( F : RR --> ( 0 [,)  +oo )  ->  F : RR --> ( 0 [,] 
+oo ) )
55 eqid 2435 . . . . . . 7  |-  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) }
5655itg2addnclem 26219 . . . . . 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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  ) )
5713, 54, 563syl 19 . . . . 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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  ) )
58 itg2addnc.f3 . . . . 5  |-  ( ph  ->  ( S.2 `  F
)  e.  RR )
5957, 58eqeltrrd 2510 . . . 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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  )  e.  RR )
60 ressxr 9119 . . . . . . 7  |-  RR  C_  RR*
616, 60sstri 3349 . . . . . 6  |-  { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) }  C_  RR*
62 supxrub 10893 . . . . . 6  |-  ( ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  ) )
6361, 62mpan 652 . . . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  ) )
6463rgen 2763 . . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  )
65 breq2 4208 . . . . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  ) ) )
6665ralbidv 2717 . . . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  ) ) )
6766rspcev 3044 . . . 4  |-  ( ( sup ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } b  <_  a )
6859, 64, 67sylancl 644 . . 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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } b  <_  a )
69 simprr 734 . . . . . . 7  |-  ( ( g  e.  dom  S.1  /\  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) )  ->  x  =  ( S.1 `  g ) )
70 itg1cl 19567 . . . . . . . 8  |-  ( g  e.  dom  S.1  ->  ( S.1 `  g )  e.  RR )
7170adantr 452 . . . . . . 7  |-  ( ( g  e.  dom  S.1  /\  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) )  -> 
( S.1 `  g )  e.  RR )
7269, 71eqeltrd 2509 . . . . . 6  |-  ( ( g  e.  dom  S.1  /\  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) )  ->  x  e.  RR )
7372rexlimiva 2817 . . . . 5  |-  ( E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) )  ->  x  e.  RR )
7473abssi 3410 . . . 4  |-  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) }  C_  RR
7574a1i 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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) }  C_  RR )
76 itg2addnc.g2 . . . . . . . . . . . . 13  |-  ( ph  ->  G : RR --> ( 0 [,)  +oo ) )
7776ffvelrnda 5862 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  RR )  ->  ( G `
 z )  e.  ( 0 [,)  +oo ) )
78 elrege0 10997 . . . . . . . . . . . 12  |-  ( ( G `  z )  e.  ( 0 [,) 
+oo )  <->  ( ( G `  z )  e.  RR  /\  0  <_ 
( G `  z
) ) )
7977, 78sylib 189 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  RR )  ->  ( ( G `  z )  e.  RR  /\  0  <_  ( G `  z
) ) )
8079simprd 450 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  RR )  ->  0  <_ 
( G `  z
) )
8180ralrimiva 2781 . . . . . . . . 9  |-  ( ph  ->  A. z  e.  RR  0  <_  ( G `  z ) )
8276feqmptd 5771 . . . . . . . . . 10  |-  ( ph  ->  G  =  ( z  e.  RR  |->  ( G `
 z ) ) )
8320, 22, 77, 23, 82ofrfval2 6315 . . . . . . . . 9  |-  ( ph  ->  ( ( z  e.  RR  |->  0 )  o R  <_  G  <->  A. z  e.  RR  0  <_  ( G `  z )
) )
8481, 83mpbird 224 . . . . . . . 8  |-  ( ph  ->  ( z  e.  RR  |->  0 )  o R  <_  G )
8584ralrimivw 2782 . . . . . . 7  |-  ( ph  ->  A. d  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  G )
86 r19.2z 3709 . . . . . . 7  |-  ( (
RR+  =/=  (/)  /\  A. d  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  G
)  ->  E. d  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  G )
8712, 85, 86sylancr 645 . . . . . 6  |-  ( ph  ->  E. d  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  G )
88 fveq2 5720 . . . . . . . . . 10  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( S.1 `  g
)  =  ( S.1 `  ( RR  X.  {
0 } ) ) )
8988, 31syl6req 2484 . . . . . . . . 9  |-  ( g  =  ( RR  X.  { 0 } )  ->  0  =  ( S.1 `  g ) )
9089biantrud 494 . . . . . . . 8  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  o R  <_  G  <->  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  0  =  ( S.1 `  g
) ) ) )
91 fveq1 5719 . . . . . . . . . . . . 13  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( g `  z )  =  ( ( RR  X.  {
0 } ) `  z ) )
9291, 35sylan9eq 2487 . . . . . . . . . . . 12  |-  ( ( g  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  (
g `  z )  =  0 )
93 iftrue 3737 . . . . . . . . . . . 12  |-  ( ( g `  z )  =  0  ->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  =  0 )
9492, 93syl 16 . . . . . . . . . . 11  |-  ( ( g  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  =  0 )
9594mpteq2dva 4287 . . . . . . . . . 10  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  =  ( z  e.  RR  |->  0 ) )
9695breq1d 4214 . . . . . . . . 9  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( ( z  e.  RR  |->  if ( ( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  d ) ) )  o R  <_  G 
<->  ( z  e.  RR  |->  0 )  o R  <_  G ) )
9796rexbidv 2718 . . . . . . . 8  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  o R  <_  G  <->  E. d  e.  RR+  (
z  e.  RR  |->  0 )  o R  <_  G ) )
9890, 97bitr3d 247 . . . . . . 7  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  0  =  ( S.1 `  g
) )  <->  E. d  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  G )
)
9998rspcev 3044 . . . . . 6  |-  ( ( ( RR  X.  {
0 } )  e. 
dom  S.1  /\  E. d  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  G )  ->  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  0  =  ( S.1 `  g
) ) )
1008, 87, 99sylancr 645 . . . . 5  |-  ( ph  ->  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  0  =  ( S.1 `  g
) ) )
101 eqeq1 2441 . . . . . . . 8  |-  ( x  =  0  ->  (
x  =  ( S.1 `  g )  <->  0  =  ( S.1 `  g ) ) )
102101anbi2d 685 . . . . . . 7  |-  ( x  =  0  ->  (
( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) )  <->  ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  d ) ) )  o R  <_  G  /\  0  =  ( S.1 `  g ) ) ) )
103102rexbidv 2718 . . . . . 6  |-  ( x  =  0  ->  ( E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  0  =  ( S.1 `  g ) ) ) )
10421, 103elab 3074 . . . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  0  =  ( S.1 `  g ) ) )
105100, 104sylibr 204 . . . 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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } )
106 ne0i 3626 . . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g ) ) }  =/=  (/) )
107105, 106syl 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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) }  =/=  (/) )
108 fss 5591 . . . . . . 7  |-  ( ( G : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  ( 0 [,]  +oo ) )  ->  G : RR --> ( 0 [,] 
+oo ) )
10952, 108mpan2 653 . . . . . 6  |-  ( G : RR --> ( 0 [,)  +oo )  ->  G : RR --> ( 0 [,] 
+oo ) )
110 eqid 2435 . . . . . . 7  |-  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) }
111110itg2addnclem 26219 . . . . . 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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  ) )
11276, 109, 1113syl 19 . . . . 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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  ) )
113 itg2addnc.g3 . . . . 5  |-  ( ph  ->  ( S.2 `  G
)  e.  RR )
114112, 113eqeltrrd 2510 . . . 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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  )  e.  RR )
11574, 60sstri 3349 . . . . . 6  |-  { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) }  C_  RR*
116 supxrub 10893 . . . . . 6  |-  ( ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  ) )
117115, 116mpan 652 . . . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  ) )
118117rgen 2763 . . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  )
119 breq2 4208 . . . . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  ) ) )
120119ralbidv 2717 . . . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR* ,  <  ) ) )
121120rspcev 3044 . . . 4  |-  ( ( sup ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } b  <_  a )
122114, 118, 121sylancl 644 . . 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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } b  <_  a )
123 eqid 2435 . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } s  =  ( t  +  u ) }
1247, 51, 68, 75, 107, 122, 123supadd 26202 . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } s  =  ( t  +  u ) } ,  RR ,  <  ) )
125 supxrre 10896 . . . . 5  |-  ( ( { x  |  E. f  e.  dom  S.1 ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR ,  <  ) )
1267, 51, 68, 125syl3anc 1184 . . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR ,  <  ) )
12757, 126eqtrd 2467 . . 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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR ,  <  ) )
128 supxrre 10896 . . . . 5  |-  ( ( { x  |  E. g  e.  dom  S.1 ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR ,  <  ) )
12975, 107, 122, 128syl3anc 1184 . . . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR ,  <  ) )
130112, 129eqtrd 2467 . . 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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR ,  <  ) )
131127, 130oveq12d 6091 . 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 ) ) )  o R  <_  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 ) ) )  o R  <_  G  /\  x  =  ( S.1 `  g
) ) } ,  RR ,  <  ) ) )
132 rexr 9120 . . . . . . . . . 10  |-  ( x  e.  RR  ->  x  e.  RR* )
133132anim1i 552 . . . . . . . . 9  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( x  e.  RR*  /\  0  <_  x )
)
134 elrege0 10997 . . . . . . . . 9  |-  ( x  e.  ( 0 [,) 
+oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
135 elxrge0 10998 . . . . . . . . 9  |-  ( x  e.  ( 0 [,] 
+oo )  <->  ( x  e.  RR*  /\  0  <_  x ) )
136133, 134, 1353imtr4i 258 . . . . . . . 8  |-  ( x  e.  ( 0 [,) 
+oo )  ->  x  e.  ( 0 [,]  +oo ) )
137136ssriv 3344 . . . . . . 7  |-  ( 0 [,)  +oo )  C_  (
0 [,]  +oo )
138 ge0addcl 10999 . . . . . . 7  |-  ( ( x  e.  ( 0 [,)  +oo )  /\  y  e.  ( 0 [,)  +oo ) )  ->  (
x  +  y )  e.  ( 0 [,) 
+oo ) )
139137, 138sseldi 3338 . . . . . 6  |-  ( ( x  e.  ( 0 [,)  +oo )  /\  y  e.  ( 0 [,)  +oo ) )  ->  (
x  +  y )  e.  ( 0 [,] 
+oo ) )
140139adantl 453 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( 0 [,)  +oo )  /\  y  e.  ( 0 [,)  +oo )
) )  ->  (
x  +  y )  e.  ( 0 [,] 
+oo ) )
141 inidm 3542 . . . . 5  |-  ( RR 
i^i  RR )  =  RR
142140, 13, 76, 20, 20, 141off 6312 . . . 4  |-  ( ph  ->  ( F  o F  +  G ) : RR --> ( 0 [,] 
+oo ) )
143 eqid 2435 . . . . 5  |-  { s  |  E. h  e. 
dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `
 z )  +  y ) ) )  o R  <_  ( F  o F  +  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 ) ) )  o R  <_  ( F  o F  +  G
)  /\  s  =  ( S.1 `  h ) ) }
144143itg2addnclem 26219 . . . 4  |-  ( ( F  o F  +  G ) : RR --> ( 0 [,]  +oo )  ->  ( S.2 `  ( F  o F  +  G
) )  =  sup ( { s  |  E. h  e.  dom  S.1 ( E. y  e.  RR+  (
z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `  z
)  +  y ) ) )  o R  <_  ( F  o F  +  G )  /\  s  =  ( S.1 `  h ) ) } ,  RR* ,  <  ) )
145142, 144syl 16 . . 3  |-  ( ph  ->  ( S.2 `  ( F  o F  +  G
) )  =  sup ( { s  |  E. h  e.  dom  S.1 ( E. y  e.  RR+  (
z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `  z
)  +  y ) ) )  o R  <_  ( F  o F  +  G )  /\  s  =  ( S.1 `  h ) ) } ,  RR* ,  <  ) )
146 itg2addnc.f1 . . . . . . . 8  |-  ( ph  ->  F  e. MblFn )
147146, 13, 58, 76, 113itg2addnclem3 26221 . . . . . . 7  |-  ( ph  ->  ( E. h  e. 
dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `
 z )  +  y ) ) )  o R  <_  ( F  o F  +  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 ) ) )  o R  <_  F  /\  t  =  ( S.1 `  f
) )  /\  ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  u  =  ( S.1 `  g
) ) )  /\  s  =  ( t  +  u ) ) ) )
148 simpl 444 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  f  e.  dom  S.1 )
149 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  g  e.  dom  S.1 )
150148, 149i1fadd 19577 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( f  o F  +  g )  e.  dom  S.1 )
151150ad3antlr 712 . . . . . . . . . . . 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 ) ) )  o R  <_  F  /\  t  =  ( S.1 `  f
) )  /\  ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  u  =  ( S.1 `  g
) ) ) )  /\  s  =  ( t  +  u ) )  ->  ( f  o F  +  g
)  e.  dom  S.1 )
152 reeanv 2867 . . . . . . . . . . . . . . . . 17  |-  ( E. c  e.  RR+  E. d  e.  RR+  ( ( z  e.  RR  |->  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  c ) ) )  o R  <_  F  /\  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  o R  <_  G
)  <->  ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  o R  <_  F  /\  E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G ) )
153152biimpri 198 . . . . . . . . . . . . . . . 16  |-  ( ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  F  /\  E. d  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  d ) ) )  o R  <_  G )  ->  E. c  e.  RR+  E. d  e.  RR+  ( ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) ) )  o R  <_  F  /\  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G ) )
154153ad2ant2r 728 . . . . . . . . . . . . . . 15  |-  ( ( ( E. c  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  F  /\  t  =  ( S.1 `  f
) )  /\  ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  u  =  ( S.1 `  g
) ) )  ->  E. c  e.  RR+  E. d  e.  RR+  ( ( z  e.  RR  |->  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  c ) ) )  o R  <_  F  /\  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) ) )  o R  <_  G
) )
155 ifcl 3767 . . . . . . . . . . . . . . . . . . 19  |-  ( ( c  e.  RR+  /\  d  e.  RR+ )  ->  if ( c  <_  d ,  c ,  d )  e.  RR+ )
156155ad2antlr 708 . . . . . . . . . . . . . . . . . 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 ) ) )  o R  <_  F  /\  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G ) )  ->  if ( c  <_  d ,  c ,  d )  e.  RR+ )
157 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0  =  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  c ) )  -> 
( 0  <_  ( F `  z )  <->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) )  <_  ( F `  z ) ) )
158157anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
159158imbi1d 309 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
160 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
161160anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
162161imbi1d 309 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
163 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( 0  <_  ( G `  z )  <->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) )  <_  ( G `  z ) ) )
164163anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
165164imbi1d 309 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
166 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
167166anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
168167imbi1d 309 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
169 oveq12 6082 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( f `  z
)  =  0  /\  ( g `  z
)  =  0 )  ->  ( ( f `
 z )  +  ( g `  z
) )  =  ( 0  +  0 ) )
170 00id 9231 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0  +  0 )  =  0
171169, 170syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f `  z
)  =  0  /\  ( g `  z
)  =  0 )  ->  ( ( f `
 z )  +  ( g `  z
) )  =  0 )
172 iftrue 3737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f `  z
)  +  ( g `
 z ) )  =  0  ->  if ( ( ( f `
 z )  +  ( g `  z
) )  =  0 ,  0 ,  ( ( ( f `  z )  +  ( g `  z ) )  +  if ( c  <_  d , 
c ,  d ) ) )  =  0 )
173171, 172syl 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 )
174173adantll 695 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
175 simpll 731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  ->  ph )
17615simplbi 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F `  z )  e.  ( 0 [,) 
+oo )  ->  ( F `  z )  e.  RR )
17714, 176syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR )  ->  ( F `
 z )  e.  RR )
17878simplbi 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( G `  z )  e.  ( 0 [,) 
+oo )  ->  ( G `  z )  e.  RR )
17977, 178syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR )  ->  ( G `
 z )  e.  RR )
180177, 179, 17, 80addge0d 9592 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  z  e.  RR )  ->  0  <_ 
( ( F `  z )  +  ( G `  z ) ) )
181175, 180sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
182181ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
183174, 182eqbrtrd 4224 . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
184183a1d 23 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
185181ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
186 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( f `  z )  =  0  ->  (
( f `  z
)  +  ( g `
 z ) )  =  ( 0  +  ( g `  z
) ) )
187 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  -> 
g  e.  dom  S.1 )
188 i1ff 19558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
189188ffvelrnda 5862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( g  e.  dom  S.1  /\  z  e.  RR )  ->  ( g `  z )  e.  RR )
190187, 189sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
191190recnd 9104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
192191addid2d 9257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
193186, 192sylan9eqr 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
194193oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
195194adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
196155rpred 10638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( c  e.  RR+  /\  d  e.  RR+ )  ->  if ( c  <_  d ,  c ,  d )  e.  RR )
197196ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
198190, 197readdcld 9105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
199198adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
200175, 179sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
201200adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
202175, 177sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
203202, 200readdcld 9105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
204203adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
205 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  d  e.  RR+ )
206205rpred 10638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
c  e.  RR+  /\  d  e.  RR+ ) )  /\  z  e.  RR )  ->  d  e.  RR )
207 rpre 10608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  e.  RR+  ->  c  e.  RR )
208 rpre 10608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( d  e.  RR+  ->  d  e.  RR )
209 min2 10767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( c  e.  RR  /\  d  e.  RR )  ->  if ( c  <_ 
d ,  c ,  d )  <_  d
)
210207, 208, 209syl2an 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  RR+  /\  d  e.  RR+ )  ->  if ( c  <_  d ,  c ,  d )  <_  d )
211210ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
212197, 206, 190, 211leadd2dd 9631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
213190, 206readdcld 9105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
214 letr 9157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
215198, 213, 200, 214syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
216212, 215mpand 657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
217216imp 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
218179, 177addge02d 9605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  RR )  ->  ( 0  <_  ( F `  z )  <->  ( G `  z )  <_  (
( F `  z
)  +  ( G `
 z ) ) ) )
21917, 218mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  RR )  ->  ( G `
 z )  <_ 
( ( F `  z )  +  ( G `  z ) ) )
220175, 219sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
221220adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
222199, 201, 204, 217, 221letrd 9217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
223222adantlr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
224195, 223eqbrtrd 4224 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
225 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
226 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
227225, 226ifboth 3762 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
228185, 224, 227syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
229228ex 424 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
230229adantld 454 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
231230adantr 452 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
232165, 168, 184, 231ifbothda 3761 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
233163anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
234233imbi1d 309 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  =  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  d ) )  -> 
( ( ( ( ( f