Step | Hyp | Ref
| Expression |
1 | | cnxmet 22946 |
. . . 4
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
3 | | difss 3964 |
. . . . 5
⊢ (ℤ
∖ ℕ) ⊆ ℤ |
4 | | lgamucov.j |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
5 | 4 | sszcld 22990 |
. . . . 5
⊢ ((ℤ
∖ ℕ) ⊆ ℤ → (ℤ ∖ ℕ) ∈
(Clsd‘𝐽)) |
6 | 4 | cnfldtopon 22956 |
. . . . . . 7
⊢ 𝐽 ∈
(TopOn‘ℂ) |
7 | 6 | toponunii 21091 |
. . . . . 6
⊢ ℂ =
∪ 𝐽 |
8 | 7 | cldopn 21206 |
. . . . 5
⊢ ((ℤ
∖ ℕ) ∈ (Clsd‘𝐽) → (ℂ ∖ (ℤ ∖
ℕ)) ∈ 𝐽) |
9 | 3, 5, 8 | mp2b 10 |
. . . 4
⊢ (ℂ
∖ (ℤ ∖ ℕ)) ∈ 𝐽 |
10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → (ℂ ∖ (ℤ
∖ ℕ)) ∈ 𝐽) |
11 | | lgamucov.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
12 | 4 | cnfldtopn 22955 |
. . . 4
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
13 | 12 | mopni2 22668 |
. . 3
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖
(ℤ ∖ ℕ)) ∈ 𝐽 ∧ 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) → ∃𝑎
∈ ℝ+ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖
(ℤ ∖ ℕ))) |
14 | 2, 10, 11, 13 | syl3anc 1494 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ ℝ+ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ))) |
15 | 11 | eldifad 3810 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
16 | 15 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 𝐴 ∈ ℂ) |
17 | 16 | abscld 14552 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (abs‘𝐴) ∈ ℝ) |
18 | | simprl 787 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ+) |
19 | 18 | rpred 12156 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ) |
20 | 17, 19 | readdcld 10386 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → ((abs‘𝐴) + 𝑎) ∈ ℝ) |
21 | | 2re 11425 |
. . . . . . 7
⊢ 2 ∈
ℝ |
22 | 21 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 2 ∈ ℝ) |
23 | 22, 18 | rerpdivcld 12187 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (2 / 𝑎) ∈ ℝ) |
24 | 20, 23 | readdcld 10386 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ) |
25 | | arch 11615 |
. . . 4
⊢
((((abs‘𝐴) +
𝑎) + (2 / 𝑎)) ∈ ℝ →
∃𝑟 ∈ ℕ
(((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) |
26 | 24, 25 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) |
27 | 4 | cnfldtop 22957 |
. . . . . . . 8
⊢ 𝐽 ∈ Top |
28 | 27 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐽 ∈ Top) |
29 | | lgamucov.u |
. . . . . . . . 9
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))} |
30 | | ssrab2 3912 |
. . . . . . . . 9
⊢ {𝑥 ∈ ℂ ∣
((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 /
𝑟) ≤ (abs‘(𝑥 + 𝑘)))} ⊆ ℂ |
31 | 29, 30 | eqsstri 3860 |
. . . . . . . 8
⊢ 𝑈 ⊆
ℂ |
32 | 31 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑈 ⊆ ℂ) |
33 | 1 | a1i 11 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
34 | 16 | ad2antrr 717 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ℂ) |
35 | 18 | ad2antrr 717 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑎 ∈ ℝ+) |
36 | 35 | rphalfcld 12168 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈
ℝ+) |
37 | 36 | rpxrd 12157 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈
ℝ*) |
38 | 12 | blopn 22675 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ*) →
(𝐴(ball‘(abs ∘
− ))(𝑎 / 2)) ∈
𝐽) |
39 | 33, 34, 37, 38 | syl3anc 1494 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽) |
40 | | simplr 785 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑥 ∈ ℂ) |
41 | 40 | abscld 14552 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ∈ ℝ) |
42 | | simp-4r 803 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℕ) |
43 | 42 | nnred 11367 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℝ) |
44 | 24 | ad4antr 724 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ) |
45 | 20 | ad4antr 724 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) ∈ ℝ) |
46 | 17 | ad4antr 724 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝐴) ∈ ℝ) |
47 | 41, 46 | resubcld 10782 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ∈ ℝ) |
48 | 19 | ad4antr 724 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ) |
49 | 48 | rehalfcld 11605 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) ∈ ℝ) |
50 | 34 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝐴 ∈ ℂ) |
51 | 40, 50 | subcld 10713 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑥 − 𝐴) ∈ ℂ) |
52 | 51 | abscld 14552 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) ∈ ℝ) |
53 | 40, 50 | abs2difd 14573 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ≤ (abs‘(𝑥 − 𝐴))) |
54 | | eqid 2825 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (abs
∘ − ) = (abs ∘ − ) |
55 | 54 | cnmetdval 22944 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥))) |
56 | 50, 40, 55 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥))) |
57 | 50, 40 | abssubd 14569 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝐴 − 𝑥)) = (abs‘(𝑥 − 𝐴))) |
58 | 56, 57 | eqtrd 2861 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝑥 − 𝐴))) |
59 | | simpr 479 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) |
60 | 58, 59 | eqbrtrrd 4897 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) < (𝑎 / 2)) |
61 | 47, 52, 49, 53, 60 | lelttrd 10514 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < (𝑎 / 2)) |
62 | 35 | ad2antrr 717 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ+) |
63 | | rphalflt 12143 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ ℝ+
→ (𝑎 / 2) < 𝑎) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) < 𝑎) |
65 | 47, 49, 48, 61, 64 | lttrd 10517 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < 𝑎) |
66 | 41, 46, 48 | ltsubadd2d 10950 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝑥) − (abs‘𝐴)) < 𝑎 ↔ (abs‘𝑥) < ((abs‘𝐴) + 𝑎))) |
67 | 65, 66 | mpbid 224 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < ((abs‘𝐴) + 𝑎)) |
68 | | 2rp 12117 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 2 ∈
ℝ+) |
70 | 69, 62 | rpdivcld 12173 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (2 / 𝑎) ∈
ℝ+) |
71 | 45, 70 | ltaddrpd 12189 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎))) |
72 | 41, 45, 44, 67, 71 | lttrd 10517 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎))) |
73 | | simpllr 793 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) |
74 | 41, 44, 43, 72, 73 | lttrd 10517 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < 𝑟) |
75 | 41, 43, 74 | ltled 10504 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ≤ 𝑟) |
76 | 42 | adantr 474 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑟 ∈
ℕ) |
77 | 76 | nnrecred 11402 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) ∈
ℝ) |
78 | | simpllr 793 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈
ℂ) |
79 | | simpr 479 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
80 | 79 | nn0cnd 11680 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℂ) |
81 | 78, 80 | addcld 10376 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥 + 𝑘) ∈ ℂ) |
82 | 81 | abscld 14552 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(abs‘(𝑥 + 𝑘)) ∈
ℝ) |
83 | 49 | adantr 474 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑎 / 2) ∈
ℝ) |
84 | 23 | ad5antr 728 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (2 /
𝑎) ∈
ℝ) |
85 | 44 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ) |
86 | 43 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑟 ∈
ℝ) |
87 | 50 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈
ℂ) |
88 | 11 | ad6antr 732 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ (ℂ ∖
(ℤ ∖ ℕ))) |
89 | 88 | dmgmn0 25165 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ≠ 0) |
90 | 87, 89 | absrpcld 14564 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(abs‘𝐴) ∈
ℝ+) |
91 | 62 | adantr 474 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ∈
ℝ+) |
92 | 90, 91 | rpaddcld 12171 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
((abs‘𝐴) + 𝑎) ∈
ℝ+) |
93 | 84, 92 | ltaddrp2d 12190 |
. . . . . . . . . . . . . . . . 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 10517 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (2 /
𝑎) < 𝑟) |
96 | 70 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (2 /
𝑎) ∈
ℝ+) |
97 | 76 | nnrpd 12154 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑟 ∈
ℝ+) |
98 | 96, 97 | ltrecd 12174 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → ((2 /
𝑎) < 𝑟 ↔ (1 / 𝑟) < (1 / (2 / 𝑎)))) |
99 | 95, 98 | mpbid 224 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) < (1 / (2 / 𝑎))) |
100 | | 2cnd 11429 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 2 ∈
ℂ) |
101 | 91 | rpcnd 12158 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ∈
ℂ) |
102 | | 2ne0 11462 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ≠
0 |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 2 ≠
0) |
104 | 91 | rpne0d 12161 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ≠ 0) |
105 | 100, 101,
103, 104 | recdivd 11144 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 / (2 /
𝑎)) = (𝑎 / 2)) |
106 | 99, 105 | breqtrd 4899 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) < (𝑎 / 2)) |
107 | | eldmgm 25161 |
. . . . . . . . . . . . . . . . 17
⊢ (-𝑘 ∈ (ℂ ∖
(ℤ ∖ ℕ)) ↔ (-𝑘 ∈ ℂ ∧ ¬ --𝑘 ∈
ℕ0)) |
108 | 107 | simprbi 492 |
. . . . . . . . . . . . . . . 16
⊢ (-𝑘 ∈ (ℂ ∖
(ℤ ∖ ℕ)) → ¬ --𝑘 ∈ ℕ0) |
109 | 80 | negnegd 10704 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → --𝑘 = 𝑘) |
110 | 109, 79 | eqeltrd 2906 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → --𝑘 ∈
ℕ0) |
111 | 108, 110 | nsyl3 136 |
. . . . . . . . . . . . . . 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 721 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑎 / 2) ∈
ℝ*) |
114 | 80 | negcld 10700 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → -𝑘 ∈
ℂ) |
115 | | elbl2 22565 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑎 / 2) ∈ ℝ*) ∧
(𝑥 ∈ ℂ ∧
-𝑘 ∈ ℂ)) →
(-𝑘 ∈ (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ↔ (𝑥(abs ∘ − )-𝑘) < (𝑎 / 2))) |
116 | 112, 113,
78, 114, 115 | syl22anc 872 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝑥(abs ∘ − )-𝑘) < (𝑎 / 2))) |
117 | 54 | cnmetdval 22944 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℂ ∧ -𝑘 ∈ ℂ) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘))) |
118 | 78, 114, 117 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘))) |
119 | 78, 80 | subnegd 10720 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥 − -𝑘) = (𝑥 + 𝑘)) |
120 | 119 | fveq2d 6437 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(abs‘(𝑥 −
-𝑘)) = (abs‘(𝑥 + 𝑘))) |
121 | 118, 120 | eqtrd 2861 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 + 𝑘))) |
122 | 121 | breq1d 4883 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → ((𝑥(abs ∘ − )-𝑘) < (𝑎 / 2) ↔ (abs‘(𝑥 + 𝑘)) < (𝑎 / 2))) |
123 | 82, 83 | ltnled 10503 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
((abs‘(𝑥 + 𝑘)) < (𝑎 / 2) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘)))) |
124 | 116, 122,
123 | 3bitrd 297 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘)))) |
125 | 48 | adantr 474 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ∈
ℝ) |
126 | | simplr 785 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) |
127 | | elbl3 22567 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑎 / 2) ∈ ℝ*) ∧
(𝑥 ∈ ℂ ∧
𝐴 ∈ ℂ)) →
(𝐴 ∈ (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ↔ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2))) |
128 | 112, 113,
78, 87, 127 | syl22anc 872 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2))) |
129 | 126, 128 | mpbird 249 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2))) |
130 | | blhalf 22580 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ∈ ℝ ∧ 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)))) → (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ⊆ (𝐴(ball‘(abs ∘ −
))𝑎)) |
131 | 112, 78, 125, 129, 130 | syl22anc 872 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ⊆ (𝐴(ball‘(abs ∘ −
))𝑎)) |
132 | | simprr 789 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖
(ℤ ∖ ℕ))) |
133 | 132 | ad5antr 728 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ))) |
134 | 131, 133 | sstrd 3837 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ⊆ (ℂ
∖ (ℤ ∖ ℕ))) |
135 | 134 | sseld 3826 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) → -𝑘 ∈ (ℂ ∖
(ℤ ∖ ℕ)))) |
136 | 124, 135 | sylbird 252 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (¬
(𝑎 / 2) ≤
(abs‘(𝑥 + 𝑘)) → -𝑘 ∈ (ℂ ∖ (ℤ ∖
ℕ)))) |
137 | 111, 136 | mt3d 143 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘))) |
138 | 77, 83, 82, 106, 137 | ltletrd 10516 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) < (abs‘(𝑥 + 𝑘))) |
139 | 77, 82, 138 | ltled 10504 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) ≤ (abs‘(𝑥 + 𝑘))) |
140 | 139 | ralrimiva 3175 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))) |
141 | 75, 140 | jca 507 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))) |
142 | 141 | ex 403 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) → ((𝐴(abs ∘ − )𝑥) < (𝑎 / 2) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))))) |
143 | 142 | ss2rabdv 3908 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)} ⊆ {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}) |
144 | | blval 22561 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ*) →
(𝐴(ball‘(abs ∘
− ))(𝑎 / 2)) = {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)}) |
145 | 33, 34, 37, 144 | syl3anc 1494 |
. . . . . . . 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 3873 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈) |
148 | 7 | ssntr 21233 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑈 ⊆ ℂ) ∧ ((𝐴(ball‘(abs ∘ −
))(𝑎 / 2)) ∈ 𝐽 ∧ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈)) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ ((int‘𝐽)‘𝑈)) |
149 | 28, 32, 39, 147, 148 | syl22anc 872 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ ((int‘𝐽)‘𝑈)) |
150 | | blcntr 22588 |
. . . . . . 7
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ+) →
𝐴 ∈ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2))) |
151 | 33, 34, 36, 150 | syl3anc 1494 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2))) |
152 | 149, 151 | sseldd 3828 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ((int‘𝐽)‘𝑈)) |
153 | 152 | ex 403 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) → ((((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → 𝐴 ∈ ((int‘𝐽)‘𝑈))) |
154 | 153 | reximdva 3225 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))) |
155 | 26, 154 | mpd 15 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈)) |
156 | 14, 155 | rexlimddv 3245 |
1
⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈)) |