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 
|- ( ph -> A e. CC )
cnrefiisplem.n 
|- ( ph -> -. A e. RR )
cnrefiisplem.b 
|- ( ph -> B e. Fin )
cnrefiisplem.c 
|- C = ( RR u. B )
cnrefiisplem.d 
|- D = ( { ( abs ` ( Im ` A ) ) } u. U_ y e. ( ( B i^i CC ) \ { A } ) { ( abs ` ( y - A ) ) } )
cnrefiisplem.x 
|- X = inf ( D , RR* , < )
Assertion cnrefiisplem 
|- ( ph -> E. x e. RR+ A. y e. C ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) )

Proof

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