Metamath Proof Explorer

Theorem ivthlem3

Description: Lemma for ivth , the intermediate value theorem. Show that ( FC ) cannot be greater than U , and so establish the existence of a root of the function. (Contributed by Mario Carneiro, 30-Apr-2014) (Revised 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 ivthlem3 
|- ( ph -> ( C e. ( A (,) B ) /\ ( 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 9 ssrab3 
 |-  S C_ ( A [,] B )
12 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
13 1 2 12 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
14 11 13 sstrid 
 |-  ( ph -> S C_ RR )
15 1 2 3 4 5 6 7 8 9 ivthlem1 
 |-  ( ph -> ( A e. S /\ A. z e. S z <_ B ) )
16 15 simpld 
 |-  ( ph -> A e. S )
17 16 ne0d 
 |-  ( ph -> S =/= (/) )
18 15 simprd 
 |-  ( ph -> A. z e. S z <_ B )
19 brralrspcev 
 |-  ( ( B e. RR /\ A. z e. S z <_ B ) -> E. x e. RR A. z e. S z <_ x )
20 2 18 19 syl2anc 
 |-  ( ph -> E. x e. RR A. z e. S z <_ x )
21 14 17 20 suprcld 
 |-  ( ph -> sup ( S , RR , < ) e. RR )
22 10 21 eqeltrid 
 |-  ( ph -> C e. RR )
23 8 simpld 
 |-  ( ph -> ( F ` A ) < U )
24 1 2 3 4 5 6 7 8 9 10 ivthlem2 
 |-  ( ph -> -. ( F ` C ) < U )
25 6 adantr 
 |-  ( ( ph /\ U < ( F ` C ) ) -> F e. ( D -cn-> CC ) )
26 14 17 20 16 suprubd 
 |-  ( ph -> A <_ sup ( S , RR , < ) )
27 26 10 breqtrrdi 
 |-  ( ph -> A <_ C )
28 14 17 20 3jca 
 |-  ( ph -> ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) )
29 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 ) )
30 28 2 29 syl2anc 
 |-  ( ph -> ( sup ( S , RR , < ) <_ B <-> A. z e. S z <_ B ) )
31 18 30 mpbird 
 |-  ( ph -> sup ( S , RR , < ) <_ B )
32 10 31 eqbrtrid 
 |-  ( ph -> C <_ B )
33 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
34 1 2 33 syl2anc 
 |-  ( ph -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
35 22 27 32 34 mpbir3and 
 |-  ( ph -> C e. ( A [,] B ) )
36 5 35 sseldd 
 |-  ( ph -> C e. D )
37 36 adantr 
 |-  ( ( ph /\ U < ( F ` C ) ) -> C e. D )
38 fveq2 
 |-  ( x = C -> ( F ` x ) = ( F ` C ) )
39 38 eleq1d 
 |-  ( x = C -> ( ( F ` x ) e. RR <-> ( F ` C ) e. RR ) )
40 7 ralrimiva 
 |-  ( ph -> A. x e. ( A [,] B ) ( F ` x ) e. RR )
41 39 40 35 rspcdva 
 |-  ( ph -> ( F ` C ) e. RR )
42 difrp 
 |-  ( ( U e. RR /\ ( F ` C ) e. RR ) -> ( U < ( F ` C ) <-> ( ( F ` C ) - U ) e. RR+ ) )
43 3 41 42 syl2anc 
 |-  ( ph -> ( U < ( F ` C ) <-> ( ( F ` C ) - U ) e. RR+ ) )
44 43 biimpa 
 |-  ( ( ph /\ U < ( F ` C ) ) -> ( ( F ` C ) - U ) e. RR+ )
45 cncfi 
 |-  ( ( F e. ( D -cn-> CC ) /\ C e. D /\ ( ( F ` C ) - U ) e. RR+ ) -> E. z e. RR+ A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) )
46 25 37 44 45 syl3anc 
 |-  ( ( ph /\ U < ( F ` C ) ) -> E. z e. RR+ A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) )
47 ssralv 
 |-  ( ( A [,] B ) C_ D -> ( A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) -> A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) ) )
48 5 47 syl 
 |-  ( ph -> ( A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) -> A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) ) )
49 48 ad2antrr 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> ( A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) -> A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) ) )
50 22 ad2antrr 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> C e. RR )
51 ltsubrp 
 |-  ( ( C e. RR /\ z e. RR+ ) -> ( C - z ) < C )
52 50 51 sylancom 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> ( C - z ) < C )
53 52 10 breqtrdi 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> ( C - z ) < sup ( S , RR , < ) )
54 28 ad2antrr 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) )
55 rpre 
 |-  ( z e. RR+ -> z e. RR )
56 55 adantl 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> z e. RR )
57 50 56 resubcld 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> ( C - z ) e. RR )
58 suprlub 
 |-  ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) /\ ( C - z ) e. RR ) -> ( ( C - z ) < sup ( S , RR , < ) <-> E. y e. S ( C - z ) < y ) )
59 54 57 58 syl2anc 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> ( ( C - z ) < sup ( S , RR , < ) <-> E. y e. S ( C - z ) < y ) )
60 53 59 mpbid 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> E. y e. S ( C - z ) < y )
61 11 sseli 
 |-  ( y e. S -> y e. ( A [,] B ) )
62 61 ad2antrl 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> y e. ( A [,] B ) )
63 simplll 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> ph )
64 63 13 syl 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> ( A [,] B ) C_ RR )
65 64 62 sseldd 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> y e. RR )
66 63 22 syl 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> C e. RR )
67 63 28 syl 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) )
68 simprl 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> y e. S )
69 suprub 
 |-  ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) /\ y e. S ) -> y <_ sup ( S , RR , < ) )
70 67 68 69 syl2anc 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> y <_ sup ( S , RR , < ) )
71 70 10 breqtrrdi 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> y <_ C )
72 65 66 71 abssuble0d 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> ( abs ` ( y - C ) ) = ( C - y ) )
73 56 adantr 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> z e. RR )
74 simprr 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> ( C - z ) < y )
75 66 73 65 74 ltsub23d 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> ( C - y ) < z )
76 72 75 eqbrtrd 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> ( abs ` ( y - C ) ) < z )
77 62 76 68 jca32 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ ( y e. S /\ ( C - z ) < y ) ) -> ( y e. ( A [,] B ) /\ ( ( abs ` ( y - C ) ) < z /\ y e. S ) ) )
78 77 ex 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> ( ( y e. S /\ ( C - z ) < y ) -> ( y e. ( A [,] B ) /\ ( ( abs ` ( y - C ) ) < z /\ y e. S ) ) ) )
79 78 reximdv2 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> ( E. y e. S ( C - z ) < y -> E. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z /\ y e. S ) ) )
80 60 79 mpd 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> E. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z /\ y e. S ) )
81 r19.29 
 |-  ( ( A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) /\ E. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z /\ y e. S ) ) -> E. y e. ( A [,] B ) ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) /\ ( ( abs ` ( y - C ) ) < z /\ y e. S ) ) )
82 pm3.45 
 |-  ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) -> ( ( ( abs ` ( y - C ) ) < z /\ y e. S ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) /\ y e. S ) ) )
83 82 imp 
 |-  ( ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) /\ ( ( abs ` ( y - C ) ) < z /\ y e. S ) ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) /\ y e. S ) )
84 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
85 84 eleq1d 
 |-  ( x = y -> ( ( F ` x ) e. RR <-> ( F ` y ) e. RR ) )
86 40 ad2antrr 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> A. x e. ( A [,] B ) ( F ` x ) e. RR )
87 61 ad2antll 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> y e. ( A [,] B ) )
88 85 86 87 rspcdva 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> ( F ` y ) e. RR )
89 41 ad2antrr 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> ( F ` C ) e. RR )
90 3 ad2antrr 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> U e. RR )
91 89 90 resubcld 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> ( ( F ` C ) - U ) e. RR )
92 88 89 91 absdifltd 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) <-> ( ( ( F ` C ) - ( ( F ` C ) - U ) ) < ( F ` y ) /\ ( F ` y ) < ( ( F ` C ) + ( ( F ` C ) - U ) ) ) ) )
93 89 recnd 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> ( F ` C ) e. CC )
94 90 recnd 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> U e. CC )
95 93 94 nncand 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> ( ( F ` C ) - ( ( F ` C ) - U ) ) = U )
96 95 breq1d 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> ( ( ( F ` C ) - ( ( F ` C ) - U ) ) < ( F ` y ) <-> U < ( F ` y ) ) )
97 84 breq1d 
 |-  ( x = y -> ( ( F ` x ) <_ U <-> ( F ` y ) <_ U ) )
98 97 9 elrab2 
 |-  ( y e. S <-> ( y e. ( A [,] B ) /\ ( F ` y ) <_ U ) )
99 98 simprbi 
 |-  ( y e. S -> ( F ` y ) <_ U )
100 99 ad2antll 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> ( F ` y ) <_ U )
101 88 90 100 lensymd 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> -. U < ( F ` y ) )
102 101 pm2.21d 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> ( U < ( F ` y ) -> -. U < ( F ` C ) ) )
103 96 102 sylbid 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> ( ( ( F ` C ) - ( ( F ` C ) - U ) ) < ( F ` y ) -> -. U < ( F ` C ) ) )
104 103 adantrd 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> ( ( ( ( F ` C ) - ( ( F ` C ) - U ) ) < ( F ` y ) /\ ( F ` y ) < ( ( F ` C ) + ( ( F ` C ) - U ) ) ) -> -. U < ( F ` C ) ) )
105 92 104 sylbid 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ ( z e. RR+ /\ y e. S ) ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) -> -. U < ( F ` C ) ) )
106 105 expr 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> ( y e. S -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) -> -. U < ( F ` C ) ) ) )
107 106 impcomd 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> ( ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) /\ y e. S ) -> -. U < ( F ` C ) ) )
108 107 adantr 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ y e. ( A [,] B ) ) -> ( ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) /\ y e. S ) -> -. U < ( F ` C ) ) )
109 83 108 syl5 
 |-  ( ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) /\ y e. ( A [,] B ) ) -> ( ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) /\ ( ( abs ` ( y - C ) ) < z /\ y e. S ) ) -> -. U < ( F ` C ) ) )
110 109 rexlimdva 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> ( E. y e. ( A [,] B ) ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) /\ ( ( abs ` ( y - C ) ) < z /\ y e. S ) ) -> -. U < ( F ` C ) ) )
111 81 110 syl5 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> ( ( A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) /\ E. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z /\ y e. S ) ) -> -. U < ( F ` C ) ) )
112 80 111 mpan2d 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> ( A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) -> -. U < ( F ` C ) ) )
113 49 112 syld 
 |-  ( ( ( ph /\ U < ( F ` C ) ) /\ z e. RR+ ) -> ( A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) -> -. U < ( F ` C ) ) )
114 113 rexlimdva 
 |-  ( ( ph /\ U < ( F ` C ) ) -> ( E. z e. RR+ A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( ( F ` C ) - U ) ) -> -. U < ( F ` C ) ) )
115 46 114 mpd 
 |-  ( ( ph /\ U < ( F ` C ) ) -> -. U < ( F ` C ) )
116 115 pm2.01da 
 |-  ( ph -> -. U < ( F ` C ) )
117 41 3 lttri3d 
 |-  ( ph -> ( ( F ` C ) = U <-> ( -. ( F ` C ) < U /\ -. U < ( F ` C ) ) ) )
118 24 116 117 mpbir2and 
 |-  ( ph -> ( F ` C ) = U )
119 23 118 breqtrrd 
 |-  ( ph -> ( F ` A ) < ( F ` C ) )
120 41 ltnrd 
 |-  ( ph -> -. ( F ` C ) < ( F ` C ) )
121 fveq2 
 |-  ( C = A -> ( F ` C ) = ( F ` A ) )
122 121 breq1d 
 |-  ( C = A -> ( ( F ` C ) < ( F ` C ) <-> ( F ` A ) < ( F ` C ) ) )
123 122 notbid 
 |-  ( C = A -> ( -. ( F ` C ) < ( F ` C ) <-> -. ( F ` A ) < ( F ` C ) ) )
124 120 123 syl5ibcom 
 |-  ( ph -> ( C = A -> -. ( F ` A ) < ( F ` C ) ) )
125 124 necon2ad 
 |-  ( ph -> ( ( F ` A ) < ( F ` C ) -> C =/= A ) )
126 125 27 jctild 
 |-  ( ph -> ( ( F ` A ) < ( F ` C ) -> ( A <_ C /\ C =/= A ) ) )
127 1 22 ltlend 
 |-  ( ph -> ( A < C <-> ( A <_ C /\ C =/= A ) ) )
128 126 127 sylibrd 
 |-  ( ph -> ( ( F ` A ) < ( F ` C ) -> A < C ) )
129 119 128 mpd 
 |-  ( ph -> A < C )
130 8 simprd 
 |-  ( ph -> U < ( F ` B ) )
131 118 130 eqbrtrd 
 |-  ( ph -> ( F ` C ) < ( F ` B ) )
132 fveq2 
 |-  ( B = C -> ( F ` B ) = ( F ` C ) )
133 132 breq2d 
 |-  ( B = C -> ( ( F ` C ) < ( F ` B ) <-> ( F ` C ) < ( F ` C ) ) )
134 133 notbid 
 |-  ( B = C -> ( -. ( F ` C ) < ( F ` B ) <-> -. ( F ` C ) < ( F ` C ) ) )
135 120 134 syl5ibrcom 
 |-  ( ph -> ( B = C -> -. ( F ` C ) < ( F ` B ) ) )
136 135 necon2ad 
 |-  ( ph -> ( ( F ` C ) < ( F ` B ) -> B =/= C ) )
137 136 32 jctild 
 |-  ( ph -> ( ( F ` C ) < ( F ` B ) -> ( C <_ B /\ B =/= C ) ) )
138 22 2 ltlend 
 |-  ( ph -> ( C < B <-> ( C <_ B /\ B =/= C ) ) )
139 137 138 sylibrd 
 |-  ( ph -> ( ( F ` C ) < ( F ` B ) -> C < B ) )
140 131 139 mpd 
 |-  ( ph -> C < B )
141 1 rexrd 
 |-  ( ph -> A e. RR* )
142 2 rexrd 
 |-  ( ph -> B e. RR* )
143 elioo2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> ( C e. RR /\ A < C /\ C < B ) ) )
144 141 142 143 syl2anc 
 |-  ( ph -> ( C e. ( A (,) B ) <-> ( C e. RR /\ A < C /\ C < B ) ) )
145 22 129 140 144 mpbir3and 
 |-  ( ph -> C e. ( A (,) B ) )
146 145 118 jca 
 |-  ( ph -> ( C e. ( A (,) B ) /\ ( F ` C ) = U ) )