MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sqvald Structured version   Unicode version

Theorem sqvald 11525
Description: Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
expcld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
sqvald  |-  ( ph  ->  ( A ^ 2 )  =  ( A  x.  A ) )

Proof of Theorem sqvald
StepHypRef Expression
1 expcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 sqval 11446 . 2  |-  ( A  e.  CC  ->  ( A ^ 2 )  =  ( A  x.  A
) )
31, 2syl 16 1  |-  ( ph  ->  ( A ^ 2 )  =  ( A  x.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726  (class class class)co 6084   CCcc 8993    x. cmul 9000   2c2 10054   ^cexp 11387
This theorem is referenced by:  cjmulval  11955  sqrlem5  12057  sqrlem6  12058  sqrlem7  12059  remsqsqr  12067  sqrmsq  12081  absid  12106  absre  12111  absresq  12112  abs1m  12144  abslem2  12148  sqreulem  12168  msqsqrd  12247  tanval3  12740  sincossq  12782  cos2t  12784  sqnprm  13103  isprm5  13117  coprimeprodsq  13188  pockthg  13279  4sqlem7  13317  4sqlem10  13320  mul4sqlem  13326  4sqlem12  13329  4sqlem15  13332  4sqlem16  13333  4sqlem17  13334  odadd2  15469  abvneg  15927  zrngunit  16770  cphsubrglem  19145  pjthlem1  19343  itgabs  19729  dvrec  19846  dveflem  19868  tangtx  20418  tanregt0  20446  tanarg  20519  cxpsqr  20599  lawcoslem1  20662  chordthmlem4  20681  quad2  20684  dcubic1lem  20688  dcubic1  20690  dcubic  20691  cubic2  20693  binom4  20695  dquartlem1  20696  dquartlem2  20697  dquart  20698  quart1lem  20700  asinsin  20737  cxp2limlem  20819  wilthlem1  20856  basellem8  20875  chpub  21009  bposlem2  21074  lgssq  21124  lgssq2  21125  lgsquad3  21150  2sqlem3  21155  2sqlem8  21161  chtppilimlem1  21172  rplogsumlem2  21184  dchrisum0lem1a  21185  dchrisum0lem1  21215  dchrisum0lem3  21218  mulog2sumlem1  21233  vmalogdivsum2  21237  logsqvma  21241  logdivbnd  21255  pntpbnd1a  21284  pntlemr  21301  pntlemf  21304  pntlemk  21305  pntlemo  21306  htthlem  22425  pjhthlem1  22898  cnlnadjlem7  23581  branmfn  23613  leopnmid  23646  lgamgulmlem3  24820  pdivsq  25373  brbtwn2  25849  colinearalglem4  25853  dvtan  26269  itgabsnc  26288  ftc1anclem3  26296  areacirclem1  26306  irrapxlem5  26903  pellexlem2  26907  pellexlem6  26911  rmxdbl  27016  jm2.18  27073  jm2.19lem1  27074  jm2.20nn  27082  jm2.25  27084  jm2.27c  27092  jm3.1lem2  27103  m1expeven  27715  wallispi2lem1  27810  stirlinglem1  27813  stirlinglem3  27815  stirlinglem10  27822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-cnex 9051  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071  ax-pre-mulgt0 9072
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-2nd 6353  df-riota 6552  df-recs 6636  df-rdg 6671  df-er 6908  df-en 7113  df-dom 7114  df-sdom 7115  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131  df-sub 9298  df-neg 9299  df-nn 10006  df-2 10063  df-n0 10227  df-z 10288  df-uz 10494  df-seq 11329  df-exp 11388
  Copyright terms: Public domain W3C validator