Metamath Proof Explorer

Theorem itg2addnclem3

Description: Lemma incomprehensible in isolation split off to shorten proof of itg2addnc . (Contributed by Brendan Leahy, 11-Mar-2018)

Ref Expression
Hypotheses itg2addnc.f1 
|- ( ph -> F e. MblFn )
itg2addnc.f2 
|- ( ph -> F : RR --> ( 0 [,) +oo ) )
itg2addnc.f3 
|- ( ph -> ( S.2 ` F ) e. RR )
itg2addnc.g2 
|- ( ph -> G : RR --> ( 0 [,) +oo ) )
itg2addnc.g3 
|- ( ph -> ( S.2 ` G ) e. RR )
Assertion itg2addnclem3 
|- ( ph -> ( E. h e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) /\ s = ( S.1 ` h ) ) -> E. t E. u ( E. f e. dom S.1 E. g e. dom S.1 ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) ) )

Proof

Step Hyp Ref Expression
1 itg2addnc.f1 
 |-  ( ph -> F e. MblFn )
2 itg2addnc.f2 
 |-  ( ph -> F : RR --> ( 0 [,) +oo ) )
3 itg2addnc.f3 
 |-  ( ph -> ( S.2 ` F ) e. RR )
4 itg2addnc.g2 
 |-  ( ph -> G : RR --> ( 0 [,) +oo ) )
5 itg2addnc.g3 
 |-  ( ph -> ( S.2 ` G ) e. RR )
6 1 2 itg2addnclem2 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) e. dom S.1 )
7 6 adantrr 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ ( y e. RR+ /\ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) ) ) -> ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) e. dom S.1 )
8 simplr 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> h e. dom S.1 )
9 i1fsub 
 |-  ( ( h e. dom S.1 /\ ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) e. dom S.1 ) -> ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) e. dom S.1 )
10 8 6 9 syl2anc 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) e. dom S.1 )
11 10 adantrr 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ ( y e. RR+ /\ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) ) ) -> ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) e. dom S.1 )
12 3rp 
 |-  3 e. RR+
13 rpdivcl 
 |-  ( ( y e. RR+ /\ 3 e. RR+ ) -> ( y / 3 ) e. RR+ )
14 12 13 mpan2 
 |-  ( y e. RR+ -> ( y / 3 ) e. RR+ )
15 14 adantl 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( y / 3 ) e. RR+ )
16 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
17 16 fvoveq1d 
 |-  ( x = z -> ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) = ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) )
18 17 oveq1d 
 |-  ( x = z -> ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) = ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) )
19 18 oveq1d 
 |-  ( x = z -> ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) = ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) )
20 fveq2 
 |-  ( x = z -> ( h ` x ) = ( h ` z ) )
21 19 20 breq12d 
 |-  ( x = z -> ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) <-> ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) ) )
22 20 neeq1d 
 |-  ( x = z -> ( ( h ` x ) =/= 0 <-> ( h ` z ) =/= 0 ) )
23 21 22 anbi12d 
 |-  ( x = z -> ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) <-> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) ) )
24 23 19 20 ifbieq12d 
 |-  ( x = z -> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) )
25 eqid 
 |-  ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) )
26 ovex 
 |-  ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) e. _V
27 fvex 
 |-  ( h ` z ) e. _V
28 26 27 ifex 
 |-  if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) e. _V
29 24 25 28 fvmpt 
 |-  ( z e. RR -> ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) )
30 29 eqeq1d 
 |-  ( z e. RR -> ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 <-> if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = 0 ) )
31 29 oveq1d 
 |-  ( z e. RR -> ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) = ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) )
32 30 31 ifbieq2d 
 |-  ( z e. RR -> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) = if ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = 0 , 0 , ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) ) )
33 32 adantl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) = if ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = 0 , 0 , ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) ) )
34 breq1 
 |-  ( 0 = if ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = 0 , 0 , ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) ) -> ( 0 <_ ( F ` z ) <-> if ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = 0 , 0 , ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) ) <_ ( F ` z ) ) )
35 breq1 
 |-  ( ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) = if ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = 0 , 0 , ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) ) -> ( ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) <_ ( F ` z ) <-> if ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = 0 , 0 , ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) ) <_ ( F ` z ) ) )
36 2 ad2antrr 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> F : RR --> ( 0 [,) +oo ) )
37 36 ffvelrnda 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( F ` z ) e. ( 0 [,) +oo ) )
38 elrege0 
 |-  ( ( F ` z ) e. ( 0 [,) +oo ) <-> ( ( F ` z ) e. RR /\ 0 <_ ( F ` z ) ) )
39 37 38 sylib 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( F ` z ) e. RR /\ 0 <_ ( F ` z ) ) )
40 39 simprd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> 0 <_ ( F ` z ) )
41 40 adantr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = 0 ) -> 0 <_ ( F ` z ) )
42 df-ne 
 |-  ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) =/= 0 <-> -. if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = 0 )
43 neeq1 
 |-  ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) =/= 0 <-> if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) =/= 0 ) )
44 oveq1 
 |-  ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) = ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) )
45 44 breq1d 
 |-  ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) -> ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) <_ ( F ` z ) <-> ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) <_ ( F ` z ) ) )
46 43 45 imbi12d 
 |-  ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) -> ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) =/= 0 -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) <_ ( F ` z ) ) <-> ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) =/= 0 -> ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) <_ ( F ` z ) ) ) )
47 neeq1 
 |-  ( ( h ` z ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) -> ( ( h ` z ) =/= 0 <-> if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) =/= 0 ) )
48 oveq1 
 |-  ( ( h ` z ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) -> ( ( h ` z ) + ( y / 3 ) ) = ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) )
49 48 breq1d 
 |-  ( ( h ` z ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) -> ( ( ( h ` z ) + ( y / 3 ) ) <_ ( F ` z ) <-> ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) <_ ( F ` z ) ) )
50 47 49 imbi12d 
 |-  ( ( h ` z ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) -> ( ( ( h ` z ) =/= 0 -> ( ( h ` z ) + ( y / 3 ) ) <_ ( F ` z ) ) <-> ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) =/= 0 -> ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) <_ ( F ` z ) ) ) )
51 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
52 51 37 sselid 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( F ` z ) e. RR )
53 14 ad2antlr 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( y / 3 ) e. RR+ )
54 52 53 rerpdivcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( F ` z ) / ( y / 3 ) ) e. RR )
55 reflcl 
 |-  ( ( ( F ` z ) / ( y / 3 ) ) e. RR -> ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) e. RR )
56 peano2rem 
 |-  ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) e. RR -> ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) e. RR )
57 54 55 56 3syl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) e. RR )
58 14 rpred 
 |-  ( y e. RR+ -> ( y / 3 ) e. RR )
59 58 ad2antlr 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( y / 3 ) e. RR )
60 57 59 remulcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) e. RR )
61 peano2rem 
 |-  ( ( ( F ` z ) / ( y / 3 ) ) e. RR -> ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) e. RR )
62 54 61 syl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) e. RR )
63 62 59 remulcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) x. ( y / 3 ) ) e. RR )
64 54 55 syl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) e. RR )
65 1red 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> 1 e. RR )
66 flle 
 |-  ( ( ( F ` z ) / ( y / 3 ) ) e. RR -> ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) <_ ( ( F ` z ) / ( y / 3 ) ) )
67 54 66 syl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) <_ ( ( F ` z ) / ( y / 3 ) ) )
68 64 54 65 67 lesub1dd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) <_ ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) )
69 57 62 53 lemul1d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) <_ ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) <-> ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) x. ( y / 3 ) ) ) )
70 68 69 mpbid 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) x. ( y / 3 ) ) )
71 60 63 59 70 leadd1dd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) <_ ( ( ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) )
72 54 recnd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( F ` z ) / ( y / 3 ) ) e. CC )
73 ax-1cn 
 |-  1 e. CC
74 subcl 
 |-  ( ( ( ( F ` z ) / ( y / 3 ) ) e. CC /\ 1 e. CC ) -> ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) e. CC )
75 72 73 74 sylancl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) e. CC )
76 73 a1i 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> 1 e. CC )
77 53 rpcnd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( y / 3 ) e. CC )
78 75 76 77 adddird 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) + 1 ) x. ( y / 3 ) ) = ( ( ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) x. ( y / 3 ) ) + ( 1 x. ( y / 3 ) ) ) )
79 npcan 
 |-  ( ( ( ( F ` z ) / ( y / 3 ) ) e. CC /\ 1 e. CC ) -> ( ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) + 1 ) = ( ( F ` z ) / ( y / 3 ) ) )
80 72 73 79 sylancl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) + 1 ) = ( ( F ` z ) / ( y / 3 ) ) )
81 80 oveq1d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) + 1 ) x. ( y / 3 ) ) = ( ( ( F ` z ) / ( y / 3 ) ) x. ( y / 3 ) ) )
82 77 mulid2d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( 1 x. ( y / 3 ) ) = ( y / 3 ) )
83 82 oveq2d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) x. ( y / 3 ) ) + ( 1 x. ( y / 3 ) ) ) = ( ( ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) )
84 78 81 83 3eqtr3rd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) = ( ( ( F ` z ) / ( y / 3 ) ) x. ( y / 3 ) ) )
85 52 recnd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( F ` z ) e. CC )
86 53 rpne0d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( y / 3 ) =/= 0 )
87 85 77 86 divcan1d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( F ` z ) / ( y / 3 ) ) x. ( y / 3 ) ) = ( F ` z ) )
88 84 87 eqtrd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( ( F ` z ) / ( y / 3 ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) = ( F ` z ) )
89 71 88 breqtrd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) <_ ( F ` z ) )
90 89 adantr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) <_ ( F ` z ) )
91 90 a1d 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) =/= 0 -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) <_ ( F ` z ) ) )
92 ianor 
 |-  ( -. ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) <-> ( -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) \/ -. ( h ` z ) =/= 0 ) )
93 92 anbi1i 
 |-  ( ( -. ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) /\ ( h ` z ) =/= 0 ) <-> ( ( -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) \/ -. ( h ` z ) =/= 0 ) /\ ( h ` z ) =/= 0 ) )
94 oranabs 
 |-  ( ( ( -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) \/ -. ( h ` z ) =/= 0 ) /\ ( h ` z ) =/= 0 ) <-> ( -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) )
95 93 94 bitri 
 |-  ( ( -. ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) /\ ( h ` z ) =/= 0 ) <-> ( -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) )
96 i1ff 
 |-  ( h e. dom S.1 -> h : RR --> RR )
97 96 ad2antlr 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> h : RR --> RR )
98 97 ffvelrnda 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( h ` z ) e. RR )
99 98 59 readdcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( h ` z ) + ( y / 3 ) ) e. RR )
100 99 adantr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) ) -> ( ( h ` z ) + ( y / 3 ) ) e. RR )
101 52 adantr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) ) -> ( F ` z ) e. RR )
102 60 59 readdcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) e. RR )
103 102 adantr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) e. RR )
104 98 adantr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) ) -> ( h ` z ) e. RR )
105 60 adantr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) ) -> ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) e. RR )
106 58 ad3antlr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) ) -> ( y / 3 ) e. RR )
107 98 60 ltnled 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( h ` z ) < ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <-> -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) ) )
108 107 biimpar 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) ) -> ( h ` z ) < ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) )
109 104 105 106 108 ltadd1dd 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) ) -> ( ( h ` z ) + ( y / 3 ) ) < ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) )
110 89 adantr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) + ( y / 3 ) ) <_ ( F ` z ) )
111 100 103 101 109 110 ltletrd 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) ) -> ( ( h ` z ) + ( y / 3 ) ) < ( F ` z ) )
112 100 101 111 ltled 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) ) -> ( ( h ` z ) + ( y / 3 ) ) <_ ( F ` z ) )
113 112 adantrr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ ( -. ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) ) -> ( ( h ` z ) + ( y / 3 ) ) <_ ( F ` z ) )
114 95 113 sylan2b 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ ( -. ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) /\ ( h ` z ) =/= 0 ) ) -> ( ( h ` z ) + ( y / 3 ) ) <_ ( F ` z ) )
115 114 expr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) ) -> ( ( h ` z ) =/= 0 -> ( ( h ` z ) + ( y / 3 ) ) <_ ( F ` z ) ) )
116 46 50 91 115 ifbothda 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) =/= 0 -> ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) <_ ( F ` z ) ) )
117 42 116 syl5bir 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( -. if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = 0 -> ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) <_ ( F ` z ) ) )
118 117 imp 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = 0 ) -> ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) <_ ( F ` z ) )
119 34 35 41 118 ifbothda 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> if ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = 0 , 0 , ( if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) + ( y / 3 ) ) ) <_ ( F ` z ) )
120 33 119 eqbrtrd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) <_ ( F ` z ) )
121 120 ralrimiva 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> A. z e. RR if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) <_ ( F ` z ) )
122 reex 
 |-  RR e. _V
123 122 a1i 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> RR e. _V )
124 c0ex 
 |-  0 e. _V
125 ovex 
 |-  ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) e. _V
126 124 125 ifex 
 |-  if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) e. _V
127 126 a1i 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) e. _V )
128 eqidd 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) ) = ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) ) )
129 2 feqmptd 
 |-  ( ph -> F = ( z e. RR |-> ( F ` z ) ) )
130 129 ad2antrr 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> F = ( z e. RR |-> ( F ` z ) ) )
131 123 127 37 128 130 ofrfval2 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) ) oR <_ F <-> A. z e. RR if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) <_ ( F ` z ) ) )
132 121 131 mpbird 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) ) oR <_ F )
133 oveq2 
 |-  ( c = ( y / 3 ) -> ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) = ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) )
134 133 ifeq2d 
 |-  ( c = ( y / 3 ) -> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) = if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) )
135 134 mpteq2dv 
 |-  ( c = ( y / 3 ) -> ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) = ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) ) )
136 135 breq1d 
 |-  ( c = ( y / 3 ) -> ( ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F <-> ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) ) oR <_ F ) )
137 136 rspcev 
 |-  ( ( ( y / 3 ) e. RR+ /\ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + ( y / 3 ) ) ) ) oR <_ F ) -> E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F )
138 15 132 137 syl2anc 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F )
139 138 adantrr 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ ( y e. RR+ /\ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) ) ) -> E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F )
140 14 ad2antrl 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ ( y e. RR+ /\ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) ) ) -> ( y / 3 ) e. RR+ )
141 96 ffnd 
 |-  ( h e. dom S.1 -> h Fn RR )
142 141 ad2antlr 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> h Fn RR )
143 ovex 
 |-  ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) e. _V
144 fvex 
 |-  ( h ` x ) e. _V
145 143 144 ifex 
 |-  if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) e. _V
146 145 25 fnmpti 
 |-  ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) Fn RR
147 146 a1i 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) Fn RR )
148 inidm 
 |-  ( RR i^i RR ) = RR
149 eqidd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( h ` z ) = ( h ` z ) )
150 29 adantl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) )
151 142 147 123 123 148 149 150 ofval 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) )
152 151 eqeq1d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 <-> ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 ) )
153 151 oveq1d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) = ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) )
154 152 153 ifbieq2d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) = if ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 , 0 , ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) ) )
155 154 adantr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) -> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) = if ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 , 0 , ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) ) )
156 breq1 
 |-  ( 0 = if ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 , 0 , ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) ) -> ( 0 <_ ( G ` z ) <-> if ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 , 0 , ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) ) <_ ( G ` z ) ) )
157 breq1 
 |-  ( ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) = if ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 , 0 , ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) ) -> ( ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) <_ ( G ` z ) <-> if ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 , 0 , ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) ) <_ ( G ` z ) ) )
158 4 ad2antrr 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> G : RR --> ( 0 [,) +oo ) )
159 158 ffvelrnda 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( G ` z ) e. ( 0 [,) +oo ) )
160 elrege0 
 |-  ( ( G ` z ) e. ( 0 [,) +oo ) <-> ( ( G ` z ) e. RR /\ 0 <_ ( G ` z ) ) )
161 159 160 sylib 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( G ` z ) e. RR /\ 0 <_ ( G ` z ) ) )
162 161 simprd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> 0 <_ ( G ` z ) )
163 162 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) /\ ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 ) -> 0 <_ ( G ` z ) )
164 oveq2 
 |-  ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) -> ( ( h ` z ) - ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) ) = ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) )
165 164 oveq1d 
 |-  ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) -> ( ( ( h ` z ) - ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) ) + ( y / 3 ) ) = ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) )
166 165 breq1d 
 |-  ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) -> ( ( ( ( h ` z ) - ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) ) + ( y / 3 ) ) <_ ( G ` z ) <-> ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) <_ ( G ` z ) ) )
167 oveq2 
 |-  ( ( h ` z ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) -> ( ( h ` z ) - ( h ` z ) ) = ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) )
168 167 oveq1d 
 |-  ( ( h ` z ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) -> ( ( ( h ` z ) - ( h ` z ) ) + ( y / 3 ) ) = ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) )
169 168 breq1d 
 |-  ( ( h ` z ) = if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) -> ( ( ( ( h ` z ) - ( h ` z ) ) + ( y / 3 ) ) <_ ( G ` z ) <-> ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) <_ ( G ` z ) ) )
170 id 
 |-  ( ( h ` z ) = 0 -> ( h ` z ) = 0 )
171 simpr 
 |-  ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) -> ( h ` z ) =/= 0 )
172 171 necon2bi 
 |-  ( ( h ` z ) = 0 -> -. ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) )
173 iffalse 
 |-  ( -. ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) -> if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = ( h ` z ) )
174 172 173 syl 
 |-  ( ( h ` z ) = 0 -> if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = ( h ` z ) )
175 174 170 eqtrd 
 |-  ( ( h ` z ) = 0 -> if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) = 0 )
176 170 175 oveq12d 
 |-  ( ( h ` z ) = 0 -> ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = ( 0 - 0 ) )
177 0m0e0 
 |-  ( 0 - 0 ) = 0
178 176 177 eqtrdi 
 |-  ( ( h ` z ) = 0 -> ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 )
179 iffalse 
 |-  ( -. ( h ` z ) = 0 -> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) = ( ( h ` z ) + y ) )
180 179 breq1d 
 |-  ( -. ( h ` z ) = 0 -> ( if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) <-> ( ( h ` z ) + y ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
181 178 180 nsyl5 
 |-  ( -. ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 -> ( if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) <-> ( ( h ` z ) + y ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
182 181 adantl 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 ) -> ( if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) <-> ( ( h ` z ) + y ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
183 98 recnd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( h ` z ) e. CC )
184 60 recnd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) e. CC )
185 183 184 77 subsubd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( h ` z ) - ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) = ( ( ( h ` z ) - ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) ) + ( y / 3 ) ) )
186 185 adantr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ ( ( h ` z ) + y ) <_ ( ( F ` z ) + ( G ` z ) ) ) -> ( ( h ` z ) - ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) = ( ( ( h ` z ) - ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) ) + ( y / 3 ) ) )
187 60 59 resubcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) e. RR )
188 rpre 
 |-  ( y e. RR+ -> y e. RR )
189 188 ad2antlr 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> y e. RR )
190 187 189 readdcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) + y ) e. RR )
191 51 159 sselid 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( G ` z ) e. RR )
192 1re 
 |-  1 e. RR
193 192 192 readdcli 
 |-  ( 1 + 1 ) e. RR
194 resubcl 
 |-  ( ( ( ( F ` z ) / ( y / 3 ) ) e. RR /\ ( 1 + 1 ) e. RR ) -> ( ( ( F ` z ) / ( y / 3 ) ) - ( 1 + 1 ) ) e. RR )
195 54 193 194 sylancl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( F ` z ) / ( y / 3 ) ) - ( 1 + 1 ) ) e. RR )
196 195 59 remulcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( F ` z ) / ( y / 3 ) ) - ( 1 + 1 ) ) x. ( y / 3 ) ) e. RR )
197 peano2re 
 |-  ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) e. RR -> ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) e. RR )
198 64 197 syl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) e. RR )
199 resubcl 
 |-  ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) e. RR /\ ( 1 + 1 ) e. RR ) -> ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) e. RR )
200 198 193 199 sylancl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) e. RR )
201 200 59 remulcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) x. ( y / 3 ) ) e. RR )
202 58 188 resubcld 
 |-  ( y e. RR+ -> ( ( y / 3 ) - y ) e. RR )
203 202 ad2antlr 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( y / 3 ) - y ) e. RR )
204 193 a1i 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( 1 + 1 ) e. RR )
205 fllep1 
 |-  ( ( ( F ` z ) / ( y / 3 ) ) e. RR -> ( ( F ` z ) / ( y / 3 ) ) <_ ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) )
206 54 205 syl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( F ` z ) / ( y / 3 ) ) <_ ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) )
207 54 198 204 206 lesub1dd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( F ` z ) / ( y / 3 ) ) - ( 1 + 1 ) ) <_ ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) )
208 195 200 53 lemul1d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( F ` z ) / ( y / 3 ) ) - ( 1 + 1 ) ) <_ ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) <-> ( ( ( ( F ` z ) / ( y / 3 ) ) - ( 1 + 1 ) ) x. ( y / 3 ) ) <_ ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) x. ( y / 3 ) ) ) )
209 207 208 mpbid 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( F ` z ) / ( y / 3 ) ) - ( 1 + 1 ) ) x. ( y / 3 ) ) <_ ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) x. ( y / 3 ) ) )
210 196 201 203 209 lesub1dd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( ( F ` z ) / ( y / 3 ) ) - ( 1 + 1 ) ) x. ( y / 3 ) ) - ( ( y / 3 ) - y ) ) <_ ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) x. ( y / 3 ) ) - ( ( y / 3 ) - y ) ) )
211 73 73 addcli 
 |-  ( 1 + 1 ) e. CC
212 211 negcli 
 |-  -u ( 1 + 1 ) e. CC
213 212 a1i 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> -u ( 1 + 1 ) e. CC )
214 72 213 77 adddird 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( F ` z ) / ( y / 3 ) ) + -u ( 1 + 1 ) ) x. ( y / 3 ) ) = ( ( ( ( F ` z ) / ( y / 3 ) ) x. ( y / 3 ) ) + ( -u ( 1 + 1 ) x. ( y / 3 ) ) ) )
215 negsub 
 |-  ( ( ( ( F ` z ) / ( y / 3 ) ) e. CC /\ ( 1 + 1 ) e. CC ) -> ( ( ( F ` z ) / ( y / 3 ) ) + -u ( 1 + 1 ) ) = ( ( ( F ` z ) / ( y / 3 ) ) - ( 1 + 1 ) ) )
216 72 211 215 sylancl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( F ` z ) / ( y / 3 ) ) + -u ( 1 + 1 ) ) = ( ( ( F ` z ) / ( y / 3 ) ) - ( 1 + 1 ) ) )
217 216 oveq1d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( F ` z ) / ( y / 3 ) ) + -u ( 1 + 1 ) ) x. ( y / 3 ) ) = ( ( ( ( F ` z ) / ( y / 3 ) ) - ( 1 + 1 ) ) x. ( y / 3 ) ) )
218 df-2 
 |-  2 = ( 1 + 1 )
219 218 negeqi 
 |-  -u 2 = -u ( 1 + 1 )
220 219 oveq1i 
 |-  ( -u 2 x. ( y / 3 ) ) = ( -u ( 1 + 1 ) x. ( y / 3 ) )
221 2cn 
 |-  2 e. CC
222 14 rpcnd 
 |-  ( y e. RR+ -> ( y / 3 ) e. CC )
223 mulneg1 
 |-  ( ( 2 e. CC /\ ( y / 3 ) e. CC ) -> ( -u 2 x. ( y / 3 ) ) = -u ( 2 x. ( y / 3 ) ) )
224 221 222 223 sylancr 
 |-  ( y e. RR+ -> ( -u 2 x. ( y / 3 ) ) = -u ( 2 x. ( y / 3 ) ) )
225 220 224 eqtr3id 
 |-  ( y e. RR+ -> ( -u ( 1 + 1 ) x. ( y / 3 ) ) = -u ( 2 x. ( y / 3 ) ) )
226 225 ad2antlr 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( -u ( 1 + 1 ) x. ( y / 3 ) ) = -u ( 2 x. ( y / 3 ) ) )
227 87 226 oveq12d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( F ` z ) / ( y / 3 ) ) x. ( y / 3 ) ) + ( -u ( 1 + 1 ) x. ( y / 3 ) ) ) = ( ( F ` z ) + -u ( 2 x. ( y / 3 ) ) ) )
228 214 217 227 3eqtr3d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( F ` z ) / ( y / 3 ) ) - ( 1 + 1 ) ) x. ( y / 3 ) ) = ( ( F ` z ) + -u ( 2 x. ( y / 3 ) ) ) )
229 rpcn 
 |-  ( y e. RR+ -> y e. CC )
230 229 222 negsubdi2d 
 |-  ( y e. RR+ -> -u ( y - ( y / 3 ) ) = ( ( y / 3 ) - y ) )
231 3cn 
 |-  3 e. CC
232 3ne0 
 |-  3 =/= 0
233 divcan2 
 |-  ( ( y e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( 3 x. ( y / 3 ) ) = y )
234 231 232 233 mp3an23 
 |-  ( y e. CC -> ( 3 x. ( y / 3 ) ) = y )
235 229 234 syl 
 |-  ( y e. RR+ -> ( 3 x. ( y / 3 ) ) = y )
236 222 mulid2d 
 |-  ( y e. RR+ -> ( 1 x. ( y / 3 ) ) = ( y / 3 ) )
237 235 236 oveq12d 
 |-  ( y e. RR+ -> ( ( 3 x. ( y / 3 ) ) - ( 1 x. ( y / 3 ) ) ) = ( y - ( y / 3 ) ) )
238 subdir 
 |-  ( ( 3 e. CC /\ 1 e. CC /\ ( y / 3 ) e. CC ) -> ( ( 3 - 1 ) x. ( y / 3 ) ) = ( ( 3 x. ( y / 3 ) ) - ( 1 x. ( y / 3 ) ) ) )
239 231 73 222 238 mp3an12i 
 |-  ( y e. RR+ -> ( ( 3 - 1 ) x. ( y / 3 ) ) = ( ( 3 x. ( y / 3 ) ) - ( 1 x. ( y / 3 ) ) ) )
240 3m1e2 
 |-  ( 3 - 1 ) = 2
241 240 oveq1i 
 |-  ( ( 3 - 1 ) x. ( y / 3 ) ) = ( 2 x. ( y / 3 ) )
242 239 241 eqtr3di 
 |-  ( y e. RR+ -> ( ( 3 x. ( y / 3 ) ) - ( 1 x. ( y / 3 ) ) ) = ( 2 x. ( y / 3 ) ) )
243 237 242 eqtr3d 
 |-  ( y e. RR+ -> ( y - ( y / 3 ) ) = ( 2 x. ( y / 3 ) ) )
244 243 negeqd 
 |-  ( y e. RR+ -> -u ( y - ( y / 3 ) ) = -u ( 2 x. ( y / 3 ) ) )
245 230 244 eqtr3d 
 |-  ( y e. RR+ -> ( ( y / 3 ) - y ) = -u ( 2 x. ( y / 3 ) ) )
246 245 ad2antlr 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( y / 3 ) - y ) = -u ( 2 x. ( y / 3 ) ) )
247 228 246 oveq12d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( ( F ` z ) / ( y / 3 ) ) - ( 1 + 1 ) ) x. ( y / 3 ) ) - ( ( y / 3 ) - y ) ) = ( ( ( F ` z ) + -u ( 2 x. ( y / 3 ) ) ) - -u ( 2 x. ( y / 3 ) ) ) )
248 rpcn 
 |-  ( ( y / 3 ) e. RR+ -> ( y / 3 ) e. CC )
249 mulcl 
 |-  ( ( 2 e. CC /\ ( y / 3 ) e. CC ) -> ( 2 x. ( y / 3 ) ) e. CC )
250 221 248 249 sylancr 
 |-  ( ( y / 3 ) e. RR+ -> ( 2 x. ( y / 3 ) ) e. CC )
251 14 250 syl 
 |-  ( y e. RR+ -> ( 2 x. ( y / 3 ) ) e. CC )
252 251 negcld 
 |-  ( y e. RR+ -> -u ( 2 x. ( y / 3 ) ) e. CC )
253 252 ad2antlr 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> -u ( 2 x. ( y / 3 ) ) e. CC )
254 85 253 pncand 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( F ` z ) + -u ( 2 x. ( y / 3 ) ) ) - -u ( 2 x. ( y / 3 ) ) ) = ( F ` z ) )
255 247 254 eqtrd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( ( F ` z ) / ( y / 3 ) ) - ( 1 + 1 ) ) x. ( y / 3 ) ) - ( ( y / 3 ) - y ) ) = ( F ` z ) )
256 64 recnd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) e. CC )
257 peano2cn 
 |-  ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) e. CC -> ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) e. CC )
258 subsub4 
 |-  ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - 1 ) - 1 ) = ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) )
259 73 73 258 mp3an23 
 |-  ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) e. CC -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - 1 ) - 1 ) = ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) )
260 256 257 259 3syl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - 1 ) - 1 ) = ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) )
261 pncan 
 |-  ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) e. CC /\ 1 e. CC ) -> ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - 1 ) = ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) )
262 256 73 261 sylancl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - 1 ) = ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) )
263 262 oveq1d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - 1 ) - 1 ) = ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) )
264 260 263 eqtr3d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) = ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) )
265 264 oveq1d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) x. ( y / 3 ) ) = ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) )
266 265 oveq1d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) x. ( y / 3 ) ) - ( ( y / 3 ) - y ) ) = ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( ( y / 3 ) - y ) ) )
267 189 recnd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> y e. CC )
268 184 77 267 subsubd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( ( y / 3 ) - y ) ) = ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) + y ) )
269 266 268 eqtrd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) + 1 ) - ( 1 + 1 ) ) x. ( y / 3 ) ) - ( ( y / 3 ) - y ) ) = ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) + y ) )
270 210 255 269 3brtr3d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( F ` z ) <_ ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) + y ) )
271 52 190 191 270 leadd1dd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( F ` z ) + ( G ` z ) ) <_ ( ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) + y ) + ( G ` z ) ) )
272 191 recnd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( G ` z ) e. CC )
273 187 recnd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) e. CC )
274 229 ad2antlr 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> y e. CC )
275 273 274 addcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) + y ) e. CC )
276 272 273 274 addassd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) + y ) = ( ( G ` z ) + ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) + y ) ) )
277 272 275 276 comraddd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) + y ) = ( ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) + y ) + ( G ` z ) ) )
278 271 277 breqtrrd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( F ` z ) + ( G ` z ) ) <_ ( ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) + y ) )
279 98 189 readdcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( h ` z ) + y ) e. RR )
280 52 191 readdcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( F ` z ) + ( G ` z ) ) e. RR )
281 191 187 readdcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) e. RR )
282 281 189 readdcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) + y ) e. RR )
283 letr 
 |-  ( ( ( ( h ` z ) + y ) e. RR /\ ( ( F ` z ) + ( G ` z ) ) e. RR /\ ( ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) + y ) e. RR ) -> ( ( ( ( h ` z ) + y ) <_ ( ( F ` z ) + ( G ` z ) ) /\ ( ( F ` z ) + ( G ` z ) ) <_ ( ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) + y ) ) -> ( ( h ` z ) + y ) <_ ( ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) + y ) ) )
284 279 280 282 283 syl3anc 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( ( h ` z ) + y ) <_ ( ( F ` z ) + ( G ` z ) ) /\ ( ( F ` z ) + ( G ` z ) ) <_ ( ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) + y ) ) -> ( ( h ` z ) + y ) <_ ( ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) + y ) ) )
285 278 284 mpan2d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( h ` z ) + y ) <_ ( ( F ` z ) + ( G ` z ) ) -> ( ( h ` z ) + y ) <_ ( ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) + y ) ) )
286 285 imp 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ ( ( h ` z ) + y ) <_ ( ( F ` z ) + ( G ` z ) ) ) -> ( ( h ` z ) + y ) <_ ( ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) + y ) )
287 98 187 191 lesubaddd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( h ` z ) - ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) <_ ( G ` z ) <-> ( h ` z ) <_ ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) ) )
288 98 281 189 leadd1d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( h ` z ) <_ ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) <-> ( ( h ` z ) + y ) <_ ( ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) + y ) ) )
289 287 288 bitrd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( h ` z ) - ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) <_ ( G ` z ) <-> ( ( h ` z ) + y ) <_ ( ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) + y ) ) )
290 289 adantr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ ( ( h ` z ) + y ) <_ ( ( F ` z ) + ( G ` z ) ) ) -> ( ( ( h ` z ) - ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) <_ ( G ` z ) <-> ( ( h ` z ) + y ) <_ ( ( ( G ` z ) + ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) + y ) ) )
291 286 290 mpbird 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ ( ( h ` z ) + y ) <_ ( ( F ` z ) + ( G ` z ) ) ) -> ( ( h ` z ) - ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) - ( y / 3 ) ) ) <_ ( G ` z ) )
292 186 291 eqbrtrrd 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ ( ( h ` z ) + y ) <_ ( ( F ` z ) + ( G ` z ) ) ) -> ( ( ( h ` z ) - ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) ) + ( y / 3 ) ) <_ ( G ` z ) )
293 292 ex 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( h ` z ) + y ) <_ ( ( F ` z ) + ( G ` z ) ) -> ( ( ( h ` z ) - ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) ) + ( y / 3 ) ) <_ ( G ` z ) ) )
294 293 adantr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 ) -> ( ( ( h ` z ) + y ) <_ ( ( F ` z ) + ( G ` z ) ) -> ( ( ( h ` z ) - ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) ) + ( y / 3 ) ) <_ ( G ` z ) ) )
295 182 294 sylbid 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 ) -> ( if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) -> ( ( ( h ` z ) - ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) ) + ( y / 3 ) ) <_ ( G ` z ) ) )
296 295 imp 
 |-  ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ -. ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 ) /\ if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) -> ( ( ( h ` z ) - ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) ) + ( y / 3 ) ) <_ ( G ` z ) )
297 296 an32s 
 |-  ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) /\ -. ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 ) -> ( ( ( h ` z ) - ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) ) + ( y / 3 ) ) <_ ( G ` z ) )
298 297 adantr 
 |-  ( ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) /\ -. ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 ) /\ ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) ) -> ( ( ( h ` z ) - ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) ) + ( y / 3 ) ) <_ ( G ` z ) )
299 173 oveq2d 
 |-  ( -. ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) -> ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = ( ( h ` z ) - ( h ` z ) ) )
300 183 subidd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( h ` z ) - ( h ` z ) ) = 0 )
301 300 adantr 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) -> ( ( h ` z ) - ( h ` z ) ) = 0 )
302 299 301 sylan9eqr 
 |-  ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) /\ -. ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) ) -> ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 )
303 302 pm2.24d 
 |-  ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) /\ -. ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) ) -> ( -. ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 -> ( ( ( h ` z ) - ( h ` z ) ) + ( y / 3 ) ) <_ ( G ` z ) ) )
304 303 imp 
 |-  ( ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) /\ -. ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) ) /\ -. ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 ) -> ( ( ( h ` z ) - ( h ` z ) ) + ( y / 3 ) ) <_ ( G ` z ) )
305 304 an32s 
 |-  ( ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) /\ -. ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 ) /\ -. ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) ) -> ( ( ( h ` z ) - ( h ` z ) ) + ( y / 3 ) ) <_ ( G ` z ) )
306 166 169 298 305 ifbothda 
 |-  ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) /\ -. ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 ) -> ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) <_ ( G ` z ) )
307 156 157 163 306 ifbothda 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) -> if ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) = 0 , 0 , ( ( ( h ` z ) - if ( ( ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` z ) /\ ( h ` z ) =/= 0 ) , ( ( ( |_ ` ( ( F ` z ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` z ) ) ) + ( y / 3 ) ) ) <_ ( G ` z ) )
308 155 307 eqbrtrd 
 |-  ( ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) /\ if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) -> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) <_ ( G ` z ) )
309 308 ex 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) -> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) <_ ( G ` z ) ) )
310 309 ralimdva 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( A. z e. RR if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) -> A. z e. RR if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) <_ ( G ` z ) ) )
311 122 a1i 
 |-  ( ph -> RR e. _V )
312 ovex 
 |-  ( ( h ` z ) + y ) e. _V
313 124 312 ifex 
 |-  if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) e. _V
314 313 a1i 
 |-  ( ( ph /\ z e. RR ) -> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) e. _V )
315 2 ffvelrnda 
 |-  ( ( ph /\ z e. RR ) -> ( F ` z ) e. ( 0 [,) +oo ) )
316 51 315 sselid 
 |-  ( ( ph /\ z e. RR ) -> ( F ` z ) e. RR )
317 4 ffvelrnda 
 |-  ( ( ph /\ z e. RR ) -> ( G ` z ) e. ( 0 [,) +oo ) )
318 51 317 sselid 
 |-  ( ( ph /\ z e. RR ) -> ( G ` z ) e. RR )
319 316 318 readdcld 
 |-  ( ( ph /\ z e. RR ) -> ( ( F ` z ) + ( G ` z ) ) e. RR )
320 eqidd 
 |-  ( ph -> ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) = ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) )
321 4 feqmptd 
 |-  ( ph -> G = ( z e. RR |-> ( G ` z ) ) )
322 311 315 317 129 321 offval2 
 |-  ( ph -> ( F oF + G ) = ( z e. RR |-> ( ( F ` z ) + ( G ` z ) ) ) )
323 311 314 319 320 322 ofrfval2 
 |-  ( ph -> ( ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) <-> A. z e. RR if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
324 323 ad2antrr 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) <-> A. z e. RR if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) <_ ( ( F ` z ) + ( G ` z ) ) ) )
325 ovex 
 |-  ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) e. _V
326 124 325 ifex 
 |-  if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) e. _V
327 326 a1i 
 |-  ( ( ph /\ z e. RR ) -> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) e. _V )
328 eqidd 
 |-  ( ph -> ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) ) = ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) ) )
329 311 327 317 328 321 ofrfval2 
 |-  ( ph -> ( ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) ) oR <_ G <-> A. z e. RR if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) <_ ( G ` z ) ) )
330 329 ad2antrr 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) ) oR <_ G <-> A. z e. RR if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) <_ ( G ` z ) ) )
331 310 324 330 3imtr4d 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) -> ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) ) oR <_ G ) )
332 331 impr 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ ( y e. RR+ /\ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) ) ) -> ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) ) oR <_ G )
333 oveq2 
 |-  ( d = ( y / 3 ) -> ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) = ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) )
334 333 ifeq2d 
 |-  ( d = ( y / 3 ) -> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) = if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) )
335 334 mpteq2dv 
 |-  ( d = ( y / 3 ) -> ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) = ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) ) )
336 335 breq1d 
 |-  ( d = ( y / 3 ) -> ( ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G <-> ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) ) oR <_ G ) )
337 336 rspcev 
 |-  ( ( ( y / 3 ) e. RR+ /\ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + ( y / 3 ) ) ) ) oR <_ G ) -> E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G )
338 140 332 337 syl2anc 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ ( y e. RR+ /\ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) ) ) -> E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G )
339 36 ffvelrnda 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
340 51 339 sselid 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ x e. RR ) -> ( F ` x ) e. RR )
341 14 ad2antlr 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ x e. RR ) -> ( y / 3 ) e. RR+ )
342 340 341 rerpdivcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ x e. RR ) -> ( ( F ` x ) / ( y / 3 ) ) e. RR )
343 reflcl 
 |-  ( ( ( F ` x ) / ( y / 3 ) ) e. RR -> ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) e. RR )
344 peano2rem 
 |-  ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) e. RR -> ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) e. RR )
345 342 343 344 3syl 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) e. RR )
346 58 ad2antlr 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ x e. RR ) -> ( y / 3 ) e. RR )
347 345 346 remulcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ x e. RR ) -> ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) e. RR )
348 97 ffvelrnda 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ x e. RR ) -> ( h ` x ) e. RR )
349 347 348 ifcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ x e. RR ) -> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) e. RR )
350 349 recnd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ x e. RR ) -> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) e. CC )
351 348 recnd 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ x e. RR ) -> ( h ` x ) e. CC )
352 350 351 pncan3d 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ x e. RR ) -> ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) + ( ( h ` x ) - if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) = ( h ` x ) )
353 352 mpteq2dva 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( x e. RR |-> ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) + ( ( h ` x ) - if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) = ( x e. RR |-> ( h ` x ) ) )
354 348 349 resubcld 
 |-  ( ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) /\ x e. RR ) -> ( ( h ` x ) - if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) e. RR )
355 eqidd 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) )
356 96 feqmptd 
 |-  ( h e. dom S.1 -> h = ( x e. RR |-> ( h ` x ) ) )
357 356 ad2antlr 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> h = ( x e. RR |-> ( h ` x ) ) )
358 123 348 349 357 355 offval2 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) = ( x e. RR |-> ( ( h ` x ) - if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) )
359 123 349 354 355 358 offval2 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) oF + ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) = ( x e. RR |-> ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) + ( ( h ` x ) - if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) )
360 353 359 357 3eqtr4d 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) oF + ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) = h )
361 360 fveq2d 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( S.1 ` ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) oF + ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) = ( S.1 ` h ) )
362 6 10 itg1add 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( S.1 ` ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) oF + ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) = ( ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) + ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) )
363 361 362 eqtr3d 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ y e. RR+ ) -> ( S.1 ` h ) = ( ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) + ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) )
364 363 adantrr 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ ( y e. RR+ /\ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) ) ) -> ( S.1 ` h ) = ( ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) + ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) )
365 fvex 
 |-  ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) e. _V
366 fvex 
 |-  ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) e. _V
367 iba 
 |-  ( t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) -> ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F <-> ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) )
368 iba 
 |-  ( u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) -> ( E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G <-> ( E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) ) )
369 367 368 bi2anan9 
 |-  ( ( t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) -> ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G ) <-> ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) ) ) )
370 369 bicomd 
 |-  ( ( t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) -> ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) ) <-> ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G ) ) )
371 oveq12 
 |-  ( ( t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) -> ( t + u ) = ( ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) + ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) )
372 371 eqeq2d 
 |-  ( ( t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) -> ( ( S.1 ` h ) = ( t + u ) <-> ( S.1 ` h ) = ( ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) + ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) ) )
373 370 372 anbi12d 
 |-  ( ( t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) -> ( ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) ) /\ ( S.1 ` h ) = ( t + u ) ) <-> ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G ) /\ ( S.1 ` h ) = ( ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) + ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) ) ) )
374 365 366 373 spc2ev 
 |-  ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G ) /\ ( S.1 ` h ) = ( ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) + ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) ) -> E. t E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) ) /\ ( S.1 ` h ) = ( t + u ) ) )
375 139 338 364 374 syl21anc 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ ( y e. RR+ /\ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) ) ) -> E. t E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) ) /\ ( S.1 ` h ) = ( t + u ) ) )
376 fveq1 
 |-  ( f = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) -> ( f ` z ) = ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) )
377 376 eqeq1d 
 |-  ( f = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) -> ( ( f ` z ) = 0 <-> ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 ) )
378 376 oveq1d 
 |-  ( f = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) -> ( ( f ` z ) + c ) = ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) )
379 377 378 ifbieq2d 
 |-  ( f = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) -> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) = if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) )
380 379 mpteq2dv 
 |-  ( f = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) -> ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) = ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) )
381 380 breq1d 
 |-  ( f = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) -> ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F <-> ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F ) )
382 381 rexbidv 
 |-  ( f = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) -> ( 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 ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F ) )
383 fveq2 
 |-  ( f = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) -> ( S.1 ` f ) = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) )
384 383 eqeq2d 
 |-  ( f = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) -> ( t = ( S.1 ` f ) <-> t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) )
385 382 384 anbi12d 
 |-  ( f = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) -> ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) <-> ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) )
386 385 anbi1d 
 |-  ( f = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) -> ( ( ( 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+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) ) )
387 386 anbi1d 
 |-  ( f = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) -> ( ( ( ( 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.1 ` h ) = ( t + u ) ) <-> ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ ( S.1 ` h ) = ( t + u ) ) ) )
388 387 2exbidv 
 |-  ( f = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) -> ( E. t E. u ( ( ( 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.1 ` h ) = ( t + u ) ) <-> E. t E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ ( S.1 ` h ) = ( t + u ) ) ) )
389 fveq1 
 |-  ( g = ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) -> ( g ` z ) = ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) )
390 389 eqeq1d 
 |-  ( g = ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) -> ( ( g ` z ) = 0 <-> ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 ) )
391 389 oveq1d 
 |-  ( g = ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) -> ( ( g ` z ) + d ) = ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) )
392 390 391 ifbieq2d 
 |-  ( g = ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) = if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) )
393 392 mpteq2dv 
 |-  ( g = ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) -> ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) = ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) )
394 393 breq1d 
 |-  ( g = ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) -> ( ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G <-> ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G ) )
395 394 rexbidv 
 |-  ( g = ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) -> ( 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 ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G ) )
396 fveq2 
 |-  ( g = ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) -> ( S.1 ` g ) = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) )
397 396 eqeq2d 
 |-  ( g = ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) -> ( u = ( S.1 ` g ) <-> u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) )
398 395 397 anbi12d 
 |-  ( g = ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) -> ( ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) <-> ( E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) ) )
399 398 anbi2d 
 |-  ( g = ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) -> ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( 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+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) ) ) )
400 399 anbi1d 
 |-  ( g = ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) -> ( ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ ( S.1 ` h ) = ( t + u ) ) <-> ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) ) /\ ( S.1 ` h ) = ( t + u ) ) ) )
401 400 2exbidv 
 |-  ( g = ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) -> ( E. t E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ ( S.1 ` h ) = ( t + u ) ) <-> E. t E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) ) /\ ( S.1 ` h ) = ( t + u ) ) ) )
402 388 401 rspc2ev 
 |-  ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) e. dom S.1 /\ ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) e. dom S.1 /\ E. t E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) = 0 , 0 , ( ( ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) = 0 , 0 , ( ( ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` ( h oF - ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( y / 3 ) ) ) - 1 ) x. ( y / 3 ) ) , ( h ` x ) ) ) ) ) ) ) /\ ( S.1 ` h ) = ( t + u ) ) ) -> E. f e. dom S.1 E. g e. dom S.1 E. t E. u ( ( ( 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.1 ` h ) = ( t + u ) ) )
403 7 11 375 402 syl3anc 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ ( y e. RR+ /\ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) ) ) -> E. f e. dom S.1 E. g e. dom S.1 E. t E. u ( ( ( 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.1 ` h ) = ( t + u ) ) )
404 eqeq1 
 |-  ( s = ( S.1 ` h ) -> ( s = ( t + u ) <-> ( S.1 ` h ) = ( t + u ) ) )
405 404 anbi2d 
 |-  ( s = ( S.1 ` h ) -> ( ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> ( ( ( E. 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.1 ` h ) = ( t + u ) ) ) )
406 405 2exbidv 
 |-  ( s = ( S.1 ` h ) -> ( E. t E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> E. t E. u ( ( ( 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.1 ` h ) = ( t + u ) ) ) )
407 406 2rexbidv 
 |-  ( s = ( S.1 ` h ) -> ( E. f e. dom S.1 E. g e. dom S.1 E. t E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> E. f e. dom S.1 E. g e. dom S.1 E. t E. u ( ( ( 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.1 ` h ) = ( t + u ) ) ) )
408 403 407 syl5ibrcom 
 |-  ( ( ( ph /\ h e. dom S.1 ) /\ ( y e. RR+ /\ ( z e. RR |-> if ( ( h ` z ) = 0 , 0 , ( ( h ` z ) + y ) ) ) oR <_ ( F oF + G ) ) ) -> ( s = ( S.1 ` h ) -> E. f e. dom S.1 E. g e. dom S.1 E. t E. u ( ( ( 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 ) ) ) )
409 408 rexlimdvaa 
 |-  ( ( ph /\ 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. f e. dom S.1 E. g e. dom S.1 E. t E. u ( ( ( 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 ) ) ) ) )
410 409 impd 
 |-  ( ( ph /\ 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. f e. dom S.1 E. g e. dom S.1 E. t E. u ( ( ( 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 ) ) ) )
411 410 rexlimdva 
 |-  ( 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. f e. dom S.1 E. g e. dom S.1 E. t E. u ( ( ( 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 ) ) ) )
412 rexcom4 
 |-  ( E. g e. dom S.1 E. t E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> E. t E. g e. dom S.1 E. u ( ( ( 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 ) ) )
413 412 rexbii 
 |-  ( E. f e. dom S.1 E. g e. dom S.1 E. t E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> E. f e. dom S.1 E. t E. g e. dom S.1 E. u ( ( ( 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 ) ) )
414 rexcom4 
 |-  ( E. f e. dom S.1 E. t E. g e. dom S.1 E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> E. t E. f e. dom S.1 E. g e. dom S.1 E. u ( ( ( 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 ) ) )
415 413 414 bitri 
 |-  ( E. f e. dom S.1 E. g e. dom S.1 E. t E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> E. t E. f e. dom S.1 E. g e. dom S.1 E. u ( ( ( 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 ) ) )
416 rexcom4 
 |-  ( E. g e. dom S.1 E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> E. u 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 ) ) )
417 416 rexbii 
 |-  ( E. f e. dom S.1 E. g e. dom S.1 E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> E. f e. dom S.1 E. u 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 ) ) )
418 rexcom4 
 |-  ( E. f e. dom S.1 E. u E. g e. dom S.1 ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> E. 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 ) ) )
419 417 418 bitri 
 |-  ( E. f e. dom S.1 E. g e. dom S.1 E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> E. 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 ) ) )
420 419 exbii 
 |-  ( E. t E. f e. dom S.1 E. g e. dom S.1 E. u ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> E. 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 ) ) )
421 r19.41vv 
 |-  ( E. f e. dom S.1 E. g e. dom S.1 ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> ( E. f e. dom S.1 E. 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 ) ) )
422 421 2exbii 
 |-  ( E. t E. u E. f e. dom S.1 E. g e. dom S.1 ( ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> E. 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 ) ) )
423 415 420 422 3bitrri 
 |-  ( E. t E. u ( E. f e. dom S.1 E. g e. dom S.1 ( ( E. c e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + c ) ) ) oR <_ F /\ t = ( S.1 ` f ) ) /\ ( E. d e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + d ) ) ) oR <_ G /\ u = ( S.1 ` g ) ) ) /\ s = ( t + u ) ) <-> E. f e. dom S.1 E. g e. dom S.1 E. t E. u ( ( ( 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 ) ) )
424 411 423 syl6ibr 
 |-  ( 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 ) ) ) )