Theorem sqcld 13612

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7182  ℂcc 10625  2c2 11783  ↑cexp 13533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pow 5242  ax-pr 5306  ax-un 7491  ax-cnex 10683  ax-resscn 10684  ax-1cn 10685  ax-icn 10686  ax-addcl 10687  ax-addrcl 10688  ax-mulcl 10689  ax-mulrcl 10690  ax-mulcom 10691  ax-addass 10692  ax-mulass 10693  ax-distr 10694  ax-i2m1 10695  ax-1ne0 10696  ax-1rid 10697  ax-rnegex 10698  ax-rrecex 10699  ax-cnre 10700  ax-pre-lttri 10701  ax-pre-lttrn 10702  ax-pre-ltadd 10703  ax-pre-mulgt0 10704

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3402  df-sbc 3686  df-csb 3801  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4222  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4807  df-iun 4893  df-br 5041  df-opab 5103  df-mpt 5121  df-tr 5147  df-id 5439  df-eprel 5444  df-po 5452  df-so 5453  df-fr 5493  df-we 5495  df-xp 5541  df-rel 5542  df-cnv 5543  df-co 5544  df-dm 5545  df-rn 5546  df-res 5547  df-ima 5548  df-pred 6139  df-ord 6185  df-on 6186  df-lim 6187  df-suc 6188  df-iota 6307  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7139  df-ov 7185  df-oprab 7186  df-mpo 7187  df-om 7612  df-2nd 7727  df-wrecs 7988  df-recs 8049  df-rdg 8087  df-er 8332  df-en 8568  df-dom 8569  df-sdom 8570  df-pnf 10767  df-mnf 10768  df-xr 10769  df-ltxr 10770  df-le 10771  df-sub 10962  df-neg 10963  df-nn 11729  df-2 11791  df-n0 11989  df-z 12075  df-uz 12337  df-seq 13473  df-exp 13534

This theorem is referenced by:  mulsubdivbinom2  13726  muldivbinom2  13727  recval  14784  bhmafibid1cn  14925  bhmafibid2cn  14926  bhmafibid2  14928  arisum2  15321  fsumcube  15518  efi4p  15594  sincossq  15633  cos2t  15635  cos2tsin  15636  sqrt2irrlem  15705  pythagtriplem1  16265  pythagtriplem2  16266  pythagtriplem6  16270  pythagtriplem7  16271  pythagtriplem12  16275  pythagtriplem14  16277  4sqlem7  16392  4sqlem10  16395  4sqlem14  16406  4cphipval2  24006  csbren  24163  rrxmval  24169  rrxmetlem  24171  dvrecg  24737  dvmptdiv  24738  dveflem  24743  coskpi  25279  coseq1  25281  tanregt0  25295  efif1olem4  25301  tanarg  25374  lawcoslem1  25565  lawcos  25566  pythag  25567  ssscongptld  25572  chordthmlem3  25584  chordthmlem4  25585  chordthmlem5  25586  heron  25588  quad2  25589  quad  25590  dcubic1lem  25593  dcubic2  25594  dcubic1  25595  dcubic  25596  mcubic  25597  cubic2  25598  cubic  25599  binom4  25600  dquartlem1  25601  dquartlem2  25602  dquart  25603  quart1cl  25604  quart1lem  25605  quart1  25606  quartlem1  25607  quartlem2  25608  quartlem4  25610  quart  25611  asinlem3  25621  asinneg  25636  asinsin  25642  atandmcj  25659  efiatan2  25667  atandmtan  25670  cosatan  25671  cosatanne0  25672  dvatan  25685  cxp2limlem  25725  lgamgulmlem4  25781  basellem8  25837  lgsdir  26080  2sqlem4  26169  2sqlem11  26177  2sqn0  26182  2sqmod  26184  2sqnn  26187  addsq2reu  26188  2sqreultlem  26195  2sqreunnltlem  26198  2sqreulem2  26200  mulog2sumlem2  26283  mulog2sumlem3  26284  logsqvma  26290  selberglem1  26293  selberglem3  26295  selberg  26296  logdivbnd  26304  pntlemf  26353  pntlemk  26354  pntlemo  26355  ax5seglem1  26886  ax5seglem2  26887  ax5seglem6  26892  ax5seglem9  26895  axlowdimlem16  26915  axlowdimlem17  26916  4ipval2  28655  ipidsq  28657  cncph  28766  hhph  29125  eigvalcl  29908  circlemethhgt  32205  hgt750leme  32220  sin2h  35422  cos2h  35423  tan2h  35424  dvtan  35482  dvasin  35516  dvacos  35517  areacirclem1  35520  areacirclem2  35521  areacirclem4  35523  areacirc  35525  ismrer1  35651  aks4d1p1p2  39729  aks4d1p1p6  39732  aks4d1p1p7  39733  aks4d1p1p5  39734  cu3addd  40114  3cubeslem2  40119  3cubeslem3l  40120  3cubeslem3r  40121  3cubeslem4  40123  pellexlem1  40263  pellexlem2  40264  pellexlem6  40268  pell1qrge1  40304  pell1qrgaplem  40307  rmspecsqrtnq  40340  rmxdbl  40373  jm2.18  40422  jm2.19lem1  40423  jm2.25  40433  jm2.27c  40441  sqrtcval  40834  dvdivf  43045  dvdivbd  43046  itgsinexplem1  43077  itgsinexp  43078  wallispi2lem1  43194  wallispi2lem2  43195  wallispi2  43196  stirlinglem1  43197  stirlinglem3  43199  stirlinglem8  43204  stirlinglem10  43206  stirlinglem15  43211  rrxtopnfi  43410  hoiqssbllem2  43743  quad1  44653  itschlc0yqe  45687  itsclc0yqsollem1  45689  itsclc0yqsol  45691  itscnhlc0xyqsol  45692  itschlc0xyqsol1  45693  itschlc0xyqsol  45694  itsclc0xyqsolr  45696  2itscplem1  45705  2itscplem3  45707  itscnhlinecirc02plem1  45709  onetansqsecsq  45963  cotsqcscsq  45964