Theorem sqcld 14081

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 14055	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) ∈ ℂ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7370  ℂcc 11038  2c2 12214  ↑cexp 13998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-cnex 11096  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116  ax-pre-mulgt0 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6269  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-om 7821  df-2nd 7946  df-frecs 8235  df-wrecs 8266  df-recs 8315  df-rdg 8353  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-sub 11380  df-neg 11381  df-nn 12160  df-2 12222  df-n0 12416  df-z 12503  df-uz 12766  df-seq 13939  df-exp 13999

This theorem is referenced by:  mulsubdivbinom2  14199  muldivbinom2  14200  recval  15260  bhmafibid1cn  15403  bhmafibid2cn  15404  bhmafibid2  15406  arisum2  15798  fsumcube  15997  efi4p  16076  sincossq  16115  cos2t  16117  cos2tsin  16118  sqrt2irrlem  16187  pythagtriplem1  16758  pythagtriplem2  16759  pythagtriplem6  16763  pythagtriplem7  16764  pythagtriplem12  16768  pythagtriplem14  16770  4sqlem7  16886  4sqlem10  16889  4sqlem14  16900  4cphipval2  25215  csbren  25372  rrxmval  25378  rrxmetlem  25380  dvrecg  25950  dvmptdiv  25951  dveflem  25956  coskpi  26505  coseq1  26507  tanregt0  26521  efif1olem4  26527  tanarg  26601  lawcoslem1  26798  lawcos  26799  pythag  26800  ssscongptld  26805  chordthmlem3  26817  chordthmlem4  26818  chordthmlem5  26819  heron  26821  quad2  26822  quad  26823  dcubic1lem  26826  dcubic2  26827  dcubic1  26828  dcubic  26829  mcubic  26830  cubic2  26831  cubic  26832  binom4  26833  dquartlem1  26834  dquartlem2  26835  dquart  26836  quart1cl  26837  quart1lem  26838  quart1  26839  quartlem1  26840  quartlem2  26841  quartlem4  26843  quart  26844  asinlem3  26854  asinneg  26869  asinsin  26875  atandmcj  26892  efiatan2  26900  atandmtan  26903  cosatan  26904  cosatanne0  26905  dvatan  26918  cxp2limlem  26959  lgamgulmlem4  27015  basellem8  27071  lgsdir  27316  2sqlem4  27405  2sqlem11  27413  2sqn0  27418  2sqmod  27420  2sqnn  27423  addsq2reu  27424  2sqreultlem  27431  2sqreunnltlem  27434  2sqreulem2  27436  mulog2sumlem2  27519  mulog2sumlem3  27520  logsqvma  27526  selberglem1  27529  selberglem3  27531  selberg  27532  logdivbnd  27540  pntlemf  27589  pntlemk  27590  pntlemo  27591  ax5seglem1  29019  ax5seglem2  29020  ax5seglem6  29025  ax5seglem9  29028  axlowdimlem16  29048  axlowdimlem17  29049  4ipval2  30802  ipidsq  30804  cncph  30913  hhph  31272  eigvalcl  32055  pythagreim  32842  quad3d  32846  constrrtlc1  33916  constrrtcclem  33918  constrrtcc  33919  constrfin  33930  constrresqrtcl  33961  cos9thpiminplylem2  33967  cos9thpiminplylem3  33968  cos9thpinconstrlem1  33973  circlemethhgt  34827  hgt750leme  34842  sin2h  37890  cos2h  37891  tan2h  37892  dvtan  37950  dvasin  37984  dvacos  37985  areacirclem1  37988  areacirclem2  37989  areacirclem4  37991  areacirc  37993  ismrer1  38118  aks4d1p1p2  42469  aks4d1p1p6  42472  aks4d1p1p7  42473  aks4d1p1p5  42474  oddnumth  42710  nicomachus  42711  sumcubes  42712  readvrec2  42760  cu3addd  43067  3cubeslem2  43071  3cubeslem3l  43072  3cubeslem3r  43073  3cubeslem4  43075  pellexlem1  43215  pellexlem2  43216  pellexlem6  43220  pell1qrge1  43256  pell1qrgaplem  43259  rmspecsqrtnq  43292  rmxdbl  43325  jm2.18  43374  jm2.19lem1  43375  jm2.25  43385  jm2.27c  43393  sqrtcval  44026  dvdivf  46309  dvdivbd  46310  itgsinexplem1  46341  itgsinexp  46342  wallispi2lem1  46458  wallispi2lem2  46459  wallispi2  46460  stirlinglem1  46461  stirlinglem3  46463  stirlinglem8  46468  stirlinglem10  46470  stirlinglem15  46475  rrxtopnfi  46674  hoiqssbllem2  47010  quad1  48009  itschlc0yqe  49149  itsclc0yqsollem1  49151  itsclc0yqsol  49153  itscnhlc0xyqsol  49154  itschlc0xyqsol1  49155  itschlc0xyqsol  49156  itsclc0xyqsolr  49158  2itscplem1  49167  2itscplem3  49169  itscnhlinecirc02plem1  49171  onetansqsecsq  50149  cotsqcscsq  50150