Metamath Proof Explorer


Theorem blcvx

Description: An open ball in the complex numbers is a convex set. (Contributed by Mario Carneiro, 12-Feb-2015) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypothesis blcvx.s S = P ball abs R
Assertion blcvx P R * A S B S T 0 1 T A + 1 T B S

Proof

Step Hyp Ref Expression
1 blcvx.s S = P ball abs R
2 simpr3 P R * A S B S T 0 1 T 0 1
3 elicc01 T 0 1 T 0 T T 1
4 2 3 sylib P R * A S B S T 0 1 T 0 T T 1
5 4 simp1d P R * A S B S T 0 1 T
6 5 recnd P R * A S B S T 0 1 T
7 simpr1 P R * A S B S T 0 1 A S
8 7 1 eleqtrdi P R * A S B S T 0 1 A P ball abs R
9 cnxmet abs ∞Met
10 simpll P R * A S B S T 0 1 P
11 simplr P R * A S B S T 0 1 R *
12 elbl abs ∞Met P R * A P ball abs R A P abs A < R
13 9 10 11 12 mp3an2i P R * A S B S T 0 1 A P ball abs R A P abs A < R
14 8 13 mpbid P R * A S B S T 0 1 A P abs A < R
15 14 simpld P R * A S B S T 0 1 A
16 6 15 mulcld P R * A S B S T 0 1 T A
17 1re 1
18 resubcl 1 T 1 T
19 17 5 18 sylancr P R * A S B S T 0 1 1 T
20 19 recnd P R * A S B S T 0 1 1 T
21 simpr2 P R * A S B S T 0 1 B S
22 21 1 eleqtrdi P R * A S B S T 0 1 B P ball abs R
23 elbl abs ∞Met P R * B P ball abs R B P abs B < R
24 9 10 11 23 mp3an2i P R * A S B S T 0 1 B P ball abs R B P abs B < R
25 22 24 mpbid P R * A S B S T 0 1 B P abs B < R
26 25 simpld P R * A S B S T 0 1 B
27 20 26 mulcld P R * A S B S T 0 1 1 T B
28 16 27 addcld P R * A S B S T 0 1 T A + 1 T B
29 eqid abs = abs
30 29 cnmetdval P T A + 1 T B P abs T A + 1 T B = P T A + 1 T B
31 10 28 30 syl2anc P R * A S B S T 0 1 P abs T A + 1 T B = P T A + 1 T B
32 6 10 15 subdid P R * A S B S T 0 1 T P A = T P T A
33 20 10 26 subdid P R * A S B S T 0 1 1 T P B = 1 T P 1 T B
34 32 33 oveq12d P R * A S B S T 0 1 T P A + 1 T P B = T P T A + 1 T P - 1 T B
35 6 10 mulcld P R * A S B S T 0 1 T P
36 20 10 mulcld P R * A S B S T 0 1 1 T P
37 35 36 16 27 addsub4d P R * A S B S T 0 1 T P + 1 T P - T A + 1 T B = T P T A + 1 T P - 1 T B
38 ax-1cn 1
39 pncan3 T 1 T + 1 - T = 1
40 6 38 39 sylancl P R * A S B S T 0 1 T + 1 - T = 1
41 40 oveq1d P R * A S B S T 0 1 T + 1 - T P = 1 P
42 6 20 10 adddird P R * A S B S T 0 1 T + 1 - T P = T P + 1 T P
43 mulid2 P 1 P = P
44 43 ad2antrr P R * A S B S T 0 1 1 P = P
45 41 42 44 3eqtr3d P R * A S B S T 0 1 T P + 1 T P = P
46 45 oveq1d P R * A S B S T 0 1 T P + 1 T P - T A + 1 T B = P T A + 1 T B
47 34 37 46 3eqtr2d P R * A S B S T 0 1 T P A + 1 T P B = P T A + 1 T B
48 47 fveq2d P R * A S B S T 0 1 T P A + 1 T P B = P T A + 1 T B
49 31 48 eqtr4d P R * A S B S T 0 1 P abs T A + 1 T B = T P A + 1 T P B
50 10 15 subcld P R * A S B S T 0 1 P A
51 6 50 mulcld P R * A S B S T 0 1 T P A
52 10 26 subcld P R * A S B S T 0 1 P B
53 20 52 mulcld P R * A S B S T 0 1 1 T P B
54 51 53 addcld P R * A S B S T 0 1 T P A + 1 T P B
55 54 abscld P R * A S B S T 0 1 T P A + 1 T P B
56 55 adantr P R * A S B S T 0 1 R T P A + 1 T P B
57 51 abscld P R * A S B S T 0 1 T P A
58 53 abscld P R * A S B S T 0 1 1 T P B
59 57 58 readdcld P R * A S B S T 0 1 T P A + 1 T P B
60 59 adantr P R * A S B S T 0 1 R T P A + 1 T P B
61 simpr P R * A S B S T 0 1 R R
62 51 53 abstrid P R * A S B S T 0 1 T P A + 1 T P B T P A + 1 T P B
63 62 adantr P R * A S B S T 0 1 R T P A + 1 T P B T P A + 1 T P B
64 oveq1 T = 0 T P A = 0 P A
65 50 mul02d P R * A S B S T 0 1 0 P A = 0
66 64 65 sylan9eqr P R * A S B S T 0 1 T = 0 T P A = 0
67 66 abs00bd P R * A S B S T 0 1 T = 0 T P A = 0
68 oveq2 T = 0 1 T = 1 0
69 1m0e1 1 0 = 1
70 68 69 eqtrdi T = 0 1 T = 1
71 70 oveq1d T = 0 1 T P B = 1 P B
72 52 mulid2d P R * A S B S T 0 1 1 P B = P B
73 71 72 sylan9eqr P R * A S B S T 0 1 T = 0 1 T P B = P B
74 73 fveq2d P R * A S B S T 0 1 T = 0 1 T P B = P B
75 67 74 oveq12d P R * A S B S T 0 1 T = 0 T P A + 1 T P B = 0 + P B
76 52 abscld P R * A S B S T 0 1 P B
77 76 recnd P R * A S B S T 0 1 P B
78 77 addid2d P R * A S B S T 0 1 0 + P B = P B
79 29 cnmetdval P B P abs B = P B
80 10 26 79 syl2anc P R * A S B S T 0 1 P abs B = P B
81 78 80 eqtr4d P R * A S B S T 0 1 0 + P B = P abs B
82 25 simprd P R * A S B S T 0 1 P abs B < R
83 81 82 eqbrtrd P R * A S B S T 0 1 0 + P B < R
84 83 adantr P R * A S B S T 0 1 T = 0 0 + P B < R
85 75 84 eqbrtrd P R * A S B S T 0 1 T = 0 T P A + 1 T P B < R
86 85 adantlr P R * A S B S T 0 1 R T = 0 T P A + 1 T P B < R
87 6 50 absmuld P R * A S B S T 0 1 T P A = T P A
88 4 simp2d P R * A S B S T 0 1 0 T
89 5 88 absidd P R * A S B S T 0 1 T = T
90 89 oveq1d P R * A S B S T 0 1 T P A = T P A
91 87 90 eqtrd P R * A S B S T 0 1 T P A = T P A
92 91 ad2antrr P R * A S B S T 0 1 R T 0 T P A = T P A
93 29 cnmetdval P A P abs A = P A
94 10 15 93 syl2anc P R * A S B S T 0 1 P abs A = P A
95 14 simprd P R * A S B S T 0 1 P abs A < R
96 94 95 eqbrtrrd P R * A S B S T 0 1 P A < R
97 96 ad2antrr P R * A S B S T 0 1 R T 0 P A < R
98 50 abscld P R * A S B S T 0 1 P A
99 98 ad2antrr P R * A S B S T 0 1 R T 0 P A
100 simplr P R * A S B S T 0 1 R T 0 R
101 5 ad2antrr P R * A S B S T 0 1 R T 0 T
102 0red P R * A S B S T 0 1 0
103 102 5 88 leltned P R * A S B S T 0 1 0 < T T 0
104 103 biimpar P R * A S B S T 0 1 T 0 0 < T
105 104 adantlr P R * A S B S T 0 1 R T 0 0 < T
106 ltmul2 P A R T 0 < T P A < R T P A < T R
107 99 100 101 105 106 syl112anc P R * A S B S T 0 1 R T 0 P A < R T P A < T R
108 97 107 mpbid P R * A S B S T 0 1 R T 0 T P A < T R
109 92 108 eqbrtrd P R * A S B S T 0 1 R T 0 T P A < T R
110 20 52 absmuld P R * A S B S T 0 1 1 T P B = 1 T P B
111 17 a1i P R * A S B S T 0 1 1
112 4 simp3d P R * A S B S T 0 1 T 1
113 5 111 112 abssubge0d P R * A S B S T 0 1 1 T = 1 T
114 113 oveq1d P R * A S B S T 0 1 1 T P B = 1 T P B
115 110 114 eqtrd P R * A S B S T 0 1 1 T P B = 1 T P B
116 115 adantr P R * A S B S T 0 1 R 1 T P B = 1 T P B
117 76 adantr P R * A S B S T 0 1 R P B
118 subge0 1 T 0 1 T T 1
119 17 5 118 sylancr P R * A S B S T 0 1 0 1 T T 1
120 112 119 mpbird P R * A S B S T 0 1 0 1 T
121 19 120 jca P R * A S B S T 0 1 1 T 0 1 T
122 121 adantr P R * A S B S T 0 1 R 1 T 0 1 T
123 80 82 eqbrtrrd P R * A S B S T 0 1 P B < R
124 123 adantr P R * A S B S T 0 1 R P B < R
125 ltle P B R P B < R P B R
126 76 125 sylan P R * A S B S T 0 1 R P B < R P B R
127 124 126 mpd P R * A S B S T 0 1 R P B R
128 lemul2a P B R 1 T 0 1 T P B R 1 T P B 1 T R
129 117 61 122 127 128 syl31anc P R * A S B S T 0 1 R 1 T P B 1 T R
130 116 129 eqbrtrd P R * A S B S T 0 1 R 1 T P B 1 T R
131 130 adantr P R * A S B S T 0 1 R T 0 1 T P B 1 T R
132 57 adantr P R * A S B S T 0 1 R T P A
133 58 adantr P R * A S B S T 0 1 R 1 T P B
134 remulcl T R T R
135 5 134 sylan P R * A S B S T 0 1 R T R
136 remulcl 1 T R 1 T R
137 19 136 sylan P R * A S B S T 0 1 R 1 T R
138 ltleadd T P A 1 T P B T R 1 T R T P A < T R 1 T P B 1 T R T P A + 1 T P B < T R + 1 T R
139 132 133 135 137 138 syl22anc P R * A S B S T 0 1 R T P A < T R 1 T P B 1 T R T P A + 1 T P B < T R + 1 T R
140 139 adantr P R * A S B S T 0 1 R T 0 T P A < T R 1 T P B 1 T R T P A + 1 T P B < T R + 1 T R
141 109 131 140 mp2and P R * A S B S T 0 1 R T 0 T P A + 1 T P B < T R + 1 T R
142 40 oveq1d P R * A S B S T 0 1 T + 1 - T R = 1 R
143 142 adantr P R * A S B S T 0 1 R T + 1 - T R = 1 R
144 6 adantr P R * A S B S T 0 1 R T
145 20 adantr P R * A S B S T 0 1 R 1 T
146 61 recnd P R * A S B S T 0 1 R R
147 144 145 146 adddird P R * A S B S T 0 1 R T + 1 - T R = T R + 1 T R
148 146 mulid2d P R * A S B S T 0 1 R 1 R = R
149 143 147 148 3eqtr3d P R * A S B S T 0 1 R T R + 1 T R = R
150 149 adantr P R * A S B S T 0 1 R T 0 T R + 1 T R = R
151 141 150 breqtrd P R * A S B S T 0 1 R T 0 T P A + 1 T P B < R
152 86 151 pm2.61dane P R * A S B S T 0 1 R T P A + 1 T P B < R
153 56 60 61 63 152 lelttrd P R * A S B S T 0 1 R T P A + 1 T P B < R
154 55 adantr P R * A S B S T 0 1 R = +∞ T P A + 1 T P B
155 154 ltpnfd P R * A S B S T 0 1 R = +∞ T P A + 1 T P B < +∞
156 simpr P R * A S B S T 0 1 R = +∞ R = +∞
157 155 156 breqtrrd P R * A S B S T 0 1 R = +∞ T P A + 1 T P B < R
158 0xr 0 *
159 158 a1i P R * A S B S T 0 1 0 *
160 98 rexrd P R * A S B S T 0 1 P A *
161 50 absge0d P R * A S B S T 0 1 0 P A
162 159 160 11 161 96 xrlelttrd P R * A S B S T 0 1 0 < R
163 159 11 162 xrltled P R * A S B S T 0 1 0 R
164 ge0nemnf R * 0 R R −∞
165 11 163 164 syl2anc P R * A S B S T 0 1 R −∞
166 11 165 jca P R * A S B S T 0 1 R * R −∞
167 xrnemnf R * R −∞ R R = +∞
168 166 167 sylib P R * A S B S T 0 1 R R = +∞
169 153 157 168 mpjaodan P R * A S B S T 0 1 T P A + 1 T P B < R
170 49 169 eqbrtrd P R * A S B S T 0 1 P abs T A + 1 T B < R
171 elbl abs ∞Met P R * T A + 1 T B P ball abs R T A + 1 T B P abs T A + 1 T B < R
172 9 10 11 171 mp3an2i P R * A S B S T 0 1 T A + 1 T B P ball abs R T A + 1 T B P abs T A + 1 T B < R
173 28 170 172 mpbir2and P R * A S B S T 0 1 T A + 1 T B P ball abs R
174 173 1 eleqtrrdi P R * A S B S T 0 1 T A + 1 T B S