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