Theorem sqrtcld 15458

Description: Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)

Hypothesis

Ref	Expression
abscld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
sqrtcld	⊢ (𝜑 → (√‘𝐴) ∈ ℂ)

Proof of Theorem sqrtcld

Step	Hyp	Ref	Expression
1		abscld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		sqrtcl 15380	. 2 ⊢ (𝐴 ∈ ℂ → (√‘𝐴) ∈ ℂ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (√‘𝐴) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2141  ‘cfv 6516  ℂcc 11065  √csqrt 15251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-cnex 11123  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143  ax-pre-mulgt0 11144  ax-pre-sup 11145

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7348  df-ov 7394  df-oprab 7395  df-mpo 7396  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-sup 9382  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-sub 11410  df-neg 11411  df-div 11839  df-nn 12205  df-2 12274  df-3 12275  df-n0 12476  df-z 12563  df-uz 12834  df-rp 12988  df-seq 14009  df-exp 14069  df-cj 15117  df-re 15118  df-im 15119  df-sqrt 15253  df-abs 15254

This theorem is referenced by:  msqsqrtd  15461  pythagtriplem12  16853  pythagtriplem14  16855  pythagtriplem16  16857  tcphcphlem1  25285  tcphcph  25287  efif1olem3  26597  efif1olem4  26598  dvcnsqrt  26797  loglesqrt  26814  quad  26893  dcubic  26899  cubic  26902  quartlem2  26911  quartlem3  26912  quartlem4  26913  quart  26914  asinlem  26921  asinlem2  26922  asinlem3a  26923  asinlem3  26924  asinf  26925  asinneg  26939  efiasin  26941  sinasin  26942  asinbnd  26952  cosasin  26957  efiatan2  26970  cosatan  26974  cosatanne0  26975  atans2  26984  addsqnreup  27495  quad3d  32912  constrsqrtcl  34037  sqsscirc1  34166  divsqrtid  34849  logdivsqrle  34905  dvasin  38164  dvacos  38165  areacirclem1  38168  areacirclem4  38171  areacirc  38173  tan3rdpi  42922  pell1234qrne0  43391  pell1234qrreccl  43392  pell1234qrmulcl  43393  pell14qrgt0  43397  pell1234qrdich  43399  pell14qrdich  43407  pell1qr1  43409  rmspecsqrtnq  43444  rmxyneg  43458  rmxyadd  43459  rmxy1  43460  rmxy0  43461  jm2.22  43533  stirlinglem3  46611  stirlinglem4  46612  stirlinglem13  46621  stirlinglem14  46622  stirlinglem15  46623  qndenserrnbllem  46829  sqrtnegnre  47862  quad1  48203  requad01  48204  requad1  48205  requad2  48206  itsclc0yqsol  49347  itscnhlc0xyqsol  49348  itschlc0xyqsol1  49349  itschlc0xyqsol  49350  itsclc0xyqsolr  49352  inlinecirc02plem  49369