Metamath Proof Explorer

Theorem ivthlem2

Description: Lemma for ivth . Show that the supremum of S cannot be less than U . If it was, continuity of F implies that there are points just above the supremum that are also less than U , a contradiction. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Hypotheses ivth.1 
|- ( ph -> A e. RR )
ivth.2 
|- ( ph -> B e. RR )
ivth.3 
|- ( ph -> U e. RR )
ivth.4 
|- ( ph -> A < B )
ivth.5 
|- ( ph -> ( A [,] B ) C_ D )
ivth.7 
|- ( ph -> F e. ( D -cn-> CC ) )
ivth.8 
|- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )
ivth.9 
|- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )
ivth.10 
|- S = { x e. ( A [,] B ) | ( F ` x ) <_ U }
ivth.11 
|- C = sup ( S , RR , < )
Assertion ivthlem2 
|- ( ph -> -. ( F ` C ) < U )

Proof

Step Hyp Ref Expression
1 ivth.1 
 |-  ( ph -> A e. RR )
2 ivth.2 
 |-  ( ph -> B e. RR )
3 ivth.3 
 |-  ( ph -> U e. RR )
4 ivth.4 
 |-  ( ph -> A < B )
5 ivth.5 
 |-  ( ph -> ( A [,] B ) C_ D )
6 ivth.7 
 |-  ( ph -> F e. ( D -cn-> CC ) )
7 ivth.8 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )
8 ivth.9 
 |-  ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )
9 ivth.10 
 |-  S = { x e. ( A [,] B ) | ( F ` x ) <_ U }
10 ivth.11 
 |-  C = sup ( S , RR , < )
11 6 adantr 
 |-  ( ( ph /\ ( F ` C ) < U ) -> F e. ( D -cn-> CC ) )
12 9 ssrab3 
 |-  S C_ ( A [,] B )
13 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
14 1 2 13 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
15 12 14 sstrid 
 |-  ( ph -> S C_ RR )
16 1 2 3 4 5 6 7 8 9 ivthlem1 
 |-  ( ph -> ( A e. S /\ A. z e. S z <_ B ) )
17 16 simpld 
 |-  ( ph -> A e. S )
18 17 ne0d 
 |-  ( ph -> S =/= (/) )
19 16 simprd 
 |-  ( ph -> A. z e. S z <_ B )
20 brralrspcev 
 |-  ( ( B e. RR /\ A. z e. S z <_ B ) -> E. x e. RR A. z e. S z <_ x )
21 2 19 20 syl2anc 
 |-  ( ph -> E. x e. RR A. z e. S z <_ x )
22 15 18 21 suprcld 
 |-  ( ph -> sup ( S , RR , < ) e. RR )
23 10 22 eqeltrid 
 |-  ( ph -> C e. RR )
24 15 18 21 17 suprubd 
 |-  ( ph -> A <_ sup ( S , RR , < ) )
25 24 10 breqtrrdi 
 |-  ( ph -> A <_ C )
26 15 18 21 3jca 
 |-  ( ph -> ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) )
27 suprleub 
 |-  ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) /\ B e. RR ) -> ( sup ( S , RR , < ) <_ B <-> A. z e. S z <_ B ) )
28 26 2 27 syl2anc 
 |-  ( ph -> ( sup ( S , RR , < ) <_ B <-> A. z e. S z <_ B ) )
29 19 28 mpbird 
 |-  ( ph -> sup ( S , RR , < ) <_ B )
30 10 29 eqbrtrid 
 |-  ( ph -> C <_ B )
31 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
32 1 2 31 syl2anc 
 |-  ( ph -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
33 23 25 30 32 mpbir3and 
 |-  ( ph -> C e. ( A [,] B ) )
34 5 33 sseldd 
 |-  ( ph -> C e. D )
35 34 adantr 
 |-  ( ( ph /\ ( F ` C ) < U ) -> C e. D )
36 fveq2 
 |-  ( x = C -> ( F ` x ) = ( F ` C ) )
37 36 eleq1d 
 |-  ( x = C -> ( ( F ` x ) e. RR <-> ( F ` C ) e. RR ) )
38 7 ralrimiva 
 |-  ( ph -> A. x e. ( A [,] B ) ( F ` x ) e. RR )
39 37 38 33 rspcdva 
 |-  ( ph -> ( F ` C ) e. RR )
40 difrp 
 |-  ( ( ( F ` C ) e. RR /\ U e. RR ) -> ( ( F ` C ) < U <-> ( U - ( F ` C ) ) e. RR+ ) )
41 39 3 40 syl2anc 
 |-  ( ph -> ( ( F ` C ) < U <-> ( U - ( F ` C ) ) e. RR+ ) )
42 41 biimpa 
 |-  ( ( ph /\ ( F ` C ) < U ) -> ( U - ( F ` C ) ) e. RR+ )
43 cncfi 
 |-  ( ( F e. ( D -cn-> CC ) /\ C e. D /\ ( U - ( F ` C ) ) e. RR+ ) -> E. z e. RR+ A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) )
44 11 35 42 43 syl3anc 
 |-  ( ( ph /\ ( F ` C ) < U ) -> E. z e. RR+ A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) )
45 ssralv 
 |-  ( ( A [,] B ) C_ D -> ( A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) -> A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) ) )
46 5 45 syl 
 |-  ( ph -> ( A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) -> A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) ) )
47 46 ad2antrr 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) -> A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) ) )
48 2 ad2antrr 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> B e. RR )
49 23 ad2antrr 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> C e. RR )
50 rphalfcl 
 |-  ( z e. RR+ -> ( z / 2 ) e. RR+ )
51 50 adantl 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( z / 2 ) e. RR+ )
52 51 rpred 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( z / 2 ) e. RR )
53 49 52 readdcld 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( C + ( z / 2 ) ) e. RR )
54 48 53 ifcld 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. RR )
55 1 ad2antrr 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> A e. RR )
56 25 ad2antrr 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> A <_ C )
57 8 simprd 
 |-  ( ph -> U < ( F ` B ) )
58 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
59 58 eleq1d 
 |-  ( x = B -> ( ( F ` x ) e. RR <-> ( F ` B ) e. RR ) )
60 1 rexrd 
 |-  ( ph -> A e. RR* )
61 2 rexrd 
 |-  ( ph -> B e. RR* )
62 1 2 4 ltled 
 |-  ( ph -> A <_ B )
63 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
64 60 61 62 63 syl3anc 
 |-  ( ph -> B e. ( A [,] B ) )
65 59 38 64 rspcdva 
 |-  ( ph -> ( F ` B ) e. RR )
66 lttr 
 |-  ( ( ( F ` C ) e. RR /\ U e. RR /\ ( F ` B ) e. RR ) -> ( ( ( F ` C ) < U /\ U < ( F ` B ) ) -> ( F ` C ) < ( F ` B ) ) )
67 39 3 65 66 syl3anc 
 |-  ( ph -> ( ( ( F ` C ) < U /\ U < ( F ` B ) ) -> ( F ` C ) < ( F ` B ) ) )
68 57 67 mpan2d 
 |-  ( ph -> ( ( F ` C ) < U -> ( F ` C ) < ( F ` B ) ) )
69 68 imp 
 |-  ( ( ph /\ ( F ` C ) < U ) -> ( F ` C ) < ( F ` B ) )
70 69 adantr 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( F ` C ) < ( F ` B ) )
71 39 ltnrd 
 |-  ( ph -> -. ( F ` C ) < ( F ` C ) )
72 fveq2 
 |-  ( B = C -> ( F ` B ) = ( F ` C ) )
73 72 breq2d 
 |-  ( B = C -> ( ( F ` C ) < ( F ` B ) <-> ( F ` C ) < ( F ` C ) ) )
74 73 notbid 
 |-  ( B = C -> ( -. ( F ` C ) < ( F ` B ) <-> -. ( F ` C ) < ( F ` C ) ) )
75 71 74 syl5ibrcom 
 |-  ( ph -> ( B = C -> -. ( F ` C ) < ( F ` B ) ) )
76 75 necon2ad 
 |-  ( ph -> ( ( F ` C ) < ( F ` B ) -> B =/= C ) )
77 76 30 jctild 
 |-  ( ph -> ( ( F ` C ) < ( F ` B ) -> ( C <_ B /\ B =/= C ) ) )
78 23 2 ltlend 
 |-  ( ph -> ( C < B <-> ( C <_ B /\ B =/= C ) ) )
79 77 78 sylibrd 
 |-  ( ph -> ( ( F ` C ) < ( F ` B ) -> C < B ) )
80 79 ad2antrr 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( ( F ` C ) < ( F ` B ) -> C < B ) )
81 70 80 mpd 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> C < B )
82 49 51 ltaddrpd 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> C < ( C + ( z / 2 ) ) )
83 breq2 
 |-  ( B = if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) -> ( C < B <-> C < if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) ) )
84 breq2 
 |-  ( ( C + ( z / 2 ) ) = if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) -> ( C < ( C + ( z / 2 ) ) <-> C < if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) ) )
85 83 84 ifboth 
 |-  ( ( C < B /\ C < ( C + ( z / 2 ) ) ) -> C < if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) )
86 81 82 85 syl2anc 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> C < if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) )
87 49 54 86 ltled 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> C <_ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) )
88 55 49 54 56 87 letrd 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> A <_ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) )
89 min1 
 |-  ( ( B e. RR /\ ( C + ( z / 2 ) ) e. RR ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) <_ B )
90 48 53 89 syl2anc 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) <_ B )
91 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. ( A [,] B ) <-> ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. RR /\ A <_ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) /\ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) <_ B ) ) )
92 1 2 91 syl2anc 
 |-  ( ph -> ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. ( A [,] B ) <-> ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. RR /\ A <_ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) /\ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) <_ B ) ) )
93 92 ad2antrr 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. ( A [,] B ) <-> ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. RR /\ A <_ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) /\ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) <_ B ) ) )
94 54 88 90 93 mpbir3and 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. ( A [,] B ) )
95 49 54 87 abssubge0d 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( abs ` ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) ) = ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) )
96 rpre 
 |-  ( z e. RR+ -> z e. RR )
97 96 adantl 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> z e. RR )
98 49 97 readdcld 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( C + z ) e. RR )
99 min2 
 |-  ( ( B e. RR /\ ( C + ( z / 2 ) ) e. RR ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) <_ ( C + ( z / 2 ) ) )
100 48 53 99 syl2anc 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) <_ ( C + ( z / 2 ) ) )
101 rphalflt 
 |-  ( z e. RR+ -> ( z / 2 ) < z )
102 101 adantl 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( z / 2 ) < z )
103 52 97 49 102 ltadd2dd 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( C + ( z / 2 ) ) < ( C + z ) )
104 54 53 98 100 103 lelttrd 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) < ( C + z ) )
105 54 49 97 ltsubadd2d 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) < z <-> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) < ( C + z ) ) )
106 104 105 mpbird 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) < z )
107 95 106 eqbrtrd 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( abs ` ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) ) < z )
108 fvoveq1 
 |-  ( y = if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) -> ( abs ` ( y - C ) ) = ( abs ` ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) ) )
109 108 breq1d 
 |-  ( y = if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) -> ( ( abs ` ( y - C ) ) < z <-> ( abs ` ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) ) < z ) )
110 breq2 
 |-  ( y = if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) -> ( C < y <-> C < if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) ) )
111 109 110 anbi12d 
 |-  ( y = if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) -> ( ( ( abs ` ( y - C ) ) < z /\ C < y ) <-> ( ( abs ` ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) ) < z /\ C < if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) ) ) )
112 111 rspcev 
 |-  ( ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. ( A [,] B ) /\ ( ( abs ` ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) ) < z /\ C < if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) ) ) -> E. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z /\ C < y ) )
113 94 107 86 112 syl12anc 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> E. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z /\ C < y ) )
114 r19.29 
 |-  ( ( A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) /\ E. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z /\ C < y ) ) -> E. y e. ( A [,] B ) ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) /\ ( ( abs ` ( y - C ) ) < z /\ C < y ) ) )
115 pm3.45 
 |-  ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) -> ( ( ( abs ` ( y - C ) ) < z /\ C < y ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) /\ C < y ) ) )
116 115 imp 
 |-  ( ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) /\ ( ( abs ` ( y - C ) ) < z /\ C < y ) ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) /\ C < y ) )
117 simprr 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> C < y )
118 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
119 118 eleq1d 
 |-  ( x = y -> ( ( F ` x ) e. RR <-> ( F ` y ) e. RR ) )
120 simplll 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ph )
121 120 38 syl 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> A. x e. ( A [,] B ) ( F ` x ) e. RR )
122 simprl 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> y e. ( A [,] B ) )
123 119 121 122 rspcdva 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( F ` y ) e. RR )
124 120 39 syl 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( F ` C ) e. RR )
125 120 3 syl 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> U e. RR )
126 125 124 resubcld 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( U - ( F ` C ) ) e. RR )
127 123 124 126 absdifltd 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) <-> ( ( ( F ` C ) - ( U - ( F ` C ) ) ) < ( F ` y ) /\ ( F ` y ) < ( ( F ` C ) + ( U - ( F ` C ) ) ) ) ) )
128 ltle 
 |-  ( ( ( F ` y ) e. RR /\ U e. RR ) -> ( ( F ` y ) < U -> ( F ` y ) <_ U ) )
129 123 125 128 syl2anc 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( F ` y ) < U -> ( F ` y ) <_ U ) )
130 124 recnd 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( F ` C ) e. CC )
131 125 recnd 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> U e. CC )
132 130 131 pncan3d 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( F ` C ) + ( U - ( F ` C ) ) ) = U )
133 132 breq2d 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( F ` y ) < ( ( F ` C ) + ( U - ( F ` C ) ) ) <-> ( F ` y ) < U ) )
134 118 breq1d 
 |-  ( x = y -> ( ( F ` x ) <_ U <-> ( F ` y ) <_ U ) )
135 134 9 elrab2 
 |-  ( y e. S <-> ( y e. ( A [,] B ) /\ ( F ` y ) <_ U ) )
136 135 baib 
 |-  ( y e. ( A [,] B ) -> ( y e. S <-> ( F ` y ) <_ U ) )
137 136 ad2antrl 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( y e. S <-> ( F ` y ) <_ U ) )
138 129 133 137 3imtr4d 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( F ` y ) < ( ( F ` C ) + ( U - ( F ` C ) ) ) -> y e. S ) )
139 suprub 
 |-  ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) /\ y e. S ) -> y <_ sup ( S , RR , < ) )
140 139 10 breqtrrdi 
 |-  ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) /\ y e. S ) -> y <_ C )
141 140 ex 
 |-  ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) -> ( y e. S -> y <_ C ) )
142 120 26 141 3syl 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( y e. S -> y <_ C ) )
143 120 14 syl 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( A [,] B ) C_ RR )
144 143 122 sseldd 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> y e. RR )
145 120 23 syl 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> C e. RR )
146 144 145 lenltd 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( y <_ C <-> -. C < y ) )
147 142 146 sylibd 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( y e. S -> -. C < y ) )
148 138 147 syld 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( F ` y ) < ( ( F ` C ) + ( U - ( F ` C ) ) ) -> -. C < y ) )
149 148 adantld 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( ( ( F ` C ) - ( U - ( F ` C ) ) ) < ( F ` y ) /\ ( F ` y ) < ( ( F ` C ) + ( U - ( F ` C ) ) ) ) -> -. C < y ) )
150 127 149 sylbid 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) -> -. C < y ) )
151 117 150 mt2d 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> -. ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) )
152 151 pm2.21d 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) -> -. ( F ` C ) < U ) )
153 152 expr 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ y e. ( A [,] B ) ) -> ( C < y -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) -> -. ( F ` C ) < U ) ) )
154 153 impcomd 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ y e. ( A [,] B ) ) -> ( ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) /\ C < y ) -> -. ( F ` C ) < U ) )
155 116 154 syl5 
 |-  ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ y e. ( A [,] B ) ) -> ( ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) /\ ( ( abs ` ( y - C ) ) < z /\ C < y ) ) -> -. ( F ` C ) < U ) )
156 155 rexlimdva 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( E. y e. ( A [,] B ) ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) /\ ( ( abs ` ( y - C ) ) < z /\ C < y ) ) -> -. ( F ` C ) < U ) )
157 114 156 syl5 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( ( A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) /\ E. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z /\ C < y ) ) -> -. ( F ` C ) < U ) )
158 113 157 mpan2d 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) -> -. ( F ` C ) < U ) )
159 47 158 syld 
 |-  ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) -> -. ( F ` C ) < U ) )
160 159 rexlimdva 
 |-  ( ( ph /\ ( F ` C ) < U ) -> ( E. z e. RR+ A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) -> -. ( F ` C ) < U ) )
161 44 160 mpd 
 |-  ( ( ph /\ ( F ` C ) < U ) -> -. ( F ` C ) < U )
162 161 pm2.01da 
 |-  ( ph -> -. ( F ` C ) < U )