Metamath Proof Explorer

Theorem rencldnfilem

Description: Lemma for rencldnfi . (Contributed by Stefan O'Rear, 18-Oct-2014)

Ref Expression
Assertion rencldnfilem 
|- ( ( ( A C_ RR /\ B e. RR /\ ( A =/= (/) /\ -. B e. A ) ) /\ A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x ) -> -. A e. Fin )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( a = c -> ( a = ( abs ` ( b - B ) ) <-> c = ( abs ` ( b - B ) ) ) )
2 1 rexbidv 
 |-  ( a = c -> ( E. b e. A a = ( abs ` ( b - B ) ) <-> E. b e. A c = ( abs ` ( b - B ) ) ) )
3 2 elrab 
 |-  ( c e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } <-> ( c e. RR /\ E. b e. A c = ( abs ` ( b - B ) ) ) )
4 simp-4l 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ c e. RR ) /\ b e. A ) -> A C_ RR )
5 simpr 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ c e. RR ) /\ b e. A ) -> b e. A )
6 4 5 sseldd 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ c e. RR ) /\ b e. A ) -> b e. RR )
7 6 recnd 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ c e. RR ) /\ b e. A ) -> b e. CC )
8 simp-4r 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ c e. RR ) /\ b e. A ) -> B e. RR )
9 8 recnd 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ c e. RR ) /\ b e. A ) -> B e. CC )
10 7 9 subcld 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ c e. RR ) /\ b e. A ) -> ( b - B ) e. CC )
11 simprr 
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) -> -. B e. A )
12 11 ad2antrr 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ c e. RR ) /\ b e. A ) -> -. B e. A )
13 nelneq 
 |-  ( ( b e. A /\ -. B e. A ) -> -. b = B )
14 5 12 13 syl2anc 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ c e. RR ) /\ b e. A ) -> -. b = B )
15 subeq0 
 |-  ( ( b e. CC /\ B e. CC ) -> ( ( b - B ) = 0 <-> b = B ) )
16 15 necon3abid 
 |-  ( ( b e. CC /\ B e. CC ) -> ( ( b - B ) =/= 0 <-> -. b = B ) )
17 7 9 16 syl2anc 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ c e. RR ) /\ b e. A ) -> ( ( b - B ) =/= 0 <-> -. b = B ) )
18 14 17 mpbird 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ c e. RR ) /\ b e. A ) -> ( b - B ) =/= 0 )
19 10 18 absrpcld 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ c e. RR ) /\ b e. A ) -> ( abs ` ( b - B ) ) e. RR+ )
20 eleq1 
 |-  ( c = ( abs ` ( b - B ) ) -> ( c e. RR+ <-> ( abs ` ( b - B ) ) e. RR+ ) )
21 19 20 syl5ibrcom 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ c e. RR ) /\ b e. A ) -> ( c = ( abs ` ( b - B ) ) -> c e. RR+ ) )
22 21 rexlimdva 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ c e. RR ) -> ( E. b e. A c = ( abs ` ( b - B ) ) -> c e. RR+ ) )
23 22 expimpd 
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) -> ( ( c e. RR /\ E. b e. A c = ( abs ` ( b - B ) ) ) -> c e. RR+ ) )
24 3 23 syl5bi 
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) -> ( c e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } -> c e. RR+ ) )
25 24 ssrdv 
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) -> { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } C_ RR+ )
26 25 adantr 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } C_ RR+ )
27 abrexfi 
 |-  ( A e. Fin -> { a | E. b e. A a = ( abs ` ( b - B ) ) } e. Fin )
28 rabssab 
 |-  { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } C_ { a | E. b e. A a = ( abs ` ( b - B ) ) }
29 ssfi 
 |-  ( ( { a | E. b e. A a = ( abs ` ( b - B ) ) } e. Fin /\ { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } C_ { a | E. b e. A a = ( abs ` ( b - B ) ) } ) -> { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } e. Fin )
30 27 28 29 sylancl 
 |-  ( A e. Fin -> { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } e. Fin )
31 30 adantl 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } e. Fin )
32 simplrl 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> A =/= (/) )
33 n0 
 |-  ( A =/= (/) <-> E. y y e. A )
34 32 33 sylib 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> E. y y e. A )
35 simp-4l 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> A C_ RR )
36 simpr 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> y e. A )
37 35 36 sseldd 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> y e. RR )
38 37 recnd 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> y e. CC )
39 simp-4r 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> B e. RR )
40 39 recnd 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> B e. CC )
41 38 40 subcld 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> ( y - B ) e. CC )
42 41 abscld 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> ( abs ` ( y - B ) ) e. RR )
43 eqid 
 |-  ( abs ` ( y - B ) ) = ( abs ` ( y - B ) )
44 fvoveq1 
 |-  ( b = y -> ( abs ` ( b - B ) ) = ( abs ` ( y - B ) ) )
45 44 rspceeqv 
 |-  ( ( y e. A /\ ( abs ` ( y - B ) ) = ( abs ` ( y - B ) ) ) -> E. b e. A ( abs ` ( y - B ) ) = ( abs ` ( b - B ) ) )
46 43 45 mpan2 
 |-  ( y e. A -> E. b e. A ( abs ` ( y - B ) ) = ( abs ` ( b - B ) ) )
47 46 adantl 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> E. b e. A ( abs ` ( y - B ) ) = ( abs ` ( b - B ) ) )
48 eqeq1 
 |-  ( a = ( abs ` ( y - B ) ) -> ( a = ( abs ` ( b - B ) ) <-> ( abs ` ( y - B ) ) = ( abs ` ( b - B ) ) ) )
49 48 rexbidv 
 |-  ( a = ( abs ` ( y - B ) ) -> ( E. b e. A a = ( abs ` ( b - B ) ) <-> E. b e. A ( abs ` ( y - B ) ) = ( abs ` ( b - B ) ) ) )
50 49 elrab 
 |-  ( ( abs ` ( y - B ) ) e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } <-> ( ( abs ` ( y - B ) ) e. RR /\ E. b e. A ( abs ` ( y - B ) ) = ( abs ` ( b - B ) ) ) )
51 42 47 50 sylanbrc 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> ( abs ` ( y - B ) ) e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } )
52 51 ne0d 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } =/= (/) )
53 34 52 exlimddv 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } =/= (/) )
54 ssrab2 
 |-  { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } C_ RR
55 54 a1i 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } C_ RR )
56 gtso 
 |-  `' < Or RR
57 fisupcl 
 |-  ( ( `' < Or RR /\ ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } e. Fin /\ { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } =/= (/) /\ { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } C_ RR ) ) -> sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } )
58 56 57 mpan 
 |-  ( ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } e. Fin /\ { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } =/= (/) /\ { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } C_ RR ) -> sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } )
59 31 53 55 58 syl3anc 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } )
60 26 59 sseldd 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) e. RR+ )
61 54 a1i 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } C_ RR )
62 soss 
 |-  ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } C_ RR -> ( `' < Or RR -> `' < Or { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } ) )
63 54 56 62 mp2 
 |-  `' < Or { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) }
64 63 a1i 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> `' < Or { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } )
65 fisupg 
 |-  ( ( `' < Or { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } /\ { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } e. Fin /\ { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } =/= (/) ) -> E. c e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } ( A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } -. c `' < d /\ A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } ( d `' < c -> E. x e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } d `' < x ) ) )
66 64 31 53 65 syl3anc 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> E. c e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } ( A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } -. c `' < d /\ A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } ( d `' < c -> E. x e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } d `' < x ) ) )
67 elrabi 
 |-  ( c e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } -> c e. RR )
68 elrabi 
 |-  ( d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } -> d e. RR )
69 vex 
 |-  c e. _V
70 vex 
 |-  d e. _V
71 69 70 brcnv 
 |-  ( c `' < d <-> d < c )
72 71 notbii 
 |-  ( -. c `' < d <-> -. d < c )
73 lenlt 
 |-  ( ( c e. RR /\ d e. RR ) -> ( c <_ d <-> -. d < c ) )
74 73 biimprd 
 |-  ( ( c e. RR /\ d e. RR ) -> ( -. d < c -> c <_ d ) )
75 72 74 syl5bi 
 |-  ( ( c e. RR /\ d e. RR ) -> ( -. c `' < d -> c <_ d ) )
76 75 adantll 
 |-  ( ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ c e. RR ) /\ d e. RR ) -> ( -. c `' < d -> c <_ d ) )
77 68 76 sylan2 
 |-  ( ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ c e. RR ) /\ d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } ) -> ( -. c `' < d -> c <_ d ) )
78 77 ralimdva 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ c e. RR ) -> ( A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } -. c `' < d -> A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } c <_ d ) )
79 78 adantrd 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ c e. RR ) -> ( ( A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } -. c `' < d /\ A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } ( d `' < c -> E. x e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } d `' < x ) ) -> A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } c <_ d ) )
80 67 79 sylan2 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ c e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } ) -> ( ( A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } -. c `' < d /\ A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } ( d `' < c -> E. x e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } d `' < x ) ) -> A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } c <_ d ) )
81 80 reximdva 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> ( E. c e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } ( A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } -. c `' < d /\ A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } ( d `' < c -> E. x e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } d `' < x ) ) -> E. c e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } c <_ d ) )
82 66 81 mpd 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> E. c e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } c <_ d )
83 82 adantr 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> E. c e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } c <_ d )
84 lbinfle 
 |-  ( ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } C_ RR /\ E. c e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } A. d e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } c <_ d /\ ( abs ` ( y - B ) ) e. { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } ) -> inf ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , < ) <_ ( abs ` ( y - B ) ) )
85 61 83 51 84 syl3anc 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> inf ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , < ) <_ ( abs ` ( y - B ) ) )
86 df-inf 
 |-  inf ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , < ) = sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < )
87 86 eqcomi 
 |-  sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) = inf ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , < )
88 87 breq1i 
 |-  ( sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) <_ ( abs ` ( y - B ) ) <-> inf ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , < ) <_ ( abs ` ( y - B ) ) )
89 85 88 sylibr 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) <_ ( abs ` ( y - B ) ) )
90 54 59 sselid 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) e. RR )
91 90 adantr 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) e. RR )
92 91 42 lenltd 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> ( sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) <_ ( abs ` ( y - B ) ) <-> -. ( abs ` ( y - B ) ) < sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) ) )
93 89 92 mpbid 
 |-  ( ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) /\ y e. A ) -> -. ( abs ` ( y - B ) ) < sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) )
94 93 ralrimiva 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> A. y e. A -. ( abs ` ( y - B ) ) < sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) )
95 breq2 
 |-  ( x = sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) -> ( ( abs ` ( y - B ) ) < x <-> ( abs ` ( y - B ) ) < sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) ) )
96 95 notbid 
 |-  ( x = sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) -> ( -. ( abs ` ( y - B ) ) < x <-> -. ( abs ` ( y - B ) ) < sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) ) )
97 96 ralbidv 
 |-  ( x = sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) -> ( A. y e. A -. ( abs ` ( y - B ) ) < x <-> A. y e. A -. ( abs ` ( y - B ) ) < sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) ) )
98 97 rspcev 
 |-  ( ( sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) e. RR+ /\ A. y e. A -. ( abs ` ( y - B ) ) < sup ( { a e. RR | E. b e. A a = ( abs ` ( b - B ) ) } , RR , `' < ) ) -> E. x e. RR+ A. y e. A -. ( abs ` ( y - B ) ) < x )
99 60 94 98 syl2anc 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> E. x e. RR+ A. y e. A -. ( abs ` ( y - B ) ) < x )
100 ralnex 
 |-  ( A. y e. A -. ( abs ` ( y - B ) ) < x <-> -. E. y e. A ( abs ` ( y - B ) ) < x )
101 100 rexbii 
 |-  ( E. x e. RR+ A. y e. A -. ( abs ` ( y - B ) ) < x <-> E. x e. RR+ -. E. y e. A ( abs ` ( y - B ) ) < x )
102 rexnal 
 |-  ( E. x e. RR+ -. E. y e. A ( abs ` ( y - B ) ) < x <-> -. A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x )
103 101 102 bitri 
 |-  ( E. x e. RR+ A. y e. A -. ( abs ` ( y - B ) ) < x <-> -. A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x )
104 99 103 sylib 
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) /\ A e. Fin ) -> -. A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x )
105 104 ex 
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ ( A =/= (/) /\ -. B e. A ) ) -> ( A e. Fin -> -. A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x ) )
106 105 3impa 
 |-  ( ( A C_ RR /\ B e. RR /\ ( A =/= (/) /\ -. B e. A ) ) -> ( A e. Fin -> -. A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x ) )
107 106 con2d 
 |-  ( ( A C_ RR /\ B e. RR /\ ( A =/= (/) /\ -. B e. A ) ) -> ( A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x -> -. A e. Fin ) )
108 107 imp 
 |-  ( ( ( A C_ RR /\ B e. RR /\ ( A =/= (/) /\ -. B e. A ) ) /\ A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x ) -> -. A e. Fin )