Theorem sqvald 14112

Description: Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
expcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
sqvald	⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴))

Proof of Theorem sqvald

Step	Hyp	Ref	Expression
1		expcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		sqval 14084	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7411  ℂcc 11110   · cmul 11117  2c2 12271  ↑cexp 14031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-n0 12477  df-z 12563  df-uz 12827  df-seq 13971  df-exp 14032

This theorem is referenced by:  sqoddm1div8  14210  cjmulval  15096  01sqrexlem5  15197  01sqrexlem6  15198  01sqrexlem7  15199  remsqsqrt  15207  sqrtmsq  15221  absid  15247  absre  15252  absresq  15253  abs1m  15286  abslem2  15290  sqreulem  15310  msqsqrtd  15391  tanval3  16081  sincossq  16123  cos2t  16125  sqrt2irrlem  16195  sqnprm  16643  isprm5  16648  prmdvdssqOLD  16660  coprimeprodsq  16745  pockthg  16843  4sqlem7  16881  4sqlem10  16884  mul4sqlem  16890  4sqlem12  16893  4sqlem15  16896  4sqlem16  16897  4sqlem17  16898  odadd2  19758  abvneg  20585  zringunit  21237  cphsubrglem  24918  rrxnm  25132  pjthlem1  25178  itgabs  25576  dvrec  25696  dvmptdiv  25715  dveflem  25720  tangtx  26239  tanregt0  26272  tanarg  26351  cxpsqrt  26435  lawcoslem1  26544  chordthmlem4  26564  heron  26567  quad2  26568  dcubic1lem  26572  dcubic1  26574  dcubic  26575  cubic2  26577  binom4  26579  dquartlem1  26580  dquartlem2  26581  dquart  26582  quart1lem  26584  asinsin  26621  cxp2limlem  26704  lgamgulmlem3  26759  wilthlem1  26796  basellem8  26816  chpub  26947  bposlem2  27012  lgssq  27064  lgssq2  27065  lgsquad3  27114  2sqlem3  27147  2sqlem8  27153  2sqmod  27163  chtppilimlem1  27200  rplogsumlem2  27212  dchrisum0lem1a  27213  dchrisum0lem1  27243  dchrisum0lem3  27246  mulog2sumlem1  27261  vmalogdivsum2  27265  logsqvma  27269  logdivbnd  27283  pntpbnd1a  27312  pntlemr  27329  pntlemf  27332  pntlemk  27333  pntlemo  27334  brbtwn2  28418  colinearalglem4  28422  htthlem  30425  pjhthlem1  30899  cnlnadjlem7  31581  branmfn  31613  leopnmid  31646  hgt750lemf  33951  hgt750leme  33956  dvtan  36841  itgabsnc  36860  ftc1anclem3  36866  areacirclem1  36879  3lexlogpow2ineq2  41230  nicomachus  41512  3cubeslem1  41724  3cubeslem2  41725  3cubeslem3l  41726  irrapxlem5  41866  pellexlem2  41870  pellexlem6  41874  rmxdbl  41980  jm2.18  42029  jm2.19lem1  42030  jm2.20nn  42038  jm2.25  42040  jm2.27c  42048  jm3.1lem2  42059  int-sqdefd  43235  int-sqgeq0d  43240  sqrlearg  44565  dvdivf  44937  wallispi2lem1  45086  stirlinglem1  45089  stirlinglem3  45091  stirlinglem10  45098  smfmullem1  45806  fmtnorec2lem  46509  fmtnorec3  46515  modexp2m1d  46579  itschlc0yqe  47534  itscnhlc0xyqsol  47539  itschlc0xyqsol1  47540  itschlc0xyqsol  47541  itsclc0xyqsolr  47543