Metamath Proof Explorer

Theorem lgamucov

Description: The U regions used in the proof of lgamgulm have interiors which cover the entire domain of the Gamma function. (Contributed by Mario Carneiro, 6-Jul-2017)

Ref Expression
Hypotheses lgamucov.u ⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
lgamucov.a ⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
lgamucov.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion lgamucov ( 𝜑 → ∃ 𝑟 ∈ ℕ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lgamucov.u ⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
2 lgamucov.a ⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
3 lgamucov.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
4 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
5 difss ⊢ ( ℤ ∖ ℕ ) ⊆ ℤ
6 3 sszcld ⊢ ( ( ℤ ∖ ℕ ) ⊆ ℤ → ( ℤ ∖ ℕ ) ∈ ( Clsd ‘ 𝐽 ) )
7 3 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
8 7 toponunii ⊢ ℂ = ∪ 𝐽
9 8 cldopn ⊢ ( ( ℤ ∖ ℕ ) ∈ ( Clsd ‘ 𝐽 ) → ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∈ 𝐽 )
10 5 6 9 mp2b ⊢ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∈ 𝐽
11 10 a1i ⊢ ( 𝜑 → ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∈ 𝐽 )
12 3 cnfldtopn ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
13 12 mopni2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∈ 𝐽 ∧ 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) → ∃ 𝑎 ∈ ℝ+ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
14 4 11 2 13 mp3an2i ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ+ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
15 2 eldifad ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) → 𝐴 ∈ ℂ )
17 16 abscld ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) → ( abs ‘ 𝐴 ) ∈ ℝ )
18 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) → 𝑎 ∈ ℝ+ )
19 18 rpred ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) → 𝑎 ∈ ℝ )
20 17 19 readdcld ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) → ( ( abs ‘ 𝐴 ) + 𝑎 ) ∈ ℝ )
21 2re ⊢ 2 ∈ ℝ
22 21 a1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) → 2 ∈ ℝ )
23 22 18 rerpdivcld ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) → ( 2 / 𝑎 ) ∈ ℝ )
24 20 23 readdcld ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) → ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) ∈ ℝ )
25 arch ⊢ ( ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) ∈ ℝ → ∃ 𝑟 ∈ ℕ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 )
26 24 25 syl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) → ∃ 𝑟 ∈ ℕ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 )
27 3 cnfldtop ⊢ 𝐽 ∈ Top
28 27 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) → 𝐽 ∈ Top )
29 1 ssrab3 ⊢ 𝑈 ⊆ ℂ
30 29 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) → 𝑈 ⊆ ℂ )
31 16 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) → 𝐴 ∈ ℂ )
32 18 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) → 𝑎 ∈ ℝ+ )
33 32 rphalfcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) → ( 𝑎 / 2 ) ∈ ℝ+ )
34 33 rpxrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) → ( 𝑎 / 2 ) ∈ ℝ* )
35 12 blopn ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐴 ∈ ℂ ∧ ( 𝑎 / 2 ) ∈ ℝ* ) → ( 𝐴 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ∈ 𝐽 )
36 4 31 34 35 mp3an2i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) → ( 𝐴 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ∈ 𝐽 )
37 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → 𝑥 ∈ ℂ )
38 37 abscld ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( abs ‘ 𝑥 ) ∈ ℝ )
39 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → 𝑟 ∈ ℕ )
40 39 nnred ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → 𝑟 ∈ ℝ )
41 24 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) ∈ ℝ )
42 20 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( ( abs ‘ 𝐴 ) + 𝑎 ) ∈ ℝ )
43 17 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( abs ‘ 𝐴 ) ∈ ℝ )
44 38 43 resubcld ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( ( abs ‘ 𝑥 ) − ( abs ‘ 𝐴 ) ) ∈ ℝ )
45 19 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → 𝑎 ∈ ℝ )
46 45 rehalfcld ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( 𝑎 / 2 ) ∈ ℝ )
47 31 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → 𝐴 ∈ ℂ )
48 37 47 subcld ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( 𝑥 − 𝐴 ) ∈ ℂ )
49 48 abscld ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( abs ‘ ( 𝑥 − 𝐴 ) ) ∈ ℝ )
50 37 47 abs2difd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( ( abs ‘ 𝑥 ) − ( abs ‘ 𝐴 ) ) ≤ ( abs ‘ ( 𝑥 − 𝐴 ) ) )
51 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
52 51 cnmetdval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝐴 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝐴 − 𝑥 ) ) )
53 47 37 52 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( 𝐴 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝐴 − 𝑥 ) ) )
54 47 37 abssubd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( abs ‘ ( 𝐴 − 𝑥 ) ) = ( abs ‘ ( 𝑥 − 𝐴 ) ) )
55 53 54 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( 𝐴 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝑥 − 𝐴 ) ) )
56 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) )
57 55 56 eqbrtrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( abs ‘ ( 𝑥 − 𝐴 ) ) < ( 𝑎 / 2 ) )
58 44 49 46 50 57 lelttrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( ( abs ‘ 𝑥 ) − ( abs ‘ 𝐴 ) ) < ( 𝑎 / 2 ) )
59 32 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → 𝑎 ∈ ℝ+ )
60 rphalflt ⊢ ( 𝑎 ∈ ℝ+ → ( 𝑎 / 2 ) < 𝑎 )
61 59 60 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( 𝑎 / 2 ) < 𝑎 )
62 44 46 45 58 61 lttrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( ( abs ‘ 𝑥 ) − ( abs ‘ 𝐴 ) ) < 𝑎 )
63 38 43 45 ltsubadd2d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( ( ( abs ‘ 𝑥 ) − ( abs ‘ 𝐴 ) ) < 𝑎 ↔ ( abs ‘ 𝑥 ) < ( ( abs ‘ 𝐴 ) + 𝑎 ) ) )
64 62 63 mpbid ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( abs ‘ 𝑥 ) < ( ( abs ‘ 𝐴 ) + 𝑎 ) )
65 2rp ⊢ 2 ∈ ℝ+
66 65 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → 2 ∈ ℝ+ )
67 66 59 rpdivcld ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( 2 / 𝑎 ) ∈ ℝ+ )
68 42 67 ltaddrpd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( ( abs ‘ 𝐴 ) + 𝑎 ) < ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) )
69 38 42 41 64 68 lttrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( abs ‘ 𝑥 ) < ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) )
70 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 )
71 38 41 40 69 70 lttrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( abs ‘ 𝑥 ) < 𝑟 )
72 38 40 71 ltled ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( abs ‘ 𝑥 ) ≤ 𝑟 )
73 39 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑟 ∈ ℕ )
74 73 nnrecred ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 1 / 𝑟 ) ∈ ℝ )
75 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑥 ∈ ℂ )
76 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
77 76 nn0cnd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
78 75 77 addcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 + 𝑘 ) ∈ ℂ )
79 78 abscld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( 𝑥 + 𝑘 ) ) ∈ ℝ )
80 46 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑎 / 2 ) ∈ ℝ )
81 23 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 2 / 𝑎 ) ∈ ℝ )
82 41 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) ∈ ℝ )
83 40 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑟 ∈ ℝ )
84 47 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
85 2 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
86 85 dmgmn0 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ≠ 0 )
87 84 86 absrpcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
88 59 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑎 ∈ ℝ+ )
89 87 88 rpaddcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) + 𝑎 ) ∈ ℝ+ )
90 81 89 ltaddrp2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 2 / 𝑎 ) < ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) )
91 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 )
92 81 82 83 90 91 lttrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 2 / 𝑎 ) < 𝑟 )
93 67 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 2 / 𝑎 ) ∈ ℝ+ )
94 73 nnrpd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑟 ∈ ℝ+ )
95 93 94 ltrecd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 2 / 𝑎 ) < 𝑟 ↔ ( 1 / 𝑟 ) < ( 1 / ( 2 / 𝑎 ) ) ) )
96 92 95 mpbid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 1 / 𝑟 ) < ( 1 / ( 2 / 𝑎 ) ) )
97 2cnd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 2 ∈ ℂ )
98 88 rpcnd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑎 ∈ ℂ )
99 2ne0 ⊢ 2 ≠ 0
100 99 a1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 2 ≠ 0 )
101 88 rpne0d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑎 ≠ 0 )
102 97 98 100 101 recdivd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( 2 / 𝑎 ) ) = ( 𝑎 / 2 ) )
103 96 102 breqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 1 / 𝑟 ) < ( 𝑎 / 2 ) )
104 eldmgm ⊢ ( - 𝑘 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ↔ ( - 𝑘 ∈ ℂ ∧ ¬ - - 𝑘 ∈ ℕ0 ) )
105 104 simprbi ⊢ ( - 𝑘 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ¬ - - 𝑘 ∈ ℕ0 )
106 77 negnegd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → - - 𝑘 = 𝑘 )
107 106 76 eqeltrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → - - 𝑘 ∈ ℕ0 )
108 105 107 nsyl3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ¬ - 𝑘 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
109 4 a1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
110 34 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑎 / 2 ) ∈ ℝ* )
111 77 negcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → - 𝑘 ∈ ℂ )
112 elbl2 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 𝑎 / 2 ) ∈ ℝ* ) ∧ ( 𝑥 ∈ ℂ ∧ - 𝑘 ∈ ℂ ) ) → ( - 𝑘 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ↔ ( 𝑥 ( abs ∘ − ) - 𝑘 ) < ( 𝑎 / 2 ) ) )
113 109 110 75 111 112 syl22anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( - 𝑘 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ↔ ( 𝑥 ( abs ∘ − ) - 𝑘 ) < ( 𝑎 / 2 ) ) )
114 51 cnmetdval ⊢ ( ( 𝑥 ∈ ℂ ∧ - 𝑘 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) - 𝑘 ) = ( abs ‘ ( 𝑥 − - 𝑘 ) ) )
115 75 111 114 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 ( abs ∘ − ) - 𝑘 ) = ( abs ‘ ( 𝑥 − - 𝑘 ) ) )
116 75 77 subnegd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 − - 𝑘 ) = ( 𝑥 + 𝑘 ) )
117 116 fveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( 𝑥 − - 𝑘 ) ) = ( abs ‘ ( 𝑥 + 𝑘 ) ) )
118 115 117 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 ( abs ∘ − ) - 𝑘 ) = ( abs ‘ ( 𝑥 + 𝑘 ) ) )
119 118 breq1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑥 ( abs ∘ − ) - 𝑘 ) < ( 𝑎 / 2 ) ↔ ( abs ‘ ( 𝑥 + 𝑘 ) ) < ( 𝑎 / 2 ) ) )
120 79 80 ltnled ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ‘ ( 𝑥 + 𝑘 ) ) < ( 𝑎 / 2 ) ↔ ¬ ( 𝑎 / 2 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) )
121 113 119 120 3bitrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( - 𝑘 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ↔ ¬ ( 𝑎 / 2 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) )
122 45 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑎 ∈ ℝ )
123 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) )
124 elbl3 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 𝑎 / 2 ) ∈ ℝ* ) ∧ ( 𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ) ) → ( 𝐴 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ↔ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) )
125 109 110 75 84 124 syl22anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ↔ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) )
126 123 125 mpbird ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) )
127 blhalf ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝐴 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ) ) → ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ⊆ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) )
128 109 75 122 126 127 syl22anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ⊆ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) )
129 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) → ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
130 129 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
131 128 130 sstrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
132 131 sseld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( - 𝑘 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) → - 𝑘 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) )
133 121 132 sylbird ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ¬ ( 𝑎 / 2 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) → - 𝑘 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) )
134 108 133 mt3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑎 / 2 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) )
135 74 80 79 103 134 ltletrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 1 / 𝑟 ) < ( abs ‘ ( 𝑥 + 𝑘 ) ) )
136 74 79 135 ltled ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) )
137 136 ralrimiva ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) )
138 72 137 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) ) → ( ( abs ‘ 𝑥 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) )
139 138 ex ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) ∧ 𝑥 ∈ ℂ ) → ( ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) → ( ( abs ‘ 𝑥 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) )
140 139 ss2rabdv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) → { 𝑥 ∈ ℂ ∣ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) } ⊆ { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) } )
141 blval ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐴 ∈ ℂ ∧ ( 𝑎 / 2 ) ∈ ℝ* ) → ( 𝐴 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) = { 𝑥 ∈ ℂ ∣ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) } )
142 4 31 34 141 mp3an2i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) → ( 𝐴 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) = { 𝑥 ∈ ℂ ∣ ( 𝐴 ( abs ∘ − ) 𝑥 ) < ( 𝑎 / 2 ) } )
143 1 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) → 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) } )
144 140 142 143 3sstr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) → ( 𝐴 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ⊆ 𝑈 )
145 8 ssntr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑈 ⊆ ℂ ) ∧ ( ( 𝐴 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ∈ 𝐽 ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ⊆ 𝑈 ) ) → ( 𝐴 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑈 ) )
146 28 30 36 144 145 syl22anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) → ( 𝐴 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑈 ) )
147 blcntr ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐴 ∈ ℂ ∧ ( 𝑎 / 2 ) ∈ ℝ+ ) → 𝐴 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) )
148 4 31 33 147 mp3an2i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) → 𝐴 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) ( 𝑎 / 2 ) ) )
149 146 148 sseldd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) ∧ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 ) → 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑈 ) )
150 149 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) ∧ 𝑟 ∈ ℕ ) → ( ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 → 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑈 ) ) )
151 150 reximdva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) → ( ∃ 𝑟 ∈ ℕ ( ( ( abs ‘ 𝐴 ) + 𝑎 ) + ( 2 / 𝑎 ) ) < 𝑟 → ∃ 𝑟 ∈ ℕ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑈 ) ) )
152 26 151 mpd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑎 ) ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) ) → ∃ 𝑟 ∈ ℕ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑈 ) )
153 14 152 rexlimddv ⊢ ( 𝜑 → ∃ 𝑟 ∈ ℕ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑈 ) )