Theorem sqcld 14115

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7389  ℂcc 11072  2c2 12242  ↑cexp 14032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  ax-cnex 11130  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150  ax-pre-mulgt0 11151

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-pss 3936  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5110  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5535  df-eprel 5540  df-po 5548  df-so 5549  df-fr 5593  df-we 5595  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-pred 6276  df-ord 6337  df-on 6338  df-lim 6339  df-suc 6340  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-riota 7346  df-ov 7392  df-oprab 7393  df-mpo 7394  df-om 7845  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8380  df-er 8673  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11216  df-mnf 11217  df-xr 11218  df-ltxr 11219  df-le 11220  df-sub 11413  df-neg 11414  df-nn 12188  df-2 12250  df-n0 12449  df-z 12536  df-uz 12800  df-seq 13973  df-exp 14033

This theorem is referenced by:  mulsubdivbinom2  14233  muldivbinom2  14234  recval  15295  bhmafibid1cn  15438  bhmafibid2cn  15439  bhmafibid2  15441  arisum2  15833  fsumcube  16032  efi4p  16111  sincossq  16150  cos2t  16152  cos2tsin  16153  sqrt2irrlem  16222  pythagtriplem1  16793  pythagtriplem2  16794  pythagtriplem6  16798  pythagtriplem7  16799  pythagtriplem12  16803  pythagtriplem14  16805  4sqlem7  16921  4sqlem10  16924  4sqlem14  16935  4cphipval2  25148  csbren  25305  rrxmval  25311  rrxmetlem  25313  dvrecg  25883  dvmptdiv  25884  dveflem  25889  coskpi  26438  coseq1  26440  tanregt0  26454  efif1olem4  26460  tanarg  26534  lawcoslem1  26731  lawcos  26732  pythag  26733  ssscongptld  26738  chordthmlem3  26750  chordthmlem4  26751  chordthmlem5  26752  heron  26754  quad2  26755  quad  26756  dcubic1lem  26759  dcubic2  26760  dcubic1  26761  dcubic  26762  mcubic  26763  cubic2  26764  cubic  26765  binom4  26766  dquartlem1  26767  dquartlem2  26768  dquart  26769  quart1cl  26770  quart1lem  26771  quart1  26772  quartlem1  26773  quartlem2  26774  quartlem4  26776  quart  26777  asinlem3  26787  asinneg  26802  asinsin  26808  atandmcj  26825  efiatan2  26833  atandmtan  26836  cosatan  26837  cosatanne0  26838  dvatan  26851  cxp2limlem  26892  lgamgulmlem4  26948  basellem8  27004  lgsdir  27249  2sqlem4  27338  2sqlem11  27346  2sqn0  27351  2sqmod  27353  2sqnn  27356  addsq2reu  27357  2sqreultlem  27364  2sqreunnltlem  27367  2sqreulem2  27369  mulog2sumlem2  27452  mulog2sumlem3  27453  logsqvma  27459  selberglem1  27462  selberglem3  27464  selberg  27465  logdivbnd  27473  pntlemf  27522  pntlemk  27523  pntlemo  27524  ax5seglem1  28861  ax5seglem2  28862  ax5seglem6  28867  ax5seglem9  28870  axlowdimlem16  28890  axlowdimlem17  28891  4ipval2  30643  ipidsq  30645  cncph  30754  hhph  31113  eigvalcl  31896  pythagreim  32675  quad3d  32679  constrrtlc1  33728  constrrtcclem  33730  constrrtcc  33731  constrfin  33742  constrresqrtcl  33773  cos9thpiminplylem2  33779  cos9thpiminplylem3  33780  cos9thpinconstrlem1  33785  circlemethhgt  34640  hgt750leme  34655  sin2h  37599  cos2h  37600  tan2h  37601  dvtan  37659  dvasin  37693  dvacos  37694  areacirclem1  37697  areacirclem2  37698  areacirclem4  37700  areacirc  37702  ismrer1  37827  aks4d1p1p2  42053  aks4d1p1p6  42056  aks4d1p1p7  42057  aks4d1p1p5  42058  oddnumth  42294  nicomachus  42295  sumcubes  42296  readvrec2  42344  cu3addd  42662  3cubeslem2  42666  3cubeslem3l  42667  3cubeslem3r  42668  3cubeslem4  42670  pellexlem1  42810  pellexlem2  42811  pellexlem6  42815  pell1qrge1  42851  pell1qrgaplem  42854  rmspecsqrtnq  42887  rmxdbl  42921  jm2.18  42970  jm2.19lem1  42971  jm2.25  42981  jm2.27c  42989  sqrtcval  43623  dvdivf  45913  dvdivbd  45914  itgsinexplem1  45945  itgsinexp  45946  wallispi2lem1  46062  wallispi2lem2  46063  wallispi2  46064  stirlinglem1  46065  stirlinglem3  46067  stirlinglem8  46072  stirlinglem10  46074  stirlinglem15  46079  rrxtopnfi  46278  hoiqssbllem2  46614  quad1  47611  itschlc0yqe  48739  itsclc0yqsollem1  48741  itsclc0yqsol  48743  itscnhlc0xyqsol  48744  itschlc0xyqsol1  48745  itschlc0xyqsol  48746  itsclc0xyqsolr  48748  2itscplem1  48757  2itscplem3  48759  itscnhlinecirc02plem1  48761  onetansqsecsq  49727  cotsqcscsq  49728