| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 = (abs‘(ℑ‘𝐴))) |
| 2 | | cnrefiisplem.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 3 | | cnrefiisplem.n |
. . . . . . . . 9
⊢ (𝜑 → ¬ 𝐴 ∈ ℝ) |
| 4 | 2, 3 | absimnre 45487 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘(ℑ‘𝐴)) ∈
ℝ+) |
| 5 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 = (abs‘(ℑ‘𝐴))) →
(abs‘(ℑ‘𝐴)) ∈
ℝ+) |
| 6 | 1, 5 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+) |
| 7 | 6 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐷) ∧ 𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+) |
| 8 | | simpll 767 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝜑) |
| 9 | | cnrefiisplem.d |
. . . . . . . . . . . 12
⊢ 𝐷 =
({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))}) |
| 10 | 9 | eleq2i 2833 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝐷 ↔ 𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))})) |
| 11 | 10 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝐷 → 𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))})) |
| 12 | | nelsn 4666 |
. . . . . . . . . 10
⊢ (𝑤 ≠
(abs‘(ℑ‘𝐴)) → ¬ 𝑤 ∈ {(abs‘(ℑ‘𝐴))}) |
| 13 | | elunnel1 4154 |
. . . . . . . . . 10
⊢ ((𝑤 ∈
({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))}) ∧ ¬ 𝑤 ∈ {(abs‘(ℑ‘𝐴))}) → 𝑤 ∈ ∪
𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))}) |
| 14 | 11, 12, 13 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝑤 ∈ 𝐷 ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ∪
𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))}) |
| 15 | | eliun 4995 |
. . . . . . . . 9
⊢ (𝑤 ∈ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))} ↔ ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦 − 𝐴))}) |
| 16 | 14, 15 | sylib 218 |
. . . . . . . 8
⊢ ((𝑤 ∈ 𝐷 ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦 − 𝐴))}) |
| 17 | | velsn 4642 |
. . . . . . . . 9
⊢ (𝑤 ∈ {(abs‘(𝑦 − 𝐴))} ↔ 𝑤 = (abs‘(𝑦 − 𝐴))) |
| 18 | 17 | rexbii 3094 |
. . . . . . . 8
⊢
(∃𝑦 ∈
((𝐵 ∩ ℂ) ∖
{𝐴})𝑤 ∈ {(abs‘(𝑦 − 𝐴))} ↔ ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦 − 𝐴))) |
| 19 | 16, 18 | sylib 218 |
. . . . . . 7
⊢ ((𝑤 ∈ 𝐷 ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦 − 𝐴))) |
| 20 | 19 | adantll 714 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦 − 𝐴))) |
| 21 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → 𝑤 = (abs‘(𝑦 − 𝐴))) |
| 22 | | eldifi 4131 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦 ∈ (𝐵 ∩ ℂ)) |
| 23 | 22 | elin2d 4205 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦 ∈ ℂ) |
| 24 | 23 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → 𝑦 ∈ ℂ) |
| 25 | 2 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → 𝐴 ∈ ℂ) |
| 26 | 24, 25 | subcld 11620 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → (𝑦 − 𝐴) ∈ ℂ) |
| 27 | | eldifsni 4790 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦 ≠ 𝐴) |
| 28 | 27 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → 𝑦 ≠ 𝐴) |
| 29 | 24, 25, 28 | subne0d 11629 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → (𝑦 − 𝐴) ≠ 0) |
| 30 | 26, 29 | absrpcld 15487 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → (abs‘(𝑦 − 𝐴)) ∈
ℝ+) |
| 31 | 21, 30 | eqeltrd 2841 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦 − 𝐴))) → 𝑤 ∈ ℝ+) |
| 32 | 31 | rexlimdva2 3157 |
. . . . . 6
⊢ (𝜑 → (∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦 − 𝐴)) → 𝑤 ∈
ℝ+)) |
| 33 | 8, 20, 32 | sylc 65 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+) |
| 34 | 7, 33 | pm2.61dane 3029 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → 𝑤 ∈ ℝ+) |
| 35 | 34 | ssd 45085 |
. . 3
⊢ (𝜑 → 𝐷 ⊆
ℝ+) |
| 36 | | cnrefiisplem.x |
. . . 4
⊢ 𝑋 = inf(𝐷, ℝ*, <
) |
| 37 | | xrltso 13183 |
. . . . . 6
⊢ < Or
ℝ* |
| 38 | 37 | a1i 11 |
. . . . 5
⊢ (𝜑 → < Or
ℝ*) |
| 39 | | snfi 9083 |
. . . . . . . 8
⊢
{(abs‘(ℑ‘𝐴))} ∈ Fin |
| 40 | 39 | a1i 11 |
. . . . . . 7
⊢ (𝜑 →
{(abs‘(ℑ‘𝐴))} ∈ Fin) |
| 41 | | cnrefiisplem.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ Fin) |
| 42 | | inss1 4237 |
. . . . . . . . . . 11
⊢ (𝐵 ∩ ℂ) ⊆ 𝐵 |
| 43 | 42 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∩ ℂ) ⊆ 𝐵) |
| 44 | 43 | ssdifssd 4147 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 ∩ ℂ) ∖ {𝐴}) ⊆ 𝐵) |
| 45 | 41, 44 | ssfid 9301 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 ∩ ℂ) ∖ {𝐴}) ∈ Fin) |
| 46 | | snfi 9083 |
. . . . . . . . 9
⊢
{(abs‘(𝑦
− 𝐴))} ∈
Fin |
| 47 | 46 | rgenw 3065 |
. . . . . . . 8
⊢
∀𝑦 ∈
((𝐵 ∩ ℂ) ∖
{𝐴}){(abs‘(𝑦 − 𝐴))} ∈ Fin |
| 48 | | iunfi 9383 |
. . . . . . . 8
⊢ ((((𝐵 ∩ ℂ) ∖ {𝐴}) ∈ Fin ∧
∀𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))} ∈ Fin) → ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))} ∈ Fin) |
| 49 | 45, 47, 48 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))} ∈ Fin) |
| 50 | 40, 49 | unfid 9212 |
. . . . . 6
⊢ (𝜑 →
({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))}) ∈ Fin) |
| 51 | 9, 50 | eqeltrid 2845 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ Fin) |
| 52 | | fvex 6919 |
. . . . . . . . . 10
⊢
(abs‘(ℑ‘𝐴)) ∈ V |
| 53 | 52 | snid 4662 |
. . . . . . . . 9
⊢
(abs‘(ℑ‘𝐴)) ∈ {(abs‘(ℑ‘𝐴))} |
| 54 | | elun1 4182 |
. . . . . . . . 9
⊢
((abs‘(ℑ‘𝐴)) ∈ {(abs‘(ℑ‘𝐴))} →
(abs‘(ℑ‘𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))})) |
| 55 | 53, 54 | ax-mp 5 |
. . . . . . . 8
⊢
(abs‘(ℑ‘𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))}) |
| 56 | 55, 9 | eleqtrri 2840 |
. . . . . . 7
⊢
(abs‘(ℑ‘𝐴)) ∈ 𝐷 |
| 57 | 56 | a1i 11 |
. . . . . 6
⊢ (𝜑 →
(abs‘(ℑ‘𝐴)) ∈ 𝐷) |
| 58 | 57 | ne0d 4342 |
. . . . 5
⊢ (𝜑 → 𝐷 ≠ ∅) |
| 59 | | rpssxr 45491 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ* |
| 60 | 35, 59 | sstrdi 3996 |
. . . . 5
⊢ (𝜑 → 𝐷 ⊆
ℝ*) |
| 61 | | fiinfcl 9541 |
. . . . 5
⊢ (( <
Or ℝ* ∧ (𝐷 ∈ Fin ∧ 𝐷 ≠ ∅ ∧ 𝐷 ⊆ ℝ*)) →
inf(𝐷, ℝ*,
< ) ∈ 𝐷) |
| 62 | 38, 51, 58, 60, 61 | syl13anc 1374 |
. . . 4
⊢ (𝜑 → inf(𝐷, ℝ*, < ) ∈ 𝐷) |
| 63 | 36, 62 | eqeltrid 2845 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
| 64 | 35, 63 | sseldd 3984 |
. 2
⊢ (𝜑 → 𝑋 ∈
ℝ+) |
| 65 | 35, 62 | sseldd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → inf(𝐷, ℝ*, < ) ∈
ℝ+) |
| 66 | 65 | rpred 13077 |
. . . . . . . . 9
⊢ (𝜑 → inf(𝐷, ℝ*, < ) ∈
ℝ) |
| 67 | 66 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ∈
ℝ) |
| 68 | 2 | imcld 15234 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℑ‘𝐴) ∈
ℝ) |
| 69 | 68 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → (ℑ‘𝐴) ∈
ℂ) |
| 70 | 69 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘𝐴) ∈
ℂ) |
| 71 | 70 | abscld 15475 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
(abs‘(ℑ‘𝐴)) ∈ ℝ) |
| 72 | | recn 11245 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
| 73 | 72 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
| 74 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐴 ∈ ℂ) |
| 75 | 73, 74 | subcld 11620 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 − 𝐴) ∈ ℂ) |
| 76 | 75 | abscld 15475 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (abs‘(𝑦 − 𝐴)) ∈ ℝ) |
| 77 | 60 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐷 ⊆
ℝ*) |
| 78 | | infxrlb 13376 |
. . . . . . . . 9
⊢ ((𝐷 ⊆ ℝ*
∧ (abs‘(ℑ‘𝐴)) ∈ 𝐷) → inf(𝐷, ℝ*, < ) ≤
(abs‘(ℑ‘𝐴))) |
| 79 | 77, 56, 78 | sylancl 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ≤
(abs‘(ℑ‘𝐴))) |
| 80 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
| 81 | 74, 80 | absimlere 45490 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
(abs‘(ℑ‘𝐴)) ≤ (abs‘(𝑦 − 𝐴))) |
| 82 | 67, 71, 76, 79, 81 | letrd 11418 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ≤
(abs‘(𝑦 − 𝐴))) |
| 83 | 36, 82 | eqbrtrid 5178 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))) |
| 84 | 83 | ad4ant14 752 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ 𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))) |
| 85 | | cnrefiisplem.c |
. . . . . . . . 9
⊢ 𝐶 = (ℝ ∪ 𝐵) |
| 86 | 85 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ (ℝ ∪ 𝐵)) |
| 87 | | elunnel1 4154 |
. . . . . . . 8
⊢ ((𝑦 ∈ (ℝ ∪ 𝐵) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦 ∈ 𝐵) |
| 88 | 86, 87 | sylanb 581 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐶 ∧ ¬ 𝑦 ∈ ℝ) → 𝑦 ∈ 𝐵) |
| 89 | 88 | ad4ant24 754 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦 ∈ 𝐵) |
| 90 | 60 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ 𝑦 ∈ 𝐵) → 𝐷 ⊆
ℝ*) |
| 91 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
| 92 | | simpll 767 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
| 93 | 91, 92 | elind 4200 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ (𝐵 ∩ ℂ)) |
| 94 | | nelsn 4666 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ≠ 𝐴 → ¬ 𝑦 ∈ {𝐴}) |
| 95 | 94 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦 ∈ {𝐴}) |
| 96 | 93, 95 | eldifd 3962 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) |
| 97 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢
(abs‘(𝑦
− 𝐴)) ∈
V |
| 98 | 97 | snid 4662 |
. . . . . . . . . . . . . 14
⊢
(abs‘(𝑦
− 𝐴)) ∈
{(abs‘(𝑦 −
𝐴))} |
| 99 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑦 → (abs‘(𝑤 − 𝐴)) = (abs‘(𝑦 − 𝐴))) |
| 100 | 99 | sneqd 4638 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑦 → {(abs‘(𝑤 − 𝐴))} = {(abs‘(𝑦 − 𝐴))}) |
| 101 | 100 | eliuni 4997 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) ∧ (abs‘(𝑦 − 𝐴)) ∈ {(abs‘(𝑦 − 𝐴))}) → (abs‘(𝑦 − 𝐴)) ∈ ∪ 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤 − 𝐴))}) |
| 102 | 96, 98, 101 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → (abs‘(𝑦 − 𝐴)) ∈ ∪ 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤 − 𝐴))}) |
| 103 | 100 | cbviunv 5040 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤 − 𝐴))} = ∪
𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))} |
| 104 | 102, 103 | eleqtrdi 2851 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → (abs‘(𝑦 − 𝐴)) ∈ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))}) |
| 105 | | elun2 4183 |
. . . . . . . . . . . 12
⊢
((abs‘(𝑦
− 𝐴)) ∈ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))} → (abs‘(𝑦 − 𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))})) |
| 106 | 104, 105 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → (abs‘(𝑦 − 𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))})) |
| 107 | 106, 9 | eleqtrrdi 2852 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) ∧ 𝑦 ∈ 𝐵) → (abs‘(𝑦 − 𝐴)) ∈ 𝐷) |
| 108 | 107 | adantll 714 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ 𝑦 ∈ 𝐵) → (abs‘(𝑦 − 𝐴)) ∈ 𝐷) |
| 109 | | infxrlb 13376 |
. . . . . . . . 9
⊢ ((𝐷 ⊆ ℝ*
∧ (abs‘(𝑦 −
𝐴)) ∈ 𝐷) → inf(𝐷, ℝ*, < ) ≤
(abs‘(𝑦 − 𝐴))) |
| 110 | 90, 108, 109 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ 𝑦 ∈ 𝐵) → inf(𝐷, ℝ*, < ) ≤
(abs‘(𝑦 − 𝐴))) |
| 111 | 36, 110 | eqbrtrid 5178 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ 𝑦 ∈ 𝐵) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))) |
| 112 | 111 | adantllr 719 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ 𝑦 ∈ 𝐵) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))) |
| 113 | 89, 112 | syldan 591 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) ∧ ¬ 𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))) |
| 114 | 84, 113 | pm2.61dan 813 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴)) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))) |
| 115 | 114 | ex 412 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑋 ≤ (abs‘(𝑦 − 𝐴)))) |
| 116 | 115 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑋 ≤ (abs‘(𝑦 − 𝐴)))) |
| 117 | | breq1 5146 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 ≤ (abs‘(𝑦 − 𝐴)) ↔ 𝑋 ≤ (abs‘(𝑦 − 𝐴)))) |
| 118 | 117 | imbi2d 340 |
. . . 4
⊢ (𝑥 = 𝑋 → (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑥 ≤ (abs‘(𝑦 − 𝐴))) ↔ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))))) |
| 119 | 118 | ralbidv 3178 |
. . 3
⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑥 ≤ (abs‘(𝑦 − 𝐴))) ↔ ∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑋 ≤ (abs‘(𝑦 − 𝐴))))) |
| 120 | 119 | rspcev 3622 |
. 2
⊢ ((𝑋 ∈ ℝ+
∧ ∀𝑦 ∈
𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑋 ≤ (abs‘(𝑦 − 𝐴)))) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑥 ≤ (abs‘(𝑦 − 𝐴)))) |
| 121 | 64, 116, 120 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑥 ≤ (abs‘(𝑦 − 𝐴)))) |