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 25617

Description: The 𝑈 regions used in the proof of lgamgulm 25614 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 23383	. . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
2		difss 4110	. . . . 5 ⊢ (ℤ ∖ ℕ) ⊆ ℤ
3		lgamucov.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
4	3	sszcld 23427	. . . . 5 ⊢ ((ℤ ∖ ℕ) ⊆ ℤ → (ℤ ∖ ℕ) ∈ (Clsd‘𝐽))
5	3	cnfldtopon 23393	. . . . . . 7 ⊢ 𝐽 ∈ (TopOn‘ℂ)
6	5	toponunii 21526	. . . . . 6 ⊢ ℂ = ∪ 𝐽
7	6	cldopn 21641	. . . . 5 ⊢ ((ℤ ∖ ℕ) ∈ (Clsd‘𝐽) → (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽)
8	2, 4, 7	mp2b 10	. . . 4 ⊢ (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽
9	8	a1i 11	. . 3 ⊢ (𝜑 → (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽)
10		lgamucov.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
11	3	cnfldtopn 23392	. . . 4 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
12	11	mopni2 23105	. . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽 ∧ 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) → ∃𝑎 ∈ ℝ⁺ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
13	1, 9, 10, 12	mp3an2i 1462	. 2 ⊢ (𝜑 → ∃𝑎 ∈ ℝ⁺ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
14	10	eldifad 3950	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
15	14	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝐴 ∈ ℂ)
16	15	abscld 14798	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (abs‘𝐴) ∈ ℝ)
17		simprl 769	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ⁺)
18	17	rpred 12434	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ)
19	16, 18	readdcld 10672	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ((abs‘𝐴) + 𝑎) ∈ ℝ)
20		2re 11714	. . . . . . 7 ⊢ 2 ∈ ℝ
21	20	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 2 ∈ ℝ)
22	21, 17	rerpdivcld 12465	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (2 / 𝑎) ∈ ℝ)
23	19, 22	readdcld 10672	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ)
24		arch 11897	. . . 4 ⊢ ((((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ → ∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
25	23, 24	syl 17	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
26	3	cnfldtop 23394	. . . . . . . 8 ⊢ 𝐽 ∈ Top
27	26	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐽 ∈ Top)
28		lgamucov.u	. . . . . . . . 9 ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}
29	28	ssrab3 4059	. . . . . . . 8 ⊢ 𝑈 ⊆ ℂ
30	29	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑈 ⊆ ℂ)
31	15	ad2antrr 724	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ℂ)
32	17	ad2antrr 724	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑎 ∈ ℝ⁺)
33	32	rphalfcld 12446	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈ ℝ⁺)
34	33	rpxrd 12435	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈ ℝ^*)
35	11	blopn 23112	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ^*) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽)
36	1, 31, 34, 35	mp3an2i 1462	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽)
37		simplr 767	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑥 ∈ ℂ)
38	37	abscld 14798	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ∈ ℝ)
39		simp-4r 782	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℕ)
40	39	nnred 11655	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℝ)
41	23	ad4antr 730	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ)
42	19	ad4antr 730	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) ∈ ℝ)
43	16	ad4antr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝐴) ∈ ℝ)
44	38, 43	resubcld 11070	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ∈ ℝ)
45	18	ad4antr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ)
46	45	rehalfcld 11887	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) ∈ ℝ)
47	31	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝐴 ∈ ℂ)
48	37, 47	subcld 10999	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑥 − 𝐴) ∈ ℂ)
49	48	abscld 14798	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) ∈ ℝ)
50	37, 47	abs2difd 14819	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ≤ (abs‘(𝑥 − 𝐴)))
51		eqid 2823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs ∘ − ) = (abs ∘ − )
52	51	cnmetdval 23381	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥)))
53	47, 37, 52	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥)))
54	47, 37	abssubd 14815	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝐴 − 𝑥)) = (abs‘(𝑥 − 𝐴)))
55	53, 54	eqtrd 2858	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝑥 − 𝐴)))
56		simpr 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2))
57	55, 56	eqbrtrrd 5092	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) < (𝑎 / 2))
58	44, 49, 46, 50, 57	lelttrd 10800	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < (𝑎 / 2))
59	32	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ⁺)
60		rphalflt 12421	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ℝ⁺ → (𝑎 / 2) < 𝑎)
61	59, 60	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) < 𝑎)
62	44, 46, 45, 58, 61	lttrd 10803	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < 𝑎)
63	38, 43, 45	ltsubadd2d 11240	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝑥) − (abs‘𝐴)) < 𝑎 ↔ (abs‘𝑥) < ((abs‘𝐴) + 𝑎)))
64	62, 63	mpbid 234	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < ((abs‘𝐴) + 𝑎))
65		2rp 12397	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ⁺
66	65	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 2 ∈ ℝ⁺)
67	66, 59	rpdivcld 12451	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (2 / 𝑎) ∈ ℝ⁺)
68	42, 67	ltaddrpd 12467	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎)))
69	38, 42, 41, 64, 68	lttrd 10803	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎)))
70		simpllr 774	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
71	38, 41, 40, 69, 70	lttrd 10803	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < 𝑟)
72	38, 40, 71	ltled 10790	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ≤ 𝑟)
73	39	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑟 ∈ ℕ)
74	73	nnrecred 11691	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) ∈ ℝ)
75		simpllr 774	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑥 ∈ ℂ)
76		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
77	76	nn0cnd 11960	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℂ)
78	75, 77	addcld 10662	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥 + 𝑘) ∈ ℂ)
79	78	abscld 14798	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝑥 + 𝑘)) ∈ ℝ)
80	46	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑎 / 2) ∈ ℝ)
81	22	ad5antr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) ∈ ℝ)
82	41	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ)
83	40	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑟 ∈ ℝ)
84	47	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ∈ ℂ)
85	10	ad6antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
86	85	dmgmn0 25605	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ≠ 0)
87	84, 86	absrpcld 14810	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ⁺)
88	59	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ∈ ℝ⁺)
89	87, 88	rpaddcld 12449	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((abs‘𝐴) + 𝑎) ∈ ℝ⁺)
90	81, 89	ltaddrp2d 12468	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎)))
91		simp-4r 782	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
92	81, 82, 83, 90, 91	lttrd 10803	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) < 𝑟)
93	67	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) ∈ ℝ⁺)
94	73	nnrpd 12432	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑟 ∈ ℝ⁺)
95	93, 94	ltrecd 12452	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((2 / 𝑎) < 𝑟 ↔ (1 / 𝑟) < (1 / (2 / 𝑎))))
96	92, 95	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) < (1 / (2 / 𝑎)))
97		2cnd 11718	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 2 ∈ ℂ)
98	88	rpcnd 12436	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ∈ ℂ)
99		2ne0 11744	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
100	99	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 2 ≠ 0)
101	88	rpne0d 12439	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ≠ 0)
102	97, 98, 100, 101	recdivd 11435	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / (2 / 𝑎)) = (𝑎 / 2))
103	96, 102	breqtrd 5094	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) < (𝑎 / 2))
104		eldmgm 25601	. . . . . . . . . . . . . . . . 17 ⊢ (-𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↔ (-𝑘 ∈ ℂ ∧ ¬ --𝑘 ∈ ℕ₀))
105	104	simprbi 499	. . . . . . . . . . . . . . . 16 ⊢ (-𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → ¬ --𝑘 ∈ ℕ₀)
106	77	negnegd 10990	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → --𝑘 = 𝑘)
107	106, 76	eqeltrd 2915	. . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑎 / 2) ∈ ℝ^*)
111	77	negcld 10986	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → -𝑘 ∈ ℂ)
112		elbl2 23002	. . . . . . . . . . . . . . . . . 18 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑥 ∈ ℂ ∧ -𝑘 ∈ ℂ)) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝑥(abs ∘ − )-𝑘) < (𝑎 / 2)))
113	109, 110, 75, 111, 112	syl22anc 836	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝑥(abs ∘ − )-𝑘) < (𝑎 / 2)))
114	51	cnmetdval 23381	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ∧ -𝑘 ∈ ℂ) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘)))
115	75, 111, 114	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘)))
116	75, 77	subnegd 11006	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥 − -𝑘) = (𝑥 + 𝑘))
117	116	fveq2d 6676	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝑥 − -𝑘)) = (abs‘(𝑥 + 𝑘)))
118	115, 117	eqtrd 2858	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 + 𝑘)))
119	118	breq1d 5078	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((𝑥(abs ∘ − )-𝑘) < (𝑎 / 2) ↔ (abs‘(𝑥 + 𝑘)) < (𝑎 / 2)))
120	79, 80	ltnled 10789	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((abs‘(𝑥 + 𝑘)) < (𝑎 / 2) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘))))
121	113, 119, 120	3bitrd 307	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘))))
122	45	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ∈ ℝ)
123		simplr 767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2))
124		elbl3 23004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ)) → (𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)))
125	109, 110, 75, 84, 124	syl22anc 836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)))
126	123, 125	mpbird 259	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)))
127		blhalf 23017	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ∈ ℝ ∧ 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)))) → (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ (𝐴(ball‘(abs ∘ − ))𝑎))
128	109, 75, 122, 126, 127	syl22anc 836	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ (𝐴(ball‘(abs ∘ − ))𝑎))
129		simprr 771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
130	129	ad5antr 732	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
131	128, 130	sstrd 3979	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
132	131	sseld 3968	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) → -𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ))))
133	121, 132	sylbird 262	. . . . . . . . . . . . . . 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 10802	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) < (abs‘(𝑥 + 𝑘)))
136	74, 79, 135	ltled 10790	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))
137	136	ralrimiva 3184	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))
138	72, 137	jca 514	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))))
139	138	ex 415	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) → ((𝐴(abs ∘ − )𝑥) < (𝑎 / 2) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))))
140	139	ss2rabdv 4054	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)} ⊆ {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))})
141		blval 22998	. . . . . . . . 9 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ^*) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) = {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)})
142	1, 31, 34, 141	mp3an2i 1462	. . . . . . . 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 4016	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈)
145	6	ssntr 21668	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑈 ⊆ ℂ) ∧ ((𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽 ∧ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈)) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ ((int‘𝐽)‘𝑈))
146	27, 30, 36, 144, 145	syl22anc 836	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ ((int‘𝐽)‘𝑈))
147		blcntr 23025	. . . . . . 7 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ⁺) → 𝐴 ∈ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)))
148	1, 31, 33, 147	mp3an2i 1462	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)))
149	146, 148	sseldd 3970	. . . . 5 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ((int‘𝐽)‘𝑈))
150	149	ex 415	. . . 4 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) → ((((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → 𝐴 ∈ ((int‘𝐽)‘𝑈)))
151	150	reximdva 3276	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈)))
152	25, 151	mpd 15	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))
153	13, 152	rexlimddv 3293	1 ⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ≠ wne 3018 ∀wral 3140 ∃wrex 3141 {crab 3144 ∖ cdif 3935 ⊆ wss 3938 class class class wbr 5068 ∘ ccom 5561 ‘cfv 6357 (class class class)co 7158 ℂcc 10537 ℝcr 10538 0cc0 10539 1c1 10540 + caddc 10542 ℝ^*cxr 10676 < clt 10677 ≤ cle 10678 − cmin 10872 -cneg 10873 / cdiv 11299 ℕcn 11640 2c2 11695 ℕ₀cn0 11900 ℤcz 11984 ℝ⁺crp 12392 abscabs 14595 TopOpenctopn 16697 ∞Metcxmet 20532 ballcbl 20534 ℂ_fldccnfld 20547 Topctop 21503 Clsdccld 21626 intcnt 21627

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616 ax-pre-sup 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-iin 4924 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-om 7583 df-1st 7691 df-2nd 7692 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-oadd 8108 df-er 8291 df-map 8410 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-fi 8877 df-sup 8908 df-inf 8909 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-div 11300 df-nn 11641 df-2 11703 df-3 11704 df-4 11705 df-5 11706 df-6 11707 df-7 11708 df-8 11709 df-9 11710 df-n0 11901 df-z 11985 df-dec 12102 df-uz 12247 df-q 12352 df-rp 12393 df-xneg 12510 df-xadd 12511 df-xmul 12512 df-ioo 12745 df-fz 12896 df-fl 13165 df-seq 13373 df-exp 13433 df-cj 14460 df-re 14461 df-im 14462 df-sqrt 14596 df-abs 14597 df-struct 16487 df-ndx 16488 df-slot 16489 df-base 16491 df-plusg 16580 df-mulr 16581 df-starv 16582 df-tset 16586 df-ple 16587 df-ds 16589 df-unif 16590 df-rest 16698 df-topn 16699 df-topgen 16719 df-psmet 20539 df-xmet 20540 df-met 20541 df-bl 20542 df-mopn 20543 df-cnfld 20548 df-top 21504 df-topon 21521 df-topsp 21543 df-bases 21556 df-cld 21629 df-ntr 21630 df-xms 22932 df-ms 22933

This theorem is referenced by: lgamucov2 25618

W3C validator