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 25623

Description: The 𝑈 regions used in the proof of lgamgulm 25620 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 23378	. . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
2		difss 4059	. . . . 5 ⊢ (ℤ ∖ ℕ) ⊆ ℤ
3		lgamucov.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
4	3	sszcld 23422	. . . . 5 ⊢ ((ℤ ∖ ℕ) ⊆ ℤ → (ℤ ∖ ℕ) ∈ (Clsd‘𝐽))
5	3	cnfldtopon 23388	. . . . . . 7 ⊢ 𝐽 ∈ (TopOn‘ℂ)
6	5	toponunii 21521	. . . . . 6 ⊢ ℂ = ∪ 𝐽
7	6	cldopn 21636	. . . . 5 ⊢ ((ℤ ∖ ℕ) ∈ (Clsd‘𝐽) → (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽)
8	2, 4, 7	mp2b 10	. . . 4 ⊢ (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽
9	8	a1i 11	. . 3 ⊢ (𝜑 → (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽)
10		lgamucov.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
11	3	cnfldtopn 23387	. . . 4 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
12	11	mopni2 23100	. . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽 ∧ 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) → ∃𝑎 ∈ ℝ⁺ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
13	1, 9, 10, 12	mp3an2i 1463	. 2 ⊢ (𝜑 → ∃𝑎 ∈ ℝ⁺ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
14	10	eldifad 3893	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
15	14	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝐴 ∈ ℂ)
16	15	abscld 14788	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (abs‘𝐴) ∈ ℝ)
17		simprl 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ⁺)
18	17	rpred 12419	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ)
19	16, 18	readdcld 10659	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ((abs‘𝐴) + 𝑎) ∈ ℝ)
20		2re 11699	. . . . . . 7 ⊢ 2 ∈ ℝ
21	20	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 2 ∈ ℝ)
22	21, 17	rerpdivcld 12450	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (2 / 𝑎) ∈ ℝ)
23	19, 22	readdcld 10659	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ)
24		arch 11882	. . . 4 ⊢ ((((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ → ∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
25	23, 24	syl 17	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
26	3	cnfldtop 23389	. . . . . . . 8 ⊢ 𝐽 ∈ Top
27	26	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐽 ∈ Top)
28		lgamucov.u	. . . . . . . . 9 ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}
29	28	ssrab3 4008	. . . . . . . 8 ⊢ 𝑈 ⊆ ℂ
30	29	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑈 ⊆ ℂ)
31	15	ad2antrr 725	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ℂ)
32	17	ad2antrr 725	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑎 ∈ ℝ⁺)
33	32	rphalfcld 12431	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈ ℝ⁺)
34	33	rpxrd 12420	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈ ℝ^*)
35	11	blopn 23107	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ^*) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽)
36	1, 31, 34, 35	mp3an2i 1463	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽)
37		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑥 ∈ ℂ)
38	37	abscld 14788	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ∈ ℝ)
39		simp-4r 783	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℕ)
40	39	nnred 11640	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℝ)
41	23	ad4antr 731	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ)
42	19	ad4antr 731	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) ∈ ℝ)
43	16	ad4antr 731	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝐴) ∈ ℝ)
44	38, 43	resubcld 11057	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ∈ ℝ)
45	18	ad4antr 731	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ)
46	45	rehalfcld 11872	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) ∈ ℝ)
47	31	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝐴 ∈ ℂ)
48	37, 47	subcld 10986	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑥 − 𝐴) ∈ ℂ)
49	48	abscld 14788	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) ∈ ℝ)
50	37, 47	abs2difd 14809	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ≤ (abs‘(𝑥 − 𝐴)))
51		eqid 2798	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs ∘ − ) = (abs ∘ − )
52	51	cnmetdval 23376	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥)))
53	47, 37, 52	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥)))
54	47, 37	abssubd 14805	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝐴 − 𝑥)) = (abs‘(𝑥 − 𝐴)))
55	53, 54	eqtrd 2833	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝑥 − 𝐴)))
56		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2))
57	55, 56	eqbrtrrd 5054	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) < (𝑎 / 2))
58	44, 49, 46, 50, 57	lelttrd 10787	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < (𝑎 / 2))
59	32	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ⁺)
60		rphalflt 12406	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ℝ⁺ → (𝑎 / 2) < 𝑎)
61	59, 60	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) < 𝑎)
62	44, 46, 45, 58, 61	lttrd 10790	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < 𝑎)
63	38, 43, 45	ltsubadd2d 11227	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝑥) − (abs‘𝐴)) < 𝑎 ↔ (abs‘𝑥) < ((abs‘𝐴) + 𝑎)))
64	62, 63	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < ((abs‘𝐴) + 𝑎))
65		2rp 12382	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ⁺
66	65	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 2 ∈ ℝ⁺)
67	66, 59	rpdivcld 12436	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (2 / 𝑎) ∈ ℝ⁺)
68	42, 67	ltaddrpd 12452	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎)))
69	38, 42, 41, 64, 68	lttrd 10790	. . . . . . . . . . . . 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 10790	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < 𝑟)
72	38, 40, 71	ltled 10777	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ≤ 𝑟)
73	39	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑟 ∈ ℕ)
74	73	nnrecred 11676	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) ∈ ℝ)
75		simpllr 775	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑥 ∈ ℂ)
76		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
77	76	nn0cnd 11945	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℂ)
78	75, 77	addcld 10649	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥 + 𝑘) ∈ ℂ)
79	78	abscld 14788	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝑥 + 𝑘)) ∈ ℝ)
80	46	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑎 / 2) ∈ ℝ)
81	22	ad5antr 733	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) ∈ ℝ)
82	41	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ)
83	40	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑟 ∈ ℝ)
84	47	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ∈ ℂ)
85	10	ad6antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
86	85	dmgmn0 25611	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ≠ 0)
87	84, 86	absrpcld 14800	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ⁺)
88	59	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ∈ ℝ⁺)
89	87, 88	rpaddcld 12434	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((abs‘𝐴) + 𝑎) ∈ ℝ⁺)
90	81, 89	ltaddrp2d 12453	. . . . . . . . . . . . . . . . 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 10790	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) < 𝑟)
93	67	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) ∈ ℝ⁺)
94	73	nnrpd 12417	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑟 ∈ ℝ⁺)
95	93, 94	ltrecd 12437	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((2 / 𝑎) < 𝑟 ↔ (1 / 𝑟) < (1 / (2 / 𝑎))))
96	92, 95	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) < (1 / (2 / 𝑎)))
97		2cnd 11703	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 2 ∈ ℂ)
98	88	rpcnd 12421	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ∈ ℂ)
99		2ne0 11729	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
100	99	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 2 ≠ 0)
101	88	rpne0d 12424	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ≠ 0)
102	97, 98, 100, 101	recdivd 11422	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / (2 / 𝑎)) = (𝑎 / 2))
103	96, 102	breqtrd 5056	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) < (𝑎 / 2))
104		eldmgm 25607	. . . . . . . . . . . . . . . . 17 ⊢ (-𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↔ (-𝑘 ∈ ℂ ∧ ¬ --𝑘 ∈ ℕ₀))
105	104	simprbi 500	. . . . . . . . . . . . . . . 16 ⊢ (-𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → ¬ --𝑘 ∈ ℕ₀)
106	77	negnegd 10977	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → --𝑘 = 𝑘)
107	106, 76	eqeltrd 2890	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → --𝑘 ∈ ℕ₀)
108	105, 107	nsyl3 140	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ¬ -𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
109	1	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs ∘ − ) ∈ (∞Met‘ℂ))
110	34	ad3antrrr 729	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑎 / 2) ∈ ℝ^*)
111	77	negcld 10973	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → -𝑘 ∈ ℂ)
112		elbl2 22997	. . . . . . . . . . . . . . . . . 18 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑥 ∈ ℂ ∧ -𝑘 ∈ ℂ)) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝑥(abs ∘ − )-𝑘) < (𝑎 / 2)))
113	109, 110, 75, 111, 112	syl22anc 837	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝑥(abs ∘ − )-𝑘) < (𝑎 / 2)))
114	51	cnmetdval 23376	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ∧ -𝑘 ∈ ℂ) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘)))
115	75, 111, 114	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘)))
116	75, 77	subnegd 10993	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥 − -𝑘) = (𝑥 + 𝑘))
117	116	fveq2d 6649	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝑥 − -𝑘)) = (abs‘(𝑥 + 𝑘)))
118	115, 117	eqtrd 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 + 𝑘)))
119	118	breq1d 5040	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((𝑥(abs ∘ − )-𝑘) < (𝑎 / 2) ↔ (abs‘(𝑥 + 𝑘)) < (𝑎 / 2)))
120	79, 80	ltnled 10776	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((abs‘(𝑥 + 𝑘)) < (𝑎 / 2) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘))))
121	113, 119, 120	3bitrd 308	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘))))
122	45	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ∈ ℝ)
123		simplr 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2))
124		elbl3 22999	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ)) → (𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)))
125	109, 110, 75, 84, 124	syl22anc 837	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)))
126	123, 125	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)))
127		blhalf 23012	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ∈ ℝ ∧ 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)))) → (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ (𝐴(ball‘(abs ∘ − ))𝑎))
128	109, 75, 122, 126, 127	syl22anc 837	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ (𝐴(ball‘(abs ∘ − ))𝑎))
129		simprr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
130	129	ad5antr 733	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
131	128, 130	sstrd 3925	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
132	131	sseld 3914	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) → -𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ))))
133	121, 132	sylbird 263	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘)) → -𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ))))
134	108, 133	mt3d 150	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘)))
135	74, 80, 79, 103, 134	ltletrd 10789	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) < (abs‘(𝑥 + 𝑘)))
136	74, 79, 135	ltled 10777	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))
137	136	ralrimiva 3149	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))
138	72, 137	jca 515	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))))
139	138	ex 416	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) → ((𝐴(abs ∘ − )𝑥) < (𝑎 / 2) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))))
140	139	ss2rabdv 4003	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)} ⊆ {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))})
141		blval 22993	. . . . . . . . 9 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ^*) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) = {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)})
142	1, 31, 34, 141	mp3an2i 1463	. . . . . . . 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 3962	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈)
145	6	ssntr 21663	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑈 ⊆ ℂ) ∧ ((𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽 ∧ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈)) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ ((int‘𝐽)‘𝑈))
146	27, 30, 36, 144, 145	syl22anc 837	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ ((int‘𝐽)‘𝑈))
147		blcntr 23020	. . . . . . 7 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ⁺) → 𝐴 ∈ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)))
148	1, 31, 33, 147	mp3an2i 1463	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)))
149	146, 148	sseldd 3916	. . . . 5 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ((int‘𝐽)‘𝑈))
150	149	ex 416	. . . 4 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) → ((((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → 𝐴 ∈ ((int‘𝐽)‘𝑈)))
151	150	reximdva 3233	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈)))
152	25, 151	mpd 15	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))
153	13, 152	rexlimddv 3250	1 ⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ≠ wne 2987 ∀wral 3106 ∃wrex 3107 {crab 3110 ∖ cdif 3878 ⊆ wss 3881 class class class wbr 5030 ∘ ccom 5523 ‘cfv 6324 (class class class)co 7135 ℂcc 10524 ℝcr 10525 0cc0 10526 1c1 10527 + caddc 10529 ℝ^*cxr 10663 < clt 10664 ≤ cle 10665 − cmin 10859 -cneg 10860 / cdiv 11286 ℕcn 11625 2c2 11680 ℕ₀cn0 11885 ℤcz 11969 ℝ⁺crp 12377 abscabs 14585 TopOpenctopn 16687 ∞Metcxmet 20076 ballcbl 20078 ℂ_fldccnfld 20091 Topctop 21498 Clsdccld 21621 intcnt 21622

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603 ax-pre-sup 10604

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-iin 4884 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-om 7561 df-1st 7671 df-2nd 7672 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-oadd 8089 df-er 8272 df-map 8391 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-fi 8859 df-sup 8890 df-inf 8891 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-div 11287 df-nn 11626 df-2 11688 df-3 11689 df-4 11690 df-5 11691 df-6 11692 df-7 11693 df-8 11694 df-9 11695 df-n0 11886 df-z 11970 df-dec 12087 df-uz 12232 df-q 12337 df-rp 12378 df-xneg 12495 df-xadd 12496 df-xmul 12497 df-ioo 12730 df-fz 12886 df-fl 13157 df-seq 13365 df-exp 13426 df-cj 14450 df-re 14451 df-im 14452 df-sqrt 14586 df-abs 14587 df-struct 16477 df-ndx 16478 df-slot 16479 df-base 16481 df-plusg 16570 df-mulr 16571 df-starv 16572 df-tset 16576 df-ple 16577 df-ds 16579 df-unif 16580 df-rest 16688 df-topn 16689 df-topgen 16709 df-psmet 20083 df-xmet 20084 df-met 20085 df-bl 20086 df-mopn 20087 df-cnfld 20092 df-top 21499 df-topon 21516 df-topsp 21538 df-bases 21551 df-cld 21624 df-ntr 21625 df-xms 22927 df-ms 22928

This theorem is referenced by: lgamucov2 25624

W3C validator