Theorem sqcld 14051

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007  2c2 12183  ↑cexp 13968

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 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-nn 12129  df-2 12191  df-n0 12385  df-z 12472  df-uz 12736  df-seq 13909  df-exp 13969

This theorem is referenced by:  mulsubdivbinom2  14169  muldivbinom2  14170  recval  15230  bhmafibid1cn  15373  bhmafibid2cn  15374  bhmafibid2  15376  arisum2  15768  fsumcube  15967  efi4p  16046  sincossq  16085  cos2t  16087  cos2tsin  16088  sqrt2irrlem  16157  pythagtriplem1  16728  pythagtriplem2  16729  pythagtriplem6  16733  pythagtriplem7  16734  pythagtriplem12  16738  pythagtriplem14  16740  4sqlem7  16856  4sqlem10  16859  4sqlem14  16870  4cphipval2  25140  csbren  25297  rrxmval  25303  rrxmetlem  25305  dvrecg  25875  dvmptdiv  25876  dveflem  25881  coskpi  26430  coseq1  26432  tanregt0  26446  efif1olem4  26452  tanarg  26526  lawcoslem1  26723  lawcos  26724  pythag  26725  ssscongptld  26730  chordthmlem3  26742  chordthmlem4  26743  chordthmlem5  26744  heron  26746  quad2  26747  quad  26748  dcubic1lem  26751  dcubic2  26752  dcubic1  26753  dcubic  26754  mcubic  26755  cubic2  26756  cubic  26757  binom4  26758  dquartlem1  26759  dquartlem2  26760  dquart  26761  quart1cl  26762  quart1lem  26763  quart1  26764  quartlem1  26765  quartlem2  26766  quartlem4  26768  quart  26769  asinlem3  26779  asinneg  26794  asinsin  26800  atandmcj  26817  efiatan2  26825  atandmtan  26828  cosatan  26829  cosatanne0  26830  dvatan  26843  cxp2limlem  26884  lgamgulmlem4  26940  basellem8  26996  lgsdir  27241  2sqlem4  27330  2sqlem11  27338  2sqn0  27343  2sqmod  27345  2sqnn  27348  addsq2reu  27349  2sqreultlem  27356  2sqreunnltlem  27359  2sqreulem2  27361  mulog2sumlem2  27444  mulog2sumlem3  27445  logsqvma  27451  selberglem1  27454  selberglem3  27456  selberg  27457  logdivbnd  27465  pntlemf  27514  pntlemk  27515  pntlemo  27516  ax5seglem1  28877  ax5seglem2  28878  ax5seglem6  28883  ax5seglem9  28886  axlowdimlem16  28906  axlowdimlem17  28907  4ipval2  30656  ipidsq  30658  cncph  30767  hhph  31126  eigvalcl  31909  pythagreim  32698  quad3d  32702  constrrtlc1  33715  constrrtcclem  33717  constrrtcc  33718  constrfin  33729  constrresqrtcl  33760  cos9thpiminplylem2  33766  cos9thpiminplylem3  33767  cos9thpinconstrlem1  33772  circlemethhgt  34627  hgt750leme  34642  sin2h  37610  cos2h  37611  tan2h  37612  dvtan  37670  dvasin  37704  dvacos  37705  areacirclem1  37708  areacirclem2  37709  areacirclem4  37711  areacirc  37713  ismrer1  37838  aks4d1p1p2  42063  aks4d1p1p6  42066  aks4d1p1p7  42067  aks4d1p1p5  42068  oddnumth  42304  nicomachus  42305  sumcubes  42306  readvrec2  42354  cu3addd  42674  3cubeslem2  42678  3cubeslem3l  42679  3cubeslem3r  42680  3cubeslem4  42682  pellexlem1  42822  pellexlem2  42823  pellexlem6  42827  pell1qrge1  42863  pell1qrgaplem  42866  rmspecsqrtnq  42899  rmxdbl  42932  jm2.18  42981  jm2.19lem1  42982  jm2.25  42992  jm2.27c  43000  sqrtcval  43634  dvdivf  45923  dvdivbd  45924  itgsinexplem1  45955  itgsinexp  45956  wallispi2lem1  46072  wallispi2lem2  46073  wallispi2  46074  stirlinglem1  46075  stirlinglem3  46077  stirlinglem8  46082  stirlinglem10  46084  stirlinglem15  46089  rrxtopnfi  46288  hoiqssbllem2  46624  quad1  47624  itschlc0yqe  48765  itsclc0yqsollem1  48767  itsclc0yqsol  48769  itscnhlc0xyqsol  48770  itschlc0xyqsol1  48771  itschlc0xyqsol  48772  itsclc0xyqsolr  48774  2itscplem1  48783  2itscplem3  48785  itscnhlinecirc02plem1  48787  onetansqsecsq  49766  cotsqcscsq  49767