Metamath Proof Explorer

Theorem rencldnfi

Description: A set of real numbers which comes arbitrarily close to some target yet excludes it is infinite. The work is done in rencldnfilem using infima; this theorem removes the requirement that A be nonempty. (Contributed by Stefan O'Rear, 19-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A C_ RR /\ B e. RR /\ -. B e. A ) /\ A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x ) -> A C_ RR )
2 simpl2 
 |-  ( ( ( A C_ RR /\ B e. RR /\ -. B e. A ) /\ A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x ) -> B e. RR )
3 rexn0 
 |-  ( E. y e. A ( abs ` ( y - B ) ) < x -> A =/= (/) )
4 3 ralimi 
 |-  ( A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x -> A. x e. RR+ A =/= (/) )
5 1rp 
 |-  1 e. RR+
6 ne0i 
 |-  ( 1 e. RR+ -> RR+ =/= (/) )
7 r19.3rzv 
 |-  ( RR+ =/= (/) -> ( A =/= (/) <-> A. x e. RR+ A =/= (/) ) )
8 5 6 7 mp2b 
 |-  ( A =/= (/) <-> A. x e. RR+ A =/= (/) )
9 4 8 sylibr 
 |-  ( A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x -> A =/= (/) )
10 9 adantl 
 |-  ( ( ( A C_ RR /\ B e. RR /\ -. B e. A ) /\ A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x ) -> A =/= (/) )
11 simpl3 
 |-  ( ( ( A C_ RR /\ B e. RR /\ -. B e. A ) /\ A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x ) -> -. B e. A )
12 10 11 jca 
 |-  ( ( ( A C_ RR /\ B e. RR /\ -. B e. A ) /\ A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x ) -> ( A =/= (/) /\ -. B e. A ) )
13 simpr 
 |-  ( ( ( A C_ RR /\ B e. RR /\ -. B e. A ) /\ A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x ) -> A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x )
14 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 )
15 1 2 12 13 14 syl31anc 
 |-  ( ( ( A C_ RR /\ B e. RR /\ -. B e. A ) /\ A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x ) -> -. A e. Fin )