Metamath Proof Explorer

Theorem cnrefiisplem

Description: Lemma for cnrefiisp (some local definitions are used). (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses cnrefiisplem.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
cnrefiisplem.n ⊢ ( 𝜑 → ¬ 𝐴 ∈ ℝ )
cnrefiisplem.b ⊢ ( 𝜑 → 𝐵 ∈ Fin )
cnrefiisplem.c ⊢ 𝐶 = ( ℝ ∪ 𝐵 )
cnrefiisplem.d ⊢ 𝐷 = ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } )
cnrefiisplem.x ⊢ 𝑋 = inf ( 𝐷 , ℝ* , < )
Assertion cnrefiisplem ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝐶 ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 cnrefiisplem.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 cnrefiisplem.n ⊢ ( 𝜑 → ¬ 𝐴 ∈ ℝ )
3 cnrefiisplem.b ⊢ ( 𝜑 → 𝐵 ∈ Fin )
4 cnrefiisplem.c ⊢ 𝐶 = ( ℝ ∪ 𝐵 )
5 cnrefiisplem.d ⊢ 𝐷 = ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } )
6 cnrefiisplem.x ⊢ 𝑋 = inf ( 𝐷 , ℝ* , < )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑤 = ( abs ‘ ( ℑ ‘ 𝐴 ) ) ) → 𝑤 = ( abs ‘ ( ℑ ‘ 𝐴 ) ) )
8 1 2 absimnre ⊢ ( 𝜑 → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ ℝ+ )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑤 = ( abs ‘ ( ℑ ‘ 𝐴 ) ) ) → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ ℝ+ )
10 7 9 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑤 = ( abs ‘ ( ℑ ‘ 𝐴 ) ) ) → 𝑤 ∈ ℝ+ )
11 10 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑤 = ( abs ‘ ( ℑ ‘ 𝐴 ) ) ) → 𝑤 ∈ ℝ+ )
12 simpll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑤 ≠ ( abs ‘ ( ℑ ‘ 𝐴 ) ) ) → 𝜑 )
13 5 eleq2i ⊢ ( 𝑤 ∈ 𝐷 ↔ 𝑤 ∈ ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ) )
14 13 biimpi ⊢ ( 𝑤 ∈ 𝐷 → 𝑤 ∈ ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ) )
15 nelsn ⊢ ( 𝑤 ≠ ( abs ‘ ( ℑ ‘ 𝐴 ) ) → ¬ 𝑤 ∈ { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } )
16 elunnel1 ⊢ ( ( 𝑤 ∈ ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ) ∧ ¬ 𝑤 ∈ { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ) → 𝑤 ∈ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } )
17 14 15 16 syl2an ⊢ ( ( 𝑤 ∈ 𝐷 ∧ 𝑤 ≠ ( abs ‘ ( ℑ ‘ 𝐴 ) ) ) → 𝑤 ∈ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } )
18 eliun ⊢ ( 𝑤 ∈ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ↔ ∃ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) 𝑤 ∈ { ( abs ‘ ( 𝑦 − 𝐴 ) ) } )
19 17 18 sylib ⊢ ( ( 𝑤 ∈ 𝐷 ∧ 𝑤 ≠ ( abs ‘ ( ℑ ‘ 𝐴 ) ) ) → ∃ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) 𝑤 ∈ { ( abs ‘ ( 𝑦 − 𝐴 ) ) } )
20 velsn ⊢ ( 𝑤 ∈ { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ↔ 𝑤 = ( abs ‘ ( 𝑦 − 𝐴 ) ) )
21 20 rexbii ⊢ ( ∃ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) 𝑤 ∈ { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ↔ ∃ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) 𝑤 = ( abs ‘ ( 𝑦 − 𝐴 ) ) )
22 19 21 sylib ⊢ ( ( 𝑤 ∈ 𝐷 ∧ 𝑤 ≠ ( abs ‘ ( ℑ ‘ 𝐴 ) ) ) → ∃ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) 𝑤 = ( abs ‘ ( 𝑦 − 𝐴 ) ) )
23 22 adantll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑤 ≠ ( abs ‘ ( ℑ ‘ 𝐴 ) ) ) → ∃ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) 𝑤 = ( abs ‘ ( 𝑦 − 𝐴 ) ) )
24 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) ) ∧ 𝑤 = ( abs ‘ ( 𝑦 − 𝐴 ) ) ) → 𝑤 = ( abs ‘ ( 𝑦 − 𝐴 ) ) )
25 eldifi ⊢ ( 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) → 𝑦 ∈ ( 𝐵 ∩ ℂ ) )
26 25 elin2d ⊢ ( 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) → 𝑦 ∈ ℂ )
27 26 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) ) ∧ 𝑤 = ( abs ‘ ( 𝑦 − 𝐴 ) ) ) → 𝑦 ∈ ℂ )
28 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) ) ∧ 𝑤 = ( abs ‘ ( 𝑦 − 𝐴 ) ) ) → 𝐴 ∈ ℂ )
29 27 28 subcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) ) ∧ 𝑤 = ( abs ‘ ( 𝑦 − 𝐴 ) ) ) → ( 𝑦 − 𝐴 ) ∈ ℂ )
30 eldifsni ⊢ ( 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) → 𝑦 ≠ 𝐴 )
31 30 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) ) ∧ 𝑤 = ( abs ‘ ( 𝑦 − 𝐴 ) ) ) → 𝑦 ≠ 𝐴 )
32 27 28 31 subne0d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) ) ∧ 𝑤 = ( abs ‘ ( 𝑦 − 𝐴 ) ) ) → ( 𝑦 − 𝐴 ) ≠ 0 )
33 29 32 absrpcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) ) ∧ 𝑤 = ( abs ‘ ( 𝑦 − 𝐴 ) ) ) → ( abs ‘ ( 𝑦 − 𝐴 ) ) ∈ ℝ+ )
34 24 33 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) ) ∧ 𝑤 = ( abs ‘ ( 𝑦 − 𝐴 ) ) ) → 𝑤 ∈ ℝ+ )
35 34 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) 𝑤 = ( abs ‘ ( 𝑦 − 𝐴 ) ) → 𝑤 ∈ ℝ+ ) )
36 12 23 35 sylc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑤 ≠ ( abs ‘ ( ℑ ‘ 𝐴 ) ) ) → 𝑤 ∈ ℝ+ )
37 11 36 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐷 ) → 𝑤 ∈ ℝ+ )
38 37 ssd ⊢ ( 𝜑 → 𝐷 ⊆ ℝ+ )
39 xrltso ⊢ < Or ℝ*
40 39 a1i ⊢ ( 𝜑 → < Or ℝ* )
41 snfi ⊢ { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∈ Fin
42 41 a1i ⊢ ( 𝜑 → { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∈ Fin )
43 inss1 ⊢ ( 𝐵 ∩ ℂ ) ⊆ 𝐵
44 43 a1i ⊢ ( 𝜑 → ( 𝐵 ∩ ℂ ) ⊆ 𝐵 )
45 44 ssdifssd ⊢ ( 𝜑 → ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) ⊆ 𝐵 )
46 3 45 ssfid ⊢ ( 𝜑 → ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) ∈ Fin )
47 snfi ⊢ { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ∈ Fin
48 47 rgenw ⊢ ∀ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ∈ Fin
49 iunfi ⊢ ( ( ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) ∈ Fin ∧ ∀ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ∈ Fin ) → ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ∈ Fin )
50 46 48 49 sylancl ⊢ ( 𝜑 → ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ∈ Fin )
51 42 50 unfid ⊢ ( 𝜑 → ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ) ∈ Fin )
52 5 51 eqeltrid ⊢ ( 𝜑 → 𝐷 ∈ Fin )
53 fvex ⊢ ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ V
54 53 snid ⊢ ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ { ( abs ‘ ( ℑ ‘ 𝐴 ) ) }
55 elun1 ⊢ ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ) )
56 54 55 ax-mp ⊢ ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } )
57 56 5 eleqtrri ⊢ ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ 𝐷
58 57 a1i ⊢ ( 𝜑 → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ 𝐷 )
59 58 ne0d ⊢ ( 𝜑 → 𝐷 ≠ ∅ )
60 rpssxr ⊢ ℝ+ ⊆ ℝ*
61 38 60 sstrdi ⊢ ( 𝜑 → 𝐷 ⊆ ℝ* )
62 fiinfcl ⊢ ( ( < Or ℝ* ∧ ( 𝐷 ∈ Fin ∧ 𝐷 ≠ ∅ ∧ 𝐷 ⊆ ℝ* ) ) → inf ( 𝐷 , ℝ* , < ) ∈ 𝐷 )
63 40 52 59 61 62 syl13anc ⊢ ( 𝜑 → inf ( 𝐷 , ℝ* , < ) ∈ 𝐷 )
64 6 63 eqeltrid ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
65 38 64 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
66 38 63 sseldd ⊢ ( 𝜑 → inf ( 𝐷 , ℝ* , < ) ∈ ℝ+ )
67 66 rpred ⊢ ( 𝜑 → inf ( 𝐷 , ℝ* , < ) ∈ ℝ )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → inf ( 𝐷 , ℝ* , < ) ∈ ℝ )
69 1 imcld ⊢ ( 𝜑 → ( ℑ ‘ 𝐴 ) ∈ ℝ )
70 69 recnd ⊢ ( 𝜑 → ( ℑ ‘ 𝐴 ) ∈ ℂ )
71 70 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ 𝐴 ) ∈ ℂ )
72 71 abscld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ ℝ )
73 recn ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
74 73 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
75 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐴 ∈ ℂ )
76 74 75 subcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 − 𝐴 ) ∈ ℂ )
77 76 abscld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( 𝑦 − 𝐴 ) ) ∈ ℝ )
78 61 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐷 ⊆ ℝ* )
79 infxrlb ⊢ ( ( 𝐷 ⊆ ℝ* ∧ ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ 𝐷 ) → inf ( 𝐷 , ℝ* , < ) ≤ ( abs ‘ ( ℑ ‘ 𝐴 ) ) )
80 78 57 79 sylancl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → inf ( 𝐷 , ℝ* , < ) ≤ ( abs ‘ ( ℑ ‘ 𝐴 ) ) )
81 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
82 75 81 absimlere ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) )
83 68 72 77 80 82 letrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → inf ( 𝐷 , ℝ* , < ) ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) )
84 6 83 eqbrtrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑋 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) )
85 84 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ) ∧ 𝑦 ∈ ℝ ) → 𝑋 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) )
86 4 eleq2i ⊢ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ( ℝ ∪ 𝐵 ) )
87 elunnel1 ⊢ ( ( 𝑦 ∈ ( ℝ ∪ 𝐵 ) ∧ ¬ 𝑦 ∈ ℝ ) → 𝑦 ∈ 𝐵 )
88 86 87 sylanb ⊢ ( ( 𝑦 ∈ 𝐶 ∧ ¬ 𝑦 ∈ ℝ ) → 𝑦 ∈ 𝐵 )
89 88 ad4ant24 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ) ∧ ¬ 𝑦 ∈ ℝ ) → 𝑦 ∈ 𝐵 )
90 61 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ⊆ ℝ* )
91 simpr ⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
92 simpll ⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℂ )
93 91 92 elind ⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ( 𝐵 ∩ ℂ ) )
94 nelsn ⊢ ( 𝑦 ≠ 𝐴 → ¬ 𝑦 ∈ { 𝐴 } )
95 94 ad2antlr ⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ¬ 𝑦 ∈ { 𝐴 } )
96 93 95 eldifd ⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) )
97 fvex ⊢ ( abs ‘ ( 𝑦 − 𝐴 ) ) ∈ V
98 97 snid ⊢ ( abs ‘ ( 𝑦 − 𝐴 ) ) ∈ { ( abs ‘ ( 𝑦 − 𝐴 ) ) }
99 fvoveq1 ⊢ ( 𝑤 = 𝑦 → ( abs ‘ ( 𝑤 − 𝐴 ) ) = ( abs ‘ ( 𝑦 − 𝐴 ) ) )
100 99 sneqd ⊢ ( 𝑤 = 𝑦 → { ( abs ‘ ( 𝑤 − 𝐴 ) ) } = { ( abs ‘ ( 𝑦 − 𝐴 ) ) } )
101 100 eliuni ⊢ ( ( 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) ∈ { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ) → ( abs ‘ ( 𝑦 − 𝐴 ) ) ∈ ∪ 𝑤 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑤 − 𝐴 ) ) } )
102 96 98 101 sylancl ⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( abs ‘ ( 𝑦 − 𝐴 ) ) ∈ ∪ 𝑤 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑤 − 𝐴 ) ) } )
103 100 cbviunv ⊢ ∪ 𝑤 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑤 − 𝐴 ) ) } = ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) }
104 102 103 eleqtrdi ⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( abs ‘ ( 𝑦 − 𝐴 ) ) ∈ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } )
105 elun2 ⊢ ( ( abs ‘ ( 𝑦 − 𝐴 ) ) ∈ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } → ( abs ‘ ( 𝑦 − 𝐴 ) ) ∈ ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ) )
106 104 105 syl ⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( abs ‘ ( 𝑦 − 𝐴 ) ) ∈ ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑦 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑦 − 𝐴 ) ) } ) )
107 106 5 eleqtrrdi ⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( abs ‘ ( 𝑦 − 𝐴 ) ) ∈ 𝐷 )
108 107 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( abs ‘ ( 𝑦 − 𝐴 ) ) ∈ 𝐷 )
109 infxrlb ⊢ ( ( 𝐷 ⊆ ℝ* ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) ∈ 𝐷 ) → inf ( 𝐷 , ℝ* , < ) ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) )
110 90 108 109 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ) ∧ 𝑦 ∈ 𝐵 ) → inf ( 𝐷 , ℝ* , < ) ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) )
111 6 110 eqbrtrid ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑋 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) )
112 111 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑋 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) )
113 89 112 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ) ∧ ¬ 𝑦 ∈ ℝ ) → 𝑋 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) )
114 85 113 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ) → 𝑋 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) )
115 114 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑋 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) )
116 115 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐶 ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑋 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) )
117 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ↔ 𝑋 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) )
118 117 imbi2d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ↔ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑋 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) )
119 118 ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑦 ∈ 𝐶 ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ↔ ∀ 𝑦 ∈ 𝐶 ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑋 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) )
120 119 rspcev ⊢ ( ( 𝑋 ∈ ℝ+ ∧ ∀ 𝑦 ∈ 𝐶 ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑋 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝐶 ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) )
121 65 116 120 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝐶 ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) )