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 ⊒ 𝐽 = ( TopOpen β€˜ β„‚fld )
reperflem.2 ⊒ ( ( 𝑒 ∈ 𝑆 ∧ 𝑣 ∈ ℝ ) β†’ ( 𝑒 + 𝑣 ) ∈ 𝑆 )
reperflem.3 ⊒ 𝑆 βŠ† β„‚
Assertion reperflem ( 𝐽 β†Ύt 𝑆 ) ∈ Perf

Proof

Step Hyp Ref Expression
1 recld2.1 ⊒ 𝐽 = ( TopOpen β€˜ β„‚fld )
2 reperflem.2 ⊒ ( ( 𝑒 ∈ 𝑆 ∧ 𝑣 ∈ ℝ ) β†’ ( 𝑒 + 𝑣 ) ∈ 𝑆 )
3 reperflem.3 ⊒ 𝑆 βŠ† β„‚
4 cnxmet ⊒ ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ )
5 3 sseli ⊒ ( 𝑒 ∈ 𝑆 β†’ 𝑒 ∈ β„‚ )
6 1 cnfldtopn ⊒ 𝐽 = ( MetOpen β€˜ ( abs ∘ βˆ’ ) )
7 6 neibl ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 𝑒 ∈ β„‚ ) β†’ ( 𝑛 ∈ ( ( nei β€˜ 𝐽 ) β€˜ { 𝑒 } ) ↔ ( 𝑛 βŠ† β„‚ ∧ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) βŠ† 𝑛 ) ) )
8 4 5 7 sylancr ⊒ ( 𝑒 ∈ 𝑆 β†’ ( 𝑛 ∈ ( ( nei β€˜ 𝐽 ) β€˜ { 𝑒 } ) ↔ ( 𝑛 βŠ† β„‚ ∧ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) βŠ† 𝑛 ) ) )
9 ssrin ⊒ ( ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) βŠ† 𝑛 β†’ ( ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) ∩ ( 𝑆 βˆ– { 𝑒 } ) ) βŠ† ( 𝑛 ∩ ( 𝑆 βˆ– { 𝑒 } ) ) )
10 2 ralrimiva ⊒ ( 𝑒 ∈ 𝑆 β†’ βˆ€ 𝑣 ∈ ℝ ( 𝑒 + 𝑣 ) ∈ 𝑆 )
11 rpre ⊒ ( π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ )
12 11 rehalfcld ⊒ ( π‘Ÿ ∈ ℝ+ β†’ ( π‘Ÿ / 2 ) ∈ ℝ )
13 oveq2 ⊒ ( 𝑣 = ( π‘Ÿ / 2 ) β†’ ( 𝑒 + 𝑣 ) = ( 𝑒 + ( π‘Ÿ / 2 ) ) )
14 13 eleq1d ⊒ ( 𝑣 = ( π‘Ÿ / 2 ) β†’ ( ( 𝑒 + 𝑣 ) ∈ 𝑆 ↔ ( 𝑒 + ( π‘Ÿ / 2 ) ) ∈ 𝑆 ) )
15 14 rspccva ⊒ ( ( βˆ€ 𝑣 ∈ ℝ ( 𝑒 + 𝑣 ) ∈ 𝑆 ∧ ( π‘Ÿ / 2 ) ∈ ℝ ) β†’ ( 𝑒 + ( π‘Ÿ / 2 ) ) ∈ 𝑆 )
16 10 12 15 syl2an ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑒 + ( π‘Ÿ / 2 ) ) ∈ 𝑆 )
17 3 16 sselid ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑒 + ( π‘Ÿ / 2 ) ) ∈ β„‚ )
18 5 adantr ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝑒 ∈ β„‚ )
19 eqid ⊒ ( abs ∘ βˆ’ ) = ( abs ∘ βˆ’ )
20 19 cnmetdval ⊒ ( ( ( 𝑒 + ( π‘Ÿ / 2 ) ) ∈ β„‚ ∧ 𝑒 ∈ β„‚ ) β†’ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) ( abs ∘ βˆ’ ) 𝑒 ) = ( abs β€˜ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) βˆ’ 𝑒 ) ) )
21 17 18 20 syl2anc ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) ( abs ∘ βˆ’ ) 𝑒 ) = ( abs β€˜ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) βˆ’ 𝑒 ) ) )
22 simpr ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ π‘Ÿ ∈ ℝ+ )
23 22 rphalfcld ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( π‘Ÿ / 2 ) ∈ ℝ+ )
24 23 rpcnd ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( π‘Ÿ / 2 ) ∈ β„‚ )
25 18 24 pncan2d ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) βˆ’ 𝑒 ) = ( π‘Ÿ / 2 ) )
26 25 fveq2d ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( abs β€˜ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) βˆ’ 𝑒 ) ) = ( abs β€˜ ( π‘Ÿ / 2 ) ) )
27 23 rpred ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( π‘Ÿ / 2 ) ∈ ℝ )
28 23 rpge0d ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ 0 ≀ ( π‘Ÿ / 2 ) )
29 27 28 absidd ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( abs β€˜ ( π‘Ÿ / 2 ) ) = ( π‘Ÿ / 2 ) )
30 21 26 29 3eqtrd ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) ( abs ∘ βˆ’ ) 𝑒 ) = ( π‘Ÿ / 2 ) )
31 rphalflt ⊒ ( π‘Ÿ ∈ ℝ+ β†’ ( π‘Ÿ / 2 ) < π‘Ÿ )
32 31 adantl ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( π‘Ÿ / 2 ) < π‘Ÿ )
33 30 32 eqbrtrd ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) ( abs ∘ βˆ’ ) 𝑒 ) < π‘Ÿ )
34 4 a1i ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) )
35 rpxr ⊒ ( π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ* )
36 35 adantl ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ π‘Ÿ ∈ ℝ* )
37 elbl3 ⊒ ( ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ π‘Ÿ ∈ ℝ* ) ∧ ( 𝑒 ∈ β„‚ ∧ ( 𝑒 + ( π‘Ÿ / 2 ) ) ∈ β„‚ ) ) β†’ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) ∈ ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) ↔ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) ( abs ∘ βˆ’ ) 𝑒 ) < π‘Ÿ ) )
38 34 36 18 17 37 syl22anc ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) ∈ ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) ↔ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) ( abs ∘ βˆ’ ) 𝑒 ) < π‘Ÿ ) )
39 33 38 mpbird ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑒 + ( π‘Ÿ / 2 ) ) ∈ ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) )
40 23 rpne0d ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( π‘Ÿ / 2 ) β‰  0 )
41 25 40 eqnetrd ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) βˆ’ 𝑒 ) β‰  0 )
42 17 18 41 subne0ad ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑒 + ( π‘Ÿ / 2 ) ) β‰  𝑒 )
43 eldifsn ⊒ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) ∈ ( 𝑆 βˆ– { 𝑒 } ) ↔ ( ( 𝑒 + ( π‘Ÿ / 2 ) ) ∈ 𝑆 ∧ ( 𝑒 + ( π‘Ÿ / 2 ) ) β‰  𝑒 ) )
44 16 42 43 sylanbrc ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑒 + ( π‘Ÿ / 2 ) ) ∈ ( 𝑆 βˆ– { 𝑒 } ) )
45 inelcm ⊒ ( ( ( 𝑒 + ( π‘Ÿ / 2 ) ) ∈ ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) ∧ ( 𝑒 + ( π‘Ÿ / 2 ) ) ∈ ( 𝑆 βˆ– { 𝑒 } ) ) β†’ ( ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) ∩ ( 𝑆 βˆ– { 𝑒 } ) ) β‰  βˆ… )
46 39 44 45 syl2anc ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) ∩ ( 𝑆 βˆ– { 𝑒 } ) ) β‰  βˆ… )
47 ssn0 ⊒ ( ( ( ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) ∩ ( 𝑆 βˆ– { 𝑒 } ) ) βŠ† ( 𝑛 ∩ ( 𝑆 βˆ– { 𝑒 } ) ) ∧ ( ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) ∩ ( 𝑆 βˆ– { 𝑒 } ) ) β‰  βˆ… ) β†’ ( 𝑛 ∩ ( 𝑆 βˆ– { 𝑒 } ) ) β‰  βˆ… )
48 47 ex ⊒ ( ( ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) ∩ ( 𝑆 βˆ– { 𝑒 } ) ) βŠ† ( 𝑛 ∩ ( 𝑆 βˆ– { 𝑒 } ) ) β†’ ( ( ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) ∩ ( 𝑆 βˆ– { 𝑒 } ) ) β‰  βˆ… β†’ ( 𝑛 ∩ ( 𝑆 βˆ– { 𝑒 } ) ) β‰  βˆ… ) )
49 9 46 48 syl2imc ⊒ ( ( 𝑒 ∈ 𝑆 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) βŠ† 𝑛 β†’ ( 𝑛 ∩ ( 𝑆 βˆ– { 𝑒 } ) ) β‰  βˆ… ) )
50 49 rexlimdva ⊒ ( 𝑒 ∈ 𝑆 β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) βŠ† 𝑛 β†’ ( 𝑛 ∩ ( 𝑆 βˆ– { 𝑒 } ) ) β‰  βˆ… ) )
51 50 adantld ⊒ ( 𝑒 ∈ 𝑆 β†’ ( ( 𝑛 βŠ† β„‚ ∧ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑒 ( ball β€˜ ( abs ∘ βˆ’ ) ) π‘Ÿ ) βŠ† 𝑛 ) β†’ ( 𝑛 ∩ ( 𝑆 βˆ– { 𝑒 } ) ) β‰  βˆ… ) )
52 8 51 sylbid ⊒ ( 𝑒 ∈ 𝑆 β†’ ( 𝑛 ∈ ( ( nei β€˜ 𝐽 ) β€˜ { 𝑒 } ) β†’ ( 𝑛 ∩ ( 𝑆 βˆ– { 𝑒 } ) ) β‰  βˆ… ) )
53 52 ralrimiv ⊒ ( 𝑒 ∈ 𝑆 β†’ βˆ€ 𝑛 ∈ ( ( nei β€˜ 𝐽 ) β€˜ { 𝑒 } ) ( 𝑛 ∩ ( 𝑆 βˆ– { 𝑒 } ) ) β‰  βˆ… )
54 1 cnfldtop ⊒ 𝐽 ∈ Top
55 1 cnfldtopon ⊒ 𝐽 ∈ ( TopOn β€˜ β„‚ )
56 55 toponunii ⊒ β„‚ = βˆͺ 𝐽
57 56 islp2 ⊒ ( ( 𝐽 ∈ Top ∧ 𝑆 βŠ† β„‚ ∧ 𝑒 ∈ β„‚ ) β†’ ( 𝑒 ∈ ( ( limPt β€˜ 𝐽 ) β€˜ 𝑆 ) ↔ βˆ€ 𝑛 ∈ ( ( nei β€˜ 𝐽 ) β€˜ { 𝑒 } ) ( 𝑛 ∩ ( 𝑆 βˆ– { 𝑒 } ) ) β‰  βˆ… ) )
58 54 3 5 57 mp3an12i ⊒ ( 𝑒 ∈ 𝑆 β†’ ( 𝑒 ∈ ( ( limPt β€˜ 𝐽 ) β€˜ 𝑆 ) ↔ βˆ€ 𝑛 ∈ ( ( nei β€˜ 𝐽 ) β€˜ { 𝑒 } ) ( 𝑛 ∩ ( 𝑆 βˆ– { 𝑒 } ) ) β‰  βˆ… ) )
59 53 58 mpbird ⊒ ( 𝑒 ∈ 𝑆 β†’ 𝑒 ∈ ( ( limPt β€˜ 𝐽 ) β€˜ 𝑆 ) )
60 59 ssriv ⊒ 𝑆 βŠ† ( ( limPt β€˜ 𝐽 ) β€˜ 𝑆 )
61 eqid ⊒ ( 𝐽 β†Ύt 𝑆 ) = ( 𝐽 β†Ύt 𝑆 )
62 56 61 restperf ⊒ ( ( 𝐽 ∈ Top ∧ 𝑆 βŠ† β„‚ ) β†’ ( ( 𝐽 β†Ύt 𝑆 ) ∈ Perf ↔ 𝑆 βŠ† ( ( limPt β€˜ 𝐽 ) β€˜ 𝑆 ) ) )
63 54 3 62 mp2an ⊒ ( ( 𝐽 β†Ύt 𝑆 ) ∈ Perf ↔ 𝑆 βŠ† ( ( limPt β€˜ 𝐽 ) β€˜ 𝑆 ) )
64 60 63 mpbir ⊒ ( 𝐽 β†Ύt 𝑆 ) ∈ Perf