Metamath Proof Explorer

Theorem itg2gt0cn

Description: itg2gt0 holds on functions continuous on an open interval in the absence of ax-cc . The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017)

Ref Expression
Hypotheses itg2gt0cn.2 
|- ( ph -> X < Y )
itg2gt0cn.3 
|- ( ph -> F : RR --> ( 0 [,) +oo ) )
itg2gt0cn.5 
|- ( ( ph /\ x e. ( X (,) Y ) ) -> 0 < ( F ` x ) )
itg2gt0cn.cn 
|- ( ph -> ( F |` ( X (,) Y ) ) e. ( ( X (,) Y ) -cn-> CC ) )
Assertion itg2gt0cn 
|- ( ph -> 0 < ( S.2 ` F ) )

Proof

Step Hyp Ref Expression
1 itg2gt0cn.2 
 |-  ( ph -> X < Y )
2 itg2gt0cn.3 
 |-  ( ph -> F : RR --> ( 0 [,) +oo ) )
3 itg2gt0cn.5 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> 0 < ( F ` x ) )
4 itg2gt0cn.cn 
 |-  ( ph -> ( F |` ( X (,) Y ) ) e. ( ( X (,) Y ) -cn-> CC ) )
5 0xr 
 |-  0 e. RR*
6 imassrn 
 |-  ( F " ( X (,) Y ) ) C_ ran F
7 2 frnd 
 |-  ( ph -> ran F C_ ( 0 [,) +oo ) )
8 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
9 7 8 sstrdi 
 |-  ( ph -> ran F C_ RR* )
10 6 9 sstrid 
 |-  ( ph -> ( F " ( X (,) Y ) ) C_ RR* )
11 supxrcl 
 |-  ( ( F " ( X (,) Y ) ) C_ RR* -> sup ( ( F " ( X (,) Y ) ) , RR* , < ) e. RR* )
12 10 11 syl 
 |-  ( ph -> sup ( ( F " ( X (,) Y ) ) , RR* , < ) e. RR* )
13 ltrelxr 
 |-  < C_ ( RR* X. RR* )
14 13 ssbri 
 |-  ( X < Y -> X ( RR* X. RR* ) Y )
15 1 14 syl 
 |-  ( ph -> X ( RR* X. RR* ) Y )
16 brxp 
 |-  ( X ( RR* X. RR* ) Y <-> ( X e. RR* /\ Y e. RR* ) )
17 15 16 sylib 
 |-  ( ph -> ( X e. RR* /\ Y e. RR* ) )
18 ioon0 
 |-  ( ( X e. RR* /\ Y e. RR* ) -> ( ( X (,) Y ) =/= (/) <-> X < Y ) )
19 17 18 syl 
 |-  ( ph -> ( ( X (,) Y ) =/= (/) <-> X < Y ) )
20 1 19 mpbird 
 |-  ( ph -> ( X (,) Y ) =/= (/) )
21 3 ralrimiva 
 |-  ( ph -> A. x e. ( X (,) Y ) 0 < ( F ` x ) )
22 r19.2z 
 |-  ( ( ( X (,) Y ) =/= (/) /\ A. x e. ( X (,) Y ) 0 < ( F ` x ) ) -> E. x e. ( X (,) Y ) 0 < ( F ` x ) )
23 20 21 22 syl2anc 
 |-  ( ph -> E. x e. ( X (,) Y ) 0 < ( F ` x ) )
24 supxrlub 
 |-  ( ( ( F " ( X (,) Y ) ) C_ RR* /\ 0 e. RR* ) -> ( 0 < sup ( ( F " ( X (,) Y ) ) , RR* , < ) <-> E. y e. ( F " ( X (,) Y ) ) 0 < y ) )
25 10 5 24 sylancl 
 |-  ( ph -> ( 0 < sup ( ( F " ( X (,) Y ) ) , RR* , < ) <-> E. y e. ( F " ( X (,) Y ) ) 0 < y ) )
26 2 ffnd 
 |-  ( ph -> F Fn RR )
27 ioossre 
 |-  ( X (,) Y ) C_ RR
28 breq2 
 |-  ( y = ( F ` x ) -> ( 0 < y <-> 0 < ( F ` x ) ) )
29 28 rexima 
 |-  ( ( F Fn RR /\ ( X (,) Y ) C_ RR ) -> ( E. y e. ( F " ( X (,) Y ) ) 0 < y <-> E. x e. ( X (,) Y ) 0 < ( F ` x ) ) )
30 26 27 29 sylancl 
 |-  ( ph -> ( E. y e. ( F " ( X (,) Y ) ) 0 < y <-> E. x e. ( X (,) Y ) 0 < ( F ` x ) ) )
31 25 30 bitrd 
 |-  ( ph -> ( 0 < sup ( ( F " ( X (,) Y ) ) , RR* , < ) <-> E. x e. ( X (,) Y ) 0 < ( F ` x ) ) )
32 23 31 mpbird 
 |-  ( ph -> 0 < sup ( ( F " ( X (,) Y ) ) , RR* , < ) )
33 qbtwnxr 
 |-  ( ( 0 e. RR* /\ sup ( ( F " ( X (,) Y ) ) , RR* , < ) e. RR* /\ 0 < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> E. y e. QQ ( 0 < y /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) )
34 5 12 32 33 mp3an2i 
 |-  ( ph -> E. y e. QQ ( 0 < y /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) )
35 qre 
 |-  ( y e. QQ -> y e. RR )
36 35 adantr 
 |-  ( ( y e. QQ /\ 0 < y ) -> y e. RR )
37 simpr 
 |-  ( ( y e. QQ /\ 0 < y ) -> 0 < y )
38 36 37 elrpd 
 |-  ( ( y e. QQ /\ 0 < y ) -> y e. RR+ )
39 38 anim1i 
 |-  ( ( ( y e. QQ /\ 0 < y ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> ( y e. RR+ /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) )
40 39 anasss 
 |-  ( ( y e. QQ /\ ( 0 < y /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) ) -> ( y e. RR+ /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) )
41 simplr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> y e. RR+ )
42 rpxr 
 |-  ( y e. RR+ -> y e. RR* )
43 supxrlub 
 |-  ( ( ( F " ( X (,) Y ) ) C_ RR* /\ y e. RR* ) -> ( y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) <-> E. z e. ( F " ( X (,) Y ) ) y < z ) )
44 10 42 43 syl2an 
 |-  ( ( ph /\ y e. RR+ ) -> ( y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) <-> E. z e. ( F " ( X (,) Y ) ) y < z ) )
45 breq2 
 |-  ( z = ( F ` x ) -> ( y < z <-> y < ( F ` x ) ) )
46 45 rexima 
 |-  ( ( F Fn RR /\ ( X (,) Y ) C_ RR ) -> ( E. z e. ( F " ( X (,) Y ) ) y < z <-> E. x e. ( X (,) Y ) y < ( F ` x ) ) )
47 26 27 46 sylancl 
 |-  ( ph -> ( E. z e. ( F " ( X (,) Y ) ) y < z <-> E. x e. ( X (,) Y ) y < ( F ` x ) ) )
48 47 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> ( E. z e. ( F " ( X (,) Y ) ) y < z <-> E. x e. ( X (,) Y ) y < ( F ` x ) ) )
49 44 48 bitrd 
 |-  ( ( ph /\ y e. RR+ ) -> ( y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) <-> E. x e. ( X (,) Y ) y < ( F ` x ) ) )
50 5 a1i 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> 0 e. RR* )
51 ioorp 
 |-  ( 0 (,) +oo ) = RR+
52 ioossicc 
 |-  ( 0 (,) +oo ) C_ ( 0 [,] +oo )
53 51 52 eqsstrri 
 |-  RR+ C_ ( 0 [,] +oo )
54 53 sseli 
 |-  ( y e. RR+ -> y e. ( 0 [,] +oo ) )
55 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
56 ifcl 
 |-  ( ( y e. ( 0 [,] +oo ) /\ 0 e. ( 0 [,] +oo ) ) -> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) e. ( 0 [,] +oo ) )
57 54 55 56 sylancl 
 |-  ( y e. RR+ -> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) e. ( 0 [,] +oo ) )
58 57 adantr 
 |-  ( ( y e. RR+ /\ w e. RR ) -> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) e. ( 0 [,] +oo ) )
59 58 fmpttd 
 |-  ( y e. RR+ -> ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) : RR --> ( 0 [,] +oo ) )
60 itg2cl 
 |-  ( ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) ) e. RR* )
61 59 60 syl 
 |-  ( y e. RR+ -> ( S.2 ` ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) ) e. RR* )
62 61 ad5antlr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( S.2 ` ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) ) e. RR* )
63 ifcl 
 |-  ( ( y e. ( 0 [,] +oo ) /\ 0 e. ( 0 [,] +oo ) ) -> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) e. ( 0 [,] +oo ) )
64 54 55 63 sylancl 
 |-  ( y e. RR+ -> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) e. ( 0 [,] +oo ) )
65 64 adantr 
 |-  ( ( y e. RR+ /\ w e. RR ) -> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) e. ( 0 [,] +oo ) )
66 65 fmpttd 
 |-  ( y e. RR+ -> ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) : RR --> ( 0 [,] +oo ) )
67 itg2cl 
 |-  ( ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) e. RR* )
68 66 67 syl 
 |-  ( y e. RR+ -> ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) e. RR* )
69 68 ad5antlr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) e. RR* )
70 rpre 
 |-  ( y e. RR+ -> y e. RR )
71 70 ad4antlr 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> y e. RR )
72 ioombl 
 |-  ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) e. dom vol
73 mblvol 
 |-  ( ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) e. dom vol -> ( vol ` ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) ) = ( vol* ` ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) ) )
74 72 73 ax-mp 
 |-  ( vol ` ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) ) = ( vol* ` ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) )
75 elioore 
 |-  ( x e. ( X (,) Y ) -> x e. RR )
76 75 ad3antlr 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> x e. RR )
77 rpre 
 |-  ( z e. RR+ -> z e. RR )
78 77 adantl 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> z e. RR )
79 76 78 resubcld 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( x - z ) e. RR )
80 79 adantr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ X <_ ( x - z ) ) -> ( x - z ) e. RR )
81 79 rexrd 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( x - z ) e. RR* )
82 81 adantr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ -. X <_ ( x - z ) ) -> ( x - z ) e. RR* )
83 17 simpld 
 |-  ( ph -> X e. RR* )
84 83 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ -. X <_ ( x - z ) ) -> X e. RR* )
85 17 simprd 
 |-  ( ph -> Y e. RR* )
86 85 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ -. X <_ ( x - z ) ) -> Y e. RR* )
87 83 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> X e. RR* )
88 xrltnle 
 |-  ( ( ( x - z ) e. RR* /\ X e. RR* ) -> ( ( x - z ) < X <-> -. X <_ ( x - z ) ) )
89 81 87 88 syl2anc 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( ( x - z ) < X <-> -. X <_ ( x - z ) ) )
90 89 biimpar 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ -. X <_ ( x - z ) ) -> ( x - z ) < X )
91 1 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ -. X <_ ( x - z ) ) -> X < Y )
92 xrre2 
 |-  ( ( ( ( x - z ) e. RR* /\ X e. RR* /\ Y e. RR* ) /\ ( ( x - z ) < X /\ X < Y ) ) -> X e. RR )
93 82 84 86 90 91 92 syl32anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ -. X <_ ( x - z ) ) -> X e. RR )
94 80 93 ifclda 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> if ( X <_ ( x - z ) , ( x - z ) , X ) e. RR )
95 85 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ Y <_ ( z + x ) ) -> Y e. RR* )
96 78 76 readdcld 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( z + x ) e. RR )
97 96 adantr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ Y <_ ( z + x ) ) -> ( z + x ) e. RR )
98 mnfxr 
 |-  -oo e. RR*
99 98 a1i 
 |-  ( ph -> -oo e. RR* )
100 mnfle 
 |-  ( X e. RR* -> -oo <_ X )
101 83 100 syl 
 |-  ( ph -> -oo <_ X )
102 99 83 85 101 1 xrlelttrd 
 |-  ( ph -> -oo < Y )
103 102 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ Y <_ ( z + x ) ) -> -oo < Y )
104 simpr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ Y <_ ( z + x ) ) -> Y <_ ( z + x ) )
105 xrre 
 |-  ( ( ( Y e. RR* /\ ( z + x ) e. RR ) /\ ( -oo < Y /\ Y <_ ( z + x ) ) ) -> Y e. RR )
106 95 97 103 104 105 syl22anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ Y <_ ( z + x ) ) -> Y e. RR )
107 96 adantr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ -. Y <_ ( z + x ) ) -> ( z + x ) e. RR )
108 106 107 ifclda 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> if ( Y <_ ( z + x ) , Y , ( z + x ) ) e. RR )
109 76 rexrd 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> x e. RR* )
110 85 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> Y e. RR* )
111 rpgt0 
 |-  ( z e. RR+ -> 0 < z )
112 111 adantl 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> 0 < z )
113 78 76 ltsubposd 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( 0 < z <-> ( x - z ) < x ) )
114 112 113 mpbid 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( x - z ) < x )
115 eliooord 
 |-  ( x e. ( X (,) Y ) -> ( X < x /\ x < Y ) )
116 115 simprd 
 |-  ( x e. ( X (,) Y ) -> x < Y )
117 116 ad3antlr 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> x < Y )
118 81 109 110 114 117 xrlttrd 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( x - z ) < Y )
119 78 76 ltaddpos2d 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( 0 < z <-> x < ( z + x ) ) )
120 112 119 mpbid 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> x < ( z + x ) )
121 79 76 96 114 120 lttrd 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( x - z ) < ( z + x ) )
122 breq2 
 |-  ( Y = if ( Y <_ ( z + x ) , Y , ( z + x ) ) -> ( ( x - z ) < Y <-> ( x - z ) < if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) )
123 breq2 
 |-  ( ( z + x ) = if ( Y <_ ( z + x ) , Y , ( z + x ) ) -> ( ( x - z ) < ( z + x ) <-> ( x - z ) < if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) )
124 122 123 ifboth 
 |-  ( ( ( x - z ) < Y /\ ( x - z ) < ( z + x ) ) -> ( x - z ) < if ( Y <_ ( z + x ) , Y , ( z + x ) ) )
125 118 121 124 syl2anc 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( x - z ) < if ( Y <_ ( z + x ) , Y , ( z + x ) ) )
126 1 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> X < Y )
127 96 rexrd 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( z + x ) e. RR* )
128 115 simpld 
 |-  ( x e. ( X (,) Y ) -> X < x )
129 128 ad3antlr 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> X < x )
130 87 109 127 129 120 xrlttrd 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> X < ( z + x ) )
131 breq2 
 |-  ( Y = if ( Y <_ ( z + x ) , Y , ( z + x ) ) -> ( X < Y <-> X < if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) )
132 breq2 
 |-  ( ( z + x ) = if ( Y <_ ( z + x ) , Y , ( z + x ) ) -> ( X < ( z + x ) <-> X < if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) )
133 131 132 ifboth 
 |-  ( ( X < Y /\ X < ( z + x ) ) -> X < if ( Y <_ ( z + x ) , Y , ( z + x ) ) )
134 126 130 133 syl2anc 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> X < if ( Y <_ ( z + x ) , Y , ( z + x ) ) )
135 breq1 
 |-  ( ( x - z ) = if ( X <_ ( x - z ) , ( x - z ) , X ) -> ( ( x - z ) < if ( Y <_ ( z + x ) , Y , ( z + x ) ) <-> if ( X <_ ( x - z ) , ( x - z ) , X ) < if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) )
136 breq1 
 |-  ( X = if ( X <_ ( x - z ) , ( x - z ) , X ) -> ( X < if ( Y <_ ( z + x ) , Y , ( z + x ) ) <-> if ( X <_ ( x - z ) , ( x - z ) , X ) < if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) )
137 135 136 ifboth 
 |-  ( ( ( x - z ) < if ( Y <_ ( z + x ) , Y , ( z + x ) ) /\ X < if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) -> if ( X <_ ( x - z ) , ( x - z ) , X ) < if ( Y <_ ( z + x ) , Y , ( z + x ) ) )
138 125 134 137 syl2anc 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> if ( X <_ ( x - z ) , ( x - z ) , X ) < if ( Y <_ ( z + x ) , Y , ( z + x ) ) )
139 94 108 138 ltled 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> if ( X <_ ( x - z ) , ( x - z ) , X ) <_ if ( Y <_ ( z + x ) , Y , ( z + x ) ) )
140 ovolioo 
 |-  ( ( if ( X <_ ( x - z ) , ( x - z ) , X ) e. RR /\ if ( Y <_ ( z + x ) , Y , ( z + x ) ) e. RR /\ if ( X <_ ( x - z ) , ( x - z ) , X ) <_ if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) -> ( vol* ` ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) ) = ( if ( Y <_ ( z + x ) , Y , ( z + x ) ) - if ( X <_ ( x - z ) , ( x - z ) , X ) ) )
141 94 108 139 140 syl3anc 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( vol* ` ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) ) = ( if ( Y <_ ( z + x ) , Y , ( z + x ) ) - if ( X <_ ( x - z ) , ( x - z ) , X ) ) )
142 74 141 syl5eq 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( vol ` ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) ) = ( if ( Y <_ ( z + x ) , Y , ( z + x ) ) - if ( X <_ ( x - z ) , ( x - z ) , X ) ) )
143 108 94 resubcld 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( if ( Y <_ ( z + x ) , Y , ( z + x ) ) - if ( X <_ ( x - z ) , ( x - z ) , X ) ) e. RR )
144 142 143 eqeltrd 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( vol ` ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) ) e. RR )
145 rpgt0 
 |-  ( y e. RR+ -> 0 < y )
146 145 ad4antlr 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> 0 < y )
147 94 108 posdifd 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( if ( X <_ ( x - z ) , ( x - z ) , X ) < if ( Y <_ ( z + x ) , Y , ( z + x ) ) <-> 0 < ( if ( Y <_ ( z + x ) , Y , ( z + x ) ) - if ( X <_ ( x - z ) , ( x - z ) , X ) ) ) )
148 138 147 mpbid 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> 0 < ( if ( Y <_ ( z + x ) , Y , ( z + x ) ) - if ( X <_ ( x - z ) , ( x - z ) , X ) ) )
149 148 142 breqtrrd 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> 0 < ( vol ` ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) ) )
150 71 144 146 149 mulgt0d 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> 0 < ( y x. ( vol ` ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) ) ) )
151 iooin 
 |-  ( ( ( X e. RR* /\ Y e. RR* ) /\ ( ( x - z ) e. RR* /\ ( z + x ) e. RR* ) ) -> ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) = ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) )
152 87 110 81 127 151 syl22anc 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) = ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) )
153 152 eleq2d 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) <-> w e. ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) ) )
154 153 ifbid 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) = if ( w e. ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) , y , 0 ) )
155 154 mpteq2dv 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) = ( w e. RR |-> if ( w e. ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) , y , 0 ) ) )
156 155 fveq2d 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( S.2 ` ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) ) = ( S.2 ` ( w e. RR |-> if ( w e. ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) , y , 0 ) ) ) )
157 rpge0 
 |-  ( y e. RR+ -> 0 <_ y )
158 elrege0 
 |-  ( y e. ( 0 [,) +oo ) <-> ( y e. RR /\ 0 <_ y ) )
159 70 157 158 sylanbrc 
 |-  ( y e. RR+ -> y e. ( 0 [,) +oo ) )
160 159 ad4antlr 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> y e. ( 0 [,) +oo ) )
161 itg2const 
 |-  ( ( ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) e. dom vol /\ ( vol ` ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) ) e. RR /\ y e. ( 0 [,) +oo ) ) -> ( S.2 ` ( w e. RR |-> if ( w e. ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) , y , 0 ) ) ) = ( y x. ( vol ` ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) ) ) )
162 72 144 160 161 mp3an2i 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( S.2 ` ( w e. RR |-> if ( w e. ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) , y , 0 ) ) ) = ( y x. ( vol ` ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) ) ) )
163 156 162 eqtrd 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> ( S.2 ` ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) ) = ( y x. ( vol ` ( if ( X <_ ( x - z ) , ( x - z ) , X ) (,) if ( Y <_ ( z + x ) , Y , ( z + x ) ) ) ) ) )
164 150 163 breqtrrd 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> 0 < ( S.2 ` ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) ) )
165 164 adantr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> 0 < ( S.2 ` ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) ) )
166 59 ad5antlr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) : RR --> ( 0 [,] +oo ) )
167 66 ad5antlr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) : RR --> ( 0 [,] +oo ) )
168 fvoveq1 
 |-  ( u = w -> ( abs ` ( u - x ) ) = ( abs ` ( w - x ) ) )
169 168 breq1d 
 |-  ( u = w -> ( ( abs ` ( u - x ) ) < z <-> ( abs ` ( w - x ) ) < z ) )
170 169 imbrov2fvoveq 
 |-  ( u = w -> ( ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) <-> ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) )
171 170 rspccva 
 |-  ( ( A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) /\ w e. ( X (,) Y ) ) -> ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) )
172 breq1 
 |-  ( y = if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) -> ( y <_ if ( y <_ ( F ` w ) , y , 0 ) <-> if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) <_ if ( y <_ ( F ` w ) , y , 0 ) ) )
173 breq1 
 |-  ( 0 = if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) -> ( 0 <_ if ( y <_ ( F ` w ) , y , 0 ) <-> if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) <_ if ( y <_ ( F ` w ) , y , 0 ) ) )
174 70 leidd 
 |-  ( y e. RR+ -> y <_ y )
175 174 ad6antlr 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. ( ( x - z ) (,) ( z + x ) ) ) -> y <_ y )
176 75 ad4antlr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> x e. RR )
177 77 ad2antlr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> z e. RR )
178 176 177 resubcld 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( x - z ) e. RR )
179 178 rexrd 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( x - z ) e. RR* )
180 177 176 readdcld 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( z + x ) e. RR )
181 180 rexrd 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( z + x ) e. RR* )
182 elioo2 
 |-  ( ( ( x - z ) e. RR* /\ ( z + x ) e. RR* ) -> ( w e. ( ( x - z ) (,) ( z + x ) ) <-> ( w e. RR /\ ( x - z ) < w /\ w < ( z + x ) ) ) )
183 179 181 182 syl2anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( w e. ( ( x - z ) (,) ( z + x ) ) <-> ( w e. RR /\ ( x - z ) < w /\ w < ( z + x ) ) ) )
184 3anass 
 |-  ( ( w e. RR /\ ( x - z ) < w /\ w < ( z + x ) ) <-> ( w e. RR /\ ( ( x - z ) < w /\ w < ( z + x ) ) ) )
185 183 184 bitrdi 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( w e. ( ( x - z ) (,) ( z + x ) ) <-> ( w e. RR /\ ( ( x - z ) < w /\ w < ( z + x ) ) ) ) )
186 simpr 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> w e. RR )
187 75 ad5antlr 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> x e. RR )
188 186 187 resubcld 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> ( w - x ) e. RR )
189 77 ad3antlr 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> z e. RR )
190 188 189 absltd 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> ( ( abs ` ( w - x ) ) < z <-> ( -u z < ( w - x ) /\ ( w - x ) < z ) ) )
191 189 renegcld 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> -u z e. RR )
192 187 191 186 ltaddsub2d 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> ( ( x + -u z ) < w <-> -u z < ( w - x ) ) )
193 187 recnd 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> x e. CC )
194 189 recnd 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> z e. CC )
195 193 194 negsubd 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> ( x + -u z ) = ( x - z ) )
196 195 breq1d 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> ( ( x + -u z ) < w <-> ( x - z ) < w ) )
197 192 196 bitr3d 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> ( -u z < ( w - x ) <-> ( x - z ) < w ) )
198 186 187 189 ltsubaddd 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> ( ( w - x ) < z <-> w < ( z + x ) ) )
199 197 198 anbi12d 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> ( ( -u z < ( w - x ) /\ ( w - x ) < z ) <-> ( ( x - z ) < w /\ w < ( z + x ) ) ) )
200 190 199 bitrd 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> ( ( abs ` ( w - x ) ) < z <-> ( ( x - z ) < w /\ w < ( z + x ) ) ) )
201 200 pm5.32da 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( ( w e. RR /\ ( abs ` ( w - x ) ) < z ) <-> ( w e. RR /\ ( ( x - z ) < w /\ w < ( z + x ) ) ) ) )
202 185 201 bitr4d 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( w e. ( ( x - z ) (,) ( z + x ) ) <-> ( w e. RR /\ ( abs ` ( w - x ) ) < z ) ) )
203 202 biimpa 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. ( ( x - z ) (,) ( z + x ) ) ) -> ( w e. RR /\ ( abs ` ( w - x ) ) < z ) )
204 pm3.35 
 |-  ( ( ( abs ` ( w - x ) ) < z /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) )
205 204 ancoms 
 |-  ( ( ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) /\ ( abs ` ( w - x ) ) < z ) -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) )
206 70 ad6antlr 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) /\ ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) -> y e. RR )
207 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
208 2 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) -> F : RR --> ( 0 [,) +oo ) )
209 208 ffvelrnda 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) -> ( F ` w ) e. ( 0 [,) +oo ) )
210 207 209 sselid 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) -> ( F ` w ) e. RR )
211 210 adantr 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) /\ ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) -> ( F ` w ) e. RR )
212 2 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> F : RR --> ( 0 [,) +oo ) )
213 212 ffvelrnda 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
214 207 213 sselid 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. RR ) -> ( F ` x ) e. RR )
215 75 214 sylan2 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) -> ( F ` x ) e. RR )
216 215 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) -> ( F ` x ) e. RR )
217 210 216 resubcld 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) -> ( ( F ` w ) - ( F ` x ) ) e. RR )
218 70 ad2antlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) -> y e. RR )
219 215 218 resubcld 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) -> ( ( F ` x ) - y ) e. RR )
220 219 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) -> ( ( F ` x ) - y ) e. RR )
221 217 220 absltd 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) -> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) <-> ( -u ( ( F ` x ) - y ) < ( ( F ` w ) - ( F ` x ) ) /\ ( ( F ` w ) - ( F ` x ) ) < ( ( F ` x ) - y ) ) ) )
222 215 recnd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) -> ( F ` x ) e. CC )
223 rpcn 
 |-  ( y e. RR+ -> y e. CC )
224 223 ad2antlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) -> y e. CC )
225 222 224 negsubdi2d 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) -> -u ( ( F ` x ) - y ) = ( y - ( F ` x ) ) )
226 225 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) -> -u ( ( F ` x ) - y ) = ( y - ( F ` x ) ) )
227 226 breq1d 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) -> ( -u ( ( F ` x ) - y ) < ( ( F ` w ) - ( F ` x ) ) <-> ( y - ( F ` x ) ) < ( ( F ` w ) - ( F ` x ) ) ) )
228 227 anbi1d 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) -> ( ( -u ( ( F ` x ) - y ) < ( ( F ` w ) - ( F ` x ) ) /\ ( ( F ` w ) - ( F ` x ) ) < ( ( F ` x ) - y ) ) <-> ( ( y - ( F ` x ) ) < ( ( F ` w ) - ( F ` x ) ) /\ ( ( F ` w ) - ( F ` x ) ) < ( ( F ` x ) - y ) ) ) )
229 221 228 bitrd 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) -> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) <-> ( ( y - ( F ` x ) ) < ( ( F ` w ) - ( F ` x ) ) /\ ( ( F ` w ) - ( F ` x ) ) < ( ( F ` x ) - y ) ) ) )
230 229 simprbda 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) /\ ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) -> ( y - ( F ` x ) ) < ( ( F ` w ) - ( F ` x ) ) )
231 215 ad4antr 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) /\ ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) -> ( F ` x ) e. RR )
232 206 211 231 ltsub1d 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) /\ ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) -> ( y < ( F ` w ) <-> ( y - ( F ` x ) ) < ( ( F ` w ) - ( F ` x ) ) ) )
233 230 232 mpbird 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) /\ ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) -> y < ( F ` w ) )
234 206 211 233 ltled 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) /\ ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) -> y <_ ( F ` w ) )
235 205 234 sylan2 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ w e. RR ) /\ ( ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) /\ ( abs ` ( w - x ) ) < z ) ) -> y <_ ( F ` w ) )
236 235 an4s 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ ( w e. RR /\ ( abs ` ( w - x ) ) < z ) ) -> y <_ ( F ` w ) )
237 203 236 syldan 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. ( ( x - z ) (,) ( z + x ) ) ) -> y <_ ( F ` w ) )
238 237 iftrued 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. ( ( x - z ) (,) ( z + x ) ) ) -> if ( y <_ ( F ` w ) , y , 0 ) = y )
239 175 238 breqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. ( ( x - z ) (,) ( z + x ) ) ) -> y <_ if ( y <_ ( F ` w ) , y , 0 ) )
240 0le0 
 |-  0 <_ 0
241 breq2 
 |-  ( y = if ( y <_ ( F ` w ) , y , 0 ) -> ( 0 <_ y <-> 0 <_ if ( y <_ ( F ` w ) , y , 0 ) ) )
242 breq2 
 |-  ( 0 = if ( y <_ ( F ` w ) , y , 0 ) -> ( 0 <_ 0 <-> 0 <_ if ( y <_ ( F ` w ) , y , 0 ) ) )
243 241 242 ifboth 
 |-  ( ( 0 <_ y /\ 0 <_ 0 ) -> 0 <_ if ( y <_ ( F ` w ) , y , 0 ) )
244 157 240 243 sylancl 
 |-  ( y e. RR+ -> 0 <_ if ( y <_ ( F ` w ) , y , 0 ) )
245 244 ad6antlr 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ -. w e. ( ( x - z ) (,) ( z + x ) ) ) -> 0 <_ if ( y <_ ( F ` w ) , y , 0 ) )
246 172 173 239 245 ifbothda 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) <_ if ( y <_ ( F ` w ) , y , 0 ) )
247 171 246 sylan2 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ ( A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) /\ w e. ( X (,) Y ) ) ) -> if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) <_ if ( y <_ ( F ` w ) , y , 0 ) )
248 247 anassrs 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. ( X (,) Y ) ) -> if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) <_ if ( y <_ ( F ` w ) , y , 0 ) )
249 iftrue 
 |-  ( w e. ( X (,) Y ) -> if ( w e. ( X (,) Y ) , if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) , 0 ) = if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) )
250 249 adantl 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. ( X (,) Y ) ) -> if ( w e. ( X (,) Y ) , if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) , 0 ) = if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) )
251 iftrue 
 |-  ( w e. ( X (,) Y ) -> if ( w e. ( X (,) Y ) , if ( y <_ ( F ` w ) , y , 0 ) , 0 ) = if ( y <_ ( F ` w ) , y , 0 ) )
252 251 adantl 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. ( X (,) Y ) ) -> if ( w e. ( X (,) Y ) , if ( y <_ ( F ` w ) , y , 0 ) , 0 ) = if ( y <_ ( F ` w ) , y , 0 ) )
253 248 250 252 3brtr4d 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. ( X (,) Y ) ) -> if ( w e. ( X (,) Y ) , if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) , 0 ) <_ if ( w e. ( X (,) Y ) , if ( y <_ ( F ` w ) , y , 0 ) , 0 ) )
254 253 ex 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( w e. ( X (,) Y ) -> if ( w e. ( X (,) Y ) , if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) , 0 ) <_ if ( w e. ( X (,) Y ) , if ( y <_ ( F ` w ) , y , 0 ) , 0 ) ) )
255 240 a1i 
 |-  ( -. w e. ( X (,) Y ) -> 0 <_ 0 )
256 iffalse 
 |-  ( -. w e. ( X (,) Y ) -> if ( w e. ( X (,) Y ) , if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) , 0 ) = 0 )
257 iffalse 
 |-  ( -. w e. ( X (,) Y ) -> if ( w e. ( X (,) Y ) , if ( y <_ ( F ` w ) , y , 0 ) , 0 ) = 0 )
258 255 256 257 3brtr4d 
 |-  ( -. w e. ( X (,) Y ) -> if ( w e. ( X (,) Y ) , if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) , 0 ) <_ if ( w e. ( X (,) Y ) , if ( y <_ ( F ` w ) , y , 0 ) , 0 ) )
259 254 258 pm2.61d1 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> if ( w e. ( X (,) Y ) , if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) , 0 ) <_ if ( w e. ( X (,) Y ) , if ( y <_ ( F ` w ) , y , 0 ) , 0 ) )
260 elin 
 |-  ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) <-> ( w e. ( X (,) Y ) /\ w e. ( ( x - z ) (,) ( z + x ) ) ) )
261 ifbi 
 |-  ( ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) <-> ( w e. ( X (,) Y ) /\ w e. ( ( x - z ) (,) ( z + x ) ) ) ) -> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) = if ( ( w e. ( X (,) Y ) /\ w e. ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) )
262 260 261 ax-mp 
 |-  if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) = if ( ( w e. ( X (,) Y ) /\ w e. ( ( x - z ) (,) ( z + x ) ) ) , y , 0 )
263 ifan 
 |-  if ( ( w e. ( X (,) Y ) /\ w e. ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) = if ( w e. ( X (,) Y ) , if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) , 0 )
264 262 263 eqtri 
 |-  if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) = if ( w e. ( X (,) Y ) , if ( w e. ( ( x - z ) (,) ( z + x ) ) , y , 0 ) , 0 )
265 fveq2 
 |-  ( v = w -> ( F ` v ) = ( F ` w ) )
266 265 breq2d 
 |-  ( v = w -> ( y <_ ( F ` v ) <-> y <_ ( F ` w ) ) )
267 266 elrab 
 |-  ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } <-> ( w e. ( X (,) Y ) /\ y <_ ( F ` w ) ) )
268 ifbi 
 |-  ( ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } <-> ( w e. ( X (,) Y ) /\ y <_ ( F ` w ) ) ) -> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) = if ( ( w e. ( X (,) Y ) /\ y <_ ( F ` w ) ) , y , 0 ) )
269 267 268 ax-mp 
 |-  if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) = if ( ( w e. ( X (,) Y ) /\ y <_ ( F ` w ) ) , y , 0 )
270 ifan 
 |-  if ( ( w e. ( X (,) Y ) /\ y <_ ( F ` w ) ) , y , 0 ) = if ( w e. ( X (,) Y ) , if ( y <_ ( F ` w ) , y , 0 ) , 0 )
271 269 270 eqtri 
 |-  if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) = if ( w e. ( X (,) Y ) , if ( y <_ ( F ` w ) , y , 0 ) , 0 )
272 259 264 271 3brtr4g 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) <_ if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) )
273 272 ralrimivw 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> A. w e. RR if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) <_ if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) )
274 reex 
 |-  RR e. _V
275 274 a1i 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> RR e. _V )
276 57 ad6antlr 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) e. ( 0 [,] +oo ) )
277 64 ad6antlr 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) /\ w e. RR ) -> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) e. ( 0 [,] +oo ) )
278 eqidd 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) = ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) )
279 eqidd 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) = ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) )
280 275 276 277 278 279 ofrfval2 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) oR <_ ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) <-> A. w e. RR if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) <_ if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) )
281 273 280 mpbird 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) oR <_ ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) )
282 itg2le 
 |-  ( ( ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) oR <_ ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) -> ( S.2 ` ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) ) <_ ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) )
283 166 167 281 282 syl3anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> ( S.2 ` ( w e. RR |-> if ( w e. ( ( X (,) Y ) i^i ( ( x - z ) (,) ( z + x ) ) ) , y , 0 ) ) ) <_ ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) )
284 50 62 69 165 283 xrltletrd 
 |-  ( ( ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) /\ z e. RR+ ) /\ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) -> 0 < ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) )
285 4 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( ( F |` ( X (,) Y ) ) ` x ) ) -> ( F |` ( X (,) Y ) ) e. ( ( X (,) Y ) -cn-> CC ) )
286 simplr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( ( F |` ( X (,) Y ) ) ` x ) ) -> x e. ( X (,) Y ) )
287 fssres 
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ ( X (,) Y ) C_ RR ) -> ( F |` ( X (,) Y ) ) : ( X (,) Y ) --> ( 0 [,) +oo ) )
288 27 287 mpan2 
 |-  ( F : RR --> ( 0 [,) +oo ) -> ( F |` ( X (,) Y ) ) : ( X (,) Y ) --> ( 0 [,) +oo ) )
289 fss 
 |-  ( ( ( F |` ( X (,) Y ) ) : ( X (,) Y ) --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> ( F |` ( X (,) Y ) ) : ( X (,) Y ) --> RR )
290 207 289 mpan2 
 |-  ( ( F |` ( X (,) Y ) ) : ( X (,) Y ) --> ( 0 [,) +oo ) -> ( F |` ( X (,) Y ) ) : ( X (,) Y ) --> RR )
291 2 288 290 3syl 
 |-  ( ph -> ( F |` ( X (,) Y ) ) : ( X (,) Y ) --> RR )
292 291 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> ( F |` ( X (,) Y ) ) : ( X (,) Y ) --> RR )
293 292 ffvelrnda 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) -> ( ( F |` ( X (,) Y ) ) ` x ) e. RR )
294 293 218 resubcld 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) -> ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) e. RR )
295 294 adantr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( ( F |` ( X (,) Y ) ) ` x ) ) -> ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) e. RR )
296 218 293 posdifd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) -> ( y < ( ( F |` ( X (,) Y ) ) ` x ) <-> 0 < ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) ) )
297 296 biimpa 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( ( F |` ( X (,) Y ) ) ` x ) ) -> 0 < ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) )
298 295 297 elrpd 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( ( F |` ( X (,) Y ) ) ` x ) ) -> ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) e. RR+ )
299 cncfi 
 |-  ( ( ( F |` ( X (,) Y ) ) e. ( ( X (,) Y ) -cn-> CC ) /\ x e. ( X (,) Y ) /\ ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) e. RR+ ) -> E. z e. RR+ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( ( F |` ( X (,) Y ) ) ` u ) - ( ( F |` ( X (,) Y ) ) ` x ) ) ) < ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) ) )
300 285 286 298 299 syl3anc 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( ( F |` ( X (,) Y ) ) ` x ) ) -> E. z e. RR+ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( ( F |` ( X (,) Y ) ) ` u ) - ( ( F |` ( X (,) Y ) ) ` x ) ) ) < ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) ) )
301 300 ex 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) -> ( y < ( ( F |` ( X (,) Y ) ) ` x ) -> E. z e. RR+ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( ( F |` ( X (,) Y ) ) ` u ) - ( ( F |` ( X (,) Y ) ) ` x ) ) ) < ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) ) ) )
302 fvres 
 |-  ( x e. ( X (,) Y ) -> ( ( F |` ( X (,) Y ) ) ` x ) = ( F ` x ) )
303 302 breq2d 
 |-  ( x e. ( X (,) Y ) -> ( y < ( ( F |` ( X (,) Y ) ) ` x ) <-> y < ( F ` x ) ) )
304 303 adantl 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) -> ( y < ( ( F |` ( X (,) Y ) ) ` x ) <-> y < ( F ` x ) ) )
305 fvres 
 |-  ( u e. ( X (,) Y ) -> ( ( F |` ( X (,) Y ) ) ` u ) = ( F ` u ) )
306 305 adantl 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ u e. ( X (,) Y ) ) -> ( ( F |` ( X (,) Y ) ) ` u ) = ( F ` u ) )
307 302 ad2antlr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ u e. ( X (,) Y ) ) -> ( ( F |` ( X (,) Y ) ) ` x ) = ( F ` x ) )
308 306 307 oveq12d 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ u e. ( X (,) Y ) ) -> ( ( ( F |` ( X (,) Y ) ) ` u ) - ( ( F |` ( X (,) Y ) ) ` x ) ) = ( ( F ` u ) - ( F ` x ) ) )
309 308 fveq2d 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ u e. ( X (,) Y ) ) -> ( abs ` ( ( ( F |` ( X (,) Y ) ) ` u ) - ( ( F |` ( X (,) Y ) ) ` x ) ) ) = ( abs ` ( ( F ` u ) - ( F ` x ) ) ) )
310 302 oveq1d 
 |-  ( x e. ( X (,) Y ) -> ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) = ( ( F ` x ) - y ) )
311 310 ad2antlr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ u e. ( X (,) Y ) ) -> ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) = ( ( F ` x ) - y ) )
312 309 311 breq12d 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ u e. ( X (,) Y ) ) -> ( ( abs ` ( ( ( F |` ( X (,) Y ) ) ` u ) - ( ( F |` ( X (,) Y ) ) ` x ) ) ) < ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) <-> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) )
313 312 imbi2d 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ u e. ( X (,) Y ) ) -> ( ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( ( F |` ( X (,) Y ) ) ` u ) - ( ( F |` ( X (,) Y ) ) ` x ) ) ) < ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) ) <-> ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) )
314 313 ralbidva 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) -> ( A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( ( F |` ( X (,) Y ) ) ` u ) - ( ( F |` ( X (,) Y ) ) ` x ) ) ) < ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) ) <-> A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) )
315 314 rexbidv 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) -> ( E. z e. RR+ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( ( F |` ( X (,) Y ) ) ` u ) - ( ( F |` ( X (,) Y ) ) ` x ) ) ) < ( ( ( F |` ( X (,) Y ) ) ` x ) - y ) ) <-> E. z e. RR+ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) )
316 301 304 315 3imtr3d 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) -> ( y < ( F ` x ) -> E. z e. RR+ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) ) )
317 316 imp 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) -> E. z e. RR+ A. u e. ( X (,) Y ) ( ( abs ` ( u - x ) ) < z -> ( abs ` ( ( F ` u ) - ( F ` x ) ) ) < ( ( F ` x ) - y ) ) )
318 284 317 r19.29a 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. ( X (,) Y ) ) /\ y < ( F ` x ) ) -> 0 < ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) )
319 318 rexlimdva2 
 |-  ( ( ph /\ y e. RR+ ) -> ( E. x e. ( X (,) Y ) y < ( F ` x ) -> 0 < ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) ) )
320 49 319 sylbid 
 |-  ( ( ph /\ y e. RR+ ) -> ( y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) -> 0 < ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) ) )
321 320 imp 
 |-  ( ( ( ph /\ y e. RR+ ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> 0 < ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) )
322 66 ad2antlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) : RR --> ( 0 [,] +oo ) )
323 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
324 fss 
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : RR --> ( 0 [,] +oo ) )
325 2 323 324 sylancl 
 |-  ( ph -> F : RR --> ( 0 [,] +oo ) )
326 325 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> F : RR --> ( 0 [,] +oo ) )
327 breq1 
 |-  ( y = if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) -> ( y <_ ( F ` w ) <-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) <_ ( F ` w ) ) )
328 breq1 
 |-  ( 0 = if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) -> ( 0 <_ ( F ` w ) <-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) <_ ( F ` w ) ) )
329 267 simprbi 
 |-  ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } -> y <_ ( F ` w ) )
330 329 adantl 
 |-  ( ( ( ph /\ w e. RR ) /\ w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } ) -> y <_ ( F ` w ) )
331 2 ffvelrnda 
 |-  ( ( ph /\ w e. RR ) -> ( F ` w ) e. ( 0 [,) +oo ) )
332 elrege0 
 |-  ( ( F ` w ) e. ( 0 [,) +oo ) <-> ( ( F ` w ) e. RR /\ 0 <_ ( F ` w ) ) )
333 331 332 sylib 
 |-  ( ( ph /\ w e. RR ) -> ( ( F ` w ) e. RR /\ 0 <_ ( F ` w ) ) )
334 333 simprd 
 |-  ( ( ph /\ w e. RR ) -> 0 <_ ( F ` w ) )
335 334 adantr 
 |-  ( ( ( ph /\ w e. RR ) /\ -. w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } ) -> 0 <_ ( F ` w ) )
336 327 328 330 335 ifbothda 
 |-  ( ( ph /\ w e. RR ) -> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) <_ ( F ` w ) )
337 336 ralrimiva 
 |-  ( ph -> A. w e. RR if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) <_ ( F ` w ) )
338 337 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> A. w e. RR if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) <_ ( F ` w ) )
339 274 a1i 
 |-  ( ( ( ph /\ y e. RR+ ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> RR e. _V )
340 64 ad3antlr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) /\ w e. RR ) -> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) e. ( 0 [,] +oo ) )
341 fvexd 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) /\ w e. RR ) -> ( F ` w ) e. _V )
342 eqidd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) = ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) )
343 2 feqmptd 
 |-  ( ph -> F = ( w e. RR |-> ( F ` w ) ) )
344 343 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> F = ( w e. RR |-> ( F ` w ) ) )
345 339 340 341 342 344 ofrfval2 
 |-  ( ( ( ph /\ y e. RR+ ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> ( ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) oR <_ F <-> A. w e. RR if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) <_ ( F ` w ) ) )
346 338 345 mpbird 
 |-  ( ( ( ph /\ y e. RR+ ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) oR <_ F )
347 itg2le 
 |-  ( ( ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) : RR --> ( 0 [,] +oo ) /\ F : RR --> ( 0 [,] +oo ) /\ ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) oR <_ F ) -> ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) <_ ( S.2 ` F ) )
348 322 326 346 347 syl3anc 
 |-  ( ( ( ph /\ y e. RR+ ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) <_ ( S.2 ` F ) )
349 41 321 348 jca32 
 |-  ( ( ( ph /\ y e. RR+ ) /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> ( y e. RR+ /\ ( 0 < ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) /\ ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) <_ ( S.2 ` F ) ) ) )
350 349 expl 
 |-  ( ph -> ( ( y e. RR+ /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> ( y e. RR+ /\ ( 0 < ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) /\ ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) <_ ( S.2 ` F ) ) ) ) )
351 40 350 syl5 
 |-  ( ph -> ( ( y e. QQ /\ ( 0 < y /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) ) -> ( y e. RR+ /\ ( 0 < ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) /\ ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) <_ ( S.2 ` F ) ) ) ) )
352 351 reximdv2 
 |-  ( ph -> ( E. y e. QQ ( 0 < y /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> E. y e. RR+ ( 0 < ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) /\ ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) <_ ( S.2 ` F ) ) ) )
353 68 adantl 
 |-  ( ( ph /\ y e. RR+ ) -> ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) e. RR* )
354 itg2cl 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* )
355 325 354 syl 
 |-  ( ph -> ( S.2 ` F ) e. RR* )
356 355 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> ( S.2 ` F ) e. RR* )
357 xrltletr 
 |-  ( ( 0 e. RR* /\ ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) e. RR* /\ ( S.2 ` F ) e. RR* ) -> ( ( 0 < ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) /\ ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) <_ ( S.2 ` F ) ) -> 0 < ( S.2 ` F ) ) )
358 5 353 356 357 mp3an2i 
 |-  ( ( ph /\ y e. RR+ ) -> ( ( 0 < ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) /\ ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) <_ ( S.2 ` F ) ) -> 0 < ( S.2 ` F ) ) )
359 358 rexlimdva 
 |-  ( ph -> ( E. y e. RR+ ( 0 < ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) /\ ( S.2 ` ( w e. RR |-> if ( w e. { v e. ( X (,) Y ) | y <_ ( F ` v ) } , y , 0 ) ) ) <_ ( S.2 ` F ) ) -> 0 < ( S.2 ` F ) ) )
360 352 359 syld 
 |-  ( ph -> ( E. y e. QQ ( 0 < y /\ y < sup ( ( F " ( X (,) Y ) ) , RR* , < ) ) -> 0 < ( S.2 ` F ) ) )
361 34 360 mpd 
 |-  ( ph -> 0 < ( S.2 ` F ) )