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 AB¬BAx+yAyB<x¬AFin

Proof

Step Hyp Ref Expression
1 simpl1 AB¬BAx+yAyB<xA
2 simpl2 AB¬BAx+yAyB<xB
3 rexn0 yAyB<xA
4 3 ralimi x+yAyB<xx+A
5 1rp 1+
6 ne0i 1++
7 r19.3rzv +Ax+A
8 5 6 7 mp2b Ax+A
9 4 8 sylibr x+yAyB<xA
10 9 adantl AB¬BAx+yAyB<xA
11 simpl3 AB¬BAx+yAyB<x¬BA
12 10 11 jca AB¬BAx+yAyB<xA¬BA
13 simpr AB¬BAx+yAyB<xx+yAyB<x
14 rencldnfilem ABA¬BAx+yAyB<x¬AFin
15 1 2 12 13 14 syl31anc AB¬BAx+yAyB<x¬AFin