Theorem sqcld 14159

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

Syntax hints:   → wi 4   ∈ wcel 2144  (class class class)co 7398  ℂcc 11073  2c2 12274  ↑cexp 14076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-om 7849  df-2nd 7973  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-sub 11418  df-neg 11419  df-nn 12213  df-2 12282  df-n0 12484  df-z 12571  df-uz 12842  df-seq 14017  df-exp 14077

This theorem is referenced by:  mulsubdivbinom2  14277  muldivbinom2  14278  recval  15352  bhmafibid1cn  15495  bhmafibid2cn  15496  bhmafibid2  15498  arisum2  15893  fsumcube  16092  efi4p  16171  sincossq  16210  cos2t  16212  cos2tsin  16213  sqrt2irrlem  16282  pythagtriplem1  16854  pythagtriplem2  16855  pythagtriplem6  16859  pythagtriplem7  16860  pythagtriplem12  16864  pythagtriplem14  16866  4sqlem7  16982  4sqlem10  16985  4sqlem14  16996  4cphipval2  25306  csbren  25463  rrxmval  25469  rrxmetlem  25471  dvrecg  26037  dvmptdiv  26038  dveflem  26043  coskpi  26590  coseq1  26592  tanregt0  26606  efif1olem4  26612  tanarg  26686  lawcoslem1  26882  lawcos  26883  pythag  26884  ssscongptld  26889  chordthmlem3  26901  chordthmlem4  26902  chordthmlem5  26903  heron  26905  quad2  26906  quad  26907  dcubic1lem  26910  dcubic2  26911  dcubic1  26912  dcubic  26913  mcubic  26914  cubic2  26915  cubic  26916  binom4  26917  dquartlem1  26918  dquartlem2  26919  dquart  26920  quart1cl  26921  quart1lem  26922  quart1  26923  quartlem1  26924  quartlem2  26925  quartlem4  26927  quart  26928  asinlem3  26938  asinneg  26953  asinsin  26959  atandmcj  26976  efiatan2  26984  atandmtan  26987  cosatan  26988  cosatanne0  26989  dvatan  27002  cxp2limlem  27042  lgamgulmlem4  27098  basellem8  27154  lgsdir  27398  2sqlem4  27487  2sqlem11  27495  2sqn0  27500  2sqmod  27502  2sqnn  27505  addsq2reu  27506  2sqreultlem  27513  2sqreunnltlem  27516  2sqreulem2  27518  mulog2sumlem2  27601  mulog2sumlem3  27602  logsqvma  27608  selberglem1  27611  selberglem3  27613  selberg  27614  logdivbnd  27622  pntlemf  27671  pntlemk  27672  pntlemo  27673  ax5seglem1  29131  ax5seglem2  29132  ax5seglem6  29137  ax5seglem9  29140  axlowdimlem16  29160  axlowdimlem17  29161  4ipval2  30913  ipidsq  30915  cncph  31024  hhph  31383  eigvalcl  32166  pythagreim  32949  quad3d  32953  constrrtlc1  34031  constrrtcclem  34033  constrrtcc  34034  constrfin  34045  constrresqrtcl  34076  cos9thpiminplylem2  34082  cos9thpiminplylem3  34083  cos9thpinconstrlem1  34088  circlemethhgt  34939  hgt750leme  34954  qdiff  37824  sin2h  38114  cos2h  38115  tan2h  38116  dvtan  38174  dvasin  38208  dvacos  38209  areacirclem1  38212  areacirclem2  38213  areacirclem4  38215  areacirc  38217  ismrer1  38342  aks4d1p1p2  42692  aks4d1p1p6  42695  aks4d1p1p7  42696  aks4d1p1p5  42697  oddnumth  42925  nicomachus  42926  sumcubes  42927  readvrec2  42975  cu3addd  43267  3cubeslem2  43271  3cubeslem3l  43272  3cubeslem3r  43273  3cubeslem4  43275  pellexlem1  43411  pellexlem2  43412  pellexlem6  43416  pell1qrge1  43452  pell1qrgaplem  43455  rmspecsqrtnq  43488  rmxdbl  43521  jm2.18  43570  jm2.19lem1  43571  jm2.25  43581  jm2.27c  43589  sqrtcval  44222  dvdivf  46501  dvdivbd  46502  itgsinexplem1  46533  itgsinexp  46534  wallispi2lem1  46650  wallispi2lem2  46651  wallispi2  46652  stirlinglem1  46653  stirlinglem3  46655  stirlinglem8  46660  stirlinglem10  46662  stirlinglem15  46667  rrxtopnfi  46866  hoiqssbllem2  47202  sin3t  47470  cos3t  47471  sin5t  47477  quad1  48247  itschlc0yqe  49387  itsclc0yqsollem1  49389  itsclc0yqsol  49391  itscnhlc0xyqsol  49392  itschlc0xyqsol1  49393  itschlc0xyqsol  49394  itsclc0xyqsolr  49396  2itscplem1  49405  2itscplem3  49407  itscnhlinecirc02plem1  49409  onetansqsecsq  50387  cotsqcscsq  50388