Theorem sqvald 14096

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027   · cmul 11034  2c2 12227  ↑cexp 14014

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-2 12235  df-n0 12429  df-z 12516  df-uz 12780  df-seq 13955  df-exp 14015

This theorem is referenced by:  sqoddm1div8  14196  cjmulval  15098  01sqrexlem5  15199  01sqrexlem6  15200  01sqrexlem7  15201  remsqsqrt  15209  sqrtmsq  15223  absid  15249  absre  15254  absresq  15255  abs1m  15289  abslem2  15293  sqreulem  15313  msqsqrtd  15396  tanval3  16092  sincossq  16134  cos2t  16136  sqrt2irrlem  16206  sqnprm  16663  isprm5  16668  coprimeprodsq  16770  pockthg  16868  4sqlem7  16906  4sqlem10  16909  mul4sqlem  16915  4sqlem12  16918  4sqlem15  16921  4sqlem16  16922  4sqlem17  16923  odadd2  19815  abvneg  20798  zringunit  21441  cphsubrglem  25162  rrxnm  25376  pjthlem1  25422  itgabs  25820  dvrec  25940  dvmptdiv  25959  dveflem  25964  tangtx  26487  tanregt0  26521  tanarg  26601  cxpsqrt  26685  lawcoslem1  26797  chordthmlem4  26817  heron  26820  quad2  26821  dcubic1lem  26825  dcubic1  26827  dcubic  26828  cubic2  26830  binom4  26832  dquartlem1  26833  dquartlem2  26834  dquart  26835  quart1lem  26837  asinsin  26874  cxp2limlem  26957  lgamgulmlem3  27012  wilthlem1  27049  basellem8  27069  chpub  27201  bposlem2  27266  lgssq  27318  lgssq2  27319  lgsquad3  27368  2sqlem3  27401  2sqlem8  27407  2sqmod  27417  chtppilimlem1  27454  rplogsumlem2  27466  dchrisum0lem1a  27467  dchrisum0lem1  27497  dchrisum0lem3  27500  mulog2sumlem1  27515  vmalogdivsum2  27519  logsqvma  27523  logdivbnd  27537  pntpbnd1a  27566  pntlemr  27583  pntlemf  27586  pntlemk  27587  pntlemo  27588  brbtwn2  28992  colinearalglem4  28996  htthlem  31006  pjhthlem1  31480  cnlnadjlem7  32162  branmfn  32194  leopnmid  32227  quad3d  32841  constrrtlc1  33916  constrrtcclem  33918  constrrtcc  33919  hgt750lemf  34837  hgt750leme  34842  dvtan  38037  itgabsnc  38056  ftc1anclem3  38062  areacirclem1  38075  3lexlogpow2ineq2  42544  aks6d1c7lem1  42665  nicomachus  42789  readvrec2  42838  3cubeslem1  43133  3cubeslem2  43134  3cubeslem3l  43135  irrapxlem5  43271  pellexlem2  43275  pellexlem6  43279  rmxdbl  43384  jm2.18  43433  jm2.19lem1  43434  jm2.20nn  43442  jm2.25  43444  jm2.27c  43452  jm3.1lem2  43463  int-sqdefd  44625  int-sqgeq0d  44630  sqrlearg  45998  dvdivf  46365  wallispi2lem1  46514  stirlinglem1  46517  stirlinglem3  46519  stirlinglem10  46526  smfmullem1  47234  sin3t  47334  cos3t  47335  2timesltsq  47841  2timesltsqm1  47842  nprmmul3  48004  fmtnorec2lem  48020  fmtnorec3  48026  modexp2m1d  48090  nprmdvdsfacm1lem1  48098  itschlc0yqe  49251  itscnhlc0xyqsol  49256  itschlc0xyqsol1  49257  itschlc0xyqsol  49258  itsclc0xyqsolr  49260