lgamucov - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lgamucov		Structured version Visualization version GIF version

Theorem lgamucov 27005

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

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

**Assertion**
Ref	Expression
lgamucov	⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))

Distinct variable groups: 𝑘,𝑟,𝑥,𝐴 𝜑,𝑘,𝑟,𝑥 Allowed substitution hints: 𝑈(𝑥,𝑘,𝑟) 𝐽(𝑥,𝑘,𝑟)

Proof of Theorem lgamucov Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnxmet 24716	. . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
2		difss 4116	. . . . 5 ⊢ (ℤ ∖ ℕ) ⊆ ℤ
3		lgamucov.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
4	3	sszcld 24762	. . . . 5 ⊢ ((ℤ ∖ ℕ) ⊆ ℤ → (ℤ ∖ ℕ) ∈ (Clsd‘𝐽))
5	3	cnfldtopon 24726	. . . . . . 7 ⊢ 𝐽 ∈ (TopOn‘ℂ)
6	5	toponunii 22859	. . . . . 6 ⊢ ℂ = ∪ 𝐽
7	6	cldopn 22974	. . . . 5 ⊢ ((ℤ ∖ ℕ) ∈ (Clsd‘𝐽) → (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽)
8	2, 4, 7	mp2b 10	. . . 4 ⊢ (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽
9	8	a1i 11	. . 3 ⊢ (𝜑 → (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽)
10		lgamucov.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
11	3	cnfldtopn 24725	. . . 4 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
12	11	mopni2 24437	. . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽 ∧ 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) → ∃𝑎 ∈ ℝ⁺ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
13	1, 9, 10, 12	mp3an2i 1468	. 2 ⊢ (𝜑 → ∃𝑎 ∈ ℝ⁺ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
14	10	eldifad 3943	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
15	14	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝐴 ∈ ℂ)
16	15	abscld 15460	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (abs‘𝐴) ∈ ℝ)
17		simprl 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ⁺)
18	17	rpred 13056	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ)
19	16, 18	readdcld 11269	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ((abs‘𝐴) + 𝑎) ∈ ℝ)
20		2re 12319	. . . . . . 7 ⊢ 2 ∈ ℝ
21	20	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 2 ∈ ℝ)
22	21, 17	rerpdivcld 13087	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (2 / 𝑎) ∈ ℝ)
23	19, 22	readdcld 11269	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ)
24		arch 12503	. . . 4 ⊢ ((((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ → ∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
25	23, 24	syl 17	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
26	3	cnfldtop 24727	. . . . . . . 8 ⊢ 𝐽 ∈ Top
27	26	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐽 ∈ Top)
28		lgamucov.u	. . . . . . . . 9 ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}
29	28	ssrab3 4062	. . . . . . . 8 ⊢ 𝑈 ⊆ ℂ
30	29	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑈 ⊆ ℂ)
31	15	ad2antrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ℂ)
32	17	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑎 ∈ ℝ⁺)
33	32	rphalfcld 13068	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈ ℝ⁺)
34	33	rpxrd 13057	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈ ℝ^*)
35	11	blopn 24444	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ^*) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽)
36	1, 31, 34, 35	mp3an2i 1468	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽)
37		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑥 ∈ ℂ)
38	37	abscld 15460	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ∈ ℝ)
39		simp-4r 783	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℕ)
40	39	nnred 12260	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℝ)
41	23	ad4antr 732	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ)
42	19	ad4antr 732	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) ∈ ℝ)
43	16	ad4antr 732	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝐴) ∈ ℝ)
44	38, 43	resubcld 11670	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ∈ ℝ)
45	18	ad4antr 732	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ)
46	45	rehalfcld 12493	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) ∈ ℝ)
47	31	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝐴 ∈ ℂ)
48	37, 47	subcld 11599	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑥 − 𝐴) ∈ ℂ)
49	48	abscld 15460	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) ∈ ℝ)
50	37, 47	abs2difd 15481	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ≤ (abs‘(𝑥 − 𝐴)))
51		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs ∘ − ) = (abs ∘ − )
52	51	cnmetdval 24714	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥)))
53	47, 37, 52	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥)))
54	47, 37	abssubd 15477	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝐴 − 𝑥)) = (abs‘(𝑥 − 𝐴)))
55	53, 54	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝑥 − 𝐴)))
56		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2))
57	55, 56	eqbrtrrd 5148	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) < (𝑎 / 2))
58	44, 49, 46, 50, 57	lelttrd 11398	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < (𝑎 / 2))
59	32	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ⁺)
60		rphalflt 13043	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ℝ⁺ → (𝑎 / 2) < 𝑎)
61	59, 60	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) < 𝑎)
62	44, 46, 45, 58, 61	lttrd 11401	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < 𝑎)
63	38, 43, 45	ltsubadd2d 11840	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝑥) − (abs‘𝐴)) < 𝑎 ↔ (abs‘𝑥) < ((abs‘𝐴) + 𝑎)))
64	62, 63	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < ((abs‘𝐴) + 𝑎))
65		2rp 13018	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ⁺
66	65	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 2 ∈ ℝ⁺)
67	66, 59	rpdivcld 13073	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (2 / 𝑎) ∈ ℝ⁺)
68	42, 67	ltaddrpd 13089	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎)))
69	38, 42, 41, 64, 68	lttrd 11401	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎)))
70		simpllr 775	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
71	38, 41, 40, 69, 70	lttrd 11401	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < 𝑟)
72	38, 40, 71	ltled 11388	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ≤ 𝑟)
73	39	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑟 ∈ ℕ)
74	73	nnrecred 12296	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) ∈ ℝ)
75		simpllr 775	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑥 ∈ ℂ)
76		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
77	76	nn0cnd 12569	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℂ)
78	75, 77	addcld 11259	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥 + 𝑘) ∈ ℂ)
79	78	abscld 15460	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝑥 + 𝑘)) ∈ ℝ)
80	46	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑎 / 2) ∈ ℝ)
81	22	ad5antr 734	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) ∈ ℝ)
82	41	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ)
83	40	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑟 ∈ ℝ)
84	47	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ∈ ℂ)
85	10	ad6antr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
86	85	dmgmn0 26993	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ≠ 0)
87	84, 86	absrpcld 15472	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ⁺)
88	59	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ∈ ℝ⁺)
89	87, 88	rpaddcld 13071	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((abs‘𝐴) + 𝑎) ∈ ℝ⁺)
90	81, 89	ltaddrp2d 13090	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎)))
91		simp-4r 783	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
92	81, 82, 83, 90, 91	lttrd 11401	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) < 𝑟)
93	67	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) ∈ ℝ⁺)
94	73	nnrpd 13054	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑟 ∈ ℝ⁺)
95	93, 94	ltrecd 13074	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((2 / 𝑎) < 𝑟 ↔ (1 / 𝑟) < (1 / (2 / 𝑎))))
96	92, 95	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) < (1 / (2 / 𝑎)))
97		2cnd 12323	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 2 ∈ ℂ)
98	88	rpcnd 13058	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ∈ ℂ)
99		2ne0 12349	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
100	99	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 2 ≠ 0)
101	88	rpne0d 13061	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ≠ 0)
102	97, 98, 100, 101	recdivd 12039	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / (2 / 𝑎)) = (𝑎 / 2))
103	96, 102	breqtrd 5150	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) < (𝑎 / 2))
104		eldmgm 26989	. . . . . . . . . . . . . . . . 17 ⊢ (-𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↔ (-𝑘 ∈ ℂ ∧ ¬ --𝑘 ∈ ℕ₀))
105	104	simprbi 496	. . . . . . . . . . . . . . . 16 ⊢ (-𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → ¬ --𝑘 ∈ ℕ₀)
106	77	negnegd 11590	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → --𝑘 = 𝑘)
107	106, 76	eqeltrd 2835	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → --𝑘 ∈ ℕ₀)
108	105, 107	nsyl3 138	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ¬ -𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
109	1	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs ∘ − ) ∈ (∞Met‘ℂ))
110	34	ad3antrrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑎 / 2) ∈ ℝ^*)
111	77	negcld 11586	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → -𝑘 ∈ ℂ)
112		elbl2 24334	. . . . . . . . . . . . . . . . . 18 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑥 ∈ ℂ ∧ -𝑘 ∈ ℂ)) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝑥(abs ∘ − )-𝑘) < (𝑎 / 2)))
113	109, 110, 75, 111, 112	syl22anc 838	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝑥(abs ∘ − )-𝑘) < (𝑎 / 2)))
114	51	cnmetdval 24714	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ∧ -𝑘 ∈ ℂ) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘)))
115	75, 111, 114	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘)))
116	75, 77	subnegd 11606	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥 − -𝑘) = (𝑥 + 𝑘))
117	116	fveq2d 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝑥 − -𝑘)) = (abs‘(𝑥 + 𝑘)))
118	115, 117	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 + 𝑘)))
119	118	breq1d 5134	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((𝑥(abs ∘ − )-𝑘) < (𝑎 / 2) ↔ (abs‘(𝑥 + 𝑘)) < (𝑎 / 2)))
120	79, 80	ltnled 11387	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((abs‘(𝑥 + 𝑘)) < (𝑎 / 2) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘))))
121	113, 119, 120	3bitrd 305	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘))))
122	45	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ∈ ℝ)
123		simplr 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2))
124		elbl3 24336	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ)) → (𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)))
125	109, 110, 75, 84, 124	syl22anc 838	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)))
126	123, 125	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)))
127		blhalf 24349	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ∈ ℝ ∧ 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)))) → (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ (𝐴(ball‘(abs ∘ − ))𝑎))
128	109, 75, 122, 126, 127	syl22anc 838	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ (𝐴(ball‘(abs ∘ − ))𝑎))
129		simprr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
130	129	ad5antr 734	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
131	128, 130	sstrd 3974	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
132	131	sseld 3962	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) → -𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ))))
133	121, 132	sylbird 260	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘)) → -𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ))))
134	108, 133	mt3d 148	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘)))
135	74, 80, 79, 103, 134	ltletrd 11400	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) < (abs‘(𝑥 + 𝑘)))
136	74, 79, 135	ltled 11388	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))
137	136	ralrimiva 3133	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))
138	72, 137	jca 511	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))))
139	138	ex 412	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) → ((𝐴(abs ∘ − )𝑥) < (𝑎 / 2) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))))
140	139	ss2rabdv 4056	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)} ⊆ {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))})
141		blval 24330	. . . . . . . . 9 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ^*) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) = {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)})
142	1, 31, 34, 141	mp3an2i 1468	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) = {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)})
143	28	a1i 11	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))})
144	140, 142, 143	3sstr4d 4019	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈)
145	6	ssntr 23001	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑈 ⊆ ℂ) ∧ ((𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽 ∧ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈)) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ ((int‘𝐽)‘𝑈))
146	27, 30, 36, 144, 145	syl22anc 838	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ ((int‘𝐽)‘𝑈))
147		blcntr 24357	. . . . . . 7 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ⁺) → 𝐴 ∈ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)))
148	1, 31, 33, 147	mp3an2i 1468	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)))
149	146, 148	sseldd 3964	. . . . 5 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ((int‘𝐽)‘𝑈))
150	149	ex 412	. . . 4 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) → ((((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → 𝐴 ∈ ((int‘𝐽)‘𝑈)))
151	150	reximdva 3154	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈)))
152	25, 151	mpd 15	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))
153	13, 152	rexlimddv 3148	1 ⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2933 ∀wral 3052 ∃wrex 3061 {crab 3420 ∖ cdif 3928 ⊆ wss 3931 class class class wbr 5124 ∘ ccom 5663 ‘cfv 6536 (class class class)co 7410 ℂcc 11132 ℝcr 11133 0cc0 11134 1c1 11135 + caddc 11137 ℝ^*cxr 11273 < clt 11274 ≤ cle 11275 − cmin 11471 -cneg 11472 / cdiv 11899 ℕcn 12245 2c2 12300 ℕ₀cn0 12506 ℤcz 12593 ℝ⁺crp 13013 abscabs 15258 TopOpenctopn 17440 ∞Metcxmet 21305 ballcbl 21307 ℂ_fldccnfld 21320 Topctop 22836 Clsdccld 22959 intcnt 22960

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-iin 4975 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-er 8724 df-map 8847 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fi 9428 df-sup 9459 df-inf 9460 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 df-9 12315 df-n0 12507 df-z 12594 df-dec 12714 df-uz 12858 df-q 12970 df-rp 13014 df-xneg 13133 df-xadd 13134 df-xmul 13135 df-ioo 13371 df-fz 13530 df-fl 13814 df-seq 14025 df-exp 14085 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-struct 17171 df-slot 17206 df-ndx 17218 df-base 17234 df-plusg 17289 df-mulr 17290 df-starv 17291 df-tset 17295 df-ple 17296 df-ds 17298 df-unif 17299 df-rest 17441 df-topn 17442 df-topgen 17462 df-psmet 21312 df-xmet 21313 df-met 21314 df-bl 21315 df-mopn 21316 df-cnfld 21321 df-top 22837 df-topon 22854 df-topsp 22876 df-bases 22889 df-cld 22962 df-ntr 22963 df-xms 24264 df-ms 24265

This theorem is referenced by: lgamucov2 27006

W3C validator