Theorem sqcld 14101

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

Syntax hints:   → wi 4   ∈ wcel 2121  (class class class)co 7360  ℂcc 11031  2c2 12231  ↑cexp 14018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-nn 12170  df-2 12239  df-n0 12433  df-z 12520  df-uz 12784  df-seq 13959  df-exp 14019

This theorem is referenced by:  mulsubdivbinom2  14219  muldivbinom2  14220  recval  15280  bhmafibid1cn  15423  bhmafibid2cn  15424  bhmafibid2  15426  arisum2  15821  fsumcube  16020  efi4p  16099  sincossq  16138  cos2t  16140  cos2tsin  16141  sqrt2irrlem  16210  pythagtriplem1  16782  pythagtriplem2  16783  pythagtriplem6  16787  pythagtriplem7  16788  pythagtriplem12  16792  pythagtriplem14  16794  4sqlem7  16910  4sqlem10  16913  4sqlem14  16924  4cphipval2  25231  csbren  25388  rrxmval  25394  rrxmetlem  25396  dvrecg  25962  dvmptdiv  25963  dveflem  25968  coskpi  26509  coseq1  26511  tanregt0  26525  efif1olem4  26531  tanarg  26605  lawcoslem1  26801  lawcos  26802  pythag  26803  ssscongptld  26808  chordthmlem3  26820  chordthmlem4  26821  chordthmlem5  26822  heron  26824  quad2  26825  quad  26826  dcubic1lem  26829  dcubic2  26830  dcubic1  26831  dcubic  26832  mcubic  26833  cubic2  26834  cubic  26835  binom4  26836  dquartlem1  26837  dquartlem2  26838  dquart  26839  quart1cl  26840  quart1lem  26841  quart1  26842  quartlem1  26843  quartlem2  26844  quartlem4  26846  quart  26847  asinlem3  26857  asinneg  26872  asinsin  26878  atandmcj  26895  efiatan2  26903  atandmtan  26906  cosatan  26907  cosatanne0  26908  dvatan  26921  cxp2limlem  26961  lgamgulmlem4  27017  basellem8  27073  lgsdir  27317  2sqlem4  27406  2sqlem11  27414  2sqn0  27419  2sqmod  27421  2sqnn  27424  addsq2reu  27425  2sqreultlem  27432  2sqreunnltlem  27435  2sqreulem2  27437  mulog2sumlem2  27520  mulog2sumlem3  27521  logsqvma  27527  selberglem1  27530  selberglem3  27532  selberg  27533  logdivbnd  27541  pntlemf  27590  pntlemk  27591  pntlemo  27592  ax5seglem1  29019  ax5seglem2  29020  ax5seglem6  29025  ax5seglem9  29028  axlowdimlem16  29048  axlowdimlem17  29049  4ipval2  30801  ipidsq  30803  cncph  30912  hhph  31271  eigvalcl  32054  pythagreim  32841  quad3d  32845  constrrtlc1  33928  constrrtcclem  33930  constrrtcc  33931  constrfin  33942  constrresqrtcl  33973  cos9thpiminplylem2  33979  cos9thpiminplylem3  33980  cos9thpinconstrlem1  33985  circlemethhgt  34839  hgt750leme  34854  qdiff  37702  sin2h  37992  cos2h  37993  tan2h  37994  dvtan  38052  dvasin  38086  dvacos  38087  areacirclem1  38090  areacirclem2  38091  areacirclem4  38093  areacirc  38095  ismrer1  38220  aks4d1p1p2  42570  aks4d1p1p6  42573  aks4d1p1p7  42574  aks4d1p1p5  42575  oddnumth  42803  nicomachus  42804  sumcubes  42805  readvrec2  42853  cu3addd  43145  3cubeslem2  43149  3cubeslem3l  43150  3cubeslem3r  43151  3cubeslem4  43153  pellexlem1  43289  pellexlem2  43290  pellexlem6  43294  pell1qrge1  43330  pell1qrgaplem  43333  rmspecsqrtnq  43366  rmxdbl  43399  jm2.18  43448  jm2.19lem1  43449  jm2.25  43459  jm2.27c  43467  sqrtcval  44100  dvdivf  46379  dvdivbd  46380  itgsinexplem1  46411  itgsinexp  46412  wallispi2lem1  46528  wallispi2lem2  46529  wallispi2  46530  stirlinglem1  46531  stirlinglem3  46533  stirlinglem8  46538  stirlinglem10  46540  stirlinglem15  46545  rrxtopnfi  46744  hoiqssbllem2  47080  sin3t  47348  cos3t  47349  sin5t  47355  quad1  48125  itschlc0yqe  49265  itsclc0yqsollem1  49267  itsclc0yqsol  49269  itscnhlc0xyqsol  49270  itschlc0xyqsol1  49271  itschlc0xyqsol  49272  itsclc0xyqsolr  49274  2itscplem1  49283  2itscplem3  49285  itscnhlinecirc02plem1  49287  onetansqsecsq  50265  cotsqcscsq  50266