Metamath Proof Explorer

Theorem reperflem

Description: A subset of the real numbers that is closed under addition with real numbers is perfect. (Contributed by Mario Carneiro, 26-Dec-2016)

Ref Expression
Hypotheses recld2.1 
|- J = ( TopOpen ` CCfld )
reperflem.2 
|- ( ( u e. S /\ v e. RR ) -> ( u + v ) e. S )
reperflem.3 
|- S C_ CC
Assertion reperflem 
|- ( J |`t S ) e. Perf

Proof

Step Hyp Ref Expression
1 recld2.1 
 |-  J = ( TopOpen ` CCfld )
2 reperflem.2 
 |-  ( ( u e. S /\ v e. RR ) -> ( u + v ) e. S )
3 reperflem.3 
 |-  S C_ CC
4 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
5 3 sseli 
 |-  ( u e. S -> u e. CC )
6 1 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
7 6 neibl 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ u e. CC ) -> ( n e. ( ( nei ` J ) ` { u } ) <-> ( n C_ CC /\ E. r e. RR+ ( u ( ball ` ( abs o. - ) ) r ) C_ n ) ) )
8 4 5 7 sylancr 
 |-  ( u e. S -> ( n e. ( ( nei ` J ) ` { u } ) <-> ( n C_ CC /\ E. r e. RR+ ( u ( ball ` ( abs o. - ) ) r ) C_ n ) ) )
9 ssrin 
 |-  ( ( u ( ball ` ( abs o. - ) ) r ) C_ n -> ( ( u ( ball ` ( abs o. - ) ) r ) i^i ( S \ { u } ) ) C_ ( n i^i ( S \ { u } ) ) )
10 2 ralrimiva 
 |-  ( u e. S -> A. v e. RR ( u + v ) e. S )
11 rpre 
 |-  ( r e. RR+ -> r e. RR )
12 11 rehalfcld 
 |-  ( r e. RR+ -> ( r / 2 ) e. RR )
13 oveq2 
 |-  ( v = ( r / 2 ) -> ( u + v ) = ( u + ( r / 2 ) ) )
14 13 eleq1d 
 |-  ( v = ( r / 2 ) -> ( ( u + v ) e. S <-> ( u + ( r / 2 ) ) e. S ) )
15 14 rspccva 
 |-  ( ( A. v e. RR ( u + v ) e. S /\ ( r / 2 ) e. RR ) -> ( u + ( r / 2 ) ) e. S )
16 10 12 15 syl2an 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( u + ( r / 2 ) ) e. S )
17 3 16 sselid 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( u + ( r / 2 ) ) e. CC )
18 5 adantr 
 |-  ( ( u e. S /\ r e. RR+ ) -> u e. CC )
19 eqid 
 |-  ( abs o. - ) = ( abs o. - )
20 19 cnmetdval 
 |-  ( ( ( u + ( r / 2 ) ) e. CC /\ u e. CC ) -> ( ( u + ( r / 2 ) ) ( abs o. - ) u ) = ( abs ` ( ( u + ( r / 2 ) ) - u ) ) )
21 17 18 20 syl2anc 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( ( u + ( r / 2 ) ) ( abs o. - ) u ) = ( abs ` ( ( u + ( r / 2 ) ) - u ) ) )
22 simpr 
 |-  ( ( u e. S /\ r e. RR+ ) -> r e. RR+ )
23 22 rphalfcld 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( r / 2 ) e. RR+ )
24 23 rpcnd 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( r / 2 ) e. CC )
25 18 24 pncan2d 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( ( u + ( r / 2 ) ) - u ) = ( r / 2 ) )
26 25 fveq2d 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( abs ` ( ( u + ( r / 2 ) ) - u ) ) = ( abs ` ( r / 2 ) ) )
27 23 rpred 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( r / 2 ) e. RR )
28 23 rpge0d 
 |-  ( ( u e. S /\ r e. RR+ ) -> 0 <_ ( r / 2 ) )
29 27 28 absidd 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( abs ` ( r / 2 ) ) = ( r / 2 ) )
30 21 26 29 3eqtrd 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( ( u + ( r / 2 ) ) ( abs o. - ) u ) = ( r / 2 ) )
31 rphalflt 
 |-  ( r e. RR+ -> ( r / 2 ) < r )
32 31 adantl 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( r / 2 ) < r )
33 30 32 eqbrtrd 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( ( u + ( r / 2 ) ) ( abs o. - ) u ) < r )
34 4 a1i 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( abs o. - ) e. ( *Met ` CC ) )
35 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
36 35 adantl 
 |-  ( ( u e. S /\ r e. RR+ ) -> r e. RR* )
37 elbl3 
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ r e. RR* ) /\ ( u e. CC /\ ( u + ( r / 2 ) ) e. CC ) ) -> ( ( u + ( r / 2 ) ) e. ( u ( ball ` ( abs o. - ) ) r ) <-> ( ( u + ( r / 2 ) ) ( abs o. - ) u ) < r ) )
38 34 36 18 17 37 syl22anc 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( ( u + ( r / 2 ) ) e. ( u ( ball ` ( abs o. - ) ) r ) <-> ( ( u + ( r / 2 ) ) ( abs o. - ) u ) < r ) )
39 33 38 mpbird 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( u + ( r / 2 ) ) e. ( u ( ball ` ( abs o. - ) ) r ) )
40 23 rpne0d 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( r / 2 ) =/= 0 )
41 25 40 eqnetrd 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( ( u + ( r / 2 ) ) - u ) =/= 0 )
42 17 18 41 subne0ad 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( u + ( r / 2 ) ) =/= u )
43 eldifsn 
 |-  ( ( u + ( r / 2 ) ) e. ( S \ { u } ) <-> ( ( u + ( r / 2 ) ) e. S /\ ( u + ( r / 2 ) ) =/= u ) )
44 16 42 43 sylanbrc 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( u + ( r / 2 ) ) e. ( S \ { u } ) )
45 inelcm 
 |-  ( ( ( u + ( r / 2 ) ) e. ( u ( ball ` ( abs o. - ) ) r ) /\ ( u + ( r / 2 ) ) e. ( S \ { u } ) ) -> ( ( u ( ball ` ( abs o. - ) ) r ) i^i ( S \ { u } ) ) =/= (/) )
46 39 44 45 syl2anc 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( ( u ( ball ` ( abs o. - ) ) r ) i^i ( S \ { u } ) ) =/= (/) )
47 ssn0 
 |-  ( ( ( ( u ( ball ` ( abs o. - ) ) r ) i^i ( S \ { u } ) ) C_ ( n i^i ( S \ { u } ) ) /\ ( ( u ( ball ` ( abs o. - ) ) r ) i^i ( S \ { u } ) ) =/= (/) ) -> ( n i^i ( S \ { u } ) ) =/= (/) )
48 47 ex 
 |-  ( ( ( u ( ball ` ( abs o. - ) ) r ) i^i ( S \ { u } ) ) C_ ( n i^i ( S \ { u } ) ) -> ( ( ( u ( ball ` ( abs o. - ) ) r ) i^i ( S \ { u } ) ) =/= (/) -> ( n i^i ( S \ { u } ) ) =/= (/) ) )
49 9 46 48 syl2imc 
 |-  ( ( u e. S /\ r e. RR+ ) -> ( ( u ( ball ` ( abs o. - ) ) r ) C_ n -> ( n i^i ( S \ { u } ) ) =/= (/) ) )
50 49 rexlimdva 
 |-  ( u e. S -> ( E. r e. RR+ ( u ( ball ` ( abs o. - ) ) r ) C_ n -> ( n i^i ( S \ { u } ) ) =/= (/) ) )
51 50 adantld 
 |-  ( u e. S -> ( ( n C_ CC /\ E. r e. RR+ ( u ( ball ` ( abs o. - ) ) r ) C_ n ) -> ( n i^i ( S \ { u } ) ) =/= (/) ) )
52 8 51 sylbid 
 |-  ( u e. S -> ( n e. ( ( nei ` J ) ` { u } ) -> ( n i^i ( S \ { u } ) ) =/= (/) ) )
53 52 ralrimiv 
 |-  ( u e. S -> A. n e. ( ( nei ` J ) ` { u } ) ( n i^i ( S \ { u } ) ) =/= (/) )
54 1 cnfldtop 
 |-  J e. Top
55 1 cnfldtopon 
 |-  J e. ( TopOn ` CC )
56 55 toponunii 
 |-  CC = U. J
57 56 islp2 
 |-  ( ( J e. Top /\ S C_ CC /\ u e. CC ) -> ( u e. ( ( limPt ` J ) ` S ) <-> A. n e. ( ( nei ` J ) ` { u } ) ( n i^i ( S \ { u } ) ) =/= (/) ) )
58 54 3 5 57 mp3an12i 
 |-  ( u e. S -> ( u e. ( ( limPt ` J ) ` S ) <-> A. n e. ( ( nei ` J ) ` { u } ) ( n i^i ( S \ { u } ) ) =/= (/) ) )
59 53 58 mpbird 
 |-  ( u e. S -> u e. ( ( limPt ` J ) ` S ) )
60 59 ssriv 
 |-  S C_ ( ( limPt ` J ) ` S )
61 eqid 
 |-  ( J |`t S ) = ( J |`t S )
62 56 61 restperf 
 |-  ( ( J e. Top /\ S C_ CC ) -> ( ( J |`t S ) e. Perf <-> S C_ ( ( limPt ` J ) ` S ) ) )
63 54 3 62 mp2an 
 |-  ( ( J |`t S ) e. Perf <-> S C_ ( ( limPt ` J ) ` S ) )
64 60 63 mpbir 
 |-  ( J |`t S ) e. Perf