Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 = (abs‘(ℑ‘𝐴))) |
2 | | cnrefiisplem.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
3 | | cnrefiisplem.n |
. . . . . . . . 9
⊢ (𝜑 → ¬ 𝐴 ∈ ℝ) |
4 | 2, 3 | absimnre 42557 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘(ℑ‘𝐴)) ∈
ℝ+) |
5 | 4 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 = (abs‘(ℑ‘𝐴))) →
(abs‘(ℑ‘𝐴)) ∈
ℝ+) |
6 | 1, 5 | eqeltrd 2833 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+) |
7 | 6 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐷) ∧ 𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+) |
8 | | simpll 767 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝜑) |
9 | | cnrefiisplem.d |
. . . . . . . . . . . 12
⊢ 𝐷 =
({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))}) |
10 | 9 | eleq2i 2824 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝐷 ↔ 𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))})) |
11 | 10 | biimpi 219 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝐷 → 𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))})) |
12 | | nelsn 4556 |
. . . . . . . . . 10
⊢ (𝑤 ≠
(abs‘(ℑ‘𝐴)) → ¬ 𝑤 ∈ {(abs‘(ℑ‘𝐴))}) |
13 | | elunnel1 4040 |
. . . . . . . . . 10
⊢ ((𝑤 ∈
({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))}) ∧ ¬ 𝑤 ∈ {(abs‘(ℑ‘𝐴))}) → 𝑤 ∈ ∪
𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))}) |
14 | 11, 12, 13 | syl2an 599 |
. . . . . . . . 9
⊢ ((𝑤 ∈ 𝐷 ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ∪
𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))}) |
15 | | eliun 4885 |
. . . . . . . . 9
⊢ (𝑤 ∈ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))} ↔ ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦 − 𝐴))}) |
16 | 14, 15 | sylib 221 |
. . . . . . . 8
⊢ ((𝑤 ∈ 𝐷 ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦 − 𝐴))}) |
17 | | velsn 4532 |
. . . . . . . . 9
⊢ (𝑤 ∈ {(abs‘(𝑦 − 𝐴))} ↔ 𝑤 = (abs‘(𝑦 − 𝐴))) |
18 | 17 | rexbii 3161 |
. . . . . . . 8
⊢
(∃𝑦 ∈
((𝐵 ∩ ℂ) ∖
{𝐴})𝑤 ∈ {(abs‘(𝑦 − 𝐴))} ↔ ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦 − 𝐴))) |
19 | 16, 18 | sylib 221 |
. . . . . . 7
⊢ ((𝑤 ∈ 𝐷 ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦 − 𝐴))) |
20 | 19 | adantll 714 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦 − 𝐴))) |
21 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → 𝑤 = (abs‘(𝑦 − 𝐴))) |
22 | | eldifi 4017 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦 ∈ (𝐵 ∩ ℂ)) |
23 | 22 | elin2d 4089 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦 ∈ ℂ) |
24 | 23 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → 𝑦 ∈ ℂ) |
25 | 2 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → 𝐴 ∈ ℂ) |
26 | 24, 25 | subcld 11075 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → (𝑦 − 𝐴) ∈ ℂ) |
27 | | eldifsni 4678 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦 ≠ 𝐴) |
28 | 27 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → 𝑦 ≠ 𝐴) |
29 | 24, 25, 28 | subne0d 11084 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → (𝑦 − 𝐴) ≠ 0) |
30 | 26, 29 | absrpcld 14898 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → (abs‘(𝑦 − 𝐴)) ∈
ℝ+) |
31 | 21, 30 | eqeltrd 2833 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → 𝑤 ∈ ℝ+) |
32 | 31 | rexlimdva2 3197 |
. . . . . 6
⊢ (𝜑 → (∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦 − 𝐴)) → 𝑤 ∈
ℝ+)) |
33 | 8, 20, 32 | sylc 65 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+) |
34 | 7, 33 | pm2.61dane 3021 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → 𝑤 ∈ ℝ+) |
35 | 34 | ssd 42168 |
. . 3
⊢ (𝜑 → 𝐷 ⊆
ℝ+) |
36 | | cnrefiisplem.x |
. . . 4
⊢ 𝑋 = inf(𝐷, ℝ*, <
) |
37 | | xrltso 12617 |
. . . . . 6
⊢ < Or
ℝ* |
38 | 37 | a1i 11 |
. . . . 5
⊢ (𝜑 → < Or
ℝ*) |
39 | | snfi 8642 |
. . . . . . . 8
⊢
{(abs‘(ℑ‘𝐴))} ∈ Fin |
40 | 39 | a1i 11 |
. . . . . . 7
⊢ (𝜑 →
{(abs‘(ℑ‘𝐴))} ∈ Fin) |
41 | | cnrefiisplem.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ Fin) |
42 | | inss1 4119 |
. . . . . . . . . . 11
⊢ (𝐵 ∩ ℂ) ⊆ 𝐵 |
43 | 42 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∩ ℂ) ⊆ 𝐵) |
44 | 43 | ssdifssd 4033 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 ∩ ℂ) ∖ {𝐴}) ⊆ 𝐵) |
45 | 41, 44 | ssfid 8819 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 ∩ ℂ) ∖ {𝐴}) ∈ Fin) |
46 | | snfi 8642 |
. . . . . . . . 9
⊢
{(abs‘(𝑦
− 𝐴))} ∈
Fin |
47 | 46 | rgenw 3065 |
. . . . . . . 8
⊢
∀𝑦 ∈
((𝐵 ∩ ℂ) ∖
{𝐴}){(abs‘(𝑦 − 𝐴))} ∈ Fin |
48 | | iunfi 8885 |
. . . . . . . 8
⊢ ((((𝐵 ∩ ℂ) ∖ {𝐴}) ∈ Fin ∧
∀𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))} ∈ Fin) → ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))} ∈ Fin) |
49 | 45, 47, 48 | sylancl 589 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))} ∈ Fin) |
50 | 40, 49 | unfid 42240 |
. . . . . 6
⊢ (𝜑 →
({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))}) ∈ Fin) |
51 | 9, 50 | eqeltrid 2837 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ Fin) |
52 | | fvex 6687 |
. . . . . . . . . 10
⊢
(abs‘(ℑ‘𝐴)) ∈ V |
53 | 52 | snid 4552 |
. . . . . . . . 9
⊢
(abs‘(ℑ‘𝐴)) ∈ {(abs‘(ℑ‘𝐴))} |
54 | | elun1 4066 |
. . . . . . . . 9
⊢
((abs‘(ℑ‘𝐴)) ∈ {(abs‘(ℑ‘𝐴))} →
(abs‘(ℑ‘𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))})) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . 8
⊢
(abs‘(ℑ‘𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))}) |
56 | 55, 9 | eleqtrri 2832 |
. . . . . . 7
⊢
(abs‘(ℑ‘𝐴)) ∈ 𝐷 |
57 | 56 | a1i 11 |
. . . . . 6
⊢ (𝜑 →
(abs‘(ℑ‘𝐴)) ∈ 𝐷) |
58 | 57 | ne0d 4224 |
. . . . 5
⊢ (𝜑 → 𝐷 ≠ ∅) |
59 | | rpssxr 42561 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ* |
60 | 35, 59 | sstrdi 3889 |
. . . . 5
⊢ (𝜑 → 𝐷 ⊆
ℝ*) |
61 | | fiinfcl 9038 |
. . . . 5
⊢ (( <
Or ℝ* ∧ (𝐷 ∈ Fin ∧ 𝐷 ≠ ∅ ∧ 𝐷 ⊆ ℝ*)) →
inf(𝐷, ℝ*,
< ) ∈ 𝐷) |
62 | 38, 51, 58, 60, 61 | syl13anc 1373 |
. . . 4
⊢ (𝜑 → inf(𝐷, ℝ*, < ) ∈ 𝐷) |
63 | 36, 62 | eqeltrid 2837 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
64 | 35, 63 | sseldd 3878 |
. 2
⊢ (𝜑 → 𝑋 ∈
ℝ+) |
65 | 35, 62 | sseldd 3878 |
. . . . . . . . . 10
⊢ (𝜑 → inf(𝐷, ℝ*, < ) ∈
ℝ+) |
66 | 65 | rpred 12514 |
. . . . . . . . 9
⊢ (𝜑 → inf(𝐷, ℝ*, < ) ∈
ℝ) |
67 | 66 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ∈
ℝ) |
68 | 2 | imcld 14644 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℑ‘𝐴) ∈
ℝ) |
69 | 68 | recnd 10747 |
. . . . . . . . . 10
⊢ (𝜑 → (ℑ‘𝐴) ∈
ℂ) |
70 | 69 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘𝐴) ∈
ℂ) |
71 | 70 | abscld 14886 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
(abs‘(ℑ‘𝐴)) ∈ ℝ) |
72 | | recn 10705 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
73 | 72 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
74 | 2 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐴 ∈ ℂ) |
75 | 73, 74 | subcld 11075 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 − 𝐴) ∈ ℂ) |
76 | 75 | abscld 14886 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (abs‘(𝑦 − 𝐴)) ∈ ℝ) |
77 | 60 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐷 ⊆
ℝ*) |
78 | | infxrlb 12810 |
. . . . . . . . 9
⊢ ((𝐷 ⊆ ℝ*
∧ (abs‘(ℑ‘𝐴)) ∈ 𝐷) → inf(𝐷, ℝ*, < ) ≤
(abs‘(ℑ‘𝐴))) |
79 | 77, 56, 78 | sylancl 589 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ≤
(abs‘(ℑ‘𝐴))) |
80 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
81 | 74, 80 | absimlere 42560 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
(abs‘(ℑ‘𝐴)) ≤ (abs‘(𝑦 − 𝐴))) |
82 | 67, 71, 76, 79, 81 | letrd 10875 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ≤
(abs‘(𝑦 − 𝐴))) |
83 | 36, 82 | eqbrtrid 5065 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))) |
84 | 83 | ad4ant14 752 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ 𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))) |
85 | | cnrefiisplem.c |
. . . . . . . . 9
⊢ 𝐶 = (ℝ ∪ 𝐵) |
86 | 85 | eleq2i 2824 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ (ℝ ∪ 𝐵)) |
87 | | elunnel1 4040 |
. . . . . . . 8
⊢ ((𝑦 ∈ (ℝ ∪ 𝐵) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦 ∈ 𝐵) |
88 | 86, 87 | sylanb 584 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐶 ∧ ¬ 𝑦 ∈ ℝ) → 𝑦 ∈ 𝐵) |
89 | 88 | ad4ant24 754 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦 ∈ 𝐵) |
90 | 60 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ 𝑦 ∈ 𝐵) → 𝐷 ⊆
ℝ*) |
91 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
92 | | simpll 767 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
93 | 91, 92 | elind 4084 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ (𝐵 ∩ ℂ)) |
94 | | nelsn 4556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ≠ 𝐴 → ¬ 𝑦 ∈ {𝐴}) |
95 | 94 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦 ∈ {𝐴}) |
96 | 93, 95 | eldifd 3854 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) |
97 | | fvex 6687 |
. . . . . . . . . . . . . . 15
⊢
(abs‘(𝑦
− 𝐴)) ∈
V |
98 | 97 | snid 4552 |
. . . . . . . . . . . . . 14
⊢
(abs‘(𝑦
− 𝐴)) ∈
{(abs‘(𝑦 −
𝐴))} |
99 | | fvoveq1 7193 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑦 → (abs‘(𝑤 − 𝐴)) = (abs‘(𝑦 − 𝐴))) |
100 | 99 | sneqd 4528 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑦 → {(abs‘(𝑤 − 𝐴))} = {(abs‘(𝑦 − 𝐴))}) |
101 | 100 | eliuni 4887 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) ∧ (abs‘(𝑦 − 𝐴)) ∈ {(abs‘(𝑦 − 𝐴))}) → (abs‘(𝑦 − 𝐴)) ∈ ∪ 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤 − 𝐴))}) |
102 | 96, 98, 101 | sylancl 589 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → (abs‘(𝑦 − 𝐴)) ∈ ∪ 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤 − 𝐴))}) |
103 | 100 | cbviunv 4926 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤 − 𝐴))} = ∪
𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))} |
104 | 102, 103 | eleqtrdi 2843 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → (abs‘(𝑦 − 𝐴)) ∈ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))}) |
105 | | elun2 4067 |
. . . . . . . . . . . 12
⊢
((abs‘(𝑦
− 𝐴)) ∈ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))} → (abs‘(𝑦 − 𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))})) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → (abs‘(𝑦 − 𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))})) |
107 | 106, 9 | eleqtrrdi 2844 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → (abs‘(𝑦 − 𝐴)) ∈ 𝐷) |
108 | 107 | adantll 714 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ 𝑦 ∈ 𝐵) → (abs‘(𝑦 − 𝐴)) ∈ 𝐷) |
109 | | infxrlb 12810 |
. . . . . . . . 9
⊢ ((𝐷 ⊆ ℝ*
∧ (abs‘(𝑦 −
𝐴)) ∈ 𝐷) → inf(𝐷, ℝ*, < ) ≤
(abs‘(𝑦 − 𝐴))) |
110 | 90, 108, 109 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ 𝑦 ∈ 𝐵) → inf(𝐷, ℝ*, < ) ≤
(abs‘(𝑦 − 𝐴))) |
111 | 36, 110 | eqbrtrid 5065 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ 𝑦 ∈ 𝐵) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))) |
112 | 111 | adantllr 719 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ 𝑦 ∈ 𝐵) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))) |
113 | 89, 112 | syldan 594 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ ¬ 𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))) |
114 | 84, 113 | pm2.61dan 813 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))) |
115 | 114 | ex 416 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑋 ≤ (abs‘(𝑦 − 𝐴)))) |
116 | 115 | ralrimiva 3096 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑋 ≤ (abs‘(𝑦 − 𝐴)))) |
117 | | breq1 5033 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 ≤ (abs‘(𝑦 − 𝐴)) ↔ 𝑋 ≤ (abs‘(𝑦 − 𝐴)))) |
118 | 117 | imbi2d 344 |
. . . 4
⊢ (𝑥 = 𝑋 → (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑥 ≤ (abs‘(𝑦 − 𝐴))) ↔ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))))) |
119 | 118 | ralbidv 3109 |
. . 3
⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑥 ≤ (abs‘(𝑦 − 𝐴))) ↔ ∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))))) |
120 | 119 | rspcev 3526 |
. 2
⊢ ((𝑋 ∈ ℝ+
∧ ∀𝑦 ∈
𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑋 ≤ (abs‘(𝑦 − 𝐴)))) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑥 ≤ (abs‘(𝑦 − 𝐴)))) |
121 | 64, 116, 120 | syl2anc 587 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑥 ≤ (abs‘(𝑦 − 𝐴)))) |