Theorem sqcld 14287

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  (class class class)co 7420  ℂcc 11198  2c2 12397  ↑cexp 14204

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-nn 12336  df-2 12405  df-n0 12607  df-z 12694  df-uz 12966  df-seq 14145  df-exp 14205

This theorem is used by:  mulsubdivbinom2  14406  muldivbinom2  14407  recval  15490  bhmafibid1cn  15633  bhmafibid2cn  15634  bhmafibid2  15636  arisum2  16030  fsumcube  16226  efi4p  16305  sincossq  16344  cos2t  16346  cos2tsin  16347  sqrt2irrlem  16416  pythagtriplem1  16994  pythagtriplem2  16995  pythagtriplem6  16999  pythagtriplem7  17000  pythagtriplem12  17004  pythagtriplem14  17006  4sqlem7  17122  4sqlem10  17125  4sqlem14  17136  4cphipval2  25563  csbren  25720  rrxmval  25726  rrxmetlem  25728  dvrecg  26293  dvmptdiv  26294  dveflem  26299  coskpi  26851  coseq1  26853  tanregt0  26867  efif1olem4  26873  tanarg  26947  lawcoslem1  27143  lawcos  27144  pythag  27145  ssscongptld  27150  chordthmlem3  27162  chordthmlem4  27163  chordthmlem5  27164  heron  27166  quad2  27167  quad  27168  dcubic1lem  27171  dcubic2  27172  dcubic1  27173  dcubic  27174  mcubic  27175  cubic2  27176  cubic  27177  binom4  27178  dquartlem1  27179  dquartlem2  27180  dquart  27181  quart1cl  27182  quart1lem  27183  quart1  27184  quartlem1  27185  quartlem2  27186  quartlem4  27188  quart  27189  asinlem3  27199  asinneg  27214  asinsin  27220  atandmcj  27237  efiatan2  27245  atandmtan  27248  cosatan  27249  cosatanne0  27250  dvatan  27263  cxp2limlem  27303  lgamgulmlem4  27359  basellem8  27415  lgsdir  27659  2sqlem4  27748  2sqlem11  27756  2sqn0  27761  2sqmod  27763  2sqnn  27766  addsq2reu  27767  2sqreultlem  27774  2sqreunnltlem  27777  2sqreulem2  27779  mulog2sumlem2  27862  mulog2sumlem3  27863  logsqvma  27869  selberglem1  27872  selberglem3  27874  selberg  27875  logdivbnd  27883  pntlemf  27932  pntlemk  27933  pntlemo  27934  ax5seglem1  29506  ax5seglem2  29507  ax5seglem6  29512  ax5seglem9  29515  axlowdimlem16  29535  axlowdimlem17  29536  4ipval2  31310  ipidsq  31312  cncph  31421  hhph  31780  eigvalcl  32563  pythagreim  33337  quad3d  33341  constrrtlc1  34364  constrrtcclem  34366  constrrtcc  34367  constrfin  34378  constrresqrtcl  34409  cos9thpiminplylem2  34415  cos9thpiminplylem3  34416  cos9thpinconstrlem1  34421  circlemethhgt  35272  hgt750leme  35287  qdiff  38249  sin2h  38534  cos2h  38535  tan2h  38536  dvtan  38589  dvasin  38623  dvacos  38624  areacirclem1  38627  areacirclem2  38628  areacirclem4  38630  areacirc  38632  ismrer1  38773  aks4d1p1p2  43121  aks4d1p1p6  43124  aks4d1p1p7  43125  aks4d1p1p5  43126  quadfac  43256  oddnumth  43369  nicomachus  43370  sumcubes  43371  readvrec2  43413  cu3addd  43692  3cubeslem2  43696  3cubeslem3l  43697  3cubeslem3r  43698  3cubeslem4  43700  pellexlem1  43836  pellexlem2  43837  pellexlem6  43841  pell1qrge1  43877  pell1qrgaplem  43880  rmspecsqrtnq  43913  rmxdbl  43946  jm2.18  43995  jm2.19lem1  43996  jm2.25  44006  jm2.27c  44014  sqrtcval  44641  dvdivf  46932  dvdivbd  46933  itgsinexplem1  46964  itgsinexp  46965  wallispi2lem1  47081  wallispi2lem2  47082  wallispi2  47083  stirlinglem1  47084  stirlinglem3  47086  stirlinglem8  47091  stirlinglem10  47093  stirlinglem15  47098  rrxtopnfi  47297  hoiqssbllem2  47633  sin3t  47917  cos3t  47918  sin5t  47924  quad1  48718  itschlc0yqe  49872  itsclc0yqsollem1  49874  itsclc0yqsol  49876  itscnhlc0xyqsol  49877  itschlc0xyqsol1  49878  itschlc0xyqsol  49879  itsclc0xyqsolr  49881  2itscplem1  49890  2itscplem3  49892  itscnhlinecirc02plem1  49894  onetansqsecsq  50854  cotsqcscsq  50855  dvcot  50858