Step | Hyp | Ref
| Expression |
1 | | cnxmet 22386 |
. . . 4
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
3 | | difss 3699 |
. . . . 5
⊢ (ℤ
∖ ℕ) ⊆ ℤ |
4 | | lgamucov.j |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
5 | 4 | sszcld 22428 |
. . . . 5
⊢ ((ℤ
∖ ℕ) ⊆ ℤ → (ℤ ∖ ℕ) ∈
(Clsd‘𝐽)) |
6 | 4 | cnfldtopon 22396 |
. . . . . . 7
⊢ 𝐽 ∈
(TopOn‘ℂ) |
7 | 6 | toponunii 20547 |
. . . . . 6
⊢ ℂ =
∪ 𝐽 |
8 | 7 | cldopn 20645 |
. . . . 5
⊢ ((ℤ
∖ ℕ) ∈ (Clsd‘𝐽) → (ℂ ∖ (ℤ ∖
ℕ)) ∈ 𝐽) |
9 | 3, 5, 8 | mp2b 10 |
. . . 4
⊢ (ℂ
∖ (ℤ ∖ ℕ)) ∈ 𝐽 |
10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → (ℂ ∖ (ℤ
∖ ℕ)) ∈ 𝐽) |
11 | | lgamucov.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
12 | 4 | cnfldtopn 22395 |
. . . 4
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
13 | 12 | mopni2 22108 |
. . 3
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖
(ℤ ∖ ℕ)) ∈ 𝐽 ∧ 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) → ∃𝑎
∈ ℝ+ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖
(ℤ ∖ ℕ))) |
14 | 2, 10, 11, 13 | syl3anc 1318 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ ℝ+ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ))) |
15 | 11 | eldifad 3552 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
16 | 15 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 𝐴 ∈ ℂ) |
17 | 16 | abscld 14023 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (abs‘𝐴) ∈ ℝ) |
18 | | simprl 790 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ+) |
19 | 18 | rpred 11748 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ) |
20 | 17, 19 | readdcld 9948 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → ((abs‘𝐴) + 𝑎) ∈ ℝ) |
21 | | 2re 10967 |
. . . . . . 7
⊢ 2 ∈
ℝ |
22 | 21 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 2 ∈ ℝ) |
23 | 22, 18 | rerpdivcld 11779 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (2 / 𝑎) ∈ ℝ) |
24 | 20, 23 | readdcld 9948 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ) |
25 | | arch 11166 |
. . . 4
⊢
((((abs‘𝐴) +
𝑎) + (2 / 𝑎)) ∈ ℝ →
∃𝑟 ∈ ℕ
(((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) |
26 | 24, 25 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) |
27 | 4 | cnfldtop 22397 |
. . . . . . . 8
⊢ 𝐽 ∈ Top |
28 | 27 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐽 ∈ Top) |
29 | | lgamucov.u |
. . . . . . . . 9
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))} |
30 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑥 ∈ ℂ ∣
((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 /
𝑟) ≤ (abs‘(𝑥 + 𝑘)))} ⊆ ℂ |
31 | 29, 30 | eqsstri 3598 |
. . . . . . . 8
⊢ 𝑈 ⊆
ℂ |
32 | 31 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑈 ⊆ ℂ) |
33 | 1 | a1i 11 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
34 | 16 | ad2antrr 758 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ℂ) |
35 | 18 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑎 ∈ ℝ+) |
36 | 35 | rphalfcld 11760 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈
ℝ+) |
37 | 36 | rpxrd 11749 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈
ℝ*) |
38 | 12 | blopn 22115 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ*) →
(𝐴(ball‘(abs ∘
− ))(𝑎 / 2)) ∈
𝐽) |
39 | 33, 34, 37, 38 | syl3anc 1318 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽) |
40 | | simplr 788 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑥 ∈ ℂ) |
41 | 40 | abscld 14023 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ∈ ℝ) |
42 | | simp-4r 803 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℕ) |
43 | 42 | nnred 10912 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℝ) |
44 | 24 | ad4antr 764 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ) |
45 | 20 | ad4antr 764 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) ∈ ℝ) |
46 | 17 | ad4antr 764 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝐴) ∈ ℝ) |
47 | 41, 46 | resubcld 10337 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ∈ ℝ) |
48 | 19 | ad4antr 764 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ) |
49 | 48 | rehalfcld 11156 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) ∈ ℝ) |
50 | 34 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝐴 ∈ ℂ) |
51 | 40, 50 | subcld 10271 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑥 − 𝐴) ∈ ℂ) |
52 | 51 | abscld 14023 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) ∈ ℝ) |
53 | 40, 50 | abs2difd 14044 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ≤ (abs‘(𝑥 − 𝐴))) |
54 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (abs
∘ − ) = (abs ∘ − ) |
55 | 54 | cnmetdval 22384 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥))) |
56 | 50, 40, 55 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥))) |
57 | 50, 40 | abssubd 14040 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝐴 − 𝑥)) = (abs‘(𝑥 − 𝐴))) |
58 | 56, 57 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝑥 − 𝐴))) |
59 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) |
60 | 58, 59 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) < (𝑎 / 2)) |
61 | 47, 52, 49, 53, 60 | lelttrd 10074 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < (𝑎 / 2)) |
62 | 35 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ+) |
63 | | rphalflt 11736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ ℝ+
→ (𝑎 / 2) < 𝑎) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) < 𝑎) |
65 | 47, 49, 48, 61, 64 | lttrd 10077 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < 𝑎) |
66 | 41, 46, 48 | ltsubadd2d 10504 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝑥) − (abs‘𝐴)) < 𝑎 ↔ (abs‘𝑥) < ((abs‘𝐴) + 𝑎))) |
67 | 65, 66 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < ((abs‘𝐴) + 𝑎)) |
68 | | 2rp 11713 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 2 ∈
ℝ+) |
70 | 69, 62 | rpdivcld 11765 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (2 / 𝑎) ∈
ℝ+) |
71 | 45, 70 | ltaddrpd 11781 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎))) |
72 | 41, 45, 44, 67, 71 | lttrd 10077 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎))) |
73 | | simpllr 795 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) |
74 | 41, 44, 43, 72, 73 | lttrd 10077 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < 𝑟) |
75 | 41, 43, 74 | ltled 10064 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ≤ 𝑟) |
76 | 42 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑟 ∈
ℕ) |
77 | 76 | nnrecred 10943 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) ∈
ℝ) |
78 | | simpllr 795 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈
ℂ) |
79 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
80 | 79 | nn0cnd 11230 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℂ) |
81 | 78, 80 | addcld 9938 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥 + 𝑘) ∈ ℂ) |
82 | 81 | abscld 14023 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(abs‘(𝑥 + 𝑘)) ∈
ℝ) |
83 | 49 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑎 / 2) ∈
ℝ) |
84 | 23 | ad5antr 766 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (2 /
𝑎) ∈
ℝ) |
85 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ) |
86 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑟 ∈
ℝ) |
87 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈
ℂ) |
88 | 11 | ad6antr 768 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ (ℂ ∖
(ℤ ∖ ℕ))) |
89 | 88 | dmgmn0 24552 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ≠ 0) |
90 | 87, 89 | absrpcld 14035 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(abs‘𝐴) ∈
ℝ+) |
91 | 62 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ∈
ℝ+) |
92 | 90, 91 | rpaddcld 11763 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
((abs‘𝐴) + 𝑎) ∈
ℝ+) |
93 | 84, 92 | ltaddrp2d 11782 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (2 /
𝑎) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎))) |
94 | | simp-4r 803 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) |
95 | 84, 85, 86, 93, 94 | lttrd 10077 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (2 /
𝑎) < 𝑟) |
96 | 70 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (2 /
𝑎) ∈
ℝ+) |
97 | 76 | nnrpd 11746 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑟 ∈
ℝ+) |
98 | 96, 97 | ltrecd 11766 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → ((2 /
𝑎) < 𝑟 ↔ (1 / 𝑟) < (1 / (2 / 𝑎)))) |
99 | 95, 98 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) < (1 / (2 / 𝑎))) |
100 | | 2cnd 10970 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 2 ∈
ℂ) |
101 | 91 | rpcnd 11750 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ∈
ℂ) |
102 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ≠
0 |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 2 ≠
0) |
104 | 91 | rpne0d 11753 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ≠ 0) |
105 | 100, 101,
103, 104 | recdivd 10697 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 / (2 /
𝑎)) = (𝑎 / 2)) |
106 | 99, 105 | breqtrd 4609 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) < (𝑎 / 2)) |
107 | | eldmgm 24548 |
. . . . . . . . . . . . . . . . 17
⊢ (-𝑘 ∈ (ℂ ∖
(ℤ ∖ ℕ)) ↔ (-𝑘 ∈ ℂ ∧ ¬ --𝑘 ∈
ℕ0)) |
108 | 107 | simprbi 479 |
. . . . . . . . . . . . . . . 16
⊢ (-𝑘 ∈ (ℂ ∖
(ℤ ∖ ℕ)) → ¬ --𝑘 ∈ ℕ0) |
109 | 80 | negnegd 10262 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → --𝑘 = 𝑘) |
110 | 109, 79 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → --𝑘 ∈
ℕ0) |
111 | 108, 110 | nsyl3 132 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → ¬
-𝑘 ∈ (ℂ ∖
(ℤ ∖ ℕ))) |
112 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (abs
∘ − ) ∈ (∞Met‘ℂ)) |
113 | 37 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑎 / 2) ∈
ℝ*) |
114 | 80 | negcld 10258 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → -𝑘 ∈
ℂ) |
115 | | elbl2 22005 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑎 / 2) ∈ ℝ*) ∧
(𝑥 ∈ ℂ ∧
-𝑘 ∈ ℂ)) →
(-𝑘 ∈ (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ↔ (𝑥(abs ∘ − )-𝑘) < (𝑎 / 2))) |
116 | 112, 113,
78, 114, 115 | syl22anc 1319 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝑥(abs ∘ − )-𝑘) < (𝑎 / 2))) |
117 | 54 | cnmetdval 22384 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℂ ∧ -𝑘 ∈ ℂ) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘))) |
118 | 78, 114, 117 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘))) |
119 | 78, 80 | subnegd 10278 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥 − -𝑘) = (𝑥 + 𝑘)) |
120 | 119 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(abs‘(𝑥 −
-𝑘)) = (abs‘(𝑥 + 𝑘))) |
121 | 118, 120 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 + 𝑘))) |
122 | 121 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → ((𝑥(abs ∘ − )-𝑘) < (𝑎 / 2) ↔ (abs‘(𝑥 + 𝑘)) < (𝑎 / 2))) |
123 | 82, 83 | ltnled 10063 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
((abs‘(𝑥 + 𝑘)) < (𝑎 / 2) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘)))) |
124 | 116, 122,
123 | 3bitrd 293 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘)))) |
125 | 48 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ∈
ℝ) |
126 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) |
127 | | elbl3 22007 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑎 / 2) ∈ ℝ*) ∧
(𝑥 ∈ ℂ ∧
𝐴 ∈ ℂ)) →
(𝐴 ∈ (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ↔ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2))) |
128 | 112, 113,
78, 87, 127 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2))) |
129 | 126, 128 | mpbird 246 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2))) |
130 | | blhalf 22020 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ∈ ℝ ∧ 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)))) → (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ⊆ (𝐴(ball‘(abs ∘ −
))𝑎)) |
131 | 112, 78, 125, 129, 130 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ⊆ (𝐴(ball‘(abs ∘ −
))𝑎)) |
132 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖
(ℤ ∖ ℕ))) |
133 | 132 | ad5antr 766 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ))) |
134 | 131, 133 | sstrd 3578 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ⊆ (ℂ
∖ (ℤ ∖ ℕ))) |
135 | 134 | sseld 3567 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) → -𝑘 ∈ (ℂ ∖
(ℤ ∖ ℕ)))) |
136 | 124, 135 | sylbird 249 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (¬
(𝑎 / 2) ≤
(abs‘(𝑥 + 𝑘)) → -𝑘 ∈ (ℂ ∖ (ℤ ∖
ℕ)))) |
137 | 111, 136 | mt3d 139 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘))) |
138 | 77, 83, 82, 106, 137 | ltletrd 10076 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) < (abs‘(𝑥 + 𝑘))) |
139 | 77, 82, 138 | ltled 10064 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) ≤ (abs‘(𝑥 + 𝑘))) |
140 | 139 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))) |
141 | 75, 140 | jca 553 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))) |
142 | 141 | ex 449 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) → ((𝐴(abs ∘ − )𝑥) < (𝑎 / 2) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))))) |
143 | 142 | ss2rabdv 3646 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)} ⊆ {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}) |
144 | | blval 22001 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ*) →
(𝐴(ball‘(abs ∘
− ))(𝑎 / 2)) = {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)}) |
145 | 33, 34, 37, 144 | syl3anc 1318 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) = {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)}) |
146 | 29 | a1i 11 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}) |
147 | 143, 145,
146 | 3sstr4d 3611 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈) |
148 | 7 | ssntr 20672 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑈 ⊆ ℂ) ∧ ((𝐴(ball‘(abs ∘ −
))(𝑎 / 2)) ∈ 𝐽 ∧ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈)) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ ((int‘𝐽)‘𝑈)) |
149 | 28, 32, 39, 147, 148 | syl22anc 1319 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ ((int‘𝐽)‘𝑈)) |
150 | | blcntr 22028 |
. . . . . . 7
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ+) →
𝐴 ∈ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2))) |
151 | 33, 34, 36, 150 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2))) |
152 | 149, 151 | sseldd 3569 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ((int‘𝐽)‘𝑈)) |
153 | 152 | ex 449 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) → ((((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → 𝐴 ∈ ((int‘𝐽)‘𝑈))) |
154 | 153 | reximdva 3000 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))) |
155 | 26, 154 | mpd 15 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈)) |
156 | 14, 155 | rexlimddv 3017 |
1
⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈)) |