Metamath Proof Explorer


Theorem sqrtcval

Description: Explicit formula for the complex square root in terms of the square root of nonnegative reals. The right-hand side is decomposed into real and imaginary parts in the format expected by crrei and crimi . This formula can be found in section 3.7.27 of Handbook of Mathematical Functions, ed. M. Abramowitz and I. A. Stegun (1965, Dover Press). (Contributed by RP, 18-May-2024)

Ref Expression
Assertion sqrtcval A A = A + A 2 + i if A < 0 1 1 A A 2

Proof

Step Hyp Ref Expression
1 sqrtcvallem5 A A + A 2
2 1 recnd A A + A 2
3 ax-icn i
4 3 a1i A i
5 neg1rr 1
6 1re 1
7 5 6 ifcli if A < 0 1 1
8 7 a1i A if A < 0 1 1
9 sqrtcvallem3 A A A 2
10 8 9 remulcld A if A < 0 1 1 A A 2
11 10 recnd A if A < 0 1 1 A A 2
12 4 11 mulcld A i if A < 0 1 1 A A 2
13 2 12 addcld A A + A 2 + i if A < 0 1 1 A A 2
14 id A A
15 binom2 A + A 2 i if A < 0 1 1 A A 2 A + A 2 + i if A < 0 1 1 A A 2 2 = A + A 2 2 + 2 A + A 2 i if A < 0 1 1 A A 2 + i if A < 0 1 1 A A 2 2
16 2 12 15 syl2anc A A + A 2 + i if A < 0 1 1 A A 2 2 = A + A 2 2 + 2 A + A 2 i if A < 0 1 1 A A 2 + i if A < 0 1 1 A A 2 2
17 abscl A A
18 recl A A
19 17 18 readdcld A A + A
20 19 rehalfcld A A + A 2
21 20 recnd A A + A 2
22 21 sqsqrtd A A + A 2 2 = A + A 2
23 4 11 sqmuld A i if A < 0 1 1 A A 2 2 = i 2 if A < 0 1 1 A A 2 2
24 i2 i 2 = 1
25 24 a1i A i 2 = 1
26 8 recnd A if A < 0 1 1
27 9 recnd A A A 2
28 26 27 sqmuld A if A < 0 1 1 A A 2 2 = if A < 0 1 1 2 A A 2 2
29 ovif if A < 0 1 1 2 = if A < 0 1 2 1 2
30 neg1sqe1 1 2 = 1
31 sq1 1 2 = 1
32 ifeq12 1 2 = 1 1 2 = 1 if A < 0 1 2 1 2 = if A < 0 1 1
33 30 31 32 mp2an if A < 0 1 2 1 2 = if A < 0 1 1
34 ifid if A < 0 1 1 = 1
35 29 33 34 3eqtri if A < 0 1 1 2 = 1
36 35 a1i A if A < 0 1 1 2 = 1
37 17 18 resubcld A A A
38 37 rehalfcld A A A 2
39 38 recnd A A A 2
40 39 sqsqrtd A A A 2 2 = A A 2
41 36 40 oveq12d A if A < 0 1 1 2 A A 2 2 = 1 A A 2
42 39 mulid2d A 1 A A 2 = A A 2
43 28 41 42 3eqtrd A if A < 0 1 1 A A 2 2 = A A 2
44 25 43 oveq12d A i 2 if A < 0 1 1 A A 2 2 = -1 A A 2
45 39 mulm1d A -1 A A 2 = A A 2
46 23 44 45 3eqtrd A i if A < 0 1 1 A A 2 2 = A A 2
47 22 46 oveq12d A A + A 2 2 + i if A < 0 1 1 A A 2 2 = A + A 2 + A A 2
48 21 39 negsubd A A + A 2 + A A 2 = A + A 2 A A 2
49 17 recnd A A
50 18 recnd A A
51 49 50 50 pnncand A A + A - A A = A + A
52 50 2timesd A 2 A = A + A
53 51 52 eqtr4d A A + A - A A = 2 A
54 53 oveq1d A A + A - A A 2 = 2 A 2
55 19 recnd A A + A
56 37 recnd A A A
57 2cnd A 2
58 2ne0 2 0
59 58 a1i A 2 0
60 55 56 57 59 divsubdird A A + A - A A 2 = A + A 2 A A 2
61 50 57 59 divcan3d A 2 A 2 = A
62 54 60 61 3eqtr3d A A + A 2 A A 2 = A
63 47 48 62 3eqtrd A A + A 2 2 + i if A < 0 1 1 A A 2 2 = A
64 57 2 mulcld A 2 A + A 2
65 64 4 11 mul12d A 2 A + A 2 i if A < 0 1 1 A A 2 = i 2 A + A 2 if A < 0 1 1 A A 2
66 57 2 12 mulassd A 2 A + A 2 i if A < 0 1 1 A A 2 = 2 A + A 2 i if A < 0 1 1 A A 2
67 57 2 11 mulassd A 2 A + A 2 if A < 0 1 1 A A 2 = 2 A + A 2 if A < 0 1 1 A A 2
68 2 26 27 mul12d A A + A 2 if A < 0 1 1 A A 2 = if A < 0 1 1 A + A 2 A A 2
69 sqrtcvallem4 A 0 A + A 2
70 halfnneg2 A + A 0 A + A 0 A + A 2
71 19 70 syl A 0 A + A 0 A + A 2
72 69 71 mpbird A 0 A + A
73 2rp 2 +
74 73 a1i A 2 +
75 19 72 74 sqrtdivd A A + A 2 = A + A 2
76 sqrtcvallem2 A 0 A A 2
77 halfnneg2 A A 0 A A 0 A A 2
78 37 77 syl A 0 A A 0 A A 2
79 76 78 mpbird A 0 A A
80 37 79 74 sqrtdivd A A A 2 = A A 2
81 75 80 oveq12d A A + A 2 A A 2 = A + A 2 A A 2
82 19 72 resqrtcld A A + A
83 82 recnd A A + A
84 2re 2
85 84 a1i A 2
86 0le2 0 2
87 86 a1i A 0 2
88 85 87 resqrtcld A 2
89 88 recnd A 2
90 37 79 resqrtcld A A A
91 90 recnd A A A
92 sqrt00 2 0 2 2 = 0 2 = 0
93 84 86 92 mp2an 2 = 0 2 = 0
94 93 necon3bii 2 0 2 0
95 58 94 mpbir 2 0
96 95 a1i A 2 0
97 83 89 91 89 96 96 divmuldivd A A + A 2 A A 2 = A + A A A 2 2
98 18 resqcld A A 2
99 98 recnd A A 2
100 imcl A A
101 100 resqcld A A 2
102 101 recnd A A 2
103 absvalsq2 A A 2 = A 2 + A 2
104 99 102 103 mvrladdd A A 2 A 2 = A 2
105 subsq A A A 2 A 2 = A + A A A
106 49 50 105 syl2anc A A 2 A 2 = A + A A A
107 104 106 eqtr3d A A 2 = A + A A A
108 107 fveq2d A A 2 = A + A A A
109 100 absred A A = A 2
110 reabsifneg A A = if A < 0 A A
111 100 110 syl A A = if A < 0 A A
112 109 111 eqtr3d A A 2 = if A < 0 A A
113 19 72 37 79 sqrtmuld A A + A A A = A + A A A
114 108 112 113 3eqtr3rd A A + A A A = if A < 0 A A
115 remsqsqrt 2 0 2 2 2 = 2
116 84 86 115 mp2an 2 2 = 2
117 116 a1i A 2 2 = 2
118 114 117 oveq12d A A + A A A 2 2 = if A < 0 A A 2
119 81 97 118 3eqtrd A A + A 2 A A 2 = if A < 0 A A 2
120 119 oveq2d A if A < 0 1 1 A + A 2 A A 2 = if A < 0 1 1 if A < 0 A A 2
121 68 120 eqtrd A A + A 2 if A < 0 1 1 A A 2 = if A < 0 1 1 if A < 0 A A 2
122 121 oveq2d A 2 A + A 2 if A < 0 1 1 A A 2 = 2 if A < 0 1 1 if A < 0 A A 2
123 100 renegcld A A
124 123 100 ifcld A if A < 0 A A
125 124 recnd A if A < 0 A A
126 26 125 57 59 divassd A if A < 0 1 1 if A < 0 A A 2 = if A < 0 1 1 if A < 0 A A 2
127 ovif12 if A < 0 1 1 if A < 0 A A = if A < 0 -1 A 1 A
128 5 a1i A 1
129 128 recnd A 1
130 100 recnd A A
131 129 129 130 mulassd A -1 -1 A = -1 -1 A
132 neg1mulneg1e1 -1 -1 = 1
133 132 a1i A -1 -1 = 1
134 133 oveq1d A -1 -1 A = 1 A
135 130 mulid2d A 1 A = A
136 134 135 eqtrd A -1 -1 A = A
137 130 mulm1d A -1 A = A
138 137 oveq2d A -1 -1 A = -1 A
139 131 136 138 3eqtr3rd A -1 A = A
140 139 adantr A A < 0 -1 A = A
141 135 adantr A ¬ A < 0 1 A = A
142 140 141 ifeqda A if A < 0 -1 A 1 A = A
143 127 142 syl5eq A if A < 0 1 1 if A < 0 A A = A
144 143 oveq1d A if A < 0 1 1 if A < 0 A A 2 = A 2
145 126 144 eqtr3d A if A < 0 1 1 if A < 0 A A 2 = A 2
146 145 oveq2d A 2 if A < 0 1 1 if A < 0 A A 2 = 2 A 2
147 130 57 59 divcan2d A 2 A 2 = A
148 146 147 eqtrd A 2 if A < 0 1 1 if A < 0 A A 2 = A
149 67 122 148 3eqtrd A 2 A + A 2 if A < 0 1 1 A A 2 = A
150 149 oveq2d A i 2 A + A 2 if A < 0 1 1 A A 2 = i A
151 65 66 150 3eqtr3d A 2 A + A 2 i if A < 0 1 1 A A 2 = i A
152 63 151 oveq12d A A + A 2 2 + i if A < 0 1 1 A A 2 2 + 2 A + A 2 i if A < 0 1 1 A A 2 = A + i A
153 1 resqcld A A + A 2 2
154 153 recnd A A + A 2 2
155 2 12 mulcld A A + A 2 i if A < 0 1 1 A A 2
156 57 155 mulcld A 2 A + A 2 i if A < 0 1 1 A A 2
157 12 sqcld A i if A < 0 1 1 A A 2 2
158 154 156 157 add32d A A + A 2 2 + 2 A + A 2 i if A < 0 1 1 A A 2 + i if A < 0 1 1 A A 2 2 = A + A 2 2 + i if A < 0 1 1 A A 2 2 + 2 A + A 2 i if A < 0 1 1 A A 2
159 replim A A = A + i A
160 152 158 159 3eqtr4d A A + A 2 2 + 2 A + A 2 i if A < 0 1 1 A A 2 + i if A < 0 1 1 A A 2 2 = A
161 16 160 eqtrd A A + A 2 + i if A < 0 1 1 A A 2 2 = A
162 20 69 sqrtge0d A 0 A + A 2
163 1 10 crred A A + A 2 + i if A < 0 1 1 A A 2 = A + A 2
164 162 163 breqtrrd A 0 A + A 2 + i if A < 0 1 1 A A 2
165 reim A + A 2 + i if A < 0 1 1 A A 2 A + A 2 + i if A < 0 1 1 A A 2 = i A + A 2 + i if A < 0 1 1 A A 2
166 13 165 syl A A + A 2 + i if A < 0 1 1 A A 2 = i A + A 2 + i if A < 0 1 1 A A 2
167 166 163 eqtr3d A i A + A 2 + i if A < 0 1 1 A A 2 = A + A 2
168 167 eqeq1d A i A + A 2 + i if A < 0 1 1 A A 2 = 0 A + A 2 = 0
169 cnsqrt00 A + A 2 A + A 2 = 0 A + A 2 = 0
170 21 169 syl A A + A 2 = 0 A + A 2 = 0
171 half0 A + A A + A 2 = 0 A + A = 0
172 55 171 syl A A + A 2 = 0 A + A = 0
173 49 50 addcomd A A + A = A + A
174 173 eqeq1d A A + A = 0 A + A = 0
175 addeq0 A A A + A = 0 A = A
176 50 49 175 syl2anc A A + A = 0 A = A
177 172 174 176 3bitrd A A + A 2 = 0 A = A
178 168 170 177 3bitrd A i A + A 2 + i if A < 0 1 1 A A 2 = 0 A = A
179 olc A = A A = A A = A
180 eqcom A 2 = A 2 A 2 = A 2
181 180 a1i A A 2 = A 2 A 2 = A 2
182 sqeqor A A A 2 = A 2 A = A A = A
183 50 49 182 syl2anc A A 2 = A 2 A = A A = A
184 103 eqeq1d A A 2 = A 2 A 2 + A 2 = A 2
185 addid0 A 2 A 2 A 2 + A 2 = A 2 A 2 = 0
186 99 102 185 syl2anc A A 2 + A 2 = A 2 A 2 = 0
187 sqeq0 A A 2 = 0 A = 0
188 130 187 syl A A 2 = 0 A = 0
189 184 186 188 3bitrd A A 2 = A 2 A = 0
190 181 183 189 3bitr3d A A = A A = A A = 0
191 179 190 syl5ib A A = A A = 0
192 191 ancld A A = A A = A A = 0
193 178 192 sylbid A i A + A 2 + i if A < 0 1 1 A A 2 = 0 A = A A = 0
194 simp2 A A = A A = 0 A = A
195 194 oveq2d A A = A A = 0 A + A = A + A
196 simp1 A A = A A = 0 A
197 196 49 syl A A = A A = 0 A
198 197 negidd A A = A A = 0 A + A = 0
199 195 198 eqtrd A A = A A = 0 A + A = 0
200 199 oveq1d A A = A A = 0 A + A 2 = 0 2
201 2cn 2
202 201 58 div0i 0 2 = 0
203 200 202 eqtrdi A A = A A = 0 A + A 2 = 0
204 203 fveq2d A A = A A = 0 A + A 2 = 0
205 sqrt0 0 = 0
206 204 205 eqtrdi A A = A A = 0 A + A 2 = 0
207 simp3 A A = A A = 0 A = 0
208 0red A A = A A = 0 0
209 208 ltnrd A A = A A = 0 ¬ 0 < 0
210 207 209 eqnbrtrd A A = A A = 0 ¬ A < 0
211 210 iffalsed A A = A A = 0 if A < 0 1 1 = 1
212 194 oveq2d A A = A A = 0 A A = A A
213 49 49 subnegd A A A = A + A
214 49 2timesd A 2 A = A + A
215 213 214 eqtr4d A A A = 2 A
216 196 215 syl A A = A A = 0 A A = 2 A
217 212 216 eqtrd A A = A A = 0 A A = 2 A
218 217 oveq1d A A = A A = 0 A A 2 = 2 A 2
219 49 57 59 divcan3d A 2 A 2 = A
220 196 219 syl A A = A A = 0 2 A 2 = A
221 218 220 eqtrd A A = A A = 0 A A 2 = A
222 221 fveq2d A A = A A = 0 A A 2 = A
223 211 222 oveq12d A A = A A = 0 if A < 0 1 1 A A 2 = 1 A
224 absge0 A 0 A
225 17 224 resqrtcld A A
226 225 recnd A A
227 226 mulid2d A 1 A = A
228 196 227 syl A A = A A = 0 1 A = A
229 223 228 eqtrd A A = A A = 0 if A < 0 1 1 A A 2 = A
230 229 oveq2d A A = A A = 0 i if A < 0 1 1 A A 2 = i A
231 206 230 oveq12d A A = A A = 0 A + A 2 + i if A < 0 1 1 A A 2 = 0 + i A
232 4 226 mulcld A i A
233 196 232 syl A A = A A = 0 i A
234 233 addid2d A A = A A = 0 0 + i A = i A
235 231 234 eqtrd A A = A A = 0 A + A 2 + i if A < 0 1 1 A A 2 = i A
236 235 oveq2d A A = A A = 0 i A + A 2 + i if A < 0 1 1 A A 2 = i i A
237 ixi i i = 1
238 237 a1i A i i = 1
239 238 oveq1d A i i A = -1 A
240 4 4 226 mulassd A i i A = i i A
241 226 mulm1d A -1 A = A
242 239 240 241 3eqtr3d A i i A = A
243 196 242 syl A A = A A = 0 i i A = A
244 236 243 eqtrd A A = A A = 0 i A + A 2 + i if A < 0 1 1 A A 2 = A
245 244 fveq2d A A = A A = 0 i A + A 2 + i if A < 0 1 1 A A 2 = A
246 225 renegcld A A
247 246 rered A A = A
248 196 247 syl A A = A A = 0 A = A
249 245 248 eqtrd A A = A A = 0 i A + A 2 + i if A < 0 1 1 A A 2 = A
250 17 224 sqrtge0d A 0 A
251 225 le0neg2d A 0 A A 0
252 250 251 mpbid A A 0
253 196 252 syl A A = A A = 0 A 0
254 249 253 eqbrtrd A A = A A = 0 i A + A 2 + i if A < 0 1 1 A A 2 0
255 254 3expib A A = A A = 0 i A + A 2 + i if A < 0 1 1 A A 2 0
256 193 255 syld A i A + A 2 + i if A < 0 1 1 A A 2 = 0 i A + A 2 + i if A < 0 1 1 A A 2 0
257 4 13 mulcld A i A + A 2 + i if A < 0 1 1 A A 2
258 257 sqrtcvallem1 A i A + A 2 + i if A < 0 1 1 A A 2 = 0 i A + A 2 + i if A < 0 1 1 A A 2 0 ¬ i A + A 2 + i if A < 0 1 1 A A 2 +
259 256 258 mpbid A ¬ i A + A 2 + i if A < 0 1 1 A A 2 +
260 13 14 161 164 259 eqsqrtd A A + A 2 + i if A < 0 1 1 A A 2 = A
261 260 eqcomd A A = A + A 2 + i if A < 0 1 1 A A 2