Theorem sqrtcld 15648

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 15570	. 2 ⊢ (𝐴 ∈ ℂ → (√‘𝐴) ∈ ℂ)
3	1, 2	syl 18	1 ⊢ (𝜑 → (√‘𝐴) ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ‘cfv 6564  ℂcc 11235  √csqrt 15441

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7781  ax-cnex 11293  ax-resscn 11294  ax-1cn 11295  ax-icn 11296  ax-addcl 11297  ax-addrcl 11298  ax-mulcl 11299  ax-mulrcl 11300  ax-mulcom 11301  ax-addass 11302  ax-mulass 11303  ax-distr 11304  ax-i2m1 11305  ax-1ne0 11306  ax-1rid 11307  ax-rnegex 11308  ax-rrecex 11309  ax-cnre 11310  ax-pre-lttri 11311  ax-pre-lttrn 11312  ax-pre-ltadd 11313  ax-pre-mulgt0 11314  ax-pre-sup 11315

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6328  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6518  df-fun 6566  df-fn 6567  df-f 6568  df-f1 6569  df-fo 6570  df-f1o 6571  df-fv 6572  df-riota 7406  df-ov 7452  df-oprab 7453  df-mpo 7454  df-om 7910  df-2nd 8034  df-frecs 8335  df-wrecs 8366  df-recs 8415  df-rdg 8454  df-er 8753  df-en 9010  df-dom 9011  df-sdom 9012  df-sup 9469  df-pnf 11382  df-mnf 11383  df-xr 11384  df-ltxr 11385  df-le 11386  df-sub 11580  df-neg 11581  df-div 12012  df-nn 12374  df-2 12443  df-3 12444  df-n0 12645  df-z 12732  df-uz 13004  df-rp 13159  df-seq 14183  df-exp 14243  df-cj 15307  df-re 15308  df-im 15309  df-sqrt 15443  df-abs 15444

This theorem is used by:  msqsqrtd  15651  pythagtriplem12  17045  pythagtriplem14  17047  pythagtriplem16  17049  tcphcphlem1  25600  tcphcph  25602  efif1olem3  26918  efif1olem4  26919  dvcnsqrt  27118  loglesqrt  27135  quad  27214  dcubic  27220  cubic  27223  quartlem2  27232  quartlem3  27233  quartlem4  27234  quart  27235  asinlem  27242  asinlem2  27243  asinlem3a  27244  asinlem3  27245  asinf  27246  asinneg  27260  efiasin  27262  sinasin  27263  asinbnd  27273  cosasin  27278  efiatan2  27291  cosatan  27295  cosatanne0  27296  atans2  27305  addsqnreup  27816  quad3d  33427  constrsqrtcl  34515  sqsscirc1  34644  divsqrtid  35327  logdivsqrle  35383  dvasin  38883  dvacos  38884  areacirclem1  38887  areacirclem4  38890  areacirc  38892  tan3rdpi  43663  pell1234qrne0  44120  pell1234qrreccl  44121  pell1234qrmulcl  44122  pell14qrgt0  44126  pell1234qrdich  44128  pell14qrdich  44136  pell1qr1  44138  rmspecsqrtnq  44173  rmxyneg  44187  rmxyadd  44188  rmxy1  44189  rmxy0  44190  jm2.22  44262  stirlinglem3  47353  stirlinglem4  47354  stirlinglem13  47363  stirlinglem14  47364  stirlinglem15  47365  qndenserrnbllem  47571  sqrtnnaa  48180  sqrtnegnre  48644  quad1  48985  requad01  48986  requad1  48987  requad2  48988  itsclc0yqsol  50201  itscnhlc0xyqsol  50202  itschlc0xyqsol1  50203  itschlc0xyqsol  50204  itsclc0xyqsolr  50206  inlinecirc02plem  50223