Theorem sqcld 14210

Description: Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

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

Assertion

Ref	Expression
sqcld	⊢ (𝜑 → (𝐴↑2) ∈ ℂ)

Proof of Theorem sqcld

Step	Hyp	Ref	Expression
1		expcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		sqcl 14184	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) ∈ ℂ)
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7416  ℂcc 11125  2c2 12322  ↑cexp 14127

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  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 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7866  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-nn 12261  df-2 12330  df-n0 12532  df-z 12619  df-uz 12891  df-seq 14068  df-exp 14128

This theorem is used by:  mulsubdivbinom2  14328  muldivbinom2  14329  recval  15412  bhmafibid1cn  15555  bhmafibid2cn  15556  bhmafibid2  15558  arisum2  15952  fsumcube  16150  efi4p  16229  sincossq  16268  cos2t  16270  cos2tsin  16271  sqrt2irrlem  16340  pythagtriplem1  16912  pythagtriplem2  16913  pythagtriplem6  16917  pythagtriplem7  16918  pythagtriplem12  16922  pythagtriplem14  16924  4sqlem7  17040  4sqlem10  17043  4sqlem14  17054  4cphipval2  25471  csbren  25628  rrxmval  25634  rrxmetlem  25636  dvrecg  26202  dvmptdiv  26203  dveflem  26208  coskpi  26758  coseq1  26760  tanregt0  26774  efif1olem4  26780  tanarg  26854  lawcoslem1  27050  lawcos  27051  pythag  27052  ssscongptld  27057  chordthmlem3  27069  chordthmlem4  27070  chordthmlem5  27071  heron  27073  quad2  27074  quad  27075  dcubic1lem  27078  dcubic2  27079  dcubic1  27080  dcubic  27081  mcubic  27082  cubic2  27083  cubic  27084  binom4  27085  dquartlem1  27086  dquartlem2  27087  dquart  27088  quart1cl  27089  quart1lem  27090  quart1  27091  quartlem1  27092  quartlem2  27093  quartlem4  27095  quart  27096  asinlem3  27106  asinneg  27121  asinsin  27127  atandmcj  27144  efiatan2  27152  atandmtan  27155  cosatan  27156  cosatanne0  27157  dvatan  27170  cxp2limlem  27210  lgamgulmlem4  27266  basellem8  27322  lgsdir  27566  2sqlem4  27655  2sqlem11  27663  2sqn0  27668  2sqmod  27670  2sqnn  27673  addsq2reu  27674  2sqreultlem  27681  2sqreunnltlem  27684  2sqreulem2  27686  mulog2sumlem2  27769  mulog2sumlem3  27770  logsqvma  27776  selberglem1  27779  selberglem3  27781  selberg  27782  logdivbnd  27790  pntlemf  27839  pntlemk  27840  pntlemo  27841  ax5seglem1  29371  ax5seglem2  29372  ax5seglem6  29377  ax5seglem9  29380  axlowdimlem16  29400  axlowdimlem17  29401  4ipval2  31175  ipidsq  31177  cncph  31286  hhph  31645  eigvalcl  32428  pythagreim  33203  quad3d  33207  constrrtlc1  34229  constrrtcclem  34231  constrrtcc  34232  constrfin  34243  constrresqrtcl  34274  cos9thpiminplylem2  34280  cos9thpiminplylem3  34281  cos9thpinconstrlem1  34286  circlemethhgt  35138  hgt750leme  35153  qdiff  38066  sin2h  38351  cos2h  38352  tan2h  38353  dvtan  38406  dvasin  38440  dvacos  38441  areacirclem1  38444  areacirclem2  38445  areacirclem4  38447  areacirc  38449  ismrer1  38575  aks4d1p1p2  42923  aks4d1p1p6  42926  aks4d1p1p7  42927  aks4d1p1p5  42928  quadfac  43058  oddnumth  43173  nicomachus  43174  sumcubes  43175  readvrec2  43223  cu3addd  43513  3cubeslem2  43517  3cubeslem3l  43518  3cubeslem3r  43519  3cubeslem4  43521  pellexlem1  43657  pellexlem2  43658  pellexlem6  43662  pell1qrge1  43698  pell1qrgaplem  43701  rmspecsqrtnq  43734  rmxdbl  43767  jm2.18  43816  jm2.19lem1  43817  jm2.25  43827  jm2.27c  43835  sqrtcval  44468  dvdivf  46737  dvdivbd  46738  itgsinexplem1  46769  itgsinexp  46770  wallispi2lem1  46886  wallispi2lem2  46887  wallispi2  46888  stirlinglem1  46889  stirlinglem3  46891  stirlinglem8  46896  stirlinglem10  46898  stirlinglem15  46903  rrxtopnfi  47102  hoiqssbllem2  47438  sin3t  47722  cos3t  47723  sin5t  47729  quad1  48523  itschlc0yqe  49677  itsclc0yqsollem1  49679  itsclc0yqsol  49681  itscnhlc0xyqsol  49682  itschlc0xyqsol1  49683  itschlc0xyqsol  49684  itsclc0xyqsolr  49686  2itscplem1  49695  2itscplem3  49697  itscnhlinecirc02plem1  49699  onetansqsecsq  50674  cotsqcscsq  50675  dvcot  50678